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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-scsd1.opb
MD5SUM18ccaf10caa576369b352d4f561a8c9e
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 22800
Biggest coefficient in the objective function 268435456000000000
Number of bits for the biggest coefficient in the objective function 58
Sum of the numbers in the objective function 188158757647584526336
Number of bits of the sum of numbers in the objective function 68
Biggest number in a constraint 268435456000000000
Number of bits of the biggest number in a constraint 58
Biggest sum of numbers in a constraint 188158757647584526336
Number of bits of the biggest sum of numbers68
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables22800
Total number of constraints77
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints77
Minimum length of a constraint600
Maximum length of a constraint1500

Trace number 2648

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-18 20:31:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2807 boxname=wulflinc21 idbench=463 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18ccaf10caa576369b352d4f561a8c9e  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb
IDLAUNCH: 2807
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        889196 kB
Buffers:         35252 kB
Cached:          82568 kB
SwapCached:        908 kB
Active:          82308 kB
Inactive:        38192 kB
HighTotal:      131008 kB
HighFree:        52248 kB
LowTotal:       903652 kB
LowFree:        836948 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            19280 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:40:14 (client local time) WITH STATUS 0 IN 490.66 SECONDS
stats: 2807 7 490.66 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 764] 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/31957/stat): 31957 (minisat+_script) R 31956 31957 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1721426832 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31957/statm): 174 3 169 147 0 27 0
[pid=31957] 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=31958
New process pid=31959
New process pid=31960
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=31959) exited with status: 0
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=31960) exited with status: 0
One traced child (pid=31958) exited with status: 0
New process pid=31961
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb
One traced child (pid=31961) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=31962
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-scsd1.opb

