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-5xp1.b.opb
MD5SUM24a8f38e94b07e6ca192a34c96c24c6e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 12
Optimality of the best value was proved YES
Number of terms in the objective function 465
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 465
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 465
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 benchmark73.2229
Number of variables464
Total number of constraints859
Number of constraints which are clauses845
Number of constraints which are cardinality constraints (but not clauses)14
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint149

Trace number 901

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        938368 kB
Buffers:         34596 kB
Cached:          32980 kB
SwapCached:        832 kB
Active:          55072 kB
Inactive:        15156 kB
HighTotal:      131008 kB
HighFree:        94332 kB
LowTotal:       903652 kB
LowFree:        844036 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20500 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 13:03:21 (client local time) WITH STATUS 10 IN 1209.75 SECONDS
stats: 2402 7 1209.75 10

Solver Data

c Parsing PB file...
c Converting 843 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 |     843    29887 |     281       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 20
c ---[   0]---> Sorter-cost:17506     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19368    73043 |    6456       0        0     nan |  0.000 % |
c |       102 |   19368    73043 |    7101     102     7508    73.6 |  0.016 % |
c |       253 |   19356    73019 |    7811     251    21282    84.8 |  0.056 % |
c ==============================================================================
c Found solution: 17
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       293 |   17268    68155 |    5756     287    23635    82.4 |  0.056 % |
c |       393 |   17268    68155 |    6331     387    30443    78.7 | 11.325 % |
c |       543 |   17268    68155 |    6964     537    39041    72.7 | 11.325 % |
c |       770 |   17268    68155 |    7661     764    50110    65.6 | 11.325 % |
c ==============================================================================
c Found solution: 15
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       864 |   17261    68142 |    5753     845    54108    64.0 | 11.325 % |
c |       964 |   17261    68142 |    6328     945    61405    65.0 | 11.470 % |
c |      1115 |   17261    68142 |    6961    1096    75538    68.9 | 11.470 % |
c |      1341 |   17261    68142 |    7657    1322    87753    66.4 | 11.470 % |
c |      1678 |   17261    68142 |    8422    1659   110793    66.8 | 11.470 % |
c |      2184 |   17261    68142 |    9265    2165   155258    71.7 | 11.470 % |
c |      2943 |   17261    68142 |   10191    2924   219586    75.1 | 11.470 % |
c ==============================================================================
c Found solution: 14
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3979 |   17273    68172 |    5757    3960   368681    93.1 | 11.470 % |
c |      4081 |   17273    68172 |    6332    4062   376314    92.6 | 11.470 % |
c |      4232 |   17273    68172 |    6965    4213   386712    91.8 | 11.470 % |
c |      4457 |   17273    68172 |    7662    4438   409455    92.3 | 11.470 % |
c |      4795 |   17273    68172 |    8428    4776   432918    90.6 | 11.470 % |
c |      5301 |   17273    68172 |    9271    5282   466487    88.3 | 11.470 % |
c |      6061 |   17273    68172 |   10198    6042   522550    86.5 | 11.470 % |
c |      7204 |   17273    68172 |   11218    7185   589528    82.0 | 11.470 % |
c |      8917 |   17273    68172 |   12340    8898   698521    78.5 | 11.470 % |
c |     11480 |   17273    68172 |   13574   11461   858013    74.9 | 11.470 % |
c |     15325 |   17273    68172 |   14932   15306  1141586    74.6 | 11.470 % |
c |     21092 |   17273    68172 |   16425   12759   938327    73.5 | 11.470 % |
c |     29741 |   17273    68172 |   18067   12053   875185    72.6 | 11.470 % |
c |     42716 |   17273    68172 |   19874   14184   867021    61.1 | 11.470 % |
c |     62178 |   17273    68172 |   21862   11498   890576    77.5 | 11.470 % |
c |     91371 |   17273    68172 |   24048   15677  1206811    77.0 | 11.470 % |
c |    135161 |   17273    68172 |   26453   20827  1226051    58.9 | 11.470 % |
c |    200848 |   17273    68172 |   29098   27816  1466699    52.7 | 11.470 % |
c |    299376 |   17273    68172 |   32008   25897  1765102    68.2 | 11.470 % |

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/6400/stat): 6400 (minisat+_script) R 6399 6400 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841344529 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/6400/statm): 174 3 169 147 0 27 0
[pid=6400] 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=6401
New process pid=6402
New process pid=6403
execve syscall for /bin/sed executable
One traced child (pid=6402) 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=6403) exited with status: 0
One traced child (pid=6401) exited with status: 0
New process pid=6404
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-5xp1.b.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 1790 0 0 0 977 9 0 0 25 0 1 0 1841344534 7958528 1774 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 1943 1774 145 145 0 1798 0
[pid=6404] vsize: 7772
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 9896

