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).
  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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-nw04.opb
MD5SUM5a18ff1f45b144b201f1f80233dc9b6b
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 30407
Optimality of the best value was proved NO
Number of terms in the objective function 87482
Biggest coefficient in the objective function 5220
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 120189580
Number of bits of the sum of numbers in the objective function 27
Biggest number in a constraint 5220
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 120189580
Number of bits of the biggest sum of numbers27
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.04
Number of variables87482
Total number of constraints87518
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)87518
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint42032

Trace number 35610 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-05-28 13:28:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24902 boxname=wulflinc13 idbench=1374 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 24902
/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:        681620 kB
Buffers:         36084 kB
Cached:         295548 kB
SwapCached:        548 kB
Active:          34524 kB
Inactive:       299096 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        681340 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5140 kB
Slab:            13628 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:33:39 (client local time) WITH STATUS 1 IN 306.758 SECONDS
stats: 24902 7 306.758 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 1.01 0.97 0.91 1/54 8001
Raw data (stat): 8001 (runsolver) R 8000 1269 1268 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806949925 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 967 0 0 0 994 4 0 0 25 0 1 0 806949925 4980736 829 4294967295 134512640 135726644 3221224592 3221221104 135101181 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 1216 829 300 300 0 916 0
vsize: 4864
[startup+20.0003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 2367 0 0 0 1992 7 0 0 25 0 1 0 806949925 8495104 1688 4294967295 134512640 135726644 3221224592 3221221680 134556195 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2074 1688 300 300 0 1774 0
vsize: 8296
[startup+30 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 3778 0 0 0 2988 11 0 0 25 0 1 0 806949925 13410304 2385 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2385 300 300 0 2974 0
vsize: 13096
[startup+40.0381 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 3927 0 0 0 3991 11 0 0 25 0 1 0 806949925 13545472 2529 4294967295 134512640 135726644 3221224592 3221221680 134556195 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3307 2529 300 300 0 3007 0
vsize: 13228
[startup+50.0383 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 4214 0 0 0 4990 12 0 0 25 0 1 0 806949925 14356480 2811 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3505 2811 300 300 0 3205 0
vsize: 14020
[startup+60.0384 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 4465 0 0 0 5990 13 0 0 25 0 1 0 806949925 14897152 3058 4294967295 134512640 135726644 3221224592 3221221528 135280844 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3637 3058 300 300 0 3337 0
vsize: 14548
[startup+70.0391 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 4692 0 0 0 6989 14 0 0 25 0 1 0 806949925 15572992 3281 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3802 3281 300 300 0 3502 0
vsize: 15208
[startup+80.0402 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 4898 0 0 0 7987 16 0 0 25 0 1 0 806949925 16113664 3484 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3934 3484 300 300 0 3634 0
vsize: 15736
[startup+90.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 5089 0 0 0 8987 16 0 0 25 0 1 0 806949925 16654336 3672 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4066 3672 300 300 0 3766 0
vsize: 16264
[startup+100.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 5270 0 0 0 9987 17 0 0 25 0 1 0 806949925 17059840 3850 4294967295 134512640 135726644 3221224592 3221221648 134851363 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4165 3850 300 300 0 3865 0
vsize: 16660
[startup+110.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 5440 0 0 0 10987 18 0 0 25 0 1 0 806949925 17600512 4017 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4297 4017 300 300 0 3997 0
vsize: 17188
[startup+120.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7472 0 0 0 11985 22 0 0 25 0 1 0 806949925 25403392 4637 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4637 300 300 0 5902 0
vsize: 24808
[startup+130.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7527 0 0 0 12984 22 0 0 25 0 1 0 806949925 25403392 4689 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4689 300 300 0 5902 0
vsize: 24808
[startup+140.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7581 0 0 0 13984 23 0 0 25 0 1 0 806949925 25403392 4741 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4741 300 300 0 5902 0
vsize: 24808
[startup+150.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7644 0 0 0 14984 23 0 0 25 0 1 0 806949925 25403392 4802 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4802 300 300 0 5902 0
vsize: 24808
[startup+160.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7711 0 0 0 15983 24 0 0 25 0 1 0 806949925 25403392 4866 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4866 300 300 0 5902 0
vsize: 24808
[startup+170.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7803 0 0 0 16983 24 0 0 25 0 1 0 806949925 25673728 4956 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6268 4956 300 300 0 5968 0
vsize: 25072
[startup+180.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 7937 0 0 0 17981 26 0 0 25 0 1 0 806949925 25944064 5088 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6334 5088 300 300 0 6034 0
vsize: 25336
[startup+190.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 8065 0 0 0 18981 26 0 0 25 0 1 0 806949925 26349568 5214 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6433 5214 300 300 0 6133 0
vsize: 25732
[startup+200.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 8193 0 0 0 19980 27 0 0 25 0 1 0 806949925 26619904 5340 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6499 5340 300 300 0 6199 0
vsize: 25996
[startup+210.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 8317 0 0 0 20979 28 0 0 25 0 1 0 806949925 27025408 5462 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6598 5462 300 300 0 6298 0
vsize: 26392
[startup+220.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 43214 0 0 0 21906 101 0 0 25 0 1 0 806949925 146104320 30213 4294967295 134512640 135726644 3221224592 3187381308 134604449 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 35670 30213 300 300 0 35370 0
vsize: 142680
[startup+230.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 81610 0 0 0 22828 179 0 0 25 0 1 0 806949925 302477312 58661 4294967295 134512640 135726644 3221224592 3187101976 135280636 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 73847 58661 300 300 0 73547 0
vsize: 295388
[startup+240.071 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 97475 0 0 0 23790 217 0 0 25 0 1 0 806949925 296509440 65038 4294967295 134512640 135726644 3221224592 3191514056 135281263 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 72390 65038 300 300 0 72090 0
vsize: 289560
[startup+250.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 129031 0 0 0 24716 292 0 0 25 0 1 0 806949925 410402816 84068 4294967295 134512640 135726644 3221224592 3208135848 135280675 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 100196 84068 300 300 0 99896 0
vsize: 400784
[startup+260.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 165292 0 0 0 25645 362 0 0 25 0 1 0 806949925 522801152 100715 4294967295 134512640 135726644 3221224592 3218293744 134554579 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127637 100715 300 300 0 127337 0
vsize: 510548
[startup+270.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 185977 0 0 0 26601 407 0 0 25 0 1 0 806949925 736026624 121096 4294967295 134512640 135726644 3221224592 3207246208 134784896 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 179694 121096 300 300 0 179394 0
vsize: 718776
[startup+280.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 225980 0 0 0 27508 500 0 0 25 0 1 0 806949925 667394048 136282 4294967295 134512640 135726644 3221224592 3215101024 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 162938 136282 300 300 0 162638 0
vsize: 651752
[startup+290.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 244213 0 0 0 28461 547 0 0 25 0 1 0 806949925 729739264 154271 4294967295 134512640 135726644 3221224592 3209003436 134603611 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 178159 154271 300 300 0 177859 0
vsize: 712636
[startup+300.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 251057 0 0 0 29447 561 0 0 25 0 1 0 806949925 740040704 160681 4294967295 134512640 135726644 3221224592 3221223056 134732753 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 180674 160681 300 300 0 180374 0
vsize: 722696
[startup+306.747 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 8001
Raw data (stat): 8001 (pb2sat) R 8000 1269 1268 0 -1 0 251057 0 0 0 29447 561 0 0 25 0 1 0 806949925 740040704 160681 4294967295 134512640 135726644 3221224592 3221223056 134732753 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 180674 160681 300 300 0 180374 0
vsize: 0

Child status: 1
Real time (s): 306.747
CPU time (s): 306.758
CPU user time (s): 300.822
CPU system time (s): 5.9361
CPU usage (%): 100.004
Max. virtual memory (Kb): 722696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####