YES Problem: C(C(x1)) -> c(c(x1)) c(c(c(c(x1)))) -> x1 b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 c(c(C(C(x1)))) -> x1 C(C(c(c(x1)))) -> x1 Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [B](x0) = x0, [b](x0) = x0, [c](x0) = x0, [C](x0) = 2x0 orientation: C(C(x1)) = 4x1 >= x1 = c(c(x1)) c(c(c(c(x1)))) = x1 >= x1 = x1 b(b(b(b(x1)))) = x1 >= x1 = B(B(x1)) B(B(B(B(x1)))) = x1 >= x1 = b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) = x1 >= x1 = B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) = x1 >= x1 = x1 B(B(b(b(x1)))) = x1 >= x1 = x1 c(c(C(C(x1)))) = 4x1 >= x1 = x1 C(C(c(c(x1)))) = 4x1 >= x1 = x1 problem: c(c(c(c(x1)))) -> x1 b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 Arctic Interpretation Processor: dimension: 1 interpretation: [B](x0) = x0, [b](x0) = x0, [c](x0) = 2x0 orientation: c(c(c(c(x1)))) = 8x1 >= x1 = x1 b(b(b(b(x1)))) = x1 >= x1 = B(B(x1)) B(B(B(B(x1)))) = x1 >= x1 = b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) = 12x1 >= 12x1 = B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) = x1 >= x1 = x1 B(B(b(b(x1)))) = x1 >= x1 = x1 problem: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 DP Processor: DPs: b#(b(b(b(x1)))) -> B#(x1) b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(x1) B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 TDG Processor: DPs: b#(b(b(b(x1)))) -> B#(x1) b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(x1) B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 graph: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) -> B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) -> B#(B(B(B(x1)))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) -> B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(B(c(c(b(b(x1)))))) -> B#(B(B(B(x1)))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) -> B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(c(c(B(B(c(c(b(b(x1))))))))))))) -> B#(B(B(B(x1)))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) -> B#(B(B(B(x1)))) -> b#(b(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B#(c(c(b(b(x1))))) -> B#(B(B(B(x1)))) -> b#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) -> b#(b(b(b(x1)))) -> B#(B(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(c(c(B(B(c(c(b(b(x1)))))))))) -> b#(b(b(b(x1)))) -> B#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(B(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) -> b#(b(b(b(x1)))) -> B#(B(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(c(c(B(B(c(c(b(b(x1))))))))) -> b#(b(b(b(x1)))) -> B#(x1) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(x1)) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(x1) B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> B#(x1) B#(B(B(B(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> B#(x1) b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> B#(B(x1)) -> B#(B(B(B(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> B#(x1) -> B#(B(B(B(x1)))) -> b#(x1) SCC Processor: #sccs: 2 #rules: 10 #arcs: 108/324 DPs: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 Arctic Interpretation Processor: dimension: 1 usable rules: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 interpretation: [c#](x0) = x0, [B](x0) = x0, [b](x0) = x0, [c](x0) = 4x0 orientation: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= 8x1 = c#(B(B(c(c(b(b(x1))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= x1 = c#(b(b(x1))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= 4x1 = c#(c(b(b(x1)))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= 12x1 = c#(c(B(B(c(c(b(b(x1)))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= 16x1 = c#(b(b(c(c(B(B(c(c(b(b(x1))))))))))) c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = 20x1 >= 20x1 = c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) b(b(b(b(x1)))) = x1 >= x1 = B(B(x1)) B(B(B(B(x1)))) = x1 >= x1 = b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) = 24x1 >= 24x1 = B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) = x1 >= x1 = x1 B(B(b(b(x1)))) = x1 >= x1 = x1 problem: DPs: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 Restore Modifier: DPs: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 EDG Processor: DPs: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 graph: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) -> c#(c(B(B(c(c(b(b(c(c(x1)))))))))) -> c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) Matrix Interpretation Processor: dim=4 interpretation: [c#](x0) = [0 0 1 0]x0, [0 1 0 0] [0 0 1 0] [B](x0) = [1 0 0 0]x0 [0 0 0 1] , [0 0 1 0] [1 0 0 0] [b](x0) = [0 1 0 0]x0 [0 0 0 1] , [0 0 0 0] [0] [0 0 0 1] [0] [c](x0) = [0 0 1 0]x0 + [0] [0 0 0 0] [1] orientation: c#(c(B(B(c(c(b(b(c(c(x1)))))))))) = [1] >= [0] = c#(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))) [0 0 1 0] [0 0 1 0] [1 0 0 0] [1 0 0 0] b(b(b(b(x1)))) = [0 1 0 0]x1 >= [0 1 0 0]x1 = B(B(x1)) [0 0 0 1] [0 0 0 1] [0 1 0 0] [0 1 0 0] [0 0 1 0] [0 0 1 0] B(B(B(B(x1)))) = [1 0 0 0]x1 >= [1 0 0 0]x1 = b(b(x1)) [0 0 0 1] [0 0 0 1] [0] [0] [1] [0] c(c(B(B(c(c(b(b(c(c(x1)))))))))) = [1] >= [1] = B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) [1] [1] b(b(B(B(x1)))) = x1 >= x1 = x1 B(B(b(b(x1)))) = x1 >= x1 = x1 problem: DPs: TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 Qed DPs: b#(b(b(b(x1)))) -> B#(x1) B#(B(B(B(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(b(x1)) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 Usable Rule Processor: DPs: b#(b(b(b(x1)))) -> B#(x1) B#(B(B(B(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> B#(B(x1)) B#(B(B(B(x1)))) -> b#(b(x1)) TRS: B(B(B(B(x1)))) -> b(b(x1)) B(B(b(b(x1)))) -> x1 b(b(b(b(x1)))) -> B(B(x1)) b(b(B(B(x1)))) -> x1 Arctic Interpretation Processor: dimension: 1 usable rules: B(B(B(B(x1)))) -> b(b(x1)) B(B(b(b(x1)))) -> x1 b(b(b(b(x1)))) -> B(B(x1)) b(b(B(B(x1)))) -> x1 interpretation: [B#](x0) = x0 + 0, [b#](x0) = 5x0, [B](x0) = 3x0 + 0, [b](x0) = 2x0 + 1 orientation: b#(b(b(b(x1)))) = 11x1 + 10 >= x1 + 0 = B#(x1) B#(B(B(B(x1)))) = 9x1 + 6 >= 5x1 = b#(x1) b#(b(b(b(x1)))) = 11x1 + 10 >= 3x1 + 0 = B#(B(x1)) B#(B(B(B(x1)))) = 9x1 + 6 >= 7x1 + 6 = b#(b(x1)) B(B(B(B(x1)))) = 12x1 + 9 >= 4x1 + 3 = b(b(x1)) B(B(b(b(x1)))) = 10x1 + 9 >= x1 = x1 b(b(b(b(x1)))) = 8x1 + 7 >= 6x1 + 3 = B(B(x1)) b(b(B(B(x1)))) = 10x1 + 7 >= x1 = x1 problem: DPs: B#(B(B(B(x1)))) -> b#(b(x1)) TRS: B(B(B(B(x1)))) -> b(b(x1)) B(B(b(b(x1)))) -> x1 b(b(b(b(x1)))) -> B(B(x1)) b(b(B(B(x1)))) -> x1 Restore Modifier: DPs: B#(B(B(B(x1)))) -> b#(b(x1)) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 EDG Processor: DPs: B#(B(B(B(x1)))) -> b#(b(x1)) TRS: b(b(b(b(x1)))) -> B(B(x1)) B(B(B(B(x1)))) -> b(b(x1)) c(c(B(B(c(c(b(b(c(c(x1)))))))))) -> B(B(c(c(b(b(c(c(B(B(c(c(b(b(x1)))))))))))))) b(b(B(B(x1)))) -> x1 B(B(b(b(x1)))) -> x1 graph: Qed