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

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb
MD5SUM2854384016ebafb26c8bfb47f81aee87
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 324
Optimality of the best value was proved NO
Number of terms in the objective function 63009
Biggest coefficient in the objective function 2
Number of bits for the biggest coefficient in the objective function 2
Sum of the numbers in the objective function 122425
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 2
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 122425
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.19
Number of variables63009
Total number of constraints63516
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63009
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint7753

Trace number 4509

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        869528 kB
Buffers:         34828 kB
Cached:          99664 kB
SwapCached:        692 kB
Active:          79044 kB
Inactive:        58072 kB
HighTotal:      131008 kB
HighFree:        29540 kB
LowTotal:       903652 kB
LowFree:        839988 kB
SwapTotal:     2097136 kB
SwapFree:      2095920 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            22232 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:06:19 (client local time) WITH STATUS 10 IN 1206.92 SECONDS
stats: 2969 7 1206.92 10

Solver Data

c Parsing PB file...
c Converting 494 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     487   407371 |     162       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 343
c ---[   0]---> Adder-cost: 125984   maxlim: 122082   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  882303  3556733 |  294101       0        0     nan |  0.000 % |
c |       100 |  882255  3556553 |  323511      96      289     3.0 |  0.016 % |
c |       250 |  881309  3553217 |  355862     114      351     3.1 |  0.101 % |
c |       475 |  880776  3551348 |  391448     259      864     3.3 |  0.151 % |
c |       812 |  880279  3549615 |  430593     523     1870     3.6 |  0.196 % |
c |      1318 |  879889  3548279 |  473652     977     4292     4.4 |  0.232 % |
c |      2077 |  879700  3547656 |  521017    1709    10871     6.4 |  0.251 % |
c |      3216 |  879644  3547470 |  573119    2839    17243     6.1 |  0.256 % |
c |      4924 |  879509  3547011 |  630431    4532    25034     5.5 |  0.270 % |
c |      7486 |  879420  3546722 |  693474    7079    43284     6.1 |  0.279 % |
c |     11330 |  879361  3546531 |  762822   10915    68960     6.3 |  0.286 % |
c |     17096 |  879361  3546531 |  839104   16681   104664     6.3 |  0.286 % |
c |     25745 |  879361  3546531 |  923014   25330   246101     9.7 |  0.286 % |
c |     38719 |  879284  3546264 | 1015316   38293   536469    14.0 |  0.293 % |
c 
c *** TERMINATED ***
s SATISFIABLE

#### TRACE IS TOO LONG. SEE FILE pb05-wulflinc15-2969-625-3-0-26715.out.gz TO GET THE COMPLETE TRACE
#### TAIL OF TRACE ####
...c Parsing PB file...
c Converting 494 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     487   407371 |     162       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 343
c ---[   0]---> Adder-cost: 125984   maxlim: 122082   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  882303  3556733 |  294101       0        0     nan |  0.000 % |
c |       100 |  882255  3556553 |  323511      96      289     3.0 |  0.016 % |
c |       250 |  881309  3553217 |  355862     114      351     3.1 |  0.101 % |
c |       475 |  880776  3551348 |  391448     259      864     3.3 |  0.151 % |
c |       812 |  880279  3549615 |  430593     523     1870     3.6 |  0.196 % |
c |      1318 |  879889  3548279 |  473652     977     4292     4.4 |  0.232 % |
c |      2077 |  879700  3547656 |  521017    1709    10871     6.4 |  0.251 % |
c |      3216 |  879644  3547470 |  573119    2839    17243     6.1 |  0.256 % |
c |      4924 |  879509  3547011 |  630431    4532    25034     5.5 |  0.270 % |
c |      7486 |  879420  3546722 |  693474    7079    43284     6.1 |  0.279 % |
c |     11330 |  879361  3546531 |  762822   10915    68960     6.3 |  0.286 % |
c |     17096 |  879361  3546531 |  839104   16681   104664     6.3 |  0.286 % |
c |     25745 |  879361  3546531 |  923014   25330   246101     9.7 |  0.286 % |
c |     38719 |  879284  3546264 | 1015316   38293   536469    14.0 |  0.293 % |
c 
c *** TERMINATED ***
s SATISFIABLE

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/26752/stat): 26752 (minisat+_script) R 26751 26752 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793566526 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26752/statm): 174 3 169 147 0 27 0
[pid=26752] 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=26753
New process pid=26754
New process pid=26755
execve syscall for /bin/sed executable
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
One traced child (pid=26754) exited with status: 0
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=26755) exited with status: 0
One traced child (pid=26753) exited with status: 0
New process pid=26756
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-fast0507.opb

[startup+10.0044 s]
Raw data (loadavg): 0.93 0.96 0.70 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 15160 0 2 0 874 61 0 0 25 0 1 0 1793566531 46866432 10633 4294967295 134512640 135094434 3221224432 3221222384 134519645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 11442 10633 145 145 0 11297 0
[pid=26756] vsize: 45768
Current children cumulated CPU time (s) 9.35
Current children cumulated vsize (Kb) 47892

