Online Otter-λ
-->
Examples
2 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).
3 [] -exists(lambda(x,Ap(Z,x)))|Ap(Z,e(Z)).
5 [] (x*y)*z=x*y*z.
6 [] divides(u,v)=exists(lambda(x,u*x=v)).
7 [] divides(a,b).
8 [] divides(b,c).
9 [] -divides(a,c).
11 [7,demod,6] exists(lambda(x,a*x=b)).
13 [8,demod,6] exists(lambda(x,b*x=c)).
15 [9,demod,6] -exists(lambda(x,a*x=c)).
16 [binary,11.1,3.1,demod,beta] a*e(lambda(x,a*x=b))=b.
17 [binary,13.1,3.1,demod,beta] b*e(lambda(x,b*x=c))=c.
18 [binary,15.1,2.2,demod,beta] a*x!=c.
28 [para_into,17.1.1.1,16.1.2,demod,5] a*e(lambda(x,a*x=b))*e(lambda(y,b*y=c))=c.
29 [binary,28.1,18.1] $F.