0 GTRS
and(tt) → X __(__(X, Y), Z) → __(X, __(Y, Z)) __(X, nil) → X __(nil, X) → X isNePal(__(I, __(P, I))) → tt