These problems are easy for Otter.
All use the autonomous mode.
These problems illustrate some of Otter's esoteric features:
hints, rewriting, tricks with orderings, algebraic geometry.
These are examples of Otter inputs constructed by Ivy.
Contributed by John Kalman.
Miscellaneous easy problems.
Examples of programming Otter.
These problems were used to test Otter's experimental splitting rule.
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
Argonne National Laboratory.