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-scfxm2.opb
MD5SUM3611fc20088602fa99726273d52175c6
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 920
Biggest coefficient in the objective function 5242880
Number of bits for the biggest coefficient in the objective function 23
Sum of the numbers in the objective function 274726650
Number of bits of the sum of numbers in the objective function 29
Biggest number in a constraint 52428800000
Number of bits of the biggest number in a constraint 36
Biggest sum of numbers in a constraint 319170501375
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.631903
Number of variables18280
Total number of constraints660
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 constraints660
Minimum length of a constraint20
Maximum length of a constraint1140

Trace number 42731 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-16 14:12:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=25948 boxname=wulflinc3 idbench=1248 idsolver=18 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3611fc20088602fa99726273d52175c6  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-scfxm2.opb
REAL COMMAND:  pb2sat-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-scfxm2.opb
IDLAUNCH: 25948
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        744332 kB
Buffers:         13708 kB
Cached:         254240 kB
SwapCached:        788 kB
Active:          32728 kB
Inactive:       237364 kB
HighTotal:      131008 kB
HighFree:         7784 kB
LowTotal:       903652 kB
LowFree:        736548 kB
SwapTotal:     2097136 kB
SwapFree:      2095372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            14420 kB
Committed_AS:    71892 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-16 14:14:14 (client local time) WITH STATUS 1 IN 113.67 SECONDS
stats: 25948 7 113.67 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.84 0.92 0.90 2/54 24396
Raw data (stat): 24396 (runsolver) R 24395 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 971379004 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.001 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 27655 0 0 0 940 58 0 0 25 0 1 0 971379004 86663168 16759 4294967295 134512640 135730672 3221224576 3221089984 134546483 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 21158 16759 301 301 0 20857 0
vsize: 84632
[startup+20.0013 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 54746 0 0 0 1882 116 0 0 25 0 1 0 971379004 170872832 32650 4294967295 134512640 135730672 3221224576 3221096944 134770727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 41717 32650 301 301 0 41416 0
vsize: 166868
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 94811 0 0 0 2806 192 0 0 25 0 1 0 971379004 297074688 50540 4294967295 134512640 135730672 3221224576 3221096568 134787727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 72528 50540 301 301 0 72227 0
vsize: 290112
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 108258 0 0 0 3781 218 0 0 25 0 1 0 971379004 338063360 63777 4294967295 134512640 135730672 3221224576 3221104832 134770759 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 82535 63777 301 301 0 82234 0
vsize: 330140
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 127431 0 0 0 4747 251 0 0 25 0 1 0 971379004 365645824 82728 4294967295 134512640 135730672 3221224576 3221097872 134546483 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 89269 82729 301 301 0 88968 0
vsize: 357076
[startup+60.003 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 185766 0 0 0 5643 355 0 0 25 0 1 0 971379004 695070720 121513 4294967295 134512640 135730672 3221224576 3221107744 134788521 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 169695 121517 301 301 0 169394 0
vsize: 678780
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 199537 0 0 0 6610 389 0 0 25 0 1 0 971379004 627957760 110525 4294967295 134512640 135730672 3221224576 3221112592 135288378 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 153310 110526 301 301 0 153009 0
vsize: 613240
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 213770 0 0 0 7585 414 0 0 25 0 1 0 971379004 635932672 124540 4294967295 134512640 135730672 3221224576 3221105000 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 155257 124541 301 301 0 154956 0
vsize: 621028
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 232739 0 0 0 8552 447 0 0 25 0 1 0 971379004 663248896 143288 4294967295 134512640 135730672 3221224576 3221115592 134787727 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 161926 143288 301 301 0 161625 0
vsize: 647704
[startup+100.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 248058 0 0 0 9522 477 0 0 25 0 1 0 971379004 735625216 158429 4294967295 134512640 135730672 3221224576 3221118456 135285983 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 179596 158430 301 301 0 179295 0
vsize: 718384
[startup+110.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 263461 0 0 0 10497 503 0 0 25 0 1 0 971379004 758710272 173654 4294967295 134512640 135730672 3221224576 3221222656 135284078 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 185232 173654 301 301 0 184931 0
vsize: 740928
[startup+113.675 s]
Raw data (loadavg): 0.97 0.94 0.91 1/53 24396
Raw data (stat): 24396 (pb2sat-v2) R 24395 20224 20223 0 -1 0 263461 0 0 0 10497 503 0 0 25 0 1 0 971379004 758710272 173654 4294967295 134512640 135730672 3221224576 3221222656 135284078 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 185232 173654 301 301 0 184931 0
vsize: 0

Child status: 1
Real time (s): 113.674
CPU time (s): 113.67
CPU user time (s): 108.281
CPU system time (s): 5.38918
CPU usage (%): 99.9958
Max. virtual memory (Kb): 740928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####