Online Otter-λ
-->
Examples
% prove the arithmetic-geometric mean inequality
% sqrt(ab) <= (a+b)/2
set(simplify).
set(binary_res).
set(hyper_res).
set(para_into).
set(para_all).
op(450, xfy, +).
op(450, xfy, -).
op(400, xfx, /).
op(350, fy, ~).
op(400, xfy, *).
op(300, xfx, ^).
assign(max_weight,32).
assign(max_distinct_vars,0).
list(usable).
x=x.
x <= y | y <= x.
-(x <= y) | -(u <= v) | (x+u <= y+v).
0 <= a.
0 <= b.
-(0<=x) | -(x <= y) | x^2 <= y^2.
-(0<=x) | -(x < y) | x^2 < y^2.
a != b.
% if you include some of these axioms it finds different proofs.
%x < y | x = y | y < x.
% -(x<= y) | -(y <= x) | x = y.
% -(x < y) | x <= y.
% -(x <= y ) | x = y | x < y.
% -(x < y) | -(u < v) | (x+u < y+v).
end_of_list.
list(sos).
-(sqrt(a*b) < (a+b)/2).
end_of_list.