Input TRS:
    1: start(i) -> busy(F(),closed(),stop(),false(),false(),false(),i)
    2: busy(BF(),d,stop(),b1,b2,b3,i) -> incorrect()
    3: busy(FS(),d,stop(),b1,b2,b3,i) -> incorrect()
    4: busy(fl,open(),up(),b1,b2,b3,i) -> incorrect()
    5: busy(fl,open(),down(),b1,b2,b3,i) -> incorrect()
    6: busy(B(),closed(),stop(),false(),false(),false(),empty()) -> correct()
    7: busy(F(),closed(),stop(),false(),false(),false(),empty()) -> correct()
    8: busy(S(),closed(),stop(),false(),false(),false(),empty()) -> correct()
    9: busy(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle(B(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
    10: busy(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle(F(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
    11: busy(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i)) -> idle(S(),closed(),stop(),false(),false(),false(),newbuttons(i1,i2,i3,i))
    12: busy(B(),open(),stop(),false(),b2,b3,i) -> idle(B(),closed(),stop(),false(),b2,b3,i)
    13: busy(F(),open(),stop(),b1,false(),b3,i) -> idle(F(),closed(),stop(),b1,false(),b3,i)
    14: busy(S(),open(),stop(),b1,b2,false(),i) -> idle(S(),closed(),stop(),b1,b2,false(),i)
    15: busy(B(),d,stop(),true(),b2,b3,i) -> idle(B(),open(),stop(),false(),b2,b3,i)
    16: busy(F(),d,stop(),b1,true(),b3,i) -> idle(F(),open(),stop(),b1,false(),b3,i)
    17: busy(S(),d,stop(),b1,b2,true(),i) -> idle(S(),open(),stop(),b1,b2,false(),i)
    18: busy(B(),closed(),down(),b1,b2,b3,i) -> idle(B(),closed(),stop(),b1,b2,b3,i)
    19: busy(S(),closed(),up(),b1,b2,b3,i) -> idle(S(),closed(),stop(),b1,b2,b3,i)
    20: busy(B(),closed(),up(),true(),b2,b3,i) -> idle(B(),closed(),stop(),true(),b2,b3,i)
    21: busy(F(),closed(),up(),b1,true(),b3,i) -> idle(F(),closed(),stop(),b1,true(),b3,i)
    22: busy(F(),closed(),down(),b1,true(),b3,i) -> idle(F(),closed(),stop(),b1,true(),b3,i)
    23: busy(S(),closed(),down(),b1,b2,true(),i) -> idle(S(),closed(),stop(),b1,b2,true(),i)
    24: busy(B(),closed(),up(),false(),b2,b3,i) -> idle(BF(),closed(),up(),false(),b2,b3,i)
    25: busy(F(),closed(),up(),b1,false(),b3,i) -> idle(FS(),closed(),up(),b1,false(),b3,i)
    26: busy(F(),closed(),down(),b1,false(),b3,i) -> idle(BF(),closed(),down(),b1,false(),b3,i)
    27: busy(S(),closed(),down(),b1,b2,false(),i) -> idle(FS(),closed(),down(),b1,b2,false(),i)
    28: busy(BF(),closed(),up(),b1,b2,b3,i) -> idle(F(),closed(),up(),b1,b2,b3,i)
    29: busy(BF(),closed(),down(),b1,b2,b3,i) -> idle(B(),closed(),down(),b1,b2,b3,i)
    30: busy(FS(),closed(),up(),b1,b2,b3,i) -> idle(S(),closed(),up(),b1,b2,b3,i)
    31: busy(FS(),closed(),down(),b1,b2,b3,i) -> idle(F(),closed(),down(),b1,b2,b3,i)
    32: busy(B(),closed(),stop(),false(),true(),b3,i) -> idle(B(),closed(),up(),false(),true(),b3,i)
    33: busy(B(),closed(),stop(),false(),false(),true(),i) -> idle(B(),closed(),up(),false(),false(),true(),i)
    34: busy(F(),closed(),stop(),true(),false(),b3,i) -> idle(F(),closed(),down(),true(),false(),b3,i)
    35: busy(F(),closed(),stop(),false(),false(),true(),i) -> idle(F(),closed(),up(),false(),false(),true(),i)
    36: busy(S(),closed(),stop(),b1,true(),false(),i) -> idle(S(),closed(),down(),b1,true(),false(),i)
    37: busy(S(),closed(),stop(),true(),false(),false(),i) -> idle(S(),closed(),down(),true(),false(),false(),i)
    38: idle(fl,d,m,b1,b2,b3,empty()) -> busy(fl,d,m,b1,b2,b3,empty())
    39: 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)
    40: or(true(),b) -> true()
    41: or(false(),b) -> b
Number of strict rules: 41
Direct Order(PosReal,>,Poly) ... removes: 4 8 1 3 5 39 7 40 6 41 2
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: (/ 3 2) + 2 * x1 + 2 * x2 + 2 * x3 + x4
     S()	weight: 0
     F()	weight: 0
 false()	weight: 0
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: (/ 1 4) + x1 + x2 + x3 + 2 * x4 + x5 + 2 * x6 + x7
  true()	weight: 0
     B()	weight: 0
correct()	weight: 0
    FS()	weight: 0
    or(x1,x2)	weight: (/ 1 4) + x1 + x2
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: (/ 1 4) + x1 + x2 + x3 + 2 * x4 + x5 + 2 * x6 + x7
  open()	weight: 0
 empty()	weight: 0
 start(x1)	weight: (/ 1 2) + x1
    BF()	weight: 0
    up()	weight: 0
Number of strict rules: 30
Direct Order(PosReal,>,Poly) ... removes: 10 11 9
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: (/ 5 4) + 2 * x1 + 2 * x2 + x3 + x4
     S()	weight: 0
     F()	weight: 0
 false()	weight: 0
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: (/ 1 4) + x1 + x2 + x3 + 2 * x4 + x5 + 2 * x6 + x7
  true()	weight: 0
     B()	weight: 0
correct()	weight: 0
    FS()	weight: 0
    or(x1,x2)	weight: (/ 1 4) + x1 + x2
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: (/ 1 4) + x1 + x2 + x3 + 2 * x4 + x5 + 2 * x6 + 2 * x7
  open()	weight: 0
 empty()	weight: 0
 start(x1)	weight: (/ 1 2) + 2 * x1
    BF()	weight: 0
    up()	weight: 0
Number of strict rules: 27
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #busy(BF(),closed(),down(),b1,b2,b3,i) -> #idle(B(),closed(),down(),b1,b2,b3,i)
   #2: #busy(F(),closed(),stop(),false(),false(),true(),i) -> #idle(F(),closed(),up(),false(),false(),true(),i)
   #3: #busy(S(),closed(),stop(),true(),false(),false(),i) -> #idle(S(),closed(),down(),true(),false(),false(),i)
   #4: #idle(fl,d,m,b1,b2,b3,empty()) -> #busy(fl,d,m,b1,b2,b3,empty())
   #5: #busy(F(),open(),stop(),b1,false(),b3,i) -> #idle(F(),closed(),stop(),b1,false(),b3,i)
   #6: #busy(B(),closed(),up(),false(),b2,b3,i) -> #idle(BF(),closed(),up(),false(),b2,b3,i)
   #7: #busy(S(),closed(),down(),b1,b2,true(),i) -> #idle(S(),closed(),stop(),b1,b2,true(),i)
   #8: #busy(B(),open(),stop(),false(),b2,b3,i) -> #idle(B(),closed(),stop(),false(),b2,b3,i)
   #9: #busy(FS(),closed(),down(),b1,b2,b3,i) -> #idle(F(),closed(),down(),b1,b2,b3,i)
   #10: #busy(S(),open(),stop(),b1,b2,false(),i) -> #idle(S(),closed(),stop(),b1,b2,false(),i)
   #11: #busy(FS(),closed(),up(),b1,b2,b3,i) -> #idle(S(),closed(),up(),b1,b2,b3,i)
   #12: #busy(F(),closed(),up(),b1,false(),b3,i) -> #idle(FS(),closed(),up(),b1,false(),b3,i)
   #13: #busy(B(),closed(),up(),true(),b2,b3,i) -> #idle(B(),closed(),stop(),true(),b2,b3,i)
   #14: #busy(B(),closed(),stop(),false(),false(),true(),i) -> #idle(B(),closed(),up(),false(),false(),true(),i)
   #15: #busy(BF(),closed(),up(),b1,b2,b3,i) -> #idle(F(),closed(),up(),b1,b2,b3,i)
   #16: #busy(F(),closed(),down(),b1,true(),b3,i) -> #idle(F(),closed(),stop(),b1,true(),b3,i)
   #17: #busy(F(),closed(),stop(),true(),false(),b3,i) -> #idle(F(),closed(),down(),true(),false(),b3,i)
   #18: #busy(S(),closed(),down(),b1,b2,false(),i) -> #idle(FS(),closed(),down(),b1,b2,false(),i)
   #19: #busy(S(),d,stop(),b1,b2,true(),i) -> #idle(S(),open(),stop(),b1,b2,false(),i)
   #20: #busy(B(),closed(),stop(),false(),true(),b3,i) -> #idle(B(),closed(),up(),false(),true(),b3,i)
   #21: #busy(S(),closed(),up(),b1,b2,b3,i) -> #idle(S(),closed(),stop(),b1,b2,b3,i)
   #22: #busy(F(),closed(),down(),b1,false(),b3,i) -> #idle(BF(),closed(),down(),b1,false(),b3,i)
   #23: #busy(S(),closed(),stop(),b1,true(),false(),i) -> #idle(S(),closed(),down(),b1,true(),false(),i)
   #24: #busy(F(),closed(),up(),b1,true(),b3,i) -> #idle(F(),closed(),stop(),b1,true(),b3,i)
   #25: #busy(F(),d,stop(),b1,true(),b3,i) -> #idle(F(),open(),stop(),b1,false(),b3,i)
   #26: #busy(B(),d,stop(),true(),b2,b3,i) -> #idle(B(),open(),stop(),false(),b2,b3,i)
   #27: #busy(B(),closed(),down(),b1,b2,b3,i) -> #idle(B(),closed(),stop(),b1,b2,b3,i)
Number of SCCs: 1, DPs: 27, edges: 52
	SCC { #1..27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 4)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 8)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x5, (/ 1 8) + x3, (/ 1 4) + x1}
 false()	weight: (/ 5 8)
closed()	weight: 0
  down()	weight: (/ 3 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 3 4)
     B()	weight: 0
correct()	weight: 0
    FS()	weight: (/ 1 4)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: 0
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x5, (/ 1 8) + x3}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: 0
    up()	weight: (/ 1 4)
    Usable rules: { }
    Removed DPs: #25
Number of SCCs: 1, DPs: 26, edges: 50
	SCC { #1..24 #26 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 11 16)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 13 16) + x4, (/ 7 16) + x3, (/ 1 16) + x2, x1}
 false()	weight: 0
closed()	weight: (/ 9 16)
  down()	weight: (/ 5 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 16)
     B()	weight: (/ 1 8)
correct()	weight: 0
    FS()	weight: (/ 3 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: 0
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 16) + x7, (/ 13 16) + x4, (/ 3 16) + x3, x1}
 empty()	weight: (/ 5 16)
 start(x1)	weight: 0
    BF()	weight: (/ 3 16)
    up()	weight: (/ 3 8)
    Usable rules: { }
    Removed DPs: #26
Number of SCCs: 1, DPs: 25, edges: 48
	SCC { #1..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 4)
     F()	weight: (/ 1 4)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 2) + x6, (/ 1 4) + x1}
 false()	weight: 0
closed()	weight: (/ 9 4)
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 4)
     B()	weight: (/ 1 4)
correct()	weight: 0
    FS()	weight: (/ 1 4)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: 0
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 2) + x6}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 4)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #19
Number of SCCs: 1, DPs: 24, edges: 46
	SCC { #1..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 5 16)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 7 32)
     F()	weight: (/ 1 16)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 2) + x4, (/ 5 32) + x3, (/ 1 16) + x2, (/ 1 16) + x1}
 false()	weight: 0
