Online Otter-λ
-->
Examples
% prove divides(2,6) to illustrate the use of "exists" in lambda logic.
set(lambda).
set(demod_inf).
set(binary_res).
set(very_verbose).
list(usable).
x = x.
2*3 = 6.
-Ap(Z,w) | exists(lambda(x, Ap(Z,x))).
end_of_list.
list(demodulators).
divides(u,v) = exists(lambda(x,u*x = v)).
end_of_list.
list(sos).
-divides(2,6).
end_of_list.