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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.18
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 6190

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        874688 kB
Buffers:         25340 kB
Cached:         107840 kB
SwapCached:        916 kB
Active:          37236 kB
Inactive:        98536 kB
HighTotal:      131008 kB
HighFree:        22596 kB
LowTotal:       903652 kB
LowFree:        852092 kB
SwapTotal:     2097136 kB
SwapFree:      2095640 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18652 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:34:55 (client local time) WITH STATUS 10 IN 1207.2 SECONDS
stats: 3353 7 1207.2 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-wulflinc11-3353-1009-3-0-32739.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/308/stat): 308 (minisat+_script) R 307 308 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797344601 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/308/statm): 174 3 169 147 0 27 0
[pid=308] 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=309
New process pid=310
New process pid=311
execve syscall for /bin/sed executable
One traced child (pid=310) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=311) exited with status: 0
One traced child (pid=309) exited with status: 0
New process pid=312
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-fast0507.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.94 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 16770 0 0 0 889 63 0 0 25 0 1 0 1797344606 55410688 12241 4294967295 134512640 135094434 3221224432 3221222128 134519913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 13528 12241 145 145 0 13383 0
[pid=312] vsize: 54112
Current children cumulated CPU time (s) 9.53
Current children cumulated vsize (Kb) 56236

[startup+20.0051 s]
Raw data (loadavg): 1.02 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) T 308 308 9854 0 -1 0 56800 0 0 0 1693 182 0 0 23 0 1 0 1797344606 187686912 42384 4294967295 134512640 135094434 3221224432 3221221292 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/312/statm): 45822 42384 145 145 0 45677 0
[pid=312] vsize: 183288
Current children cumulated CPU time (s) 18.76
Current children cumulated vsize (Kb) 185412

[startup+30.0058 s]
Raw data (loadavg): 1.01 0.99 0.95 1/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) T 308 308 9854 0 -1 0 98834 0 0 0 2494 303 0 0 23 0 1 0 1797344606 335245312 73872 4294967295 134512640 135094434 3221224432 3221220508 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/312/statm): 81847 73872 145 145 0 81702 0
[pid=312] vsize: 327388
Current children cumulated CPU time (s) 27.98
Current children cumulated vsize (Kb) 329512