closed()	weight: (/ 1 4)
  down()	weight: (/ 11 32)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: 0
correct()	weight: 0
    FS()	weight: (/ 11 32)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 17 32)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 7 16) + x7, (/ 1 2) + x4, (/ 1 32) + x3, x2}
 empty()	weight: (/ 1 16)
 start(x1)	weight: 0
    BF()	weight: (/ 7 16)
    up()	weight: (/ 1 16)
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 1, DPs: 23, edges: 44
	SCC { #1..7 #9..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 16)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x6, x2, (/ 1 4) + x1}
 false()	weight: 0
closed()	weight: (/ 3 4)
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 7 16)
correct()	weight: 0
    FS()	weight: (/ 3 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 13 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x6, x2, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 7 16)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 1, DPs: 22, edges: 42
	SCC { #1..7 #9 #11..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 5 8)
     F()	weight: (/ 5 8)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 8) + x4, (/ 3 8) + x3, x2, x1}
 false()	weight: (/ 1 2)
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 3 8)
correct()	weight: 0
    FS()	weight: (/ 5 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 3 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x7, (/ 1 8) + x4, (/ 3 8) + x3, x2, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 5 8)
    up()	weight: (/ 1 8)
    Usable rules: { }
    Removed DPs: #13
Number of SCCs: 1, DPs: 21, edges: 40
	SCC { #1..7 #9 #11 #12 #14..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 4)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 2)
     F()	weight: (/ 1 2)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x3, x2, x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: (/ 1 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 2)
correct()	weight: 0
    FS()	weight: (/ 1 2)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, x3, x2, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 2)
    up()	weight: (/ 3 8)
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 1, DPs: 20, edges: 38
	SCC { #1..4 #6 #7 #9 #11 #12 #14..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: 0
     F()	weight: (/ 3 4)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x6, (/ 1 4) + x3, x2, x1}
 false()	weight: (/ 3 4)
