/home/mccune/otter-3.3/examples

• auto . These problems are easy for Otter. All use the autonomous mode.
• fringe . These problems illustrate some of Otter's esoteric features: hints, rewriting, tricks with orderings, algebraic geometry.
• ivy . These are examples of Otter inputs constructed by Ivy.
• kalman . Contributed by John Kalman.
• misc . Miscellaneous easy problems.
• program . Examples of programming Otter.
• split . These problems were used to test Otter's experimental splitting rule.
• wos . These problems were contributed by Larry Wos in 1994. Most illustrate the resonance strategy.

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.