means that at least i and at most j
of the n propositions are true. An andor rule is built with the SNePSUL command:
(assert min i max j
arg (
))
The following special cases of andor are representations of standard connectives: i=j=n is AND; i=j=0 is a generalization of NOR; and i=j=1 is a generalization of EXCLUSIVE OR.