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-israel.opb
MD5SUM326c72a25c8066513471046cf298330a
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -20715832672
Optimality of the best value was proved NO
Number of terms in the objective function 1780
Biggest coefficient in the objective function 788267008000
Number of bits for the biggest coefficient in the objective function 40
Sum of the numbers in the objective function 9669174315900
Number of bits of the sum of numbers in the objective function 44
Biggest number in a constraint 788267008000
Number of bits of the biggest number in a constraint 40
Biggest sum of numbers in a constraint 9669174315900
Number of bits of the biggest sum of numbers44
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.11
Number of variables2840
Total number of constraints174
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 constraints174
Minimum length of a constraint20
Maximum length of a constraint2360

Trace number 6038

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-20 02:48:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3167 boxname=wulflinc18 idbench=823 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  326c72a25c8066513471046cf298330a  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb
IDLAUNCH: 3167
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        859592 kB
Buffers:         23060 kB
Cached:         118952 kB
SwapCached:        856 kB
Active:          33124 kB
Inactive:       111524 kB
HighTotal:      131008 kB
HighFree:        26516 kB
LowTotal:       903652 kB
LowFree:        833076 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            24812 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:08:10 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 3167 7 1200.14 0

Solver Data

c Parsing PB file...
c Converting 174 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssssssssssssssss
c ---[ 193]---> Adder-cost: 1210   maxlim: 14189788   bits: 24/24
c ---[ 191]---> Adder-cost: 349   maxlim: 104839835   bits: 28/27
c ---[ 190]---> Sorter-cost: 3818     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 189]---> Sorter-cost: 3582     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 188]---> Sorter-cost: 3582     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 187]---> Sorter-cost: 3582     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 186]---> Sorter-cost: 3582     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2
c ---[ 185]---> Sorter-cost: 3557     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 3393     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 3393     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2
c ---[ 182]---> Adder-cost: 403   maxlim: 104838683   bits: 28/27
c ---[ 180]---> Adder-cost: 313   maxlim: 104838555   bits: 28/27
c ---[ 179]---> Sorter-cost: 1779     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 178]---> Sorter-cost: 1345     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[ 177]---> Sorter-cost: 1408     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost: 1690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 175]---> Sorter-cost: 1793     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 2477     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 2309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 172]---> Sorter-cost: 2428     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 171]---> Sorter-cost: 2782     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 170]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 169]---> Sorter-cost: 2475     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 2310     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 2373     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 166]---> Sorter-cost: 2284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 165]---> Sorter-cost: 2282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 164]---> Sorter-cost: 2285     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 163]---> Sorter-cost: 2282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 162]---> Sorter-cost: 2283     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 161]---> Sorter-cost: 2282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 160]---> Sorter-cost: 2284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 159]---> Sorter-cost: 4744     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 2284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 157]---> Sorter-cost: 2282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 156]---> Sorter-cost: 2284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3
c ---[ 155]---> Adder-cost: 510   maxlim: 85195112   bits: 27/27
c ---[ 154]---> Adder-cost: 474   maxlim: 45873511   bits: 26/26
c ---[ 153]---> Adder-cost: 478   maxlim: 45873511   bits: 26/26
c ---[ 152]---> Adder-cost: 468   maxlim: 45873510   bits: 26/26
c ---[ 151]---> Adder-cost: 468   maxlim: 45873510   bits: 26/26
c ---[ 150]---> Adder-cost: 468   maxlim: 45873509   bits: 26/26
c ---[ 149]---> Adder-cost: 468   maxlim: 45873509   bits: 26/26
c ---[ 148]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Adder-cost: 468   maxlim: 45873508   bits: 26/26
c ---[ 146]---> Adder-cost: 468   maxlim: 45873508   bits: 26/26
c ---[ 145]---> Adder-cost: 468   maxlim: 45873507   bits: 26/26
c ---[ 144]---> Adder-cost: 460   maxlim: 45873507   bits: 26/26
c ---[ 143]---> Adder-cost: 460   maxlim: 45873506   bits: 26/26
c ---[ 142]---> Sorter-cost: 1285     Base: 2 2

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/27608/stat): 27608 (minisat+_script) R 27607 27608 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855022392 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27608/statm): 174 3 169 147 0 27 0
[pid=27608] 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=27609
New process pid=27610
New process pid=27611
execve syscall for /bin/sed executable
One traced child (pid=27610) 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=27611) exited with status: 0
One traced child (pid=27609) exited with status: 0
New process pid=27612
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-israel.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.98 0.92 1/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) T 27608 27608 31027 0 -1 0 1986 0 0 0 980 8 0 0 25 0 1 0 1855022397 7983104 1629 4294967295 134512640 135094434 3221224432 3221218700 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27612/statm): 1949 1629 145 145 0 1804 0
[pid=27612] vsize: 7796
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 9920

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 2306 0 0 0 1977 9 0 0 25 0 1 0 1855022397 8835072 1949 4294967295 134512640 135094434 3221224432 3221221004 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27612/statm): 2157 1949 145 145 0 2012 0
[pid=27612] vsize: 8628
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 10752

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 2364 0 0 0 2976 10 0 0 25 0 1 0 1855022397 8990720 2007 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 2195 2007 145 145 0 2050 0
[pid=27612] vsize: 8780
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 10904

[startup+40.007 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 3969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218112 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 16136

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 4969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218284 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 49.85
Current children cumulated vsize (Kb) 16136

[startup+60.0079 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 5969 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 16136

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 6970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218912 134676349 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 69.86
Current children cumulated vsize (Kb) 16136

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 7970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 79.86
Current children cumulated vsize (Kb) 16136

[startup+90.0107 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 8970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219048 134677377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 89.86
Current children cumulated vsize (Kb) 16136

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 9970 15 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220100 134677232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 99.86
Current children cumulated vsize (Kb) 16136

[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 10970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219440 134676259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 109.87
Current children cumulated vsize (Kb) 16136

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 11970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219572 134677232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 119.87
Current children cumulated vsize (Kb) 16136

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 12970 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219440 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 129.87
Current children cumulated vsize (Kb) 16136

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 13971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219408 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 139.88
Current children cumulated vsize (Kb) 16136

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 14971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 149.88
Current children cumulated vsize (Kb) 16136

[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 15971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219392 134677233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 159.88
Current children cumulated vsize (Kb) 16136

[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 16971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 169.88
Current children cumulated vsize (Kb) 16136

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 17971 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 179.88
Current children cumulated vsize (Kb) 16136

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 18972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 189.89
Current children cumulated vsize (Kb) 16136

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 19972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 199.89
Current children cumulated vsize (Kb) 16136

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 20972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 209.89
Current children cumulated vsize (Kb) 16136

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 21972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219088 134676273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 219.89
Current children cumulated vsize (Kb) 16136

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 22972 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219232 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 229.89
Current children cumulated vsize (Kb) 16136

[startup+240.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 23973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219680 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 239.9
Current children cumulated vsize (Kb) 16136

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 24973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219792 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 249.9
Current children cumulated vsize (Kb) 16136

[startup+260.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 25973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 259.9
Current children cumulated vsize (Kb) 16136

[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 26973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 269.9
Current children cumulated vsize (Kb) 16136

[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 27973 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218448 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 279.9
Current children cumulated vsize (Kb) 16136

[startup+290.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 28974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219592 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 289.91
Current children cumulated vsize (Kb) 16136

[startup+300.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 29974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220672 134676311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 299.91
Current children cumulated vsize (Kb) 16136

[startup+310.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 30974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 309.91
Current children cumulated vsize (Kb) 16136

[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 31974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 319.91
Current children cumulated vsize (Kb) 16136

[startup+330.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 32974 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219932 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 329.91
Current children cumulated vsize (Kb) 16136

[startup+340.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 33975 16 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219968 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 339.92
Current children cumulated vsize (Kb) 16136

[startup+350.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 34975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 349.93
Current children cumulated vsize (Kb) 16136

[startup+360.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 35975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218884 134677085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 359.93
Current children cumulated vsize (Kb) 16136

[startup+370.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 36975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 369.93
Current children cumulated vsize (Kb) 16136

[startup+380.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 37975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219088 134676321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 379.93
Current children cumulated vsize (Kb) 16136

[startup+390.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 38975 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219728 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 389.93
Current children cumulated vsize (Kb) 16136

[startup+400.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 39976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 399.94
Current children cumulated vsize (Kb) 16136

[startup+410.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 40976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 409.94
Current children cumulated vsize (Kb) 16136

[startup+420.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 41976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 419.94
Current children cumulated vsize (Kb) 16136

[startup+430.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 42976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 429.94
Current children cumulated vsize (Kb) 16136

[startup+440.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 43976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 439.94
Current children cumulated vsize (Kb) 16136

[startup+450.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 44976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220224 134676519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 449.94
Current children cumulated vsize (Kb) 16136

[startup+460.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 45976 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219316 134676992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 459.94
Current children cumulated vsize (Kb) 16136

[startup+470.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 46977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 469.95
Current children cumulated vsize (Kb) 16136

[startup+480.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 47977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219264 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 479.95
Current children cumulated vsize (Kb) 16136

[startup+490.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 48977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218640 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 489.95
Current children cumulated vsize (Kb) 16136

[startup+500.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 49977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 499.95
Current children cumulated vsize (Kb) 16136

[startup+510.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 50977 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134677257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 509.95
Current children cumulated vsize (Kb) 16136

[startup+520.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 51978 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 519.96
Current children cumulated vsize (Kb) 16136

[startup+530.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 52978 17 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 529.96
Current children cumulated vsize (Kb) 16136

[startup+540.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 53978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134677287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 539.97
Current children cumulated vsize (Kb) 16136

[startup+550.045 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 54978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134600904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 549.97
Current children cumulated vsize (Kb) 16136

[startup+560.046 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 55978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 559.97
Current children cumulated vsize (Kb) 16136

[startup+570.047 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 56978 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 569.97
Current children cumulated vsize (Kb) 16136

[startup+580.047 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 57979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 579.98
Current children cumulated vsize (Kb) 16136

[startup+590.049 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 58979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 589.98
Current children cumulated vsize (Kb) 16136

[startup+600.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 59979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134600232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 599.98
Current children cumulated vsize (Kb) 16136

[startup+610.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 60979 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219948 134677081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 609.98
Current children cumulated vsize (Kb) 16136

[startup+620.051 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 61980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219848 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 619.99
Current children cumulated vsize (Kb) 16136

[startup+630.052 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 62980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 629.99
Current children cumulated vsize (Kb) 16136

[startup+640.053 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 63980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219320 134676241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 639.99
Current children cumulated vsize (Kb) 16136

[startup+650.054 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 64980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218700 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 649.99
Current children cumulated vsize (Kb) 16136

[startup+660.054 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 65980 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 659.99
Current children cumulated vsize (Kb) 16136

[startup+670.055 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 66981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 670
Current children cumulated vsize (Kb) 16136

[startup+680.056 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 67981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 680
Current children cumulated vsize (Kb) 16136

[startup+690.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 68981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 690
Current children cumulated vsize (Kb) 16136

[startup+700.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 69981 18 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219580 134677378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 700
Current children cumulated vsize (Kb) 16136

[startup+710.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 70981 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 710.01
Current children cumulated vsize (Kb) 16136

[startup+720.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 71981 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 720.01
Current children cumulated vsize (Kb) 16136

[startup+730.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 72982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134600295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 730.02
Current children cumulated vsize (Kb) 16136

[startup+740.062 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 73982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134676595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 740.02
Current children cumulated vsize (Kb) 16136

[startup+750.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 74982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220300 134676331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 750.02
Current children cumulated vsize (Kb) 16136

[startup+760.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 75982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 760.02
Current children cumulated vsize (Kb) 16136

[startup+770.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 76982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 770.02
Current children cumulated vsize (Kb) 16136

[startup+780.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 77982 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 780.02
Current children cumulated vsize (Kb) 16136

[startup+790.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 78983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 790.03
Current children cumulated vsize (Kb) 16136

[startup+800.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 79983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 800.03
Current children cumulated vsize (Kb) 16136

[startup+810.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 80983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 810.03
Current children cumulated vsize (Kb) 16136

[startup+820.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 81983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 820.03
Current children cumulated vsize (Kb) 16136

[startup+830.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 82983 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134676545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 830.03
Current children cumulated vsize (Kb) 16136

[startup+840.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 83984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 840.04
Current children cumulated vsize (Kb) 16136

[startup+850.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 84984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 850.04
Current children cumulated vsize (Kb) 16136

[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 85984 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220112 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 860.04
Current children cumulated vsize (Kb) 16136

[startup+870.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 86985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 870.05
Current children cumulated vsize (Kb) 16136

[startup+880.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 87985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 880.05
Current children cumulated vsize (Kb) 16136

[startup+890.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 88985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219312 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 890.05
Current children cumulated vsize (Kb) 16136

[startup+900.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 89985 19 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219500 134676382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 900.05
Current children cumulated vsize (Kb) 16136

[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 90985 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218640 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 910.06
Current children cumulated vsize (Kb) 16136

[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 91985 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 920.06
Current children cumulated vsize (Kb) 16136

[startup+930.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 92986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220104 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 930.07
Current children cumulated vsize (Kb) 16136

[startup+940.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 93986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219684 134600238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 940.07
Current children cumulated vsize (Kb) 16136

[startup+950.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 94986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 950.07
Current children cumulated vsize (Kb) 16136

[startup+960.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 95986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219328 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 960.07
Current children cumulated vsize (Kb) 16136

[startup+970.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 96986 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 970.07
Current children cumulated vsize (Kb) 16136

[startup+980.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 97987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220400 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 980.08
Current children cumulated vsize (Kb) 16136

[startup+990.088 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 98987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219840 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 990.08
Current children cumulated vsize (Kb) 16136

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 99987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219168 134677354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1000.08
Current children cumulated vsize (Kb) 16136

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 100987 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1010.08
Current children cumulated vsize (Kb) 16136

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 101988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220496 134676999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1020.09
Current children cumulated vsize (Kb) 16136

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 102988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1030.09
Current children cumulated vsize (Kb) 16136

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 103988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1040.09
Current children cumulated vsize (Kb) 16136

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 104988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1050.09
Current children cumulated vsize (Kb) 16136

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 105988 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220372 134676244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1060.09
Current children cumulated vsize (Kb) 16136

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 106989 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1070.1
Current children cumulated vsize (Kb) 16136

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 107989 20 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219848 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1080.1
Current children cumulated vsize (Kb) 16136

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 108989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1090.11
Current children cumulated vsize (Kb) 16136

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 109989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1100.11
Current children cumulated vsize (Kb) 16136

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 110989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1110.11
Current children cumulated vsize (Kb) 16136

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 111989 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220112 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1120.11
Current children cumulated vsize (Kb) 16136

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 112990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220496 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1130.12
Current children cumulated vsize (Kb) 16136

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 113990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1140.12
Current children cumulated vsize (Kb) 16136

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 114990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220928 134676542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1150.12
Current children cumulated vsize (Kb) 16136

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 115990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221218976 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1160.12
Current children cumulated vsize (Kb) 16136

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 116990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134600310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1170.12
Current children cumulated vsize (Kb) 16136

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 117990 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1180.12
Current children cumulated vsize (Kb) 16136

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 118991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1190.13
Current children cumulated vsize (Kb) 16136

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 119991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219840 134676245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1200.13
Current children cumulated vsize (Kb) 16136



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 27612
Raw data (/proc/27608/stat): 27608 (minisat+_script) S 27607 27608 31027 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855022392 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27608/statm): 531 226 485 147 0 384 0
[pid=27608] vsize: 2124
Raw data (/proc/27612/stat): 27612 (minisat+_64-bit) R 27608 27608 31027 0 -1 0 4058 0 0 0 119991 21 0 0 25 0 1 0 1855022397 14348288 3049 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27612/statm): 3503 3049 145 145 0 3358 0
[pid=27612] vsize: 14012
Current children cumulated CPU time (s) 1200.13
Current children cumulated vsize (Kb) 16136

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.14
CPU user time (s): 1199.91
CPU system time (s): 0.224965
CPU usage (%): 100.002
Max. virtual memory (cumulated for all children) (Kb): 16136

Verifier Data

ERROR: no interpretation found !