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/submitted/manquinho/primes-dimacs-cnf/normalized-jnh209.opb
MD5SUM	ad3e64e9cdbd56e02705ba9162b58982
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	93
Optimality of the best value was proved	NO
Number of terms in the objective function	200
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	200
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	200
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.137978
Number of variables	200
Total number of constraints	900
Number of constraints which are clauses	900
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	11

Trace number 40734

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-08 20:42:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=28798 boxname=wulflinc3 idbench=184 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  ad3e64e9cdbd56e02705ba9162b58982  /oldhome/oroussel/tmp/wulflinc3/normalized-jnh209.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-jnh209.opb
IDLAUNCH: 28798
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        740288 kB
Buffers:         26744 kB
Cached:         247576 kB
SwapCached:        808 kB
Active:          43328 kB
Inactive:       233112 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        740036 kB
SwapTotal:     2097136 kB
SwapFree:      2095332 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5012 kB
Slab:            12176 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-08 20:47:03 (client local time) WITH STATUS 30 IN 300.377 SECONDS
stats: 28798 0 300.377 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c Initial problem consists of 200 variables and 900 constraints.
c After prepocess the problem consists of 198 variables and 886 constraints.
c preprocess terminated 0.472 s
c Initial Lower Bound: 71
c Lower Bound Elapsed time: 0.97
c Not use computed LB before first solution.
c NEW SOLUTION FOUND: 100 @ 1.54
c NEW SOLUTION FOUND: 99 @ 1.54
c NEW SOLUTION FOUND: 98 @ 1.545
c NEW SOLUTION FOUND: 97 @ 1.611
c NEW SOLUTION FOUND: 96 @ 1.807
c NEW SOLUTION FOUND: 95 @ 1.984
c NEW SOLUTION FOUND: 94 @ 2.539
c NEW SOLUTION FOUND: 93 @ 58.26
s OPTIMUM FOUND
v -x1 x2 x3 -x4 -x5 x6 -x7 x8 -x9 x10 -x11 x12 x13 -x14 -x15 x16 x17 -x18 -x19 x20 -x21 x22 -x23 x24 -x25 x26 x27 -x28 -x29 x30 -x31 x32 -x33 x34 -x35 x36 x37 -x38 -x39 x40 -x41 x42 -x43 x44 -x45 x46 x47 -x48 -x49 x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 -x61 x62 -x63 x64 -x65 x66 x67 -x68 -x69 x70 -x71 x72 -x73 x74 x75 -x76 x77 -x78 -x79 x80 -x81 x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 -x91 x92 -x93 -x94 -x95 x96 x97 -x98 x99 -x100 -x101 x102 x103 -x104 x105 -x106 x107 -x108 -x109 x110 -x111 -x112 -x113 x114 -x115 x116 x117 -x118 x119 -x120 -x121 x122 -x123 -x124 x125 -x126 x127 -x128 -x129 x130 x131 -x132 -x133 -x134 -x135 x136 x137 -x138 -x139 -x140 -x141 x142 -x143 x144 x145 -x146 -x147 x148 x149 -x150 x151 -x152 x153 -x154 -x155 x156 x157 -x158 x159 -x160 -x161 x162 -x163 x164 x165 -x166 x167 -x168 -x169 x170 x171 -x172 -x173 x174 x175 -x176 x177 -x178 -x179 x180 x181 -x182 x183 -x184 -x185 x186 x187 -x188 x189 -x190 -x191 -x192 -x193 -x194 x195 -x196 x197 -x198 x199 -x200 
c Exit Code: 30
c Total time: 300.365 s
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.97 0.93 2/54 30045
Raw data (stat): 30045 (runsolver) R 30044 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 904588831 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 4125 0 0 0 986 12 0 0 25 0 1 0 904588831 7421952 1071 4294967295 134512640 134716908 3221224576 3221220848 1074799138 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 1812 1071 1111 63 0 1749 0
vsize: 7248
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 8245 0 0 0 1972 26 0 0 25 0 1 0 904588831 7614464 1124 4294967295 134512640 134716908 3221224576 3221220720 1074969688 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 1859 1124 1111 63 0 1796 0
vsize: 7436
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 12480 0 0 0 2958 40 0 0 25 0 1 0 904588831 7880704 1188 4294967295 134512640 134716908 3221224576 3221222828 1077781665 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 1924 1188 1111 63 0 1861 0
vsize: 7696
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 16350 0 0 0 3949 49 0 0 25 0 1 0 904588831 8491008 1296 4294967295 134512640 134716908 3221224576 3221220380 1074787813 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2073 1296 1111 63 0 2010 0
vsize: 8292
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 20496 0 0 0 4937 61 0 0 25 0 1 0 904588831 8466432 1363 4294967295 134512640 134716908 3221224576 3221221768 1074138297 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2113 1366 1111 63 0 2050 0
vsize: 8268
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 25307 0 0 0 5925 73 0 0 25 0 1 0 904588831 8794112 1405 4294967295 134512640 134716908 3221224576 3221220720 1074969467 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 2147 1405 1111 63 0 2084 0
vsize: 8588
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 31050 0 0 0 6908 90 0 0 25 0 1 0 904588831 8765440 1461 4294967295 134512640 134716908 3221224576 3221223268 134528601 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2140 1461 1111 63 0 2077 0
vsize: 8560
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 34950 0 0 0 7898 100 0 0 25 0 1 0 904588831 8847360 1484 4294967295 134512640 134716908 3221224576 3221222856 1074138271 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2160 1484 1111 63 0 2097 0
vsize: 8640
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 38765 0 0 0 8888 110 0 0 25 0 1 0 904588831 9420800 1579 4294967295 134512640 134716908 3221224576 3221220508 1074788177 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2300 1579 1111 63 0 2237 0
vsize: 9200
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 42487 0 0 0 9880 118 0 0 25 0 1 0 904588831 8908800 1509 4294967295 134512640 134716908 3221224576 3221222928 1074153782 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2175 1509 1111 63 0 2112 0
vsize: 8700
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 46224 0 0 0 10871 128 0 0 25 0 1 0 904588831 9826304 1658 4294967295 134512640 134716908 3221224576 3221220804 1075115039 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2399 1658 1111 63 0 2336 0
vsize: 9596
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 50035 0 0 0 11861 138 0 0 25 0 1 0 904588831 9207808 1582 4294967295 134512640 134716908 3221224576 3221222536 1074138297 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2283 1583 1111 63 0 2220 0
vsize: 8992
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 53575 0 0 0 12852 147 0 0 25 0 1 0 904588831 9170944 1573 4294967295 134512640 134716908 3221224576 3221222600 1077380373 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2239 1573 1111 63 0 2176 0
vsize: 8956
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 58206 0 0 0 13840 159 0 0 25 0 1 0 904588831 9248768 1592 4294967295 134512640 134716908 3221224576 3221222928 1074153786 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2258 1592 1111 63 0 2195 0
vsize: 9032
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 62791 0 0 0 14829 170 0 0 25 0 1 0 904588831 10412032 1802 4294967295 134512640 134716908 3221224576 3221220784 1074815247 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2542 1802 1111 63 0 2479 0
vsize: 10168
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 67186 0 0 0 15819 181 0 0 25 0 1 0 904588831 9994240 1758 4294967295 134512640 134716908 3221224576 3221221720 1074138271 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2525 1759 1111 63 0 2462 0
vsize: 9760
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 71436 0 0 0 16807 192 0 0 25 0 1 0 904588831 10416128 1743 4294967295 134512640 134716908 3221224576 3221220756 1075114960 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2543 1743 1111 63 0 2480 0
vsize: 10172
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 74962 0 0 0 17799 200 0 0 25 0 1 0 904588831 9785344 1712 4294967295 134512640 134716908 3221224576 3221222576 1074918594 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2389 1712 1111 63 0 2326 0
vsize: 9556
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 79026 0 0 0 18790 210 0 0 25 0 1 0 904588831 9965568 1767 4294967295 134512640 134716908 3221224576 3221222576 1074918597 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2433 1767 1111 63 0 2370 0
vsize: 9732
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 83037 0 0 0 19780 220 0 0 25 0 1 0 904588831 9969664 1768 4294967295 134512640 134716908 3221224576 3221222848 1074153782 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2434 1768 1111 63 0 2371 0
vsize: 9736
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 86759 0 0 0 20771 230 0 0 25 0 1 0 904588831 11030528 1963 4294967295 134512640 134716908 3221224576 3221220544 1074872799 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2693 1963 1111 63 0 2630 0
vsize: 10772
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 89543 0 0 0 21765 236 0 0 25 0 1 0 904588831 10121216 1805 4294967295 134512640 134716908 3221224576 3221222848 1074153786 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2471 1805 1111 63 0 2408 0
vsize: 9884
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 93007 0 0 0 22757 244 0 0 25 0 1 0 904588831 10780672 1811 4294967295 134512640 134716908 3221224576 3221221104 1075120005 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2632 1811 1111 63 0 2569 0
vsize: 10528
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 96936 0 0 0 23746 255 0 0 25 0 1 0 904588831 10518528 1858 4294967295 134512640 134716908 3221224576 3221223216 134651068 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2568 1858 1111 63 0 2505 0
vsize: 10272
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 100524 0 0 0 24735 266 0 0 25 0 1 0 904588831 11018240 1943 4294967295 134512640 134716908 3221224576 3221220460 1074788143 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2690 1943 1111 63 0 2627 0
vsize: 10760
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 103759 0 0 0 25727 275 0 0 25 0 1 0 904588831 10252288 1805 4294967295 134512640 134716908 3221224576 3221222688 1074867340 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2503 1805 1111 63 0 2440 0
vsize: 10012
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 107974 0 0 0 26715 286 0 0 25 0 1 0 904588831 10874880 1910 4294967295 134512640 134716908 3221224576 3221220756 1075115141 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2655 1910 1111 63 0 2592 0
vsize: 10620
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 111776 0 0 0 27706 296 0 0 25 0 1 0 904588831 11038720 1887 4294967295 134512640 134716908 3221224576 3221220816 1075115709 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2695 1887 1111 63 0 2632 0
vsize: 10780
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 116059 0 0 0 28696 306 0 0 25 0 1 0 904588831 10731520 1892 4294967295 134512640 134716908 3221224576 3221221052 1074968484 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2620 1892 1111 63 0 2557 0
vsize: 10480
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 120918 0 0 0 29682 320 0 0 25 0 1 0 904588831 11177984 1912 4294967295 134512640 134716908 3221224576 3221220848 1074961146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2729 1912 1111 63 0 2666 0
vsize: 10916
[startup+300.355 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 30045
Raw data (stat): 30045 (bsolo_lpr_cuts-) R 30044 20224 20223 0 -1 0 120918 0 0 0 29682 320 0 0 25 0 1 0 904588831 11177984 1912 4294967295 134512640 134716908 3221224576 3221220848 1074961146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 2729 1912 1111 63 0 2666 0
vsize: 0

Child status: 30
Real time (s): 300.354
CPU time (s): 300.377
CPU user time (s): 297.167
CPU system time (s): 3.21051
CPU usage (%): 100.008
Max. virtual memory (Kb): 10916
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	93
#### END VERIFIER DATA ####