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-stair.opb
MD5SUM07f65f29ee2937de43752221c6dbdf88
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 20
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 1048575
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 516561567744
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 3615347139525
Number of bits of the biggest sum of numbers42
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark158.962
Number of variables7646
Total number of constraints362
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 constraints362
Minimum length of a constraint10
Maximum length of a constraint540

Trace number 6059

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        918396 kB
Buffers:          6132 kB
Cached:          82028 kB
SwapCached:        852 kB
Active:          20936 kB
Inactive:        69852 kB
HighTotal:      131008 kB
HighFree:        45528 kB
LowTotal:       903652 kB
LowFree:        872868 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            19656 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:16:20 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 3207 7 1200.09 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/27106/stat): 27106 (minisat+_script) R 27105 27106 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855132597 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27106/statm): 174 3 169 147 0 27 0
[pid=27106] 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=27107
New process pid=27108
New process pid=27109
execve syscall for /bin/sed executable
One traced child (pid=27108) 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=27109) exited with status: 0
One traced child (pid=27107) exited with status: 0
New process pid=27110
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-stair.opb

[startup+10.0032 s]
Raw data (loadavg): 0.73 0.90 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1329 0 0 0 980 7 0 0 25 0 1 0 1855132602 5627904 1271 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1374 1271 145 145 0 1229 0
[pid=27110] vsize: 5496
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 7620

[startup+20.0038 s]
Raw data (loadavg): 0.77 0.90 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1329 0 0 0 1981 7 0 0 25 0 1 0 1855132602 5627904 1271 4294967295 134512640 135094434 3221224432 3221221436 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1374 1271 145 145 0 1229 0
[pid=27110] vsize: 5496
Current children cumulated CPU time (s) 19.89
Current children cumulated vsize (Kb) 7620

[startup+30.0044 s]
Raw data (loadavg): 0.81 0.90 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1589 0 0 0 2980 8 0 0 25 0 1 0 1855132602 6602752 1489 4294967295 134512640 135094434 3221224432 3221220472 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1612 1489 145 145 0 1467 0
[pid=27110] vsize: 6448
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 8572

[startup+40.005 s]
Raw data (loadavg): 0.84 0.91 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1628 0 0 0 3979 8 0 0 25 0 1 0 1855132602 6705152 1528 4294967295 134512640 135094434 3221224432 3221219168 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1637 1528 145 145 0 1492 0
[pid=27110] vsize: 6548
Current children cumulated CPU time (s) 39.88
Current children cumulated vsize (Kb) 8672

[startup+50.0056 s]
Raw data (loadavg): 0.86 0.91 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1628 0 0 0 4979 8 0 0 25 0 1 0 1855132602 6705152 1528 4294967295 134512640 135094434 3221224432 3221220224 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1637 1528 145 145 0 1492 0
[pid=27110] vsize: 6548
Current children cumulated CPU time (s) 49.88
Current children cumulated vsize (Kb) 8672

[startup+60.0052 s]
Raw data (loadavg): 0.88 0.91 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1628 0 0 0 5979 8 0 0 25 0 1 0 1855132602 6705152 1528 4294967295 134512640 135094434 3221224432 3221221808 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1637 1528 145 145 0 1492 0
[pid=27110] vsize: 6548
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 8672

[startup+70.0059 s]
Raw data (loadavg): 0.90 0.91 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 6980 8 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221219168 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 69.89
Current children cumulated vsize (Kb) 8720

[startup+80.0065 s]
Raw data (loadavg): 0.91 0.92 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 7980 9 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 79.9
Current children cumulated vsize (Kb) 8720

[startup+90.0071 s]
Raw data (loadavg): 0.93 0.92 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 8980 9 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221220560 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 89.9
Current children cumulated vsize (Kb) 8720

[startup+100.008 s]
Raw data (loadavg): 0.94 0.92 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 9980 9 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221221376 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 99.9
Current children cumulated vsize (Kb) 8720

[startup+110.008 s]
Raw data (loadavg): 0.95 0.92 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 10980 9 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 109.9
Current children cumulated vsize (Kb) 8720

