Proving theorems by pattern recognition I | Synapse