test/golden/formula/encoding tasks.golden


1
2
3
4
5
6
7
8

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)).
------------------
fof(formula_test_not_exists,conjecture,?[Xx,Xy]:Xx=Xy<=>~?[Xx]:Xx!=Xx).
fof(formula_test_exists,axiom,?[Xx,Xy]:Xx=Xy).
fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).