closed()	weight: (/ 1 4)
  down()	weight: (/ 3 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 8)
     B()	weight: (/ 3 4)
correct()	weight: 0
    FS()	weight: (/ 3 4)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x6, x3, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 3 4)
    up()	weight: (/ 1 4)
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 1, DPs: 19, edges: 36
	SCC { #1..4 #6 #9 #11 #12 #14..18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 2)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 3 4)
     F()	weight: (/ 1 4)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x5, x3, x2, x1}
 false()	weight: (/ 3 4)
closed()	weight: (/ 1 4)
  down()	weight: (/ 3 4)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 2)
     B()	weight: 0
correct()	weight: 0
    FS()	weight: (/ 3 4)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 4)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x5, x3, x2, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 4)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #16
Number of SCCs: 1, DPs: 18, edges: 34
	SCC { #1..4 #6 #9 #11 #12 #14 #15 #17 #18 #20..24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 3 8)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 4)
     F()	weight: (/ 1 2)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x6, (/ 1 2) + x5, (/ 1 4) + x3, (/ 1 8) + x2, x1}
 false()	weight: (/ 1 8)
closed()	weight: (/ 1 8)
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 5 8)
correct()	weight: 0
    FS()	weight: (/ 3 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x7, (/ 3 8) + x6, (/ 1 2) + x5, (/ 1 4) + x3, x2, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 5 8)
    up()	weight: (/ 3 8)
    Usable rules: { }
    Removed DPs: #23