[startup+20.0063 s]
Raw data (loadavg): 0.94 0.96 0.70 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 55609 0 2 0 1674 182 0 0 23 0 1 0 1793566531 184619008 41195 4294967295 134512640 135094434 3221224432 3221221536 134781751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 45073 41195 145 145 0 44928 0
[pid=26756] vsize: 180292
Current children cumulated CPU time (s) 18.56
Current children cumulated vsize (Kb) 182416

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.71 1/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) T 26752 26752 31778 0 -1 0 97330 0 2 0 2479 301 0 0 24 0 1 0 1793566531 331378688 72370 4294967295 134512640 135094434 3221224432 3221221180 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26756/statm): 80903 72370 145 145 0 80758 0
[pid=26756] vsize: 323612
Current children cumulated CPU time (s) 27.8
Current children cumulated vsize (Kb) 325736

[startup+40.0079 s]
Raw data (loadavg): 0.96 0.96 0.71 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 113784 0 2 0 3366 355 0 0 25 0 1 0 1793566531 371798016 88101 4294967295 134512640 135094434 3221224432 3221222992 134516573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 90771 88101 145 145 0 90626 0
[pid=26756] vsize: 363084
Current children cumulated CPU time (s) 37.21
Current children cumulated vsize (Kb) 365208

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.96 0.71 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 126979 0 2 0 4250 411 0 0 25 0 1 0 1793566531 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 104579 101111 145 145 0 104434 0
[pid=26756] vsize: 418316
Current children cumulated CPU time (s) 46.61
Current children cumulated vsize (Kb) 420440

[startup+60.0096 s]
Raw data (loadavg): 0.97 0.96 0.72 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 126988 0 2 0 5251 411 0 0 25 0 1 0 1793566531 428392448 101120 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 104588 101120 145 145 0 104443 0
[pid=26756] vsize: 418352
Current children cumulated CPU time (s) 56.62
Current children cumulated vsize (Kb) 420476

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.96 0.72 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127007 0 2 0 6250 411 0 0 25 0 1 0 1793566531 428470272 101139 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 104607 101139 145 145 0 104462 0
[pid=26756] vsize: 418428
Current children cumulated CPU time (s) 66.61
Current children cumulated vsize (Kb) 420552

[startup+80.0124 s]
Raw data (loadavg): 0.98 0.96 0.72 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127056 0 2 0 7249 411 0 0 25 0 1 0 1793566531 428670976 101188 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 104656 101188 145 145 0 104511 0
[pid=26756] vsize: 418624
Current children cumulated CPU time (s) 76.6
Current children cumulated vsize (Kb) 420748

