The following sidenote is not correct: "As a side note, Libor was able to prove
it using t of arity 5, however he needs to to assume finiteness." 

Libor was able to prove something else -- the local loop lemma with unoriented
cycle of length 5 (analogous to the theorem 9).