Number of SCCs: 1, DPs: 17, edges: 32
	SCC { #1..4 #6 #9 #11 #12 #14 #15 #17 #18 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 9 16)
     F()	weight: (/ 9 16)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 16) + x4, x3, (/ 3 8) + x2, (/ 1 16) + x1}
 false()	weight: (/ 1 8)
closed()	weight: (/ 1 8)
  down()	weight: (/ 11 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 9 16)
     B()	weight: (/ 5 8)
correct()	weight: 0
    FS()	weight: (/ 1 2)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x7, (/ 3 16) + x4, x3, (/ 1 8) + x2, (/ 1 16) + x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 16)
    up()	weight: (/ 5 8)
    Usable rules: { }
    Removed DPs: #6
Number of SCCs: 1, DPs: 16, edges: 30
	SCC { #1..4 #9 #11 #12 #14 #15 #17 #18 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 2)
     F()	weight: (/ 1 2)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: 0
correct()	weight: 0
    FS()	weight: (/ 1 2)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 2)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 2)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 1, DPs: 15, edges: 28
	SCC { #2..4 #9 #11 #12 #14 #15 #17 #18 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 3 32)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 2)
     F()	weight: (/ 1 32)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 3 16) + x6, (/ 15 32) + x3, (/ 3 32) + x2, (/ 1 32) + x1}
 false()	weight: (/ 5 16)