[startup+90.0132 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127543 0 2 0 8243 414 0 0 25 0 1 0 1793566531 430665728 101675 4294967295 134512640 135094434 3221224432 3221223092 134553506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105143 101675 145 145 0 104998 0
[pid=26756] vsize: 420572
Current children cumulated CPU time (s) 86.57
Current children cumulated vsize (Kb) 422696

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.73 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127742 0 2 0 9239 416 0 0 25 0 1 0 1793566531 431714304 101874 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105399 101874 145 145 0 105254 0
[pid=26756] vsize: 421596
Current children cumulated CPU time (s) 96.55
Current children cumulated vsize (Kb) 423720

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.73 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127829 0 2 0 10239 416 0 0 25 0 1 0 1793566531 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105468 101961 145 145 0 105323 0
[pid=26756] vsize: 421872
Current children cumulated CPU time (s) 106.55
Current children cumulated vsize (Kb) 423996

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127887 0 2 0 11236 418 0 0 25 0 1 0 1793566531 432234496 102019 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105526 102019 145 145 0 105381 0
[pid=26756] vsize: 422104
Current children cumulated CPU time (s) 116.54
Current children cumulated vsize (Kb) 424228

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.73 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127933 0 2 0 12235 419 0 0 25 0 1 0 1793566531 432418816 102065 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 105571 102065 145 145 0 105426 0
[pid=26756] vsize: 422284
Current children cumulated CPU time (s) 126.54
Current children cumulated vsize (Kb) 424408

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127976 0 2 0 13234 419 0 0 25 0 1 0 1793566531 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105598 102108 145 145 0 105453 0
[pid=26756] vsize: 422392
Current children cumulated CPU time (s) 136.53
Current children cumulated vsize (Kb) 424516

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128005 0 2 0 14234 419 0 0 25 0 1 0 1793566531 432631808 102137 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105623 102137 145 145 0 105478 0
[pid=26756] vsize: 422492
Current children cumulated CPU time (s) 146.53
Current children cumulated vsize (Kb) 424616

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128026 0 2 0 15233 420 0 0 25 0 1 0 1793566531 432701440 102158 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105640 102158 145 145 0 105495 0
[pid=26756] vsize: 422560
Current children cumulated CPU time (s) 156.53
Current children cumulated vsize (Kb) 424684

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128041 0 2 0 16234 420 0 0 25 0 1 0 1793566531 432762880 102173 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105655 102173 145 145 0 105510 0
[pid=26756] vsize: 422620
Current children cumulated CPU time (s) 166.54
Current children cumulated vsize (Kb) 424744

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.74 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128054 0 2 0 17233 420 0 0 25 0 1 0 1793566531 432812032 102186 4294967295 134512640 135094434 3221224432 3221223168 134559155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105667 102186 145 145 0 105522 0
[pid=26756] vsize: 422668
Current children cumulated CPU time (s) 176.53
Current children cumulated vsize (Kb) 424792

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128063 0 2 0 18233 420 0 0 25 0 1 0 1793566531 432848896 102195 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105676 102195 145 145 0 105531 0
[pid=26756] vsize: 422704
Current children cumulated CPU time (s) 186.53
Current children cumulated vsize (Kb) 424828

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128079 0 2 0 19233 421 0 0 25 0 1 0 1793566531 432943104 102211 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105699 102211 145 145 0 105554 0
[pid=26756] vsize: 422796
Current children cumulated CPU time (s) 196.54
Current children cumulated vsize (Kb) 424920

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128079 0 2 0 20233 421 0 0 25 0 1 0 1793566531 432943104 102211 4294967295 134512640 135094434 3221224432 3221223148 134561442 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105699 102211 145 145 0 105554 0
[pid=26756] vsize: 422796
Current children cumulated CPU time (s) 206.54
Current children cumulated vsize (Kb) 424920

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128086 0 2 0 21234 421 0 0 25 0 1 0 1793566531 432967680 102218 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105705 102218 145 145 0 105560 0
[pid=26756] vsize: 422820
Current children cumulated CPU time (s) 216.55
Current children cumulated vsize (Kb) 424944

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128095 0 2 0 22233 421 0 0 25 0 1 0 1793566531 432988160 102227 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105710 102227 145 145 0 105565 0
[pid=26756] vsize: 422840
Current children cumulated CPU time (s) 226.54
Current children cumulated vsize (Kb) 424964

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128100 0 2 0 23233 421 0 0 25 0 1 0 1793566531 433008640 102232 4294967295 134512640 135094434 3221224432 3221223136 134554526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105715 102232 145 145 0 105570 0
[pid=26756] vsize: 422860
Current children cumulated CPU time (s) 236.54
Current children cumulated vsize (Kb) 424984

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128108 0 2 0 24234 421 0 0 25 0 1 0 1793566531 433037312 102240 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105722 102240 145 145 0 105577 0
[pid=26756] vsize: 422888
Current children cumulated CPU time (s) 246.55
Current children cumulated vsize (Kb) 425012

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128112 0 2 0 25234 422 0 0 25 0 1 0 1793566531 433053696 102244 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105726 102244 145 145 0 105581 0
[pid=26756] vsize: 422904
Current children cumulated CPU time (s) 256.56
Current children cumulated vsize (Kb) 425028

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128122 0 2 0 26234 422 0 0 25 0 1 0 1793566531 433074176 102254 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105731 102254 145 145 0 105586 0
[pid=26756] vsize: 422924
Current children cumulated CPU time (s) 266.56
Current children cumulated vsize (Kb) 425048

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128128 0 2 0 27234 422 0 0 25 0 1 0 1793566531 433098752 102260 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105737 102260 145 145 0 105592 0
[pid=26756] vsize: 422948
Current children cumulated CPU time (s) 276.56
Current children cumulated vsize (Kb) 425072

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128130 0 2 0 28234 422 0 0 25 0 1 0 1793566531 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105739 102262 145 145 0 105594 0
[pid=26756] vsize: 422956
Current children cumulated CPU time (s) 286.56
Current children cumulated vsize (Kb) 425080

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128132 0 2 0 29234 422 0 0 25 0 1 0 1793566531 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105741 102264 145 145 0 105596 0
[pid=26756] vsize: 422964
Current children cumulated CPU time (s) 296.56
Current children cumulated vsize (Kb) 425088

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128139 0 2 0 30234 422 0 0 25 0 1 0 1793566531 433135616 102271 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105746 102271 145 145 0 105601 0
[pid=26756] vsize: 422984
Current children cumulated CPU time (s) 306.56
Current children cumulated vsize (Kb) 425108

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128144 0 2 0 31234 422 0 0 25 0 1 0 1793566531 433147904 102276 4294967295 134512640 135094434 3221224432 3221223088 134561720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105749 102276 145 145 0 105604 0
[pid=26756] vsize: 422996
Current children cumulated CPU time (s) 316.56
Current children cumulated vsize (Kb) 425120

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128148 0 2 0 32234 422 0 0 25 0 1 0 1793566531 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105753 102280 145 145 0 105608 0
[pid=26756] vsize: 423012
Current children cumulated CPU time (s) 326.56
Current children cumulated vsize (Kb) 425136

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128151 0 2 0 33234 422 0 0 25 0 1 0 1793566531 433172480 102283 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105755 102283 145 145 0 105610 0
[pid=26756] vsize: 423020
Current children cumulated CPU time (s) 336.56
Current children cumulated vsize (Kb) 425144

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128154 0 2 0 34235 422 0 0 25 0 1 0 1793566531 433184768 102286 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105758 102286 145 145 0 105613 0
[pid=26756] vsize: 423032
Current children cumulated CPU time (s) 346.57
Current children cumulated vsize (Kb) 425156

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128157 0 2 0 35235 423 0 0 25 0 1 0 1793566531 433197056 102289 4294967295 134512640 135094434 3221224432 3221223044 134563039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105761 102289 145 145 0 105616 0
[pid=26756] vsize: 423044
Current children cumulated CPU time (s) 356.58
Current children cumulated vsize (Kb) 425168

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128165 0 2 0 36235 423 0 0 25 0 1 0 1793566531 433225728 102297 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105768 102297 145 145 0 105623 0
[pid=26756] vsize: 423072
Current children cumulated CPU time (s) 366.58
Current children cumulated vsize (Kb) 425196

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128167 0 2 0 37235 423 0 0 25 0 1 0 1793566531 433233920 102299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105770 102299 145 145 0 105625 0
[pid=26756] vsize: 423080
Current children cumulated CPU time (s) 376.58
Current children cumulated vsize (Kb) 425204

[startup+390.042 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128171 0 2 0 38236 423 0 0 25 0 1 0 1793566531 433238016 102303 4294967295 134512640 135094434 3221224432 3221223088 134561707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105771 102303 145 145 0 105626 0
[pid=26756] vsize: 423084
Current children cumulated CPU time (s) 386.59
Current children cumulated vsize (Kb) 425208

[startup+400.043 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128173 0 2 0 39236 423 0 0 25 0 1 0 1793566531 433246208 102305 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105773 102305 145 145 0 105628 0
[pid=26756] vsize: 423092
Current children cumulated CPU time (s) 396.59
Current children cumulated vsize (Kb) 425216

[startup+410.043 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128176 0 2 0 40236 423 0 0 25 0 1 0 1793566531 433254400 102308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105775 102308 145 145 0 105630 0
[pid=26756] vsize: 423100
Current children cumulated CPU time (s) 406.59
Current children cumulated vsize (Kb) 425224

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128178 0 2 0 41236 423 0 0 25 0 1 0 1793566531 433262592 102310 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105777 102310 145 145 0 105632 0
[pid=26756] vsize: 423108
Current children cumulated CPU time (s) 416.59
Current children cumulated vsize (Kb) 425232

[startup+430.046 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128181 0 2 0 42236 423 0 0 25 0 1 0 1793566531 433274880 102313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105780 102313 145 145 0 105635 0
[pid=26756] vsize: 423120
Current children cumulated CPU time (s) 426.59
Current children cumulated vsize (Kb) 425244

[startup+440.047 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128185 0 2 0 43236 423 0 0 25 0 1 0 1793566531 433291264 102317 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105784 102317 145 145 0 105639 0
[pid=26756] vsize: 423136
Current children cumulated CPU time (s) 436.59
Current children cumulated vsize (Kb) 425260

[startup+450.047 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128191 0 2 0 44236 423 0 0 25 0 1 0 1793566531 433311744 102323 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105789 102323 145 145 0 105644 0
[pid=26756] vsize: 423156
Current children cumulated CPU time (s) 446.59
Current children cumulated vsize (Kb) 425280

[startup+460.049 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128213 0 2 0 45236 424 0 0 25 0 1 0 1793566531 433446912 102345 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105822 102345 145 145 0 105677 0
[pid=26756] vsize: 423288
Current children cumulated CPU time (s) 456.6
Current children cumulated vsize (Kb) 425412

[startup+470.049 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128215 0 2 0 46235 424 0 0 25 0 1 0 1793566531 433451008 102347 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105823 102347 145 145 0 105678 0
[pid=26756] vsize: 423292
Current children cumulated CPU time (s) 466.59
Current children cumulated vsize (Kb) 425416

[startup+480.05 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128217 0 2 0 47235 424 0 0 25 0 1 0 1793566531 433459200 102349 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105825 102349 145 145 0 105680 0
[pid=26756] vsize: 423300
Current children cumulated CPU time (s) 476.59
Current children cumulated vsize (Kb) 425424

[startup+490.051 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128227 0 2 0 48235 424 0 0 25 0 1 0 1793566531 433496064 102359 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105834 102359 145 145 0 105689 0
[pid=26756] vsize: 423336
Current children cumulated CPU time (s) 486.59
Current children cumulated vsize (Kb) 425460

[startup+500.052 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128234 0 2 0 49236 424 0 0 25 0 1 0 1793566531 433524736 102366 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105841 102366 145 145 0 105696 0
[pid=26756] vsize: 423364
Current children cumulated CPU time (s) 496.6
Current children cumulated vsize (Kb) 425488

[startup+510.053 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128245 0 2 0 50236 424 0 0 25 0 1 0 1793566531 433565696 102377 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105851 102377 145 145 0 105706 0
[pid=26756] vsize: 423404
Current children cumulated CPU time (s) 506.6
Current children cumulated vsize (Kb) 425528

[startup+520.054 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128252 0 2 0 51236 424 0 0 25 0 1 0 1793566531 433594368 102384 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105858 102384 145 145 0 105713 0
[pid=26756] vsize: 423432
Current children cumulated CPU time (s) 516.6
Current children cumulated vsize (Kb) 425556

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128262 0 2 0 52236 424 0 0 25 0 1 0 1793566531 433631232 102394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105867 102394 145 145 0 105722 0
[pid=26756] vsize: 423468
Current children cumulated CPU time (s) 526.6
Current children cumulated vsize (Kb) 425592

[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.81 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128321 0 2 0 53235 425 0 0 25 0 1 0 1793566531 433831936 102453 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105916 102453 145 145 0 105771 0
[pid=26756] vsize: 423664
Current children cumulated CPU time (s) 536.6
Current children cumulated vsize (Kb) 425788

[startup+550.057 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128324 0 2 0 54236 425 0 0 25 0 1 0 1793566531 433844224 102456 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105919 102456 145 145 0 105774 0
[pid=26756] vsize: 423676
Current children cumulated CPU time (s) 546.61
Current children cumulated vsize (Kb) 425800

[startup+560.058 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128327 0 2 0 55236 425 0 0 25 0 1 0 1793566531 433856512 102459 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105922 102459 145 145 0 105777 0
[pid=26756] vsize: 423688
Current children cumulated CPU time (s) 556.61
Current children cumulated vsize (Kb) 425812

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128332 0 2 0 56236 425 0 0 25 0 1 0 1793566531 433872896 102464 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105926 102464 145 145 0 105781 0
[pid=26756] vsize: 423704
Current children cumulated CPU time (s) 566.61
Current children cumulated vsize (Kb) 425828

[startup+580.06 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128339 0 2 0 57236 425 0 0 25 0 1 0 1793566531 433901568 102471 4294967295 134512640 135094434 3221224432 3221223088 134561784 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105933 102471 145 145 0 105788 0
[pid=26756] vsize: 423732
Current children cumulated CPU time (s) 576.61
Current children cumulated vsize (Kb) 425856

[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128346 0 2 0 58236 425 0 0 25 0 1 0 1793566531 433930240 102478 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105940 102478 145 145 0 105795 0
[pid=26756] vsize: 423760
Current children cumulated CPU time (s) 586.61
Current children cumulated vsize (Kb) 425884

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128355 0 2 0 59236 425 0 0 25 0 1 0 1793566531 433958912 102487 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105947 102487 145 145 0 105802 0
[pid=26756] vsize: 423788
Current children cumulated CPU time (s) 596.61
Current children cumulated vsize (Kb) 425912

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128383 0 2 0 60235 425 0 0 25 0 1 0 1793566531 434073600 102515 4294967295 134512640 135094434 3221224432 3221223060 134562984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 105975 102515 145 145 0 105830 0
[pid=26756] vsize: 423900
Current children cumulated CPU time (s) 606.6
Current children cumulated vsize (Kb) 426024

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.82 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128387 0 2 0 61233 426 0 0 25 0 1 0 1793566531 434089984 102519 4294967295 134512640 135094434 3221224432 3221223156 134558440 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105979 102519 145 145 0 105834 0
[pid=26756] vsize: 423916
Current children cumulated CPU time (s) 616.59
Current children cumulated vsize (Kb) 426040

[startup+630.064 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128396 0 2 0 62234 426 0 0 25 0 1 0 1793566531 434122752 102528 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105987 102528 145 145 0 105842 0
[pid=26756] vsize: 423948
Current children cumulated CPU time (s) 626.6
Current children cumulated vsize (Kb) 426072

[startup+640.065 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128403 0 2 0 63234 426 0 0 25 0 1 0 1793566531 434151424 102535 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 105994 102535 145 145 0 105849 0
[pid=26756] vsize: 423976
Current children cumulated CPU time (s) 636.6
Current children cumulated vsize (Kb) 426100

[startup+650.066 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128412 0 2 0 64233 427 0 0 25 0 1 0 1793566531 434188288 102544 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106003 102544 145 145 0 105858 0
[pid=26756] vsize: 424012
Current children cumulated CPU time (s) 646.6
Current children cumulated vsize (Kb) 426136

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128429 0 2 0 65233 427 0 0 25 0 1 0 1793566531 434253824 102561 4294967295 134512640 135094434 3221224432 3221223088 134561589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106019 102561 145 145 0 105874 0
[pid=26756] vsize: 424076
Current children cumulated CPU time (s) 656.6
Current children cumulated vsize (Kb) 426200

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128495 0 2 0 66233 427 0 0 25 0 1 0 1793566531 434515968 102627 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 106083 102627 145 145 0 105938 0
[pid=26756] vsize: 424332
Current children cumulated CPU time (s) 666.6
Current children cumulated vsize (Kb) 426456

[startup+680.069 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128503 0 2 0 67231 427 0 0 25 0 1 0 1793566531 434548736 102635 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 106091 102635 145 145 0 105946 0
[pid=26756] vsize: 424364
Current children cumulated CPU time (s) 676.58
Current children cumulated vsize (Kb) 426488

[startup+690.07 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128510 0 2 0 68231 427 0 0 25 0 1 0 1793566531 434565120 102642 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106095 102642 145 145 0 105950 0
[pid=26756] vsize: 424380
Current children cumulated CPU time (s) 686.58
Current children cumulated vsize (Kb) 426504

[startup+700.071 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128515 0 2 0 69231 428 0 0 25 0 1 0 1793566531 434585600 102647 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106100 102647 145 145 0 105955 0
[pid=26756] vsize: 424400
Current children cumulated CPU time (s) 696.59
Current children cumulated vsize (Kb) 426524

[startup+710.072 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128517 0 2 0 70231 428 0 0 25 0 1 0 1793566531 434593792 102649 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106102 102649 145 145 0 105957 0
[pid=26756] vsize: 424408
Current children cumulated CPU time (s) 706.59
Current children cumulated vsize (Kb) 426532

[startup+720.073 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128521 0 2 0 71230 429 0 0 25 0 1 0 1793566531 434601984 102653 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106104 102653 145 145 0 105959 0
[pid=26756] vsize: 424416
Current children cumulated CPU time (s) 716.59
Current children cumulated vsize (Kb) 426540

[startup+730.074 s]
Raw data (loadavg): 0.99 0.97 0.83 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128522 0 2 0 72230 429 0 0 25 0 1 0 1793566531 434606080 102654 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106105 102654 145 145 0 105960 0
[pid=26756] vsize: 424420
Current children cumulated CPU time (s) 726.59
Current children cumulated vsize (Kb) 426544

[startup+740.076 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128531 0 2 0 73230 430 0 0 25 0 1 0 1793566531 434642944 102663 4294967295 134512640 135094434 3221224432 3221223088 134561744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106114 102663 145 145 0 105969 0
[pid=26756] vsize: 424456
Current children cumulated CPU time (s) 736.6
Current children cumulated vsize (Kb) 426580

[startup+750.076 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128534 0 2 0 74230 430 0 0 25 0 1 0 1793566531 434655232 102666 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106117 102666 145 145 0 105972 0
[pid=26756] vsize: 424468
Current children cumulated CPU time (s) 746.6
Current children cumulated vsize (Kb) 426592

[startup+760.077 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128536 0 2 0 75230 430 0 0 25 0 1 0 1793566531 434663424 102668 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106119 102668 145 145 0 105974 0
[pid=26756] vsize: 424476
Current children cumulated CPU time (s) 756.6
Current children cumulated vsize (Kb) 426600

[startup+770.077 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128540 0 2 0 76230 430 0 0 25 0 1 0 1793566531 434675712 102672 4294967295 134512640 135094434 3221224432 3221223136 134554559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106122 102672 145 145 0 105977 0
[pid=26756] vsize: 424488
Current children cumulated CPU time (s) 766.6
Current children cumulated vsize (Kb) 426612

[startup+780.079 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128567 0 2 0 77229 430 0 0 25 0 1 0 1793566531 434786304 102699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106149 102699 145 145 0 106004 0
[pid=26756] vsize: 424596
Current children cumulated CPU time (s) 776.59
Current children cumulated vsize (Kb) 426720

[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128657 0 2 0 78227 431 0 0 25 0 1 0 1793566531 435146752 102789 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106237 102789 145 145 0 106092 0
[pid=26756] vsize: 424948
Current children cumulated CPU time (s) 786.58
Current children cumulated vsize (Kb) 427072

[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128664 0 2 0 79227 432 0 0 25 0 1 0 1793566531 435175424 102796 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106244 102796 145 145 0 106099 0
[pid=26756] vsize: 424976
Current children cumulated CPU time (s) 796.59
Current children cumulated vsize (Kb) 427100

[startup+810.082 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128675 0 2 0 80227 432 0 0 25 0 1 0 1793566531 435220480 102807 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106255 102807 145 145 0 106110 0
[pid=26756] vsize: 425020
Current children cumulated CPU time (s) 806.59
Current children cumulated vsize (Kb) 427144

[startup+820.083 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 81227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 816.59
Current children cumulated vsize (Kb) 427428

[startup+830.084 s]
Raw data (loadavg): 0.99 0.97 0.84 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 82227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 826.59
Current children cumulated vsize (Kb) 427428

[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 83227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 836.59
Current children cumulated vsize (Kb) 427428

[startup+850.085 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128716 0 2 0 84227 432 0 0 25 0 1 0 1793566531 435511296 102848 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102848 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 846.59
Current children cumulated vsize (Kb) 427428

[startup+860.086 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128716 0 2 0 85227 432 0 0 25 0 1 0 1793566531 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102848 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 856.59
Current children cumulated vsize (Kb) 427428

[startup+870.087 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128717 0 2 0 86227 432 0 0 25 0 1 0 1793566531 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102849 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 866.59
Current children cumulated vsize (Kb) 427428

[startup+880.089 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128718 0 2 0 87228 432 0 0 25 0 1 0 1793566531 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106326 102850 145 145 0 106181 0
[pid=26756] vsize: 425304
Current children cumulated CPU time (s) 876.6
Current children cumulated vsize (Kb) 427428

[startup+890.09 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128719 0 2 0 88228 432 0 0 25 0 1 0 1793566531 435515392 102851 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106327 102851 145 145 0 106182 0
[pid=26756] vsize: 425308
Current children cumulated CPU time (s) 886.6
Current children cumulated vsize (Kb) 427432

[startup+900.089 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128722 0 2 0 89228 433 0 0 25 0 1 0 1793566531 435527680 102854 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106330 102854 145 145 0 106185 0
[pid=26756] vsize: 425320
Current children cumulated CPU time (s) 896.61
Current children cumulated vsize (Kb) 427444

[startup+910.09 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128725 0 2 0 90228 433 0 0 25 0 1 0 1793566531 435539968 102857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106333 102857 145 145 0 106188 0
[pid=26756] vsize: 425332
Current children cumulated CPU time (s) 906.61
Current children cumulated vsize (Kb) 427456

[startup+920.091 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128741 0 2 0 91228 433 0 0 25 0 1 0 1793566531 435601408 102873 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106348 102873 145 145 0 106203 0
[pid=26756] vsize: 425392
Current children cumulated CPU time (s) 916.61
Current children cumulated vsize (Kb) 427516

[startup+930.092 s]
Raw data (loadavg): 0.99 0.97 0.85 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128768 0 2 0 92228 433 0 0 25 0 1 0 1793566531 435712000 102900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106375 102900 145 145 0 106230 0
[pid=26756] vsize: 425500
Current children cumulated CPU time (s) 926.61
Current children cumulated vsize (Kb) 427624

[startup+940.093 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128802 0 2 0 93227 434 0 0 25 0 1 0 1793566531 435847168 102934 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106408 102934 145 145 0 106263 0
[pid=26756] vsize: 425632
Current children cumulated CPU time (s) 936.61
Current children cumulated vsize (Kb) 427756

[startup+950.093 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128827 0 2 0 94227 434 0 0 25 0 1 0 1793566531 435945472 102959 4294967295 134512640 135094434 3221224432 3221223088 134561511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106432 102959 145 145 0 106287 0
[pid=26756] vsize: 425728
Current children cumulated CPU time (s) 946.61
Current children cumulated vsize (Kb) 427852

[startup+960.094 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128851 0 2 0 95227 434 0 0 25 0 1 0 1793566531 436043776 102983 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106456 102983 145 145 0 106311 0
[pid=26756] vsize: 425824
Current children cumulated CPU time (s) 956.61
Current children cumulated vsize (Kb) 427948

[startup+970.095 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128870 0 2 0 96227 434 0 0 25 0 1 0 1793566531 436117504 103002 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106474 103002 145 145 0 106329 0
[pid=26756] vsize: 425896
Current children cumulated CPU time (s) 966.61
Current children cumulated vsize (Kb) 428020

[startup+980.097 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128957 0 2 0 97224 435 0 0 25 0 1 0 1793566531 436465664 103089 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 106559 103089 145 145 0 106414 0
[pid=26756] vsize: 426236
Current children cumulated CPU time (s) 976.59
Current children cumulated vsize (Kb) 428360

[startup+990.099 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129064 0 2 0 98222 436 0 0 25 0 1 0 1793566531 436895744 103196 4294967295 134512640 135094434 3221224432 3221223088 134561755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26756/statm): 106664 103196 145 145 0 106519 0
[pid=26756] vsize: 426656
Current children cumulated CPU time (s) 986.58
Current children cumulated vsize (Kb) 428780

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129081 0 2 0 99222 436 0 0 25 0 1 0 1793566531 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106680 103213 145 145 0 106535 0
[pid=26756] vsize: 426720
Current children cumulated CPU time (s) 996.58
Current children cumulated vsize (Kb) 428844

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129086 0 2 0 100222 436 0 0 25 0 1 0 1793566531 436981760 103218 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106685 103218 145 145 0 106540 0
[pid=26756] vsize: 426740
Current children cumulated CPU time (s) 1006.58
Current children cumulated vsize (Kb) 428864

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129104 0 2 0 101222 437 0 0 25 0 1 0 1793566531 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106703 103236 145 145 0 106558 0
[pid=26756] vsize: 426812
Current children cumulated CPU time (s) 1016.59
Current children cumulated vsize (Kb) 428936

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.86 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129113 0 2 0 102222 437 0 0 25 0 1 0 1793566531 437088256 103245 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106711 103245 145 145 0 106566 0
[pid=26756] vsize: 426844
Current children cumulated CPU time (s) 1026.59
Current children cumulated vsize (Kb) 428968

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129132 0 2 0 103221 437 0 0 25 0 1 0 1793566531 437166080 103264 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106730 103264 145 145 0 106585 0
[pid=26756] vsize: 426920
Current children cumulated CPU time (s) 1036.58
Current children cumulated vsize (Kb) 429044

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129169 0 2 0 104221 437 0 0 25 0 1 0 1793566531 437313536 103301 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106766 103301 145 145 0 106621 0
[pid=26756] vsize: 427064
Current children cumulated CPU time (s) 1046.58
Current children cumulated vsize (Kb) 429188

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129196 0 2 0 105220 438 0 0 25 0 1 0 1793566531 437424128 103328 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106793 103328 145 145 0 106648 0
[pid=26756] vsize: 427172
Current children cumulated CPU time (s) 1056.58
Current children cumulated vsize (Kb) 429296

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129218 0 2 0 106220 438 0 0 25 0 1 0 1793566531 437514240 103350 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106815 103350 145 145 0 106670 0
[pid=26756] vsize: 427260
Current children cumulated CPU time (s) 1066.58
Current children cumulated vsize (Kb) 429384

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129234 0 2 0 107220 438 0 0 25 0 1 0 1793566531 437575680 103366 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106830 103366 145 145 0 106685 0
[pid=26756] vsize: 427320
Current children cumulated CPU time (s) 1076.58
Current children cumulated vsize (Kb) 429444

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129251 0 2 0 108219 439 0 0 25 0 1 0 1793566531 437645312 103383 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106847 103383 145 145 0 106702 0
[pid=26756] vsize: 427388
Current children cumulated CPU time (s) 1086.58
Current children cumulated vsize (Kb) 429512

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129263 0 2 0 109219 439 0 0 25 0 1 0 1793566531 437694464 103395 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106859 103395 145 145 0 106714 0
[pid=26756] vsize: 427436
Current children cumulated CPU time (s) 1096.58
Current children cumulated vsize (Kb) 429560

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129277 0 2 0 110219 439 0 0 25 0 1 0 1793566531 437747712 103409 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106872 103409 145 145 0 106727 0
[pid=26756] vsize: 427488
Current children cumulated CPU time (s) 1106.58
Current children cumulated vsize (Kb) 429612

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129297 0 2 0 111219 439 0 0 25 0 1 0 1793566531 437829632 103429 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106892 103429 145 145 0 106747 0
[pid=26756] vsize: 427568
Current children cumulated CPU time (s) 1116.58
Current children cumulated vsize (Kb) 429692

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129316 0 2 0 112219 439 0 0 25 0 1 0 1793566531 437907456 103448 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106911 103448 145 145 0 106766 0
[pid=26756] vsize: 427644
Current children cumulated CPU time (s) 1126.58
Current children cumulated vsize (Kb) 429768

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.87 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129326 0 2 0 113219 439 0 0 25 0 1 0 1793566531 437944320 103458 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106920 103458 145 145 0 106775 0
[pid=26756] vsize: 427680
Current children cumulated CPU time (s) 1136.58
Current children cumulated vsize (Kb) 429804

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129335 0 2 0 114219 440 0 0 25 0 1 0 1793566531 437985280 103467 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106930 103467 145 145 0 106785 0
[pid=26756] vsize: 427720
Current children cumulated CPU time (s) 1146.59
Current children cumulated vsize (Kb) 429844

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129338 0 2 0 115219 440 0 0 25 0 1 0 1793566531 437997568 103470 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106933 103470 145 145 0 106788 0
[pid=26756] vsize: 427732
Current children cumulated CPU time (s) 1156.59
Current children cumulated vsize (Kb) 429856

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129342 0 2 0 116220 440 0 0 25 0 1 0 1793566531 438013952 103474 4294967295 134512640 135094434 3221224432 3221223184 134559288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106937 103474 145 145 0 106792 0
[pid=26756] vsize: 427748
Current children cumulated CPU time (s) 1166.6
Current children cumulated vsize (Kb) 429872

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129350 0 2 0 117220 440 0 0 25 0 1 0 1793566531 438046720 103482 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106945 103482 145 145 0 106800 0
[pid=26756] vsize: 427780
Current children cumulated CPU time (s) 1176.6
Current children cumulated vsize (Kb) 429904

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129357 0 2 0 118220 440 0 0 25 0 1 0 1793566531 438071296 103489 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106951 103489 145 145 0 106806 0
[pid=26756] vsize: 427804
Current children cumulated CPU time (s) 1186.6
Current children cumulated vsize (Kb) 429928

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129373 0 2 0 119219 440 0 0 25 0 1 0 1793566531 438136832 103505 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106967 103505 145 145 0 106822 0
[pid=26756] vsize: 427868
Current children cumulated CPU time (s) 1196.59
Current children cumulated vsize (Kb) 429992

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129391 0 2 0 120219 440 0 0 25 0 1 0 1793566531 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106985 103523 145 145 0 106840 0
[pid=26756] vsize: 427940
Current children cumulated CPU time (s) 1206.59
Current children cumulated vsize (Kb) 430064



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 26756
Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26752/statm): 531 226 485 147 0 384 0
[pid=26752] vsize: 2124
Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129391 0 2 0 120219 440 0 0 25 0 1 0 1793566531 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26756/statm): 106985 103523 145 145 0 106840 0
[pid=26756] vsize: 427940
Current children cumulated CPU time (s) 1206.59
Current children cumulated vsize (Kb) 430064

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

Child status: 10
Real time (s): 1210.51
CPU time (s): 1206.92
CPU user time (s): 1202.3
CPU system time (s): 4.6183
CPU usage (%): 99.7029
Max. virtual memory (cumulated for all children) (Kb): 430064

Verifier Data

ERROR: no interpretation found !