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/web/uclid_pb_benchmarks/normalized-cache-ibm-q-full.all.ucl.opb
MD5SUMb8424149645ffb0af409a9e7aef74685
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
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 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 68
Number of bits of the biggest number in a constraint 7
Biggest sum of numbers in a constraint 257
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables81558
Total number of constraints240469
Number of constraints which are clauses235865
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints4604
Minimum length of a constraint1
Maximum length of a constraint13

Trace number 24494 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-10 18:44:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2433 boxname=wulflinc31 idbench=271 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  b8424149645ffb0af409a9e7aef74685  /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-full.all.ucl.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-full.all.ucl.opb
IDLAUNCH: 2433
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        891184 kB
Buffers:         35696 kB
Cached:          79220 kB
SwapCached:       3268 kB
Active:          19956 kB
Inactive:        99744 kB
HighTotal:      131008 kB
HighFree:        88592 kB
LowTotal:       903652 kB
LowFree:        802592 kB
SwapTotal:     2097892 kB
SwapFree:      2093736 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17976 kB
Committed_AS:    63652 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-10 18:49:24 (client local time) WITH STATUS 0 IN 292.719 SECONDS
stats: 2433 7 292.719 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 81558 variables and 240469 constraints.
#### 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
Raw data (loadavg): 0.92 0.98 0.93 2/54 15247
Raw data (stat): 15247 (runsolver) R 15246 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 711502732 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 15372 0 0 0 956 38 0 0 25 0 1 0 711502732 47247360 8160 4294967295 134512640 134714540 3221221776 3221220080 134568040 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11577 8161 1111 63 0 11514 0
vsize: 46140
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 94423 0 0 0 1814 181 0 0 25 0 1 0 711502732 66916352 12952 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16337 12952 1111 63 0 16274 0
vsize: 65348
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 317749 0 0 0 2418 577 0 0 25 0 1 0 711502732 78004224 15641 4294967295 134512640 134714540 3221221776 3221220036 1077378596 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 19083 15648 1111 63 0 19020 0
vsize: 76176
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 546124 0 0 0 3016 980 0 0 25 0 1 0 711502732 87531520 17919 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 21370 17926 1111 63 0 21307 0
vsize: 85480
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 773692 0 0 0 3603 1392 0 0 25 0 1 0 711502732 95682560 19952 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23360 19958 1111 63 0 23297 0
vsize: 93440
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 992882 0 0 0 4191 1805 0 0 25 0 1 0 711502732 103890944 21953 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 25364 21959 1111 63 0 25301 0
vsize: 101456
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 1208520 0 0 0 4798 2198 0 0 25 0 1 0 711502732 110415872 23573 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 26957 23578 1111 63 0 26894 0
vsize: 107828
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 1419938 0 0 0 5411 2586 0 0 25 0 1 0 711502732 116285440 25012 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 28390 25012 1111 63 0 28327 0
vsize: 113560
[startup+90.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 1629267 0 0 0 6018 2979 0 0 25 0 1 0 711502732 122232832 26441 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 29842 26446 1111 63 0 29779 0
vsize: 119368
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 1835648 0 0 0 6627 3369 0 0 25 0 1 0 711502732 128299008 27781 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 31256 27718 1111 63 0 31193 0
vsize: 125292
[startup+110.007 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2041963 0 0 0 7238 3759 0 0 25 0 1 0 711502732 133451776 28998 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 32581 29004 1111 63 0 32518 0
vsize: 130324
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2245391 0 0 0 7848 4149 0 0 25 0 1 0 711502732 138342400 30223 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 33775 30228 1111 63 0 33712 0
vsize: 135100
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2446426 0 0 0 8463 4534 0 0 25 0 1 0 711502732 142831616 31359 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 34796 31288 1111 63 0 34733 0
vsize: 139484
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2647800 0 0 0 9076 4922 0 0 25 0 1 0 711502732 147308544 32445 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 35964 32450 1111 63 0 35901 0
vsize: 143856
[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2846844 0 0 0 9690 5308 0 0 25 0 1 0 711502732 151195648 33411 4294967295 134512640 134714540 3221221776 3221220056 1077378031 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 36993 33413 1111 63 0 36930 0
vsize: 147652
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 2990845 0 0 0 10350 5648 0 0 25 0 1 0 711502732 353366016 84530 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 86271 84536 1111 63 0 86208 0
vsize: 345084
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3192200 0 0 0 10874 6124 0 0 25 0 1 0 711502732 622718976 150285 4294967295 134512640 134714540 3221221776 3221220304 134554857 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 152031 150290 1111 63 0 151968 0
vsize: 608124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3339304 0 0 0 11506 6492 0 0 25 0 1 0 711502732 501805056 120989 4294967295 134512640 134714540 3221221776 3221220184 134543600 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122511 120989 1111 63 0 122448 0
vsize: 490044
[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3467709 0 0 0 12193 6806 0 0 25 0 1 0 711502732 501936128 120994 4294967295 134512640 134714540 3221221776 3221220108 134535956 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122543 120994 1111 63 0 122480 0
vsize: 490172
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3582445 0 0 0 12915 7084 0 0 25 0 1 0 711502732 502919168 121250 4294967295 134512640 134714540 3221221776 3221220528 134630798 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122783 121250 1111 63 0 122720 0
vsize: 491132
[startup+210.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3681400 0 0 0 13677 7322 0 0 25 0 1 0 711502732 522579968 125885 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 127583 125891 1111 63 0 127520 0
vsize: 510332
[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3799923 0 0 0 14389 7610 0 0 25 0 1 0 711502732 511766528 123208 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 124943 123214 1111 63 0 124880 0
vsize: 499772
[startup+230.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 3919277 0 0 0 15101 7898 0 0 25 0 1 0 711502732 505999360 121842 4294967295 134512640 134714540 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 123535 121848 1111 63 0 123472 0
vsize: 494140
[startup+240.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4053353 0 0 0 15776 8224 0 0 25 0 1 0 711502732 502067200 121038 4294967295 134512640 134714540 3221221776 3221220256 134536638 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122575 121038 1111 63 0 122512 0
vsize: 490300
[startup+250.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4176481 0 0 0 16475 8525 0 0 25 0 1 0 711502732 524677120 126566 4294967295 134512640 134714540 3221221776 3221220400 134529003 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 128095 126566 1111 63 0 128032 0
vsize: 512380
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4275127 0 0 0 17239 8760 0 0 25 0 1 0 711502732 522711040 126092 4294967295 134512640 134714540 3221221776 3221220272 134543686 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 127615 126092 1111 63 0 127552 0
vsize: 510460
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4388897 0 0 0 17965 9034 0 0 25 0 1 0 711502732 502202368 121062 4294967295 134512640 134714540 3221221776 3221220140 134539235 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122608 121062 1111 63 0 122545 0
vsize: 490432
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4509313 0 0 0 18679 9321 0 0 25 0 1 0 711502732 599523328 144758 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 146368 144764 1111 63 0 146305 0
vsize: 585472
[startup+290.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4725852 0 0 0 19150 9850 0 0 25 0 1 0 711502732 707792896 171217 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 172801 171223 1111 63 0 172738 0
vsize: 691204
[startup+292.725 s]
Raw data (loadavg): 0.99 0.98 0.93 1/53 15247
Raw data (stat): 15247 (bsolo_mis) R 15246 7876 7672 0 -1 0 4725852 0 0 0 19150 9850 0 0 25 0 1 0 711502732 707792896 171217 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 172801 171223 1111 63 0 172738 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 292.724
CPU time (s): 292.719
CPU user time (s): 192.385
CPU system time (s): 100.334
CPU usage (%): 99.9981
Max. virtual memory (Kb): 691204
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####