[startup+10.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 3112 0 0 0 959 15 0 0 25 0 1 0 1721426838 13500416 3056 4294967295 134512640 135167914 3221224448 3221221520 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 3296 3056 162 162 0 3134 0
[pid=31962] vsize: 13184
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 15312

[startup+20.0045 s]
Raw data (loadavg): 0.92 0.94 0.90 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 8195 0 0 0 1912 37 0 0 25 0 1 0 1721426838 31383552 7427 4294967295 134512640 135167914 3221224448 3221061852 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 7662 7427 162 162 0 7500 0
[pid=31962] vsize: 30648
Current children cumulated CPU time (s) 19.5
Current children cumulated vsize (Kb) 32776

[startup+30.0052 s]
Raw data (loadavg): 0.93 0.94 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 13227 0 0 0 2865 58 0 0 25 0 1 0 1721426838 49295360 11800 4294967295 134512640 135167914 3221224448 3221063712 134696045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 12035 11800 162 162 0 11873 0
[pid=31962] vsize: 48140
Current children cumulated CPU time (s) 29.24
Current children cumulated vsize (Kb) 50268

[startup+40.0059 s]
Raw data (loadavg): 0.94 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 19463 0 0 0 3822 80 0 0 25 0 1 0 1721426838 69439488 16718 4294967295 134512640 135167914 3221224448 3221065104 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 16953 16718 162 162 0 16791 0
[pid=31962] vsize: 67812
Current children cumulated CPU time (s) 39.03
Current children cumulated vsize (Kb) 69940

[startup+50.0065 s]
Raw data (loadavg): 0.95 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 23399 0 0 0 4782 96 0 0 25 0 1 0 1721426838 85561344 20654 4294967295 134512640 135167914 3221224448 3221063584 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 20889 20654 162 162 0 20727 0
[pid=31962] vsize: 83556
Current children cumulated CPU time (s) 48.79
Current children cumulated vsize (Kb) 85684

[startup+60.0062 s]
Raw data (loadavg): 0.96 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 31978 0 0 0 5734 123 0 0 25 0 1 0 1721426838 109899776 26596 4294967295 134512640 135167914 3221224448 3221062640 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 26831 26596 162 162 0 26669 0
[pid=31962] vsize: 107324
Current children cumulated CPU time (s) 58.58
Current children cumulated vsize (Kb) 109452

[startup+70.0069 s]
Raw data (loadavg): 0.96 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 35985 0 0 0 6686 143 0 0 25 0 1 0 1721426838 126312448 30603 4294967295 134512640 135167914 3221224448 3221061788 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 30838 30603 162 162 0 30676 0
[pid=31962] vsize: 123352
Current children cumulated CPU time (s) 68.3
Current children cumulated vsize (Kb) 125480

[startup+80.0076 s]
Raw data (loadavg): 0.97 0.95 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 39967 0 0 0 7644 159 0 0 25 0 1 0 1721426838 142622720 34585 4294967295 134512640 135167914 3221224448 3221061564 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 34820 34585 162 162 0 34658 0
[pid=31962] vsize: 139280
Current children cumulated CPU time (s) 78.04
Current children cumulated vsize (Kb) 141408

[startup+90.0083 s]
Raw data (loadavg): 0.97 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 44093 0 0 0 8597 180 0 0 25 0 1 0 1721426838 159522816 38711 4294967295 134512640 135167914 3221224448 3221062860 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 38946 38711 162 162 0 38784 0
[pid=31962] vsize: 155784
Current children cumulated CPU time (s) 87.78
Current children cumulated vsize (Kb) 157912

[startup+100.009 s]
Raw data (loadavg): 0.98 0.95 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 56908 0 0 0 9547 213 0 0 25 0 1 0 1721426838 190414848 46253 4294967295 134512640 135167914 3221224448 3221062460 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 46488 46253 162 162 0 46326 0
[pid=31962] vsize: 185952
Current children cumulated CPU time (s) 97.61
Current children cumulated vsize (Kb) 188080

[startup+110.01 s]
Raw data (loadavg): 0.98 0.95 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 61065 0 0 0 10503 230 0 0 25 0 1 0 1721426838 207441920 50410 4294967295 134512640 135167914 3221224448 3221063196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 50645 50410 162 162 0 50483 0
[pid=31962] vsize: 202580
Current children cumulated CPU time (s) 107.34
Current children cumulated vsize (Kb) 204708

[startup+120.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 65039 0 0 0 11458 248 0 0 25 0 1 0 1721426838 223719424 54384 4294967295 134512640 135167914 3221224448 3221061968 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 54619 54384 162 162 0 54457 0
[pid=31962] vsize: 218476
Current children cumulated CPU time (s) 117.07
Current children cumulated vsize (Kb) 220604

[startup+130.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 68972 0 0 0 12417 265 0 0 25 0 1 0 1721426838 239828992 58317 4294967295 134512640 135167914 3221224448 3221063536 134694351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 58552 58317 162 162 0 58390 0
[pid=31962] vsize: 234208
Current children cumulated CPU time (s) 126.83
Current children cumulated vsize (Kb) 236336

[startup+140.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 72988 0 0 0 13374 283 0 0 25 0 1 0 1721426838 256282624 62333 4294967295 134512640 135167914 3221224448 3221064080 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 62569 62333 162 162 0 62407 0
[pid=31962] vsize: 250276
Current children cumulated CPU time (s) 136.58
Current children cumulated vsize (Kb) 252404

[startup+150.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 77114 0 0 0 14330 302 0 0 25 0 1 0 1721426838 273182720 66459 4294967295 134512640 135167914 3221224448 3221065600 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 66695 66459 162 162 0 66533 0
[pid=31962] vsize: 266780
Current children cumulated CPU time (s) 146.33
Current children cumulated vsize (Kb) 268908

[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 81062 0 0 0 15286 320 0 0 25 0 1 0 1721426838 289349632 70407 4294967295 134512640 135167914 3221224448 3221062356 134697279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 70642 70407 162 162 0 70480 0
[pid=31962] vsize: 282568
Current children cumulated CPU time (s) 156.07
Current children cumulated vsize (Kb) 284696

[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 85044 0 0 0 16243 338 0 0 25 0 1 0 1721426838 305659904 74389 4294967295 134512640 135167914 3221224448 3221063956 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 74624 74389 162 162 0 74462 0
[pid=31962] vsize: 298496
Current children cumulated CPU time (s) 165.82
Current children cumulated vsize (Kb) 300624

[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 109232 0 0 0 17161 400 0 0 25 0 1 0 1721426838 404733952 98577 4294967295 134512640 135167914 3221224448 3221063252 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 98812 98577 162 162 0 98650 0
[pid=31962] vsize: 395248
Current children cumulated CPU time (s) 175.62
Current children cumulated vsize (Kb) 397376

[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 110893 0 0 0 18141 409 0 0 25 0 1 0 1721426838 368340992 89692 4294967295 134512640 135167914 3221224448 3221062496 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 89927 89692 162 162 0 89765 0
[pid=31962] vsize: 359708
Current children cumulated CPU time (s) 185.51
Current children cumulated vsize (Kb) 361836

[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 115015 0 0 0 19099 427 0 0 25 0 1 0 1721426838 385224704 93814 4294967295 134512640 135167914 3221224448 3221062820 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 94049 93814 162 162 0 93887 0
[pid=31962] vsize: 376196
Current children cumulated CPU time (s) 195.27
Current children cumulated vsize (Kb) 378324

[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 119309 0 0 0 20050 449 0 0 25 0 1 0 1721426838 402812928 98108 4294967295 134512640 135167914 3221224448 3221062684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31962/statm): 98343 98108 162 162 0 98181 0
[pid=31962] vsize: 393372
Current children cumulated CPU time (s) 205
Current children cumulated vsize (Kb) 395500

[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 123571 0 0 0 21004 465 0 0 25 0 1 0 1721426838 420270080 102370 4294967295 134512640 135167914 3221224448 3221063852 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 102605 102370 162 162 0 102443 0
[pid=31962] vsize: 410420
Current children cumulated CPU time (s) 214.7
Current children cumulated vsize (Kb) 412548

[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 127748 0 0 0 21959 483 0 0 25 0 1 0 1721426838 437379072 106547 4294967295 134512640 135167914 3221224448 3221061788 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 106782 106547 162 162 0 106620 0
[pid=31962] vsize: 427128
Current children cumulated CPU time (s) 224.43
Current children cumulated vsize (Kb) 429256

[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 131798 0 0 0 22914 502 0 0 25 0 1 0 1721426838 453967872 110597 4294967295 134512640 135167914 3221224448 3221062752 134694419 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 110832 110597 162 162 0 110670 0
[pid=31962] vsize: 443328
Current children cumulated CPU time (s) 234.17
Current children cumulated vsize (Kb) 445456

[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 135842 0 0 0 23871 520 0 0 25 0 1 0 1721426838 470532096 114641 4294967295 134512640 135167914 3221224448 3221062768 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 114876 114641 162 162 0 114714 0
[pid=31962] vsize: 459504
Current children cumulated CPU time (s) 243.92
Current children cumulated vsize (Kb) 461632

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 139927 0 0 0 24826 540 0 0 25 0 1 0 1721426838 487264256 118726 4294967295 134512640 135167914 3221224448 3221061776 134621149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 118961 118726 162 162 0 118799 0
[pid=31962] vsize: 475844
Current children cumulated CPU time (s) 253.67
Current children cumulated vsize (Kb) 477972

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 143791 0 0 0 25785 556 0 0 25 0 1 0 1721426838 503091200 122590 4294967295 134512640 135167914 3221224448 3221062620 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 122825 122590 162 162 0 122663 0
[pid=31962] vsize: 491300
Current children cumulated CPU time (s) 263.42
Current children cumulated vsize (Kb) 493428

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 147743 0 0 0 26742 573 0 0 25 0 1 0 1721426838 519286784 126542 4294967295 134512640 135167914 3221224448 3221063312 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 126779 126542 162 162 0 126617 0
[pid=31962] vsize: 507116
Current children cumulated CPU time (s) 273.16
Current children cumulated vsize (Kb) 509244

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 151697 0 0 0 27699 591 0 0 25 0 1 0 1721426838 535482368 130496 4294967295 134512640 135167914 3221224448 3221063936 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 130733 130496 162 162 0 130571 0
[pid=31962] vsize: 522932
Current children cumulated CPU time (s) 282.91
Current children cumulated vsize (Kb) 525060

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 155697 0 0 0 28656 609 0 0 25 0 1 0 1721426838 551866368 134496 4294967295 134512640 135167914 3221224448 3221063344 134619572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 134733 134496 162 162 0 134571 0
[pid=31962] vsize: 538932
Current children cumulated CPU time (s) 292.66
Current children cumulated vsize (Kb) 541060

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 159505 0 0 0 29614 628 0 0 25 0 1 0 1721426838 567463936 138304 4294967295 134512640 135167914 3221224448 3221065344 134621119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 138541 138304 162 162 0 138379 0
[pid=31962] vsize: 554164
Current children cumulated CPU time (s) 302.43
Current children cumulated vsize (Kb) 556292

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 163311 0 0 0 30572 646 0 0 25 0 1 0 1721426838 583053312 142110 4294967295 134512640 135167914 3221224448 3221062300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 142347 142110 162 162 0 142185 0
[pid=31962] vsize: 569388
Current children cumulated CPU time (s) 312.19
Current children cumulated vsize (Kb) 571516

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 167164 0 0 0 31530 663 0 0 25 0 1 0 1721426838 598835200 145963 4294967295 134512640 135167914 3221224448 3221062912 134844866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 146200 145963 162 162 0 146038 0
[pid=31962] vsize: 584800
Current children cumulated CPU time (s) 321.94
Current children cumulated vsize (Kb) 586928

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 171017 0 0 0 32490 680 0 0 25 0 1 0 1721426838 614617088 149816 4294967295 134512640 135167914 3221224448 3221062784 134624387 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 150053 149816 162 162 0 149891 0
[pid=31962] vsize: 600212
Current children cumulated CPU time (s) 331.71
Current children cumulated vsize (Kb) 602340

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 215010 0 0 0 33376 783 0 0 25 0 1 0 1721426838 794808320 193809 4294967295 134512640 135167914 3221224448 3221063276 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 194045 193809 162 162 0 193883 0
[pid=31962] vsize: 776180
Current children cumulated CPU time (s) 341.6
Current children cumulated vsize (Kb) 778308

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 215010 0 0 0 34376 783 0 0 25 0 1 0 1721426838 794808320 193809 4294967295 134512640 135167914 3221224448 3221063328 134625428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 194045 193809 162 162 0 193883 0
[pid=31962] vsize: 776180
Current children cumulated CPU time (s) 351.6
Current children cumulated vsize (Kb) 778308

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 218424 0 0 0 35335 803 0 0 25 0 1 0 1721426838 722407424 176132 4294967295 134512640 135167914 3221224448 3221061696 134854320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 176369 176132 162 162 0 176207 0
[pid=31962] vsize: 705476
Current children cumulated CPU time (s) 361.39
Current children cumulated vsize (Kb) 707604

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 222584 0 0 0 36286 822 0 0 25 0 1 0 1721426838 739442688 180292 4294967295 134512640 135167914 3221224448 3221063456 134623781 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 180528 180292 162 162 0 180366 0
[pid=31962] vsize: 722112
Current children cumulated CPU time (s) 371.09
Current children cumulated vsize (Kb) 724240

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 226823 0 0 0 37240 839 0 0 25 0 1 0 1721426838 756805632 184531 4294967295 134512640 135167914 3221224448 3221063304 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 184767 184531 162 162 0 184605 0
[pid=31962] vsize: 739068
Current children cumulated CPU time (s) 380.8
Current children cumulated vsize (Kb) 741196

[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 230981 0 0 0 38196 857 0 0 25 0 1 0 1721426838 773836800 188689 4294967295 134512640 135167914 3221224448 3221063612 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31962/statm): 188925 188689 162 162 0 188763 0
[pid=31962] vsize: 755700
Current children cumulated CPU time (s) 390.54
Current children cumulated vsize (Kb) 757828

[startup+410.028 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 235103 0 0 0 39150 875 0 0 24 0 1 0 1721426838 790720512 192811 4294967295 134512640 135167914 3221224448 3221064560 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 193047 192811 162 162 0 192885 0
[pid=31962] vsize: 772188
Current children cumulated CPU time (s) 400.26
Current children cumulated vsize (Kb) 774316

[startup+420.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 239122 0 0 0 40106 896 0 0 25 0 1 0 1721426838 807182336 196830 4294967295 134512640 135167914 3221224448 3221063744 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 197066 196830 162 162 0 196904 0
[pid=31962] vsize: 788264
Current children cumulated CPU time (s) 410.03
Current children cumulated vsize (Kb) 790392

[startup+430.029 s]
Raw data (loadavg): 1.05 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 243114 0 0 0 41058 915 0 0 25 0 1 0 1721426838 823533568 200822 4294967295 134512640 135167914 3221224448 3221062576 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 201058 200822 162 162 0 200896 0
[pid=31962] vsize: 804232
Current children cumulated CPU time (s) 419.74
Current children cumulated vsize (Kb) 806360

[startup+440.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 247112 0 0 0 42018 933 0 0 25 0 1 0 1721426838 839909376 204820 4294967295 134512640 135167914 3221224448 3221061776 134618969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31962/statm): 205056 204820 162 162 0 204894 0
[pid=31962] vsize: 820224
Current children cumulated CPU time (s) 429.52
Current children cumulated vsize (Kb) 822352

[startup+450.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 251112 0 0 0 42969 953 0 0 25 0 1 0 1721426838 856293376 208820 4294967295 134512640 135167914 3221224448 3221062844 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 209056 208820 162 162 0 208894 0
[pid=31962] vsize: 836224
Current children cumulated CPU time (s) 439.23
Current children cumulated vsize (Kb) 838352

[startup+460.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 255062 0 0 0 43927 970 0 0 25 0 1 0 1721426838 872472576 212770 4294967295 134512640 135167914 3221224448 3221062384 134522460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 213006 212770 162 162 0 212844 0
[pid=31962] vsize: 852024
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 854152

[startup+470.032 s]
Raw data (loadavg): 1.03 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 259023 0 0 0 44882 987 0 0 25 0 1 0 1721426838 888696832 216731 4294967295 134512640 135167914 3221224448 3221062868 134619947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 216967 216731 162 162 0 216805 0
[pid=31962] vsize: 867868
Current children cumulated CPU time (s) 458.7
Current children cumulated vsize (Kb) 869996

[startup+480.033 s]
Raw data (loadavg): 1.02 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 263010 0 0 0 45843 1003 0 0 25 0 1 0 1721426838 905027584 220718 4294967295 134512640 135167914 3221224448 3221063360 134845396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 220954 220718 162 162 0 220792 0
[pid=31962] vsize: 883816
Current children cumulated CPU time (s) 468.47
Current children cumulated vsize (Kb) 885944

[startup+490.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) R 31957 31957 20602 0 -1 0 267052 0 46 0 46756 1024 0 0 25 0 1 0 1721426838 920588288 224316 4294967295 134512640 135167914 3221224448 3221062992 134693558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31962/statm): 224753 224316 162 162 0 224591 0
[pid=31962] vsize: 899012
Current children cumulated CPU time (s) 477.81
Current children cumulated vsize (Kb) 901140

[startup+500.035 s]
Raw data (loadavg): 1.01 0.99 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 271072 0 50 0 47702 1048 0 0 25 0 1 0 1721426838 936988672 227755 4294967295 134512640 135167914 3221224448 3221063196 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31962/statm): 228757 227755 162 162 0 228595 0
[pid=31962] vsize: 915028
Current children cumulated CPU time (s) 487.51
Current children cumulated vsize (Kb) 917156



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+502.891 s]
Raw data (loadavg): 1.01 0.99 0.91 1/58 31962
Raw data (/proc/31957/stat): 31957 (minisat+_script) S 31956 31957 20602 0 -1 0 314 332 0 0 0 0 0 1 22 0 1 0 1721426832 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31957/statm): 532 234 485 147 0 385 0
[pid=31957] vsize: 2128
Raw data (/proc/31962/stat): 31962 (minisat+_bignum) T 31957 31957 20602 0 -1 0 272192 0 54 0 47969 1053 0 0 25 0 1 0 1721426838 941543424 228465 4294967295 134512640 135167914 3221224448 3221062396 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/31962/statm): 229869 228465 162 162 0 229707 0
[pid=31962] vsize: 919476
Current children cumulated CPU time (s) 490.23
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 503.319
CPU time (s): 490.66
CPU user time (s): 479.699
CPU system time (s): 10.9613
CPU usage (%): 97.4849
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !