able to reprodu e the polynomial-length proofs, and we do not observe a dramati hange in the running times. With a timeout of 2 hours, smodels gives no answer for n = 12 on PHPn+1 n or CPHPn+1 n . However, for EPHPn+1 n smodels returns without any bran hing, whi h is due to the fa t that smodels' 
omplete lookahead noti
es that by bran hing on the riti al extension atoms (as in part (ii) of the proof of Theorem 5.2) the false bran
h be
omes 
ontradi
tory immediately. With this in mind, an interesting further study out of the s ope of this work would be the possibilities of integrating oni t learning te hniques with (partial) lookahead.

In the se ond experiment, we study the ee t of having a modest number of redundant rules on the behavior of ASP solvers. For this we apply the pro edure AddRandomRedundan
y(Π**, n, p**) shown in Algorithm 1. Given a program Π,
the pro edure iteratively adds rules of the form ri ← l1, l2 to Π, where l1, l2 are random default literals urrently in the program and ri is a new atom. The number of introdu ed rules is p% of the integer n.

## Algorithm 1 Addrandomredundan
Y(Π**, N, P**) 1. For I = 1 To ⌊ P 100N⌋:

1a. Randomly sele t l1, l2 ∈ dlit(Π) su
h that l1 6= l2 .

1b. Π := Π ∪ {ri ← l1, l2}, where ri 6∈ atom(Π) **∪ {⊥}**.

## 2. Return Π

In Figure 5, the median, minimum, and maximum number of de isions and running times for the solvers on AddRandomRedundan
y(PHPn+1 n**, n, p**) are shown for p = 50, 100**, . . .,** 450 over 15 trials for ea
h value of p. The mean number of de isions (left) and running times (right) on the original PHPn+1 n are presented by the horizontal lines. Noti e that the number of added atoms and rules is linear to n, whi
h is negligible to the number of atoms (in the order of n 2
) and rules (n 3
)

in PHPn+1 n . For similar running times, the number of holes n is 10 for clasp and smodels and 11 for cmodels. The results are very interesting: ea
h of the solvers seems to rea t individually to the added redundan y. For cmodels (b), only a few added redundant rules are enough to worsen its behavior. For smodels (
), the number of de isions de reases linearly with the number of added rules. However, the running times grow fast at the same time, most likely due to smodels' lookahead.

We also ran the experiment for smodels without using lookahead (d). This had a visible ee t on the number of de isions ompared to smodels on PHPn+1 n.

The most interesting ee t is seen for clasp (a); clasp benets from the added rules with respe t to the number of de isions, while the running times stay similar on the average, ontrarily to the other solvers. In addition to this robustness against redundan y, we believe that this shows promise for further exploiting redundan y added in a ontrolled way during sear h; the added rules give new possibilities to bran h on denitions whi h were not available in the original program. However, for beneting from redundan y with running times in mind, optimized lightweight propagation me hanisms are essential.