closed()	weight: (/ 1 32)
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 15 32)
     B()	weight: (/ 19 32)
correct()	weight: 0
    FS()	weight: (/ 1 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 32)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 7 32) + x7, (/ 3 16) + x6, (/ 15 32) + x3, (/ 1 16) + x2, (/ 1 32) + x1}
 empty()	weight: (/ 7 32)
 start(x1)	weight: 0
    BF()	weight: 0
    up()	weight: (/ 1 8)
    Usable rules: { }
    Removed DPs: #3 #18
Number of SCCs: 1, DPs: 13, edges: 24
	SCC { #2 #4 #9 #11 #12 #14 #15 #17 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 4)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 3 16)
     F()	weight: (/ 3 16)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 32) + x6, (/ 7 32) + x4, (/ 11 32) + x3, (/ 9 32) + x2, (/ 1 2) + x1}
 false()	weight: (/ 5 32)
closed()	weight: (/ 3 16)
  down()	weight: (/ 5 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 3 8)
     B()	weight: (/ 1 32)
correct()	weight: 0
    FS()	weight: (/ 3 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 32)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 2) + x7, (/ 1 32) + x6, (/ 7 32) + x4, (/ 5 16) + x3, (/ 1 4) + x2, (/ 1 2) + x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 3 16)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #14
Number of SCCs: 1, DPs: 12, edges: 22
	SCC { #2 #4 #9 #11 #12 #15 #17 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 8)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 16)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 8) + x4, (/ 5 16) + x3, (/ 3 16) + x2, x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 4)
     B()	weight: (/ 1 2)
correct()	weight: 0
    FS()	weight: (/ 1 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x7, (/ 1 8) + x4, (/ 5 16) + x3, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 8)
    up()	weight: (/ 1 8)
    Usable rules: { }
    Removed DPs: #17
Number of SCCs: 1, DPs: 11, edges: 20
	SCC { #2 #4 #9 #11 #12 #15 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 1 4)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: 0
     F()	weight: (/ 1 2)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x5, x3, x2, x1}
 false()	weight: 0
closed()	weight: (/ 1 4)
  down()	weight: (/ 1 2)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 1 2)
     B()	weight: (/ 3 4)
correct()	weight: 0
    FS()	weight: 0
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 4)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x5, x3, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 2)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #12
Number of SCCs: 1, DPs: 10, edges: 18
	SCC { #2 #4 #9 #11 #15 #20..22 #24 #27 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: 0
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 1 2) + x3, x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: (/ 1 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 2)
correct()	weight: 0
    FS()	weight: 0
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x7, (/ 1 2) + x3}
 empty()	weight: (/ 1 8)
 start(x1)	weight: 0
    BF()	weight: (/ 1 8)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #27
Number of SCCs: 1, DPs: 9, edges: 16
	SCC { #2 #4 #9 #11 #15 #20..22 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: 0
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 8) + x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: 0
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 2)
correct()	weight: 0
    FS()	weight: (/ 1 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 1 8) + x1}
 empty()	weight: (/ 1 8)
 start(x1)	weight: 0
    BF()	weight: 0
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #9 #11
Number of SCCs: 1, DPs: 7, edges: 12
	SCC { #2 #4 #15 #20..22 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: 0
     F()	weight: (/ 1 8)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 8) + x5, x3, (/ 3 16) + x2, (/ 1 2) + x1}
 false()	weight: (/ 1 4)
