/* run */ define answer_2a() = {
    exists A, B :{
        A = 0 AND B = 0 AND skip;
        B = 1 AND skip;
        empty AND B = 0
    }
}.