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/submitted/manquinho/primes-dimacs-cnf/normalized-par32-3-c.opb
MD5SUMb552ff39062b6c42ea64365c815cbd78
Bench Categoryoptimization, small integers (OPTSMALLINT)
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 2650
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 2650
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2650
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2650
Total number of constraints6619
Number of constraints which are clauses6619
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 34818 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-28 10:57:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24133 boxname=wulflinc24 idbench=207 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b552ff39062b6c42ea64365c815cbd78  /oldhome/oroussel/tmp/wulflinc24/normalized-par32-3-c.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc24/normalized-par32-3-c.opb
IDLAUNCH: 24133
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        713472 kB
Buffers:         36492 kB
Cached:         262956 kB
SwapCached:        636 kB
Active:          18636 kB
Inactive:       282856 kB
HighTotal:      131008 kB
HighFree:        29260 kB
LowTotal:       903652 kB
LowFree:        684212 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5144 kB
Slab:            14076 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 10:59:16 (client local time) WITH STATUS 1 IN 114.311 SECONDS
stats: 24133 7 114.311 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
Raw data (loadavg): 0.90 0.95 0.90 2/54 18597
Raw data (stat): 18597 (runsolver) R 18596 4613 4612 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 864255247 884736 93 4294967295 134512640 135332820 3221224464 3221219360 134799896 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 93 205 205 0 11 0
vsize: 864
Current StackSize limit: 67108864 bytes
[startup+10.0002 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 29137 0 0 0 939 59 0 0 25 0 1 0 864255247 89174016 18203 4294967295 134512640 135726644 3221224592 3220684412 135297992 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 21771 18203 300 300 0 21471 0
vsize: 87084
[startup+20.0005 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 57458 0 0 0 1879 119 0 0 25 0 1 0 864255247 174895104 35570 4294967295 134512640 135726644 3221224592 3221102024 135105699 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 42699 35570 300 300 0 42399 0
vsize: 170796
[startup+30.0015 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 97684 0 0 0 2797 201 0 0 25 0 1 0 864255247 298995712 54122 4294967295 134512640 135726644 3221224592 3220929616 135105730 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 72997 54122 300 300 0 72697 0
vsize: 291988
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 113086 0 0 0 3763 235 0 0 25 0 1 0 864255247 344985600 69302 4294967295 134512640 135726644 3221224592 3220472108 134604437 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 84225 69302 300 300 0 83925 0
vsize: 336900
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 133400 0 0 0 4721 277 0 0 25 0 1 0 864255247 516792320 89365 4294967295 134512640 135726644 3221224592 3221042140 135297998 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 126170 89365 300 300 0 125870 0
vsize: 504680
[startup+60.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 193435 0 0 0 5604 394 0 0 25 0 1 0 864255247 595214336 106316 4294967295 134512640 135726644 3221224592 3220379472 134560113 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 145316 106316 300 300 0 145016 0
vsize: 581264
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 204879 0 0 0 6577 422 0 0 25 0 1 0 864255247 628768768 117556 4294967295 134512640 135726644 3221224592 3221182108 134604449 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 153508 117556 300 300 0 153208 0
vsize: 614032
[startup+80.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 222367 0 0 0 7539 460 0 0 25 0 1 0 864255247 648503296 134818 4294967295 134512640 135726644 3221224592 3220640544 134554546 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 158326 134818 300 300 0 158026 0
vsize: 633304
[startup+90.0055 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 240277 0 0 0 8504 494 0 0 25 0 1 0 864255247 724652032 152520 4294967295 134512640 135726644 3221224592 3220572416 134780348 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 176917 152520 300 300 0 176617 0
vsize: 707668
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 256764 0 0 0 9468 531 0 0 25 0 1 0 864255247 748441600 168816 4294967295 134512640 135726644 3221224592 3220752096 134782648 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 182725 168816 300 300 0 182425 0
vsize: 730900
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 265199 0 0 0 10447 551 0 0 25 0 1 0 864255247 761655296 177154 4294967295 134512640 135726644 3221224592 3221222844 135277555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 185951 177154 300 300 0 185651 0
vsize: 743804
[startup+114.323 s]
Raw data (loadavg): 0.98 0.96 0.91 1/53 18597
Raw data (stat): 18597 (pb2sat) R 18596 4613 4612 0 -1 0 265199 0 0 0 10447 551 0 0 25 0 1 0 864255247 761655296 177154 4294967295 134512640 135726644 3221224592 3221222844 135277555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 185951 177154 300 300 0 185651 0
vsize: 0

Child status: 1
Real time (s): 114.323
CPU time (s): 114.311
CPU user time (s): 108.43
CPU system time (s): 5.8811
CPU usage (%): 99.9894
Max. virtual memory (Kb): 743804
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####