PB'05 competition: run trace

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:

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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb
MD5SUM	c2339539ffa69702e62053614fe34ce1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	44800
Optimality of the best value was proved	NO
Number of terms in the objective function	252
Biggest coefficient in the objective function	2621440
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	35682270
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	2621440
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	35682270
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	24.1133
Number of variables	252
Total number of constraints	19
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	19
Minimum length of a constraint	21
Maximum length of a constraint	80

Trace number 31213

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-05-25 23:23:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22644 boxname=wulflinc13 idbench=1460 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 22644
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        901860 kB
Buffers:         21424 kB
Cached:          91520 kB
SwapCached:        412 kB
Active:          17388 kB
Inactive:        97864 kB
HighTotal:      131008 kB
HighFree:       105336 kB
LowTotal:       903652 kB
LowFree:        796524 kB
SwapTotal:     2097136 kB
SwapFree:      2096060 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5948 kB
Slab:            11972 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:24:16 (client local time) WITH STATUS 30 IN 28.1337 SECONDS
stats: 22644 0 28.1337 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 26 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5719    13584 |    1906       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 69632[0m
c ---[   0]---> Sorter-cost: 6116     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   19981    46877 |    6660       2       15     7.5 |  0.000 % |
c |       104 |   19981    46877 |    7326     104     1142    11.0 |  4.283 % |
c ==============================================================================
c [1mFound solution: 63168[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       187 |   20028    47001 |    6676     187     2186    11.7 |  4.283 % |
c ==============================================================================
c [1mFound solution: 63040[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   20040    47036 |    6680     244     3256    13.3 |  4.283 % |
c |       344 |   20040    47036 |    7348     344     4021    11.7 |  4.288 % |
c |       494 |   20040    47036 |    8082     494     5290    10.7 |  4.288 % |
c |       720 |   20040    47036 |    8891     720     9531    13.2 |  4.288 % |
c ==============================================================================
c [1mFound solution: 62454[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       841 |   20055    47085 |    6685     841    13225    15.7 |  4.288 % |
c |       943 |   20055    47085 |    7353     943    16068    17.0 |  4.296 % |
c ==============================================================================
c [1mFound solution: 59900[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1076 |   20046    47073 |    6682    1074    18047    16.8 |  4.296 % |
c |      1176 |   20046    47073 |    7350    1174    19285    16.4 |  4.396 % |
c |      1326 |   20046    47073 |    8085    1324    27692    20.9 |  4.396 % |
c ==============================================================================
c [1mFound solution: 57622[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1418 |   20072    47141 |    6690    1416    29974    21.2 |  4.396 % |
c |      1518 |   20072    47141 |    7359    1516    31706    20.9 |  4.400 % |
c |      1668 |   20072    47141 |    8094    1666    37067    22.2 |  4.400 % |
c |      1893 |   20043    47079 |    8904    1889    42867    22.7 |  4.530 % |
c |      2230 |   20043    47079 |    9794    2226    53581    24.1 |  4.530 % |
c |      2736 |   20040    47072 |   10774    2657    77254    29.1 |  4.555 % |
c |      3497 |   20040    47072 |   11851    3418   106715    31.2 |  4.555 % |
c |      4637 |   20033    47057 |   13036    4557   137444    30.2 |  4.581 % |
c |      6345 |   20033    47057 |   14340    6265   235328    37.6 |  4.581 % |
c |      8911 |   20033    47057 |   15774    8831   324335    36.7 |  4.581 % |
c ==============================================================================
c [1mFound solution: 57620[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12119 |   20040    47080 |    6680   12038   491447    40.8 |  4.581 % |
c |     12219 |   20040    47080 |    7348    6119   242617    39.6 |  4.615 % |
c |     12372 |   20040    47080 |    8082    6272   246261    39.3 |  4.615 % |
c ==============================================================================
c [1mFound solution: 50172[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12394 |   20086    47198 |    6695    6294   246681    39.2 |  4.615 % |
c |     12494 |   20086    47198 |    7364    6394   249097    39.0 |  4.611 % |
c |     12644 |   20086    47198 |    8100    6544   254240    38.9 |  4.611 % |
c |     12869 |   20086    47198 |    8911    6769   260927    38.5 |  4.611 % |
c |     13206 |   20086    47198 |    9802    7106   271797    38.2 |  4.611 % |
c ==============================================================================
c [1mFound solution: 49620[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13637 |   20096    47227 |    6698    7537   283569    37.6 |  4.611 % |
c |     13739 |   20096    47227 |    7367    3871   118107    30.5 |  4.621 % |
c |     13889 |   20096    47227 |    8104    4021   124612    31.0 |  4.621 % |
c |     14115 |   20096    47227 |    8915    4247   129988    30.6 |  4.621 % |
c |     14452 |   20096    47227 |    9806    4584   138421    30.2 |  4.621 % |
c ==============================================================================
c [1mFound solution: 48640[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |   20107    47256 |    6702    4658   139936    30.0 |  4.621 % |
c |     14627 |   20107    47256 |    7372    4759   142402    29.9 |  4.630 % |
c |     14777 |   20100    47240 |    8109    4908   146510    29.9 |  4.643 % |
c |     15003 |   20100    47240 |    8920    5134   150696    29.4 |  4.643 % |
c |     15340 |   20100    47240 |    9812    5471   156640    28.6 |  4.643 % |
c |     15846 |   20100    47240 |   10793    5977   169252    28.3 |  4.643 % |
c |     16608 |   20100    47240 |   11873    6739   187436    27.8 |  4.643 % |
c ==============================================================================
c [1mFound solution: 46080[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17676 |   20118    47292 |    6706    7806   229462    29.4 |  4.643 % |
c |     17779 |   20118    47292 |    7376    4006    91340    22.8 |  4.672 % |
c |     17929 |   20118    47292 |    8114    4156    94666    22.8 |  4.672 % |
c |     18154 |   20118    47292 |    8925    4381   101775    23.2 |  4.672 % |
c |     18493 |   20118    47292 |    9818    4720   109794    23.3 |  4.672 % |
c |     18999 |   20118    47292 |   10800    5226   127053    24.3 |  4.672 % |
c |     19759 |   20118    47292 |   11880    5986   145165    24.3 |  4.672 % |
c ==============================================================================
c [1mFound solution: 44800[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19805 |   20129    47324 |    6709    6032   146213    24.2 |  4.672 % |
c |     19905 |   20129    47324 |    7379    6132   148197    24.2 |  4.681 % |
c |     20055 |   20129    47324 |    8117    6282   150779    24.0 |  4.681 % |
c |     20281 |   20129    47324 |    8929    6508   155379    23.9 |  4.681 % |
c |     20618 |   20129    47324 |    9822    6845   161306    23.6 |  4.681 % |
c |     21124 |   20129    47324 |   10804    7351   170025    23.1 |  4.681 % |
c |     21883 |   20129    47324 |   11885    8110   184974    22.8 |  4.681 % |
c |     23022 |   19495    45902 |   13073    3587    71348    19.9 |  7.707 % |
c ==============================================================================
c [1mOptimal solution: 44800[0m
s OPTIMUM FOUND
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0
c _______________________________________________________________________________
c 
c restarts              : 58
c conflicts             : 23099          (823 /sec)
c decisions             : 41358          (1474 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 28.0647 s
c _______________________________________________________________________________
#### 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.84 0.94 0.92 2/54 17796
Raw data (stat): 17796 (runsolver) R 17795 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784598318 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.87 0.94 0.92 2/55 17801
Raw data (stat): 17796 (minisat+_script) S 17795 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784598318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9996 s]
Raw data (loadavg): 0.89 0.94 0.92 2/55 17801
Raw data (stat): 17796 (minisat+_script) S 17795 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784598318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+28.1531 s]
Raw data (loadavg): 0.89 0.94 0.92 1/53 17801
Raw data (stat): 17796 (minisat+_script) S 17795 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784598318 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 28.1525
CPU time (s): 28.1337
CPU user time (s): 28.0757
CPU system time (s): 0.057991
CPU usage (%): 99.9332
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	44800
#### END VERIFIER DATA ####