TORPAcyc is applied to the string rewriting system b b -> c c c c c -> b c b -> b b b Arctic matrix interpretation interpretation of b: / 1 1 \ \ 1 1 / interpretation of c: / 0 2 \ \ - 0 / remove rule 3 continue with: b b -> c c c c c -> interpretation of b: 8 interpretation of c: 1 remove rule 2 continue with: b b -> c c c c interpretation of b: 10 interpretation of c: 0 remove rule 1 termination has been proved