% a small example file

PROVER otter  % put "otter2" here if you want another otter than "otter"
DIRECTORY ""  % put "groups" here if you want to store the .in files
              % in a sub-directory called "groups" instead of in the
              % current directory
% you don't need these directives, "otter" and "" are the defaults

OPTION @basic  % you can name blocks of lines for convenience
set(auto).
NOITPO

AXIOM @right_identity @identity
  all x (x * e = x).
MOIXA

AXIOM @the_other_group_axioms
  all x (x * i(x) = e).
  all x y z (x * (y * z) = (x * y) * z).
MOIXA

LEMMA @left_inverse
  all x (i(x) * x = e)
PROOF
set(auto).
formula_list(usable).
@right_identity.
@the_other_group_axioms.
end_of_list.
formula_list(sos).
-(@left_inverse).
end_of_list.
FOORP

LEMMA @left_identity @identity
  all x (e * x = x)
PROOF
@basic
USEALL
QED

% you can refer to groups of statements with classes like "@identity"
% every statement until the current point will automatically be in "@ALL"
% USEALL means something like "formula_list(usable). @ALL. end_of_list."
% QED means something like "formula_list(sos). -(@lemmaname). end_of_list."