Cet article définit deux formules CNF se comportant de manière identique sous la propagation de clause unitaire (UCP) comme ucp-équivalentes, et définit une formule qui n'est pas ucp-équivalente à la formule originale, quelle que soit la clause supprimée, comme ucp-irrédundante. D'après des recherches antérieures, le rapport entre la taille d'une formule ucp-irrédundante et la taille de la plus petite formule ucp-équivalente est au plus $n^2$ (n étant le nombre de variables). Dans cet article, nous montrons que la borne supérieure générale du rapport ne peut être inférieure à cette valeur en donnant l'exemple d'une formule ucp-irrédundante dont la taille est $\Omega(n/\ln n)$ fois supérieure à celle de la plus petite formule ucp-équivalente pour une fonction de Horn définie symétrique.
