Online Otter-λ
-->
Examples
6 [] sum(u,v,x,y+1)=sum(u,v,x,y)+Ap(lambda(u,v),1+y).
7 [] sum(u,v,x,x)=Ap(lambda(u,v),x).
10 [] x+1!=y+1|x=y.
11 [] -Ap(y,0)|Ap(y,g(y))|Ap(y,z).
12 [] -Ap(y,0)| -Ap(y,g(y)+1)|Ap(y,z).
14 [] 6*sum(x,x^2,0,n)!=n* (n+1)* (2*n+1).
15 [binary,14,12,demod,beta,7,beta,beta,6,beta,simplify] 6* (1+2*g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1)))+g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1)))^2+sum(x,x^2,0,g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1)))))!= (1+g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))))* (2+g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))))* (3+2*g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1)))).
16 [binary,14,11,demod,beta,7,beta,beta,simplify] 6*sum(x,x^2,0,g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))))= (1+2*g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))))* (1+g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))))*g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))).
26 [binary,15,10,simplify] 6*g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1)))^2+12*g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1)))+6*sum(z,z^2,0,g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1))))!=2*g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1)))^3+9*g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1)))^2+13*g(lambda(x,6*sum(y,y^2,0,x)=x* (x+1)* (2*x+1))).
32 [para_into,26,16,simplify] $F.