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-scorpion.opb
MD5SUMd78b2a3709ef5514ef5552f6badb37ec
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 8460
Biggest coefficient in the objective function 10788957847552
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 603693086370759
Number of bits of the sum of numbers in the objective function 50
Biggest number in a constraint 33554432000000
Number of bits of the biggest number in a constraint 45
Biggest sum of numbers in a constraint 603693086370759
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables10740
Total number of constraints388
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 constraints388
Minimum length of a constraint30
Maximum length of a constraint600

Trace number 2635

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901724 kB
Buffers:         35908 kB
Cached:          69440 kB
SwapCached:        868 kB
Active:          69460 kB
Inactive:        38464 kB
HighTotal:      131008 kB
HighFree:        58884 kB
LowTotal:       903652 kB
LowFree:        842840 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19312 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:37:30 (client local time) WITH STATUS 139 IN 362.832 SECONDS
stats: 2805 7 362.832 139

Solver Data

c Parsing PB file...
c Converting 602 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 631]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 629]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 627]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 625]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 623]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 621]---> Adder-cost: 942   maxlim: 164416716600   bits: 38/38
c ---[ 619]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 617]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 615]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 613]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 611]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 609]---> Adder-cost: 930   maxlim: 137573171000   bits: 38/38
c ---[ 607]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 605]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 603]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 601]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 599]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 597]---> Adder-cost: 886   maxlim: 83047219000   bits: 37/37
c ---[ 595]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 593]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 591]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 589]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 587]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 585]---> Adder-cost: 948   maxlim: 187904819000   bits: 38/38
c ---[ 583]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 581]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 579]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 577]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 575]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 573]---> Adder-cost: 966   maxlim: 107374182300   bits: 38/37
c ---[ 571]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 569]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 567]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 565]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 563]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 561]---> Adder-cost: 1116   maxlim: 107374182300   bits: 38/37
c ---[ 559]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 557]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 555]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 553]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 551]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 549]---> Sorter-cost: 6393     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 547]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 545]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 543]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 541]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 539]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 537]---> Adder-cost: 956   maxlim: 322122546900   bits: 39/39
c ---[ 535]---> Adder-cost: 300   maxlim: 3221225469   bits: 33/32
c ---[ 533]---> Adder-cost: 300/oldhome/oroussel/solvers/minisat+_script: line 9: 26988 Segmentation fault      $XDIR/minisat+_64-bit_static -try "$@"

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/26984/stat): 26984 (minisat+_script) R 26983 26984 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844165388 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26984/statm): 174 3 169 147 0 27 0
[pid=26984] 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=26985
New process pid=26986
New process pid=26987
execve syscall for /bin/sed executable
One traced child (pid=26986) 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=26987) exited with status: 0
One traced child (pid=26985) exited with status: 0
New process pid=26988
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-scorpion.opb

[startup+10.0073 s]
Raw data (loadavg): 0.77 0.88 0.88 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1456 0 0 0 981 6 0 0 25 0 1 0 1844165393 6397952 1380 4294967295 134512640 135094434 3221224432 3221219872 134601016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26988/statm): 1562 1380 145 145 0 1417 0
[pid=26988] vsize: 6248
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 8372

[startup+20.0089 s]
Raw data (loadavg): 0.80 0.88 0.88 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1473 0 0 0 1981 6 0 0 25 0 1 0 1844165393 6430720 1397 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1570 1397 145 145 0 1425 0
[pid=26988] vsize: 6280
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 8404

[startup+30.0096 s]
Raw data (loadavg): 0.83 0.89 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1502 0 0 0 2981 6 0 0 25 0 1 0 1844165393 6574080 1394 4294967295 134512640 135094434 3221224432 3221220812 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1605 1394 145 145 0 1460 0
[pid=26988] vsize: 6420
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 8544

[startup+40.0103 s]
Raw data (loadavg): 0.86 0.89 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1676 0 0 0 3980 7 0 0 25 0 1 0 1844165393 6811648 1462 4294967295 134512640 135094434 3221224432 3221220208 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1663 1462 145 145 0 1518 0
[pid=26988] vsize: 6652
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 8776

[startup+50.011 s]
Raw data (loadavg): 0.88 0.89 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1812 0 0 0 4980 7 0 0 25 0 1 0 1844165393 6909952 1501 4294967295 134512640 135094434 3221224432 3221218816 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1687 1501 145 145 0 1542 0
[pid=26988] vsize: 6748
Current children cumulated CPU time (s) 49.87
Current children cumulated vsize (Kb) 8872

[startup+60.0107 s]
Raw data (loadavg): 0.90 0.90 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1899 0 0 0 5979 8 0 0 25 0 1 0 1844165393 6971392 1524 4294967295 134512640 135094434 3221224432 3221219344 134600116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1702 1524 145 145 0 1557 0
[pid=26988] vsize: 6808
Current children cumulated CPU time (s) 59.87
Current children cumulated vsize (Kb) 8932

[startup+70.0114 s]
Raw data (loadavg): 0.91 0.90 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 1988 0 0 0 6979 8 0 0 25 0 1 0 1844165393 7036928 1549 4294967295 134512640 135094434 3221224432 3221219792 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1718 1549 145 145 0 1573 0
[pid=26988] vsize: 6872
Current children cumulated CPU time (s) 69.87
Current children cumulated vsize (Kb) 8996

[startup+80.012 s]
Raw data (loadavg): 0.93 0.90 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2078 0 0 0 7978 9 0 0 25 0 1 0 1844165393 7495680 1575 4294967295 134512640 135094434 3221224432 3221221984 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1830 1575 145 145 0 1685 0
[pid=26988] vsize: 7320
Current children cumulated CPU time (s) 79.87
Current children cumulated vsize (Kb) 9444

[startup+90.0127 s]
Raw data (loadavg): 0.94 0.90 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2173 0 0 0 8978 9 0 0 25 0 1 0 1844165393 7577600 1605 4294967295 134512640 135094434 3221224432 3221221984 134600191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1850 1605 145 145 0 1705 0
[pid=26988] vsize: 7400
Current children cumulated CPU time (s) 89.87
Current children cumulated vsize (Kb) 9524

[startup+100.013 s]
Raw data (loadavg): 0.95 0.91 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2474 0 0 0 9977 10 0 0 25 0 1 0 1844165393 8015872 1727 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1957 1727 145 145 0 1812 0
[pid=26988] vsize: 7828
Current children cumulated CPU time (s) 99.87
Current children cumulated vsize (Kb) 9952

[startup+110.013 s]
Raw data (loadavg): 0.95 0.91 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2648 0 0 0 10976 10 0 0 25 0 1 0 1844165393 8097792 1757 4294967295 134512640 135094434 3221224432 3221217936 134600354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1977 1757 145 145 0 1832 0
[pid=26988] vsize: 7908
Current children cumulated CPU time (s) 109.86
Current children cumulated vsize (Kb) 10032

[startup+120.014 s]
Raw data (loadavg): 0.96 0.91 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2648 0 0 0 11976 10 0 0 25 0 1 0 1844165393 8097792 1757 4294967295 134512640 135094434 3221224432 3221220400 134600283 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1977 1757 145 145 0 1832 0
[pid=26988] vsize: 7908
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 10032

[startup+130.014 s]
Raw data (loadavg): 0.97 0.91 0.89 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2783 0 0 0 12975 11 0 0 25 0 1 0 1844165393 8159232 1780 4294967295 134512640 135094434 3221224432 3221219872 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1992 1780 145 145 0 1847 0
[pid=26988] vsize: 7968
Current children cumulated CPU time (s) 129.86
Current children cumulated vsize (Kb) 10092

[startup+140.015 s]
Raw data (loadavg): 0.97 0.92 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2783 0 0 0 13975 11 0 0 25 0 1 0 1844165393 8159232 1780 4294967295 134512640 135094434 3221224432 3221222052 134783044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 1992 1780 145 145 0 1847 0
[pid=26988] vsize: 7968
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 10092

[startup+150.016 s]
Raw data (loadavg): 0.97 0.92 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 2909 0 0 0 14975 12 0 0 25 0 1 0 1844165393 8196096 1794 4294967295 134512640 135094434 3221224432 3221220272 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2001 1794 145 145 0 1856 0
[pid=26988] vsize: 8004
Current children cumulated CPU time (s) 149.87
Current children cumulated vsize (Kb) 10128

