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-ship12s.opb
MD5SUM8b36f38cb0ceb42bd2113a818ef52485
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 82890
Biggest coefficient in the objective function 1511023181824000
Number of bits for the biggest coefficient in the objective function 51
Sum of the numbers in the objective function 204819735955723812
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 1511023181824000
Number of bits of the biggest number in a constraint 51
Biggest sum of numbers in a constraint 204819735955723812
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark18.0513
Number of variables82890
Total number of constraints1042
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 constraints1042
Minimum length of a constraint30
Maximum length of a constraint1470

Trace number 9947

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-23 16:12:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=8681 boxname=wulflinc11 idbench=477 idsolver=8 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8b36f38cb0ceb42bd2113a818ef52485  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-ship12s.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-ship12s.opb
IDLAUNCH: 8681
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.045
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	: 2
cpu MHz		: 451.045
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:        902000 kB
Buffers:          8860 kB
Cached:          98240 kB
SwapCached:          0 kB
Active:          63648 kB
Inactive:        52984 kB
HighTotal:      131008 kB
HighFree:        30436 kB
LowTotal:       903652 kB
LowFree:        871564 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6980 kB
Slab:            10296 kB
Committed_AS:    63624 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-23 16:16:57 (client local time) WITH STATUS 0 IN 267.579 SECONDS
stats: 8681 7 267.579 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/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21533794 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 373 2 364 364 0 9 0
[pid=9377] vsize: 1492
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-ship12s.opb

