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/MIPLIB/miplib2003/normalized-mps-v2-13-7-momentum3.opb
MD5SUMbdf0df6b57384ca8a37c1ce2e87cfc07
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 67174
Biggest coefficient in the objective function 163840000
Number of bits for the biggest coefficient in the objective function 28
Sum of the numbers in the objective function 1696626095
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1280000000000000115964116992
Number of bits of the biggest number in a constraint 91
Biggest sum of numbers in a constraint 3721289892401349417752330240
Number of bits of the biggest sum of numbers92
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables71194
Total number of constraints70153
Number of constraints which are clauses6081
Number of constraints which are cardinality constraints (but not clauses)7185
Number of constraints which are nor clauses,nor cardinality constraints56887
Minimum length of a constraint1
Maximum length of a constraint814

Trace number 10430

Launcher Data

LAUNCH ON wulflinc4 THE 2005-09-23 18:15:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=9169 boxname=wulflinc4 idbench=965 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bdf0df6b57384ca8a37c1ce2e87cfc07  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb
IDLAUNCH: 9169
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        658176 kB
Buffers:         12948 kB
Cached:         345276 kB
SwapCached:          0 kB
Active:         279568 kB
Inactive:        81556 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        654396 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              20 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:             9700 kB
Committed_AS:    63660 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 18:19:35 (client local time) WITH STATUS 1 IN 222.316 SECONDS
stats: 9169 7 222.316 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc

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/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 18 0 0 0 0 0 0 0 19 0 1 0 22290848 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 373 2 364 364 0 9 0
[pid=10315] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-momentum3.opb

