Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proof system

A cyclic proof system, called CLKIDω, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKIDω includes the provability of Martin-Löf’s system of inductive definitions, called LKID, and conjectured the equivalence. Since then, the equivalence has been left an open question. This paper shows that CLKIDω and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKIDω, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.