[startup+120.009 s]
Raw data (loadavg): 0.95 0.92 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1647 0 0 0 11981 9 0 0 25 0 1 0 1855132602 6754304 1547 4294967295 134512640 135094434 3221224432 3221221792 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1649 1547 145 145 0 1504 0
[pid=27110] vsize: 6596
Current children cumulated CPU time (s) 119.91
Current children cumulated vsize (Kb) 8720

[startup+130.009 s]
Raw data (loadavg): 0.96 0.93 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1707 0 0 0 12981 9 0 0 25 0 1 0 1855132602 7303168 1607 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1783 1607 145 145 0 1638 0
[pid=27110] vsize: 7132
Current children cumulated CPU time (s) 129.91
Current children cumulated vsize (Kb) 9256

[startup+140.01 s]
Raw data (loadavg): 0.97 0.93 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1707 0 0 0 13981 9 0 0 25 0 1 0 1855132602 7303168 1607 4294967295 134512640 135094434 3221224432 3221220748 134600154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1783 1607 145 145 0 1638 0
[pid=27110] vsize: 7132
Current children cumulated CPU time (s) 139.91
Current children cumulated vsize (Kb) 9256

[startup+150.011 s]
Raw data (loadavg): 0.97 0.93 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1707 0 0 0 14981 9 0 0 25 0 1 0 1855132602 7303168 1607 4294967295 134512640 135094434 3221224432 3221221280 134677330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1783 1607 145 145 0 1638 0
[pid=27110] vsize: 7132
Current children cumulated CPU time (s) 149.91
Current children cumulated vsize (Kb) 9256

[startup+160.01 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1709 0 0 0 15981 9 0 0 25 0 1 0 1855132602 7307264 1609 4294967295 134512640 135094434 3221224432 3221218560 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1784 1609 145 145 0 1639 0
[pid=27110] vsize: 7136
Current children cumulated CPU time (s) 159.91
Current children cumulated vsize (Kb) 9260

[startup+170.011 s]
Raw data (loadavg): 0.98 0.93 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1709 0 0 0 16981 9 0 0 25 0 1 0 1855132602 7307264 1609 4294967295 134512640 135094434 3221224432 3221221436 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1784 1609 145 145 0 1639 0
[pid=27110] vsize: 7136
Current children cumulated CPU time (s) 169.91
Current children cumulated vsize (Kb) 9260

[startup+180.011 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1709 0 0 0 17981 9 0 0 25 0 1 0 1855132602 7307264 1609 4294967295 134512640 135094434 3221224432 3221219728 134780529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1784 1609 145 145 0 1639 0
[pid=27110] vsize: 7136
Current children cumulated CPU time (s) 179.91
Current children cumulated vsize (Kb) 9260

[startup+190.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1709 0 0 0 18982 9 0 0 25 0 1 0 1855132602 7307264 1609 4294967295 134512640 135094434 3221224432 3221221352 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1784 1609 145 145 0 1639 0
[pid=27110] vsize: 7136
Current children cumulated CPU time (s) 189.92
Current children cumulated vsize (Kb) 9260

[startup+200.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1824 0 0 0 19981 10 0 0 25 0 1 0 1855132602 7413760 1646 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1810 1646 145 145 0 1665 0
[pid=27110] vsize: 7240
Current children cumulated CPU time (s) 199.92
Current children cumulated vsize (Kb) 9364

[startup+210.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 1824 0 0 0 20981 10 0 0 25 0 1 0 1855132602 7413760 1646 4294967295 134512640 135094434 3221224432 3221220992 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1810 1646 145 145 0 1665 0
[pid=27110] vsize: 7240
Current children cumulated CPU time (s) 209.92
Current children cumulated vsize (Kb) 9364

[startup+220.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2134 0 0 0 21980 11 0 0 25 0 1 0 1855132602 7892992 1783 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1927 1783 145 145 0 1782 0
[pid=27110] vsize: 7708
Current children cumulated CPU time (s) 219.92
Current children cumulated vsize (Kb) 9832

[startup+230.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2134 0 0 0 22980 11 0 0 25 0 1 0 1855132602 7892992 1783 4294967295 134512640 135094434 3221224432 3221219840 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1927 1783 145 145 0 1782 0
[pid=27110] vsize: 7708
Current children cumulated CPU time (s) 229.92
Current children cumulated vsize (Kb) 9832

[startup+240.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2134 0 0 0 23981 11 0 0 25 0 1 0 1855132602 7892992 1783 4294967295 134512640 135094434 3221224432 3221221280 134600225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1927 1783 145 145 0 1782 0
[pid=27110] vsize: 7708
Current children cumulated CPU time (s) 239.93
Current children cumulated vsize (Kb) 9832

[startup+250.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2134 0 0 0 24981 11 0 0 25 0 1 0 1855132602 7892992 1783 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1927 1783 145 145 0 1782 0
[pid=27110] vsize: 7708
Current children cumulated CPU time (s) 249.93
Current children cumulated vsize (Kb) 9832

[startup+260.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2134 0 0 0 25981 11 0 0 25 0 1 0 1855132602 7892992 1783 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1927 1783 145 145 0 1782 0
[pid=27110] vsize: 7708
Current children cumulated CPU time (s) 259.93
Current children cumulated vsize (Kb) 9832

[startup+270.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 26979 12 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 269.92
Current children cumulated vsize (Kb) 9852

[startup+280.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 27979 12 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 279.92
Current children cumulated vsize (Kb) 9852

[startup+290.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 28979 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221220296 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 289.93
Current children cumulated vsize (Kb) 9852

[startup+300.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 29979 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221220752 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 299.93
Current children cumulated vsize (Kb) 9852

[startup+310.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 30979 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221220928 134676471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 309.93
Current children cumulated vsize (Kb) 9852

[startup+320.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 31980 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 319.94
Current children cumulated vsize (Kb) 9852

[startup+330.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 32980 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221221280 134677257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 329.94
Current children cumulated vsize (Kb) 9852

[startup+340.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 33980 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221221864 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 339.94
Current children cumulated vsize (Kb) 9852

[startup+350.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 34980 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221221456 134600274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 349.94
Current children cumulated vsize (Kb) 9852

[startup+360.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2397 0 0 0 35980 13 0 0 25 0 1 0 1855132602 7913472 1793 4294967295 134512640 135094434 3221224432 3221221968 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1932 1793 145 145 0 1787 0
[pid=27110] vsize: 7728
Current children cumulated CPU time (s) 359.94
Current children cumulated vsize (Kb) 9852

[startup+370.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2521 0 0 0 36980 13 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221219696 134677300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 369.94
Current children cumulated vsize (Kb) 9968

[startup+380.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2521 0 0 0 37980 14 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221221280 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 379.95
Current children cumulated vsize (Kb) 9968

[startup+390.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2615 0 0 0 38980 14 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221219968 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 389.95
Current children cumulated vsize (Kb) 9968

[startup+400.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2615 0 0 0 39980 14 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221220672 134677042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 399.95
Current children cumulated vsize (Kb) 9968

[startup+410.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2615 0 0 0 40980 14 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221221456 134600008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 409.95
Current children cumulated vsize (Kb) 9968

[startup+420.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2615 0 0 0 41980 14 0 0 25 0 1 0 1855132602 8032256 1836 4294967295 134512640 135094434 3221224432 3221221528 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1961 1836 145 145 0 1816 0
[pid=27110] vsize: 7844
Current children cumulated CPU time (s) 419.95
Current children cumulated vsize (Kb) 9968

[startup+430.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2729 0 0 0 42980 14 0 0 25 0 1 0 1855132602 8126464 1872 4294967295 134512640 135094434 3221224432 3221220928 134600274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1984 1872 145 145 0 1839 0
[pid=27110] vsize: 7936
Current children cumulated CPU time (s) 429.95
Current children cumulated vsize (Kb) 10060

[startup+440.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2729 0 0 0 43980 15 0 0 25 0 1 0 1855132602 8126464 1872 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1984 1872 145 145 0 1839 0
[pid=27110] vsize: 7936
Current children cumulated CPU time (s) 439.96
Current children cumulated vsize (Kb) 10060

[startup+450.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2729 0 0 0 44981 15 0 0 25 0 1 0 1855132602 8126464 1872 4294967295 134512640 135094434 3221224432 3221221516 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1984 1872 145 145 0 1839 0
[pid=27110] vsize: 7936
Current children cumulated CPU time (s) 449.97
Current children cumulated vsize (Kb) 10060

[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2820 0 0 0 45980 15 0 0 25 0 1 0 1855132602 8155136 1884 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1991 1884 145 145 0 1846 0
[pid=27110] vsize: 7964
Current children cumulated CPU time (s) 459.96
Current children cumulated vsize (Kb) 10088

[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2820 0 0 0 46980 15 0 0 25 0 1 0 1855132602 8155136 1884 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 1991 1884 145 145 0 1846 0
[pid=27110] vsize: 7964
Current children cumulated CPU time (s) 469.96
Current children cumulated vsize (Kb) 10088

[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2869 0 0 0 47980 15 0 0 25 0 1 0 1855132602 8200192 1901 4294967295 134512640 135094434 3221224432 3221218992 134677366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2002 1901 145 145 0 1857 0
[pid=27110] vsize: 8008
Current children cumulated CPU time (s) 479.96
Current children cumulated vsize (Kb) 10132

[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2869 0 0 0 48980 15 0 0 25 0 1 0 1855132602 8200192 1901 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2002 1901 145 145 0 1857 0
[pid=27110] vsize: 8008
Current children cumulated CPU time (s) 489.96
Current children cumulated vsize (Kb) 10132

[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 2869 0 0 0 49981 15 0 0 25 0 1 0 1855132602 8200192 1901 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2002 1901 145 145 0 1857 0
[pid=27110] vsize: 8008
Current children cumulated CPU time (s) 499.97
Current children cumulated vsize (Kb) 10132

[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3020 0 0 0 50980 16 0 0 25 0 1 0 1855132602 9175040 1973 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2240 1973 145 145 0 2095 0
[pid=27110] vsize: 8960
Current children cumulated CPU time (s) 509.97
Current children cumulated vsize (Kb) 11084

[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3020 0 0 0 51980 16 0 0 25 0 1 0 1855132602 9175040 1973 4294967295 134512640 135094434 3221224432 3221220828 134677081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2240 1973 145 145 0 2095 0
[pid=27110] vsize: 8960
Current children cumulated CPU time (s) 519.97
Current children cumulated vsize (Kb) 11084

[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3020 0 0 0 52980 16 0 0 25 0 1 0 1855132602 9175040 1973 4294967295 134512640 135094434 3221224432 3221221552 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2240 1973 145 145 0 2095 0
[pid=27110] vsize: 8960
Current children cumulated CPU time (s) 529.97
Current children cumulated vsize (Kb) 11084

[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3144 0 0 0 53979 17 0 0 25 0 1 0 1855132602 9297920 2019 4294967295 134512640 135094434 3221224432 3221219396 134676608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2270 2019 145 145 0 2125 0
[pid=27110] vsize: 9080
Current children cumulated CPU time (s) 539.97
Current children cumulated vsize (Kb) 11204

[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3144 0 0 0 54979 17 0 0 25 0 1 0 1855132602 9297920 2019 4294967295 134512640 135094434 3221224432 3221220224 134676542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2270 2019 145 145 0 2125 0
[pid=27110] vsize: 9080
Current children cumulated CPU time (s) 549.97
Current children cumulated vsize (Kb) 11204

[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3144 0 0 0 55980 17 0 0 25 0 1 0 1855132602 9297920 2019 4294967295 134512640 135094434 3221224432 3221220672 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2270 2019 145 145 0 2125 0
[pid=27110] vsize: 9080
Current children cumulated CPU time (s) 559.98
Current children cumulated vsize (Kb) 11204

[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3144 0 0 0 56980 17 0 0 25 0 1 0 1855132602 9297920 2019 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2270 2019 145 145 0 2125 0
[pid=27110] vsize: 9080
Current children cumulated CPU time (s) 569.98
Current children cumulated vsize (Kb) 11204

[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3144 0 0 0 57980 17 0 0 25 0 1 0 1855132602 9297920 2019 4294967295 134512640 135094434 3221224432 3221222056 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2270 2019 145 145 0 2125 0
[pid=27110] vsize: 9080
Current children cumulated CPU time (s) 579.98
Current children cumulated vsize (Kb) 11204

[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3192 0 0 0 58980 17 0 0 25 0 1 0 1855132602 9334784 2033 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2279 2033 145 145 0 2134 0
[pid=27110] vsize: 9116
Current children cumulated CPU time (s) 589.98
Current children cumulated vsize (Kb) 11240

[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3192 0 0 0 59980 17 0 0 25 0 1 0 1855132602 9334784 2033 4294967295 134512640 135094434 3221224432 3221220672 134676376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2279 2033 145 145 0 2134 0
[pid=27110] vsize: 9116
Current children cumulated CPU time (s) 599.98
Current children cumulated vsize (Kb) 11240

[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3192 0 0 0 60980 17 0 0 25 0 1 0 1855132602 9334784 2033 4294967295 134512640 135094434 3221224432 3221221168 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2279 2033 145 145 0 2134 0
[pid=27110] vsize: 9116
Current children cumulated CPU time (s) 609.98
Current children cumulated vsize (Kb) 11240

[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 61980 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221218640 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 619.99
Current children cumulated vsize (Kb) 11312

[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 62980 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221219696 134676586 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 629.99
Current children cumulated vsize (Kb) 11312

[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 63980 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 639.99
Current children cumulated vsize (Kb) 11312

[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 64980 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221220224 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 649.99
Current children cumulated vsize (Kb) 11312

[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 65981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 660
Current children cumulated vsize (Kb) 11312

[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 66981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221220208 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 670
Current children cumulated vsize (Kb) 11312

[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 67981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 680
Current children cumulated vsize (Kb) 11312

[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 68981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 690
Current children cumulated vsize (Kb) 11312

[startup+700.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 69981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221376 134676311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 700
Current children cumulated vsize (Kb) 11312

[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 70981 18 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221704 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 710
Current children cumulated vsize (Kb) 11312

[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 71980 19 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221456 134600915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 720
Current children cumulated vsize (Kb) 11312

[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3298 0 0 0 72980 19 0 0 25 0 1 0 1855132602 9408512 2061 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2297 2061 145 145 0 2152 0
[pid=27110] vsize: 9188
Current children cumulated CPU time (s) 730
Current children cumulated vsize (Kb) 11312

[startup+740.043 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3710 0 0 0 73979 20 0 0 25 0 1 0 1855132602 10162176 2266 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2481 2266 145 145 0 2336 0
[pid=27110] vsize: 9924
Current children cumulated CPU time (s) 740
Current children cumulated vsize (Kb) 12048

[startup+750.044 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3806 0 0 0 74979 20 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221219344 134676503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 750
Current children cumulated vsize (Kb) 12120

[startup+760.044 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3806 0 0 0 75979 20 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 760
Current children cumulated vsize (Kb) 12120

[startup+770.045 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3806 0 0 0 76979 20 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221221104 134676542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 770
Current children cumulated vsize (Kb) 12120

[startup+780.046 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3806 0 0 0 77979 20 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221221696 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 780
Current children cumulated vsize (Kb) 12120

[startup+790.046 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3884 0 0 0 78979 21 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221218964 134676380 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 790.01
Current children cumulated vsize (Kb) 12120

[startup+800.047 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3884 0 0 0 79979 21 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221220672 134676251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 800.01
Current children cumulated vsize (Kb) 12120

[startup+810.048 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3884 0 0 0 80979 21 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221221176 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 810.01
Current children cumulated vsize (Kb) 12120

[startup+820.048 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3884 0 0 0 81980 21 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221221456 134677290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 820.02
Current children cumulated vsize (Kb) 12120

[startup+830.049 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3962 0 0 0 82979 22 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221219872 134676532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 830.02
Current children cumulated vsize (Kb) 12120

[startup+840.049 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3962 0 0 0 83979 22 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221220400 134601029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 840.02
Current children cumulated vsize (Kb) 12120

[startup+850.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3962 0 0 0 84980 22 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221220812 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 850.03
Current children cumulated vsize (Kb) 12120

[startup+860.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 3962 0 0 0 85980 22 0 0 25 0 1 0 1855132602 10235904 2284 4294967295 134512640 135094434 3221224432 3221220804 134677232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2499 2284 145 145 0 2354 0
[pid=27110] vsize: 9996
Current children cumulated CPU time (s) 860.03
Current children cumulated vsize (Kb) 12120

[startup+870.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4065 0 0 0 86979 22 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221221104 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 870.02
Current children cumulated vsize (Kb) 12056

[startup+880.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 87978 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 880.02
Current children cumulated vsize (Kb) 12056

[startup+890.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 88978 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220224 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 890.02
Current children cumulated vsize (Kb) 12056

[startup+900.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 89979 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 900.03
Current children cumulated vsize (Kb) 12056

[startup+910.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 90979 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220544 134676245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 910.03
Current children cumulated vsize (Kb) 12056

[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 91979 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221221104 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 920.03
Current children cumulated vsize (Kb) 12056

[startup+930.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 92980 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 930.04
Current children cumulated vsize (Kb) 12056

[startup+940.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 93980 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 940.04
Current children cumulated vsize (Kb) 12056

[startup+950.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4207 0 0 0 94980 23 0 0 25 0 1 0 1855132602 10170368 2277 4294967295 134512640 135094434 3221224432 3221220752 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2483 2277 145 145 0 2338 0
[pid=27110] vsize: 9932
Current children cumulated CPU time (s) 950.04
Current children cumulated vsize (Kb) 12056

[startup+960.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 95979 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221219168 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 960.04
Current children cumulated vsize (Kb) 12088

[startup+970.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 96979 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221219088 134677042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 970.04
Current children cumulated vsize (Kb) 12088

[startup+980.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 97980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220276 134676608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 980.05
Current children cumulated vsize (Kb) 12088

[startup+990.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 98980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 990.05
Current children cumulated vsize (Kb) 12088

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 99980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220400 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1000.05
Current children cumulated vsize (Kb) 12088

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 100980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220016 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1010.05
Current children cumulated vsize (Kb) 12088

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 101980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221219344 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1020.05
Current children cumulated vsize (Kb) 12088

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 102980 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220400 134600175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1030.05
Current children cumulated vsize (Kb) 12088

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 103981 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1040.06
Current children cumulated vsize (Kb) 12088

[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 104981 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220400 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1050.06
Current children cumulated vsize (Kb) 12088

[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 105981 24 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220576 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1060.06
Current children cumulated vsize (Kb) 12088

[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 106981 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1070.07
Current children cumulated vsize (Kb) 12088

[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 107981 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220380 134676240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1080.07
Current children cumulated vsize (Kb) 12088

[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 108981 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220824 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1090.07
Current children cumulated vsize (Kb) 12088

[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 109981 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220784 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1100.07
Current children cumulated vsize (Kb) 12088

[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 110982 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1110.08
Current children cumulated vsize (Kb) 12088

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 111982 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220904 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1120.08
Current children cumulated vsize (Kb) 12088

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 112982 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221221072 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1130.08
Current children cumulated vsize (Kb) 12088

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 113982 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1140.08
Current children cumulated vsize (Kb) 12088

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4332 0 0 0 114982 25 0 0 25 0 1 0 1855132602 10203136 2290 4294967295 134512640 135094434 3221224432 3221221200 134677028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2491 2290 145 145 0 2346 0
[pid=27110] vsize: 9964
Current children cumulated CPU time (s) 1150.08
Current children cumulated vsize (Kb) 12088

[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 115980 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221219168 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1160.08
Current children cumulated vsize (Kb) 12188

[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 116980 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221219872 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1170.08
Current children cumulated vsize (Kb) 12188

[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 117980 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1180.08
Current children cumulated vsize (Kb) 12188

[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 118980 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221220836 134677077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1190.08
Current children cumulated vsize (Kb) 12188

[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 119981 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221221004 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1200.09
Current children cumulated vsize (Kb) 12188



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 27110
Raw data (/proc/27106/stat): 27106 (minisat+_script) S 27105 27106 4419 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855132597 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27106/statm): 531 226 485 147 0 384 0
[pid=27106] vsize: 2124
Raw data (/proc/27110/stat): 27110 (minisat+_64-bit) R 27106 27106 4419 0 -1 0 4629 0 0 0 119981 27 0 0 25 0 1 0 1855132602 10305536 2329 4294967295 134512640 135094434 3221224432 3221221200 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27110/statm): 2516 2329 145 145 0 2371 0
[pid=27110] vsize: 10064
Current children cumulated CPU time (s) 1200.09
Current children cumulated vsize (Kb) 12188

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

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.09
CPU user time (s): 1199.81
CPU system time (s): 0.277957
CPU usage (%): 100.001
Max. virtual memory (cumulated for all children) (Kb): 12188



Verifier Data




ERROR: no interpretation found !