TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1895ms).
 | – Problem 2 was processed with processor SubtermCriterion (7ms).
 |    | – Problem 3 was processed with processor DependencyGraph (1269ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (1188ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (554ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (767ms).
 |    |    |    |    |    | – Problem 7 remains open; application of the following processors failed [DependencyGraph (439ms), PolynomialLinearRange4iUR (8824ms), DependencyGraph (438ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (467ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 7

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)
busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)
busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, i)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)
busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)
busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, newbuttons, incorrect

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)start#(i) → busy#(F, closed, stop, false, false, false, i)
busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, 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#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)
busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)
busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → or#(b2, i2)
busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)
idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → or#(b3, i3)busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)
busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, 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#(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle#(F, 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, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, 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)busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)
busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)
idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → or#(b1, i1)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, incorrect, newbuttons

Strategy

The following SCCs where found

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, 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#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)
busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)
busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)
busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, 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, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle#(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)
busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, 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)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)
busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, 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#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)
busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)
busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)
busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, 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, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, 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#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, 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)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)
busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, incorrect, newbuttons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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)

Problem 3: DependencyGraph

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, 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#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)
busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)
busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)
busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, 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#(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle#(F, 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, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)
busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)
busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, newbuttons, incorrect

Strategy

The following SCCs where found

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, i)
busy#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)
busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)
busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)
busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)
busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, i)busy#(B, open, stop, false, b2, b3, i) → idle#(B, closed, stop, false, b2, b3, i)
busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)
busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Problem 4: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)
busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, i)
busy#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)
busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)
busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)
busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)
busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, i)busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)
busy#(B, open, stop, false, b2, b3, i) → idle#(B, closed, stop, false, b2, b3, i)busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)
busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, newbuttons, incorrect

Strategy

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

busy#(S, d, stop, b1, b2, true, i) → idle#(S, open, stop, b1, b2, false, i)

Problem 5: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)
idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)
busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)
busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, i)busy#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)
busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)
busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)
busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, i)
busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)busy#(B, open, stop, false, b2, b3, i) → idle#(B, closed, stop, false, b2, b3, i)
busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)
busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, incorrect, newbuttons

Strategy

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

busy#(F, d, stop, b1, true, b3, i) → idle#(F, open, stop, b1, false, b3, i)busy#(B, d, stop, true, b2, b3, i) → idle#(B, open, stop, false, b2, b3, i)

Problem 6: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

busy#(F, closed, down, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(S, closed, stop, true, false, false, i) → idle#(S, closed, down, true, false, false, i)
busy#(B, closed, stop, false, false, true, i) → idle#(B, closed, up, false, false, true, i)busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, i)
busy#(F, closed, down, b1, false, b3, i) → idle#(BF, closed, down, b1, false, b3, i)idle#(fl, d, m, b1, b2, b3, empty) → busy#(fl, d, m, b1, b2, b3, empty)
busy#(B, closed, stop, false, true, b3, i) → idle#(B, closed, up, false, true, b3, i)busy#(S, closed, down, b1, b2, true, i) → idle#(S, closed, stop, b1, b2, true, i)
busy#(B, open, stop, false, b2, b3, i) → idle#(B, closed, stop, false, b2, b3, i)busy#(F, closed, stop, false, false, true, i) → idle#(F, closed, up, false, false, true, i)
busy#(FS, closed, down, b1, b2, b3, i) → idle#(F, closed, down, b1, b2, b3, i)busy#(FS, closed, up, b1, b2, b3, i) → idle#(S, closed, up, b1, b2, b3, i)
busy#(B, closed, down, b1, b2, b3, i) → idle#(B, closed, stop, b1, b2, b3, i)busy#(F, closed, up, b1, false, b3, i) → idle#(FS, closed, up, b1, false, b3, i)
busy#(F, closed, stop, true, false, b3, i) → idle#(F, closed, down, true, false, b3, i)busy#(B, closed, up, true, b2, b3, i) → idle#(B, closed, stop, true, b2, b3, i)
busy#(S, closed, down, b1, b2, false, i) → idle#(FS, closed, down, b1, b2, false, i)busy#(B, closed, up, false, b2, b3, i) → idle#(BF, closed, up, false, b2, b3, i)
busy#(F, open, stop, b1, false, b3, i) → idle#(F, closed, stop, b1, false, b3, i)busy#(S, closed, stop, b1, true, false, i) → idle#(S, closed, down, b1, true, false, i)
busy#(F, closed, up, b1, true, b3, i) → idle#(F, closed, stop, b1, true, b3, i)busy#(S, closed, up, b1, b2, b3, i) → idle#(S, closed, stop, b1, b2, b3, i)
busy#(BF, closed, down, b1, b2, b3, i) → idle#(B, closed, down, b1, b2, b3, i)busy#(BF, closed, up, b1, b2, b3, i) → idle#(F, closed, up, b1, b2, b3, i)

Rewrite Rules

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) → incorrectbusy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrectbusy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correctbusy(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

Original Signature

Termination of terms over the following signature is verified: stop, F, or, B, true, busy, up, BF, FS, idle, open, correct, start, S, empty, false, closed, down, newbuttons, incorrect

Strategy

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

busy#(S, open, stop, b1, b2, false, i) → idle#(S, closed, stop, b1, b2, false, 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)