<?php

echo (int)"123H3llo W0rld";