[startup+40.0066 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 115785 0 0 0 3383 358 0 0 22 0 1 0 1797344606 379695104 89915 4294967295 134512640 135094434 3221224432 3221216480 134522806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 92699 89915 145 145 0 92554 0
[pid=312] vsize: 370796
Current children cumulated CPU time (s) 37.42
Current children cumulated vsize (Kb) 372920

[startup+50.0084 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 126981 0 0 0 4277 410 0 0 25 0 1 0 1797344606 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 104579 101111 145 145 0 104434 0
[pid=312] vsize: 418316
Current children cumulated CPU time (s) 46.88
Current children cumulated vsize (Kb) 420440

[startup+60.0092 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 126991 0 0 0 5278 410 0 0 25 0 1 0 1797344606 428396544 101121 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 104589 101121 145 145 0 104444 0
[pid=312] vsize: 418356
Current children cumulated CPU time (s) 56.89
Current children cumulated vsize (Kb) 420480

[startup+70.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127009 0 0 0 6277 410 0 0 25 0 1 0 1797344606 428470272 101139 4294967295 134512640 135094434 3221224432 3221223108 134553436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 104607 101139 145 145 0 104462 0
[pid=312] vsize: 418428
Current children cumulated CPU time (s) 66.88
Current children cumulated vsize (Kb) 420552

[startup+80.0118 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127066 0 0 0 7275 411 0 0 25 0 1 0 1797344606 428703744 101196 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 104664 101196 145 145 0 104519 0
[pid=312] vsize: 418656
Current children cumulated CPU time (s) 76.87
Current children cumulated vsize (Kb) 420780

[startup+90.0115 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127547 0 0 0 8269 413 0 0 25 0 1 0 1797344606 430673920 101677 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105145 101677 145 145 0 105000 0
[pid=312] vsize: 420580
Current children cumulated CPU time (s) 86.83
Current children cumulated vsize (Kb) 422704

[startup+100.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127744 0 0 0 9267 414 0 0 25 0 1 0 1797344606 431714304 101874 4294967295 134512640 135094434 3221224432 3221223152 134558439 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105399 101874 145 145 0 105254 0
[pid=312] vsize: 421596
Current children cumulated CPU time (s) 96.82
Current children cumulated vsize (Kb) 423720

[startup+110.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127831 0 0 0 10266 415 0 0 25 0 1 0 1797344606 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105468 101961 145 145 0 105323 0
[pid=312] vsize: 421872
Current children cumulated CPU time (s) 106.82
Current children cumulated vsize (Kb) 423996

[startup+120.015 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127890 0 0 0 11264 416 0 0 25 0 1 0 1797344606 432238592 102020 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105527 102020 145 145 0 105382 0
[pid=312] vsize: 422108
Current children cumulated CPU time (s) 116.81
Current children cumulated vsize (Kb) 424232

[startup+130.016 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127936 0 0 0 12264 416 0 0 25 0 1 0 1797344606 432422912 102066 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105572 102066 145 145 0 105427 0
[pid=312] vsize: 422288
Current children cumulated CPU time (s) 126.81
Current children cumulated vsize (Kb) 424412

[startup+140.016 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 127978 0 0 0 13262 417 0 0 25 0 1 0 1797344606 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105598 102108 145 145 0 105453 0
[pid=312] vsize: 422392
Current children cumulated CPU time (s) 136.8
Current children cumulated vsize (Kb) 424516

[startup+150.018 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128007 0 0 0 14261 418 0 0 25 0 1 0 1797344606 432631808 102137 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105623 102137 145 145 0 105478 0
[pid=312] vsize: 422492
Current children cumulated CPU time (s) 146.8
Current children cumulated vsize (Kb) 424616

[startup+160.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128028 0 0 0 15261 418 0 0 25 0 1 0 1797344606 432701440 102158 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105640 102158 145 145 0 105495 0
[pid=312] vsize: 422560
Current children cumulated CPU time (s) 156.8
Current children cumulated vsize (Kb) 424684

[startup+170.021 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128043 0 0 0 16261 418 0 0 25 0 1 0 1797344606 432762880 102173 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105655 102173 145 145 0 105510 0
[pid=312] vsize: 422620
Current children cumulated CPU time (s) 166.8
Current children cumulated vsize (Kb) 424744

[startup+180.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128056 0 0 0 17261 418 0 0 25 0 1 0 1797344606 432812032 102186 4294967295 134512640 135094434 3221224432 3221223120 134554859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105667 102186 145 145 0 105522 0
[pid=312] vsize: 422668
Current children cumulated CPU time (s) 176.8
Current children cumulated vsize (Kb) 424792

[startup+190.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128065 0 0 0 18261 418 0 0 25 0 1 0 1797344606 432848896 102195 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105676 102195 145 145 0 105531 0
[pid=312] vsize: 422704
Current children cumulated CPU time (s) 186.8
Current children cumulated vsize (Kb) 424828

[startup+200.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128081 0 0 0 19261 418 0 0 25 0 1 0 1797344606 432943104 102211 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105699 102211 145 145 0 105554 0
[pid=312] vsize: 422796
Current children cumulated CPU time (s) 196.8
Current children cumulated vsize (Kb) 424920

[startup+210.024 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128081 0 0 0 20261 418 0 0 25 0 1 0 1797344606 432943104 102211 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105699 102211 145 145 0 105554 0
[pid=312] vsize: 422796
Current children cumulated CPU time (s) 206.8
Current children cumulated vsize (Kb) 424920

[startup+220.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128088 0 0 0 21261 418 0 0 25 0 1 0 1797344606 432967680 102218 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105705 102218 145 145 0 105560 0
[pid=312] vsize: 422820
Current children cumulated CPU time (s) 216.8
Current children cumulated vsize (Kb) 424944

[startup+230.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128097 0 0 0 22261 418 0 0 25 0 1 0 1797344606 432988160 102227 4294967295 134512640 135094434 3221224432 3221223044 134562998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105710 102227 145 145 0 105565 0
[pid=312] vsize: 422840
Current children cumulated CPU time (s) 226.8
Current children cumulated vsize (Kb) 424964

[startup+240.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128102 0 0 0 23261 418 0 0 25 0 1 0 1797344606 433008640 102232 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105715 102232 145 145 0 105570 0
[pid=312] vsize: 422860
Current children cumulated CPU time (s) 236.8
Current children cumulated vsize (Kb) 424984

[startup+250.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128110 0 0 0 24261 418 0 0 25 0 1 0 1797344606 433037312 102240 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105722 102240 145 145 0 105577 0
[pid=312] vsize: 422888
Current children cumulated CPU time (s) 246.8
Current children cumulated vsize (Kb) 425012

[startup+260.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128114 0 0 0 25262 418 0 0 25 0 1 0 1797344606 433053696 102244 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105726 102244 145 145 0 105581 0
[pid=312] vsize: 422904
Current children cumulated CPU time (s) 256.81
Current children cumulated vsize (Kb) 425028

[startup+270.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128124 0 0 0 26262 418 0 0 25 0 1 0 1797344606 433074176 102254 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105731 102254 145 145 0 105586 0
[pid=312] vsize: 422924
Current children cumulated CPU time (s) 266.81
Current children cumulated vsize (Kb) 425048

[startup+280.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128130 0 0 0 27262 418 0 0 25 0 1 0 1797344606 433098752 102260 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105737 102260 145 145 0 105592 0
[pid=312] vsize: 422948
Current children cumulated CPU time (s) 276.81
Current children cumulated vsize (Kb) 425072

[startup+290.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128132 0 0 0 28262 418 0 0 25 0 1 0 1797344606 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105739 102262 145 145 0 105594 0
[pid=312] vsize: 422956
Current children cumulated CPU time (s) 286.81
Current children cumulated vsize (Kb) 425080

[startup+300.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128134 0 0 0 29263 418 0 0 25 0 1 0 1797344606 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105741 102264 145 145 0 105596 0
[pid=312] vsize: 422964
Current children cumulated CPU time (s) 296.82
Current children cumulated vsize (Kb) 425088

[startup+310.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128141 0 0 0 30263 418 0 0 25 0 1 0 1797344606 433135616 102271 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105746 102271 145 145 0 105601 0
[pid=312] vsize: 422984
Current children cumulated CPU time (s) 306.82
Current children cumulated vsize (Kb) 425108

[startup+320.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128146 0 0 0 31263 418 0 0 25 0 1 0 1797344606 433147904 102276 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105749 102276 145 145 0 105604 0
[pid=312] vsize: 422996
Current children cumulated CPU time (s) 316.82
Current children cumulated vsize (Kb) 425120

[startup+330.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128150 0 0 0 32263 418 0 0 25 0 1 0 1797344606 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105753 102280 145 145 0 105608 0
[pid=312] vsize: 423012
Current children cumulated CPU time (s) 326.82
Current children cumulated vsize (Kb) 425136

[startup+340.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128153 0 0 0 33263 418 0 0 25 0 1 0 1797344606 433172480 102283 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105755 102283 145 145 0 105610 0
[pid=312] vsize: 423020
Current children cumulated CPU time (s) 336.82
Current children cumulated vsize (Kb) 425144

[startup+350.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128156 0 0 0 34263 418 0 0 25 0 1 0 1797344606 433184768 102286 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105758 102286 145 145 0 105613 0
[pid=312] vsize: 423032
Current children cumulated CPU time (s) 346.82
Current children cumulated vsize (Kb) 425156

[startup+360.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128159 0 0 0 35264 418 0 0 25 0 1 0 1797344606 433197056 102289 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105761 102289 145 145 0 105616 0
[pid=312] vsize: 423044
Current children cumulated CPU time (s) 356.83
Current children cumulated vsize (Kb) 425168

[startup+370.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128167 0 0 0 36264 418 0 0 25 0 1 0 1797344606 433225728 102297 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105768 102297 145 145 0 105623 0
[pid=312] vsize: 423072
Current children cumulated CPU time (s) 366.83
Current children cumulated vsize (Kb) 425196

[startup+380.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128169 0 0 0 37264 418 0 0 25 0 1 0 1797344606 433233920 102299 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105770 102299 145 145 0 105625 0
[pid=312] vsize: 423080
Current children cumulated CPU time (s) 376.83
Current children cumulated vsize (Kb) 425204

[startup+390.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128173 0 0 0 38264 418 0 0 25 0 1 0 1797344606 433238016 102303 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105771 102303 145 145 0 105626 0
[pid=312] vsize: 423084
Current children cumulated CPU time (s) 386.83
Current children cumulated vsize (Kb) 425208

[startup+400.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128175 0 0 0 39264 418 0 0 25 0 1 0 1797344606 433246208 102305 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105773 102305 145 145 0 105628 0
[pid=312] vsize: 423092
Current children cumulated CPU time (s) 396.83
Current children cumulated vsize (Kb) 425216

[startup+410.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128178 0 0 0 40264 419 0 0 25 0 1 0 1797344606 433254400 102308 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105775 102308 145 145 0 105630 0
[pid=312] vsize: 423100
Current children cumulated CPU time (s) 406.84
Current children cumulated vsize (Kb) 425224

[startup+420.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128180 0 0 0 41265 419 0 0 25 0 1 0 1797344606 433262592 102310 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105777 102310 145 145 0 105632 0
[pid=312] vsize: 423108
Current children cumulated CPU time (s) 416.85
Current children cumulated vsize (Kb) 425232

[startup+430.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128183 0 0 0 42265 419 0 0 25 0 1 0 1797344606 433274880 102313 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105780 102313 145 145 0 105635 0
[pid=312] vsize: 423120
Current children cumulated CPU time (s) 426.85
Current children cumulated vsize (Kb) 425244

[startup+440.045 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128187 0 0 0 43265 419 0 0 25 0 1 0 1797344606 433291264 102317 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105784 102317 145 145 0 105639 0
[pid=312] vsize: 423136
Current children cumulated CPU time (s) 436.85
Current children cumulated vsize (Kb) 425260

[startup+450.046 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128193 0 0 0 44265 419 0 0 25 0 1 0 1797344606 433311744 102323 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105789 102323 145 145 0 105644 0
[pid=312] vsize: 423156
Current children cumulated CPU time (s) 446.85
Current children cumulated vsize (Kb) 425280

[startup+460.047 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128215 0 0 0 45266 419 0 0 25 0 1 0 1797344606 433446912 102345 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105822 102345 145 145 0 105677 0
[pid=312] vsize: 423288
Current children cumulated CPU time (s) 456.86
Current children cumulated vsize (Kb) 425412

[startup+470.048 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128217 0 0 0 46265 419 0 0 25 0 1 0 1797344606 433451008 102347 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105823 102347 145 145 0 105678 0
[pid=312] vsize: 423292
Current children cumulated CPU time (s) 466.85
Current children cumulated vsize (Kb) 425416

[startup+480.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128219 0 0 0 47265 419 0 0 25 0 1 0 1797344606 433459200 102349 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105825 102349 145 145 0 105680 0
[pid=312] vsize: 423300
Current children cumulated CPU time (s) 476.85
Current children cumulated vsize (Kb) 425424

[startup+490.051 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128229 0 0 0 48265 420 0 0 25 0 1 0 1797344606 433496064 102359 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105834 102359 145 145 0 105689 0
[pid=312] vsize: 423336
Current children cumulated CPU time (s) 486.86
Current children cumulated vsize (Kb) 425460

[startup+500.053 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128235 0 0 0 49264 420 0 0 25 0 1 0 1797344606 433520640 102365 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105840 102365 145 145 0 105695 0
[pid=312] vsize: 423360
Current children cumulated CPU time (s) 496.85
Current children cumulated vsize (Kb) 425484

[startup+510.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128247 0 0 0 50264 421 0 0 25 0 1 0 1797344606 433565696 102377 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105851 102377 145 145 0 105706 0
[pid=312] vsize: 423404
Current children cumulated CPU time (s) 506.86
Current children cumulated vsize (Kb) 425528

[startup+520.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128254 0 0 0 51263 421 0 0 25 0 1 0 1797344606 433594368 102384 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105858 102384 145 145 0 105713 0
[pid=312] vsize: 423432
Current children cumulated CPU time (s) 516.85
Current children cumulated vsize (Kb) 425556

[startup+530.057 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128263 0 0 0 52263 421 0 0 25 0 1 0 1797344606 433631232 102393 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105867 102393 145 145 0 105722 0
[pid=312] vsize: 423468
Current children cumulated CPU time (s) 526.85
Current children cumulated vsize (Kb) 425592

[startup+540.058 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128322 0 0 0 53262 422 0 0 25 0 1 0 1797344606 433827840 102452 4294967295 134512640 135094434 3221224432 3221223076 134561789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105915 102452 145 145 0 105770 0
[pid=312] vsize: 423660
Current children cumulated CPU time (s) 536.85
Current children cumulated vsize (Kb) 425784

[startup+550.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128324 0 0 0 54261 423 0 0 25 0 1 0 1797344606 433836032 102454 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105917 102454 145 145 0 105772 0
[pid=312] vsize: 423668
Current children cumulated CPU time (s) 546.85
Current children cumulated vsize (Kb) 425792

[startup+560.061 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128328 0 0 0 55261 423 0 0 25 0 1 0 1797344606 433852416 102458 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105921 102458 145 145 0 105776 0
[pid=312] vsize: 423684
Current children cumulated CPU time (s) 556.85
Current children cumulated vsize (Kb) 425808

[startup+570.061 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128334 0 0 0 56261 423 0 0 25 0 1 0 1797344606 433872896 102464 4294967295 134512640 135094434 3221224432 3221223136 134554413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105926 102464 145 145 0 105781 0
[pid=312] vsize: 423704
Current children cumulated CPU time (s) 566.85
Current children cumulated vsize (Kb) 425828

[startup+580.062 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128339 0 0 0 57260 424 0 0 25 0 1 0 1797344606 433893376 102469 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 105931 102469 145 145 0 105786 0
[pid=312] vsize: 423724
Current children cumulated CPU time (s) 576.85
Current children cumulated vsize (Kb) 425848

[startup+590.063 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128347 0 0 0 58260 424 0 0 25 0 1 0 1797344606 433926144 102477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105939 102477 145 145 0 105794 0
[pid=312] vsize: 423756
Current children cumulated CPU time (s) 586.85
Current children cumulated vsize (Kb) 425880

[startup+600.064 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128354 0 0 0 59260 424 0 0 25 0 1 0 1797344606 433950720 102484 4294967295 134512640 135094434 3221224432 3221223056 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105945 102484 145 145 0 105800 0
[pid=312] vsize: 423780
Current children cumulated CPU time (s) 596.85
Current children cumulated vsize (Kb) 425904

[startup+610.064 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128382 0 0 0 60260 424 0 0 25 0 1 0 1797344606 434061312 102512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105972 102512 145 145 0 105827 0
[pid=312] vsize: 423888
Current children cumulated CPU time (s) 606.85
Current children cumulated vsize (Kb) 426012

[startup+620.065 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128389 0 0 0 61260 424 0 0 25 0 1 0 1797344606 434089984 102519 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105979 102519 145 145 0 105834 0
[pid=312] vsize: 423916
Current children cumulated CPU time (s) 616.85
Current children cumulated vsize (Kb) 426040

[startup+630.066 s]
Raw data (loadavg): 1.00 0.99 0.95 3/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128397 0 0 0 62260 424 0 0 25 0 1 0 1797344606 434118656 102527 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105986 102527 145 145 0 105841 0
[pid=312] vsize: 423944
Current children cumulated CPU time (s) 626.85
Current children cumulated vsize (Kb) 426068

[startup+640.067 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128404 0 0 0 63261 424 0 0 25 0 1 0 1797344606 434147328 102534 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 105993 102534 145 145 0 105848 0
[pid=312] vsize: 423972
Current children cumulated CPU time (s) 636.86
Current children cumulated vsize (Kb) 426096

[startup+650.068 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128413 0 0 0 64261 424 0 0 25 0 1 0 1797344606 434184192 102543 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106002 102543 145 145 0 105857 0
[pid=312] vsize: 424008
Current children cumulated CPU time (s) 646.86
Current children cumulated vsize (Kb) 426132

[startup+660.069 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128431 0 0 0 65261 425 0 0 25 0 1 0 1797344606 434253824 102561 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106019 102561 145 145 0 105874 0
[pid=312] vsize: 424076
Current children cumulated CPU time (s) 656.87
Current children cumulated vsize (Kb) 426200

[startup+670.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128465 0 0 0 66260 425 0 0 25 0 1 0 1797344606 434388992 102595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 106052 102595 145 145 0 105907 0
[pid=312] vsize: 424208
Current children cumulated CPU time (s) 666.86
Current children cumulated vsize (Kb) 426332

[startup+680.071 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128505 0 0 0 67259 425 0 0 25 0 1 0 1797344606 434548736 102635 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106091 102635 145 145 0 105946 0
[pid=312] vsize: 424364
Current children cumulated CPU time (s) 676.85
Current children cumulated vsize (Kb) 426488

[startup+690.072 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128512 0 0 0 68259 425 0 0 25 0 1 0 1797344606 434565120 102642 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106095 102642 145 145 0 105950 0
[pid=312] vsize: 424380
Current children cumulated CPU time (s) 686.85
Current children cumulated vsize (Kb) 426504

[startup+700.073 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128517 0 0 0 69259 425 0 0 25 0 1 0 1797344606 434585600 102647 4294967295 134512640 135094434 3221224432 3221223136 134554559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106100 102647 145 145 0 105955 0
[pid=312] vsize: 424400
Current children cumulated CPU time (s) 696.85
Current children cumulated vsize (Kb) 426524

[startup+710.074 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128519 0 0 0 70260 425 0 0 25 0 1 0 1797344606 434593792 102649 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106102 102649 145 145 0 105957 0
[pid=312] vsize: 424408
Current children cumulated CPU time (s) 706.86
Current children cumulated vsize (Kb) 426532

[startup+720.075 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128523 0 0 0 71260 425 0 0 25 0 1 0 1797344606 434601984 102653 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106104 102653 145 145 0 105959 0
[pid=312] vsize: 424416
Current children cumulated CPU time (s) 716.86
Current children cumulated vsize (Kb) 426540

[startup+730.076 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128524 0 0 0 72260 425 0 0 25 0 1 0 1797344606 434606080 102654 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106105 102654 145 145 0 105960 0
[pid=312] vsize: 424420
Current children cumulated CPU time (s) 726.86
Current children cumulated vsize (Kb) 426544

[startup+740.077 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128533 0 0 0 73260 426 0 0 25 0 1 0 1797344606 434642944 102663 4294967295 134512640 135094434 3221224432 3221223056 134563167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106114 102663 145 145 0 105969 0
[pid=312] vsize: 424456
Current children cumulated CPU time (s) 736.87
Current children cumulated vsize (Kb) 426580

[startup+750.078 s]
Raw data (loadavg): 1.00 0.99 0.95 3/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128536 0 0 0 74260 426 0 0 25 0 1 0 1797344606 434655232 102666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106117 102666 145 145 0 105972 0
[pid=312] vsize: 424468
Current children cumulated CPU time (s) 746.87
Current children cumulated vsize (Kb) 426592

[startup+760.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128538 0 0 0 75260 426 0 0 25 0 1 0 1797344606 434663424 102668 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106119 102668 145 145 0 105974 0
[pid=312] vsize: 424476
Current children cumulated CPU time (s) 756.87
Current children cumulated vsize (Kb) 426600

[startup+770.081 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128541 0 0 0 76261 426 0 0 25 0 1 0 1797344606 434671616 102671 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106121 102671 145 145 0 105976 0
[pid=312] vsize: 424484
Current children cumulated CPU time (s) 766.88
Current children cumulated vsize (Kb) 426608

[startup+780.082 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128549 0 0 0 77261 426 0 0 25 0 1 0 1797344606 434704384 102679 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106129 102679 145 145 0 105984 0
[pid=312] vsize: 424516
Current children cumulated CPU time (s) 776.88
Current children cumulated vsize (Kb) 426640

[startup+790.082 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128659 0 0 0 78259 426 0 0 25 0 1 0 1797344606 435146752 102789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106237 102789 145 145 0 106092 0
[pid=312] vsize: 424948
Current children cumulated CPU time (s) 786.86
Current children cumulated vsize (Kb) 427072

[startup+800.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128665 0 0 0 79259 426 0 0 25 0 1 0 1797344606 435171328 102795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106243 102795 145 145 0 106098 0
[pid=312] vsize: 424972
Current children cumulated CPU time (s) 796.86
Current children cumulated vsize (Kb) 427096

[startup+810.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128675 0 0 0 80259 426 0 0 25 0 1 0 1797344606 435212288 102805 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106253 102805 145 145 0 106108 0
[pid=312] vsize: 425012
Current children cumulated CPU time (s) 806.86
Current children cumulated vsize (Kb) 427136

[startup+820.085 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 81259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 816.86
Current children cumulated vsize (Kb) 427428

[startup+830.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 82259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 826.86
Current children cumulated vsize (Kb) 427428

[startup+840.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128717 0 0 0 83259 426 0 0 25 0 1 0 1797344606 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102847 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 836.86
Current children cumulated vsize (Kb) 427428

[startup+850.087 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128718 0 0 0 84260 426 0 0 25 0 1 0 1797344606 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102848 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 846.87
Current children cumulated vsize (Kb) 427428

[startup+860.088 s]
Raw data (loadavg): 1.00 0.99 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128718 0 0 0 85260 426 0 0 25 0 1 0 1797344606 435511296 102848 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102848 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 856.87
Current children cumulated vsize (Kb) 427428

[startup+870.089 s]
Raw data (loadavg): 1.08 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128719 0 0 0 86260 426 0 0 25 0 1 0 1797344606 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102849 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 866.87
Current children cumulated vsize (Kb) 427428

[startup+880.09 s]
Raw data (loadavg): 1.07 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128720 0 0 0 87260 426 0 0 25 0 1 0 1797344606 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106326 102850 145 145 0 106181 0
[pid=312] vsize: 425304
Current children cumulated CPU time (s) 876.87
Current children cumulated vsize (Kb) 427428

[startup+890.09 s]
Raw data (loadavg): 1.06 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128721 0 0 0 88261 426 0 0 25 0 1 0 1797344606 435515392 102851 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106327 102851 145 145 0 106182 0
[pid=312] vsize: 425308
Current children cumulated CPU time (s) 886.88
Current children cumulated vsize (Kb) 427432

[startup+900.091 s]
Raw data (loadavg): 1.05 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128723 0 0 0 89261 426 0 0 25 0 1 0 1797344606 435523584 102853 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106329 102853 145 145 0 106184 0
[pid=312] vsize: 425316
Current children cumulated CPU time (s) 896.88
Current children cumulated vsize (Kb) 427440

[startup+910.092 s]
Raw data (loadavg): 1.04 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128727 0 0 0 90261 426 0 0 25 0 1 0 1797344606 435539968 102857 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106333 102857 145 145 0 106188 0
[pid=312] vsize: 425332
Current children cumulated CPU time (s) 906.88
Current children cumulated vsize (Kb) 427456

[startup+920.093 s]
Raw data (loadavg): 1.03 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128742 0 0 0 91261 426 0 0 25 0 1 0 1797344606 435597312 102872 4294967295 134512640 135094434 3221224432 3221223120 134554821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106347 102872 145 145 0 106202 0
[pid=312] vsize: 425388
Current children cumulated CPU time (s) 916.88
Current children cumulated vsize (Kb) 427512

[startup+930.093 s]
Raw data (loadavg): 1.03 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128770 0 0 0 92261 426 0 0 25 0 1 0 1797344606 435712000 102900 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106375 102900 145 145 0 106230 0
[pid=312] vsize: 425500
Current children cumulated CPU time (s) 926.88
Current children cumulated vsize (Kb) 427624

[startup+940.094 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128787 0 0 0 93261 426 0 0 25 0 1 0 1797344606 435777536 102917 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106391 102917 145 145 0 106246 0
[pid=312] vsize: 425564
Current children cumulated CPU time (s) 936.88
Current children cumulated vsize (Kb) 427688

[startup+950.096 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128829 0 0 0 94260 427 0 0 25 0 1 0 1797344606 435945472 102959 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106432 102959 145 145 0 106287 0
[pid=312] vsize: 425728
Current children cumulated CPU time (s) 946.88
Current children cumulated vsize (Kb) 427852

[startup+960.097 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128853 0 0 0 95260 427 0 0 25 0 1 0 1797344606 436043776 102983 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106456 102983 145 145 0 106311 0
[pid=312] vsize: 425824
Current children cumulated CPU time (s) 956.88
Current children cumulated vsize (Kb) 427948

[startup+970.098 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128871 0 0 0 96260 427 0 0 25 0 1 0 1797344606 436113408 103001 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106473 103001 145 145 0 106328 0
[pid=312] vsize: 425892
Current children cumulated CPU time (s) 966.88
Current children cumulated vsize (Kb) 428016

[startup+980.1 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 128941 0 0 0 97258 428 0 0 25 0 1 0 1797344606 436396032 103071 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/312/statm): 106542 103071 145 145 0 106397 0
[pid=312] vsize: 426168
Current children cumulated CPU time (s) 976.87
Current children cumulated vsize (Kb) 428292

[startup+990.1 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129063 0 0 0 98256 429 0 0 25 0 1 0 1797344606 436883456 103193 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106661 103193 145 145 0 106516 0
[pid=312] vsize: 426644
Current children cumulated CPU time (s) 986.86
Current children cumulated vsize (Kb) 428768

[startup+1000.1 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129083 0 0 0 99256 429 0 0 25 0 1 0 1797344606 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106680 103213 145 145 0 106535 0
[pid=312] vsize: 426720
Current children cumulated CPU time (s) 996.86
Current children cumulated vsize (Kb) 428844

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129088 0 0 0 100256 429 0 0 25 0 1 0 1797344606 436981760 103218 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106685 103218 145 145 0 106540 0
[pid=312] vsize: 426740
Current children cumulated CPU time (s) 1006.86
Current children cumulated vsize (Kb) 428864

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129105 0 0 0 101255 429 0 0 25 0 1 0 1797344606 437051392 103235 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106702 103235 145 145 0 106557 0
[pid=312] vsize: 426808
Current children cumulated CPU time (s) 1016.85
Current children cumulated vsize (Kb) 428932

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129115 0 0 0 102255 429 0 0 25 0 1 0 1797344606 437088256 103245 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106711 103245 145 145 0 106566 0
[pid=312] vsize: 426844
Current children cumulated CPU time (s) 1026.85
Current children cumulated vsize (Kb) 428968

[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129130 0 0 0 103256 429 0 0 25 0 1 0 1797344606 437149696 103260 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106726 103260 145 145 0 106581 0
[pid=312] vsize: 426904
Current children cumulated CPU time (s) 1036.86
Current children cumulated vsize (Kb) 429028

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129168 0 0 0 104255 430 0 0 25 0 1 0 1797344606 437305344 103298 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106764 103298 145 145 0 106619 0
[pid=312] vsize: 427056
Current children cumulated CPU time (s) 1046.86
Current children cumulated vsize (Kb) 429180

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129195 0 0 0 105255 430 0 0 25 0 1 0 1797344606 437411840 103325 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106790 103325 145 145 0 106645 0
[pid=312] vsize: 427160
Current children cumulated CPU time (s) 1056.86
Current children cumulated vsize (Kb) 429284

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129220 0 0 0 106255 430 0 0 25 0 1 0 1797344606 437514240 103350 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106815 103350 145 145 0 106670 0
[pid=312] vsize: 427260
Current children cumulated CPU time (s) 1066.86
Current children cumulated vsize (Kb) 429384

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129235 0 0 0 107255 430 0 0 25 0 1 0 1797344606 437571584 103365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106829 103365 145 145 0 106684 0
[pid=312] vsize: 427316
Current children cumulated CPU time (s) 1076.86
Current children cumulated vsize (Kb) 429440

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129251 0 0 0 108255 430 0 0 25 0 1 0 1797344606 437637120 103381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106845 103381 145 145 0 106700 0
[pid=312] vsize: 427380
Current children cumulated CPU time (s) 1086.86
Current children cumulated vsize (Kb) 429504

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129265 0 0 0 109255 430 0 0 25 0 1 0 1797344606 437694464 103395 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106859 103395 145 145 0 106714 0
[pid=312] vsize: 427436
Current children cumulated CPU time (s) 1096.86
Current children cumulated vsize (Kb) 429560

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129279 0 0 0 110255 430 0 0 25 0 1 0 1797344606 437747712 103409 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106872 103409 145 145 0 106727 0
[pid=312] vsize: 427488
Current children cumulated CPU time (s) 1106.86
Current children cumulated vsize (Kb) 429612

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129299 0 0 0 111255 431 0 0 25 0 1 0 1797344606 437829632 103429 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106892 103429 145 145 0 106747 0
[pid=312] vsize: 427568
Current children cumulated CPU time (s) 1116.87
Current children cumulated vsize (Kb) 429692

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129318 0 0 0 112254 431 0 0 25 0 1 0 1797344606 437907456 103448 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106911 103448 145 145 0 106766 0
[pid=312] vsize: 427644
Current children cumulated CPU time (s) 1126.86
Current children cumulated vsize (Kb) 429768

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129327 0 0 0 113254 431 0 0 25 0 1 0 1797344606 437944320 103457 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106920 103457 145 145 0 106775 0
[pid=312] vsize: 427680
Current children cumulated CPU time (s) 1136.86
Current children cumulated vsize (Kb) 429804

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129337 0 0 0 114254 431 0 0 25 0 1 0 1797344606 437985280 103467 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106930 103467 145 145 0 106785 0
[pid=312] vsize: 427720
Current children cumulated CPU time (s) 1146.86
Current children cumulated vsize (Kb) 429844

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129339 0 0 0 115255 431 0 0 25 0 1 0 1797344606 437993472 103469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106932 103469 145 145 0 106787 0
[pid=312] vsize: 427728
Current children cumulated CPU time (s) 1156.87
Current children cumulated vsize (Kb) 429852

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129343 0 0 0 116255 431 0 0 25 0 1 0 1797344606 438009856 103473 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106936 103473 145 145 0 106791 0
[pid=312] vsize: 427744
Current children cumulated CPU time (s) 1166.87
Current children cumulated vsize (Kb) 429868

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129351 0 0 0 117255 431 0 0 25 0 1 0 1797344606 438042624 103481 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106944 103481 145 145 0 106799 0
[pid=312] vsize: 427776
Current children cumulated CPU time (s) 1176.87
Current children cumulated vsize (Kb) 429900

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129358 0 0 0 118255 431 0 0 25 0 1 0 1797344606 438067200 103488 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106950 103488 145 145 0 106805 0
[pid=312] vsize: 427800
Current children cumulated CPU time (s) 1186.87
Current children cumulated vsize (Kb) 429924

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129374 0 0 0 119255 431 0 0 25 0 1 0 1797344606 438132736 103504 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106966 103504 145 145 0 106821 0
[pid=312] vsize: 427864
Current children cumulated CPU time (s) 1196.87
Current children cumulated vsize (Kb) 429988

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129393 0 0 0 120256 431 0 0 25 0 1 0 1797344606 438210560 103523 4294967295 134512640 135094434 3221224432 3221223100 134562168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106985 103523 145 145 0 106840 0
[pid=312] vsize: 427940
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 430064



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 312
Raw data (/proc/308/stat): 308 (minisat+_script) S 307 308 9854 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797344601 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/308/statm): 531 226 485 147 0 384 0
[pid=308] vsize: 2124
Raw data (/proc/312/stat): 312 (minisat+_64-bit) R 308 308 9854 0 -1 0 129393 0 0 0 120256 431 0 0 25 0 1 0 1797344606 438210560 103523 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/312/statm): 106985 103523 145 145 0 106840 0
[pid=312] vsize: 427940
Current children cumulated CPU time (s) 1206.88
Current children cumulated vsize (Kb) 430064

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

Child status: 10
Real time (s): 1210.51
CPU time (s): 1207.2
CPU user time (s): 1202.66
CPU system time (s): 4.54231
CPU usage (%): 99.7267
Max. virtual memory (cumulated for all children) (Kb): 430064

Verifier Data

ERROR: no interpretation found !