def ftmfactoreq "?msd_fib At,u (t>=i & t<i+n & i+u=t+j) => FTM[t]=FTM[u]": 
def isftmrs "?msd_fib Ej $ftmfactoreq(i,j,n) & FTM[i+n] != FTM[j+n]":
def ftmrsn "?msd_fib $isftmrs(i,n) & Aj (j<i) => ~$ftmfactoreq(i,j,n)":

eval ftmatrix n "?msd_fib $ftmrsn(i,n)":

reg fibo msd_fib "0*10*":
reg oddfib msd_fib "0*10(00)*":
reg evenfib msd_fib "0*1(00)*":
def consecfib "?msd_fib (t<u) & $fibo(t) & $fibo(u) & Av (t<v & v<u) => ~$fibo(v)": 
reg fib1001 msd_fib "0*10010*":

def interval1 "?msd_fib Et,u,y $oddfib(t) & $evenfib(u) & $consecfib(t,u) & $fib1001(y) & (t<y) & (y<=u) & (t+2<=n) & (n<=y+1)":
def interval2 "?msd_fib Et,u,y $oddfib(t) & $evenfib(u) & $consecfib(t,u) & $fib1001(y) & (t<y) & (y<=u) & (y+2<=n) & (n<=u)":
def interval3 "?msd_fib Ew,x,z $evenfib(x) & $oddfib(z) & $consecfib(x,z) & $fib1001(w) & (x<w) & (w<=z) & (x+1<=n) & (n<=w)":
def interval4 "?msd_fib Ew,x,z $evenfib(x) & $oddfib(z) & $consecfib(x,z) & $fib1001(w) & (x<w) & (w<=z) & (w+1<=n) & (n<=z+1)":

def all "?msd_fib $interval1(n) | $interval2(n) | $interval3(n) | $interval4(n)":

eval test1 "?msd_fib An $interval1(n) => FTMD[n]=@8": 
eval test2 "?msd_fib An $interval2(n) => FTMD[n]=@6": 
eval test3 "?msd_fib An $interval3(n) => FTMD[n]=@8": 
eval test4 "?msd_fib An $interval4(n) => FTMD[n]=@6":