Add STP example in SMT-LIB 2.0 format.

This file can serve as input for Z3.