Case splitting on opti atoms in premises (abduction and disjunction elimination). Generating opti atoms in disjunction elimination (initial commit).