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/miplib3/normalized-mps-v2-13-7-nw04.opb
MD5SUMa5c401bba5afccf02c7b40cb1c595b15
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 benchmark1192.4
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 35677 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-28 13:42:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24965 boxname=wulflinc7 idbench=1437 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 24965
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        665960 kB
Buffers:         34220 kB
Cached:         312616 kB
SwapCached:        644 kB
Active:          34396 kB
Inactive:       314456 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        665708 kB
SwapTotal:     2097136 kB
SwapFree:      2095560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            14124 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:47:40 (client local time) WITH STATUS 1 IN 311.318 SECONDS
stats: 24965 7 311.318 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.00 0.95 0.91 1/54 10522
Raw data (stat): 10522 (runsolver) R 10521 24300 24299 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 807035393 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.0008 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 966 0 0 0 997 2 0 0 25 0 1 0 807035393 4980736 829 4294967295 134512640 135726644 3221224592 3221221088 135280446 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.0009 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 2341 0 0 0 1993 6 0 0 25 0 1 0 807035393 8359936 1663 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2041 1663 300 300 0 1741 0
vsize: 8164
[startup+30.0005 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 2799 0 0 0 2993 6 0 0 25 0 1 0 807035393 9576448 2114 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2338 2114 300 300 0 2038 0
vsize: 9352
[startup+40.0015 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 3895 0 0 0 3990 9 0 0 25 0 1 0 807035393 13410304 2499 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3274 2499 300 300 0 2974 0
vsize: 13096
[startup+50.0019 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 4164 0 0 0 4989 10 0 0 25 0 1 0 807035393 14221312 2763 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3472 2763 300 300 0 3172 0
vsize: 13888
[startup+60.0025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 4413 0 0 0 5989 10 0 0 25 0 1 0 807035393 14761984 3008 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 3008 300 300 0 3304 0
vsize: 14416
[startup+70.0026 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 4642 0 0 0 6988 12 0 0 25 0 1 0 807035393 15437824 3233 4294967295 134512640 135726644 3221224592 3221221680 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3769 3233 300 300 0 3469 0
vsize: 15076
[startup+80.0027 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 4851 0 0 0 7988 12 0 0 25 0 1 0 807035393 15978496 3439 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3901 3439 300 300 0 3601 0
vsize: 15604
[startup+90.0023 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 5045 0 0 0 8987 13 0 0 25 0 1 0 807035393 16519168 3630 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4033 3630 300 300 0 3733 0
vsize: 16132
[startup+100.002 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 5227 0 0 0 9986 13 0 0 25 0 1 0 807035393 16924672 3809 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4132 3809 300 300 0 3832 0
vsize: 16528
[startup+110.003 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 5402 0 0 0 10986 14 0 0 25 0 1 0 807035393 17465344 3981 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4264 3981 300 300 0 3964 0
vsize: 17056
[startup+120.003 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7459 0 0 0 11982 18 0 0 25 0 1 0 807035393 25403392 4625 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4625 300 300 0 5902 0
vsize: 24808
[startup+130.003 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7514 0 0 0 12982 18 0 0 25 0 1 0 807035393 25403392 4678 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4678 300 300 0 5902 0
vsize: 24808
[startup+140.003 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7568 0 0 0 13982 18 0 0 25 0 1 0 807035393 25403392 4729 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4729 300 300 0 5902 0
vsize: 24808
[startup+150.003 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7619 0 0 0 14982 18 0 0 25 0 1 0 807035393 25403392 4778 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4778 300 300 0 5902 0
vsize: 24808
[startup+160.004 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7695 0 0 0 15981 19 0 0 25 0 1 0 807035393 25403392 4852 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4852 300 300 0 5902 0
vsize: 24808
[startup+170.004 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7762 0 0 0 16981 19 0 0 25 0 1 0 807035393 25538560 4917 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4917 300 300 0 5935 0
vsize: 24940
[startup+180.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 7893 0 0 0 17981 19 0 0 25 0 1 0 807035393 25944064 5046 4294967295 134512640 135726644 3221224592 3221221680 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6334 5046 300 300 0 6034 0
vsize: 25336
[startup+190.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 8024 0 0 0 18981 19 0 0 25 0 1 0 807035393 26214400 5174 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6400 5174 300 300 0 6100 0
vsize: 25600
[startup+200.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 8149 0 0 0 19981 20 0 0 25 0 1 0 807035393 26619904 5297 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6499 5297 300 300 0 6199 0
vsize: 25996
[startup+210.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 8273 0 0 0 20981 20 0 0 25 0 1 0 807035393 26890240 5419 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6565 5419 300 300 0 6265 0
vsize: 26260
[startup+220.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 30485 0 0 0 21928 73 0 0 25 0 1 0 807035393 102580224 23698 4294967295 134512640 135726644 3221224592 3187824544 134554700 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 25044 23698 300 300 0 24744 0
vsize: 100176
[startup+230.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 57370 0 0 0 22869 131 0 0 25 0 1 0 807035393 180592640 41130 4294967295 134512640 135726644 3221224592 3186494528 134554799 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 44090 41131 300 300 0 43790 0
vsize: 176360
[startup+240.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 89374 0 0 0 23804 196 0 0 25 0 1 0 807035393 286101504 57084 4294967295 134512640 135726644 3221224592 3219831008 134607571 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 69849 57084 300 300 0 69549 0
vsize: 279396
[startup+250.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 122059 0 0 0 24728 273 0 0 25 0 1 0 807035393 367521792 77179 4294967295 134512640 135726644 3221224592 3190456916 134604404 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 89727 77180 300 300 0 89427 0
vsize: 358908
[startup+260.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 159244 0 0 0 25653 349 0 0 25 0 1 0 807035393 522801152 94780 4294967295 134512640 135726644 3221224592 3201571272 135281786 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127637 94780 300 300 0 127337 0
vsize: 510548
[startup+270.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 173505 0 0 0 26620 381 0 0 25 0 1 0 807035393 522801152 108740 4294967295 134512640 135726644 3221224592 3203564608 134607269 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 127637 108741 300 300 0 127337 0
vsize: 510548
[startup+280.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 216594 0 0 0 27518 483 0 0 25 0 1 0 807035393 653606912 127008 4294967295 134512640 135726644 3221224592 3197783880 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 159572 127008 300 300 0 159272 0
vsize: 638288
[startup+290.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 234846 0 0 0 28472 529 0 0 25 0 1 0 807035393 716627968 145022 4294967295 134512640 135726644 3221224592 3194077272 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 174958 145022 300 300 0 174658 0
vsize: 699832
[startup+300.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 251129 0 0 0 29433 569 0 0 25 0 1 0 807035393 742547456 161096 4294967295 134512640 135726644 3221224592 3209256352 135104037 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 181286 161096 300 300 0 180986 0
vsize: 725144
[startup+310.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 251131 0 0 0 30422 580 0 0 25 0 1 0 807035393 430055424 104556 4294967295 134512640 135726644 3221224592 3221222848 135279084 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 104994 104556 300 300 0 104694 0
vsize: 419976
[startup+311.298 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 10522
Raw data (stat): 10522 (pb2sat) R 10521 24300 24299 0 -1 0 251131 0 0 0 30422 580 0 0 25 0 1 0 807035393 430055424 104556 4294967295 134512640 135726644 3221224592 3221222848 135279084 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 104994 104556 300 300 0 104694 0
vsize: 0

Child status: 1
Real time (s): 311.298
CPU time (s): 311.318
CPU user time (s): 305.301
CPU system time (s): 6.01708
CPU usage (%): 100.006
Max. virtual memory (Kb): 725144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####