r(ft(fn(Y,Z),X),fn(ft(Y,Z),X)).
r(ft(X,fn(Y,Z)),fn(X,ft(Y,Z))).
r(fn(ft(Y,Z),X),ft(fn(Y,Z),X)).
r(fn(X,ft(Y,Z)),ft(X,fn(Y,Z))).

r(X,X).
r(fn(X,Z),fn(Y,V)) :- r(X,Y), r(Z,V).
r(ft(X,Z),ft(Y,V)) :- r(X,Y), r(Z,V).
r(X,Z) :- r(X,Y), r(Y,Z).

i1(fn(e,e)).
i1(fn(X,Y)) :- i1(X), i1(Y).
init(ft(X,Y)) :- i1(X), i1(Y).
init(fn(X,Y)) :- init(X), i1(Y).
init(fn(X,Y)) :- i1(X), init(Y).

b1(ft(X,Y)).
b1(fn(X,Y)) :- b1(X).
b1(fn(X,Y)) :- b1(Y).
unsafe(ft(X,Y)) :- b1(X).
unsafe(ft(X,Y)) :- b1(Y).
unsafe(fn(X,Y)) :- b1(X), b1(Y).
unsafe(ft(X,Y)) :- b1(X), b1(Y).
unsafe(fn(X,Y)) :- unsafe(X).
unsafe(fn(X,Y)) :- unsafe(Y).
unsafe(ft(X,Y)) :- unsafe(X).
unsafe(ft(X,Y)) :- unsafe(Y).

#false(rewrite) :- init(X), r(X,Y), unsafe(Y).