[startup+160.017 s]
Raw data (loadavg): 0.98 0.92 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3035 0 0 0 15974 12 0 0 25 0 1 0 1844165393 8237056 1809 4294967295 134512640 135094434 3221224432 3221219520 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2011 1809 145 145 0 1866 0
[pid=26988] vsize: 8044
Current children cumulated CPU time (s) 159.86
Current children cumulated vsize (Kb) 10168

[startup+170.017 s]
Raw data (loadavg): 0.98 0.92 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3035 0 0 0 16975 12 0 0 25 0 1 0 1844165393 8237056 1809 4294967295 134512640 135094434 3221224432 3221221632 134600144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2011 1809 145 145 0 1866 0
[pid=26988] vsize: 8044
Current children cumulated CPU time (s) 169.87
Current children cumulated vsize (Kb) 10168

[startup+180.017 s]
Raw data (loadavg): 0.98 0.92 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3160 0 0 0 17974 13 0 0 25 0 1 0 1844165393 8273920 1823 4294967295 134512640 135094434 3221224432 3221219168 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2020 1823 145 145 0 1875 0
[pid=26988] vsize: 8080
Current children cumulated CPU time (s) 179.87
Current children cumulated vsize (Kb) 10204

[startup+190.019 s]
Raw data (loadavg): 0.99 0.93 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3285 0 0 0 18973 13 0 0 25 0 1 0 1844165393 8310784 1837 4294967295 134512640 135094434 3221224432 3221218560 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2029 1837 145 145 0 1884 0
[pid=26988] vsize: 8116
Current children cumulated CPU time (s) 189.86
Current children cumulated vsize (Kb) 10240

[startup+200.019 s]
Raw data (loadavg): 0.99 0.93 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3285 0 0 0 19973 13 0 0 25 0 1 0 1844165393 8310784 1837 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2029 1837 145 145 0 1884 0
[pid=26988] vsize: 8116
Current children cumulated CPU time (s) 199.86
Current children cumulated vsize (Kb) 10240

[startup+210.019 s]
Raw data (loadavg): 0.99 0.93 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3421 0 0 0 20973 14 0 0 25 0 1 0 1844165393 8351744 1852 4294967295 134512640 135094434 3221224432 3221219396 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2039 1852 145 145 0 1894 0
[pid=26988] vsize: 8156
Current children cumulated CPU time (s) 209.87
Current children cumulated vsize (Kb) 10280

[startup+220.02 s]
Raw data (loadavg): 0.99 0.93 0.90 3/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3421 0 0 0 21973 14 0 0 25 0 1 0 1844165393 8351744 1852 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2039 1852 145 145 0 1894 0
[pid=26988] vsize: 8156
Current children cumulated CPU time (s) 219.87
Current children cumulated vsize (Kb) 10280

[startup+230.02 s]
Raw data (loadavg): 0.99 0.93 0.90 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3571 0 0 0 22972 14 0 0 25 0 1 0 1844165393 8425472 1881 4294967295 134512640 135094434 3221224432 3221219616 134677007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2057 1881 145 145 0 1912 0
[pid=26988] vsize: 8228
Current children cumulated CPU time (s) 229.86
Current children cumulated vsize (Kb) 10352

[startup+240.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3571 0 0 0 23972 14 0 0 25 0 1 0 1844165393 8425472 1881 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2057 1881 145 145 0 1912 0
[pid=26988] vsize: 8228
Current children cumulated CPU time (s) 239.86
Current children cumulated vsize (Kb) 10352

[startup+250.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3707 0 0 0 24972 14 0 0 25 0 1 0 1844165393 8462336 1896 4294967295 134512640 135094434 3221224432 3221219520 134600354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2066 1896 145 145 0 1921 0
[pid=26988] vsize: 8264
Current children cumulated CPU time (s) 249.86
Current children cumulated vsize (Kb) 10388

[startup+260.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3707 0 0 0 25972 15 0 0 25 0 1 0 1844165393 8462336 1896 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2066 1896 145 145 0 1921 0
[pid=26988] vsize: 8264
Current children cumulated CPU time (s) 259.87
Current children cumulated vsize (Kb) 10388

[startup+270.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3843 0 0 0 26971 15 0 0 25 0 1 0 1844165393 9289728 1911 4294967295 134512640 135094434 3221224432 3221219152 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2268 1911 145 145 0 2123 0
[pid=26988] vsize: 9072
Current children cumulated CPU time (s) 269.86
Current children cumulated vsize (Kb) 11196

[startup+280.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3843 0 0 0 27971 15 0 0 25 0 1 0 1844165393 9289728 1911 4294967295 134512640 135094434 3221224432 3221221696 134677086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2268 1911 145 145 0 2123 0
[pid=26988] vsize: 9072
Current children cumulated CPU time (s) 279.86
Current children cumulated vsize (Kb) 11196

[startup+290.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3979 0 0 0 28970 16 0 0 25 0 1 0 1844165393 9326592 1926 4294967295 134512640 135094434 3221224432 3221218816 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2277 1926 145 145 0 2132 0
[pid=26988] vsize: 9108
Current children cumulated CPU time (s) 289.86
Current children cumulated vsize (Kb) 11232

[startup+300.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 3979 0 0 0 29971 16 0 0 25 0 1 0 1844165393 9326592 1926 4294967295 134512640 135094434 3221224432 3221221280 134600151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2277 1926 145 145 0 2132 0
[pid=26988] vsize: 9108
Current children cumulated CPU time (s) 299.87
Current children cumulated vsize (Kb) 11232

[startup+310.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 4114 0 0 0 30971 16 0 0 25 0 1 0 1844165393 9363456 1940 4294967295 134512640 135094434 3221224432 3221219872 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2286 1940 145 145 0 2141 0
[pid=26988] vsize: 9144
Current children cumulated CPU time (s) 309.87
Current children cumulated vsize (Kb) 11268

[startup+320.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 4114 0 0 0 31971 16 0 0 25 0 1 0 1844165393 9363456 1940 4294967295 134512640 135094434 3221224432 3221220048 134601148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2286 1940 145 145 0 2141 0
[pid=26988] vsize: 9144
Current children cumulated CPU time (s) 319.87
Current children cumulated vsize (Kb) 11268

[startup+330.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 4158 0 0 0 32971 16 0 0 25 0 1 0 1844165393 9494528 1984 4294967295 134512640 135094434 3221224432 3221219168 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2318 1984 145 145 0 2173 0
[pid=26988] vsize: 9272
Current children cumulated CPU time (s) 329.87
Current children cumulated vsize (Kb) 11396

[startup+340.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 4742 0 0 0 33968 19 0 0 25 0 1 0 1844165393 10899456 2403 4294967295 134512640 135094434 3221224432 3221220224 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2661 2403 145 145 0 2516 0
[pid=26988] vsize: 10644
Current children cumulated CPU time (s) 339.87
Current children cumulated vsize (Kb) 12768

[startup+350.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 4953 0 0 0 34966 20 0 0 25 0 1 0 1844165393 11063296 2486 4294967295 134512640 135094434 3221224432 3221218992 134676480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26988/statm): 2701 2486 145 145 0 2556 0
[pid=26988] vsize: 10804
Current children cumulated CPU time (s) 349.86
Current children cumulated vsize (Kb) 12928

[startup+360.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 26988
Raw data (/proc/26984/stat): 26984 (minisat+_script) S 26983 26984 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844165388 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26984/statm): 531 226 485 147 0 384 0
[pid=26984] vsize: 2124
Raw data (/proc/26988/stat): 26988 (minisat+_64-bit) R 26984 26984 16528 0 -1 0 87430 0 0 0 35783 203 0 0 25 0 1 0 1844165393 548147200 84898 4294967295 134512640 135094434 3221224432 3221222576 134605136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26988/statm): 133825 84898 145 145 0 133680 0
[pid=26988] vsize: 535300
Current children cumulated CPU time (s) 359.86
Current children cumulated vsize (Kb) 537424
One traced child (pid=26988) ended because it received signal 11 (SIGSEGV)
One traced child (pid=26984) exited with status: 139
All traced children have exited ! Game is over.

Child status: 139
Real time (s): 362.98
CPU time (s): 362.832
CPU user time (s): 359.453
CPU system time (s): 3.37849
CPU usage (%): 99.9591
Max. virtual memory (cumulated for all children) (Kb): 537424

Verifier Data

ERROR: no interpretation found !