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-glass4.opb
MD5SUM5c79ed79e417ba1b9a49f75d042f5e94
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 8257573732279
Optimality of the best value was proved NO
Number of terms in the objective function 478
Biggest coefficient in the objective function 536870912000000
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 1073761158741413
Number of bits of the sum of numbers in the objective function 50
Biggest number in a constraint 71583145981965762560
Number of bits of the biggest number in a constraint 66
Biggest sum of numbers in a constraint 303620978593259257856
Number of bits of the biggest sum of numbers69
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1255.19
Number of variables780
Total number of constraints707
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)338
Number of constraints which are nor clauses,nor cardinality constraints369
Minimum length of a constraint1
Maximum length of a constraint101

Trace number 5916

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 02:07:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3107 boxname=wulflinc22 idbench=763 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5c79ed79e417ba1b9a49f75d042f5e94  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb
IDLAUNCH: 3107
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        889804 kB
Buffers:          8104 kB
Cached:         109808 kB
SwapCached:        476 kB
Active:          15576 kB
Inactive:       104800 kB
HighTotal:      131008 kB
HighFree:        21392 kB
LowTotal:       903652 kB
LowFree:        868412 kB
SwapTotal:     2097892 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18748 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:14:44 (client local time) WITH STATUS 0 IN 400.002 SECONDS
stats: 3107 7 400.002 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 326] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/15025/stat): 15025 (minisat+_script) R 15024 15025 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854814891 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/15025/statm): 174 3 169 147 0 27 0
[pid=15025] 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=15026
New process pid=15027
New process pid=15028
execve syscall for /bin/sed executable
One traced child (pid=15027) 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=15028) exited with status: 0
One traced child (pid=15026) exited with status: 0
New process pid=15029
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb
One traced child (pid=15029) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=15030
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-glass4.opb

