<?php

declare(encoding = 1);
declare(encoding = 112313123213131232100);
declare(encoding = 'utf-8');
declare(encoding = M_PI);

print 'DONE';

?>