(VAR X) (RULES f(a,b,X) -> f(X,X,X) c -> a c -> b )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend