<?php

declare(encoding = 1);
declare(encoding = 1123131232131312321);
declare(encoding = M_PI);

print 'DONE';

?>