-- ROBOT2PROOF


Derivation of

Any AS:
(  robot(0,0,[],AS)
 & Acts = OS(blue):AS++[C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C])

Narrowing (11 steps) the preceding tree leads to new ones. The current summand is given by

Any AS:
(  robot(6,2,[M(2),M(2),M(2),R,M(2),L],AS)
 & Acts = OS(blue):AS++[C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C])

Narrowing (11 steps) the preceding summand leads to new ones. The current summand is given by

Any AS:
(  robot(8,10,[M(2),M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L],AS)
 & Acts = OS(blue):AS++[C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C])

Narrowing (111 steps) the preceding summand leads to new ones. The current summand is given by

Any AS:
(  robot(8,6,[M(2),R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,M(2)],AS)
 & Acts = OS(blue):AS++[C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C])

The following solutions were computed:

Acts = [OS(blue),M(2),M(2),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),R,M(2),L,M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,M(2),M(2),C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]

Acts = [OS(blue),M(2),R,M(2),L,R,M(2),L,M(2),M(2),M(2),R,M(2),L,R,M(2),L,R,M(2),L,R,M(2),L,C,O,J(2),R,J(6),circ(2,red),B,J(4),R,J(4),circ(2,red),C]