WARNING : In order to see the result page porperly you need to install MathML player. Use MOZILLA browser for better looking output.

Run Argolib:

From my file
Create
Upload file:
Name:
Language:
Theories:
LISTS (theory of lists))
PRA (Presburger Rational Arithmetic)
FOLeq (universally quanti fragment of equality)
Output Level:
Extra:
Functions:
Predicates:
Hypotheses:
Formula:
Status:
valid
satisfiable
unsatisfiable
invalid
Scheme:
Tecton
Nelson and Oppen's