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-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-ship08s.opb
MD5SUM7f0ee4cf0d8dc7a24a6781a6419bf20e
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 71610
Biggest coefficient in the objective function 435455996723200
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 112415039381732472
Number of bits of the sum of numbers in the objective function 57
Biggest number in a constraint 435455996723200
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 112415039381732472
Number of bits of the biggest sum of numbers57
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark23.4694
Number of variables71610
Total number of constraints712
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 constraints712
Minimum length of a constraint30
Maximum length of a constraint1830

Trace number 9939

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-23 16:12:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8679 boxname=wulflinc25 idbench=475 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7f0ee4cf0d8dc7a24a6781a6419bf20e  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-ship08s.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-ship08s.opb
IDLAUNCH: 8679
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.002
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.002
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:        920188 kB
Buffers:         17168 kB
Cached:          77556 kB
SwapCached:          0 kB
Active:          51292 kB
Inactive:        46372 kB
HighTotal:      131008 kB
HighFree:        49504 kB
LowTotal:       903652 kB
LowFree:        870684 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6984 kB
Slab:            11236 kB
Committed_AS:    63660 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-23 16:16:02 (client local time) WITH STATUS 0 IN 220.438 SECONDS
stats: 8679 7 220.438 0

Solver Data

c This solver internally uses Chaff 2004.11.15 Simplified
s UNKNOWN

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/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 18 0 0 0 0 0 0 0 19 0 1 0 21497065 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 373 2 364 364 0 9 0
[pid=7798] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-ship08s.opb

[startup+10.0021 s]
Raw data (loadavg): 0.94 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 2572 0 0 0 991 7 0 0 25 0 1 0 21497065 9641984 1885 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 2354 1885 364 364 0 1990 0
[pid=7798] vsize: 9416
Current children cumulated CPU time (s) 9.98
Current children cumulated vsize (Kb) 9416

[startup+20.0027 s]
Raw data (loadavg): 0.95 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 3893 0 0 0 1989 9 0 0 25 0 1 0 21497065 16400384 3166 4294967295 134512640 135987407 3221224560 3221221296 134892999 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4004 3166 364 364 0 3640 0
[pid=7798] vsize: 16016
Current children cumulated CPU time (s) 19.98
Current children cumulated vsize (Kb) 16016

[startup+30.0033 s]
Raw data (loadavg): 0.95 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 4432 0 0 0 2987 11 0 0 25 0 1 0 21497065 15769600 2992 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 3850 2992 364 364 0 3486 0
[pid=7798] vsize: 15400
Current children cumulated CPU time (s) 29.98
Current children cumulated vsize (Kb) 15400

[startup+40.0039 s]
Raw data (loadavg): 0.96 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 4701 0 0 0 3986 12 0 0 25 0 1 0 21497065 16445440 3257 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4015 3257 364 364 0 3651 0
[pid=7798] vsize: 16060
Current children cumulated CPU time (s) 39.98
Current children cumulated vsize (Kb) 16060

[startup+50.0035 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 4951 0 0 0 4985 13 0 0 25 0 1 0 21497065 17121280 3503 4294967295 134512640 135987407 3221224560 3221221872 134555852 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4180 3503 364 364 0 3816 0
[pid=7798] vsize: 16720
Current children cumulated CPU time (s) 49.98
Current children cumulated vsize (Kb) 16720

[startup+60.0041 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 5177 0 0 0 5984 13 0 0 25 0 1 0 21497065 17661952 3725 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4312 3725 364 364 0 3948 0
[pid=7798] vsize: 17248
Current children cumulated CPU time (s) 59.97
Current children cumulated vsize (Kb) 17248

[startup+70.0037 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 5381 0 0 0 6984 14 0 0 25 0 1 0 21497065 18202624 3926 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4444 3926 364 364 0 4080 0
[pid=7798] vsize: 17776
Current children cumulated CPU time (s) 69.98
Current children cumulated vsize (Kb) 17776

[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 5572 0 0 0 7983 15 0 0 25 0 1 0 21497065 18608128 4114 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4543 4114 364 364 0 4179 0
[pid=7798] vsize: 18172
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 18172

[startup+90.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 5753 0 0 0 8982 16 0 0 25 0 1 0 21497065 19148800 4292 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4675 4292 364 364 0 4311 0
[pid=7798] vsize: 18700
Current children cumulated CPU time (s) 89.98
Current children cumulated vsize (Kb) 18700

[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 5924 0 0 0 9982 16 0 0 25 0 1 0 21497065 19554304 4460 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 4774 4460 364 364 0 4410 0
[pid=7798] vsize: 19096
Current children cumulated CPU time (s) 99.98
Current children cumulated vsize (Kb) 19096

[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 8299 0 0 0 10977 21 0 0 25 0 1 0 21497065 28835840 5357 4294967295 134512640 135987407 3221224560 3221221872 134555870 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 7040 5357 364 364 0 6676 0
[pid=7798] vsize: 28160
Current children cumulated CPU time (s) 109.98
Current children cumulated vsize (Kb) 28160

[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 8358 0 0 0 11976 21 0 0 25 0 1 0 21497065 28835840 5414 4294967295 134512640 135987407 3221224560 3221221904 134612802 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 7040 5414 364 364 0 6676 0
[pid=7798] vsize: 28160
Current children cumulated CPU time (s) 119.97
Current children cumulated vsize (Kb) 28160

[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 8463 0 0 0 12976 21 0 0 25 0 1 0 21497065 28971008 5516 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 7073 5516 364 364 0 6709 0
[pid=7798] vsize: 28292
Current children cumulated CPU time (s) 129.97
Current children cumulated vsize (Kb) 28292

[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 34467 0 0 0 13913 82 0 0 25 0 1 0 21497065 108638208 22797 4294967295 134512640 135987407 3221224560 3220774400 134862209 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 26523 22797 364 364 0 26159 0
[pid=7798] vsize: 106092
Current children cumulated CPU time (s) 139.95
Current children cumulated vsize (Kb) 106092

[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 61519 0 0 0 14850 144 0 0 25 0 1 0 21497065 183648256 38617 4294967295 134512640 135987407 3221224560 3220830304 134887887 0 0 5 16384 0 0 0 17 0 0 0
Raw data (/proc/7798/statm): 44836 38617 364 364 0 44472 0
[pid=7798] vsize: 179344
Current children cumulated CPU time (s) 149.94
Current children cumulated vsize (Kb) 179344

[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 100538 0 0 0 15765 229 0 0 25 0 1 0 21497065 331505664 55430 4294967295 134512640 135987407 3221224560 3221153292 135499903 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 80934 55430 364 364 0 80570 0
[pid=7798] vsize: 323736
Current children cumulated CPU time (s) 159.94
Current children cumulated vsize (Kb) 323736

[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 116826 0 0 0 16731 262 0 0 25 0 1 0 21497065 336101376 71451 4294967295 134512640 135987407 3221224560 3221079696 134865976 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 82056 71451 364 364 0 81692 0
[pid=7798] vsize: 328224
Current children cumulated CPU time (s) 169.93
Current children cumulated vsize (Kb) 328224

[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 160707 0 0 0 17633 356 0 0 25 0 1 0 21497065 666320896 95701 4294967295 134512640 135987407 3221224560 3221171984 134887487 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 162676 95701 364 364 0 162312 0
[pid=7798] vsize: 650704
Current children cumulated CPU time (s) 179.89
Current children cumulated vsize (Kb) 650704

[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 195745 0 0 0 18554 435 0 0 25 0 1 0 21497065 602451968 105960 4294967295 134512640 135987407 3221224560 3221062432 134537483 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 147083 105960 364 364 0 146719 0
[pid=7798] vsize: 588332
Current children cumulated CPU time (s) 189.89
Current children cumulated vsize (Kb) 588332

[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 212090 0 0 0 19515 473 0 0 25 0 1 0 21497065 607858688 122040 4294967295 134512640 135987407 3221224560 3220995188 134641878 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 148403 122040 364 364 0 148039 0
[pid=7798] vsize: 593612
Current children cumulated CPU time (s) 199.88
Current children cumulated vsize (Kb) 593612

[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 227892 0 0 0 20476 512 0 0 25 0 1 0 21497065 612184064 137582 4294967295 134512640 135987407 3221224560 3221221872 134555870 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 149459 137582 364 364 0 149095 0
[pid=7798] vsize: 597836
Current children cumulated CPU time (s) 209.88
Current children cumulated vsize (Kb) 597836

[startup+220.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) R 7797 7798 4004 0 -1 0 241815 0 0 0 21443 545 0 0 25 0 1 0 21497065 669274112 151289 4294967295 134512640 135987407 3221224560 3221221408 134562572 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/7798/statm): 163397 151289 364 364 0 163033 0
[pid=7798] vsize: 653588
Current children cumulated CPU time (s) 219.88
Current children cumulated vsize (Kb) 653588



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+220.159 s]
Raw data (loadavg): 0.99 0.98 0.95 1/55 7798
Raw data (/proc/7798/stat): 7798 (pb2sat) T 7797 7798 4004 0 -1 0 241846 0 0 0 21458 545 0 0 25 0 1 0 21497065 954490880 151319 4294967295 134512640 135987407 3221224560 3220838688 135544035 0 0 5 16384 3222434794 0 0 17 1 0 0
Raw data (/proc/7798/statm): 233030 151319 364 364 0 232666 0
[pid=7798] vsize: 932120
Current children cumulated CPU time (s) 220.03
Current children cumulated vsize (Kb) 932120

Sending SIGTERM to -7798
Sleeping 2 seconds
Sending SIGKILL to -7798
One traced child (pid=7798) ended because it received signal 9 (SIGKILL)
All traced children have exited ! Game is over.

Child ended because it received signal 9 (SIGKILL)
Real time (s): 222.47
CPU time (s): 220.438
CPU user time (s): 214.676
CPU system time (s): 5.76212
CPU usage (%): 99.0867
Max. virtual memory (cumulated for all children) (Kb): 932120

Verifier Data

ERROR: no interpretation found !