본 논문은 Unit Clause Propagation (UCP)에 대해 동일하게 동작하는 두 CNF 공식을 ucp-equivalent라고 정의하고, 어떤 절을 제거해도 원래 공식과 ucp-equivalent하지 않은 공식이 되는 공식을 ucp-irredundant라고 정의합니다. 기존 연구 결과에 따르면, ucp-irredundant 공식의 크기와 가장 작은 ucp-equivalent 공식의 크기 비율은 최대 $n^2$ (n은 변수 개수)입니다. 본 논문은 대칭적인 definite Horn 함수에 대해, 가장 작은 ucp-equivalent 공식보다 크기가 $\Omega(n/\ln n)$ 배 더 큰 ucp-irredundant 공식의 예시를 보여줌으로써, 위 비율에 대한 일반적인 상한이 이 값보다 작을 수 없음을 증명합니다.
