Online Otter-λ
-->
Examples
12 [] P(i(x,i(y,x))).
13 [] P(i(i(x,y),i(i(x,i(y,z)),i(x,z)))).
14 [] P(i(i(x,y),i(i(x,n(y)),n(x)))).
15 [] P(i(n(x),i(x,y))).
16 [] P(i(u,u)).
19 [] P(i(all(lambda(x,Ap(y,x))),Ap(y,z))).
20 [] P(Ap(a,c)).
27 [] -P(x)| -P(i(x,y))|P(y).
28 [] -P(n(all(lambda(x,n(Ap(a,x)))))).
37 [hyper,27,16,12] P(i(x,i(y,y))).
45 [hyper,27,12,13] P(i(i(x,i(i(y,x),z)),i(x,z))).
46 [hyper,27,12,12] P(i(x,i(y,i(z,y)))).
49 [hyper,37,27,13] P(i(i(x,i(i(y,y),z)),i(x,z))).
279 [hyper,45,27,46] P(i(x,i(y,i(z,x)))).
289 [hyper,279,27,20] P(i(x,i(y,Ap(a,c)))).
326 [hyper,49,27,15] P(i(n(i(x,x)),y)).
342 [hyper,289,27,326] P(i(x,Ap(a,c))).
363 [hyper,342,27,14] P(i(i(x,n(Ap(a,c))),n(x))).
621 [ur,363,27,28] -P(i(all(lambda(x,n(Ap(a,x)))),n(Ap(a,c)))).
622 [binary,621.1,19.1] $F.