YES
0 QTRS
↳1 QTRSRRRProof (⇔, 135 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 43 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 0 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 8 ms)
↳8 QTRS
↳9 AAECC Innermost (⇔, 0 ms)
↳10 QTRS
↳11 DependencyPairsProof (⇔, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QReductionProof (⇔, 0 ms)
↳16 QDP
↳17 TransformationProof (⇔, 0 ms)
↳18 QDP
↳19 TransformationProof (⇔, 0 ms)
↳20 QDP
↳21 TransformationProof (⇔, 0 ms)
↳22 QDP
↳23 TransformationProof (⇔, 0 ms)
↳24 QDP
↳25 TransformationProof (⇔, 0 ms)
↳26 QDP
↳27 TransformationProof (⇔, 0 ms)
↳28 QDP
↳29 TransformationProof (⇔, 0 ms)
↳30 QDP
↳31 TransformationProof (⇔, 0 ms)
↳32 QDP
↳33 TransformationProof (⇔, 0 ms)
↳34 QDP
↳35 TransformationProof (⇔, 0 ms)
↳36 QDP
↳37 TransformationProof (⇔, 0 ms)
↳38 QDP
↳39 TransformationProof (⇔, 0 ms)
↳40 QDP
↳41 TransformationProof (⇔, 0 ms)
↳42 QDP
↳43 TransformationProof (⇔, 0 ms)
↳44 QDP
↳45 TransformationProof (⇔, 0 ms)
↳46 QDP
↳47 TransformationProof (⇔, 0 ms)
↳48 QDP
↳49 TransformationProof (⇔, 0 ms)
↳50 QDP
↳51 TransformationProof (⇔, 0 ms)
↳52 QDP
↳53 TransformationProof (⇔, 0 ms)
↳54 QDP
↳55 TransformationProof (⇔, 0 ms)
↳56 QDP
↳57 TransformationProof (⇔, 0 ms)
↳58 QDP
↳59 DependencyGraphProof (⇔, 0 ms)
↳60 QDP
↳61 TransformationProof (⇔, 0 ms)
↳62 QDP
↳63 TransformationProof (⇔, 0 ms)
↳64 QDP
↳65 TransformationProof (⇔, 0 ms)
↳66 QDP
↳67 TransformationProof (⇔, 0 ms)
↳68 QDP
↳69 DependencyGraphProof (⇔, 0 ms)
↳70 QDP
↳71 TransformationProof (⇔, 0 ms)
↳72 QDP
↳73 TransformationProof (⇔, 0 ms)
↳74 QDP
↳75 TransformationProof (⇔, 0 ms)
↳76 QDP
↳77 TransformationProof (⇔, 0 ms)
↳78 QDP
↳79 TransformationProof (⇔, 0 ms)
↳80 QDP
↳81 TransformationProof (⇔, 0 ms)
↳82 QDP
↳83 DependencyGraphProof (⇔, 0 ms)
↳84 TRUE
start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = 1 + 2·x1 + x2 + x3 + 2·x4 + 2·x5 + 2·x6 + x7
POL(closed) = 0
POL(correct) = 1
POL(down) = 0
POL(empty) = 1
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 1 + 2·x1 + x2 + 2·x3 + 2·x4 + 2·x5 + 2·x6 + x7
POL(incorrect) = 0
POL(newbuttons(x1, x2, x3, x4)) = 2 + 2·x1 + 2·x2 + 2·x3 + 2·x4
POL(open) = 2
POL(or(x1, x2)) = x1 + x2
POL(start(x1)) = 1 + 2·x1
POL(stop) = 0
POL(true) = 1
POL(up) = 0
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
start(i) → busy(F, closed, stop, false, false, false, i)
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
or(true, b) → true
or(false, b) → b
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(B) = 1
POL(BF) = 1
POL(F) = 1
POL(FS) = 1
POL(S) = 1
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = 2·x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(closed) = 0
POL(down) = 0
POL(empty) = 1
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 2·x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(newbuttons(x1, x2, x3, x4)) = 2 + x1 + 2·x2 + x3 + x4
POL(open) = 1
POL(or(x1, x2)) = 1 + 2·x1 + x2
POL(start(x1)) = 2 + 2·x1
POL(stop) = 0
POL(true) = 2
POL(up) = 0
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
or(true, b) → true
or(false, b) → b
start(i) → busy(F, closed, stop, false, false, false, i)
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = 2 + x1 + x2 + x3 + x4 + x5 + x6 + 2·x7
POL(closed) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 2 + 2·x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(newbuttons(x1, x2, x3, x4)) = 1 + x1 + 2·x2 + x3 + x4
POL(start(x1)) = 2 + 2·x1
POL(stop) = 0
POL(true) = 0
POL(up) = 0
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
start(i) → busy(F, closed, stop, false, false, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = x1 + x2 + x3 + 2·x4 + 2·x5 + x6 + 2·x7
POL(closed) = 1
POL(down) = 0
POL(empty) = 1
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 2·x1 + x2 + 2·x3 + 2·x4 + 2·x5 + x6 + 2·x7
POL(start(x1)) = 2 + 2·x1
POL(stop) = 0
POL(true) = 0
POL(up) = 0
start(i) → busy(F, closed, stop, false, false, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty) → BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty) → BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty) → BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty) → BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty) → BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty) → BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty) → BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty) → BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty) → BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty) → BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty) → BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty) → BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty) → BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty) → BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty) → BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty) → BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty) → BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty) → IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty) → IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty) → IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty) → IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty) → IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty) → IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty) → IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty) → IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty) → IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty) → IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty) → IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty) → IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty) → IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty) → IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty) → IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)