[startup+10.0041 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 5174 0 0 0 946 21 0 0 25 0 1 0 1854814897 19070976 4540 4294967295 134512640 135167914 3221224448 3221200860 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 4656 4540 162 162 0 4494 0
[pid=15030] vsize: 18624
Current children cumulated CPU time (s) 9.69
Current children cumulated vsize (Kb) 20752

[startup+20.0048 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 13911 0 0 0 1883 54 0 0 25 0 1 0 1854814897 52158464 12618 4294967295 134512640 135167914 3221224448 3221200560 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 12734 12618 162 162 0 12572 0
[pid=15030] vsize: 50936
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 53064

[startup+30.0055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 18547 0 0 0 2832 75 0 0 25 0 1 0 1854814897 65748992 15936 4294967295 134512640 135167914 3221224448 3221201712 134522355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 16052 15936 162 162 0 15890 0
[pid=15030] vsize: 64208
Current children cumulated CPU time (s) 29.09
Current children cumulated vsize (Kb) 66336

[startup+40.0062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 27773 0 0 0 3778 105 0 0 25 0 1 0 1854814897 92737536 22525 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 22641 22525 162 162 0 22479 0
[pid=15030] vsize: 90564
Current children cumulated CPU time (s) 38.85
Current children cumulated vsize (Kb) 92692

[startup+50.0069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 32445 0 0 0 4727 126 0 0 25 0 1 0 1854814897 111874048 27197 4294967295 134512640 135167914 3221224448 3221204268 134847144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 27313 27197 162 162 0 27151 0
[pid=15030] vsize: 109252
Current children cumulated CPU time (s) 48.55
Current children cumulated vsize (Kb) 111380

[startup+60.0076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 37233 0 0 0 5675 147 0 0 25 0 1 0 1854814897 131485696 31985 4294967295 134512640 135167914 3221224448 3221200800 134691325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 32101 31985 162 162 0 31939 0
[pid=15030] vsize: 128404
Current children cumulated CPU time (s) 58.24
Current children cumulated vsize (Kb) 130532

[startup+70.0083 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 42085 0 0 0 6621 171 0 0 25 0 1 0 1854814897 151359488 36837 4294967295 134512640 135167914 3221224448 3221200756 134622688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 36953 36837 162 162 0 36791 0
[pid=15030] vsize: 147812
Current children cumulated CPU time (s) 67.94
Current children cumulated vsize (Kb) 149940

[startup+80.0091 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 55622 0 0 0 7562 209 0 0 25 0 1 0 1854814897 185208832 45101 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 45217 45101 162 162 0 45055 0
[pid=15030] vsize: 180868
Current children cumulated CPU time (s) 77.73
Current children cumulated vsize (Kb) 182996

[startup+90.0098 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 60790 0 0 0 8507 235 0 0 25 0 1 0 1854814897 206376960 50269 4294967295 134512640 135167914 3221224448 3221202416 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 50385 50269 162 162 0 50223 0
[pid=15030] vsize: 201540
Current children cumulated CPU time (s) 87.44
Current children cumulated vsize (Kb) 203668

[startup+100.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 65640 0 0 0 9452 258 0 0 25 0 1 0 1854814897 226242560 55119 4294967295 134512640 135167914 3221224448 3221200548 134624735 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 55235 55119 162 162 0 55073 0
[pid=15030] vsize: 220940
Current children cumulated CPU time (s) 97.12
Current children cumulated vsize (Kb) 223068

[startup+110.011 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 70484 0 0 0 10397 282 0 0 25 0 1 0 1854814897 246083584 59963 4294967295 134512640 135167914 3221224448 3221201020 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 60079 59963 162 162 0 59917 0
[pid=15030] vsize: 240316
Current children cumulated CPU time (s) 106.81
Current children cumulated vsize (Kb) 242444

[startup+120.012 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 75352 0 0 0 11345 307 0 0 25 0 1 0 1854814897 266027008 64831 4294967295 134512640 135167914 3221224448 3221200668 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 64948 64831 162 162 0 64786 0
[pid=15030] vsize: 259792
Current children cumulated CPU time (s) 116.54
Current children cumulated vsize (Kb) 261920

[startup+130.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 80154 0 0 0 12293 329 0 0 25 0 1 0 1854814897 285691904 69633 4294967295 134512640 135167914 3221224448 3221201696 134695961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 69749 69633 162 162 0 69587 0
[pid=15030] vsize: 278996
Current children cumulated CPU time (s) 126.24
Current children cumulated vsize (Kb) 281124

[startup+140.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 84957 0 0 0 13242 348 0 0 25 0 1 0 1854814897 305364992 74436 4294967295 134512640 135167914 3221224448 3221200512 134694389 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 74552 74436 162 162 0 74390 0
[pid=15030] vsize: 298208
Current children cumulated CPU time (s) 135.92
Current children cumulated vsize (Kb) 300336

[startup+150.015 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 106880 0 0 0 14183 401 0 0 25 0 1 0 1854814897 351965184 85813 4294967295 134512640 135167914 3221224448 3221200956 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 85929 85813 162 162 0 85767 0
[pid=15030] vsize: 343716
Current children cumulated CPU time (s) 145.86
Current children cumulated vsize (Kb) 345844

[startup+160.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 112079 0 0 0 15125 427 0 0 25 0 1 0 1854814897 373260288 91012 4294967295 134512640 135167914 3221224448 3221200992 134844700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 91128 91012 162 162 0 90966 0
[pid=15030] vsize: 364512
Current children cumulated CPU time (s) 155.54
Current children cumulated vsize (Kb) 366640

[startup+170.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 117137 0 0 0 16066 453 0 0 25 0 1 0 1854814897 393977856 96070 4294967295 134512640 135167914 3221224448 3221201072 134693563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 96186 96070 162 162 0 96024 0
[pid=15030] vsize: 384744
Current children cumulated CPU time (s) 165.21
Current children cumulated vsize (Kb) 386872

[startup+180.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 122158 0 0 0 17011 476 0 0 25 0 1 0 1854814897 414543872 101091 4294967295 134512640 135167914 3221224448 3221201664 134845930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 101207 101091 162 162 0 101045 0
[pid=15030] vsize: 404828
Current children cumulated CPU time (s) 174.89
Current children cumulated vsize (Kb) 406956

[startup+190.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 127173 0 0 0 17957 499 0 0 25 0 1 0 1854814897 435085312 106106 4294967295 134512640 135167914 3221224448 3221201952 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 106222 106106 162 162 0 106060 0
[pid=15030] vsize: 424888
Current children cumulated CPU time (s) 184.58
Current children cumulated vsize (Kb) 427016

[startup+200.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 132202 0 0 0 18904 523 0 0 25 0 1 0 1854814897 455684096 111135 4294967295 134512640 135167914 3221224448 3221200832 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 111251 111135 162 162 0 111089 0
[pid=15030] vsize: 445004
Current children cumulated CPU time (s) 194.29
Current children cumulated vsize (Kb) 447132

[startup+210.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 137140 0 0 0 19850 545 0 0 25 0 1 0 1854814897 475910144 116073 4294967295 134512640 135167914 3221224448 3221200552 134693665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 116189 116073 162 162 0 116027 0
[pid=15030] vsize: 464756
Current children cumulated CPU time (s) 203.97
Current children cumulated vsize (Kb) 466884

[startup+220.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 142078 0 0 0 20792 569 0 0 25 0 1 0 1854814897 496136192 121011 4294967295 134512640 135167914 3221224448 3221200348 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 121127 121011 162 162 0 120965 0
[pid=15030] vsize: 484508
Current children cumulated CPU time (s) 213.63
Current children cumulated vsize (Kb) 486636

[startup+230.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 146811 0 0 0 21738 592 0 0 25 0 1 0 1854814897 515522560 125744 4294967295 134512640 135167914 3221224448 3221201824 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 125860 125744 162 162 0 125698 0
[pid=15030] vsize: 503440
Current children cumulated CPU time (s) 223.32
Current children cumulated vsize (Kb) 505568

[startup+240.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 151811 0 0 0 22683 615 0 0 25 0 1 0 1854814897 536002560 130744 4294967295 134512640 135167914 3221224448 3221201888 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 130860 130744 162 162 0 130698 0
[pid=15030] vsize: 523440
Current children cumulated CPU time (s) 233
Current children cumulated vsize (Kb) 525568

[startup+250.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 156610 0 0 0 23632 635 0 0 25 0 1 0 1854814897 555659264 135543 4294967295 134512640 135167914 3221224448 3221200768 134843015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 135659 135543 162 162 0 135497 0
[pid=15030] vsize: 542636
Current children cumulated CPU time (s) 242.69
Current children cumulated vsize (Kb) 544764

[startup+260.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 161313 0 0 0 24577 658 0 0 25 0 1 0 1854814897 574922752 140246 4294967295 134512640 135167914 3221224448 3221200828 134722218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 140362 140246 162 162 0 140200 0
[pid=15030] vsize: 561448
Current children cumulated CPU time (s) 252.37
Current children cumulated vsize (Kb) 563576

[startup+270.022 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 166041 0 0 0 25524 679 0 0 25 0 1 0 1854814897 594288640 144974 4294967295 134512640 135167914 3221224448 3221200700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 145090 144974 162 162 0 144928 0
[pid=15030] vsize: 580360
Current children cumulated CPU time (s) 262.05
Current children cumulated vsize (Kb) 582488

[startup+280.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 212239 0 0 0 26384 793 0 0 25 0 1 0 1854814897 783515648 191172 4294967295 134512640 135167914 3221224448 3221201536 134625515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 191288 191172 162 162 0 191126 0
[pid=15030] vsize: 765152
Current children cumulated CPU time (s) 271.79
Current children cumulated vsize (Kb) 767280

[startup+290.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 212239 0 0 0 27384 793 0 0 25 0 1 0 1854814897 783515648 191172 4294967295 134512640 135167914 3221224448 3221201488 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 191288 191172 162 162 0 191126 0
[pid=15030] vsize: 765152
Current children cumulated CPU time (s) 281.79
Current children cumulated vsize (Kb) 767280

[startup+300.024 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 214616 0 0 0 28354 809 0 0 25 0 1 0 1854814897 706863104 172458 4294967295 134512640 135167914 3221224448 3221200396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 172574 172458 162 162 0 172412 0
[pid=15030] vsize: 690296
Current children cumulated CPU time (s) 291.65
Current children cumulated vsize (Kb) 692424

[startup+310.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 219596 0 0 0 29302 830 0 0 25 0 1 0 1854814897 727261184 177438 4294967295 134512640 135167914 3221224448 3221200172 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 177554 177438 162 162 0 177392 0
[pid=15030] vsize: 710216
Current children cumulated CPU time (s) 301.34
Current children cumulated vsize (Kb) 712344

[startup+320.025 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 224832 0 0 0 30248 855 0 0 25 0 1 0 1854814897 748707840 182674 4294967295 134512640 135167914 3221224448 3221200252 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 182790 182674 162 162 0 182628 0
[pid=15030] vsize: 731160
Current children cumulated CPU time (s) 311.05
Current children cumulated vsize (Kb) 733288

[startup+330.026 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 230047 0 0 0 31193 879 0 0 25 0 1 0 1854814897 770068480 187889 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 188005 187889 162 162 0 187843 0
[pid=15030] vsize: 752020
Current children cumulated CPU time (s) 320.74
Current children cumulated vsize (Kb) 754148

[startup+340.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 235147 0 0 0 32134 904 0 0 25 0 1 0 1854814897 790958080 192989 4294967295 134512640 135167914 3221224448 3221200604 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 193105 192989 162 162 0 192943 0
[pid=15030] vsize: 772420
Current children cumulated CPU time (s) 330.4
Current children cumulated vsize (Kb) 774548

[startup+350.026 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 240331 0 0 0 33073 929 0 0 25 0 1 0 1854814897 812191744 198173 4294967295 134512640 135167914 3221224448 3221202012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 198289 198173 162 162 0 198127 0
[pid=15030] vsize: 793156
Current children cumulated CPU time (s) 340.04
Current children cumulated vsize (Kb) 795284

[startup+360.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 245490 0 0 0 34017 952 0 0 25 0 1 0 1854814897 833323008 203332 4294967295 134512640 135167914 3221224448 3221200800 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 203448 203332 162 162 0 203286 0
[pid=15030] vsize: 813792
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 815920

[startup+370.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 250727 0 0 0 34958 977 0 0 25 0 1 0 1854814897 854773760 208569 4294967295 134512640 135167914 3221224448 3221200444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/15030/statm): 208685 208569 162 162 0 208523 0
[pid=15030] vsize: 834740
Current children cumulated CPU time (s) 359.37
Current children cumulated vsize (Kb) 836868

[startup+380.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 255968 0 0 0 35901 1003 0 0 25 0 1 0 1854814897 876240896 213810 4294967295 134512640 135167914 3221224448 3221200864 134619044 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/15030/statm): 213926 213810 162 162 0 213764 0
[pid=15030] vsize: 855704
Current children cumulated CPU time (s) 369.06
Current children cumulated vsize (Kb) 857832

[startup+390.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 261082 0 0 0 36843 1028 0 0 25 0 1 0 1854814897 897187840 218924 4294967295 134512640 135167914 3221224448 3221201480 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 219040 218924 162 162 0 218878 0
[pid=15030] vsize: 876160
Current children cumulated CPU time (s) 378.73
Current children cumulated vsize (Kb) 878288

[startup+400.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) R 15025 15025 21452 0 -1 0 266339 0 45 0 37747 1053 0 0 24 0 1 0 1854814897 917487616 222850 4294967295 134512640 135167914 3221224448 3221200448 134845315 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15030/statm): 223996 222850 162 162 0 223834 0
[pid=15030] vsize: 895984
Current children cumulated CPU time (s) 388.02
Current children cumulated vsize (Kb) 898112

[startup+410.029 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) D 15025 15025 21452 0 -1 0 271082 0 93 0 38638 1078 0 0 18 0 1 0 1854814897 936292352 221324 4294967295 134512640 135167914 3221224448 3221203920 134623811 0 0 5 16386 3222515881 0 0 17 0 0 0
Raw data (/proc/15030/statm): 228587 221324 162 162 0 228425 0
[pid=15030] vsize: 914348
Current children cumulated CPU time (s) 397.18
Current children cumulated vsize (Kb) 916476



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+413.521 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 15030
Raw data (/proc/15025/stat): 15025 (minisat+_script) S 15024 15025 21452 0 -1 0 314 345 0 0 0 1 0 1 22 0 1 0 1854814891 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/15025/statm): 532 234 485 147 0 385 0
[pid=15025] vsize: 2128
Raw data (/proc/15030/stat): 15030 (minisat+_bignum) T 15025 15025 21452 0 -1 0 272729 0 173 0 38873 1084 0 0 25 0 1 0 1854814897 941543424 222893 4294967295 134512640 135167914 3221224448 3221201788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15030/statm): 229869 222893 162 162 0 229707 0
[pid=15030] vsize: 919476
Current children cumulated CPU time (s) 399.59
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 413.986
CPU time (s): 400.002
CPU user time (s): 388.738
CPU system time (s): 11.2643
CPU usage (%): 96.6221
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !