  Two CNF formulas are called ucp-equivalent, if they behave in the same way
with respect to the unit clause propagation (UCP). A formula is called
ucp-irredundant, if removing any clause leads to a formula which is not
ucp-equivalent to the original one. As a consequence of known results, the
ratio of the size of a ucp-irredundant formula and the size of a smallest
ucp-equivalent formula is at most $n^2$, where $n$ is the number of the
variables. We demonstrate an example of a ucp-irredundant formula for a
symmetric definite Horn function which is larger than a smallest ucp-equivalent
formula by a factor $\Omega(n/\ln n)$ and, hence, a general upper bound on the
above ratio cannot be smaller than this.
