% 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."