Some explanations

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

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-glass4.opb
MD5SUM7ca49051adbbebe6e2c6f68e4bc64c63
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 863236227986
Optimality of the best value was proved NO
Number of terms in the objective function 351
Biggest coefficient in the objective function 524288000000
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 1048594922917
Number of bits of the sum of numbers in the objective function 40
Biggest number in a constraint 1075200000000000000
Number of bits of the biggest number in a constraint 60
Biggest sum of numbers in a constraint 2440670651161677657
Number of bits of the biggest sum of numbers62
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1226.23
Number of variables653
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 constraint75

Trace number 6308

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        885128 kB
Buffers:         27808 kB
Cached:          92708 kB
SwapCached:        660 kB
Active:          36212 kB
Inactive:        86832 kB
HighTotal:      131008 kB
HighFree:        34860 kB
LowTotal:       903652 kB
LowFree:        850268 kB
SwapTotal:     2097640 kB
SwapFree:      2096408 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5820 kB
Slab:            20776 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:44:54 (client local time) WITH STATUS 0 IN 403.028 SECONDS
stats: 3492 7 403.028 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 653] 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/21958/stat): 21958 (minisat+_script) R 21957 21958 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1856085842 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21958/statm): 174 3 169 147 0 27 0
[pid=21958] 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=21959
New process pid=21960
New process pid=21961
execve syscall for /bin/sed executable
One traced child (pid=21960) 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=21961) exited with status: 0
One traced child (pid=21959) exited with status: 0
New process pid=21962
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-glass4.opb
One traced child (pid=21962) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=21963
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-glass4.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.96 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 5487 0 0 0 939 24 0 0 25 0 1 0 1856085850 20357120 4853 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 4970 4853 162 162 0 4808 0
[pid=21963] vsize: 19880
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 22008

