Formalization and Automated reasoning about a Complex Signalling Network