Problem HirokawaMiddeldorp 04 t009

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputHirokawaMiddeldorp 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 TimeUnknown
Answer
MAYBE
InputHirokawaMiddeldorp 04 t009

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputHirokawaMiddeldorp 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 TimeUnknown
Answer
MAYBE
InputHirokawaMiddeldorp 04 t009

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputHirokawaMiddeldorp 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