Online Otter-λ
-->
Examples
1 [] 1!=0.
2 [] pow(o,x)=0|pow(g(x,y),x)!=0|pow(y,x)!=0.
3 [] pow(o,x)=0|pow(g(x,y)+1,x)=0|pow(y,x)!=0.
4 [] b!=0.
5 [] x=x.
29 [] x*y!=0|x=0|y=0.
31,30 [] pow(x+1,y)=y*pow(x,y).
35,34 [] pow(o,x)=1.
36 [] pow(c,b)=0.
39 [back_demod,3,demod,35,31,unit_del,1] x*pow(g(x,y),x)=0|pow(y,x)!=0.
40 [back_demod,2,demod,35,unit_del,1] pow(g(x,y),x)!=0|pow(y,x)!=0.
274 [para_from,29.2.1,4.1.1,unit_del,5] b*x!=0|x=0.
602,601 [hyper,39,36] b*pow(g(b,c),b)=0.
691 [para_into,40.2.1,36.1.1,unit_del,5] pow(g(b,c),b)!=0.
718 [para_into,691.1.1,274.2.1,demod,602,unit_del,5,5] $F.