Try form input.

The input formulas may contain no more than 20,000characters total in the format. Please enter either:

1. the name of a file containing the wff here:
   
2. or the actual wff here:
   

       Brief output format:

• Math ref.
• Java with input from file
• html
http://altavista.digital.com/">Altavista
• Altavista
• Theory archive