Problem HirokawaMiddeldorp 04 t009

Tool Bounds

Execution Time	60.09601ms
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  or(false(), b) -> b
     , or(true(), b) -> true()
     , 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)
     , idle(fl, d, m, b1, b2, b3, empty()) ->
       busy(fl, d, m, b1, b2, b3, empty())
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), false(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(F(), closed(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(F(), closed(), stop(), true(), false(), b3, i) ->
       idle(F(), closed(), down(), true(), false(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), closed(), up(), false(), false(), true(), i)
     , busy(B(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), 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(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(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , 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)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, 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(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(B(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , busy(S(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	60.05779ms
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

TIMEOUT

Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0

Tool EDA

Execution Time	60.144176ms
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

Tool IDA

Execution Time	60.137215ms
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

Tool TRI

Execution Time	32.622765ms
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t009

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  or(false(), b) -> b
     , or(true(), b) -> true()
     , 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)
     , idle(fl, d, m, b1, b2, b3, empty()) ->
       busy(fl, d, m, b1, b2, b3, empty())
     , busy(S(), closed(), stop(), true(), false(), false(), i) ->
       idle(S(), closed(), down(), true(), false(), false(), i)
     , busy(S(), closed(), stop(), b1, true(), false(), i) ->
       idle(S(), closed(), down(), b1, true(), false(), i)
     , busy(F(), closed(), stop(), false(), false(), true(), i) ->
       idle(F(), closed(), up(), false(), false(), true(), i)
     , busy(F(), closed(), stop(), true(), false(), b3, i) ->
       idle(F(), closed(), down(), true(), false(), b3, i)
     , busy(B(), closed(), stop(), false(), false(), true(), i) ->
       idle(B(), closed(), up(), false(), false(), true(), i)
     , busy(B(), closed(), stop(), false(), true(), b3, i) ->
       idle(B(), closed(), up(), false(), true(), 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(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(), down(), b1, b2, false(), i) ->
       idle(FS(), closed(), down(), b1, b2, false(), i)
     , busy(F(), closed(), down(), b1, false(), b3, i) ->
       idle(BF(), closed(), down(), b1, false(), b3, i)
     , busy(F(), closed(), up(), b1, false(), b3, i) ->
       idle(FS(), closed(), up(), b1, false(), b3, i)
     , busy(B(), closed(), up(), false(), b2, b3, i) ->
       idle(BF(), closed(), up(), false(), b2, b3, i)
     , busy(S(), closed(), down(), b1, b2, true(), i) ->
       idle(S(), closed(), stop(), b1, b2, true(), i)
     , busy(F(), closed(), down(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(F(), closed(), up(), b1, true(), b3, i) ->
       idle(F(), closed(), stop(), b1, true(), b3, i)
     , busy(B(), closed(), up(), true(), b2, b3, i) ->
       idle(B(), closed(), stop(), true(), b2, b3, i)
     , busy(S(), closed(), up(), b1, b2, b3, i) ->
       idle(S(), closed(), stop(), b1, b2, b3, i)
     , busy(B(), closed(), down(), b1, b2, b3, i) ->
       idle(B(), closed(), stop(), b1, b2, b3, i)
     , busy(S(), d, stop(), b1, b2, true(), i) ->
       idle(S(), open(), stop(), b1, b2, false(), i)
     , 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)
     , busy(S(), open(), stop(), b1, b2, false(), i) ->
       idle(S(), closed(), stop(), b1, b2, false(), i)
     , busy(F(), open(), stop(), b1, false(), b3, i) ->
       idle(F(), closed(), stop(), b1, false(), b3, i)
     , busy(B(), open(), stop(), false(), b2, b3, i) ->
       idle(B(), closed(), stop(), false(), b2, 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(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
       ->
       idle(B(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     , busy(S(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(F(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(B(), closed(), stop(), false(), false(), false(), empty())
       -> correct()
     , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
     , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
     , busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect()
     , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
     , start(i) ->
       busy(F(), closed(), stop(), false(), false(), false(), i)}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'matrix-interpretation of dimension 4' failed due to the following reason:
         The input cannot be shown compatible

    2) 'matrix-interpretation of dimension 3' failed due to the following reason:
         The input cannot be shown compatible

    3) 'matrix-interpretation of dimension 2' failed due to the following reason:
         The input cannot be shown compatible

    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible


Arrrr..

Tool TRI2

Execution Time	3.4032848ms
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t009