Classical nonempty-domain FOL; original example
D={A,B}; P={A}; R={(A,A),(B,A)}
Formula: (forall x Rxy) and Px
Occurrence 1: x in Rxy is bound by forall x
Occurrence 2: y in Rxy is free
Occurrence 3: x in Px is free
Assignments x=A,y=A: true; x=B,y=A: false; x=A,y=B: false; x=B,y=B: false
Safe rename of chosen binder: (forall z Rzy) and Px
Unsafe capture: forall y Ryy instead of forall x Rxy
For y=A original forall x Rxy is true; captured forall y Ryy is false