closed()	weight: (/ 1 8)
  down()	weight: (/ 9 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 3 16)
correct()	weight: 0
    FS()	weight: (/ 1 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 7 16) + x7, (/ 1 8) + x5, x3, (/ 1 16) + x2, (/ 1 2) + x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: 0
    up()	weight: (/ 5 8)
    Usable rules: { }
    Removed DPs: #22
Number of SCCs: 1, DPs: 6, edges: 10
	SCC { #2 #4 #15 #20 #21 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 9 32)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 17 32)
     F()	weight: (/ 17 32)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 16) + x7, (/ 1 8) + x5, (/ 5 32) + x4, (/ 1 4) + x3, (/ 1 16) + x2, (/ 1 32) + x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: (/ 9 32)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 16)
correct()	weight: 0
    FS()	weight: (/ 1 32)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 32)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 7 32) + x7, (/ 1 8) + x5, (/ 5 32) + x4, x3, (/ 1 32) + x1}
 empty()	weight: (/ 1 32)
 start(x1)	weight: 0
    BF()	weight: (/ 17 32)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #20
Number of SCCs: 1, DPs: 5, edges: 8
	SCC { #2 #4 #15 #21 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 1 4)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 8) + x7, (/ 3 8) + x3, (/ 1 8) + x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: (/ 9 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 4)
correct()	weight: 0
    FS()	weight: (/ 1 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 8) + x7, x1}
 empty()	weight: 0
 start(x1)	weight: 0
    BF()	weight: (/ 1 2)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #15
Number of SCCs: 1, DPs: 4, edges: 6
	SCC { #2 #4 #21 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 5 16)
     F()	weight: (/ 7 16)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 1 8) + x3, (/ 7 16) + x2, (/ 3 16) + x1}
 false()	weight: 0
closed()	weight: 0
  down()	weight: (/ 9 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: 0
     B()	weight: (/ 1 8)
correct()	weight: 0
    FS()	weight: (/ 1 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 3 16) + x7, (/ 1 16) + x3, (/ 7 16) + x2, (/ 3 16) + x1}
 empty()	weight: (/ 1 4)
 start(x1)	weight: 0
    BF()	weight: (/ 1 4)
    up()	weight: (/ 1 2)
    Usable rules: { }
    Removed DPs: #21
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #2 #4 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: (/ 7 8)
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 5 8)
     F()	weight: (/ 1 8)
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 1 4) + x7, (/ 3 8) + x6, (/ 7 4) + x5, (/ 17 8) + x3, 2 + x2, x1}
 false()	weight: (/ 3 4)
closed()	weight: (/ 3 8)
  down()	weight: (/ 9 8)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 11 8)
     B()	weight: (/ 1 4)
correct()	weight: 0
    FS()	weight: (/ 1 8)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 8)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, (/ 15 8) + x7, (/ 3 8) + x6, (/ 7 4) + x5, (/ 7 4) + x3, (/ 15 8) + x2, x1}
 empty()	weight: (/ 1 4)
 start(x1)	weight: 0
    BF()	weight: (/ 1 2)
    up()	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #4 #24 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  stop()	weight: 0
newbuttons(x1,x2,x3,x4)	weight: 0
     S()	weight: (/ 5 16)
     F()	weight: 0
#idle(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 3 16) + x5, (/ 5 16) + x3, (/ 5 16) + x1}
 false()	weight: (/ 3 8)
closed()	weight: 0
  down()	weight: (/ 9 16)
incorrect()	weight: 0
  idle(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  true()	weight: (/ 5 16)
     B()	weight: (/ 1 8)
correct()	weight: 0
    FS()	weight: (/ 1 16)
    or(x1,x2)	weight: 0
  busy(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  open()	weight: (/ 5 16)
#busy(x1,x2,x3,x4,x5,x6,x7)	weight: max{0, x7, (/ 1 16) + x5, (/ 1 4) + x3}
 empty()	weight: (/ 1 8)
 start(x1)	weight: 0
    BF()	weight: (/ 1 4)
    up()	weight: (/ 5 16)
    Usable rules: { }
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES