This set contains handmade ground instances all of which are
unsatisfiable. The programs follow simple patterns, one pattern yields
family "Head," the other family "Body." Instances of the "Head" family
are easily determined unsatisfiable by smodels, but take exponential
time with noMoRe (but not with nomore++). With family "Body," it is the
other way round.
et 'n' be the number in an instance name. The pattern for family "Body"
is like this:
x :- not x.
x :- not a_1, not b_1.
a_1 :- not b_1.
b_1 :- not a_1.
x :- not a_n, not b_n.
a_n :- not b_n.
b_n :- not a_n.
Author: Martin Gebser.
1 - 20 of 101