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.

翻译：两个CNF公式称为ucp等价的，当它们关于单位子句传播（UCP）具有相同的行为。如果一个公式删除任意子句后得到的公式与原公式不再ucp等价，则称该公式为ucp不可冗余的。根据已知结果，ucp不可冗余公式的大小与最小ucp等价公式的大小之比至多为$n^2$，其中$n$为变量个数。我们针对对称确定Horn函数给出了一个ucp不可冗余公式的实例，其规模比最小ucp等价公式大$\Omega(n/\ln n)$倍，因此上述比值的一般下界不可能低于这个数值。