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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen3.opb
MD5SUM60f638829868e3a2820fb14a59c3225e
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 31460
Biggest coefficient in the objective function 977797120
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 331425197400
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 977797120
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 331425197400
Number of bits of the biggest sum of numbers39
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.311952
Number of variables36360
Total number of constraints1503
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 constraints1503
Minimum length of a constraint40
Maximum length of a constraint4060

Trace number 35428 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-28 13:10:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24736 boxname=wulflinc15 idbench=1208 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  60f638829868e3a2820fb14a59c3225e  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-degen3.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-degen3.opb
IDLAUNCH: 24736
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        746640 kB
Buffers:         33724 kB
Cached:         231348 kB
SwapCached:        604 kB
Active:          67864 kB
Inactive:       199328 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        746388 kB
SwapTotal:     2097136 kB
SwapFree:      2095616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5120 kB
Slab:            15212 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:12:42 (client local time) WITH STATUS 1 IN 128.532 SECONDS
stats: 24736 7 128.532 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): 0.91 0.95 0.90 2/54 3677
Raw data (stat): 3677 (runsolver) R 3676 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806829007 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): 0.93 0.95 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 2193 0 0 0 994 5 0 0 25 0 1 0 806829007 8089600 1518 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1975 1518 300 300 0 1675 0
vsize: 7900
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 2695 0 0 0 1993 6 0 0 25 0 1 0 806829007 9306112 2012 4294967295 134512640 135726644 3221224576 3221221408 134541893 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2272 2012 300 300 0 1972 0
vsize: 9088
[startup+30.003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 32616 0 0 0 2926 72 0 0 25 0 1 0 806829007 107945984 21451 4294967295 134512640 135726644 3221224576 3209442000 134780348 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 26354 21451 300 300 0 26054 0
vsize: 105416
[startup+40.005 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 60032 0 0 0 3870 129 0 0 25 0 1 0 806829007 193634304 37658 4294967295 134512640 135726644 3221224576 3209095432 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 47274 37658 300 300 0 46974 0
vsize: 189096
[startup+50.0055 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 86783 0 0 0 4822 177 0 0 25 0 1 0 806829007 260714496 54505 4294967295 134512640 135726644 3221224576 3208755056 134558304 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 63651 54505 300 300 0 63351 0
vsize: 254604
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 115612 0 0 0 5760 239 0 0 25 0 1 0 806829007 364875776 70802 4294967295 134512640 135726644 3221224576 3209999820 134603714 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 89081 70802 300 300 0 88781 0
vsize: 356324
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 157502 0 0 0 6686 314 0 0 25 0 1 0 806829007 570068992 111504 4294967295 134512640 135726644 3221224576 3209740508 135280490 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 139177 111504 300 300 0 138877 0
vsize: 556708
[startup+80.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 169347 0 0 0 7659 340 0 0 25 0 1 0 806829007 502956032 104713 4294967295 134512640 135726644 3221224576 3209697292 134604449 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 122792 104713 300 300 0 122492 0
vsize: 491168
[startup+90.0069 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 207161 0 0 0 8581 419 0 0 25 0 1 0 806829007 645824512 117746 4294967295 134512640 135726644 3221224576 3209669200 134780348 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 157672 117746 300 300 0 157372 0
vsize: 630688
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 225438 0 0 0 9543 457 0 0 25 0 1 0 806829007 673533952 135814 4294967295 134512640 135726644 3221224576 3208844152 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 164437 135815 300 300 0 164137 0
vsize: 657748
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 245411 0 0 0 10501 500 0 0 25 0 1 0 806829007 703135744 155561 4294967295 134512640 135726644 3221224576 3209826572 135287606 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 171664 155562 300 300 0 171364 0
vsize: 686656
[startup+120.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 260951 0 0 0 11472 529 0 0 25 0 1 0 806829007 776040448 170923 4294967295 134512640 135726644 3221224576 3208970552 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 189463 170923 300 300 0 189163 0
vsize: 757852
[startup+128.533 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 3677
Raw data (stat): 3677 (pb2sat) R 3676 23514 23513 0 -1 0 260951 0 0 0 11472 529 0 0 25 0 1 0 806829007 776040448 170923 4294967295 134512640 135726644 3221224576 3208970552 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 189463 170923 300 300 0 189163 0
vsize: 0

Child status: 1
Real time (s): 128.532
CPU time (s): 128.532
CPU user time (s): 122.88
CPU system time (s): 5.65214
CPU usage (%): 100
Max. virtual memory (Kb): 757852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####