notp1 has no fixed point.list(usable). a(notp1,x) != x. % (not used in later proofs) end_of_list.
Proof of a(notp1,x) != x. | OTTER output file
Applying notp1 to any combinator yields a characteristic function.
list(usable). a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2. end_of_list.
Proof of a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2. | OTTER output file