[startup+20.0068 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 13781 0 0 0 1884 53 0 0 25 0 1 0 1856085850 51630080 12488 4294967295 134512640 135167914 3221224448 3221208256 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 12605 12488 162 162 0 12443 0
[pid=21963] vsize: 50420
Current children cumulated CPU time (s) 19.39
Current children cumulated vsize (Kb) 52548

[startup+30.0074 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 18496 0 0 0 2833 75 0 0 25 0 1 0 1856085850 65544192 15885 4294967295 134512640 135167914 3221224448 3221207008 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 16002 15885 162 162 0 15840 0
[pid=21963] vsize: 64008
Current children cumulated CPU time (s) 29.1
Current children cumulated vsize (Kb) 66136

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 27468 0 0 0 3784 101 0 0 25 0 1 0 1856085850 91492352 22220 4294967295 134512640 135167914 3221224448 3221207148 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 22337 22220 162 162 0 22175 0
[pid=21963] vsize: 89348
Current children cumulated CPU time (s) 38.87
Current children cumulated vsize (Kb) 91476

[startup+50.0078 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 32352 0 0 0 4734 123 0 0 25 0 1 0 1856085850 111497216 27104 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 27221 27104 162 162 0 27059 0
[pid=21963] vsize: 108884
Current children cumulated CPU time (s) 48.59
Current children cumulated vsize (Kb) 111012

[startup+60.0085 s]
Raw data (loadavg): 0.97 0.96 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 37279 0 0 0 5682 145 0 0 25 0 1 0 1856085850 131678208 32031 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 32148 32031 162 162 0 31986 0
[pid=21963] vsize: 128592
Current children cumulated CPU time (s) 58.29
Current children cumulated vsize (Kb) 130720

[startup+70.0092 s]
Raw data (loadavg): 0.97 0.96 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 42173 0 0 0 6628 168 0 0 25 0 1 0 1856085850 151724032 36925 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 37042 36925 162 162 0 36880 0
[pid=21963] vsize: 148168
Current children cumulated CPU time (s) 67.98
Current children cumulated vsize (Kb) 150296

[startup+80.0099 s]
Raw data (loadavg): 0.98 0.96 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 55693 0 0 0 7571 207 0 0 25 0 1 0 1856085850 185503744 45172 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 45289 45172 162 162 0 45127 0
[pid=21963] vsize: 181156
Current children cumulated CPU time (s) 77.8
Current children cumulated vsize (Kb) 183284

[startup+90.0096 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 60853 0 0 0 8514 233 0 0 25 0 1 0 1856085850 206639104 50332 4294967295 134512640 135167914 3221224448 3221206172 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 50449 50332 162 162 0 50287 0
[pid=21963] vsize: 201796
Current children cumulated CPU time (s) 87.49
Current children cumulated vsize (Kb) 203924

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 65896 0 0 0 9457 257 0 0 25 0 1 0 1856085850 227295232 55375 4294967295 134512640 135167914 3221224448 3221205980 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 55492 55375 162 162 0 55330 0
[pid=21963] vsize: 221968
Current children cumulated CPU time (s) 97.16
Current children cumulated vsize (Kb) 224096

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 70914 0 0 0 10402 279 0 0 25 0 1 0 1856085850 247848960 60393 4294967295 134512640 135167914 3221224448 3221206688 134620493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21963/statm): 60510 60393 162 162 0 60348 0
[pid=21963] vsize: 242040
Current children cumulated CPU time (s) 106.83
Current children cumulated vsize (Kb) 244168

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 75936 0 0 0 11350 301 0 0 25 0 1 0 1856085850 268419072 65415 4294967295 134512640 135167914 3221224448 3221206640 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 65532 65415 162 162 0 65370 0
[pid=21963] vsize: 262128
Current children cumulated CPU time (s) 116.53
Current children cumulated vsize (Kb) 264256

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 80919 0 0 0 12293 324 0 0 25 0 1 0 1856085850 288829440 70398 4294967295 134512640 135167914 3221224448 3221206896 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 70515 70398 162 162 0 70353 0
[pid=21963] vsize: 282060
Current children cumulated CPU time (s) 126.19
Current children cumulated vsize (Kb) 284188

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 106334 0 0 0 13199 390 0 0 25 0 1 0 1856085850 392929280 95813 4294967295 134512640 135167914 3221224448 3221207336 134624945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 95930 95813 162 162 0 95768 0
[pid=21963] vsize: 383720
Current children cumulated CPU time (s) 135.91
Current children cumulated vsize (Kb) 385848

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 107998 0 0 0 14180 397 0 0 25 0 1 0 1856085850 356548608 86931 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 87048 86931 162 162 0 86886 0
[pid=21963] vsize: 348192
Current children cumulated CPU time (s) 145.79
Current children cumulated vsize (Kb) 350320

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 113038 0 0 0 15124 423 0 0 25 0 1 0 1856085850 377192448 91971 4294967295 134512640 135167914 3221224448 3221206592 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 92088 91971 162 162 0 91926 0
[pid=21963] vsize: 368352
Current children cumulated CPU time (s) 155.49
Current children cumulated vsize (Kb) 370480

[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 117912 0 0 0 16074 444 0 0 25 0 1 0 1856085850 397156352 96845 4294967295 134512640 135167914 3221224448 3221209280 134844641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 96962 96845 162 162 0 96800 0
[pid=21963] vsize: 387848
Current children cumulated CPU time (s) 165.2
Current children cumulated vsize (Kb) 389976

[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 122832 0 0 0 17023 466 0 0 25 0 1 0 1856085850 417308672 101765 4294967295 134512640 135167914 3221224448 3221206784 134694407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 101882 101765 162 162 0 101720 0
[pid=21963] vsize: 407528
Current children cumulated CPU time (s) 174.91
Current children cumulated vsize (Kb) 409656

[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 127692 0 0 0 17971 487 0 0 25 0 1 0 1856085850 437215232 106625 4294967295 134512640 135167914 3221224448 3221206432 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 106742 106625 162 162 0 106580 0
[pid=21963] vsize: 426968
Current children cumulated CPU time (s) 184.6
Current children cumulated vsize (Kb) 429096

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 132585 0 0 0 18916 510 0 0 25 0 1 0 1856085850 457256960 111518 4294967295 134512640 135167914 3221224448 3221207164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 111635 111518 162 162 0 111473 0
[pid=21963] vsize: 446540
Current children cumulated CPU time (s) 194.28
Current children cumulated vsize (Kb) 448668

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 137429 0 0 0 19863 531 0 0 25 0 1 0 1856085850 477097984 116362 4294967295 134512640 135167914 3221224448 3221206748 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 116479 116362 162 162 0 116317 0
[pid=21963] vsize: 465916
Current children cumulated CPU time (s) 203.96
Current children cumulated vsize (Kb) 468044

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 142235 0 0 0 20810 553 0 0 25 0 1 0 1856085850 496783360 121168 4294967295 134512640 135167914 3221224448 3221207316 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 121285 121168 162 162 0 121123 0
[pid=21963] vsize: 485140
Current children cumulated CPU time (s) 213.65
Current children cumulated vsize (Kb) 487268

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 146789 0 0 0 21759 575 0 0 25 0 1 0 1856085850 515436544 125722 4294967295 134512640 135167914 3221224448 3221206544 134625115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 125839 125722 162 162 0 125677 0
[pid=21963] vsize: 503356
Current children cumulated CPU time (s) 223.36
Current children cumulated vsize (Kb) 505484

[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 151781 0 0 0 22705 597 0 0 25 0 1 0 1856085850 535883776 130714 4294967295 134512640 135167914 3221224448 3221205980 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 130831 130714 162 162 0 130669 0
[pid=21963] vsize: 523324
Current children cumulated CPU time (s) 233.04
Current children cumulated vsize (Kb) 525452

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 156546 0 0 0 23654 618 0 0 25 0 1 0 1856085850 555401216 135479 4294967295 134512640 135167914 3221224448 3221206748 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 135596 135479 162 162 0 135434 0
[pid=21963] vsize: 542384
Current children cumulated CPU time (s) 242.74
Current children cumulated vsize (Kb) 544512

[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 161120 0 0 0 24605 636 0 0 25 0 1 0 1856085850 574136320 140053 4294967295 134512640 135167914 3221224448 3221207068 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 140170 140053 162 162 0 140008 0
[pid=21963] vsize: 560680
Current children cumulated CPU time (s) 252.43
Current children cumulated vsize (Kb) 562808

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 165655 0 0 0 25558 654 0 0 25 0 1 0 1856085850 592711680 144588 4294967295 134512640 135167914 3221224448 3221208772 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 144705 144588 162 162 0 144543 0
[pid=21963] vsize: 578820
Current children cumulated CPU time (s) 262.14
Current children cumulated vsize (Kb) 580948

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 191495 0 0 0 26465 720 0 0 25 0 1 0 1856085850 782987264 170428 4294967295 134512640 135167914 3221224448 3221206464 134625368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 191159 170435 162 162 0 190997 0
[pid=21963] vsize: 764636
Current children cumulated CPU time (s) 271.87
Current children cumulated vsize (Kb) 766764

[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 212109 0 0 0 27420 765 0 0 25 0 1 0 1856085850 782987264 191042 4294967295 134512640 135167914 3221224448 3221206448 134625468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 191159 191042 162 162 0 190997 0
[pid=21963] vsize: 764636
Current children cumulated CPU time (s) 281.87
Current children cumulated vsize (Kb) 766764

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 214077 0 0 0 28398 777 0 0 25 0 1 0 1856085850 704659456 171919 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 172036 171919 162 162 0 171874 0
[pid=21963] vsize: 688144
Current children cumulated CPU time (s) 291.77
Current children cumulated vsize (Kb) 690272

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 218914 0 0 0 29346 798 0 0 25 0 1 0 1856085850 724475904 176756 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 176874 176756 162 162 0 176712 0
[pid=21963] vsize: 707496
Current children cumulated CPU time (s) 301.46
Current children cumulated vsize (Kb) 709624

[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 224018 0 0 0 30289 821 0 0 25 0 1 0 1856085850 745377792 181860 4294967295 134512640 135167914 3221224448 3221206304 134844694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 181977 181860 162 162 0 181815 0
[pid=21963] vsize: 727908
Current children cumulated CPU time (s) 311.12
Current children cumulated vsize (Kb) 730036

[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 229134 0 0 0 31232 846 0 0 25 0 1 0 1856085850 766332928 186976 4294967295 134512640 135167914 3221224448 3221206284 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 187093 186976 162 162 0 186931 0
[pid=21963] vsize: 748372
Current children cumulated CPU time (s) 320.8
Current children cumulated vsize (Kb) 750500

[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 234170 0 0 0 32175 871 0 0 25 0 1 0 1856085850 786960384 192012 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 192129 192012 162 162 0 191967 0
[pid=21963] vsize: 768516
Current children cumulated CPU time (s) 330.48
Current children cumulated vsize (Kb) 770644

[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 239221 0 0 0 33118 895 0 0 25 0 1 0 1856085850 807649280 197063 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 197180 197063 162 162 0 197018 0
[pid=21963] vsize: 788720
Current children cumulated CPU time (s) 340.15
Current children cumulated vsize (Kb) 790848

[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 244265 0 0 0 34061 918 0 0 25 0 1 0 1856085850 828309504 202107 4294967295 134512640 135167914 3221224448 3221207488 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 202224 202107 162 162 0 202062 0
[pid=21963] vsize: 808896
Current children cumulated CPU time (s) 349.81
Current children cumulated vsize (Kb) 811024

[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 249385 0 0 0 35002 941 0 0 25 0 1 0 1856085850 849281024 207227 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 207344 207227 162 162 0 207182 0
[pid=21963] vsize: 829376
Current children cumulated CPU time (s) 359.45
Current children cumulated vsize (Kb) 831504

[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 254498 0 0 0 35943 966 0 0 25 0 1 0 1856085850 870223872 212340 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 212457 212340 162 162 0 212295 0
[pid=21963] vsize: 849828
Current children cumulated CPU time (s) 369.11
Current children cumulated vsize (Kb) 851956

[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 259574 0 0 0 36887 991 0 0 25 0 1 0 1856085850 891015168 217416 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21963/statm): 217533 217416 162 162 0 217371 0
[pid=21963] vsize: 870132
Current children cumulated CPU time (s) 378.8
Current children cumulated vsize (Kb) 872260

[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 264639 0 1 0 37825 1017 0 0 25 0 1 0 1856085850 911761408 221923 4294967295 134512640 135167914 3221224448 3221207152 134619111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21963/statm): 222598 221923 162 162 0 222436 0
[pid=21963] vsize: 890392
Current children cumulated CPU time (s) 388.44
Current children cumulated vsize (Kb) 892520

[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) R 21958 21958 20115 0 -1 0 269761 0 58 0 38741 1042 0 0 25 0 1 0 1856085850 931631104 225442 4294967295 134512640 135167914 3221224448 3221206368 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21963/statm): 227449 225442 162 162 0 227287 0
[pid=21963] vsize: 909796
Current children cumulated CPU time (s) 397.85
Current children cumulated vsize (Kb) 911924



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+415.862 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21963
Raw data (/proc/21958/stat): 21958 (minisat+_script) S 21957 21958 20115 0 -1 0 314 375 0 0 0 1 1 0 21 0 1 0 1856085842 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21958/statm): 532 234 485 147 0 385 0
[pid=21958] vsize: 2128
Raw data (/proc/21963/stat): 21963 (minisat+_bignum) T 21958 21958 20115 0 -1 0 272653 0 183 0 39202 1057 0 0 25 0 1 0 1856085850 941543424 226877 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/21963/statm): 229869 226877 162 162 0 229707 0
[pid=21963] vsize: 919476
Current children cumulated CPU time (s) 402.61
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 416.294
CPU time (s): 403.028
CPU user time (s): 392.028
CPU system time (s): 10.9993
CPU usage (%): 96.8132
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !