Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ic98.opb
MD5SUM9ca02e5a1540510bce8e96ecb8f82d9c
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 83886080000000
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 783292842349555
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables15501
Total number of constraints14313
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)14177
Number of constraints which are nor clauses,nor cardinality constraints136
Minimum length of a constraint1
Maximum length of a constraint13581

Trace number 5919

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        911956 kB
Buffers:           132 kB
Cached:          92928 kB
SwapCached:        780 kB
Active:          35016 kB
Inactive:        60660 kB
HighTotal:      131008 kB
HighFree:        33992 kB
LowTotal:       903652 kB
LowFree:        877964 kB
SwapTotal:     2097892 kB
SwapFree:      2096552 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5632 kB
Slab:            21284 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:16:47 (client local time) WITH STATUS 0 IN 996.233 SECONDS
stats: 3097 7 996.233 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 27287] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 853 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################################################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   12
c ---[ 855]---> BDD-cost:   13
c ---[ 854]---> BDD-cost:   13
c ---[ 853]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   13
c ---[ 849]---> BDD-cost:   13
c ---[ 848]---> BDD-cost:   13
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   13
c ---[ 845]---> BDD-cost:   12
c ---[ 844]---> BDD-cost:   13
c ---[ 842]---> BDD-cost:   13
c ---[ 841]---> BDD-cost:   13
c ---[ 840]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:   13
c ---[ 838]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   13
c ---[ 835]---> BDD-cost:   12
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   12
c ---[ 830]---> BDD-cost:   12
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:   13
c ---[ 826]---> BDD-cost:   13
c ---[ 825]---> BDD-cost:   12
c ---[ 824]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   13
c ---[ 813]---> BDD-cost:   13
c ---[ 812]---> BDD-cost:   12
c ---[ 810]---> Adder-cost: 2530   maxlim: 1873920   bits: 21/21
c ---[ 808]---> Adder-cost: 954   maxlim: 966656   bits: 20/20
c ---[ 806]---> Adder-cost: 6532   maxlim: 4710400   bits: 23/23
c ---[ 804]---> Adder-cost: 1924   maxlim: 1470464   bits: 21/21
c ---[ 802]---> Adder-cost: 428   maxlim: 339968   bits: 19/19
c ---[ 800]---> Adder-cost: 10296   maxlim: 7658496   bits: 23/23
c ---[ 798]---> Adder-cost: 4976   maxlim: 5065728   bits: 23/23
c ---[ 796]---> Adder-cost: 2746   maxlim: 3383296   bits: 22/22
c ---[ 794]---> Adder-cost: 3164   maxlim: 2670592   bits: 22/22
c ---[ 792]---> Adder-cost: 2142   maxlim: 1794048   bits: 21/21
c ---[ 790]---> Adder-cost: 1618   maxlim: 1335296   bits: 21/21
c ---[ 788]---> Adder-cost: 3844   maxlim: 4069376   bits: 22/22
c ---[ 786]---> Adder-cost: 2790   maxlim: 2551808   bits: 22/22
c ---[ 784]---> Adder-cost: 962   maxlim: 854016   bits: 20/20
c ---[ 782]---> Adder-cost: 1114   maxlim: 930816   bits: 20/20
c ---[ 780]---> Adder-cost: 1356   maxlim: 1298432   bits: 21/21
c ---[ 778]---> Adder-cost: 2260   maxlim: 1982464   bits: 21/21
c ---[ 776]---> Adder-cost: 2598   maxlim: 2123776   bits: 22/22
c ---[ 774]---> Adder-cost: 1746   maxlim: 1540096   bits: 21/21
c ---[ 772]---> Adder-cost: 2930   maxlim: 2441216   bits: 22/22
c ---[ 770]---> Adder-cost: 1820   maxlim: 1594368   bits: 21/21
c ---[ 768]---> Adder-cost: 4014   maxlim: 3783680   bits: 22/22
c ---[ 766]---> Adder-cost: 6654   maxlim: 6837248   bits: 23/23
c ---[ 764]---> Adder-cost: 2044   maxlim: 1741824   bits: 21/21
c ---[ 762]---> Adder-cost: 1242   maxlim: 1152000   bits: 21/21
c ---[ 760]---> Adder-cost: 268   maxlim: 339968   bits: 19/19
c ---[ 758]---> Adder-cost: 1576   maxlim: 2551808   bits: 22/22
c ---[ 756]---> Adder-cost: 2740   maxlim: 2395136   bits: 22/22
c ---[ 754]---> Adder-cost: 2394   maxlim: 2307072   bits: 22/22
c ---[ 752]---> Adder-cost: 5924   maxlim: 5430272   bits: 23/23
c ---[ 750]---> Adder-cost: 4334   maxlim: 4377600   bits: 23/23
c ---[ 748]---> Adder-cost: 942   maxlim: 1334272   bits: 21/21
c ---[ 746]---> Adder-cost: 4304   maxlim: 4227072   bits: 23/23
c ---[ 744]---> Adder-cost: 784   maxlim: 715776   bits: 20/20
c ---[ 742]---> Adder-cost: 4446   maxlim: 4887552   bits: 23/23
c ---[ 740]---> Adder-cost: 3354   maxlim: 3956736   bits: 22/22
c ---[ 738]---> Adder-cost: 802   maxlim: 850944   bits: 20/20
c ---[ 736]---> Adder-cost: 1286   maxlim: 1291264   bits: 21/21
c ---[ 734]---> Adder-cost: 1962   maxlim: 1976320   bits: 21/21
c ---[ 732]---> Adder-c

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/27513/stat): 27513 (minisat+_script) R 27512 27513 2660 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1854745915 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27513/statm): 174 3 169 147 0 27 0
[pid=27513] 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=27514
New process pid=27515
New process pid=27516
execve syscall for /bin/sed executable
One traced child (pid=27515) 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=27516) exited with status: 0
One traced child (pid=27514) exited with status: 0
New process pid=27517
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb

[startup+10.0036 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 338 0 0 0 987 4 0 0 25 0 1 0 1854745920 1798144 324 4294967295 134512640 135094434 3221224432 3221223328 134588031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 439 324 145 145 0 294 0
[pid=27517] vsize: 1756
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 3880

[startup+20.0043 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 476 0 0 0 1985 5 0 0 25 0 1 0 1854745920 2682880 459 4294967295 134512640 135094434 3221224432 3221223300 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 655 459 145 145 0 510 0
[pid=27517] vsize: 2620
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 4744

[startup+30.0041 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 549 0 0 0 2984 5 0 0 25 0 1 0 1854745920 2854912 532 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 697 532 145 145 0 552 0
[pid=27517] vsize: 2788
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 4912

[startup+40.0058 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 577 0 0 0 3983 6 0 0 25 0 1 0 1854745920 2871296 560 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 701 560 145 145 0 556 0
[pid=27517] vsize: 2804
Current children cumulated CPU time (s) 39.91
Current children cumulated vsize (Kb) 4928

[startup+50.0065 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 621 0 0 0 4982 7 0 0 25 0 1 0 1854745920 2965504 604 4294967295 134512640 135094434 3221224432 3221223300 134796021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 724 604 145 145 0 579 0
[pid=27517] vsize: 2896
Current children cumulated CPU time (s) 49.91
Current children cumulated vsize (Kb) 5020

[startup+60.0062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 816 0 0 0 5978 9 0 0 25 0 1 0 1854745920 3710976 725 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 906 725 145 145 0 761 0
[pid=27517] vsize: 3624
Current children cumulated CPU time (s) 59.89
Current children cumulated vsize (Kb) 5748

[startup+70.0069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 823 0 0 0 6976 11 0 0 25 0 1 0 1854745920 3760128 732 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 918 732 145 145 0 773 0
[pid=27517] vsize: 3672
Current children cumulated CPU time (s) 69.89
Current children cumulated vsize (Kb) 5796

[startup+80.0077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1073 0 0 0 7973 13 0 0 25 0 1 0 1854745920 4374528 786 4294967295 134512640 135094434 3221224432 3221223316 134796012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 1068 786 145 145 0 923 0
[pid=27517] vsize: 4272
Current children cumulated CPU time (s) 79.88
Current children cumulated vsize (Kb) 6396

[startup+90.0084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1268 0 0 0 8970 15 0 0 25 0 1 0 1854745920 5083136 849 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 1241 849 145 145 0 1096 0
[pid=27517] vsize: 4964
Current children cumulated CPU time (s) 89.87
Current children cumulated vsize (Kb) 7088

[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1394 0 0 0 9968 16 0 0 25 0 1 0 1854745920 5603328 905 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 1368 905 145 145 0 1223 0
[pid=27517] vsize: 5472
Current children cumulated CPU time (s) 99.86
Current children cumulated vsize (Kb) 7596

[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1459 0 0 0 10966 17 0 0 25 0 1 0 1854745920 5861376 970 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 1431 970 145 145 0 1286 0
[pid=27517] vsize: 5724
Current children cumulated CPU time (s) 109.85
Current children cumulated vsize (Kb) 7848

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1613 0 0 0 11963 19 0 0 25 0 1 0 1854745920 6549504 1124 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 1599 1124 145 145 0 1454 0
[pid=27517] vsize: 6396
Current children cumulated CPU time (s) 119.84
Current children cumulated vsize (Kb) 8520

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) T 27513 27513 2660 0 -1 0 1686 0 0 0 12960 20 0 0 25 0 1 0 1854745920 6823936 1147 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27517/statm): 1666 1147 145 145 0 1521 0
[pid=27517] vsize: 6664
Current children cumulated CPU time (s) 129.82
Current children cumulated vsize (Kb) 8788

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1858 0 0 0 13958 21 0 0 25 0 1 0 1854745920 7430144 1197 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 1814 1197 145 145 0 1669 0
[pid=27517] vsize: 7256
Current children cumulated CPU time (s) 139.81
Current children cumulated vsize (Kb) 9380

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1978 0 0 0 14957 22 0 0 25 0 1 0 1854745920 7942144 1317 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 1939 1317 145 145 0 1794 0
[pid=27517] vsize: 7756
Current children cumulated CPU time (s) 149.81
Current children cumulated vsize (Kb) 9880

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2171 0 0 0 15954 23 0 0 25 0 1 0 1854745920 8667136 1374 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27517/statm): 2116 1374 145 145 0 1971 0
[pid=27517] vsize: 8464
Current children cumulated CPU time (s) 159.79
Current children cumulated vsize (Kb) 10588

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2280 0 0 0 16950 24 0 0 25 0 1 0 1854745920 9035776 1411 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 2206 1411 145 145 0 2061 0
[pid=27517] vsize: 8824
Current children cumulated CPU time (s) 169.76
Current children cumulated vsize (Kb) 10948

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2468 0 0 0 17947 25 0 0 25 0 1 0 1854745920 9654272 1456 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 2357 1456 145 145 0 2212 0
[pid=27517] vsize: 9428
Current children cumulated CPU time (s) 179.74
Current children cumulated vsize (Kb) 11552

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2513 0 0 0 18945 26 0 0 25 0 1 0 1854745920 9961472 1501 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 2432 1501 145 145 0 2287 0
[pid=27517] vsize: 9728
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 11852

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2680 0 0 0 19943 28 0 0 25 0 1 0 1854745920 10514432 1540 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 2567 1540 145 145 0 2422 0
[pid=27517] vsize: 10268
Current children cumulated CPU time (s) 199.73
Current children cumulated vsize (Kb) 12392

[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27517
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27513/statm): 531 226 485 147 0 384 0
[pid=27513] vsize: 2124
Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2841 0 0 0 20940 29 0 0 25 0 1 0 1854745920 11022336 1580 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27517/statm): 2691 1580 145 145 0 2546 0
[pid=27517] vsize: 10764
Current children cumulated CPU time (s) 209.71
Current children cumulated vsize (Kb) 12888
One traced child (pid=27517) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27518
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb

[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 339 0 0 0 934 3 0 0 25 0 1 0 1854766977 1859584 324 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 454 324 162 162 0 292 0
[pid=27518] vsize: 1816
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 3944

[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 480 0 0 0 1931 5 0 0 25 0 1 0 1854766977 2760704 462 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 674 462 162 162 0 512 0
[pid=27518] vsize: 2696
Current children cumulated CPU time (s) 229.65
Current children cumulated vsize (Kb) 4824

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 548 0 0 0 2930 7 0 0 25 0 1 0 1854766977 2932736 530 4294967295 134512640 135167914 3221224448 3221223280 134608445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 716 530 162 162 0 554 0
[pid=27518] vsize: 2864
Current children cumulated CPU time (s) 239.66
Current children cumulated vsize (Kb) 4992

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 572 0 0 0 3928 8 0 0 25 0 1 0 1854766977 2932736 554 4294967295 134512640 135167914 3221224448 3221223268 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 716 554 162 162 0 554 0
[pid=27518] vsize: 2864
Current children cumulated CPU time (s) 249.65
Current children cumulated vsize (Kb) 4992

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 610 0 0 0 4927 9 0 0 25 0 1 0 1854766977 3018752 592 4294967295 134512640 135167914 3221224448 3221223268 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 737 592 162 162 0 575 0
[pid=27518] vsize: 2948
Current children cumulated CPU time (s) 259.65
Current children cumulated vsize (Kb) 5076

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 749 0 0 0 5925 10 0 0 25 0 1 0 1854766977 3538944 731 4294967295 134512640 135167914 3221224448 3221223360 134572026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 864 731 162 162 0 702 0
[pid=27518] vsize: 3456
Current children cumulated CPU time (s) 269.64
Current children cumulated vsize (Kb) 5584

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 1016 0 0 0 6920 13 0 0 25 0 1 0 1854766977 4149248 880 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1013 880 162 162 0 851 0
[pid=27518] vsize: 4052
Current children cumulated CPU time (s) 279.62
Current children cumulated vsize (Kb) 6180

[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 1714 0 0 0 7912 18 0 0 25 0 1 0 1854766977 5042176 1032 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1231 1032 162 162 0 1069 0
[pid=27518] vsize: 4924
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 7052

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 1918 0 0 0 8909 20 0 0 25 0 1 0 1854766977 5861376 1236 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1431 1236 162 162 0 1269 0
[pid=27518] vsize: 5724
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 7852

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2127 0 0 0 9904 23 0 0 25 0 1 0 1854766977 6062080 1285 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1480 1285 162 162 0 1318 0
[pid=27518] vsize: 5920
Current children cumulated CPU time (s) 309.56
Current children cumulated vsize (Kb) 8048

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2332 0 0 0 10901 24 0 0 25 0 1 0 1854766977 6914048 1490 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1688 1490 162 162 0 1526 0
[pid=27518] vsize: 6752
Current children cumulated CPU time (s) 319.54
Current children cumulated vsize (Kb) 8880

[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2448 0 0 0 11899 25 0 0 25 0 1 0 1854766977 6955008 1503 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 1698 1503 162 162 0 1536 0
[pid=27518] vsize: 6792
Current children cumulated CPU time (s) 329.53
Current children cumulated vsize (Kb) 8920

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2665 0 0 0 12895 26 0 0 25 0 1 0 1854766977 7843840 1720 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 1915 1720 162 162 0 1753 0
[pid=27518] vsize: 7660
Current children cumulated CPU time (s) 339.5
Current children cumulated vsize (Kb) 9788

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2828 0 0 0 13891 28 0 0 25 0 1 0 1854766977 8527872 1883 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2082 1883 162 162 0 1920 0
[pid=27518] vsize: 8328
Current children cumulated CPU time (s) 349.48
Current children cumulated vsize (Kb) 10456

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3221 0 0 0 14886 31 0 0 25 0 1 0 1854766977 9027584 2009 4294967295 134512640 135167914 3221224448 3221223284 134860186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2204 2009 162 162 0 2042 0
[pid=27518] vsize: 8816
Current children cumulated CPU time (s) 359.46
Current children cumulated vsize (Kb) 10944

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3366 0 0 0 15884 31 0 0 25 0 1 0 1854766977 9621504 2154 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2349 2154 162 162 0 2187 0
[pid=27518] vsize: 9396
Current children cumulated CPU time (s) 369.44
Current children cumulated vsize (Kb) 11524

[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3644 0 0 0 16880 34 0 0 25 0 1 0 1854766977 10760192 2432 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2627 2432 162 162 0 2465 0
[pid=27518] vsize: 10508
Current children cumulated CPU time (s) 379.43
Current children cumulated vsize (Kb) 12636

[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3837 0 0 0 17876 35 0 0 25 0 1 0 1854766977 11018240 2493 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2690 2493 162 162 0 2528 0
[pid=27518] vsize: 10760
Current children cumulated CPU time (s) 389.4
Current children cumulated vsize (Kb) 12888

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 4092 0 0 0 18871 38 0 0 25 0 1 0 1854766977 11649024 2645 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2844 2645 162 162 0 2682 0
[pid=27518] vsize: 11376
Current children cumulated CPU time (s) 399.38
Current children cumulated vsize (Kb) 13504

[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4244 0 0 0 19867 39 0 0 25 0 1 0 1854766977 12267520 2797 4294967295 134512640 135167914 3221224448 3221223284 134860186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 2995 2797 162 162 0 2833 0
[pid=27518] vsize: 11980
Current children cumulated CPU time (s) 409.35
Current children cumulated vsize (Kb) 14108

[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4263 0 0 0 20865 40 0 0 25 0 1 0 1854766977 12333056 2816 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 3011 2816 162 162 0 2849 0
[pid=27518] vsize: 12044
Current children cumulated CPU time (s) 419.34
Current children cumulated vsize (Kb) 14172

[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4699 0 0 0 21859 43 0 0 25 0 1 0 1854766977 13123584 3009 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 3204 3009 162 162 0 3042 0
[pid=27518] vsize: 12816
Current children cumulated CPU time (s) 429.31
Current children cumulated vsize (Kb) 14944

[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5071 0 0 0 22854 45 0 0 25 0 1 0 1854766977 14118912 3249 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 3447 3249 162 162 0 3285 0
[pid=27518] vsize: 13788
Current children cumulated CPU time (s) 439.28
Current children cumulated vsize (Kb) 15916

[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5193 0 0 0 23850 47 0 0 25 0 1 0 1854766977 14610432 3371 4294967295 134512640 135167914 3221224448 3221223312 134608300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 3567 3371 162 162 0 3405 0
[pid=27518] vsize: 14268
Current children cumulated CPU time (s) 449.26
Current children cumulated vsize (Kb) 16396

[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5195 0 0 0 24847 48 0 0 25 0 1 0 1854766977 14610432 3373 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 3567 3373 162 162 0 3405 0
[pid=27518] vsize: 14268
Current children cumulated CPU time (s) 459.24
Current children cumulated vsize (Kb) 16396

[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5195 0 0 0 25845 49 0 0 25 0 1 0 1854766977 14610432 3373 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 3567 3373 162 162 0 3405 0
[pid=27518] vsize: 14268
Current children cumulated CPU time (s) 469.23
Current children cumulated vsize (Kb) 16396

[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 6444 0 0 0 26833 55 0 0 25 0 1 0 1854766977 16707584 3887 4294967295 134512640 135167914 3221224448 3221223312 134608332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4079 3887 162 162 0 3917 0
[pid=27518] vsize: 16316
Current children cumulated CPU time (s) 479.17
Current children cumulated vsize (Kb) 18444

[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 6545 0 0 0 27831 56 0 0 25 0 1 0 1854766977 17117184 3988 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4179 3988 162 162 0 4017 0
[pid=27518] vsize: 16716
Current children cumulated CPU time (s) 489.16
Current children cumulated vsize (Kb) 18844

[startup+500.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7152 0 0 0 28823 60 0 0 25 0 1 0 1854766977 17616896 4050 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4301 4050 162 162 0 4139 0
[pid=27518] vsize: 17204
Current children cumulated CPU time (s) 499.12
Current children cumulated vsize (Kb) 19332

[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7353 0 0 0 29820 62 0 0 25 0 1 0 1854766977 18440192 4251 4294967295 134512640 135167914 3221224448 3221220460 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4502 4251 162 162 0 4340 0
[pid=27518] vsize: 18008
Current children cumulated CPU time (s) 509.11
Current children cumulated vsize (Kb) 20136

[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7577 0 0 0 30816 64 0 0 25 0 1 0 1854766977 18690048 4313 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4563 4313 162 162 0 4401 0
[pid=27518] vsize: 18252
Current children cumulated CPU time (s) 519.09
Current children cumulated vsize (Kb) 20380

[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7775 0 0 0 31814 65 0 0 25 0 1 0 1854766977 19501056 4511 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4761 4511 162 162 0 4599 0
[pid=27518] vsize: 19044
Current children cumulated CPU time (s) 529.08
Current children cumulated vsize (Kb) 21172

[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7862 0 0 0 32812 66 0 0 25 0 1 0 1854766977 19853312 4598 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 4847 4598 162 162 0 4685 0
[pid=27518] vsize: 19388
Current children cumulated CPU time (s) 539.07
Current children cumulated vsize (Kb) 21516

[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8018 0 0 0 33809 67 0 0 25 0 1 0 1854766977 20484096 4754 4294967295 134512640 135167914 3221224448 3221223312 134608307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 5001 4754 162 162 0 4839 0
[pid=27518] vsize: 20004
Current children cumulated CPU time (s) 549.05
Current children cumulated vsize (Kb) 22132

[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8175 0 0 0 34805 69 0 0 25 0 1 0 1854766977 21143552 4911 4294967295 134512640 135167914 3221224448 3221223284 134860172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 5162 4911 162 162 0 5000 0
[pid=27518] vsize: 20648
Current children cumulated CPU time (s) 559.03
Current children cumulated vsize (Kb) 22776

[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8606 0 0 0 35800 71 0 0 25 0 1 0 1854766977 21790720 5074 4294967295 134512640 135167914 3221224448 3221223284 134860164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 5320 5074 162 162 0 5158 0
[pid=27518] vsize: 21280
Current children cumulated CPU time (s) 569
Current children cumulated vsize (Kb) 23408

[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8705 0 0 0 36797 73 0 0 25 0 1 0 1854766977 22196224 5173 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 5419 5173 162 162 0 5257 0
[pid=27518] vsize: 21676
Current children cumulated CPU time (s) 578.99
Current children cumulated vsize (Kb) 23804

[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8997 0 0 0 37791 75 0 0 25 0 1 0 1854766977 23396352 5465 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 5712 5465 162 162 0 5550 0
[pid=27518] vsize: 22848
Current children cumulated CPU time (s) 588.95
Current children cumulated vsize (Kb) 24976

[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9111 0 0 0 38788 76 0 0 25 0 1 0 1854766977 23416832 5476 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 5717 5476 162 162 0 5555 0
[pid=27518] vsize: 22868
Current children cumulated CPU time (s) 598.93
Current children cumulated vsize (Kb) 24996

[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9413 0 0 0 39782 79 0 0 25 0 1 0 1854766977 24662016 5778 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 6021 5778 162 162 0 5859 0
[pid=27518] vsize: 24084
Current children cumulated CPU time (s) 608.9
Current children cumulated vsize (Kb) 26212

[startup+620.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9436 0 0 0 40781 80 0 0 25 0 1 0 1854766977 24735744 5801 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 6039 5801 162 162 0 5877 0
[pid=27518] vsize: 24156
Current children cumulated CPU time (s) 618.9
Current children cumulated vsize (Kb) 26284

[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9866 0 0 0 41776 83 0 0 25 0 1 0 1854766977 25526272 5988 4294967295 134512640 135167914 3221224448 3221223312 134608296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 6232 5988 162 162 0 6070 0
[pid=27518] vsize: 24928
Current children cumulated CPU time (s) 628.88
Current children cumulated vsize (Kb) 27056

[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10073 0 0 0 42772 84 0 0 25 0 1 0 1854766977 25804800 6063 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 6300 6063 162 162 0 6138 0
[pid=27518] vsize: 25200
Current children cumulated CPU time (s) 638.85
Current children cumulated vsize (Kb) 27328

[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10371 0 0 0 43766 87 0 0 25 0 1 0 1854766977 27033600 6361 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 6600 6361 162 162 0 6438 0
[pid=27518] vsize: 26400
Current children cumulated CPU time (s) 648.82
Current children cumulated vsize (Kb) 28528

[startup+660.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10371 0 0 0 44765 88 0 0 25 0 1 0 1854766977 27033600 6361 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 6600 6361 162 162 0 6438 0
[pid=27518] vsize: 26400
Current children cumulated CPU time (s) 658.82
Current children cumulated vsize (Kb) 28528

[startup+670.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10381 0 0 0 45763 88 0 0 25 0 1 0 1854766977 27090944 6371 4294967295 134512640 135167914 3221224448 3221223296 134608317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 6614 6371 162 162 0 6452 0
[pid=27518] vsize: 26456
Current children cumulated CPU time (s) 668.8
Current children cumulated vsize (Kb) 28584

[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 12623 0 0 0 46748 97 0 0 25 0 1 0 1854766977 34770944 8228 4294967295 134512640 135167914 3221224448 3221080156 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 8489 8228 162 162 0 8327 0
[pid=27518] vsize: 33956
Current children cumulated CPU time (s) 678.74
Current children cumulated vsize (Kb) 36084

[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14649 0 0 0 47737 104 0 0 25 0 1 0 1854766977 41537536 9812 4294967295 134512640 135167914 3221224448 3221223112 134847007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 10141 9812 162 162 0 9979 0
[pid=27518] vsize: 40564
Current children cumulated CPU time (s) 688.7
Current children cumulated vsize (Kb) 42692

[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14649 0 0 0 48737 104 0 0 25 0 1 0 1854766977 41537536 9812 4294967295 134512640 135167914 3221224448 3221221408 134718203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 10141 9812 162 162 0 9979 0
[pid=27518] vsize: 40564
Current children cumulated CPU time (s) 698.7
Current children cumulated vsize (Kb) 42692

[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 49737 104 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221223112 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0
[pid=27518] vsize: 40696
Current children cumulated CPU time (s) 708.7
Current children cumulated vsize (Kb) 42824

[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 50737 105 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221221404 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0
[pid=27518] vsize: 40696
Current children cumulated CPU time (s) 718.71
Current children cumulated vsize (Kb) 42824

[startup+730.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 51737 105 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221221072 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0
[pid=27518] vsize: 40696
Current children cumulated CPU time (s) 728.71
Current children cumulated vsize (Kb) 42824

[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 15002 0 0 0 52734 106 0 0 25 0 1 0 1854766977 45424640 10165 4294967295 134512640 135167914 3221224448 3221223168 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 11090 10165 162 162 0 10928 0
[pid=27518] vsize: 44360
Current children cumulated CPU time (s) 738.69
Current children cumulated vsize (Kb) 46488

[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 19870 0 0 0 53695 124 0 0 25 0 1 0 1854766977 62824448 14413 4294967295 134512640 135167914 3221224448 3219998112 134845149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 15338 14413 162 162 0 15176 0
[pid=27518] vsize: 61352
Current children cumulated CPU time (s) 748.48
Current children cumulated vsize (Kb) 63480

[startup+760.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 24650 0 0 0 54655 143 0 0 25 0 1 0 1854766977 79704064 18534 4294967295 134512640 135167914 3221224448 3219027520 134624395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 19459 18534 162 162 0 19297 0
[pid=27518] vsize: 77836
Current children cumulated CPU time (s) 758.27
Current children cumulated vsize (Kb) 79964

[startup+770.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 30516 0 0 0 55611 166 0 0 25 0 1 0 1854766977 98332672 23082 4294967295 134512640 135167914 3221224448 3218836288 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 24007 23082 162 162 0 23845 0
[pid=27518] vsize: 96028
Current children cumulated CPU time (s) 768.06
Current children cumulated vsize (Kb) 98156

[startup+780.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 34283 0 0 0 56569 184 0 0 25 0 1 0 1854766977 113762304 26849 4294967295 134512640 135167914 3221224448 3220005028 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 27774 26849 162 162 0 27612 0
[pid=27518] vsize: 111096
Current children cumulated CPU time (s) 777.82
Current children cumulated vsize (Kb) 113224

[startup+790.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 42446 0 0 0 57523 211 0 0 25 0 1 0 1854766977 136396800 32375 4294967295 134512640 135167914 3221224448 3219625164 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 33300 32375 162 162 0 33138 0
[pid=27518] vsize: 133200
Current children cumulated CPU time (s) 787.63
Current children cumulated vsize (Kb) 135328

[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 46173 0 0 0 58479 231 0 0 25 0 1 0 1854766977 151662592 36102 4294967295 134512640 135167914 3221224448 3219825136 134625053 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 37027 36102 162 162 0 36865 0
[pid=27518] vsize: 148108
Current children cumulated CPU time (s) 797.39
Current children cumulated vsize (Kb) 150236

[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 49784 0 0 0 59440 246 0 0 25 0 1 0 1854766977 166453248 39713 4294967295 134512640 135167914 3221224448 3219698944 134621141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 40638 39713 162 162 0 40476 0
[pid=27518] vsize: 162552
Current children cumulated CPU time (s) 807.15
Current children cumulated vsize (Kb) 164680

[startup+820.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 53337 0 0 0 60401 262 0 0 25 0 1 0 1854766977 181006336 43266 4294967295 134512640 135167914 3221224448 3219298536 134846958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 44191 43266 162 162 0 44029 0
[pid=27518] vsize: 176764
Current children cumulated CPU time (s) 816.92
Current children cumulated vsize (Kb) 178892

[startup+830.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 56943 0 0 0 61361 281 0 0 25 0 1 0 1854766977 195776512 46872 4294967295 134512640 135167914 3221224448 3219982232 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 47797 46872 162 162 0 47635 0
[pid=27518] vsize: 191188
Current children cumulated CPU time (s) 826.71
Current children cumulated vsize (Kb) 193316

[startup+840.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 69649 0 0 0 62313 316 0 0 25 0 1 0 1854766977 226222080 54305 4294967295 134512640 135167914 3221224448 3219294576 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 55230 54305 162 162 0 55068 0
[pid=27518] vsize: 220920
Current children cumulated CPU time (s) 836.58
Current children cumulated vsize (Kb) 223048

[startup+850.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 73302 0 0 0 63271 333 0 0 25 0 1 0 1854766977 241184768 57958 4294967295 134512640 135167914 3221224448 3219260028 134722576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 58883 57958 162 162 0 58721 0
[pid=27518] vsize: 235532
Current children cumulated CPU time (s) 846.33
Current children cumulated vsize (Kb) 237660

[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 77016 0 0 0 64228 352 0 0 25 0 1 0 1854766977 256397312 61672 4294967295 134512640 135167914 3221224448 3219539848 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 62597 61672 162 162 0 62435 0
[pid=27518] vsize: 250388
Current children cumulated CPU time (s) 856.09
Current children cumulated vsize (Kb) 252516

[startup+870.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 80688 0 0 0 65184 371 0 0 25 0 1 0 1854766977 271437824 65344 4294967295 134512640 135167914 3221224448 3220781944 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 66269 65344 162 162 0 66107 0
[pid=27518] vsize: 265076
Current children cumulated CPU time (s) 865.84
Current children cumulated vsize (Kb) 267204

[startup+880.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 84366 0 0 0 66142 389 0 0 25 0 1 0 1854766977 286502912 69022 4294967295 134512640 135167914 3221224448 3220424832 134845197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 69947 69022 162 162 0 69785 0
[pid=27518] vsize: 279788
Current children cumulated CPU time (s) 875.6
Current children cumulated vsize (Kb) 281916

[startup+890.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 88118 0 0 0 67099 408 0 0 25 0 1 0 1854766977 301871104 72774 4294967295 134512640 135167914 3221224448 3220499036 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 73699 72774 162 162 0 73537 0
[pid=27518] vsize: 294796
Current children cumulated CPU time (s) 885.36
Current children cumulated vsize (Kb) 296924

[startup+900.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 91874 0 0 0 68056 427 0 0 25 0 1 0 1854766977 317255680 76530 4294967295 134512640 135167914 3221224448 3220024928 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 77455 76530 162 162 0 77293 0
[pid=27518] vsize: 309820
Current children cumulated CPU time (s) 895.12
Current children cumulated vsize (Kb) 311948

[startup+910.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 95678 0 0 0 69015 445 0 0 25 0 1 0 1854766977 332836864 80334 4294967295 134512640 135167914 3221224448 3219853568 134845702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 81259 80334 162 162 0 81097 0
[pid=27518] vsize: 325036
Current children cumulated CPU time (s) 904.89
Current children cumulated vsize (Kb) 327164

[startup+920.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 99500 0 0 0 69974 462 0 0 25 0 1 0 1854766977 348491776 84156 4294967295 134512640 135167914 3221224448 3220294016 134844767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 85081 84156 162 162 0 84919 0
[pid=27518] vsize: 340324
Current children cumulated CPU time (s) 914.65
Current children cumulated vsize (Kb) 342452

[startup+930.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 121355 0 0 0 70918 513 0 0 25 0 1 0 1854766977 438009856 106011 4294967295 134512640 135167914 3221224448 3218198992 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 106936 106011 162 162 0 106774 0
[pid=27518] vsize: 427744
Current children cumulated CPU time (s) 924.6
Current children cumulated vsize (Kb) 429872

[startup+940.055 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 125163 0 0 0 71871 536 0 0 25 0 1 0 1854766977 410411008 99273 4294967295 134512640 135167914 3221224448 3218407564 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 100198 99273 162 162 0 100036 0
[pid=27518] vsize: 400792
Current children cumulated CPU time (s) 934.36
Current children cumulated vsize (Kb) 402920

[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 129211 0 0 0 72823 557 0 0 25 0 1 0 1854766977 426995712 103321 4294967295 134512640 135167914 3221224448 3219865660 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 104247 103321 162 162 0 104085 0
[pid=27518] vsize: 416988
Current children cumulated CPU time (s) 944.09
Current children cumulated vsize (Kb) 419116

[startup+960.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 133201 0 0 0 73775 577 0 0 25 0 1 0 1854766977 443334656 107311 4294967295 134512640 135167914 3221224448 3219403996 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 108236 107311 162 162 0 108074 0
[pid=27518] vsize: 432944
Current children cumulated CPU time (s) 953.81
Current children cumulated vsize (Kb) 435072

[startup+970.056 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 137274 0 0 0 74730 596 0 0 25 0 1 0 1854766977 460017664 111384 4294967295 134512640 135167914 3221224448 3218287484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 112309 111384 162 162 0 112147 0
[pid=27518] vsize: 449236
Current children cumulated CPU time (s) 963.55
Current children cumulated vsize (Kb) 451364

[startup+980.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 141391 0 0 0 75682 618 0 0 25 0 1 0 1854766977 476880896 115501 4294967295 134512640 135167914 3221224448 3218208508 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 116426 115501 162 162 0 116264 0
[pid=27518] vsize: 465704
Current children cumulated CPU time (s) 973.29
Current children cumulated vsize (Kb) 467832

[startup+990.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 145475 0 0 0 76634 637 0 0 25 0 1 0 1854766977 493608960 119585 4294967295 134512640 135167914 3221224448 3219558576 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 120510 119585 162 162 0 120348 0
[pid=27518] vsize: 482040
Current children cumulated CPU time (s) 983
Current children cumulated vsize (Kb) 484168

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 149612 0 0 0 77586 657 0 0 25 0 1 0 1854766977 510554112 123722 4294967295 134512640 135167914 3221224448 3218209488 134624410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 124647 123722 162 162 0 124485 0
[pid=27518] vsize: 498588
Current children cumulated CPU time (s) 992.72
Current children cumulated vsize (Kb) 500716

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 153702 0 0 0 78538 676 0 0 25 0 1 0 1854766977 527306752 127812 4294967295 134512640 135167914 3221224448 3218206016 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 128737 127812 162 162 0 128575 0
[pid=27518] vsize: 514948
Current children cumulated CPU time (s) 1002.43
Current children cumulated vsize (Kb) 517076

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 157703 0 0 0 79492 696 0 0 25 0 1 0 1854766977 543694848 131813 4294967295 134512640 135167914 3221224448 3220033360 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 132738 131813 162 162 0 132576 0
[pid=27518] vsize: 530952
Current children cumulated CPU time (s) 1012.17
Current children cumulated vsize (Kb) 533080

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 161824 0 0 0 80446 715 0 0 25 0 1 0 1854766977 560574464 135934 4294967295 134512640 135167914 3221224448 3220218012 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 136859 135934 162 162 0 136697 0
[pid=27518] vsize: 547436
Current children cumulated CPU time (s) 1021.9
Current children cumulated vsize (Kb) 549564

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 165895 0 0 0 81401 733 0 0 25 0 1 0 1854766977 577249280 140005 4294967295 134512640 135167914 3221224448 3218321596 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 140930 140005 162 162 0 140768 0
[pid=27518] vsize: 563720
Current children cumulated CPU time (s) 1031.63
Current children cumulated vsize (Kb) 565848

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 170072 0 0 0 82358 753 0 0 25 0 1 0 1854766977 594358272 144182 4294967295 134512640 135167914 3221224448 3218219484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 145107 144182 162 162 0 144945 0
[pid=27518] vsize: 580428
Current children cumulated CPU time (s) 1041.4
Current children cumulated vsize (Kb) 582556

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 174148 0 0 0 83310 773 0 0 25 0 1 0 1854766977 611053568 148258 4294967295 134512640 135167914 3221224448 3219464924 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 149183 148258 162 162 0 149021 0
[pid=27518] vsize: 596732
Current children cumulated CPU time (s) 1051.12
Current children cumulated vsize (Kb) 598860

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 178245 0 0 0 84264 793 0 0 25 0 1 0 1854766977 627834880 152355 4294967295 134512640 135167914 3221224448 3218192072 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 153280 152355 162 162 0 153118 0
[pid=27518] vsize: 613120
Current children cumulated CPU time (s) 1060.86
Current children cumulated vsize (Kb) 615248

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 182282 0 0 0 85217 812 0 0 25 0 1 0 1854766977 644370432 156392 4294967295 134512640 135167914 3221224448 3218217604 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 157317 156392 162 162 0 157155 0
[pid=27518] vsize: 629268
Current children cumulated CPU time (s) 1070.58
Current children cumulated vsize (Kb) 631396

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 227074 0 0 0 86085 926 0 0 25 0 1 0 1854766977 827838464 201184 4294967295 134512640 135167914 3221224448 3219792976 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 202109 201184 162 162 0 201947 0
[pid=27518] vsize: 808436
Current children cumulated CPU time (s) 1080.4
Current children cumulated vsize (Kb) 810564

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 227074 0 0 0 87085 926 0 0 25 0 1 0 1854766977 827838464 201184 4294967295 134512640 135167914 3221224448 3219792976 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 202109 201184 162 162 0 201947 0
[pid=27518] vsize: 808436
Current children cumulated CPU time (s) 1090.4
Current children cumulated vsize (Kb) 810564

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 230187 0 0 0 88043 944 0 0 25 0 1 0 1854766977 754200576 183206 4294967295 134512640 135167914 3221224448 3219858720 134849440 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 184131 183206 162 162 0 183969 0
[pid=27518] vsize: 736524
Current children cumulated CPU time (s) 1100.16
Current children cumulated vsize (Kb) 738652

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 234467 0 0 0 88993 967 0 0 25 0 1 0 1854766977 771731456 187486 4294967295 134512640 135167914 3221224448 3218278340 134619308 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 188411 187486 162 162 0 188249 0
[pid=27518] vsize: 753644
Current children cumulated CPU time (s) 1109.89
Current children cumulated vsize (Kb) 755772

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 238633 0 0 0 89945 988 0 0 25 0 1 0 1854766977 788795392 191652 4294967295 134512640 135167914 3221224448 3218281976 134849558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 192577 191652 162 162 0 192415 0
[pid=27518] vsize: 770308
Current children cumulated CPU time (s) 1119.62
Current children cumulated vsize (Kb) 772436

[startup+1140.07 s]
Raw data (loadavg): 1.07 0.99 0.93 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 242860 0 0 0 90896 1008 0 0 25 0 1 0 1854766977 806109184 195879 4294967295 134512640 135167914 3221224448 3220208928 134522497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 196804 195879 162 162 0 196642 0
[pid=27518] vsize: 787216
Current children cumulated CPU time (s) 1129.33
Current children cumulated vsize (Kb) 789344

[startup+1150.07 s]
Raw data (loadavg): 1.06 0.99 0.93 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 247070 0 0 0 91847 1030 0 0 25 0 1 0 1854766977 823353344 200089 4294967295 134512640 135167914 3221224448 3218184284 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27518/statm): 201014 200089 162 162 0 200852 0
[pid=27518] vsize: 804056
Current children cumulated CPU time (s) 1139.06
Current children cumulated vsize (Kb) 806184

[startup+1160.07 s]
Raw data (loadavg): 1.05 0.99 0.93 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 251259 0 0 0 92803 1050 0 0 25 0 1 0 1854766977 840511488 204278 4294967295 134512640 135167914 3221224448 3218240284 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 205203 204278 162 162 0 205041 0
[pid=27518] vsize: 820812
Current children cumulated CPU time (s) 1148.82
Current children cumulated vsize (Kb) 822940

[startup+1170.07 s]
Raw data (loadavg): 1.11 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 255495 0 0 0 93754 1071 0 0 25 0 1 0 1854766977 857862144 208514 4294967295 134512640 135167914 3221224448 3218207760 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 209439 208514 162 162 0 209277 0
[pid=27518] vsize: 837756
Current children cumulated CPU time (s) 1158.54
Current children cumulated vsize (Kb) 839884

[startup+1180.07 s]
Raw data (loadavg): 1.10 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 259648 0 0 0 94709 1091 0 0 25 0 1 0 1854766977 874872832 212667 4294967295 134512640 135167914 3221224448 3219732960 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 213592 212667 162 162 0 213430 0
[pid=27518] vsize: 854368
Current children cumulated CPU time (s) 1168.29
Current children cumulated vsize (Kb) 856496

[startup+1190.07 s]
Raw data (loadavg): 1.08 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 263868 0 0 0 95661 1111 0 0 25 0 1 0 1854766977 892157952 216887 4294967295 134512640 135167914 3221224448 3218251744 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 217812 216887 162 162 0 217650 0
[pid=27518] vsize: 871248
Current children cumulated CPU time (s) 1178.01
Current children cumulated vsize (Kb) 873376

[startup+1200.07 s]
Raw data (loadavg): 1.07 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 268022 0 0 0 96612 1132 0 0 25 0 1 0 1854766977 909172736 221041 4294967295 134512640 135167914 3221224448 3218273588 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 221966 221041 162 162 0 221804 0
[pid=27518] vsize: 887864
Current children cumulated CPU time (s) 1187.73
Current children cumulated vsize (Kb) 889992

[startup+1210.07 s]
Raw data (loadavg): 1.06 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 272224 0 0 0 97561 1155 0 0 25 0 1 0 1854766977 926384128 225243 4294967295 134512640 135167914 3221224448 3218270712 134694321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27518/statm): 226168 225243 162 162 0 226006 0
[pid=27518] vsize: 904672
Current children cumulated CPU time (s) 1197.45
Current children cumulated vsize (Kb) 906800

[startup+1220.07 s]
Raw data (loadavg): 1.05 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 277105 0 58 0 98404 1176 0 0 21 0 1 0 1854766977 940875776 224614 4294967295 134512640 135167914 3221224448 3218211488 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 229706 224614 162 162 0 229544 0
[pid=27518] vsize: 918824
Current children cumulated CPU time (s) 1206.09
Current children cumulated vsize (Kb) 920952



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1220.07 s]
Raw data (loadavg): 1.05 1.00 0.94 2/57 27518
Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27513/statm): 532 234 485 147 0 385 0
[pid=27513] vsize: 2128
Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 277105 0 58 0 98404 1176 0 0 21 0 1 0 1854766977 940875776 224614 4294967295 134512640 135167914 3221224448 3218211488 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27518/statm): 229706 224614 162 162 0 229544 0
[pid=27518] vsize: 918824
Current children cumulated CPU time (s) 1206.09
Current children cumulated vsize (Kb) 920952

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

Child status: 0
Real time (s): 1220.5
CPU time (s): 996.233
CPU user time (s): 984.047
CPU system time (s): 12.1851
CPU usage (%): 81.6251
Max. virtual memory (cumulated for all children) (Kb): 920952

Verifier Data

ERROR: no interpretation found !