encoding tasks.golden « formula « golden « test - naproche-zf.git - Unnamed repository; edit this file 'description' to name the repository.

summary refs log tree commit diff

path: root/test/golden/formula/encoding tasks.golden

blob: ab149dda44fc4b6e24f65e0c1d62e7cbf5edd39d (plain)

fof(formula_test_forall,conjecture,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
------------------
fof(formula_test_exists,conjecture,?[Xx,Xy]:Xx=Xy).
fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).