[startup+10.0034 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 2496 0 0 0 992 7 0 0 25 0 1 0 22290848 9367552 1810 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 2287 1810 364 364 0 1923 0
[pid=10315] vsize: 9148
Current children cumulated CPU time (s) 9.99
Current children cumulated vsize (Kb) 9148

[startup+20.0043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4189 0 0 0 1988 11 0 0 25 0 1 0 22290848 15360000 2755 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 3750 2755 364 364 0 3386 0
[pid=10315] vsize: 15000
Current children cumulated CPU time (s) 19.99
Current children cumulated vsize (Kb) 15000

[startup+30.0052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4426 0 0 0 2987 11 0 0 25 0 1 0 22290848 15765504 2986 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 3849 2986 364 364 0 3485 0
[pid=10315] vsize: 15396
Current children cumulated CPU time (s) 29.98
Current children cumulated vsize (Kb) 15396

[startup+40.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4693 0 0 0 3986 12 0 0 25 0 1 0 22290848 16441344 3249 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/10315/statm): 4014 3249 364 364 0 3650 0
[pid=10315] vsize: 16056
Current children cumulated CPU time (s) 39.98
Current children cumulated vsize (Kb) 16056

[startup+50.0069 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 4943 0 0 0 4985 13 0 0 25 0 1 0 22290848 17117184 3495 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4179 3495 364 364 0 3815 0
[pid=10315] vsize: 16716
Current children cumulated CPU time (s) 49.98
Current children cumulated vsize (Kb) 16716

[startup+60.0077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5176 0 0 0 5985 13 0 0 25 0 1 0 22290848 17657856 3724 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4311 3724 364 364 0 3947 0
[pid=10315] vsize: 17244
Current children cumulated CPU time (s) 59.98
Current children cumulated vsize (Kb) 17244

[startup+70.0086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5390 0 0 0 6985 14 0 0 25 0 1 0 22290848 18198528 3935 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4443 3935 364 364 0 4079 0
[pid=10315] vsize: 17772
Current children cumulated CPU time (s) 69.99
Current children cumulated vsize (Kb) 17772

[startup+80.0085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5588 0 0 0 7984 14 0 0 25 0 1 0 22290848 18739200 4129 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4575 4129 364 364 0 4211 0
[pid=10315] vsize: 18300
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 18300

[startup+90.0093 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5775 0 0 0 8983 15 0 0 25 0 1 0 22290848 19279872 4313 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4707 4313 364 364 0 4343 0
[pid=10315] vsize: 18828
Current children cumulated CPU time (s) 89.98
Current children cumulated vsize (Kb) 18828

[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 5949 0 0 0 9983 16 0 0 25 0 1 0 22290848 19685376 4485 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 4806 4485 364 364 0 4442 0
[pid=10315] vsize: 19224
Current children cumulated CPU time (s) 99.99
Current children cumulated vsize (Kb) 19224

[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 8316 0 0 0 10976 22 0 0 25 0 1 0 22290848 28831744 5374 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 7039 5374 364 364 0 6675 0
[pid=10315] vsize: 28156
Current children cumulated CPU time (s) 109.98
Current children cumulated vsize (Kb) 28156

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 17395 0 0 0 11952 44 0 0 25 0 1 0 22290848 56791040 10448 4294967295 134512640 135987407 3221224560 3221222028 134609743 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 13865 10448 364 364 0 13501 0
[pid=10315] vsize: 55460
Current children cumulated CPU time (s) 119.96
Current children cumulated vsize (Kb) 55460

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 44089 0 0 0 12891 103 0 0 25 0 1 0 22290848 137244672 27482 4294967295 134512640 135987407 3221224560 3220978144 134887305 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 33507 27482 364 364 0 33143 0
[pid=10315] vsize: 134028
Current children cumulated CPU time (s) 129.94
Current children cumulated vsize (Kb) 134028

[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 82005 0 0 0 13808 182 0 0 25 0 1 0 22290848 297803776 58546 4294967295 134512640 135987407 3221224560 3220998512 134861431 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 72706 58546 364 364 0 72342 0
[pid=10315] vsize: 290824
Current children cumulated CPU time (s) 139.9
Current children cumulated vsize (Kb) 290824

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 111782 0 0 0 14742 246 0 0 25 0 1 0 22290848 370708480 66610 4294967295 134512640 135987407 3221224560 3221039272 134537317 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 90505 66610 364 364 0 90141 0
[pid=10315] vsize: 362020
Current children cumulated CPU time (s) 149.88
Current children cumulated vsize (Kb) 362020

[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 132597 0 0 0 15698 288 0 0 25 0 1 0 22290848 400445440 87184 4294967295 134512640 135987407 3221224560 3221019808 134887887 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 97765 87184 364 364 0 97401 0
[pid=10315] vsize: 391060
Current children cumulated CPU time (s) 159.86
Current children cumulated vsize (Kb) 391060

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 176762 0 0 0 16608 372 0 0 25 0 1 0 22290848 541097984 111734 4294967295 134512640 135987407 3221224560 3221012368 134537352 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 132104 111734 364 364 0 131740 0
[pid=10315] vsize: 528416
Current children cumulated CPU time (s) 169.8
Current children cumulated vsize (Kb) 528416

[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 216634 0 0 0 17508 471 0 0 25 0 1 0 22290848 695590912 126845 4294967295 134512640 135987407 3221224560 3221030656 134877726 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 169822 126845 364 364 0 169458 0
[pid=10315] vsize: 679288
Current children cumulated CPU time (s) 179.79
Current children cumulated vsize (Kb) 679288

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 235015 0 0 0 18468 509 0 0 25 0 1 0 22290848 720326656 145003 4294967295 134512640 135987407 3221224560 3221024176 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/10315/statm): 175861 145004 364 364 0 175497 0
[pid=10315] vsize: 703444
Current children cumulated CPU time (s) 189.77
Current children cumulated vsize (Kb) 703444

[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 254208 0 0 0 19428 548 0 0 25 0 1 0 22290848 745873408 163965 4294967295 134512640 135987407 3221224560 3220990776 134533885 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/10315/statm): 182098 163965 364 364 0 181734 0
[pid=10315] vsize: 728392
Current children cumulated CPU time (s) 199.76
Current children cumulated vsize (Kb) 728392

[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 269363 0 0 0 20387 580 0 0 25 0 1 0 22290848 817020928 178940 4294967295 134512640 135987407 3221224560 3220994464 134878060 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/10315/statm): 199468 178940 364 364 0 199104 0
[pid=10315] vsize: 797872
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 797872

[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 10315
Raw data (/proc/10315/stat): 10315 (pb2sat) R 10314 10315 4060 0 -1 0 280275 0 0 0 21343 618 0 0 25 0 1 0 22290848 473493504 115135 4294967295 134512640 135987407 3221224560 3221223224 135477314 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10315/statm): 115599 115135 364 364 0 115235 0
[pid=10315] vsize: 462396
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 462396
One traced child (pid=10315) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 222.711
CPU time (s): 222.316
CPU user time (s): 215.884
CPU system time (s): 6.43202
CPU usage (%): 99.8227
Max. virtual memory (cumulated for all children) (Kb): 797872

Verifier Data

ERROR: no interpretation found !