The System for Automated Deduction accepts one-goal first-order sequents in the form of a sequence of dot-terminated formulas where the goal formula is separated from premises by a colon. Thus, a sequent  P1, P2, P3 -> G  is written as  P1. P2. P3. : G.  Sequents with the empty goal are also allowed, in the form  P1. P2. P3. :  

Formulas are built from tokens: variables, function symbols and predicate symbols, with the help of the propositional connectives, quantifiers and parentheses. You can also use Church's dot to group subformulas. Note that we use the same character to terminate formulas as this is unambiguous for well-formed formulas. We adopt the following notation (in parentheses, alternative names are shown):

Enter a first-order sequent in the window below. Use the command [Prove] to launch the prover of SAD, Moses, or the command [Prove with SPASS] to use an external prover, SPASS. The settings 'Time limit', 'Initial depth bound', and 'Final depth bound' control the process of inference search by the prover of SAD. Turn on 'Equality handling' if your problem contains the equality predicate without the axioms of equality (Brand's modification method is used). When SPASS is used, only the time limit setting is taken into account.

1. A simple lemma of the group theory. [Try this example]