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-net12.opb
MD5SUM1e83ed64f0fd862e44095daf089e38c2
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 benchmark1239.36
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 6310

Launcher Data

LAUNCH ON wulflinc17 THE 2005-09-20 05:39:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3493 boxname=wulflinc17 idbench=1149 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1e83ed64f0fd862e44095daf089e38c2  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb
IDLAUNCH: 3493
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        897352 kB
Buffers:         20508 kB
Cached:          88904 kB
SwapCached:        612 kB
Active:          32152 kB
Inactive:        79836 kB
HighTotal:      131008 kB
HighFree:        42364 kB
LowTotal:       903652 kB
LowFree:        854988 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            19784 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:46:28 (client local time) WITH STATUS 0 IN 403.239 SECONDS
stats: 3493 7 403.239 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/7595/stat): 7595 (minisat+_script) R 7594 7595 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856109726 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7595/statm): 174 3 169 147 0 27 0
[pid=7595] 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=7596
New process pid=7597
New process pid=7598
One traced child (pid=7597) exited with status: 0
execve syscall for /bin/sed executable
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=7598) exited with status: 0
One traced child (pid=7596) exited with status: 0
New process pid=7599
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb
One traced child (pid=7599) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7600
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-net12.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.98 0.98 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 5469 0 0 0 943 23 0 0 25 0 1 0 1856109734 20283392 4835 4294967295 134512640 135167914 3221224448 3221206352 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 4952 4835 162 162 0 4790 0
[pid=7600] vsize: 19808
Current children cumulated CPU time (s) 9.69
Current children cumulated vsize (Kb) 21936

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.98 0.98 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 13781 0 0 0 1886 54 0 0 25 0 1 0 1856109734 51630080 12488 4294967295 134512640 135167914 3221224448 3221208240 134625468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 12605 12488 162 162 0 12443 0
[pid=7600] vsize: 50420
Current children cumulated CPU time (s) 19.43
Current children cumulated vsize (Kb) 52548

[startup+30.0054 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 18490 0 0 0 2837 75 0 0 25 0 1 0 1856109734 65519616 15879 4294967295 134512640 135167914 3221224448 3221207152 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 15996 15879 162 162 0 15834 0
[pid=7600] vsize: 63984
Current children cumulated CPU time (s) 29.15
Current children cumulated vsize (Kb) 66112

[startup+40.006 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 27447 0 0 0 3787 105 0 0 25 0 1 0 1856109734 91406336 22199 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 22316 22199 162 162 0 22154 0
[pid=7600] vsize: 89264
Current children cumulated CPU time (s) 38.95
Current children cumulated vsize (Kb) 91392

[startup+50.0066 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 32334 0 0 0 4737 126 0 0 25 0 1 0 1856109734 111423488 27086 4294967295 134512640 135167914 3221224448 3221207520 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 27203 27086 162 162 0 27041 0
[pid=7600] vsize: 108812
Current children cumulated CPU time (s) 48.66
Current children cumulated vsize (Kb) 110940

[startup+60.0072 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 37265 0 0 0 5681 149 0 0 25 0 1 0 1856109734 131620864 32017 4294967295 134512640 135167914 3221224448 3221207920 134624972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 32134 32017 162 162 0 31972 0
[pid=7600] vsize: 128536
Current children cumulated CPU time (s) 58.33
Current children cumulated vsize (Kb) 130664

[startup+70.0078 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 42150 0 0 0 6625 172 0 0 25 0 1 0 1856109734 151629824 36902 4294967295 134512640 135167914 3221224448 3221206300 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 37019 36902 162 162 0 36857 0
[pid=7600] vsize: 148076
Current children cumulated CPU time (s) 68
Current children cumulated vsize (Kb) 150204

[startup+80.0084 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 55673 0 0 0 7569 211 0 0 25 0 1 0 1856109734 185421824 45152 4294967295 134512640 135167914 3221224448 3221208252 134522320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 45269 45152 162 162 0 45107 0
[pid=7600] vsize: 181076
Current children cumulated CPU time (s) 77.83
Current children cumulated vsize (Kb) 183204

[startup+90.009 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 60830 0 0 0 8511 234 0 0 25 0 1 0 1856109734 206544896 50309 4294967295 134512640 135167914 3221224448 3221207040 134624821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 50426 50309 162 162 0 50264 0
[pid=7600] vsize: 201704
Current children cumulated CPU time (s) 87.48
Current children cumulated vsize (Kb) 203832

[startup+100.01 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 65873 0 0 0 9458 258 0 0 25 0 1 0 1856109734 227201024 55352 4294967295 134512640 135167914 3221224448 3221206396 134697040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 55469 55352 162 162 0 55307 0
[pid=7600] vsize: 221876
Current children cumulated CPU time (s) 97.19
Current children cumulated vsize (Kb) 224004

[startup+110.01 s]
Raw data (loadavg): 1.00 1.00 0.99 1/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 70903 0 0 0 10405 281 0 0 25 0 1 0 1856109734 247808000 60382 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 60500 60382 162 162 0 60338 0
[pid=7600] vsize: 242000
Current children cumulated CPU time (s) 106.89
Current children cumulated vsize (Kb) 244128

[startup+120.011 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 75911 0 0 0 11349 308 0 0 25 0 1 0 1856109734 268316672 65390 4294967295 134512640 135167914 3221224448 3221206320 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 65507 65390 162 162 0 65345 0
[pid=7600] vsize: 262028
Current children cumulated CPU time (s) 116.6
Current children cumulated vsize (Kb) 264156

[startup+130.011 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 80894 0 0 0 12297 332 0 0 25 0 1 0 1856109734 288727040 70373 4294967295 134512640 135167914 3221224448 3221206432 134694410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 70490 70373 162 162 0 70328 0
[pid=7600] vsize: 281960
Current children cumulated CPU time (s) 126.32
Current children cumulated vsize (Kb) 284088

[startup+140.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 106334 0 0 0 13200 402 0 0 25 0 1 0 1856109734 392929280 95813 4294967295 134512640 135167914 3221224448 3221207360 134625423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 95930 95813 162 162 0 95768 0
[pid=7600] vsize: 383720
Current children cumulated CPU time (s) 136.05
Current children cumulated vsize (Kb) 385848

[startup+150.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 107955 0 0 0 14180 411 0 0 25 0 1 0 1856109734 356372480 86888 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 87005 86888 162 162 0 86843 0
[pid=7600] vsize: 348020
Current children cumulated CPU time (s) 145.94
Current children cumulated vsize (Kb) 350148

[startup+160.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 112991 0 0 0 15126 436 0 0 25 0 1 0 1856109734 376999936 91924 4294967295 134512640 135167914 3221224448 3221207328 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 92041 91924 162 162 0 91879 0
[pid=7600] vsize: 368164
Current children cumulated CPU time (s) 155.65
Current children cumulated vsize (Kb) 370292

[startup+170.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 117862 0 0 0 16076 457 0 0 25 0 1 0 1856109734 396951552 96795 4294967295 134512640 135167914 3221224448 3221207104 134843402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7600/statm): 96912 96795 162 162 0 96750 0
[pid=7600] vsize: 387648
Current children cumulated CPU time (s) 165.36
Current children cumulated vsize (Kb) 389776

[startup+180.013 s]
Raw data (loadavg): 1.00 1.00 0.99 1/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 122768 0 0 0 17022 479 0 0 25 0 1 0 1856109734 417046528 101701 4294967295 134512640 135167914 3221224448 3221206844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 101818 101701 162 162 0 101656 0
[pid=7600] vsize: 407272
Current children cumulated CPU time (s) 175.04
Current children cumulated vsize (Kb) 409400

[startup+190.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 127638 0 0 0 17969 500 0 0 25 0 1 0 1856109734 436994048 106571 4294967295 134512640 135167914 3221224448 3221206524 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 106688 106571 162 162 0 106526 0
[pid=7600] vsize: 426752
Current children cumulated CPU time (s) 184.72
Current children cumulated vsize (Kb) 428880

[startup+200.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 132532 0 0 0 18921 520 0 0 25 0 1 0 1856109734 457039872 111465 4294967295 134512640 135167914 3221224448 3221207136 134847335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 111582 111465 162 162 0 111420 0
[pid=7600] vsize: 446328
Current children cumulated CPU time (s) 194.44
Current children cumulated vsize (Kb) 448456

[startup+210.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 137360 0 0 0 19868 543 0 0 25 0 1 0 1856109734 476815360 116293 4294967295 134512640 135167914 3221224448 3221206204 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 116410 116293 162 162 0 116248 0
[pid=7600] vsize: 465640
Current children cumulated CPU time (s) 204.14
Current children cumulated vsize (Kb) 467768

[startup+220.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 142173 0 0 0 20814 567 0 0 25 0 1 0 1856109734 496529408 121106 4294967295 134512640 135167914 3221224448 3221207100 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 121223 121106 162 162 0 121061 0
[pid=7600] vsize: 484892
Current children cumulated CPU time (s) 213.84
Current children cumulated vsize (Kb) 487020

[startup+230.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 146727 0 0 0 21766 584 0 0 25 0 1 0 1856109734 515182592 125660 4294967295 134512640 135167914 3221224448 3221206764 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 125777 125660 162 162 0 125615 0
[pid=7600] vsize: 503108
Current children cumulated CPU time (s) 223.53
Current children cumulated vsize (Kb) 505236

[startup+240.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 151708 0 0 0 22713 607 0 0 25 0 1 0 1856109734 535584768 130641 4294967295 134512640 135167914 3221224448 3221206256 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 130758 130641 162 162 0 130596 0
[pid=7600] vsize: 523032
Current children cumulated CPU time (s) 233.23
Current children cumulated vsize (Kb) 525160

[startup+250.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 156443 0 0 0 23662 628 0 0 25 0 1 0 1856109734 554979328 135376 4294967295 134512640 135167914 3221224448 3221206492 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 135493 135376 162 162 0 135331 0
[pid=7600] vsize: 541972
Current children cumulated CPU time (s) 242.93
Current children cumulated vsize (Kb) 544100

[startup+260.017 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 161025 0 0 0 24615 650 0 0 25 0 1 0 1856109734 573747200 139958 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 140075 139958 162 162 0 139913 0
[pid=7600] vsize: 560300
Current children cumulated CPU time (s) 252.68
Current children cumulated vsize (Kb) 562428

[startup+270.018 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 165551 0 0 0 25565 672 0 0 25 0 1 0 1856109734 592285696 144484 4294967295 134512640 135167914 3221224448 3221206400 134695619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 144601 144484 162 162 0 144439 0
[pid=7600] vsize: 578404
Current children cumulated CPU time (s) 262.4
Current children cumulated vsize (Kb) 580532

[startup+280.017 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 184881 0 0 0 26483 725 0 0 25 0 1 0 1856109734 782987264 163814 4294967295 134512640 135167914 3221224448 3221206464 134625368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 191159 163821 162 162 0 190997 0
[pid=7600] vsize: 764636
Current children cumulated CPU time (s) 272.11
Current children cumulated vsize (Kb) 766764

[startup+290.018 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 212109 0 0 0 27423 785 0 0 25 0 1 0 1856109734 782987264 191042 4294967295 134512640 135167914 3221224448 3221206448 134625468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 191159 191042 162 162 0 190997 0
[pid=7600] vsize: 764636
Current children cumulated CPU time (s) 282.11
Current children cumulated vsize (Kb) 766764

[startup+300.019 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 213981 0 0 0 28401 796 0 0 25 0 1 0 1856109734 704266240 171823 4294967295 134512640 135167914 3221224448 3221207808 134621050 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 171940 171823 162 162 0 171778 0
[pid=7600] vsize: 687760
Current children cumulated CPU time (s) 292
Current children cumulated vsize (Kb) 689888

[startup+310.019 s]
Raw data (loadavg): 1.00 1.00 0.99 1/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 218803 0 0 0 29351 817 0 0 25 0 1 0 1856109734 724017152 176645 4294967295 134512640 135167914 3221224448 3221206428 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 176762 176645 162 162 0 176600 0
[pid=7600] vsize: 707048
Current children cumulated CPU time (s) 301.71
Current children cumulated vsize (Kb) 709176

[startup+320.02 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 223918 0 0 0 30291 841 0 0 25 0 1 0 1856109734 744968192 181760 4294967295 134512640 135167914 3221224448 3221206268 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 181877 181760 162 162 0 181715 0
[pid=7600] vsize: 727508
Current children cumulated CPU time (s) 311.35
Current children cumulated vsize (Kb) 729636

[startup+330.02 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 229029 0 0 0 31233 865 0 0 25 0 1 0 1856109734 765906944 186871 4294967295 134512640 135167914 3221224448 3221206044 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7600/statm): 186989 186871 162 162 0 186827 0
[pid=7600] vsize: 747956
Current children cumulated CPU time (s) 321.01
Current children cumulated vsize (Kb) 750084

[startup+340.021 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 234056 0 0 0 32178 889 0 0 25 0 1 0 1856109734 786493440 191898 4294967295 134512640 135167914 3221224448 3221207528 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 192015 191898 162 162 0 191853 0
[pid=7600] vsize: 768060
Current children cumulated CPU time (s) 330.7
Current children cumulated vsize (Kb) 770188

[startup+350.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 239107 0 0 0 33123 914 0 0 25 0 1 0 1856109734 807182336 196949 4294967295 134512640 135167914 3221224448 3221206076 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 197066 196949 162 162 0 196904 0
[pid=7600] vsize: 788264
Current children cumulated CPU time (s) 340.4
Current children cumulated vsize (Kb) 790392

[startup+360.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 244151 0 0 0 34067 938 0 0 25 0 1 0 1856109734 827842560 201993 4294967295 134512640 135167914 3221224448 3221206224 134695541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 202110 201993 162 162 0 201948 0
[pid=7600] vsize: 808440
Current children cumulated CPU time (s) 350.08
Current children cumulated vsize (Kb) 810568

[startup+370.023 s]
Raw data (loadavg): 1.07 1.02 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 249263 0 0 0 35009 964 0 0 25 0 1 0 1856109734 848781312 207105 4294967295 134512640 135167914 3221224448 3221206780 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 207222 207105 162 162 0 207060 0
[pid=7600] vsize: 828888
Current children cumulated CPU time (s) 359.76
Current children cumulated vsize (Kb) 831016

[startup+380.022 s]
Raw data (loadavg): 1.06 1.02 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 254377 0 0 0 35947 990 0 0 25 0 1 0 1856109734 869728256 212219 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 212336 212219 162 162 0 212174 0
[pid=7600] vsize: 849344
Current children cumulated CPU time (s) 369.4
Current children cumulated vsize (Kb) 851472

[startup+390.023 s]
Raw data (loadavg): 1.05 1.01 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 259454 0 0 0 36895 1014 0 0 25 0 1 0 1856109734 890523648 217296 4294967295 134512640 135167914 3221224448 3221207196 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 217413 217296 162 162 0 217251 0
[pid=7600] vsize: 869652
Current children cumulated CPU time (s) 379.12
Current children cumulated vsize (Kb) 871780

[startup+400.024 s]
Raw data (loadavg): 1.04 1.01 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) R 7595 7595 19316 0 -1 0 264573 0 0 0 37834 1038 0 0 25 0 1 0 1856109734 911491072 222415 4294967295 134512640 135167914 3221224448 3221206096 134854320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7600/statm): 222532 222415 162 162 0 222370 0
[pid=7600] vsize: 890128
Current children cumulated CPU time (s) 388.75
Current children cumulated vsize (Kb) 892256

[startup+410.024 s]
Raw data (loadavg): 1.04 1.01 0.99 2/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 269591 0 5 0 38769 1062 0 0 25 0 1 0 1856109734 932016128 225937 4294967295 134512640 135167914 3221224448 3221206172 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 227543 225937 162 162 0 227381 0
[pid=7600] vsize: 910172
Current children cumulated CPU time (s) 398.34
Current children cumulated vsize (Kb) 912300



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+414.719 s]
Raw data (loadavg): 1.03 1.01 0.99 1/57 7600
Raw data (/proc/7595/stat): 7595 (minisat+_script) S 7594 7595 19316 0 -1 0 314 375 0 0 0 1 1 1 20 0 1 0 1856109726 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7595/statm): 532 234 485 147 0 385 0
[pid=7595] vsize: 2128
Raw data (/proc/7600/stat): 7600 (minisat+_bignum) T 7595 7595 19316 0 -1 0 271923 0 9 0 39205 1075 0 0 25 0 1 0 1856109734 941543424 227887 4294967295 134512640 135167914 3221224448 3221206220 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7600/statm): 229869 227887 162 162 0 229707 0
[pid=7600] vsize: 919476
Current children cumulated CPU time (s) 402.83
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 415.148
CPU time (s): 403.239
CPU user time (s): 392.059
CPU system time (s): 11.1793
CPU usage (%): 97.1312
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !