MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    Loc, State
  Signature
    crit0: Loc
    crit1: Loc
    error: State
    noncrit0: Loc
    noncrit1: Loc
    state: (Loc, Loc, Bool, Bool, Int) -> State
    success: State
    wait0: Loc
    wait1: Loc
  Rules
    state(noncrit0, !p1, !b0, !b1, !x) -> state(wait0, !p1, !b01, !b1, !x1) [and(!b01, !x1 = 1)]
    state(wait0, !p1, !b0, !b1, !x) -> state(crit0, !p1, !b0, !b1, !x) [or(!x = 0, not(!b1))]
    state(crit0, !p1, !b0, !b1, !x) -> state(noncrit0, !p1, !b01, !b1, !x) [not(!b01)]
    state(!p0, noncrit1, !b0, !b1, !x) -> state(!p0, wait1, !b0, !b11, !x1) [and(!b11, !x1 = 0)]
    state(!p0, wait1, !b0, !b1, !x) -> state(!p0, crit1, !b0, !b1, !x) [or(!x = 1, not(!b0))]
    state(!p0, crit1, !b0, !b1, !x) -> state(!p0, noncrit1, !b0, !b11, !x) [not(!b11)]
    state(!p0, !p1, !b0, !b1, !x) -> success
    state(crit0, crit1, !b0, !b1, !x) -> error
* No termination info given.

Elapsed Time:  31.84 ms