  The framework of cyclic proof systems provides a reasonable proof system for
logics with inductive definitions. It also offers an effective automated proof
search procedure for such logics without finding induction hypotheses. Recent
researches have shown that the cut-elimination property, one of the most
fundamental properties in proof theory, of cyclic proof systems for several
logics does not hold. These results suggest that a naive proof search, which
avoids the Cut rule, is not enough.
  This paper shows that the cut-elimination property still fails in a simple
cyclic proof system even if we restrict languages to unary inductive predicates
and unary functions, aiming to clarify why the cut-elimination property fails
in the cyclic proof systems. The result in this paper is a sharper one than
that of the first authors' previous result, which gave a counterexample using
two ternary inductive predicates and a unary function symbol to show the
failure of the cut-elimination property in the cyclic proof system of the
first-order logic.