[startup+20.005 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2103 0 0 0 1970 12 0 0 25 0 1 0 1841344534 9256960 2087 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 2260 2087 145 145 0 2115 0
[pid=6404] vsize: 9040
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 11164

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.95 0.91 1/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) T 6400 6400 2660 0 -1 0 2458 0 0 0 2964 15 0 0 25 0 1 0 1841344534 10698752 2442 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/6404/statm): 2612 2442 145 145 0 2467 0
[pid=6404] vsize: 10448
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 12572

[startup+40.0065 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2652 0 0 0 3960 16 0 0 25 0 1 0 1841344534 11563008 2636 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 2823 2636 145 145 0 2678 0
[pid=6404] vsize: 11292
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 13416

[startup+50.0082 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2652 0 0 0 4960 16 0 0 25 0 1 0 1841344534 11563008 2636 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 2823 2636 145 145 0 2678 0
[pid=6404] vsize: 11292
Current children cumulated CPU time (s) 49.76
Current children cumulated vsize (Kb) 13416

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2664 0 0 0 5960 16 0 0 25 0 1 0 1841344534 11608064 2648 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 2834 2648 145 145 0 2689 0
[pid=6404] vsize: 11336
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 13460

[startup+70.0106 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2855 0 0 0 6958 17 0 0 25 0 1 0 1841344534 12410880 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3030 2839 145 145 0 2885 0
[pid=6404] vsize: 12120
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 14244

[startup+80.0114 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2855 0 0 0 7958 17 0 0 25 0 1 0 1841344534 12410880 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3030 2839 145 145 0 2885 0
[pid=6404] vsize: 12120
Current children cumulated CPU time (s) 79.75
Current children cumulated vsize (Kb) 14244

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2961 0 0 0 8956 18 0 0 25 0 1 0 1841344534 12849152 2945 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3137 2945 145 145 0 2992 0
[pid=6404] vsize: 12548
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 14672

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3079 0 0 0 9954 19 0 0 25 0 1 0 1841344534 13332480 3063 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3255 3063 145 145 0 3110 0
[pid=6404] vsize: 13020
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 15144

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3085 0 0 0 10954 19 0 0 25 0 1 0 1841344534 13365248 3069 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3263 3069 145 145 0 3118 0
[pid=6404] vsize: 13052
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 15176

[startup+120.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3133 0 0 0 11954 19 0 0 25 0 1 0 1841344534 13574144 3117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 3314 3117 145 145 0 3169 0
[pid=6404] vsize: 13256
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 15380

[startup+130.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3338 0 0 0 12949 21 0 0 25 0 1 0 1841344534 14413824 3322 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3519 3322 145 145 0 3374 0
[pid=6404] vsize: 14076
Current children cumulated CPU time (s) 129.7
Current children cumulated vsize (Kb) 16200

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3356 0 0 0 13948 22 0 0 25 0 1 0 1841344534 14495744 3340 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3539 3340 145 145 0 3394 0
[pid=6404] vsize: 14156
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 16280

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3396 0 0 0 14947 23 0 0 25 0 1 0 1841344534 14671872 3380 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3582 3380 145 145 0 3437 0
[pid=6404] vsize: 14328
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 16452

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3638 0 0 0 15943 25 0 0 25 0 1 0 1841344534 15663104 3622 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3824 3622 145 145 0 3679 0
[pid=6404] vsize: 15296
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 17420

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3671 0 0 0 16943 26 0 0 25 0 1 0 1841344534 15826944 3655 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3864 3655 145 145 0 3719 0
[pid=6404] vsize: 15456
Current children cumulated CPU time (s) 169.69
Current children cumulated vsize (Kb) 17580

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3684 0 0 0 17942 26 0 0 25 0 1 0 1841344534 15876096 3668 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3876 3668 145 145 0 3731 0
[pid=6404] vsize: 15504
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 17628

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3729 0 0 0 18941 27 0 0 25 0 1 0 1841344534 16121856 3713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 3936 3713 145 145 0 3791 0
[pid=6404] vsize: 15744
Current children cumulated CPU time (s) 189.68
Current children cumulated vsize (Kb) 17868

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3773 0 0 0 19941 27 0 0 25 0 1 0 1841344534 16400384 3757 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4004 3757 145 145 0 3859 0
[pid=6404] vsize: 16016
Current children cumulated CPU time (s) 199.68
Current children cumulated vsize (Kb) 18140

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3774 0 0 0 20940 28 0 0 25 0 1 0 1841344534 16400384 3758 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4004 3758 145 145 0 3859 0
[pid=6404] vsize: 16016
Current children cumulated CPU time (s) 209.68
Current children cumulated vsize (Kb) 18140

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3786 0 0 0 21940 28 0 0 25 0 1 0 1841344534 16465920 3770 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4020 3770 145 145 0 3875 0
[pid=6404] vsize: 16080
Current children cumulated CPU time (s) 219.68
Current children cumulated vsize (Kb) 18204

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3786 0 0 0 22940 29 0 0 25 0 1 0 1841344534 16465920 3770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4020 3770 145 145 0 3875 0
[pid=6404] vsize: 16080
Current children cumulated CPU time (s) 229.69
Current children cumulated vsize (Kb) 18204

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3798 0 0 0 23940 29 0 0 25 0 1 0 1841344534 16531456 3782 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4036 3782 145 145 0 3891 0
[pid=6404] vsize: 16144
Current children cumulated CPU time (s) 239.69
Current children cumulated vsize (Kb) 18268

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3893 0 0 0 24938 30 0 0 25 0 1 0 1841344534 16904192 3877 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4127 3877 145 145 0 3982 0
[pid=6404] vsize: 16508
Current children cumulated CPU time (s) 249.68
Current children cumulated vsize (Kb) 18632

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3985 0 0 0 25936 31 0 0 25 0 1 0 1841344534 17317888 3969 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4228 3969 145 145 0 4083 0
[pid=6404] vsize: 16912
Current children cumulated CPU time (s) 259.67
Current children cumulated vsize (Kb) 19036

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3996 0 0 0 26936 31 0 0 25 0 1 0 1841344534 17416192 3980 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4252 3980 145 145 0 4107 0
[pid=6404] vsize: 17008
Current children cumulated CPU time (s) 269.67
Current children cumulated vsize (Kb) 19132

[startup+280.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4008 0 0 0 27936 32 0 0 25 0 1 0 1841344534 17481728 3992 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4268 3992 145 145 0 4123 0
[pid=6404] vsize: 17072
Current children cumulated CPU time (s) 279.68
Current children cumulated vsize (Kb) 19196

[startup+290.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4020 0 0 0 28935 32 0 0 25 0 1 0 1841344534 17547264 4004 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4284 4004 145 145 0 4139 0
[pid=6404] vsize: 17136
Current children cumulated CPU time (s) 289.67
Current children cumulated vsize (Kb) 19260

[startup+300.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4034 0 0 0 29935 33 0 0 25 0 1 0 1841344534 17612800 4018 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4300 4018 145 145 0 4155 0
[pid=6404] vsize: 17200
Current children cumulated CPU time (s) 299.68
Current children cumulated vsize (Kb) 19324

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4034 0 0 0 30935 33 0 0 25 0 1 0 1841344534 17612800 4018 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4300 4018 145 145 0 4155 0
[pid=6404] vsize: 17200
Current children cumulated CPU time (s) 309.68
Current children cumulated vsize (Kb) 19324

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4047 0 0 0 31935 33 0 0 25 0 1 0 1841344534 17645568 4031 4294967295 134512640 135094434 3221224448 3221223120 134555429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4308 4031 145 145 0 4163 0
[pid=6404] vsize: 17232
Current children cumulated CPU time (s) 319.68
Current children cumulated vsize (Kb) 19356

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4054 0 0 0 32934 34 0 0 25 0 1 0 1841344534 17694720 4038 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4320 4038 145 145 0 4175 0
[pid=6404] vsize: 17280
Current children cumulated CPU time (s) 329.68
Current children cumulated vsize (Kb) 19404

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4085 0 0 0 33934 34 0 0 25 0 1 0 1841344534 17842176 4069 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4356 4069 145 145 0 4211 0
[pid=6404] vsize: 17424
Current children cumulated CPU time (s) 339.68
Current children cumulated vsize (Kb) 19548

[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4094 0 0 0 34933 35 0 0 25 0 1 0 1841344534 17874944 4078 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4364 4078 145 145 0 4219 0
[pid=6404] vsize: 17456
Current children cumulated CPU time (s) 349.68
Current children cumulated vsize (Kb) 19580

[startup+360.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4102 0 0 0 35933 35 0 0 25 0 1 0 1841344534 17907712 4086 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4372 4086 145 145 0 4227 0
[pid=6404] vsize: 17488
Current children cumulated CPU time (s) 359.68
Current children cumulated vsize (Kb) 19612

[startup+370.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4110 0 0 0 36933 36 0 0 25 0 1 0 1841344534 17940480 4094 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4380 4094 145 145 0 4235 0
[pid=6404] vsize: 17520
Current children cumulated CPU time (s) 369.69
Current children cumulated vsize (Kb) 19644

[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4111 0 0 0 37932 36 0 0 25 0 1 0 1841344534 17940480 4095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4380 4095 145 145 0 4235 0
[pid=6404] vsize: 17520
Current children cumulated CPU time (s) 379.68
Current children cumulated vsize (Kb) 19644

[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4114 0 0 0 38932 37 0 0 25 0 1 0 1841344534 17940480 4098 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4380 4098 145 145 0 4235 0
[pid=6404] vsize: 17520
Current children cumulated CPU time (s) 389.69
Current children cumulated vsize (Kb) 19644

[startup+400.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4114 0 0 0 39932 37 0 0 25 0 1 0 1841344534 17940480 4098 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4380 4098 145 145 0 4235 0
[pid=6404] vsize: 17520
Current children cumulated CPU time (s) 399.69
Current children cumulated vsize (Kb) 19644

[startup+410.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4121 0 0 0 40932 37 0 0 25 0 1 0 1841344534 17973248 4105 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4388 4105 145 145 0 4243 0
[pid=6404] vsize: 17552
Current children cumulated CPU time (s) 409.69
Current children cumulated vsize (Kb) 19676

[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4131 0 0 0 41932 37 0 0 25 0 1 0 1841344534 18071552 4115 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4412 4115 145 145 0 4267 0
[pid=6404] vsize: 17648
Current children cumulated CPU time (s) 419.69
Current children cumulated vsize (Kb) 19772

[startup+430.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4132 0 0 0 42932 38 0 0 25 0 1 0 1841344534 18071552 4116 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4412 4116 145 145 0 4267 0
[pid=6404] vsize: 17648
Current children cumulated CPU time (s) 429.7
Current children cumulated vsize (Kb) 19772

[startup+440.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4138 0 0 0 43932 38 0 0 25 0 1 0 1841344534 18071552 4122 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4412 4122 145 145 0 4267 0
[pid=6404] vsize: 17648
Current children cumulated CPU time (s) 439.7
Current children cumulated vsize (Kb) 19772

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4138 0 0 0 44932 38 0 0 25 0 1 0 1841344534 18071552 4122 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4412 4122 145 145 0 4267 0
[pid=6404] vsize: 17648
Current children cumulated CPU time (s) 449.7
Current children cumulated vsize (Kb) 19772

[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4146 0 0 0 45932 38 0 0 25 0 1 0 1841344534 18104320 4130 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4420 4130 145 145 0 4275 0
[pid=6404] vsize: 17680
Current children cumulated CPU time (s) 459.7
Current children cumulated vsize (Kb) 19804

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4157 0 0 0 46932 38 0 0 25 0 1 0 1841344534 18202624 4141 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4444 4141 145 145 0 4299 0
[pid=6404] vsize: 17776
Current children cumulated CPU time (s) 469.7
Current children cumulated vsize (Kb) 19900

[startup+480.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4158 0 0 0 47933 38 0 0 25 0 1 0 1841344534 18202624 4142 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4444 4142 145 145 0 4299 0
[pid=6404] vsize: 17776
Current children cumulated CPU time (s) 479.71
Current children cumulated vsize (Kb) 19900

[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4158 0 0 0 48933 38 0 0 25 0 1 0 1841344534 18202624 4142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4444 4142 145 145 0 4299 0
[pid=6404] vsize: 17776
Current children cumulated CPU time (s) 489.71
Current children cumulated vsize (Kb) 19900

[startup+500.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4169 0 0 0 49933 38 0 0 25 0 1 0 1841344534 18235392 4153 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4452 4153 145 145 0 4307 0
[pid=6404] vsize: 17808
Current children cumulated CPU time (s) 499.71
Current children cumulated vsize (Kb) 19932

[startup+510.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4181 0 0 0 50933 38 0 0 25 0 1 0 1841344534 18300928 4165 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4468 4165 145 145 0 4323 0
[pid=6404] vsize: 17872
Current children cumulated CPU time (s) 509.71
Current children cumulated vsize (Kb) 19996

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4192 0 0 0 51934 38 0 0 25 0 1 0 1841344534 18366464 4176 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4484 4176 145 145 0 4339 0
[pid=6404] vsize: 17936
Current children cumulated CPU time (s) 519.72
Current children cumulated vsize (Kb) 20060

[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4216 0 0 0 52934 38 0 0 25 0 1 0 1841344534 18497536 4200 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4516 4200 145 145 0 4371 0
[pid=6404] vsize: 18064
Current children cumulated CPU time (s) 529.72
Current children cumulated vsize (Kb) 20188

[startup+540.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4218 0 0 0 53934 38 0 0 25 0 1 0 1841344534 18497536 4202 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4516 4202 145 145 0 4371 0
[pid=6404] vsize: 18064
Current children cumulated CPU time (s) 539.72
Current children cumulated vsize (Kb) 20188

[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 54934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0
[pid=6404] vsize: 18224
Current children cumulated CPU time (s) 549.72
Current children cumulated vsize (Kb) 20348

[startup+560.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 55934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0
[pid=6404] vsize: 18224
Current children cumulated CPU time (s) 559.72
Current children cumulated vsize (Kb) 20348

[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 56934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0
[pid=6404] vsize: 18224
Current children cumulated CPU time (s) 569.72
Current children cumulated vsize (Kb) 20348

[startup+580.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4258 0 0 0 57934 38 0 0 25 0 1 0 1841344534 18726912 4242 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4572 4242 145 145 0 4427 0
[pid=6404] vsize: 18288
Current children cumulated CPU time (s) 579.72
Current children cumulated vsize (Kb) 20412

[startup+590.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4269 0 0 0 58935 38 0 0 25 0 1 0 1841344534 18792448 4253 4294967295 134512640 135094434 3221224448 3221223072 134557593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6404/statm): 4588 4253 145 145 0 4443 0
[pid=6404] vsize: 18352
Current children cumulated CPU time (s) 589.73
Current children cumulated vsize (Kb) 20476

[startup+600.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4295 0 0 0 59934 39 0 0 25 0 1 0 1841344534 18923520 4279 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4620 4279 145 145 0 4475 0
[pid=6404] vsize: 18480
Current children cumulated CPU time (s) 599.73
Current children cumulated vsize (Kb) 20604

[startup+610.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 60934 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0
[pid=6404] vsize: 18480
Current children cumulated CPU time (s) 609.73
Current children cumulated vsize (Kb) 20604

[startup+620.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 61935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0
[pid=6404] vsize: 18480
Current children cumulated CPU time (s) 619.74
Current children cumulated vsize (Kb) 20604

[startup+630.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 62935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0
[pid=6404] vsize: 18480
Current children cumulated CPU time (s) 629.74
Current children cumulated vsize (Kb) 20604

[startup+640.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 63935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0
[pid=6404] vsize: 18480
Current children cumulated CPU time (s) 639.74
Current children cumulated vsize (Kb) 20604

[startup+650.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4313 0 0 0 64935 39 0 0 25 0 1 0 1841344534 19021824 4297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4644 4297 145 145 0 4499 0
[pid=6404] vsize: 18576
Current children cumulated CPU time (s) 649.74
Current children cumulated vsize (Kb) 20700

[startup+660.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4317 0 0 0 65935 39 0 0 25 0 1 0 1841344534 19087360 4301 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4660 4301 145 145 0 4515 0
[pid=6404] vsize: 18640
Current children cumulated CPU time (s) 659.74
Current children cumulated vsize (Kb) 20764

[startup+670.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4317 0 0 0 66936 39 0 0 25 0 1 0 1841344534 19087360 4301 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4660 4301 145 145 0 4515 0
[pid=6404] vsize: 18640
Current children cumulated CPU time (s) 669.75
Current children cumulated vsize (Kb) 20764

[startup+680.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4328 0 0 0 67936 39 0 0 25 0 1 0 1841344534 19120128 4312 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4668 4312 145 145 0 4523 0
[pid=6404] vsize: 18672
Current children cumulated CPU time (s) 679.75
Current children cumulated vsize (Kb) 20796

[startup+690.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4338 0 0 0 68936 39 0 0 25 0 1 0 1841344534 19185664 4322 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4322 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 689.75
Current children cumulated vsize (Kb) 20860

[startup+700.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 69936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 699.75
Current children cumulated vsize (Kb) 20860

[startup+710.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 70936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 709.75
Current children cumulated vsize (Kb) 20860

[startup+720.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 71936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 719.75
Current children cumulated vsize (Kb) 20860

[startup+730.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 72937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 729.76
Current children cumulated vsize (Kb) 20860

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 73937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 739.76
Current children cumulated vsize (Kb) 20860

[startup+750.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 74937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0
[pid=6404] vsize: 18736
Current children cumulated CPU time (s) 749.76
Current children cumulated vsize (Kb) 20860

[startup+760.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4526 0 0 0 75934 40 0 0 25 0 1 0 1841344534 19976192 4510 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 4877 4510 145 145 0 4732 0
[pid=6404] vsize: 19508
Current children cumulated CPU time (s) 759.74
Current children cumulated vsize (Kb) 21632

[startup+770.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4648 0 0 0 76933 41 0 0 25 0 1 0 1841344534 20484096 4632 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5001 4632 145 145 0 4856 0
[pid=6404] vsize: 20004
Current children cumulated CPU time (s) 769.74
Current children cumulated vsize (Kb) 22128

[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4654 0 0 0 77933 41 0 0 25 0 1 0 1841344534 20516864 4638 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5009 4638 145 145 0 4864 0
[pid=6404] vsize: 20036
Current children cumulated CPU time (s) 779.74
Current children cumulated vsize (Kb) 22160

[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4657 0 0 0 78933 41 0 0 25 0 1 0 1841344534 20533248 4641 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5013 4641 145 145 0 4868 0
[pid=6404] vsize: 20052
Current children cumulated CPU time (s) 789.74
Current children cumulated vsize (Kb) 22176

[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4664 0 0 0 79933 41 0 0 25 0 1 0 1841344534 20566016 4648 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5021 4648 145 145 0 4876 0
[pid=6404] vsize: 20084
Current children cumulated CPU time (s) 799.74
Current children cumulated vsize (Kb) 22208

[startup+810.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4689 0 0 0 80933 41 0 0 25 0 1 0 1841344534 20697088 4673 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5053 4673 145 145 0 4908 0
[pid=6404] vsize: 20212
Current children cumulated CPU time (s) 809.74
Current children cumulated vsize (Kb) 22336

[startup+820.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4706 0 0 0 81933 41 0 0 25 0 1 0 1841344534 20762624 4690 4294967295 134512640 135094434 3221224448 3221223120 134555765 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5069 4690 145 145 0 4924 0
[pid=6404] vsize: 20276
Current children cumulated CPU time (s) 819.74
Current children cumulated vsize (Kb) 22400

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4718 0 0 0 82934 42 0 0 25 0 1 0 1841344534 20828160 4702 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4702 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 829.76
Current children cumulated vsize (Kb) 22464

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4720 0 0 0 83934 42 0 0 25 0 1 0 1841344534 20828160 4704 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4704 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 839.76
Current children cumulated vsize (Kb) 22464

[startup+850.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4721 0 0 0 84934 42 0 0 25 0 1 0 1841344534 20828160 4705 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4705 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 849.76
Current children cumulated vsize (Kb) 22464

[startup+860.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4723 0 0 0 85934 42 0 0 25 0 1 0 1841344534 20828160 4707 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4707 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 859.76
Current children cumulated vsize (Kb) 22464

[startup+870.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4724 0 0 0 86935 42 0 0 25 0 1 0 1841344534 20828160 4708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4708 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 869.77
Current children cumulated vsize (Kb) 22464

[startup+880.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4724 0 0 0 87935 42 0 0 25 0 1 0 1841344534 20828160 4708 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4708 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 879.77
Current children cumulated vsize (Kb) 22464

[startup+890.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4725 0 0 0 88935 42 0 0 25 0 1 0 1841344534 20828160 4709 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4709 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 889.77
Current children cumulated vsize (Kb) 22464

[startup+900.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4726 0 0 0 89935 42 0 0 25 0 1 0 1841344534 20828160 4710 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5085 4710 145 145 0 4940 0
[pid=6404] vsize: 20340
Current children cumulated CPU time (s) 899.77
Current children cumulated vsize (Kb) 22464

[startup+910.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4758 0 0 0 90935 42 0 0 25 0 1 0 1841344534 20959232 4742 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5117 4742 145 145 0 4972 0
[pid=6404] vsize: 20468
Current children cumulated CPU time (s) 909.77
Current children cumulated vsize (Kb) 22592

[startup+920.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4781 0 0 0 91935 42 0 0 25 0 1 0 1841344534 21045248 4765 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5138 4765 145 145 0 4993 0
[pid=6404] vsize: 20552
Current children cumulated CPU time (s) 919.77
Current children cumulated vsize (Kb) 22676

[startup+930.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4942 0 0 0 92931 44 0 0 25 0 1 0 1841344534 21729280 4926 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5305 4926 145 145 0 5160 0
[pid=6404] vsize: 21220
Current children cumulated CPU time (s) 929.75
Current children cumulated vsize (Kb) 23344

[startup+940.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5073 0 0 0 93929 45 0 0 25 0 1 0 1841344534 22380544 5057 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5464 5057 145 145 0 5319 0
[pid=6404] vsize: 21856
Current children cumulated CPU time (s) 939.74
Current children cumulated vsize (Kb) 23980

[startup+950.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5080 0 0 0 94929 45 0 0 25 0 1 0 1841344534 22413312 5064 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5472 5064 145 145 0 5327 0
[pid=6404] vsize: 21888
Current children cumulated CPU time (s) 949.74
Current children cumulated vsize (Kb) 24012

[startup+960.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5083 0 0 0 95929 45 0 0 25 0 1 0 1841344534 22478848 5067 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5488 5067 145 145 0 5343 0
[pid=6404] vsize: 21952
Current children cumulated CPU time (s) 959.74
Current children cumulated vsize (Kb) 24076

[startup+970.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5083 0 0 0 96930 45 0 0 25 0 1 0 1841344534 22478848 5067 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5488 5067 145 145 0 5343 0
[pid=6404] vsize: 21952
Current children cumulated CPU time (s) 969.75
Current children cumulated vsize (Kb) 24076

[startup+980.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5089 0 0 0 97930 45 0 0 25 0 1 0 1841344534 22478848 5073 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5488 5073 145 145 0 5343 0
[pid=6404] vsize: 21952
Current children cumulated CPU time (s) 979.75
Current children cumulated vsize (Kb) 24076

[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5241 0 0 0 98928 46 0 0 25 0 1 0 1841344534 23113728 5225 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5643 5225 145 145 0 5498 0
[pid=6404] vsize: 22572
Current children cumulated CPU time (s) 989.74
Current children cumulated vsize (Kb) 24696

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5484 0 0 0 99924 48 0 0 25 0 1 0 1841344534 24109056 5468 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5886 5468 145 145 0 5741 0
[pid=6404] vsize: 23544
Current children cumulated CPU time (s) 999.72
Current children cumulated vsize (Kb) 25668

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 100923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0
[pid=6404] vsize: 23748
Current children cumulated CPU time (s) 1009.71
Current children cumulated vsize (Kb) 25872

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 101923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0
[pid=6404] vsize: 23748
Current children cumulated CPU time (s) 1019.71
Current children cumulated vsize (Kb) 25872

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 102923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0
[pid=6404] vsize: 23748
Current children cumulated CPU time (s) 1029.71
Current children cumulated vsize (Kb) 25872

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5536 0 0 0 103923 48 0 0 25 0 1 0 1841344534 24317952 5520 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5937 5520 145 145 0 5792 0
[pid=6404] vsize: 23748
Current children cumulated CPU time (s) 1039.71
Current children cumulated vsize (Kb) 25872

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5577 0 0 0 104924 48 0 0 25 0 1 0 1841344534 24514560 5561 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 5985 5561 145 145 0 5840 0
[pid=6404] vsize: 23940
Current children cumulated CPU time (s) 1049.72
Current children cumulated vsize (Kb) 26064

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5725 0 0 0 105921 49 0 0 25 0 1 0 1841344534 25116672 5709 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6132 5709 145 145 0 5987 0
[pid=6404] vsize: 24528
Current children cumulated CPU time (s) 1059.7
Current children cumulated vsize (Kb) 26652

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5943 0 0 0 106918 51 0 0 25 0 1 0 1841344534 26038272 5927 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6357 5927 145 145 0 6212 0
[pid=6404] vsize: 25428
Current children cumulated CPU time (s) 1069.69
Current children cumulated vsize (Kb) 27552

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5951 0 0 0 107918 51 0 0 25 0 1 0 1841344534 26071040 5935 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6365 5935 145 145 0 6220 0
[pid=6404] vsize: 25460
Current children cumulated CPU time (s) 1079.69
Current children cumulated vsize (Kb) 27584

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5951 0 0 0 108918 51 0 0 25 0 1 0 1841344534 26071040 5935 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6365 5935 145 145 0 6220 0
[pid=6404] vsize: 25460
Current children cumulated CPU time (s) 1089.69
Current children cumulated vsize (Kb) 27584

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5956 0 0 0 109918 51 0 0 25 0 1 0 1841344534 26103808 5940 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6373 5940 145 145 0 6228 0
[pid=6404] vsize: 25492
Current children cumulated CPU time (s) 1099.69
Current children cumulated vsize (Kb) 27616

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5956 0 0 0 110919 51 0 0 25 0 1 0 1841344534 26103808 5940 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6373 5940 145 145 0 6228 0
[pid=6404] vsize: 25492
Current children cumulated CPU time (s) 1109.7
Current children cumulated vsize (Kb) 27616

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5963 0 0 0 111919 51 0 0 25 0 1 0 1841344534 26136576 5947 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6381 5947 145 145 0 6236 0
[pid=6404] vsize: 25524
Current children cumulated CPU time (s) 1119.7
Current children cumulated vsize (Kb) 27648

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 112919 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0
[pid=6404] vsize: 25588
Current children cumulated CPU time (s) 1129.7
Current children cumulated vsize (Kb) 27712

[startup+1140.11 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 113919 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0
[pid=6404] vsize: 25588
Current children cumulated CPU time (s) 1139.7
Current children cumulated vsize (Kb) 27712

[startup+1150.11 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 114920 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0
[pid=6404] vsize: 25588
Current children cumulated CPU time (s) 1149.71
Current children cumulated vsize (Kb) 27712

[startup+1160.11 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5978 0 0 0 115920 51 0 0 25 0 1 0 1841344534 26202112 5962 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6397 5962 145 145 0 6252 0
[pid=6404] vsize: 25588
Current children cumulated CPU time (s) 1159.71
Current children cumulated vsize (Kb) 27712

[startup+1170.11 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5989 0 0 0 116920 51 0 0 25 0 1 0 1841344534 26267648 5973 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6413 5973 145 145 0 6268 0
[pid=6404] vsize: 25652
Current children cumulated CPU time (s) 1169.71
Current children cumulated vsize (Kb) 27776

[startup+1180.11 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6000 0 0 0 117920 51 0 0 25 0 1 0 1841344534 26333184 5984 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6429 5984 145 145 0 6284 0
[pid=6404] vsize: 25716
Current children cumulated CPU time (s) 1179.71
Current children cumulated vsize (Kb) 27840

[startup+1190.11 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6001 0 0 0 118921 51 0 0 25 0 1 0 1841344534 26333184 5985 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6429 5985 145 145 0 6284 0
[pid=6404] vsize: 25716
Current children cumulated CPU time (s) 1189.72
Current children cumulated vsize (Kb) 27840

[startup+1200.11 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 119921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221223104 134558549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0
[pid=6404] vsize: 25716
Current children cumulated CPU time (s) 1199.72
Current children cumulated vsize (Kb) 27840

[startup+1210.11 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 120921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0
[pid=6404] vsize: 25716
Current children cumulated CPU time (s) 1209.72
Current children cumulated vsize (Kb) 27840



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 6404
Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6400/statm): 531 226 485 147 0 384 0
[pid=6400] vsize: 2124
Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 120921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221222912 134781560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0
[pid=6404] vsize: 25716
Current children cumulated CPU time (s) 1209.72
Current children cumulated vsize (Kb) 27840

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.75
CPU user time (s): 1209.22
CPU system time (s): 0.529919
CPU usage (%): 99.9683
Max. virtual memory (cumulated for all children) (Kb): 27840

Verifier Data

ERROR: no interpretation found !