Problem HirokawaMiddeldorp 04 t009

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t009

stdout:

MAYBE

Problem:
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

Proof:
Complexity Transformation Processor:
  strict:
   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
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [or](x0, x1) = x0 + x1 + 22,

     [true] = 0,

     [idle](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6 + 25,

     [newbuttons](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 10,

     [S] = 5,

     [correct] = 0,

     [empty] = 0,

     [B] = 67,

     [down] = 22,

     [up] = 0,

     [open] = 0,

     [FS] = 14,

     [incorrect] = 0,

     [BF] = 7,

     [busy](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6 + 96,

     [false] = 0,

     [stop] = 12,

     [closed] = 49,

     [F] = 88,

     [start](x0) = x0
    orientation:
     start(i) = i >= i + 245 = busy(F(),closed(),stop(),false(),false(),false(),i)

     busy(BF(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 115 >= 0 = incorrect()

     busy(FS(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 122 >= 0 = incorrect()

     busy(fl,open(),up(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 96 >= 0 = incorrect()

     busy(fl,open(),down(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 118 >= 0 = incorrect()

     busy(B(),closed(),stop(),false(),false(),false(),empty()) = 224 >= 0 = correct()

     busy(F(),closed(),stop(),false(),false(),false(),empty()) = 245 >= 0 = correct()

     busy(S(),closed(),stop(),false(),false(),false(),empty()) = 162 >= 0 = correct()

     busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 234 >= i + i1 + i2 + i3 + 163 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

     busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 255 >= i + i1 + i2 + i3 + 184 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

     busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 172 >= i + i1 + i2 + i3 + 101 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

     busy(B(),open(),stop(),false(),b2,b3,i) = b2 + b3 + i + 175 >= b2 + b3 + i + 153 = idle(B(),closed(),stop(),false(),b2,b3,i)

     busy(F(),open(),stop(),b1,false(),b3,i) = b1 + b3 + i + 196 >= b1 + b3 + i + 174 = idle(F(),closed(),stop(),b1,false(),b3,i)

     busy(S(),open(),stop(),b1,b2,false(),i) = b1 + b2 + i + 113 >= b1 + b2 + i + 91 = idle(S(),closed(),stop(),b1,b2,false(),i)

     busy(B(),d,stop(),true(),b2,b3,i) = b2 + b3 + d + i + 175 >= b2 + b3 + i + 104 = idle(B(),open(),stop(),false(),b2,b3,i)

     busy(F(),d,stop(),b1,true(),b3,i) = b1 + b3 + d + i + 196 >= b1 + b3 + i + 125 = idle(F(),open(),stop(),b1,false(),b3,i)

     busy(S(),d,stop(),b1,b2,true(),i) = b1 + b2 + d + i + 113 >= b1 + b2 + i + 42 = idle(S(),open(),stop(),b1,b2,false(),i)

     busy(B(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 234 >= b1 + b2 + b3 + i + 153 = idle(B(),closed(),stop(),b1,b2,b3,i)

     busy(S(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 150 >= b1 + b2 + b3 + i + 91 = idle(S(),closed(),stop(),b1,b2,b3,i)

     busy(B(),closed(),up(),true(),b2,b3,i) = b2 + b3 + i + 212 >= b2 + b3 + i + 153 = idle(B(),closed(),stop(),true(),b2,b3,i)

     busy(F(),closed(),up(),b1,true(),b3,i) = b1 + b3 + i + 233 >= b1 + b3 + i + 174 = idle(F(),closed(),stop(),b1,true(),b3,i)

     busy(F(),closed(),down(),b1,true(),b3,i) = b1 + b3 + i + 255 >= b1 + b3 + i + 174 = idle(F(),closed(),stop(),b1,true(),b3,i)

     busy(S(),closed(),down(),b1,b2,true(),i) = b1 + b2 + i + 172 >= b1 + b2 + i + 91 = idle(S(),closed(),stop(),b1,b2,true(),i)

     busy(B(),closed(),up(),false(),b2,b3,i) = b2 + b3 + i + 212 >= b2 + b3 + i + 81 = idle(BF(),closed(),up(),false(),b2,b3,i)

     busy(F(),closed(),up(),b1,false(),b3,i) = b1 + b3 + i + 233 >= b1 + b3 + i + 88 = idle(FS(),closed(),up(),b1,false(),b3,i)

     busy(F(),closed(),down(),b1,false(),b3,i) = b1 + b3 + i + 255 >= b1 + b3 + i + 103 = idle(BF(),closed(),down(),b1,false(),b3,i)

     busy(S(),closed(),down(),b1,b2,false(),i) = b1 + b2 + i + 172 >= b1 + b2 + i + 110 = idle(FS(),closed(),down(),b1,b2,false(),i)

     busy(BF(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 152 >= b1 + b2 + b3 + i + 162 = idle(F(),closed(),up(),b1,b2,b3,i)

     busy(BF(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 174 >= b1 + b2 + b3 + i + 163 = idle(B(),closed(),down(),b1,b2,b3,i)

     busy(FS(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 159 >= b1 + b2 + b3 + i + 79 = idle(S(),closed(),up(),b1,b2,b3,i)

     busy(FS(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 181 >= b1 + b2 + b3 + i + 184 = idle(F(),closed(),down(),b1,b2,b3,i)

     busy(B(),closed(),stop(),false(),true(),b3,i) = b3 + i + 224 >= b3 + i + 141 = idle(B(),closed(),up(),false(),true(),b3,i)

     busy(B(),closed(),stop(),false(),false(),true(),i) = i + 224 >= i + 141 = idle(B(),closed(),up(),false(),false(),true(),i)

     busy(F(),closed(),stop(),true(),false(),b3,i) = b3 + i + 245 >= b3 + i + 184 = idle(F(),closed(),down(),true(),false(),b3,i)

     busy(F(),closed(),stop(),false(),false(),true(),i) = i + 245 >= i + 162 = idle(F(),closed(),up(),false(),false(),true(),i)

     busy(S(),closed(),stop(),b1,true(),false(),i) = b1 + i + 162 >= b1 + i + 101 = idle(S(),closed(),down(),b1,true(),false(),i)

     busy(S(),closed(),stop(),true(),false(),false(),i) = i + 162 >= i + 101 = idle(S(),closed(),down(),true(),false(),false(),i)

     idle(fl,d,m,b1,b2,b3,empty()) = b1 + b2 + b3 + d + fl + m + 25 >= b1 + b2 + b3 + d + fl + m + 96 = busy(fl,d,m,b1,b2,b3,empty())

     idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m + 35 >= b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m + 162 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)

     or(true(),b) = b + 22 >= 0 = true()

     or(false(),b) = b + 22 >= b = b
    problem:
     strict:
      start(i) -> busy(F(),closed(),stop(),false(),false(),false(),i)
      busy(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
      busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,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)
     weak:
      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(),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(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)
      or(true(),b) -> true()
      or(false(),b) -> b
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [or](x0, x1) = x0 + x1 + 8,

       [true] = 0,

       [idle](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6,

       [newbuttons](x0, x1, x2, x3) = x0 + x1 + x2 + x3,

       [S] = 0,

       [correct] = 0,

       [empty] = 0,

       [B] = 9,

       [down] = 0,

       [up] = 2,

       [open] = 3,

       [FS] = 3,

       [incorrect] = 7,

       [BF] = 5,

       [busy](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6 + 4,

       [false] = 1,

       [stop] = 2,

       [closed] = 0,

       [F] = 1,

       [start](x0) = x0
      orientation:
       start(i) = i >= i + 10 = busy(F(),closed(),stop(),false(),false(),false(),i)

       busy(BF(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 11 >= b1 + b2 + b3 + i + 3 = idle(F(),closed(),up(),b1,b2,b3,i)

       busy(FS(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 7 >= b1 + b2 + b3 + i + 1 = idle(F(),closed(),down(),b1,b2,b3,i)

       idle(fl,d,m,b1,b2,b3,empty()) = b1 + b2 + b3 + d + fl + m >= b1 + b2 + b3 + d + fl + m + 4 = busy(fl,d,m,b1,b2,b3,empty())

       idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m >= b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m + 28 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)

       busy(BF(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 11 >= 7 = incorrect()

       busy(FS(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 9 >= 7 = incorrect()

       busy(fl,open(),up(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 9 >= 7 = incorrect()

       busy(fl,open(),down(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 7 >= 7 = incorrect()

       busy(B(),closed(),stop(),false(),false(),false(),empty()) = 18 >= 0 = correct()

       busy(F(),closed(),stop(),false(),false(),false(),empty()) = 10 >= 0 = correct()

       busy(S(),closed(),stop(),false(),false(),false(),empty()) = 9 >= 0 = correct()

       busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 18 >= i + i1 + i2 + i3 + 14 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

       busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 10 >= i + i1 + i2 + i3 + 6 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

       busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 9 >= i + i1 + i2 + i3 + 5 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

       busy(B(),open(),stop(),false(),b2,b3,i) = b2 + b3 + i + 19 >= b2 + b3 + i + 12 = idle(B(),closed(),stop(),false(),b2,b3,i)

       busy(F(),open(),stop(),b1,false(),b3,i) = b1 + b3 + i + 11 >= b1 + b3 + i + 4 = idle(F(),closed(),stop(),b1,false(),b3,i)

       busy(S(),open(),stop(),b1,b2,false(),i) = b1 + b2 + i + 10 >= b1 + b2 + i + 3 = idle(S(),closed(),stop(),b1,b2,false(),i)

       busy(B(),d,stop(),true(),b2,b3,i) = b2 + b3 + d + i + 15 >= b2 + b3 + i + 15 = idle(B(),open(),stop(),false(),b2,b3,i)

       busy(F(),d,stop(),b1,true(),b3,i) = b1 + b3 + d + i + 7 >= b1 + b3 + i + 7 = idle(F(),open(),stop(),b1,false(),b3,i)

       busy(S(),d,stop(),b1,b2,true(),i) = b1 + b2 + d + i + 6 >= b1 + b2 + i + 6 = idle(S(),open(),stop(),b1,b2,false(),i)

       busy(B(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 13 >= b1 + b2 + b3 + i + 11 = idle(B(),closed(),stop(),b1,b2,b3,i)

       busy(S(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 6 >= b1 + b2 + b3 + i + 2 = idle(S(),closed(),stop(),b1,b2,b3,i)

       busy(B(),closed(),up(),true(),b2,b3,i) = b2 + b3 + i + 15 >= b2 + b3 + i + 11 = idle(B(),closed(),stop(),true(),b2,b3,i)

       busy(F(),closed(),up(),b1,true(),b3,i) = b1 + b3 + i + 7 >= b1 + b3 + i + 3 = idle(F(),closed(),stop(),b1,true(),b3,i)

       busy(F(),closed(),down(),b1,true(),b3,i) = b1 + b3 + i + 5 >= b1 + b3 + i + 3 = idle(F(),closed(),stop(),b1,true(),b3,i)

       busy(S(),closed(),down(),b1,b2,true(),i) = b1 + b2 + i + 4 >= b1 + b2 + i + 2 = idle(S(),closed(),stop(),b1,b2,true(),i)

       busy(B(),closed(),up(),false(),b2,b3,i) = b2 + b3 + i + 16 >= b2 + b3 + i + 8 = idle(BF(),closed(),up(),false(),b2,b3,i)

       busy(F(),closed(),up(),b1,false(),b3,i) = b1 + b3 + i + 8 >= b1 + b3 + i + 6 = idle(FS(),closed(),up(),b1,false(),b3,i)

       busy(F(),closed(),down(),b1,false(),b3,i) = b1 + b3 + i + 6 >= b1 + b3 + i + 6 = idle(BF(),closed(),down(),b1,false(),b3,i)

       busy(S(),closed(),down(),b1,b2,false(),i) = b1 + b2 + i + 5 >= b1 + b2 + i + 4 = idle(FS(),closed(),down(),b1,b2,false(),i)

       busy(BF(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 9 >= b1 + b2 + b3 + i + 9 = idle(B(),closed(),down(),b1,b2,b3,i)

       busy(FS(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 9 >= b1 + b2 + b3 + i + 2 = idle(S(),closed(),up(),b1,b2,b3,i)

       busy(B(),closed(),stop(),false(),true(),b3,i) = b3 + i + 16 >= b3 + i + 12 = idle(B(),closed(),up(),false(),true(),b3,i)

       busy(B(),closed(),stop(),false(),false(),true(),i) = i + 17 >= i + 13 = idle(B(),closed(),up(),false(),false(),true(),i)

       busy(F(),closed(),stop(),true(),false(),b3,i) = b3 + i + 8 >= b3 + i + 2 = idle(F(),closed(),down(),true(),false(),b3,i)

       busy(F(),closed(),stop(),false(),false(),true(),i) = i + 9 >= i + 5 = idle(F(),closed(),up(),false(),false(),true(),i)

       busy(S(),closed(),stop(),b1,true(),false(),i) = b1 + i + 7 >= b1 + i + 1 = idle(S(),closed(),down(),b1,true(),false(),i)

       busy(S(),closed(),stop(),true(),false(),false(),i) = i + 8 >= i + 2 = idle(S(),closed(),down(),true(),false(),false(),i)

       or(true(),b) = b + 8 >= 0 = true()

       or(false(),b) = b + 9 >= b = b
      problem:
       strict:
        start(i) -> busy(F(),closed(),stop(),false(),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)
       weak:
        busy(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
        busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,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(),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(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)
        or(true(),b) -> true()
        or(false(),b) -> b
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [or](x0, x1) = x0 + x1,

         [true] = 3,

         [idle](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6,

         [newbuttons](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 4,

         [S] = 6,

         [correct] = 0,

         [empty] = 0,

         [B] = 15,

         [down] = 0,

         [up] = 1,

         [open] = 6,

         [FS] = 9,

         [incorrect] = 0,

         [BF] = 12,

         [busy](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6 + 3,

         [false] = 0,

         [stop] = 0,

         [closed] = 9,

         [F] = 9,

         [start](x0) = x0
        orientation:
         start(i) = i >= i + 21 = busy(F(),closed(),stop(),false(),false(),false(),i)

         idle(fl,d,m,b1,b2,b3,empty()) = b1 + b2 + b3 + d + fl + m >= b1 + b2 + b3 + d + fl + m + 3 = busy(fl,d,m,b1,b2,b3,empty())

         idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m + 4 >= b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m + 3 = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)

         busy(BF(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 25 >= b1 + b2 + b3 + i + 19 = idle(F(),closed(),up(),b1,b2,b3,i)

         busy(FS(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 21 >= b1 + b2 + b3 + i + 18 = idle(F(),closed(),down(),b1,b2,b3,i)

         busy(BF(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 15 >= 0 = incorrect()

         busy(FS(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i + 12 >= 0 = incorrect()

         busy(fl,open(),up(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 10 >= 0 = incorrect()

         busy(fl,open(),down(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i + 9 >= 0 = incorrect()

         busy(B(),closed(),stop(),false(),false(),false(),empty()) = 27 >= 0 = correct()

         busy(F(),closed(),stop(),false(),false(),false(),empty()) = 21 >= 0 = correct()

         busy(S(),closed(),stop(),false(),false(),false(),empty()) = 18 >= 0 = correct()

         busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 31 >= i + i1 + i2 + i3 + 28 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

         busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 25 >= i + i1 + i2 + i3 + 22 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

         busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 + 22 >= i + i1 + i2 + i3 + 19 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

         busy(B(),open(),stop(),false(),b2,b3,i) = b2 + b3 + i + 24 >= b2 + b3 + i + 24 = idle(B(),closed(),stop(),false(),b2,b3,i)

         busy(F(),open(),stop(),b1,false(),b3,i) = b1 + b3 + i + 18 >= b1 + b3 + i + 18 = idle(F(),closed(),stop(),b1,false(),b3,i)

         busy(S(),open(),stop(),b1,b2,false(),i) = b1 + b2 + i + 15 >= b1 + b2 + i + 15 = idle(S(),closed(),stop(),b1,b2,false(),i)

         busy(B(),d,stop(),true(),b2,b3,i) = b2 + b3 + d + i + 21 >= b2 + b3 + i + 21 = idle(B(),open(),stop(),false(),b2,b3,i)

         busy(F(),d,stop(),b1,true(),b3,i) = b1 + b3 + d + i + 15 >= b1 + b3 + i + 15 = idle(F(),open(),stop(),b1,false(),b3,i)

         busy(S(),d,stop(),b1,b2,true(),i) = b1 + b2 + d + i + 12 >= b1 + b2 + i + 12 = idle(S(),open(),stop(),b1,b2,false(),i)

         busy(B(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 27 >= b1 + b2 + b3 + i + 24 = idle(B(),closed(),stop(),b1,b2,b3,i)

         busy(S(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 19 >= b1 + b2 + b3 + i + 15 = idle(S(),closed(),stop(),b1,b2,b3,i)

         busy(B(),closed(),up(),true(),b2,b3,i) = b2 + b3 + i + 31 >= b2 + b3 + i + 27 = idle(B(),closed(),stop(),true(),b2,b3,i)

         busy(F(),closed(),up(),b1,true(),b3,i) = b1 + b3 + i + 25 >= b1 + b3 + i + 21 = idle(F(),closed(),stop(),b1,true(),b3,i)

         busy(F(),closed(),down(),b1,true(),b3,i) = b1 + b3 + i + 24 >= b1 + b3 + i + 21 = idle(F(),closed(),stop(),b1,true(),b3,i)

         busy(S(),closed(),down(),b1,b2,true(),i) = b1 + b2 + i + 21 >= b1 + b2 + i + 18 = idle(S(),closed(),stop(),b1,b2,true(),i)

         busy(B(),closed(),up(),false(),b2,b3,i) = b2 + b3 + i + 28 >= b2 + b3 + i + 22 = idle(BF(),closed(),up(),false(),b2,b3,i)

         busy(F(),closed(),up(),b1,false(),b3,i) = b1 + b3 + i + 22 >= b1 + b3 + i + 19 = idle(FS(),closed(),up(),b1,false(),b3,i)

         busy(F(),closed(),down(),b1,false(),b3,i) = b1 + b3 + i + 21 >= b1 + b3 + i + 21 = idle(BF(),closed(),down(),b1,false(),b3,i)

         busy(S(),closed(),down(),b1,b2,false(),i) = b1 + b2 + i + 18 >= b1 + b2 + i + 18 = idle(FS(),closed(),down(),b1,b2,false(),i)

         busy(BF(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i + 24 >= b1 + b2 + b3 + i + 24 = idle(B(),closed(),down(),b1,b2,b3,i)

         busy(FS(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i + 22 >= b1 + b2 + b3 + i + 16 = idle(S(),closed(),up(),b1,b2,b3,i)

         busy(B(),closed(),stop(),false(),true(),b3,i) = b3 + i + 30 >= b3 + i + 28 = idle(B(),closed(),up(),false(),true(),b3,i)

         busy(B(),closed(),stop(),false(),false(),true(),i) = i + 30 >= i + 28 = idle(B(),closed(),up(),false(),false(),true(),i)

         busy(F(),closed(),stop(),true(),false(),b3,i) = b3 + i + 24 >= b3 + i + 21 = idle(F(),closed(),down(),true(),false(),b3,i)

         busy(F(),closed(),stop(),false(),false(),true(),i) = i + 24 >= i + 22 = idle(F(),closed(),up(),false(),false(),true(),i)

         busy(S(),closed(),stop(),b1,true(),false(),i) = b1 + i + 21 >= b1 + i + 18 = idle(S(),closed(),down(),b1,true(),false(),i)

         busy(S(),closed(),stop(),true(),false(),false(),i) = i + 21 >= i + 18 = idle(S(),closed(),down(),true(),false(),false(),i)

         or(true(),b) = b + 3 >= 3 = true()

         or(false(),b) = b >= b = b
        problem:
         strict:
          start(i) -> busy(F(),closed(),stop(),false(),false(),false(),i)
          idle(fl,d,m,b1,b2,b3,empty()) -> busy(fl,d,m,b1,b2,b3,empty())
         weak:
          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(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
          busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,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(),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(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)
          or(true(),b) -> true()
          or(false(),b) -> b
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [or](x0, x1) = x0 + x1,

           [true] = 0,

           [idle](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6,

           [newbuttons](x0, x1, x2, x3) = x0 + x1 + x2 + x3,

           [S] = 0,

           [correct] = 1,

           [empty] = 1,

           [B] = 0,

           [down] = 0,

           [up] = 0,

           [open] = 0,

           [FS] = 0,

           [incorrect] = 0,

           [BF] = 0,

           [busy](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + x2 + x3 + x4 + x5 + x6,

           [false] = 0,

           [stop] = 0,

           [closed] = 0,

           [F] = 0,

           [start](x0) = x0 + 8
          orientation:
           start(i) = i + 8 >= i = busy(F(),closed(),stop(),false(),false(),false(),i)

           idle(fl,d,m,b1,b2,b3,empty()) = b1 + b2 + b3 + d + fl + m + 1 >= b1 + b2 + b3 + d + fl + m + 1 = busy(fl,d,m,b1,b2,b3,empty())

           idle(fl,d,m,b1,b2,b3,newbuttons(i1,i2,i3,i)) = b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m >= b1 + b2 + b3 + d + fl + i + i1 + i2 + i3 + m = busy(fl,d,m,or(b1,i1),or(b2,i2),or(b3,i3),i)

           busy(BF(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(F(),closed(),up(),b1,b2,b3,i)

           busy(FS(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(F(),closed(),down(),b1,b2,b3,i)

           busy(BF(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i >= 0 = incorrect()

           busy(FS(),d,stop(),b1,b2,b3,i) = b1 + b2 + b3 + d + i >= 0 = incorrect()

           busy(fl,open(),up(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i >= 0 = incorrect()

           busy(fl,open(),down(),b1,b2,b3,i) = b1 + b2 + b3 + fl + i >= 0 = incorrect()

           busy(B(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 1 = correct()

           busy(F(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 1 = correct()

           busy(S(),closed(),stop(),false(),false(),false(),empty()) = 1 >= 1 = correct()

           busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 >= i + i1 + i2 + i3 = idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

           busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 >= i + i1 + i2 + i3 = idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

           busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) = i + i1 + i2 + i3 >= i + i1 + i2 + i3 = idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))

           busy(B(),open(),stop(),false(),b2,b3,i) = b2 + b3 + i >= b2 + b3 + i = idle(B(),closed(),stop(),false(),b2,b3,i)

           busy(F(),open(),stop(),b1,false(),b3,i) = b1 + b3 + i >= b1 + b3 + i = idle(F(),closed(),stop(),b1,false(),b3,i)

           busy(S(),open(),stop(),b1,b2,false(),i) = b1 + b2 + i >= b1 + b2 + i = idle(S(),closed(),stop(),b1,b2,false(),i)

           busy(B(),d,stop(),true(),b2,b3,i) = b2 + b3 + d + i >= b2 + b3 + i = idle(B(),open(),stop(),false(),b2,b3,i)

           busy(F(),d,stop(),b1,true(),b3,i) = b1 + b3 + d + i >= b1 + b3 + i = idle(F(),open(),stop(),b1,false(),b3,i)

           busy(S(),d,stop(),b1,b2,true(),i) = b1 + b2 + d + i >= b1 + b2 + i = idle(S(),open(),stop(),b1,b2,false(),i)

           busy(B(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(B(),closed(),stop(),b1,b2,b3,i)

           busy(S(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(S(),closed(),stop(),b1,b2,b3,i)

           busy(B(),closed(),up(),true(),b2,b3,i) = b2 + b3 + i >= b2 + b3 + i = idle(B(),closed(),stop(),true(),b2,b3,i)

           busy(F(),closed(),up(),b1,true(),b3,i) = b1 + b3 + i >= b1 + b3 + i = idle(F(),closed(),stop(),b1,true(),b3,i)

           busy(F(),closed(),down(),b1,true(),b3,i) = b1 + b3 + i >= b1 + b3 + i = idle(F(),closed(),stop(),b1,true(),b3,i)

           busy(S(),closed(),down(),b1,b2,true(),i) = b1 + b2 + i >= b1 + b2 + i = idle(S(),closed(),stop(),b1,b2,true(),i)

           busy(B(),closed(),up(),false(),b2,b3,i) = b2 + b3 + i >= b2 + b3 + i = idle(BF(),closed(),up(),false(),b2,b3,i)

           busy(F(),closed(),up(),b1,false(),b3,i) = b1 + b3 + i >= b1 + b3 + i = idle(FS(),closed(),up(),b1,false(),b3,i)

           busy(F(),closed(),down(),b1,false(),b3,i) = b1 + b3 + i >= b1 + b3 + i = idle(BF(),closed(),down(),b1,false(),b3,i)

           busy(S(),closed(),down(),b1,b2,false(),i) = b1 + b2 + i >= b1 + b2 + i = idle(FS(),closed(),down(),b1,b2,false(),i)

           busy(BF(),closed(),down(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(B(),closed(),down(),b1,b2,b3,i)

           busy(FS(),closed(),up(),b1,b2,b3,i) = b1 + b2 + b3 + i >= b1 + b2 + b3 + i = idle(S(),closed(),up(),b1,b2,b3,i)

           busy(B(),closed(),stop(),false(),true(),b3,i) = b3 + i >= b3 + i = idle(B(),closed(),up(),false(),true(),b3,i)

           busy(B(),closed(),stop(),false(),false(),true(),i) = i >= i = idle(B(),closed(),up(),false(),false(),true(),i)

           busy(F(),closed(),stop(),true(),false(),b3,i) = b3 + i >= b3 + i = idle(F(),closed(),down(),true(),false(),b3,i)

           busy(F(),closed(),stop(),false(),false(),true(),i) = i >= i = idle(F(),closed(),up(),false(),false(),true(),i)

           busy(S(),closed(),stop(),b1,true(),false(),i) = b1 + i >= b1 + i = idle(S(),closed(),down(),b1,true(),false(),i)

           busy(S(),closed(),stop(),true(),false(),false(),i) = i >= i = idle(S(),closed(),down(),true(),false(),false(),i)

           or(true(),b) = b >= 0 = true()

           or(false(),b) = b >= b = b
          problem:
           strict:
            idle(fl,d,m,b1,b2,b3,empty()) -> busy(fl,d,m,b1,b2,b3,empty())
           weak:
            start(i) -> busy(F(),closed(),stop(),false(),false(),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)
            busy(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
            busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,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(),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(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)
            or(true(),b) -> true()
            or(false(),b) -> b
          Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t009

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  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) -> 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}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t009

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t009

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  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) -> 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}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds