Enter one or more PL sentences in the top window.
Use the ~ v & > and = keys for the connectives.
Use the ! and @ keys for the quantifiers.
Prefix # to a line to prevent it from being evaluated.