predT(n,n,q0).
predT(t,n,q1).
predT(n,t,q3).

predT(fT(X,Y),fN(Z,V),q1) :- predT(X,Z,q0), predT(Y,V,q0).
predT(fN(X,Y),fT(Z,V),q2) :- predT(X,Z,q1), predT(Y,V,q0).
predT(fN(X,Y),fT(Z,V),q2) :- predT(X,Z,q0), predT(Y,V,q1).
predT(fN(X,Y),fN(Z,V),q0) :- predT(X,Z,q0), predT(Y,V,q0).
predT(fN(X,Y),fN(Z,V),q2) :- predT(X,Z,q0), predT(Y,V,q2).
predT(fN(X,Y),fN(Z,V),q2) :- predT(X,Z,q2), predT(Y,V,q0).
predT(fT(X,Y),fN(Z,V),q2) :- predT(X,Z,q3), predT(Y,V,q0).
predT(fT(X,Y),fN(Z,V),q2) :- predT(X,Z,q0), predT(Y,V,q3).
predT(fN(X,Y),fT(Z,V),q3) :- predT(X,Z,q0), predT(Y,V,q0).

init(n,q0).
init(t,q1).
init(fT(X,Y),q1) :- init(X,q0), init(Y,q0).
init(fN(X,Y),q1) :- init(X,q0), init(Y,q1).
init(fN(X,Y),q0) :- init(X,q0), init(Y,q0).
init(fN(X,Y),q1) :- init(X,q1), init(Y,q0).

bad(n,q0).
bad(t,q1).
bad(fN(X,Y),q0) :- bad(X,q0), bad(Y,q0).
bad(fT(X,Y),q1) :- bad(X,q0), bad(Y,q0).
bad(fN(X,Y),q1) :- bad(X,q0), bad(Y,q1).
bad(fN(X,Y),q0) :- bad(X,q1), bad(Y,q0).

bad(fT(X,Y),q2) :- bad(X,q0), bad(Y,q1).
bad(fT(X,Y),q2) :- bad(X,q1), bad(Y,q0).
bad(fN(X,Y),q2) :- bad(X,q1), bad(Y,q1).
bad(fT(X,Y),q2) :- bad(X,q1), bad(Y,q2).

bad(fT(X,Y),q2) :- bad(X,q2), bad(Y,q1).
bad(fT(X,Y),q2) :- bad(X,q2), bad(Y,q2).
bad(fN(X,Y),q2) :- bad(X,q1), bad(Y,q1).
bad(fN(X,Y),q2) :- bad(X,q0), bad(Y,q2).
bad(fN(X,Y),q2) :- bad(X,q2), bad(Y,q0).
bad(fN(X,Y),q2) :- bad(X,q1), bad(Y,q2).
bad(fN(X,Y),q2) :- bad(X,q2), bad(Y,q1).
bad(fN(X,Y),q2) :- bad(X,q2), bad(Y,q2).

r(X,Y) :- predT(X,Y,q2).
r(X,Z) :- r(X,Y), r(Y,Z).

init1(X) :- init(X,q1).
bad1(X) :- bad(X,q2).

#false(rtmc) :- init1(X), r(X,Y), bad1(Y).