[startup+10.0015 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 2544 0 0 0 993 5 0 0 25 0 1 0 21533794 9506816 1857 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 2321 1857 364 364 0 1957 0
[pid=9377] vsize: 9284
Current children cumulated CPU time (s) 9.98
Current children cumulated vsize (Kb) 9284

[startup+20.0023 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 3055 0 0 0 1992 6 0 0 25 0 1 0 21533794 10858496 2360 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 2651 2360 364 364 0 2287 0
[pid=9377] vsize: 10604
Current children cumulated CPU time (s) 19.98
Current children cumulated vsize (Kb) 10604

[startup+30.0021 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 4428 0 0 0 2989 9 0 0 25 0 1 0 21533794 15769600 2988 4294967295 134512640 135987407 3221224560 3221221872 134555852 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 3850 2988 364 364 0 3486 0
[pid=9377] vsize: 15400
Current children cumulated CPU time (s) 29.98
Current children cumulated vsize (Kb) 15400

[startup+40.0029 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 4700 0 0 0 3988 10 0 0 25 0 1 0 21533794 16445440 3256 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4015 3256 364 364 0 3651 0
[pid=9377] vsize: 16060
Current children cumulated CPU time (s) 39.98
Current children cumulated vsize (Kb) 16060

[startup+50.0037 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 4951 0 0 0 4987 11 0 0 25 0 1 0 21533794 17121280 3503 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4180 3503 364 364 0 3816 0
[pid=9377] vsize: 16720
Current children cumulated CPU time (s) 49.98
Current children cumulated vsize (Kb) 16720

[startup+60.0034 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 5182 0 0 0 5987 11 0 0 25 0 1 0 21533794 17661952 3730 4294967295 134512640 135987407 3221224560 3221221872 134555852 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4312 3730 364 364 0 3948 0
[pid=9377] vsize: 17248
Current children cumulated CPU time (s) 59.98
Current children cumulated vsize (Kb) 17248

[startup+70.0042 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 5390 0 0 0 6987 11 0 0 25 0 1 0 21533794 18202624 3934 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4444 3934 364 364 0 4080 0
[pid=9377] vsize: 17776
Current children cumulated CPU time (s) 69.98
Current children cumulated vsize (Kb) 17776

[startup+80.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 5583 0 0 0 7986 12 0 0 25 0 1 0 21533794 18743296 4124 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4576 4124 364 364 0 4212 0
[pid=9377] vsize: 18304
Current children cumulated CPU time (s) 79.98
Current children cumulated vsize (Kb) 18304

[startup+90.0058 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 5762 0 0 0 8986 13 0 0 25 0 1 0 21533794 19148800 4300 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4675 4300 364 364 0 4311 0
[pid=9377] vsize: 18700
Current children cumulated CPU time (s) 89.99
Current children cumulated vsize (Kb) 18700

[startup+100.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 5933 0 0 0 9985 13 0 0 25 0 1 0 21533794 19554304 4469 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 4774 4469 364 364 0 4410 0
[pid=9377] vsize: 19096
Current children cumulated CPU time (s) 99.98
Current children cumulated vsize (Kb) 19096

[startup+110.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8302 0 0 0 10980 18 0 0 25 0 1 0 21533794 28835840 5360 4294967295 134512640 135987407 3221224560 3221221792 134534618 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7040 5360 364 364 0 6676 0
[pid=9377] vsize: 28160
Current children cumulated CPU time (s) 109.98
Current children cumulated vsize (Kb) 28160

[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8359 0 0 0 11980 18 0 0 25 0 1 0 21533794 28835840 5415 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7040 5415 364 364 0 6676 0
[pid=9377] vsize: 28160
Current children cumulated CPU time (s) 119.98
Current children cumulated vsize (Kb) 28160

[startup+130.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8468 0 0 0 12980 18 0 0 25 0 1 0 21533794 28971008 5521 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7073 5521 364 364 0 6709 0
[pid=9377] vsize: 28292
Current children cumulated CPU time (s) 129.98
Current children cumulated vsize (Kb) 28292

[startup+140.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8594 0 0 0 13979 19 0 0 25 0 1 0 21533794 29241344 5645 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7139 5645 364 364 0 6775 0
[pid=9377] vsize: 28556
Current children cumulated CPU time (s) 139.98
Current children cumulated vsize (Kb) 28556

[startup+150.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8716 0 0 0 14979 19 0 0 25 0 1 0 21533794 29646848 5765 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7238 5765 364 364 0 6874 0
[pid=9377] vsize: 28952
Current children cumulated CPU time (s) 149.98
Current children cumulated vsize (Kb) 28952

[startup+160.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8836 0 0 0 15978 20 0 0 25 0 1 0 21533794 29917184 5882 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7304 5882 364 364 0 6940 0
[pid=9377] vsize: 29216
Current children cumulated CPU time (s) 159.98
Current children cumulated vsize (Kb) 29216

[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 8952 0 0 0 16977 21 0 0 25 0 1 0 21533794 30187520 5996 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7370 5996 364 364 0 7006 0
[pid=9377] vsize: 29480
Current children cumulated CPU time (s) 169.98
Current children cumulated vsize (Kb) 29480

[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 9070 0 0 0 17977 21 0 0 25 0 1 0 21533794 30457856 6112 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 7436 6112 364 364 0 7072 0
[pid=9377] vsize: 29744
Current children cumulated CPU time (s) 179.98
Current children cumulated vsize (Kb) 29744

[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 40854 0 0 0 18908 86 0 0 25 0 1 0 21533794 134258688 24314 4294967295 134512640 135987407 3221224560 3221176972 134636980 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 32778 24314 364 364 0 32414 0
[pid=9377] vsize: 131112
Current children cumulated CPU time (s) 189.94
Current children cumulated vsize (Kb) 131112

[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 63773 0 0 0 19859 135 0 0 25 0 1 0 21533794 255078400 40800 4294967295 134512640 135987407 3221224560 3221158652 135499906 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 62275 40800 364 364 0 61911 0
[pid=9377] vsize: 249100
Current children cumulated CPU time (s) 199.94
Current children cumulated vsize (Kb) 249100

[startup+210.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 101994 0 0 0 20775 217 0 0 25 0 1 0 21533794 329601024 56844 4294967295 134512640 135987407 3221224560 3221073292 135499901 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 80469 56844 364 364 0 80105 0
[pid=9377] vsize: 321876
Current children cumulated CPU time (s) 209.92
Current children cumulated vsize (Kb) 321876

[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 119118 0 0 0 21732 259 0 0 25 0 1 0 21533794 336629760 73694 4294967295 134512640 135987407 3221224560 3220807108 134559711 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 82185 73694 364 364 0 81821 0
[pid=9377] vsize: 328740
Current children cumulated CPU time (s) 219.91
Current children cumulated vsize (Kb) 328740

[startup+230.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 183483 0 0 0 22597 390 0 0 25 0 1 0 21533794 563748864 93886 4294967295 134512640 135987407 3221224560 3221172536 135486713 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 137634 93886 364 364 0 137270 0
[pid=9377] vsize: 550536
Current children cumulated CPU time (s) 229.87
Current children cumulated vsize (Kb) 550536

[startup+240.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 197900 0 0 0 23562 425 0 0 25 0 1 0 21533794 600952832 108064 4294967295 134512640 135987407 3221224560 3221082964 134559697 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 146717 108064 364 364 0 146353 0
[pid=9377] vsize: 586868
Current children cumulated CPU time (s) 239.87
Current children cumulated vsize (Kb) 586868

[startup+250.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 214056 0 0 0 24523 464 0 0 25 0 1 0 21533794 604872704 123949 4294967295 134512640 135987407 3221224560 3220983116 134635332 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 147674 123949 364 364 0 147310 0
[pid=9377] vsize: 590696
Current children cumulated CPU time (s) 249.87
Current children cumulated vsize (Kb) 590696

[startup+260.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) R 9376 9377 4060 0 -1 0 228486 0 0 0 25489 497 0 0 25 0 1 0 21533794 660205568 138146 4294967295 134512640 135987407 3221224560 3221129776 134877726 0 0 5 16384 0 0 0 17 1 0 0
Raw data (/proc/9377/statm): 161183 138146 364 364 0 160819 0
[pid=9377] vsize: 644732
Current children cumulated CPU time (s) 259.86
Current children cumulated vsize (Kb) 644732



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+267.314 s]
Raw data (loadavg): 0.99 0.96 0.91 1/55 9377
Raw data (/proc/9377/stat): 9377 (pb2sat) T 9376 9377 4060 0 -1 0 240581 0 0 0 26187 528 0 0 25 0 1 0 21533794 951640064 150054 4294967295 134512640 135987407 3221224560 3221076912 135544035 0 0 5 16384 3222434794 0 0 17 1 0 0
Raw data (/proc/9377/statm): 232334 150054 364 364 0 231970 0
[pid=9377] vsize: 929336
Current children cumulated CPU time (s) 267.15
Current children cumulated vsize (Kb) 929336

Sending SIGTERM to -9377
Sleeping 2 seconds
Sending SIGKILL to -9377
One traced child (pid=9377) 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): 269.624
CPU time (s): 267.579
CPU user time (s): 261.986
CPU system time (s): 5.59315
CPU usage (%): 99.2415
Max. virtual memory (cumulated for all children) (Kb): 929336

Verifier Data

ERROR: no interpretation found !