Hello! You can start creating a proof.

Type :help to get help.
Type :license to view license information.
Haskell implementation of [SOFiA] developed by Gregor Feierabend @ Centre for Experimental Mathematics (SU) & Mathematical Structures Research Programme (NITheCS)