Solution of B&L inching towards solution of BB&L in Clingo

This works with Clingo:

role(robot).

time(1..7).

base(step(1..7)).

base(p).

base(q).

base(r).

true(step(1),1).

legal(robot,a,T) :- time(T), not terminal(T).

input(robot,a).

legal(robot,b,T) :- time(T), not terminal(T).

input(robot,b).

legal(robot,c,T) :- time(T), not terminal(T).

input(robot,c).

true(p,T+1) :- time(T), does(robot,a,T), not true(p,T).

true(p,T+1) :- time(T), does(robot,b,T), true(q,T).

true(p,T+1) :- time(T), true(p,T), not does(robot,a,T), not does(robot,b,T).

true(q,T+1) :- time(T), does(robot,b,T), true(p,T).

true(q,T+1) :- time(T), does(robot,c,T), true(r,T).

true(q,T+1) :- time(T), true(q,T), not does(robot,b,T), not does(robot,c,T).

true(r,T+1) :- time(T), does(robot,c,T), true(q,T).

true(r,T+1) :- time(T), true(r,T), not does(robot,c,T).

true(step(Y),T+1) :- time(T), true(step(X),T), successor(X,Y).

goal(robot,100,T) :- time(T), row(T).

goal(robot,0,T) :- time(T), not row(T).

terminal(T) :- time(T), row(T).

terminal(T) :- time(T), true(step(7),T).

row(T) :- time(T), true(p,T), true(q,T), true(r,T).

successor(1,2).

successor(2,3).

successor(3,4).

successor(4,5).

successor(5,6).

successor(6,7).

:- does(R,M,T), not legal(R,M,T).

:- 0{ terminal(T) : time(T) }0.

terminal(7).

goal(robot,100,7).

not goal(robot,0,7).

:- terminal(T), role(robot), not goal(robot,100,T).

1{ does(robot,a,1); does(robot,b,1); does(robot,c,1) }1 :- time(1).

1{ does(robot,a,2); does(robot,b,2); does(robot,c,2) }1 :- time(2).

1{ does(robot,a,3); does(robot,b,3); does(robot,c,3) }1 :- time(3).

1{ does(robot,a,4); does(robot,b,4); does(robot,c,4) }1 :- time(4).

1{ does(robot,a,5); does(robot,b,5); does(robot,c,5) }1 :- time(5).

1{ does(robot,a,6); does(robot,b,6); does(robot,c,6) }1 :- time(6).

Getting the uniqueness constraints per move at the end for multiple BB&L is challenging, the latest Clingo is tricky and somewhat undocumented it seems.