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/logic-synthesis/normalized-count.b.opb
MD5SUMf13ba9c997276002b5bd6db1f679a6f5
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 24
Optimality of the best value was proved YES
Number of terms in the objective function 467
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 467
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 467
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark11.9012
Number of variables466
Total number of constraints694
Number of constraints which are clauses694
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 constraint2
Maximum length of a constraint78

Trace number 908

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906528 kB
Buffers:         37184 kB
Cached:          61188 kB
SwapCached:        908 kB
Active:          83572 kB
Inactive:        17676 kB
HighTotal:      131008 kB
HighFree:        73668 kB
LowTotal:       903652 kB
LowFree:        832860 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21136 kB
Committed_AS:    93168 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 13:04:27 (client local time) WITH STATUS 10 IN 1209.89 SECONDS
stats: 2407 7 1209.89 10

Solver Data

c Parsing PB file...
c Converting 694 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 |     694    17335 |     231       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 31
c ---[   0]---> Sorter-cost:17658     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19647    61494 |    6549       0        0     nan |  0.000 % |
c |       101 |   19445    61064 |    7203      89     3487    39.2 |  1.289 % |
c |       257 |   19445    61064 |    7924     245     9767    39.9 |  1.289 % |
c |       484 |   19445    61064 |    8716     472    31182    66.1 |  1.289 % |
c |       822 |   19445    61064 |    9588     810    74289    91.7 |  1.289 % |
c ==============================================================================
c Found solution: 28
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1166 |   19469    61124 |    6489    1154   114761    99.4 |  1.289 % |
c |      1267 |   19469    61124 |    7137    1255   124729    99.4 |  1.311 % |
c |      1418 |   19469    61124 |    7851    1406   135092    96.1 |  1.311 % |
c |      1643 |   19454    61093 |    8636    1630   144695    88.8 |  1.373 % |
c |      1982 |   19454    61093 |    9500    1969   167082    84.9 |  1.373 % |
c |      2489 |   19454    61093 |   10450    2476   202121    81.6 |  1.373 % |
c |      3249 |   19454    61093 |   11495    3236   266695    82.4 |  1.373 % |
c ==============================================================================
c Found solution: 27
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4035 |   19146    60373 |    6382    3959   296660    74.9 |  1.373 % |
c |      4135 |   19146    60373 |    7020    4059   303620    74.8 |  3.040 % |
c |      4285 |   19146    60373 |    7722    4209   313768    74.5 |  3.040 % |
c |      4510 |   19146    60373 |    8494    4434   325949    73.5 |  3.040 % |
c |      4848 |   19101    60270 |    9343    4770   341762    71.6 |  3.265 % |
c |      5355 |   19101    60270 |   10278    5277   366069    69.4 |  3.265 % |
c ==============================================================================
c Found solution: 26
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5912 |   19115    60306 |    6371    5834   399340    68.5 |  3.265 % |
c |      6015 |   19115    60306 |    7008    5937   406999    68.6 |  3.278 % |
c |      6166 |   19100    60273 |    7708    6087   413641    68.0 |  3.348 % |
c |      6393 |   19100    60273 |    8479    6314   428942    67.9 |  3.348 % |
c |      6730 |   19100    60273 |    9327    6651   444512    66.8 |  3.348 % |
c |      7237 |   19100    60273 |   10260    7158   469534    65.6 |  3.348 % |
c |      7996 |   19100    60273 |   11286    7917   505459    63.8 |  3.348 % |
c |      9135 |   19100    60273 |   12415    9056   570860    63.0 |  3.348 % |
c |     10843 |   19100    60273 |   13656   10764   693406    64.4 |  3.348 % |
c |     13407 |   19100    60273 |   15022   13328   804791    60.4 |  3.348 % |
c |     17252 |   19100    60273 |   16524    9015   600405    66.6 |  3.348 % |
c |     23019 |   19100    60273 |   18177   14782  1097525    74.2 |  3.348 % |
c ==============================================================================
c Found solution: 25
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27329 |   19083    60230 |    6361   19088  1430862    75.0 |  3.348 % |
c |     27430 |   19083    60230 |    6997    4873   311386    63.9 |  3.486 % |
c |     27581 |   19083    60230 |    7696    5024   318135    63.3 |  3.486 % |
c |     27807 |   18979    59989 |    8466    5235   330614    63.2 |  4.006 % |
c |     28145 |   18979    59989 |    9313    5573   345816    62.1 |  4.006 % |
c |     28651 |   18979    59989 |   10244    6079   368825    60.7 |  4.006 % |
c |     29411 |   18979    59989 |   11268    6839   414066    60.5 |  4.006 % |
c |     30551 |   18979    59989 |   12395    7979   477554    59.9 |  4.006 % |
c |     32259 |   18979    59989 |   13635    9687   588178    60.7 |  4.006 % |
c |     34821 |   18979    59989 |   14998   12249   741563    60.5 |  4.006 % |
c ==============================================================================
c Found solution: 24
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38313 |   18993    60024 |    6331   15741   911578    57.9 |  4.006 % |
c |     38413 |   18993    60024 |    6964    4036   167384    41.5 |  4.018 % |
c |     38563 |   18993    60024 |    7660    4186   172590    41.2 |  4.018 % |
c |     38791 |   18993    60024 |    8426    4414   179565    40.7 |  4.018 % |
c |     39128 |   18993    60024 |    9269    4751   186680    39.3 |  4.018 % |
c |     39638 |   18993    60024 |   10196    5261   201797    38.4 |  4.018 % |
c |     40398 |   18993    60024 |   11215    6021   227834    37.8 |  4.018 % |
c |     41537 |   18993    60024 |   12337    7160   281186    39.3 |  4.018 % |
c |     43245 |   18993    60024 |   13571    8868   361128    40.7 |  4.018 % |
c |     45807 |   18993    60024 |   14928   11430   472504    41.3 |  4.018 % |
c |     49652 |   18993    60024 |   16420   15275   637818    41.8 |  4.018 % |
c |     55420 |   18993    60024 |   18063   12289   467797    38.1 |  4.018 % |
c |     64073 |   18993    60024 |   19869   11350   439625    38.7 |  4.018 % |
c |     77047 |   18993    60024 |   21856   13267   640705    48.3 |  4.018 % |
c |     96509 |   18993    60024 |   24041   21195   872945    41.2 |  4.018 % |
c |    125704 |   18993    60024 |   26446   25028  1205586    48.2 |  4.018 % |
c |    169495 |   18978    59993 |   29090   27177  1048115    38.6 |  4.072 % |
c |    235179 |   18978    59993 |   31999   25525  1312075    51.4 |  4.072 % |
c |    333706 |   18978    59993 |   35199   32412  1339748    41.3 |  4.072 % |
c |    481495 |   18978    59993 |   38719   33150  1162730    35.1 |  4.072 % |

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/21739/stat): 21739 (minisat+_script) R 21738 21739 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1726267886 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21739/statm): 174 3 169 147 0 27 0
[pid=21739] 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=21740
New process pid=21741
New process pid=21742
execve syscall for /bin/sed executable
One traced child (pid=21741) 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=21742) exited with status: 0
One traced child (pid=21740) exited with status: 0
New process pid=21743
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-count.b.opb

[startup+10.0031 s]
Raw data (loadavg): 0.87 0.94 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 1700 0 0 0 977 9 0 0 25 0 1 0 1726267891 7729152 1683 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 1887 1683 145 145 0 1742 0
[pid=21743] vsize: 7548
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 9672

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.94 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2106 0 0 0 1970 12 0 0 25 0 1 0 1726267891 9400320 2089 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 2295 2089 145 145 0 2150 0
[pid=21743] vsize: 9180
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 11304

[startup+30.0057 s]
Raw data (loadavg): 0.91 0.94 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2425 0 0 0 2964 14 0 0 25 0 1 0 1726267891 10698752 2408 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 2612 2408 145 145 0 2467 0
[pid=21743] vsize: 10448
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 12572

[startup+40.0065 s]
Raw data (loadavg): 0.92 0.94 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2776 0 0 0 3958 17 0 0 25 0 1 0 1726267891 12189696 2759 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 2976 2759 145 145 0 2831 0
[pid=21743] vsize: 11904
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 14028

[startup+50.0083 s]
Raw data (loadavg): 0.93 0.94 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 4955 18 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 14480

[startup+60.0091 s]
Raw data (loadavg): 0.94 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 5954 19 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 14480

[startup+70.0109 s]
Raw data (loadavg): 0.95 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 6954 19 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 14480

[startup+80.0127 s]
Raw data (loadavg): 0.96 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 7954 19 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 79.73
Current children cumulated vsize (Kb) 14480

[startup+90.0134 s]
Raw data (loadavg): 0.96 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 8954 19 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 14480

[startup+100.014 s]
Raw data (loadavg): 0.97 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 9954 19 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 14480

[startup+110.015 s]
Raw data (loadavg): 0.97 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 10953 20 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 14480

[startup+120.017 s]
Raw data (loadavg): 0.98 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2890 0 0 0 11953 20 0 0 25 0 1 0 1726267891 12652544 2873 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2873 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 14480

[startup+130.018 s]
Raw data (loadavg): 0.98 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2893 0 0 0 12953 21 0 0 25 0 1 0 1726267891 12652544 2876 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2876 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 129.74
Current children cumulated vsize (Kb) 14480

[startup+140.018 s]
Raw data (loadavg): 0.98 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2893 0 0 0 13953 21 0 0 25 0 1 0 1726267891 12652544 2876 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2876 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 139.74
Current children cumulated vsize (Kb) 14480

[startup+150.02 s]
Raw data (loadavg): 0.98 0.95 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2893 0 0 0 14953 21 0 0 25 0 1 0 1726267891 12652544 2876 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2876 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 149.74
Current children cumulated vsize (Kb) 14480

[startup+160.021 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2894 0 0 0 15953 21 0 0 25 0 1 0 1726267891 12652544 2877 4294967295 134512640 135094434 3221224448 3221223104 134556043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2877 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 159.74
Current children cumulated vsize (Kb) 14480

[startup+170.022 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2894 0 0 0 16953 21 0 0 25 0 1 0 1726267891 12652544 2877 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3089 2877 145 145 0 2944 0
[pid=21743] vsize: 12356
Current children cumulated CPU time (s) 169.74
Current children cumulated vsize (Kb) 14480

[startup+180.023 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2905 0 0 0 17953 21 0 0 25 0 1 0 1726267891 12718080 2888 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3105 2888 145 145 0 2960 0
[pid=21743] vsize: 12420
Current children cumulated CPU time (s) 179.74
Current children cumulated vsize (Kb) 14544

[startup+190.023 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2917 0 0 0 18953 22 0 0 25 0 1 0 1726267891 12783616 2900 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3121 2900 145 145 0 2976 0
[pid=21743] vsize: 12484
Current children cumulated CPU time (s) 189.75
Current children cumulated vsize (Kb) 14608

[startup+200.024 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2917 0 0 0 19952 22 0 0 25 0 1 0 1726267891 12783616 2900 4294967295 134512640 135094434 3221224448 3221223136 134554717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3121 2900 145 145 0 2976 0
[pid=21743] vsize: 12484
Current children cumulated CPU time (s) 199.74
Current children cumulated vsize (Kb) 14608

[startup+210.025 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 2942 0 0 0 20952 22 0 0 25 0 1 0 1726267891 12890112 2925 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3147 2925 145 145 0 3002 0
[pid=21743] vsize: 12588
Current children cumulated CPU time (s) 209.74
Current children cumulated vsize (Kb) 14712

[startup+220.027 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3074 0 0 0 21951 23 0 0 25 0 1 0 1726267891 13426688 3057 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3278 3057 145 145 0 3133 0
[pid=21743] vsize: 13112
Current children cumulated CPU time (s) 219.74
Current children cumulated vsize (Kb) 15236

[startup+230.028 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3077 0 0 0 22950 24 0 0 25 0 1 0 1726267891 13443072 3060 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3282 3060 145 145 0 3137 0
[pid=21743] vsize: 13128
Current children cumulated CPU time (s) 229.74
Current children cumulated vsize (Kb) 15252

[startup+240.028 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3091 0 0 0 23950 24 0 0 25 0 1 0 1726267891 13508608 3074 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3298 3074 145 145 0 3153 0
[pid=21743] vsize: 13192
Current children cumulated CPU time (s) 239.74
Current children cumulated vsize (Kb) 15316

[startup+250.029 s]
Raw data (loadavg): 0.99 0.96 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3166 0 0 0 24949 24 0 0 25 0 1 0 1726267891 13828096 3149 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3376 3149 145 145 0 3231 0
[pid=21743] vsize: 13504
Current children cumulated CPU time (s) 249.73
Current children cumulated vsize (Kb) 15628

[startup+260.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3227 0 0 0 25948 25 0 0 25 0 1 0 1726267891 14086144 3210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3439 3210 145 145 0 3294 0
[pid=21743] vsize: 13756
Current children cumulated CPU time (s) 259.73
Current children cumulated vsize (Kb) 15880

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3253 0 0 0 26948 25 0 0 25 0 1 0 1726267891 14233600 3236 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3475 3236 145 145 0 3330 0
[pid=21743] vsize: 13900
Current children cumulated CPU time (s) 269.73
Current children cumulated vsize (Kb) 16024

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3253 0 0 0 27948 25 0 0 25 0 1 0 1726267891 14233600 3236 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3475 3236 145 145 0 3330 0
[pid=21743] vsize: 13900
Current children cumulated CPU time (s) 279.73
Current children cumulated vsize (Kb) 16024

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3253 0 0 0 28948 25 0 0 25 0 1 0 1726267891 14233600 3236 4294967295 134512640 135094434 3221224448 3221223040 134556969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3475 3236 145 145 0 3330 0
[pid=21743] vsize: 13900
Current children cumulated CPU time (s) 289.73
Current children cumulated vsize (Kb) 16024

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3262 0 0 0 29949 25 0 0 25 0 1 0 1726267891 14282752 3245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3487 3245 145 145 0 3342 0
[pid=21743] vsize: 13948
Current children cumulated CPU time (s) 299.74
Current children cumulated vsize (Kb) 16072

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3264 0 0 0 30949 25 0 0 25 0 1 0 1726267891 14282752 3247 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3487 3247 145 145 0 3342 0
[pid=21743] vsize: 13948
Current children cumulated CPU time (s) 309.74
Current children cumulated vsize (Kb) 16072

[startup+320.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3276 0 0 0 31949 25 0 0 25 0 1 0 1726267891 14348288 3259 4294967295 134512640 135094434 3221224448 3221223084 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3503 3259 145 145 0 3358 0
[pid=21743] vsize: 14012
Current children cumulated CPU time (s) 319.74
Current children cumulated vsize (Kb) 16136

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3292 0 0 0 32949 25 0 0 25 0 1 0 1726267891 14430208 3275 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3523 3275 145 145 0 3378 0
[pid=21743] vsize: 14092
Current children cumulated CPU time (s) 329.74
Current children cumulated vsize (Kb) 16216

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3299 0 0 0 33949 25 0 0 25 0 1 0 1726267891 14462976 3282 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3531 3282 145 145 0 3386 0
[pid=21743] vsize: 14124
Current children cumulated CPU time (s) 339.74
Current children cumulated vsize (Kb) 16248

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3310 0 0 0 34949 25 0 0 25 0 1 0 1726267891 14528512 3293 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3547 3293 145 145 0 3402 0
[pid=21743] vsize: 14188
Current children cumulated CPU time (s) 349.74
Current children cumulated vsize (Kb) 16312

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3314 0 0 0 35949 25 0 0 25 0 1 0 1726267891 14528512 3297 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3547 3297 145 145 0 3402 0
[pid=21743] vsize: 14188
Current children cumulated CPU time (s) 359.74
Current children cumulated vsize (Kb) 16312

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3320 0 0 0 36950 25 0 0 25 0 1 0 1726267891 14561280 3303 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3555 3303 145 145 0 3410 0
[pid=21743] vsize: 14220
Current children cumulated CPU time (s) 369.75
Current children cumulated vsize (Kb) 16344

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3328 0 0 0 37950 25 0 0 25 0 1 0 1726267891 14594048 3311 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3563 3311 145 145 0 3418 0
[pid=21743] vsize: 14252
Current children cumulated CPU time (s) 379.75
Current children cumulated vsize (Kb) 16376

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3338 0 0 0 38950 25 0 0 25 0 1 0 1726267891 14659584 3321 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3579 3321 145 145 0 3434 0
[pid=21743] vsize: 14316
Current children cumulated CPU time (s) 389.75
Current children cumulated vsize (Kb) 16440

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3357 0 0 0 39950 26 0 0 25 0 1 0 1726267891 14757888 3340 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3603 3340 145 145 0 3458 0
[pid=21743] vsize: 14412
Current children cumulated CPU time (s) 399.76
Current children cumulated vsize (Kb) 16536

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3381 0 0 0 40949 26 0 0 25 0 1 0 1726267891 14856192 3364 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3627 3364 145 145 0 3482 0
[pid=21743] vsize: 14508
Current children cumulated CPU time (s) 409.75
Current children cumulated vsize (Kb) 16632

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3381 0 0 0 41950 26 0 0 25 0 1 0 1726267891 14856192 3364 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3627 3364 145 145 0 3482 0
[pid=21743] vsize: 14508
Current children cumulated CPU time (s) 419.76
Current children cumulated vsize (Kb) 16632

[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3408 0 0 0 42950 26 0 0 25 0 1 0 1726267891 14954496 3391 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3651 3391 145 145 0 3506 0
[pid=21743] vsize: 14604
Current children cumulated CPU time (s) 429.76
Current children cumulated vsize (Kb) 16728

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3517 0 0 0 43948 27 0 0 25 0 1 0 1726267891 15400960 3500 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3760 3500 145 145 0 3615 0
[pid=21743] vsize: 15040
Current children cumulated CPU time (s) 439.75
Current children cumulated vsize (Kb) 17164

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3666 0 0 0 44945 28 0 0 25 0 1 0 1726267891 16023552 3649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3912 3649 145 145 0 3767 0
[pid=21743] vsize: 15648
Current children cumulated CPU time (s) 449.73
Current children cumulated vsize (Kb) 17772

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3666 0 0 0 45946 28 0 0 25 0 1 0 1726267891 16023552 3649 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3912 3649 145 145 0 3767 0
[pid=21743] vsize: 15648
Current children cumulated CPU time (s) 459.74
Current children cumulated vsize (Kb) 17772

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3666 0 0 0 46946 28 0 0 25 0 1 0 1726267891 16023552 3649 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3912 3649 145 145 0 3767 0
[pid=21743] vsize: 15648
Current children cumulated CPU time (s) 469.74
Current children cumulated vsize (Kb) 17772

[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3676 0 0 0 47946 28 0 0 25 0 1 0 1726267891 16072704 3659 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3924 3659 145 145 0 3779 0
[pid=21743] vsize: 15696
Current children cumulated CPU time (s) 479.74
Current children cumulated vsize (Kb) 17820

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3690 0 0 0 48946 28 0 0 25 0 1 0 1726267891 16138240 3673 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3940 3673 145 145 0 3795 0
[pid=21743] vsize: 15760
Current children cumulated CPU time (s) 489.74
Current children cumulated vsize (Kb) 17884

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3690 0 0 0 49946 28 0 0 25 0 1 0 1726267891 16138240 3673 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3940 3673 145 145 0 3795 0
[pid=21743] vsize: 15760
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 17884

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3690 0 0 0 50946 29 0 0 25 0 1 0 1726267891 16138240 3673 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3940 3673 145 145 0 3795 0
[pid=21743] vsize: 15760
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 17884

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3717 0 0 0 51946 29 0 0 25 0 1 0 1726267891 16302080 3700 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 3980 3700 145 145 0 3835 0
[pid=21743] vsize: 15920
Current children cumulated CPU time (s) 519.75
Current children cumulated vsize (Kb) 18044

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3732 0 0 0 52946 29 0 0 25 0 1 0 1726267891 16367616 3715 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 3996 3715 145 145 0 3851 0
[pid=21743] vsize: 15984
Current children cumulated CPU time (s) 529.75
Current children cumulated vsize (Kb) 18108

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3866 0 0 0 53944 29 0 0 25 0 1 0 1726267891 17051648 3849 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4163 3849 145 145 0 4018 0
[pid=21743] vsize: 16652
Current children cumulated CPU time (s) 539.73
Current children cumulated vsize (Kb) 18776

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3872 0 0 0 54944 29 0 0 25 0 1 0 1726267891 17076224 3855 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4169 3855 145 145 0 4024 0
[pid=21743] vsize: 16676
Current children cumulated CPU time (s) 549.73
Current children cumulated vsize (Kb) 18800

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3876 0 0 0 55944 29 0 0 25 0 1 0 1726267891 17092608 3859 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4173 3859 145 145 0 4028 0
[pid=21743] vsize: 16692
Current children cumulated CPU time (s) 559.73
Current children cumulated vsize (Kb) 18816

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3886 0 0 0 56944 29 0 0 25 0 1 0 1726267891 17133568 3869 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4183 3869 145 145 0 4038 0
[pid=21743] vsize: 16732
Current children cumulated CPU time (s) 569.73
Current children cumulated vsize (Kb) 18856

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3900 0 0 0 57944 30 0 0 25 0 1 0 1726267891 17199104 3883 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4199 3883 145 145 0 4054 0
[pid=21743] vsize: 16796
Current children cumulated CPU time (s) 579.74
Current children cumulated vsize (Kb) 18920

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3922 0 0 0 58945 30 0 0 25 0 1 0 1726267891 17330176 3905 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3905 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 589.75
Current children cumulated vsize (Kb) 19048

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3922 0 0 0 59945 30 0 0 25 0 1 0 1726267891 17330176 3905 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3905 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 599.75
Current children cumulated vsize (Kb) 19048

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3922 0 0 0 60944 31 0 0 25 0 1 0 1726267891 17330176 3905 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3905 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 609.75
Current children cumulated vsize (Kb) 19048

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3924 0 0 0 61944 31 0 0 25 0 1 0 1726267891 17330176 3907 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3907 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 619.75
Current children cumulated vsize (Kb) 19048

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3924 0 0 0 62944 31 0 0 25 0 1 0 1726267891 17330176 3907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3907 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 629.75
Current children cumulated vsize (Kb) 19048

[startup+640.058 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3924 0 0 0 63944 31 0 0 25 0 1 0 1726267891 17330176 3907 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3907 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 639.75
Current children cumulated vsize (Kb) 19048

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3924 0 0 0 64944 32 0 0 25 0 1 0 1726267891 17330176 3907 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4231 3907 145 145 0 4086 0
[pid=21743] vsize: 16924
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 19048

[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3927 0 0 0 65945 32 0 0 25 0 1 0 1726267891 17346560 3910 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4235 3910 145 145 0 4090 0
[pid=21743] vsize: 16940
Current children cumulated CPU time (s) 659.77
Current children cumulated vsize (Kb) 19064

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3940 0 0 0 66944 32 0 0 25 0 1 0 1726267891 17412096 3923 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4251 3923 145 145 0 4106 0
[pid=21743] vsize: 17004
Current children cumulated CPU time (s) 669.76
Current children cumulated vsize (Kb) 19128

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3943 0 0 0 67945 32 0 0 25 0 1 0 1726267891 17444864 3926 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4259 3926 145 145 0 4114 0
[pid=21743] vsize: 17036
Current children cumulated CPU time (s) 679.77
Current children cumulated vsize (Kb) 19160

[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3943 0 0 0 68945 32 0 0 25 0 1 0 1726267891 17444864 3926 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4259 3926 145 145 0 4114 0
[pid=21743] vsize: 17036
Current children cumulated CPU time (s) 689.77
Current children cumulated vsize (Kb) 19160

[startup+700.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3945 0 0 0 69945 32 0 0 25 0 1 0 1726267891 17444864 3928 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4259 3928 145 145 0 4114 0
[pid=21743] vsize: 17036
Current children cumulated CPU time (s) 699.77
Current children cumulated vsize (Kb) 19160

[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3977 0 0 0 70945 32 0 0 25 0 1 0 1726267891 17575936 3960 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4291 3960 145 145 0 4146 0
[pid=21743] vsize: 17164
Current children cumulated CPU time (s) 709.77
Current children cumulated vsize (Kb) 19288

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3980 0 0 0 71945 33 0 0 25 0 1 0 1726267891 17641472 3963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4307 3963 145 145 0 4162 0
[pid=21743] vsize: 17228
Current children cumulated CPU time (s) 719.78
Current children cumulated vsize (Kb) 19352

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3982 0 0 0 72945 33 0 0 25 0 1 0 1726267891 17641472 3965 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4307 3965 145 145 0 4162 0
[pid=21743] vsize: 17228
Current children cumulated CPU time (s) 729.78
Current children cumulated vsize (Kb) 19352

[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3986 0 0 0 73945 33 0 0 25 0 1 0 1726267891 17641472 3969 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4307 3969 145 145 0 4162 0
[pid=21743] vsize: 17228
Current children cumulated CPU time (s) 739.78
Current children cumulated vsize (Kb) 19352

[startup+750.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3986 0 0 0 74945 33 0 0 25 0 1 0 1726267891 17641472 3969 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4307 3969 145 145 0 4162 0
[pid=21743] vsize: 17228
Current children cumulated CPU time (s) 749.78
Current children cumulated vsize (Kb) 19352

[startup+760.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 3987 0 0 0 75946 33 0 0 25 0 1 0 1726267891 17641472 3970 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4307 3970 145 145 0 4162 0
[pid=21743] vsize: 17228
Current children cumulated CPU time (s) 759.79
Current children cumulated vsize (Kb) 19352

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4008 0 0 0 76945 33 0 0 25 0 1 0 1726267891 17739776 3991 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3991 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 769.78
Current children cumulated vsize (Kb) 19448

[startup+780.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 77945 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 779.78
Current children cumulated vsize (Kb) 19448

[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 78945 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 789.78
Current children cumulated vsize (Kb) 19448

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 79946 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 799.79
Current children cumulated vsize (Kb) 19448

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 80946 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 809.79
Current children cumulated vsize (Kb) 19448

[startup+820.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 81946 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 819.79
Current children cumulated vsize (Kb) 19448

[startup+830.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 82946 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 829.79
Current children cumulated vsize (Kb) 19448

[startup+840.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4013 0 0 0 83946 33 0 0 25 0 1 0 1726267891 17739776 3996 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4331 3996 145 145 0 4186 0
[pid=21743] vsize: 17324
Current children cumulated CPU time (s) 839.79
Current children cumulated vsize (Kb) 19448

[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4025 0 0 0 84946 33 0 0 25 0 1 0 1726267891 17805312 4008 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4347 4008 145 145 0 4202 0
[pid=21743] vsize: 17388
Current children cumulated CPU time (s) 849.79
Current children cumulated vsize (Kb) 19512

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4039 0 0 0 85947 33 0 0 25 0 1 0 1726267891 17870848 4022 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4363 4022 145 145 0 4218 0
[pid=21743] vsize: 17452
Current children cumulated CPU time (s) 859.8
Current children cumulated vsize (Kb) 19576

[startup+870.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4045 0 0 0 86947 33 0 0 25 0 1 0 1726267891 17870848 4028 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4363 4028 145 145 0 4218 0
[pid=21743] vsize: 17452
Current children cumulated CPU time (s) 869.8
Current children cumulated vsize (Kb) 19576

[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4046 0 0 0 87947 33 0 0 25 0 1 0 1726267891 17870848 4029 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4363 4029 145 145 0 4218 0
[pid=21743] vsize: 17452
Current children cumulated CPU time (s) 879.8
Current children cumulated vsize (Kb) 19576

[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4046 0 0 0 88947 34 0 0 25 0 1 0 1726267891 17870848 4029 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4363 4029 145 145 0 4218 0
[pid=21743] vsize: 17452
Current children cumulated CPU time (s) 889.81
Current children cumulated vsize (Kb) 19576

[startup+900.073 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4057 0 0 0 89947 34 0 0 25 0 1 0 1726267891 17936384 4040 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4040 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 899.81
Current children cumulated vsize (Kb) 19640

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4062 0 0 0 90947 34 0 0 25 0 1 0 1726267891 17936384 4045 4294967295 134512640 135094434 3221224448 3221223120 134556526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4045 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 909.81
Current children cumulated vsize (Kb) 19640

[startup+920.075 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4063 0 0 0 91948 34 0 0 25 0 1 0 1726267891 17936384 4046 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4046 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 919.82
Current children cumulated vsize (Kb) 19640

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4064 0 0 0 92948 34 0 0 25 0 1 0 1726267891 17936384 4047 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4047 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 929.82
Current children cumulated vsize (Kb) 19640

[startup+940.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4064 0 0 0 93948 34 0 0 25 0 1 0 1726267891 17936384 4047 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4047 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 939.82
Current children cumulated vsize (Kb) 19640

[startup+950.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4064 0 0 0 94948 34 0 0 25 0 1 0 1726267891 17936384 4047 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4047 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 949.82
Current children cumulated vsize (Kb) 19640

[startup+960.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4064 0 0 0 95948 34 0 0 25 0 1 0 1726267891 17936384 4047 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4379 4047 145 145 0 4234 0
[pid=21743] vsize: 17516
Current children cumulated CPU time (s) 959.82
Current children cumulated vsize (Kb) 19640

[startup+970.077 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4073 0 0 0 96948 34 0 0 25 0 1 0 1726267891 18001920 4056 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4395 4056 145 145 0 4250 0
[pid=21743] vsize: 17580
Current children cumulated CPU time (s) 969.82
Current children cumulated vsize (Kb) 19704

[startup+980.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4073 0 0 0 97949 34 0 0 25 0 1 0 1726267891 18001920 4056 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4395 4056 145 145 0 4250 0
[pid=21743] vsize: 17580
Current children cumulated CPU time (s) 979.83
Current children cumulated vsize (Kb) 19704

[startup+990.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4073 0 0 0 98949 34 0 0 25 0 1 0 1726267891 18001920 4056 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4395 4056 145 145 0 4250 0
[pid=21743] vsize: 17580
Current children cumulated CPU time (s) 989.83
Current children cumulated vsize (Kb) 19704

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21743
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4073 0 0 0 99949 34 0 0 25 0 1 0 1726267891 18001920 4056 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4395 4056 145 145 0 4250 0
[pid=21743] vsize: 17580
Current children cumulated CPU time (s) 999.83
Current children cumulated vsize (Kb) 19704

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4073 0 0 0 100949 34 0 0 25 0 1 0 1726267891 18001920 4056 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4395 4056 145 145 0 4250 0
[pid=21743] vsize: 17580
Current children cumulated CPU time (s) 1009.83
Current children cumulated vsize (Kb) 19704

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4086 0 0 0 101949 34 0 0 25 0 1 0 1726267891 18067456 4069 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4411 4069 145 145 0 4266 0
[pid=21743] vsize: 17644
Current children cumulated CPU time (s) 1019.83
Current children cumulated vsize (Kb) 19768

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4086 0 0 0 102949 34 0 0 25 0 1 0 1726267891 18067456 4069 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4411 4069 145 145 0 4266 0
[pid=21743] vsize: 17644
Current children cumulated CPU time (s) 1029.83
Current children cumulated vsize (Kb) 19768

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4086 0 0 0 103949 34 0 0 25 0 1 0 1726267891 18067456 4069 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4411 4069 145 145 0 4266 0
[pid=21743] vsize: 17644
Current children cumulated CPU time (s) 1039.83
Current children cumulated vsize (Kb) 19768

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4096 0 0 0 104950 34 0 0 25 0 1 0 1726267891 18132992 4079 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4079 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1049.84
Current children cumulated vsize (Kb) 19832

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4098 0 0 0 105950 34 0 0 25 0 1 0 1726267891 18132992 4081 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4081 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1059.84
Current children cumulated vsize (Kb) 19832

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4099 0 0 0 106950 34 0 0 25 0 1 0 1726267891 18132992 4082 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4082 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1069.84
Current children cumulated vsize (Kb) 19832

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4101 0 0 0 107950 34 0 0 25 0 1 0 1726267891 18132992 4084 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4084 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1079.84
Current children cumulated vsize (Kb) 19832

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4102 0 0 0 108950 34 0 0 25 0 1 0 1726267891 18132992 4085 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4085 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1089.84
Current children cumulated vsize (Kb) 19832

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4102 0 0 0 109950 34 0 0 25 0 1 0 1726267891 18132992 4085 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4085 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1099.84
Current children cumulated vsize (Kb) 19832

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4102 0 0 0 110951 34 0 0 25 0 1 0 1726267891 18132992 4085 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4427 4085 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1109.85
Current children cumulated vsize (Kb) 19832

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4104 0 0 0 111951 34 0 0 25 0 1 0 1726267891 18132992 4087 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21743/statm): 4427 4087 145 145 0 4282 0
[pid=21743] vsize: 17708
Current children cumulated CPU time (s) 1119.85
Current children cumulated vsize (Kb) 19832

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4130 0 0 0 112950 35 0 0 25 0 1 0 1726267891 18264064 4113 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4459 4113 145 145 0 4314 0
[pid=21743] vsize: 17836
Current children cumulated CPU time (s) 1129.85
Current children cumulated vsize (Kb) 19960

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4134 0 0 0 113950 35 0 0 25 0 1 0 1726267891 18264064 4117 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4459 4117 145 145 0 4314 0
[pid=21743] vsize: 17836
Current children cumulated CPU time (s) 1139.85
Current children cumulated vsize (Kb) 19960

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4134 0 0 0 114950 35 0 0 25 0 1 0 1726267891 18264064 4117 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4459 4117 145 145 0 4314 0
[pid=21743] vsize: 17836
Current children cumulated CPU time (s) 1149.85
Current children cumulated vsize (Kb) 19960

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4134 0 0 0 115951 35 0 0 25 0 1 0 1726267891 18264064 4117 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4459 4117 145 145 0 4314 0
[pid=21743] vsize: 17836
Current children cumulated CPU time (s) 1159.86
Current children cumulated vsize (Kb) 19960

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4144 0 0 0 116951 35 0 0 25 0 1 0 1726267891 18329600 4127 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4475 4127 145 145 0 4330 0
[pid=21743] vsize: 17900
Current children cumulated CPU time (s) 1169.86
Current children cumulated vsize (Kb) 20024

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4151 0 0 0 117951 35 0 0 25 0 1 0 1726267891 18329600 4134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4475 4134 145 145 0 4330 0
[pid=21743] vsize: 17900
Current children cumulated CPU time (s) 1179.86
Current children cumulated vsize (Kb) 20024

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4165 0 0 0 118951 35 0 0 25 0 1 0 1726267891 18395136 4148 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4491 4148 145 145 0 4346 0
[pid=21743] vsize: 17964
Current children cumulated CPU time (s) 1189.86
Current children cumulated vsize (Kb) 20088

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4167 0 0 0 119951 36 0 0 25 0 1 0 1726267891 18395136 4150 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4491 4150 145 145 0 4346 0
[pid=21743] vsize: 17964
Current children cumulated CPU time (s) 1199.87
Current children cumulated vsize (Kb) 20088

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4167 0 0 0 120950 36 0 0 25 0 1 0 1726267891 18395136 4150 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4491 4150 145 145 0 4346 0
[pid=21743] vsize: 17964
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 20088



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 21745
Raw data (/proc/21739/stat): 21739 (minisat+_script) S 21738 21739 17733 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1726267886 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21739/statm): 531 226 485 147 0 384 0
[pid=21739] vsize: 2124
Raw data (/proc/21743/stat): 21743 (minisat+_64-bit) R 21739 21739 17733 0 -1 0 4167 0 0 0 120950 36 0 0 25 0 1 0 1726267891 18395136 4150 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21743/statm): 4491 4150 145 145 0 4346 0
[pid=21743] vsize: 17964
Current children cumulated CPU time (s) 1209.86
Current children cumulated vsize (Kb) 20088

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.89
CPU user time (s): 1209.51
CPU system time (s): 0.377942
CPU usage (%): 99.9817
Max. virtual memory (cumulated for all children) (Kb): 20088

Verifier Data

ERROR: no interpretation found !