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).
    Note that some very long lines in this section may be truncated by your web browser !
  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

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-czprob.opb
MD5SUMcfa1bf2f1dd2df0f424e37a2971f8ba1
Bench Categoryoptimization, big integers (OPTBIGINT)
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 65500
Biggest coefficient in the objective function 16110321664000
Number of bits for the biggest coefficient in the objective function 44
Sum of the numbers in the objective function 32674140101032650
Number of bits of the sum of numbers in the objective function 55
Biggest number in a constraint 16110321664000
Number of bits of the biggest number in a constraint 44
Biggest sum of numbers in a constraint 32674140101032650
Number of bits of the biggest sum of numbers55
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables65880
Total number of constraints927
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 constraints927
Minimum length of a constraint20
Maximum length of a constraint7460

Trace number 10280

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-23 17:44:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=9007 boxname=wulflinc27 idbench=803 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cfa1bf2f1dd2df0f424e37a2971f8ba1  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-czprob.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-czprob.opb
IDLAUNCH: 9007
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.039
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	: 3
cpu MHz		: 451.039
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:        929008 kB
Buffers:         12036 kB
Cached:          76160 kB
SwapCached:          0 kB
Active:          51432 kB
Inactive:        39736 kB
HighTotal:      131008 kB
HighFree:        50372 kB
LowTotal:       903652 kB
LowFree:        878636 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6984 kB
Slab:             8864 kB
Committed_AS:    63624 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 17:47:34 (client local time) WITH STATUS 1 IN 211.891 SECONDS
stats: 9007 7 211.891 1

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22045555 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 373 2 364 364 0 9 0
[pid=10178] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-czprob.opb

[startup+10.0024 s]
Raw data (loadavg): 0.92 0.95 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 2547 0 0 0 993 5 0 0 25 0 1 0 22045555 9596928 1862 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 2343 1862 364 364 0 1979 0
[pid=10178] vsize: 9372
Current children cumulated CPU time (s) 9.98
Current children cumulated vsize (Kb) 9372

[startup+20.0032 s]
Raw data (loadavg): 0.93 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 3081 0 0 0 1990 8 0 0 25 0 1 0 22045555 10948608 2387 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 2673 2387 364 364 0 2309 0
[pid=10178] vsize: 10692
Current children cumulated CPU time (s) 19.98
Current children cumulated vsize (Kb) 10692

[startup+30.0041 s]
Raw data (loadavg): 0.94 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 4474 0 0 0 2988 10 0 0 25 0 1 0 22045555 15994880 3035 4294967295 134512640 135987407 3221224560 3221221728 134566692 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 3905 3035 364 364 0 3541 0
[pid=10178] vsize: 15620
Current children cumulated CPU time (s) 29.98
Current children cumulated vsize (Kb) 15620

[startup+40.0049 s]
Raw data (loadavg): 0.95 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 4753 0 0 0 3987 11 0 0 25 0 1 0 22045555 16670720 3309 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4070 3309 364 364 0 3706 0
[pid=10178] vsize: 16280
Current children cumulated CPU time (s) 39.98
Current children cumulated vsize (Kb) 16280

[startup+50.0047 s]
Raw data (loadavg): 0.96 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5003 0 0 0 4986 12 0 0 25 0 1 0 22045555 17346560 3555 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4235 3555 364 364 0 3871 0
[pid=10178] vsize: 16940
Current children cumulated CPU time (s) 49.98
Current children cumulated vsize (Kb) 16940

[startup+60.0055 s]
Raw data (loadavg): 0.96 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5228 0 0 0 5986 12 0 0 25 0 1 0 22045555 17887232 3776 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4367 3776 364 364 0 4003 0
[pid=10178] vsize: 17468
Current children cumulated CPU time (s) 59.98
Current children cumulated vsize (Kb) 17468

