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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-adlittle.opb
MD5SUMf517bba7737c6a2d32340ac67613cda8
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 1640
Biggest coefficient in the objective function 86769664000
Number of bits for the biggest coefficient in the objective function 37
Sum of the numbers in the objective function 3602973954525
Number of bits of the sum of numbers in the objective function 42
Biggest number in a constraint 351272960000
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 5928173491850
Number of bits of the biggest sum of numbers43
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables1940
Total number of constraints56
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints56
Minimum length of a constraint20
Maximum length of a constraint540

Trace number 5971

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-20 02:29:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3132 boxname=wulflinc5 idbench=788 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f517bba7737c6a2d32340ac67613cda8  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-adlittle.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-adlittle.opb
IDLAUNCH: 3132
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        888408 kB
Buffers:         22360 kB
Cached:          99232 kB
SwapCached:        740 kB
Active:          30624 kB
Inactive:        93668 kB
HighTotal:      131008 kB
HighFree:        32844 kB
LowTotal:       903652 kB
LowFree:        855564 kB
SwapTotal:     2097136 kB
SwapFree:      2095892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            16360 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:50:09 (client local time) WITH STATUS 0 IN 1209.55 SECONDS
stats: 3132 7 1209.55 0

Solver Data



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/24460/stat): 24460 (minisat+_script) R 24459 24460 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796724840 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/24460/statm): 174 3 169 147 0 27 0
[pid=24460] 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=24461
New process pid=24462
New process pid=24463
execve syscall for /bin/sed executable
One traced child (pid=24462) 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=24463) exited with status: 0
One traced child (pid=24461) exited with status: 0
New process pid=24464
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-adlittle.opb

[startup+10.0042 s]
Raw data (loadavg): 0.87 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 537 0 0 0 990 1 0 0 25 0 1 0 1796724845 2048000 405 4294967295 134512640 135094434 3221224432 3221221904 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24464/statm): 500 405 145 145 0 355 0
[pid=24464] vsize: 2000
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 4124

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 1985 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 19.89
Current children cumulated vsize (Kb) 4392

[startup+30.0067 s]
Raw data (loadavg): 0.91 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 2985 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 4392

[startup+40.0074 s]
Raw data (loadavg): 0.92 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 3986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 39.9
Current children cumulated vsize (Kb) 4392

[startup+50.0082 s]
Raw data (loadavg): 0.93 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 4986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221219968 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 4392

[startup+60.0089 s]
Raw data (loadavg): 0.94 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 5986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221219676 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 59.9
Current children cumulated vsize (Kb) 4392

[startup+70.0096 s]
Raw data (loadavg): 0.95 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 6986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 69.9
Current children cumulated vsize (Kb) 4392

[startup+80.0104 s]
Raw data (loadavg): 0.96 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 7986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221219704 134780514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 79.9
Current children cumulated vsize (Kb) 4392

[startup+90.0111 s]
Raw data (loadavg): 0.96 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1220 0 0 0 8986 4 0 0 25 0 1 0 1796724845 2322432 443 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 567 443 145 145 0 422 0
[pid=24464] vsize: 2268
Current children cumulated CPU time (s) 89.9
Current children cumulated vsize (Kb) 4392

[startup+100.011 s]
Raw data (loadavg): 0.97 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1808 0 0 0 9983 6 0 0 25 0 1 0 1796724845 3932160 828 4294967295 134512640 135094434 3221224432 3221221104 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 960 828 145 145 0 815 0
[pid=24464] vsize: 3840
Current children cumulated CPU time (s) 99.89
Current children cumulated vsize (Kb) 5964

[startup+110.013 s]
Raw data (loadavg): 0.97 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 1808 0 0 0 10984 6 0 0 25 0 1 0 1796724845 3932160 828 4294967295 134512640 135094434 3221224432 3221221456 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 960 828 145 145 0 815 0
[pid=24464] vsize: 3840
Current children cumulated CPU time (s) 109.9
Current children cumulated vsize (Kb) 5964

