Example 1.
Large-scale formal analysis of “How I Feel.”