Theorem 2.6 ([1]}) 

There is an algorithm which, given a binary structure \(S\)  on \(n\)  vertices,
a contraction sequence of width \(k\)  for \(S\) , and a FO formula \(\phi \) ,
decides if \(S \models \phi \)  in time \(f(k,\phi ) \cdot n\) .