[startup+120.013 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 2010 0 0 0 11983 6 0 0 25 0 1 0 1796724845 3932160 828 4294967295 134512640 135094434 3221224432 3221221104 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 960 828 145 145 0 815 0
[pid=24464] vsize: 3840
Current children cumulated CPU time (s) 119.89
Current children cumulated vsize (Kb) 5964

[startup+130.013 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 2550 0 0 0 12980 8 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221176 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 129.88
Current children cumulated vsize (Kb) 5940

[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.97 1/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) T 24460 24460 824 0 -1 0 7959 0 0 0 13944 26 0 0 24 0 1 0 1796724845 20824064 4952 4294967295 134512640 135094434 3221224432 3221186252 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/24464/statm): 5084 4952 145 145 0 4939 0
[pid=24464] vsize: 20336
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 22460

[startup+150.015 s]
Raw data (loadavg): 0.98 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 14850 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219168 134677313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 149.28
Current children cumulated vsize (Kb) 5940

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 15850 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219488 134518677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 159.28
Current children cumulated vsize (Kb) 5940

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 16850 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219248 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 169.28
Current children cumulated vsize (Kb) 5940

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 17850 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 179.28
Current children cumulated vsize (Kb) 5940

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 18851 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219264 134677138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 189.29
Current children cumulated vsize (Kb) 5940

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 19851 78 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 199.29
Current children cumulated vsize (Kb) 5940

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 20851 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 209.3
Current children cumulated vsize (Kb) 5940

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 21851 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134677323 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 5940

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 22851 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219520 134600151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 5940

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 23851 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134600191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 239.3
Current children cumulated vsize (Kb) 5940

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 24852 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134676522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 249.31
Current children cumulated vsize (Kb) 5940

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 25852 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220036 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 259.31
Current children cumulated vsize (Kb) 5940

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 26852 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 269.31
Current children cumulated vsize (Kb) 5940

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 27852 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 279.31
Current children cumulated vsize (Kb) 5940

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 28853 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 289.32
Current children cumulated vsize (Kb) 5940

[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 29853 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219520 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 299.32
Current children cumulated vsize (Kb) 5940

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 30853 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 309.32
Current children cumulated vsize (Kb) 5940

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 31853 79 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220496 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 319.32
Current children cumulated vsize (Kb) 5940

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 32853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220204 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 329.33
Current children cumulated vsize (Kb) 5940

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 33853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 339.33
Current children cumulated vsize (Kb) 5940

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 34853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220028 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 349.33
Current children cumulated vsize (Kb) 5940

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 35853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219328 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 359.33
Current children cumulated vsize (Kb) 5940

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 36853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219168 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 369.33
Current children cumulated vsize (Kb) 5940

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 37853 80 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 379.33
Current children cumulated vsize (Kb) 5940

[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 38853 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219616 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 389.34
Current children cumulated vsize (Kb) 5940

[startup+400.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 39853 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134600002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 399.34
Current children cumulated vsize (Kb) 5940

[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 40853 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 5940

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 41854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134600295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 419.35
Current children cumulated vsize (Kb) 5940

[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 42854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 429.35
Current children cumulated vsize (Kb) 5940

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 43854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 439.35
Current children cumulated vsize (Kb) 5940

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 44854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219592 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 449.35
Current children cumulated vsize (Kb) 5940

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 45854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134600283 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 459.35
Current children cumulated vsize (Kb) 5940

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 46854 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134677278 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 469.35
Current children cumulated vsize (Kb) 5940

[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 47855 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220216 134600155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 479.36
Current children cumulated vsize (Kb) 5940

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 48855 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 489.36
Current children cumulated vsize (Kb) 5940

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 49855 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 499.36
Current children cumulated vsize (Kb) 5940

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 50855 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220320 134677056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 509.36
Current children cumulated vsize (Kb) 5940

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 51855 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 519.36
Current children cumulated vsize (Kb) 5940

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 52856 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220112 134676336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 529.37
Current children cumulated vsize (Kb) 5940

[startup+540.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 53856 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219852 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 539.37
Current children cumulated vsize (Kb) 5940

[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 54856 81 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220032 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 549.37
Current children cumulated vsize (Kb) 5940

[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 55856 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134676532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 559.38
Current children cumulated vsize (Kb) 5940

[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 56856 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 569.38
Current children cumulated vsize (Kb) 5940

[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 57857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220116 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 579.39
Current children cumulated vsize (Kb) 5940

[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 58857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 589.39
Current children cumulated vsize (Kb) 5940

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 59857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219768 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 599.39
Current children cumulated vsize (Kb) 5940

[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 60857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 609.39
Current children cumulated vsize (Kb) 5940

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 61857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 619.39
Current children cumulated vsize (Kb) 5940

[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 62857 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219520 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 629.39
Current children cumulated vsize (Kb) 5940

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 63858 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 639.4
Current children cumulated vsize (Kb) 5940

[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 64858 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220548 134676992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 649.4
Current children cumulated vsize (Kb) 5940

[startup+660.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 65858 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 659.4
Current children cumulated vsize (Kb) 5940

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 66858 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 5940

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 67858 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 679.4
Current children cumulated vsize (Kb) 5940

[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 68859 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 689.41
Current children cumulated vsize (Kb) 5940

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 69859 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 699.41
Current children cumulated vsize (Kb) 5940

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 70859 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219228 134677378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 709.41
Current children cumulated vsize (Kb) 5940

[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 71859 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 719.41
Current children cumulated vsize (Kb) 5940

[startup+730.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 72860 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 729.42
Current children cumulated vsize (Kb) 5940

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 73860 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219168 134677287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 739.42
Current children cumulated vsize (Kb) 5940

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 74860 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 749.42
Current children cumulated vsize (Kb) 5940

[startup+760.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 75860 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 759.42
Current children cumulated vsize (Kb) 5940

[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 76861 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220544 134676245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 769.43
Current children cumulated vsize (Kb) 5940

[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 77861 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134601029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 779.43
Current children cumulated vsize (Kb) 5940

[startup+790.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 78861 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134600915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 789.43
Current children cumulated vsize (Kb) 5940

[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 79861 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221200 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 799.43
Current children cumulated vsize (Kb) 5940

[startup+810.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 80861 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 809.43
Current children cumulated vsize (Kb) 5940

[startup+820.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 81862 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221104 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 819.44
Current children cumulated vsize (Kb) 5940

[startup+830.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 82862 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221200 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 829.44
Current children cumulated vsize (Kb) 5940

[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 83862 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221176 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 839.44
Current children cumulated vsize (Kb) 5940

[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 84862 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 849.44
Current children cumulated vsize (Kb) 5940

[startup+860.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 85863 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219592 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 859.45
Current children cumulated vsize (Kb) 5940

[startup+870.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 86863 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220204 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 869.45
Current children cumulated vsize (Kb) 5940

[startup+880.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 87863 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 879.45
Current children cumulated vsize (Kb) 5940

[startup+890.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 88863 82 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 889.45
Current children cumulated vsize (Kb) 5940

[startup+900.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 89863 83 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 899.46
Current children cumulated vsize (Kb) 5940

[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 90864 83 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 909.47
Current children cumulated vsize (Kb) 5940

[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 91864 83 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 919.47
Current children cumulated vsize (Kb) 5940

[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 92863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 929.47
Current children cumulated vsize (Kb) 5940

[startup+940.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 93863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219416 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 939.47
Current children cumulated vsize (Kb) 5940

[startup+950.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 94863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 949.47
Current children cumulated vsize (Kb) 5940

[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 95863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134676542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 959.47
Current children cumulated vsize (Kb) 5940

[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 96863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 969.47
Current children cumulated vsize (Kb) 5940

[startup+980.069 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 97863 84 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 979.47
Current children cumulated vsize (Kb) 5940

[startup+990.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 98863 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220560 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 989.48
Current children cumulated vsize (Kb) 5940

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 99864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 999.49
Current children cumulated vsize (Kb) 5940

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 100864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1009.49
Current children cumulated vsize (Kb) 5940

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 101864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220908 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1019.49
Current children cumulated vsize (Kb) 5940

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 102864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1029.49
Current children cumulated vsize (Kb) 5940

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 103864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219588 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1039.49
Current children cumulated vsize (Kb) 5940

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 104864 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220224 134677287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1049.49
Current children cumulated vsize (Kb) 5940

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 105865 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1059.5
Current children cumulated vsize (Kb) 5940

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 106865 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221104 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1069.5
Current children cumulated vsize (Kb) 5940

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 107865 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1079.5
Current children cumulated vsize (Kb) 5940

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 108865 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221280 134677310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1089.5
Current children cumulated vsize (Kb) 5940

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 109865 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1099.5
Current children cumulated vsize (Kb) 5940

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 110866 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220028 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1109.51
Current children cumulated vsize (Kb) 5940

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 111866 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1119.51
Current children cumulated vsize (Kb) 5940

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 112866 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1129.51
Current children cumulated vsize (Kb) 5940

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 113866 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220384 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1139.51
Current children cumulated vsize (Kb) 5940

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 114867 85 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1149.52
Current children cumulated vsize (Kb) 5940

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 115867 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1159.53
Current children cumulated vsize (Kb) 5940

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 116867 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219872 134676586 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1169.53
Current children cumulated vsize (Kb) 5940

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 117867 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1179.53
Current children cumulated vsize (Kb) 5940

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 118867 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219696 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1189.53
Current children cumulated vsize (Kb) 5940

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 119867 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221221280 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1199.53
Current children cumulated vsize (Kb) 5940

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 120868 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1209.54
Current children cumulated vsize (Kb) 5940



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 24464
Raw data (/proc/24460/stat): 24460 (minisat+_script) S 24459 24460 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796724840 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/24460/statm): 531 226 485 147 0 384 0
[pid=24460] vsize: 2124
Raw data (/proc/24464/stat): 24464 (minisat+_64-bit) R 24460 24460 824 0 -1 0 23199 0 0 0 120868 86 0 0 25 0 1 0 1796724845 3907584 822 4294967295 134512640 135094434 3221224432 3221219792 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24464/statm): 954 822 145 145 0 809 0
[pid=24464] vsize: 3816
Current children cumulated CPU time (s) 1209.54
Current children cumulated vsize (Kb) 5940

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.55
CPU user time (s): 1208.68
CPU system time (s): 0.866868
CPU usage (%): 99.9552
Max. virtual memory (cumulated for all children) (Kb): 22460



Verifier Data




ERROR: no interpretation found !