[startup+70.0054 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5432 0 0 0 6985 13 0 0 25 0 1 0 22045555 18427904 3977 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4499 3977 364 364 0 4135 0
[pid=10178] vsize: 17996
Current children cumulated CPU time (s) 69.98
Current children cumulated vsize (Kb) 17996

[startup+80.0062 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5621 0 0 0 7984 14 0 0 25 0 1 0 22045555 18968576 4163 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4631 4163 364 364 0 4267 0
[pid=10178] vsize: 18524
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 18524

[startup+90.006 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5800 0 0 0 8983 15 0 0 25 0 1 0 22045555 19374080 4339 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4730 4339 364 364 0 4366 0
[pid=10178] vsize: 18920
Current children cumulated CPU time (s) 89.98
Current children cumulated vsize (Kb) 18920

[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 5969 0 0 0 9983 15 0 0 25 0 1 0 22045555 19779584 4505 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 4829 4505 364 364 0 4465 0
[pid=10178] vsize: 19316
Current children cumulated CPU time (s) 99.98
Current children cumulated vsize (Kb) 19316

[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 9625 0 0 0 10974 23 0 0 25 0 1 0 22045555 33607680 6628 4294967295 134512640 135987407 3221224560 3220044208 134856487 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 8205 6628 364 364 0 7841 0
[pid=10178] vsize: 32820
Current children cumulated CPU time (s) 109.97
Current children cumulated vsize (Kb) 32820

[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 44574 0 0 0 11897 96 0 0 25 0 1 0 22045555 145379328 28012 4294967295 134512640 135987407 3221224560 3220083804 135500008 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 35493 28012 364 364 0 35129 0
[pid=10178] vsize: 141972
Current children cumulated CPU time (s) 119.93
Current children cumulated vsize (Kb) 141972

[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 70691 0 0 0 12839 151 0 0 25 0 1 0 22045555 217194496 47757 4294967295 134512640 135987407 3221224560 3220043852 135480718 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 53026 47757 364 364 0 52662 0
[pid=10178] vsize: 212104
Current children cumulated CPU time (s) 129.9
Current children cumulated vsize (Kb) 212104

[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 112955 0 0 0 13748 239 0 0 25 0 1 0 22045555 380866560 67823 4294967295 134512640 135987407 3221224560 3220121776 134877628 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 92985 67823 364 364 0 92621 0
[pid=10178] vsize: 371940
Current children cumulated CPU time (s) 139.87
Current children cumulated vsize (Kb) 371940

[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 131614 0 0 0 14709 276 0 0 25 0 1 0 22045555 405602304 86260 4294967295 134512640 135987407 3221224560 3220070048 134866017 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 99024 86260 364 364 0 98660 0
[pid=10178] vsize: 396096
Current children cumulated CPU time (s) 149.85
Current children cumulated vsize (Kb) 396096

[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 175962 0 0 0 15620 359 0 0 25 0 1 0 22045555 547332096 110995 4294967295 134512640 135987407 3221224560 3220074444 135482112 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 133626 110995 364 364 0 133262 0
[pid=10178] vsize: 534504
Current children cumulated CPU time (s) 159.79
Current children cumulated vsize (Kb) 534504

[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 217339 0 0 0 16533 444 0 0 25 0 1 0 22045555 670568448 127594 4294967295 134512640 135987407 3221224560 3220112272 134887793 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 163713 127594 364 364 0 163349 0
[pid=10178] vsize: 654852
Current children cumulated CPU time (s) 169.77
Current children cumulated vsize (Kb) 654852

[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 234297 0 0 0 17498 476 0 0 25 0 1 0 22045555 726966272 144351 4294967295 134512640 135987407 3221224560 3220166780 134892452 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 177482 144351 364 364 0 177118 0
[pid=10178] vsize: 709928
Current children cumulated CPU time (s) 179.74
Current children cumulated vsize (Kb) 709928

[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 253688 0 0 0 18458 514 0 0 25 0 1 0 22045555 752513024 163510 4294967295 134512640 135987407 3221224560 3220096356 135477872 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 183719 163510 364 364 0 183355 0
[pid=10178] vsize: 734876
Current children cumulated CPU time (s) 189.72
Current children cumulated vsize (Kb) 734876

[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 269084 0 0 0 19427 543 0 0 25 0 1 0 22045555 822984704 178721 4294967295 134512640 135987407 3221224560 3220167664 134537491 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 200924 178721 364 364 0 200560 0
[pid=10178] vsize: 803696
Current children cumulated CPU time (s) 199.7
Current children cumulated vsize (Kb) 803696

[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 10178
Raw data (/proc/10178/stat): 10178 (pb2sat) R 10177 10178 4005 0 -1 0 283208 0 0 0 20398 569 0 0 25 0 1 0 22045555 841801728 192424 4294967295 134512640 135987407 3221224560 3221223424 134795939 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/10178/statm): 205518 192424 364 364 0 205154 0
[pid=10178] vsize: 822072
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 822072
One traced child (pid=10178) exited with status: 1
All traced children have exited ! Game is over.

Child status: 1
Real time (s): 212.22
CPU time (s): 211.891
CPU user time (s): 205.797
CPU system time (s): 6.09407
CPU usage (%): 99.8449
Max. virtual memory (cumulated for all children) (Kb): 822072

Verifier Data

ERROR: no interpretation found !