- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [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 Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_idle -> 7 Marked_busy -> 7 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { busy(F,closed,stop,false,false,false,empty) >= correct ; busy(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) >= idle( F, closed, stop, false, false, false, newbuttons( i1, i2, i3, i)) ; busy(F,closed,stop,false,false,true,i) >= idle(F,closed,up,false,false, true,i) ; busy(F,closed,stop,true,false,b3,i) >= idle(F,closed,down,true,false,b3,i) ; busy(F,closed,up,b1,false,b3,i) >= idle(FS,closed,up,b1,false,b3,i) ; busy(F,closed,up,b1,true,b3,i) >= idle(F,closed,stop,b1,true,b3,i) ; busy(F,closed,down,b1,false,b3,i) >= idle(BF,closed,down,b1,false,b3,i) ; busy(F,closed,down,b1,true,b3,i) >= idle(F,closed,stop,b1,true,b3,i) ; busy(F,open,stop,b1,false,b3,i) >= idle(F,closed,stop,b1,false,b3,i) ; busy(F,d,stop,b1,true,b3,i) >= idle(F,open,stop,b1,false,b3,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(BF,d,stop,b1,b2,b3,i) >= incorrect ; 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(FS,d,stop,b1,b2,b3,i) >= incorrect ; busy(B,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(B,closed,stop,false,false,true,i) >= idle(B,closed,up,false,false, true,i) ; busy(B,closed,stop,false,true,b3,i) >= idle(B,closed,up,false,true,b3,i) ; busy(B,closed,up,false,b2,b3,i) >= idle(BF,closed,up,false,b2,b3,i) ; busy(B,closed,up,true,b2,b3,i) >= idle(B,closed,stop,true,b2,b3,i) ; busy(B,closed,down,b1,b2,b3,i) >= idle(B,closed,stop,b1,b2,b3,i) ; busy(B,open,stop,false,b2,b3,i) >= idle(B,closed,stop,false,b2,b3,i) ; busy(B,d,stop,true,b2,b3,i) >= idle(B,open,stop,false,b2,b3,i) ; busy(S,closed,stop,false,false,false,empty) >= correct ; 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(S,closed,stop,true,false,false,i) >= idle(S,closed,down,true,false, false,i) ; busy(S,closed,stop,b1,true,false,i) >= idle(S,closed,down,b1,true,false,i) ; busy(S,closed,up,b1,b2,b3,i) >= idle(S,closed,stop,b1,b2,b3,i) ; busy(S,closed,down,b1,b2,false,i) >= idle(FS,closed,down,b1,b2,false,i) ; busy(S,closed,down,b1,b2,true,i) >= idle(S,closed,stop,b1,b2,true,i) ; busy(S,open,stop,b1,b2,false,i) >= idle(S,closed,stop,b1,b2,false,i) ; busy(S,d,stop,b1,b2,true,i) >= idle(S,open,stop,b1,b2,false,i) ; busy(fl,open,up,b1,b2,b3,i) >= incorrect ; busy(fl,open,down,b1,b2,b3,i) >= incorrect ; 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) ; or(false,b) >= b ; or(true,b) >= true ; Marked_idle(fl,d,m,b1,b2,b3,empty) >= Marked_busy(fl,d,m,b1,b2,b3,empty) ; Marked_busy(F,closed,stop,false,false,true,i) >= Marked_idle(F,closed, up,false,false,true, i) ; Marked_busy(F,closed,stop,true,false,b3,i) >= Marked_idle(F,closed, down,true,false,b3,i) ; Marked_busy(F,closed,up,b1,false,b3,i) >= Marked_idle(FS,closed,up, b1,false,b3,i) ; Marked_busy(F,closed,up,b1,true,b3,i) >= Marked_idle(F,closed,stop, b1,true,b3,i) ; Marked_busy(F,closed,down,b1,false,b3,i) >= Marked_idle(BF,closed,down, b1,false,b3,i) ; Marked_busy(F,closed,down,b1,true,b3,i) >= Marked_idle(F,closed,stop, b1,true,b3,i) ; Marked_busy(F,open,stop,b1,false,b3,i) >= Marked_idle(F,closed,stop, b1,false,b3,i) ; Marked_busy(F,d,stop,b1,true,b3,i) >= Marked_idle(F,open,stop,b1,false,b3,i) ; Marked_busy(BF,closed,up,b1,b2,b3,i) >= Marked_idle(F,closed,up,b1,b2,b3,i) ; Marked_busy(BF,closed,down,b1,b2,b3,i) >= Marked_idle(B,closed,down, b1,b2,b3,i) ; Marked_busy(FS,closed,up,b1,b2,b3,i) >= Marked_idle(S,closed,up,b1,b2,b3,i) ; Marked_busy(FS,closed,down,b1,b2,b3,i) >= Marked_idle(F,closed,down, b1,b2,b3,i) ; Marked_busy(B,closed,stop,false,false,true,i) >= Marked_idle(B,closed, up,false,false,true, i) ; Marked_busy(B,closed,stop,false,true,b3,i) >= Marked_idle(B,closed, up,false,true,b3,i) ; Marked_busy(B,closed,up,false,b2,b3,i) >= Marked_idle(BF,closed,up, false,b2,b3,i) ; Marked_busy(B,closed,up,true,b2,b3,i) >= Marked_idle(B,closed,stop, true,b2,b3,i) ; Marked_busy(B,closed,down,b1,b2,b3,i) >= Marked_idle(B,closed,stop, b1,b2,b3,i) ; Marked_busy(B,open,stop,false,b2,b3,i) >= Marked_idle(B,closed,stop, false,b2,b3,i) ; Marked_busy(B,d,stop,true,b2,b3,i) >= Marked_idle(B,open,stop,false,b2,b3,i) ; Marked_busy(S,closed,stop,true,false,false,i) >= Marked_idle(S,closed, down,true,false,false, i) ; Marked_busy(S,closed,stop,b1,true,false,i) >= Marked_idle(S,closed, down,b1,true,false,i) ; Marked_busy(S,closed,up,b1,b2,b3,i) >= Marked_idle(S,closed,stop,b1,b2,b3,i) ; Marked_busy(S,closed,down,b1,b2,false,i) >= Marked_idle(FS,closed,down, b1,b2,false,i) ; Marked_busy(S,closed,down,b1,b2,true,i) >= Marked_idle(S,closed,stop, b1,b2,true,i) ; Marked_busy(S,open,stop,b1,b2,false,i) >= Marked_idle(S,closed,stop, b1,b2,false,i) ; Marked_busy(S,d,stop,b1,b2,true,i) >= Marked_idle(S,open,stop,b1,b2,false,i) ; } + Disjunctions:{ { Marked_idle(fl,d,m,b1,b2,b3,empty) > Marked_busy(fl,d,m,b1,b2,b3,empty) ; } { Marked_busy(F,closed,stop,false,false,true,i) > Marked_idle(F,closed, up,false,false,true, i) ; } { Marked_busy(F,closed,stop,true,false,b3,i) > Marked_idle(F,closed,down, true,false,b3,i) ; } { Marked_busy(F,closed,up,b1,false,b3,i) > Marked_idle(FS,closed,up,b1, false,b3,i) ; } { Marked_busy(F,closed,up,b1,true,b3,i) > Marked_idle(F,closed,stop,b1, true,b3,i) ; } { Marked_busy(F,closed,down,b1,false,b3,i) > Marked_idle(BF,closed,down, b1,false,b3,i) ; } { Marked_busy(F,closed,down,b1,true,b3,i) > Marked_idle(F,closed,stop, b1,true,b3,i) ; } { Marked_busy(F,open,stop,b1,false,b3,i) > Marked_idle(F,closed,stop, b1,false,b3,i) ; } { Marked_busy(F,d,stop,b1,true,b3,i) > Marked_idle(F,open,stop,b1,false,b3,i) ; } { Marked_busy(BF,closed,up,b1,b2,b3,i) > Marked_idle(F,closed,up,b1,b2,b3,i) ; } { Marked_busy(BF,closed,down,b1,b2,b3,i) > Marked_idle(B,closed,down, b1,b2,b3,i) ; } { Marked_busy(FS,closed,up,b1,b2,b3,i) > Marked_idle(S,closed,up,b1,b2,b3,i) ; } { Marked_busy(FS,closed,down,b1,b2,b3,i) > Marked_idle(F,closed,down, b1,b2,b3,i) ; } { Marked_busy(B,closed,stop,false,false,true,i) > Marked_idle(B,closed, up,false,false,true, i) ; } { Marked_busy(B,closed,stop,false,true,b3,i) > Marked_idle(B,closed,up, false,true,b3,i) ; } { Marked_busy(B,closed,up,false,b2,b3,i) > Marked_idle(BF,closed,up,false, b2,b3,i) ; } { Marked_busy(B,closed,up,true,b2,b3,i) > Marked_idle(B,closed,stop,true, b2,b3,i) ; } { Marked_busy(B,closed,down,b1,b2,b3,i) > Marked_idle(B,closed,stop,b1,b2,b3,i) ; } { Marked_busy(B,open,stop,false,b2,b3,i) > Marked_idle(B,closed,stop, false,b2,b3,i) ; } { Marked_busy(B,d,stop,true,b2,b3,i) > Marked_idle(B,open,stop,false,b2,b3,i) ; } { Marked_busy(S,closed,stop,true,false,false,i) > Marked_idle(S,closed, down,true,false,false, i) ; } { Marked_busy(S,closed,stop,b1,true,false,i) > Marked_idle(S,closed,down, b1,true,false,i) ; } { Marked_busy(S,closed,up,b1,b2,b3,i) > Marked_idle(S,closed,stop,b1,b2,b3,i) ; } { Marked_busy(S,closed,down,b1,b2,false,i) > Marked_idle(FS,closed,down, b1,b2,false,i) ; } { Marked_busy(S,closed,down,b1,b2,true,i) > Marked_idle(S,closed,stop, b1,b2,true,i) ; } { Marked_busy(S,open,stop,b1,b2,false,i) > Marked_idle(S,closed,stop, b1,b2,false,i) ; } { Marked_busy(S,d,stop,b1,b2,true,i) > Marked_idle(S,open,stop,b1,b2,false,i) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: busy(F,closed,stop,false,false,false,empty) >= correct constraint: busy(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) >= idle(F,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) constraint: busy(F,closed,stop,false,false,true,i) >= idle(F,closed,up, false,false,true, i) constraint: busy(F,closed,stop,true,false,b3,i) >= idle(F,closed,down, true,false,b3,i) constraint: busy(F,closed,up,b1,false,b3,i) >= idle(FS,closed,up,b1,false,b3,i) constraint: busy(F,closed,up,b1,true,b3,i) >= idle(F,closed,stop,b1,true,b3,i) constraint: busy(F,closed,down,b1,false,b3,i) >= idle(BF,closed,down, b1,false,b3,i) constraint: busy(F,closed,down,b1,true,b3,i) >= idle(F,closed,stop,b1, true,b3,i) constraint: busy(F,open,stop,b1,false,b3,i) >= idle(F,closed,stop,b1, false,b3,i) constraint: busy(F,d,stop,b1,true,b3,i) >= idle(F,open,stop,b1,false,b3,i) constraint: busy(BF,closed,up,b1,b2,b3,i) >= idle(F,closed,up,b1,b2,b3,i) constraint: busy(BF,closed,down,b1,b2,b3,i) >= idle(B,closed,down,b1,b2,b3,i) constraint: busy(BF,d,stop,b1,b2,b3,i) >= incorrect constraint: busy(FS,closed,up,b1,b2,b3,i) >= idle(S,closed,up,b1,b2,b3,i) constraint: busy(FS,closed,down,b1,b2,b3,i) >= idle(F,closed,down,b1,b2,b3,i) constraint: busy(FS,d,stop,b1,b2,b3,i) >= incorrect constraint: busy(B,closed,stop,false,false,false,empty) >= correct constraint: busy(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) >= idle(B,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) constraint: busy(B,closed,stop,false,false,true,i) >= idle(B,closed,up, false,false,true, i) constraint: busy(B,closed,stop,false,true,b3,i) >= idle(B,closed,up,false, true,b3,i) constraint: busy(B,closed,up,false,b2,b3,i) >= idle(BF,closed,up,false,b2,b3,i) constraint: busy(B,closed,up,true,b2,b3,i) >= idle(B,closed,stop,true,b2,b3,i) constraint: busy(B,closed,down,b1,b2,b3,i) >= idle(B,closed,stop,b1,b2,b3,i) constraint: busy(B,open,stop,false,b2,b3,i) >= idle(B,closed,stop,false, b2,b3,i) constraint: busy(B,d,stop,true,b2,b3,i) >= idle(B,open,stop,false,b2,b3,i) constraint: busy(S,closed,stop,false,false,false,empty) >= correct constraint: busy(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) >= idle(S,closed,stop,false,false,false,newbuttons(i1,i2,i3,i)) constraint: busy(S,closed,stop,true,false,false,i) >= idle(S,closed,down, true,false,false, i) constraint: busy(S,closed,stop,b1,true,false,i) >= idle(S,closed,down, b1,true,false,i) constraint: busy(S,closed,up,b1,b2,b3,i) >= idle(S,closed,stop,b1,b2,b3,i) constraint: busy(S,closed,down,b1,b2,false,i) >= idle(FS,closed,down, b1,b2,false,i) constraint: busy(S,closed,down,b1,b2,true,i) >= idle(S,closed,stop,b1, b2,true,i) constraint: busy(S,open,stop,b1,b2,false,i) >= idle(S,closed,stop,b1, b2,false,i) constraint: busy(S,d,stop,b1,b2,true,i) >= idle(S,open,stop,b1,b2,false,i) constraint: busy(fl,open,up,b1,b2,b3,i) >= incorrect constraint: busy(fl,open,down,b1,b2,b3,i) >= incorrect constraint: start(i) >= busy(F,closed,stop,false,false,false,i) constraint: idle(fl,d,m,b1,b2,b3,empty) >= busy(fl,d,m,b1,b2,b3,empty) constraint: 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) constraint: or(false,b) >= b constraint: or(true,b) >= true constraint: Marked_idle(fl,d,m,b1,b2,b3,empty) >= Marked_busy(fl,d,m, b1,b2,b3,empty) constraint: Marked_busy(F,closed,stop,false,false,true,i) >= Marked_idle( F,closed, up,false, false,true, i) constraint: Marked_busy(F,closed,stop,true,false,b3,i) >= Marked_idle( F,closed,down, true,false, b3,i) constraint: Marked_busy(F,closed,up,b1,false,b3,i) >= Marked_idle(FS, closed,up,b1,false, b3,i) constraint: Marked_busy(F,closed,up,b1,true,b3,i) >= Marked_idle(F,closed, stop,b1,true,b3, i) constraint: Marked_busy(F,closed,down,b1,false,b3,i) >= Marked_idle(BF, closed,down, b1,false,b3, i) constraint: Marked_busy(F,closed,down,b1,true,b3,i) >= Marked_idle(F, closed,stop,b1, true,b3,i) constraint: Marked_busy(F,open,stop,b1,false,b3,i) >= Marked_idle(F,closed, stop,b1,false, b3,i) constraint: Marked_busy(F,d,stop,b1,true,b3,i) >= Marked_idle(F,open, stop,b1,false,b3,i) constraint: Marked_busy(BF,closed,up,b1,b2,b3,i) >= Marked_idle(F,closed, up,b1,b2,b3,i) constraint: Marked_busy(BF,closed,down,b1,b2,b3,i) >= Marked_idle(B,closed, down,b1,b2,b3, i) constraint: Marked_busy(FS,closed,up,b1,b2,b3,i) >= Marked_idle(S,closed, up,b1,b2,b3,i) constraint: Marked_busy(FS,closed,down,b1,b2,b3,i) >= Marked_idle(F,closed, down,b1,b2,b3, i) constraint: Marked_busy(B,closed,stop,false,false,true,i) >= Marked_idle( B,closed, up,false, false,true, i) constraint: Marked_busy(B,closed,stop,false,true,b3,i) >= Marked_idle( B,closed,up, false,true, b3,i) constraint: Marked_busy(B,closed,up,false,b2,b3,i) >= Marked_idle(BF, closed,up,false, b2,b3,i) constraint: Marked_busy(B,closed,up,true,b2,b3,i) >= Marked_idle(B,closed, stop,true,b2,b3, i) constraint: Marked_busy(B,closed,down,b1,b2,b3,i) >= Marked_idle(B,closed, stop,b1,b2,b3,i) constraint: Marked_busy(B,open,stop,false,b2,b3,i) >= Marked_idle(B,closed, stop,false,b2, b3,i) constraint: Marked_busy(B,d,stop,true,b2,b3,i) >= Marked_idle(B,open, stop,false,b2,b3,i) constraint: Marked_busy(S,closed,stop,true,false,false,i) >= Marked_idle( S,closed, down,true, false,false, i) constraint: Marked_busy(S,closed,stop,b1,true,false,i) >= Marked_idle( S,closed,down, b1,true,false, i) constraint: Marked_busy(S,closed,up,b1,b2,b3,i) >= Marked_idle(S,closed, stop,b1,b2,b3,i) constraint: Marked_busy(S,closed,down,b1,b2,false,i) >= Marked_idle(FS, closed,down, b1,b2,false, i) constraint: Marked_busy(S,closed,down,b1,b2,true,i) >= Marked_idle(S, closed,stop,b1, b2,true,i) constraint: Marked_busy(S,open,stop,b1,b2,false,i) >= Marked_idle(S,closed, stop,b1,b2,false, i) constraint: Marked_busy(S,d,stop,b1,b2,true,i) >= Marked_idle(S,open, stop,b1,b2,false,i) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> -->