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-blp-ic97.opb
MD5SUMa763f1a89c66e69c15e96e7ec1ddc143
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 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 81920000000
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 32392558579027
Number of bits of the biggest sum of numbers45
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables10959
Total number of constraints10724
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)10588
Number of constraints which are nor clauses,nor cardinality constraints136
Minimum length of a constraint1
Maximum length of a constraint9774

Trace number 6292

Launcher Data

LAUNCH ON wulflinc13 THE 2005-09-20 05:30:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3481 boxname=wulflinc13 idbench=1137 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a763f1a89c66e69c15e96e7ec1ddc143  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb
IDLAUNCH: 3481
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        887168 kB
Buffers:         32916 kB
Cached:          86812 kB
SwapCached:        700 kB
Active:          49444 kB
Inactive:        72948 kB
HighTotal:      131008 kB
HighFree:        40236 kB
LowTotal:       903652 kB
LowFree:        846932 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            19376 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:34:46 (client local time) WITH STATUS 0 IN 228.193 SECONDS
stats: 3481 7 228.193 0

Solver Data

c Parsing PB file...
c Converting 932 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 931]---> BDD-cost:    7
c ---[ 930]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:    8
c ---[ 928]---> BDD-cost:    8
c ---[ 927]---> BDD-cost:    7
c ---[ 926]---> BDD-cost:    7
c ---[ 925]---> BDD-cost:    8
c ---[ 924]---> BDD-cost:    7
c ---[ 923]---> BDD-cost:    7
c ---[ 922]---> BDD-cost:    7
c ---[ 921]---> BDD-cost:    7
c ---[ 920]---> BDD-cost:    8
c ---[ 919]---> BDD-cost:    8
c ---[ 918]---> BDD-cost:    7
c ---[ 917]---> BDD-cost:    7
c ---[ 916]---> BDD-cost:    7
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    7
c ---[ 913]---> BDD-cost:    7
c ---[ 912]---> BDD-cost:    7
c ---[ 911]---> BDD-cost:    8
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    8
c ---[ 907]---> BDD-cost:    8
c ---[ 906]---> BDD-cost:    8
c ---[ 905]---> BDD-cost:    7
c ---[ 904]---> BDD-cost:    7
c ---[ 903]---> BDD-cost:    8
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    8
c ---[ 900]---> BDD-cost:    8
c ---[ 899]---> BDD-cost:    8
c ---[ 898]---> BDD-cost:    8
c ---[ 897]---> BDD-cost:    8
c ---[ 896]---> BDD-cost:    8
c ---[ 895]---> BDD-cost:    8
c ---[ 894]---> BDD-cost:    8
c ---[ 893]---> BDD-cost:    7
c ---[ 892]---> BDD-cost:    7
c ---[ 891]---> BDD-cost:    7
c ---[ 890]---> BDD-cost:    7
c ---[ 889]---> BDD-cost:    7
c ---[ 888]---> BDD-cost:    8
c ---[ 887]---> BDD-cost:    8
c ---[ 886]---> BDD-cost:    7
c ---[ 885]---> BDD-cost:    7
c ---[ 884]---> BDD-cost:    7
c ---[ 882]---> BDD-cost: 3755
c ---[ 880]---> Adder-cost: 1658   maxlim: 106240   bits: 17/17
c ---[ 878]---> Adder-cost: 2794   maxlim: 179456   bits: 18/18
c ---[ 876]---> Adder-cost: 2732   maxlim: 175360   bits: 18/18
c ---[ 874]---> Adder-cost: 430   maxlim: 28928   bits: 15/15
c ---[ 872]---> Adder-cost: 220   maxlim: 15360   bits: 14/14
c ---[ 870]---> Adder-cost: 4934   maxlim: 340864   bits: 19/19
c ---[ 868]---> Adder-cost: 2686   maxlim: 176768   bits: 18/18
c ---[ 866]---> Adder-cost: 2688   maxlim: 186496   bits: 18/18
c ---[ 864]---> Adder-cost: 1518   maxlim: 142848   bits: 18/18
c ---[ 862]---> Adder-cost: 1392   maxlim: 159616   bits: 18/18
c ---[ 860]---> Adder-cost: 866   maxlim: 56320   bits: 16/16
c ---[ 858]---> Adder-cost: 682   maxlim: 51328   bits: 16/16
c ---[ 856]---> Adder-cost: 374   maxlim: 24448   bits: 15/15
c ---[ 854]---> Adder-cost: 788   maxlim: 62848   bits: 16/16
c ---[ 852]---> Adder-cost: 1240   maxlim: 104320   bits: 17/17
c ---[ 850]---> Adder-cost: 1634   maxlim: 106752   bits: 17/17
c ---[ 848]---> Adder-cost: 652   maxlim: 47232   bits: 16/16
c ---[ 846]---> Adder-cost: 2186   maxlim: 151424   bits: 18/18
c ---[ 844]---> Adder-cost: 620   maxlim: 44288   bits: 16/16
c ---[ 842]---> Adder-cost: 2500   maxlim: 192768   bits: 18/18
c ---[ 840]---> BDD-cost: 2438
c ---[ 838]---> Adder-cost: 172   maxlim: 15360   bits: 14/14
c ---[ 836]---> Adder-cost: 712   maxlim: 56320   bits: 16/16
c ---[ 834]---> Adder-cost: 1206   maxlim: 122880   bits: 17/17
c ---[ 832]---> Adder-cost: 4018   maxlim: 307968   bits: 19/19
c ---[ 830]---> Adder-cost: 1362   maxlim: 105344   bits: 17/17
c ---[ 828]---> BDD-cost: 1898
c ---[ 826]---> Adder-cost: 3290   maxlim: 272768   bits: 19/19
c ---[ 824]---> BDD-cost: 1637
c ---[ 822]---> Adder-cost: 1202   maxlim: 91264   bits: 17/17
c ---[ 820]---> Adder-cost: 1866   maxlim: 156160   bits: 18/18
c ---[ 818]---> Adder-cost: 2840   maxlim: 260864   bits: 18/18
c ---[ 816]---> Adder-cost: 1130   maxlim: 89600   bits: 17/17
c ---[ 814]---> Adder-cost: 604   maxlim: 44672   bits: 16/16
c ---[ 812]---> Adder-cost: 1424   maxlim: 122880   bits: 17/17
c ---[ 810]---> Adder-cost: 456   maxlim: 34688   bits: 16/16
c ---[ 808]---> Adder-cost: 456   maxlim: 34432   bits: 16/16
c ---[ 806]---> BDD-cost: 1595
c ---[ 804]---> BDD-cost:

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/22626/stat): 22626 (minisat+_script) R 22625 22626 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797824647 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22626/statm): 174 3 169 147 0 27 0
[pid=22626] 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=22627
New process pid=22628
New process pid=22629
execve syscall for /bin/sed executable
One traced child (pid=22628) 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=22629) exited with status: 0
One traced child (pid=22627) exited with status: 0
New process pid=22630
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb

[startup+10.0039 s]
Raw data (loadavg): 0.87 0.94 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 350 0 0 0 988 2 0 0 25 0 1 0 1797824652 1814528 336 4294967295 134512640 135094434 3221224432 3221223300 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 443 336 145 145 0 298 0
[pid=22630] vsize: 1772
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 3896

[startup+20.0046 s]
Raw data (loadavg): 0.89 0.94 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 486 0 0 0 1987 3 0 0 25 0 1 0 1797824652 2686976 469 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 656 469 145 145 0 511 0
[pid=22630] vsize: 2624
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 4748

[startup+30.0052 s]
Raw data (loadavg): 0.90 0.94 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 602 0 0 0 2984 4 0 0 25 0 1 0 1797824652 3129344 585 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 764 585 145 145 0 619 0
[pid=22630] vsize: 3056
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 5180

[startup+40.0059 s]
Raw data (loadavg): 0.92 0.94 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 759 0 0 0 3981 5 0 0 25 0 1 0 1797824652 3698688 670 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 903 670 145 145 0 758 0
[pid=22630] vsize: 3612
Current children cumulated CPU time (s) 39.87
Current children cumulated vsize (Kb) 5736

[startup+50.0065 s]
Raw data (loadavg): 0.93 0.94 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 894 0 0 0 4978 7 0 0 25 0 1 0 1797824652 4251648 805 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1038 805 145 145 0 893 0
[pid=22630] vsize: 4152
Current children cumulated CPU time (s) 49.86
Current children cumulated vsize (Kb) 6276

[startup+60.0072 s]
Raw data (loadavg): 0.94 0.95 0.90 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1092 0 0 0 5974 8 0 0 25 0 1 0 1797824652 5111808 1003 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1248 1003 145 145 0 1103 0
[pid=22630] vsize: 4992
Current children cumulated CPU time (s) 59.83
Current children cumulated vsize (Kb) 7116

[startup+70.0079 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1336 0 0 0 6970 10 0 0 25 0 1 0 1797824652 6049792 1132 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1477 1132 145 145 0 1332 0
[pid=22630] vsize: 5908
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 8032

[startup+80.0095 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1524 0 0 0 7967 11 0 0 25 0 1 0 1797824652 6848512 1270 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1672 1270 145 145 0 1527 0
[pid=22630] vsize: 6688
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 8812

[startup+90.0102 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1761 0 0 0 8963 14 0 0 25 0 1 0 1797824652 7774208 1452 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1898 1452 145 145 0 1753 0
[pid=22630] vsize: 7592
Current children cumulated CPU time (s) 89.78
Current children cumulated vsize (Kb) 9716

[startup+100.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1778 0 0 0 9961 15 0 0 25 0 1 0 1797824652 7864320 1469 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 1920 1469 145 145 0 1775 0
[pid=22630] vsize: 7680
Current children cumulated CPU time (s) 99.77
Current children cumulated vsize (Kb) 9804

[startup+110.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2076 0 0 0 10957 17 0 0 25 0 1 0 1797824652 9150464 1590 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 2234 1590 145 145 0 2089 0
[pid=22630] vsize: 8936
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 11060

[startup+120.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2208 0 0 0 11954 19 0 0 25 0 1 0 1797824652 9711616 1653 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 2371 1653 145 145 0 2226 0
[pid=22630] vsize: 9484
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 11608

[startup+130.014 s]
Raw data (loadavg): 0.98 0.95 0.91 1/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 2381 0 0 0 12951 21 0 0 25 0 1 0 1797824652 10543104 1826 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 2574 1826 145 145 0 2429 0
[pid=22630] vsize: 10296
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 12420

[startup+140.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2560 0 0 0 13948 23 0 0 25 0 1 0 1797824652 11235328 1907 4294967295 134512640 135094434 3221224432 3221223316 134795999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 2743 1907 145 145 0 2598 0
[pid=22630] vsize: 10972
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 13096

[startup+150.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2698 0 0 0 14946 23 0 0 25 0 1 0 1797824652 11866112 1994 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 2897 1994 145 145 0 2752 0
[pid=22630] vsize: 11588
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 13712

[startup+160.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2897 0 0 0 15943 25 0 0 25 0 1 0 1797824652 12603392 2141 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 3077 2141 145 145 0 2932 0
[pid=22630] vsize: 12308
Current children cumulated CPU time (s) 159.69
Current children cumulated vsize (Kb) 14432

[startup+170.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2995 0 0 0 16939 27 0 0 25 0 1 0 1797824652 13037568 2239 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 3183 2239 145 145 0 3038 0
[pid=22630] vsize: 12732
Current children cumulated CPU time (s) 169.67
Current children cumulated vsize (Kb) 14856

[startup+180.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 6182 0 0 0 17923 38 0 0 25 0 1 0 1797824652 23887872 4754 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22630/statm): 5832 4754 145 145 0 5687 0
[pid=22630] vsize: 23328
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 25452

[startup+190.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 42598 0 0 0 18703 169 0 0 20 0 1 0 1797824652 129986560 30663 4294967295 134512640 135094434 3221224432 3220296448 134594941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 31735 30663 145 145 0 31590 0
[pid=22630] vsize: 126940
Current children cumulated CPU time (s) 188.73
Current children cumulated vsize (Kb) 129064

[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 82011 0 0 0 19453 310 0 0 20 0 1 0 1797824652 248225792 59530 4294967295 134512640 135094434 3221224432 3219763644 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 60602 59530 145 145 0 60457 0
[pid=22630] vsize: 242408
Current children cumulated CPU time (s) 197.64
Current children cumulated vsize (Kb) 244532

[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 144101 0 0 0 20149 497 0 0 25 0 1 0 1797824652 502546432 121620 4294967295 134512640 135094434 3221224432 3219758528 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22630/statm): 122692 121620 145 145 0 122547 0
[pid=22630] vsize: 490768
Current children cumulated CPU time (s) 206.47
Current children cumulated vsize (Kb) 492892

[startup+220.021 s]
Raw data (loadavg): 0.99 0.96 0.91 1/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 161743 0 0 0 20955 588 0 0 20 0 1 0 1797824652 488419328 118171 4294967295 134512640 135094434 3221224432 3219773676 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 119243 118171 145 145 0 119098 0
[pid=22630] vsize: 476972
Current children cumulated CPU time (s) 215.44
Current children cumulated vsize (Kb) 479096

[startup+230.022 s]
Raw data (loadavg): 0.99 0.96 0.91 1/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 186307 0 0 0 21690 703 0 0 19 0 1 0 1797824652 589033472 142735 4294967295 134512640 135094434 3221224432 3219755196 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 143807 142735 145 145 0 143662 0
[pid=22630] vsize: 575228
Current children cumulated CPU time (s) 223.94
Current children cumulated vsize (Kb) 577352



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+234.653 s]
Raw data (loadavg): 0.99 0.96 0.91 1/57 22630
Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22626/statm): 531 226 485 147 0 384 0
[pid=22626] vsize: 2124
Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 197574 0 0 0 22034 755 0 0 20 0 1 0 1797824652 980733952 154002 4294967295 134512640 135094434 3221224432 3219767004 134802701 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22630/statm): 239437 154002 145 145 0 239292 0
[pid=22630] vsize: 957748
Current children cumulated CPU time (s) 227.9
Current children cumulated vsize (Kb) 959872

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

Child status: 0
Real time (s): 234.941
CPU time (s): 228.193
CPU user time (s): 220.349
CPU system time (s): 7.84481
CPU usage (%): 97.1279
Max. virtual memory (cumulated for all children) (Kb): 959872

Verifier Data

ERROR: no interpretation found !