YES Problem: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Proof: DP Processor: DPs: 5#(9(x1)) -> 5#(x1) 5#(9(x1)) -> 2#(6(5(x1))) 3#(5(x1)) -> 7#(x1) 3#(5(x1)) -> 9#(7(x1)) 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 2#(x1) 9#(x1) -> 5#(0(2(x1))) 8#(8(4(x1))) -> 9#(x1) 7#(1(x1)) -> 9#(x1) 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) TDG Processor: DPs: 5#(9(x1)) -> 5#(x1) 5#(9(x1)) -> 2#(6(5(x1))) 3#(5(x1)) -> 7#(x1) 3#(5(x1)) -> 9#(7(x1)) 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 2#(x1) 9#(x1) -> 5#(0(2(x1))) 8#(8(4(x1))) -> 9#(x1) 7#(1(x1)) -> 9#(x1) 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1))) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(x1) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(x1) 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 5#(0(2(x1))) -> 5#(9(x1)) -> 2#(6(5(x1))) 9#(x1) -> 5#(0(2(x1))) -> 5#(9(x1)) -> 5#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) 5#(9(x1)) -> 2#(6(5(x1))) -> 2#(6(x1)) -> 3#(x1) 5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 2#(6(5(x1))) 5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 5#(x1) 3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 7#(x1) 3#(5(x1)) -> 8#(9(7(x1))) -> 8#(8(4(x1))) -> 9#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 5#(0(2(x1))) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1) 3#(5(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 5#(0(2(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) EDG Processor: DPs: 5#(9(x1)) -> 5#(x1) 5#(9(x1)) -> 2#(6(5(x1))) 3#(5(x1)) -> 7#(x1) 3#(5(x1)) -> 9#(7(x1)) 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 2#(x1) 9#(x1) -> 5#(0(2(x1))) 8#(8(4(x1))) -> 9#(x1) 7#(1(x1)) -> 9#(x1) 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(x1) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(x1) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1))) 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 5#(9(x1)) -> 2#(6(5(x1))) -> 2#(6(x1)) -> 3#(x1) 5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 5#(x1) 5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 2#(6(5(x1))) 3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 3#(5(x1)) -> 8#(9(7(x1))) -> 8#(8(4(x1))) -> 9#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 5#(0(2(x1))) 3#(5(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 5#(0(2(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) SCC Processor: #sccs: 2 #rules: 16 #arcs: 69/324 DPs: 5#(9(x1)) -> 5#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [5#](x0) = 2x0, [0](x0) = 0, [8](x0) = -16x0 + 0, [7](x0) = 0, [2](x0) = x0, [6](x0) = 0, [5](x0) = x0 + 0, [9](x0) = 1x0 + 0, [4](x0) = 0, [3](x0) = x0, [1](x0) = 0 orientation: 5#(9(x1)) = 3x1 + 2 >= 2x1 = 5#(x1) 3(1(x1)) = 0 >= 0 = 4(1(x1)) 5(9(x1)) = 1x1 + 0 >= 0 = 2(6(5(x1))) 3(5(x1)) = x1 + 0 >= 0 = 8(9(7(x1))) 9(x1) = 1x1 + 0 >= x1 = 3(2(3(x1))) 8(4(x1)) = 0 >= 0 = 6(x1) 2(6(x1)) = 0 >= 0 = 4(3(x1)) 3(8(x1)) = -16x1 + 0 >= 0 = 3(2(7(x1))) 9(x1) = 1x1 + 0 >= 0 = 5(0(2(x1))) 8(8(4(x1))) = 0 >= 0 = 1(9(x1)) 7(1(x1)) = 0 >= 0 = 6(9(x1)) 3(9(x1)) = 1x1 + 0 >= 1x1 + 0 = 9(3(x1)) 7(5(x1)) = 0 >= 0 = 1(0(x1)) problem: DPs: TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Qed DPs: 8#(8(4(x1))) -> 9#(x1) 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 8#(9(7(x1))) 3#(5(x1)) -> 9#(7(x1)) 3#(5(x1)) -> 7#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [8#](x0) = x0 + 0, [9#](x0) = x0 + 0, [7#](x0) = x0 + 0, [2#](x0) = x0, [3#](x0) = x0, [0](x0) = 0, [8](x0) = x0 + 2, [7](x0) = x0 + 2, [2](x0) = x0 + 0, [6](x0) = x0, [5](x0) = 2x0 + 2, [9](x0) = x0 + 2, [4](x0) = x0, [3](x0) = x0 + 0, [1](x0) = x0 orientation: 8#(8(4(x1))) = x1 + 2 >= x1 + 0 = 9#(x1) 9#(x1) = x1 + 0 >= x1 = 2#(x1) 2#(6(x1)) = x1 >= x1 = 3#(x1) 3#(9(x1)) = x1 + 2 >= x1 + 0 = 9#(3(x1)) 9#(x1) = x1 + 0 >= x1 + 0 = 3#(2(3(x1))) 3#(9(x1)) = x1 + 2 >= x1 = 3#(x1) 3#(8(x1)) = x1 + 2 >= x1 + 2 = 3#(2(7(x1))) 3#(8(x1)) = x1 + 2 >= x1 + 2 = 2#(7(x1)) 3#(8(x1)) = x1 + 2 >= x1 + 0 = 7#(x1) 7#(1(x1)) = x1 + 0 >= x1 + 0 = 9#(x1) 9#(x1) = x1 + 0 >= x1 + 0 = 2#(3(x1)) 9#(x1) = x1 + 0 >= x1 = 3#(x1) 3#(5(x1)) = 2x1 + 2 >= x1 + 2 = 8#(9(7(x1))) 3#(5(x1)) = 2x1 + 2 >= x1 + 2 = 9#(7(x1)) 3#(5(x1)) = 2x1 + 2 >= x1 + 0 = 7#(x1) 3(1(x1)) = x1 + 0 >= x1 = 4(1(x1)) 5(9(x1)) = 2x1 + 4 >= 2x1 + 2 = 2(6(5(x1))) 3(5(x1)) = 2x1 + 2 >= x1 + 2 = 8(9(7(x1))) 9(x1) = x1 + 2 >= x1 + 0 = 3(2(3(x1))) 8(4(x1)) = x1 + 2 >= x1 = 6(x1) 2(6(x1)) = x1 + 0 >= x1 + 0 = 4(3(x1)) 3(8(x1)) = x1 + 2 >= x1 + 2 = 3(2(7(x1))) 9(x1) = x1 + 2 >= 2 = 5(0(2(x1))) 8(8(4(x1))) = x1 + 2 >= x1 + 2 = 1(9(x1)) 7(1(x1)) = x1 + 2 >= x1 + 2 = 6(9(x1)) 3(9(x1)) = x1 + 2 >= x1 + 2 = 9(3(x1)) 7(5(x1)) = 2x1 + 2 >= 0 = 1(0(x1)) problem: DPs: 8#(8(4(x1))) -> 9#(x1) 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 8#(9(7(x1))) 3#(5(x1)) -> 9#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) EDG Processor: DPs: 8#(8(4(x1))) -> 9#(x1) 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 8#(9(7(x1))) 3#(5(x1)) -> 9#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(x1) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(x1) 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 3#(5(x1)) -> 8#(9(7(x1))) -> 8#(8(4(x1))) -> 9#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) Matrix Interpretation Processor: dim=3 interpretation: [8#](x0) = [1 0 0]x0, [9#](x0) = [0], [7#](x0) = [0], [2#](x0) = [0], [3#](x0) = [0], [0] [0](x0) = [0] [1], [0 0 1] [8](x0) = [0 0 1]x0 [0 0 1] , [0 0 0] [0] [7](x0) = [0 1 0]x0 + [1] [0 1 0] [0], [0 0 1] [2](x0) = [0 0 0]x0 [0 0 1] , [0] [6](x0) = [0] [1], [0 1 0] [5](x0) = [0 0 1]x0 [0 1 0] , [0] [9](x0) = [1] [0], [0] [4](x0) = [0] [1], [0 0 0] [3](x0) = [0 1 0]x0 [0 1 0] , [0] [1](x0) = [1] [0] orientation: 8#(8(4(x1))) = [1] >= [0] = 9#(x1) 9#(x1) = [0] >= [0] = 2#(x1) 2#(6(x1)) = [0] >= [0] = 3#(x1) 3#(9(x1)) = [0] >= [0] = 9#(3(x1)) 9#(x1) = [0] >= [0] = 3#(2(3(x1))) 3#(9(x1)) = [0] >= [0] = 3#(x1) 3#(8(x1)) = [0] >= [0] = 3#(2(7(x1))) 3#(8(x1)) = [0] >= [0] = 2#(7(x1)) 3#(8(x1)) = [0] >= [0] = 7#(x1) 7#(1(x1)) = [0] >= [0] = 9#(x1) 9#(x1) = [0] >= [0] = 2#(3(x1)) 9#(x1) = [0] >= [0] = 3#(x1) 3#(5(x1)) = [0] >= [0] = 8#(9(7(x1))) 3#(5(x1)) = [0] >= [0] = 9#(7(x1)) [0] [0] 3(1(x1)) = [1] >= [0] = 4(1(x1)) [1] [1] [1] [1] 5(9(x1)) = [0] >= [0] = 2(6(5(x1))) [1] [1] [0 0 0] [0] 3(5(x1)) = [0 0 1]x1 >= [0] = 8(9(7(x1))) [0 0 1] [0] [0] [0] 9(x1) = [1] >= [0] = 3(2(3(x1))) [0] [0] [1] [0] 8(4(x1)) = [1] >= [0] = 6(x1) [1] [1] [1] [0] 2(6(x1)) = [0] >= [0] = 4(3(x1)) [1] [1] [0 0 0] [0] 3(8(x1)) = [0 0 1]x1 >= [0] = 3(2(7(x1))) [0 0 1] [0] [0] [0] 9(x1) = [1] >= [1] = 5(0(2(x1))) [0] [0] [1] [0] 8(8(4(x1))) = [1] >= [1] = 1(9(x1)) [1] [0] [0] [0] 7(1(x1)) = [2] >= [0] = 6(9(x1)) [1] [1] [0] [0] 3(9(x1)) = [1] >= [1] = 9(3(x1)) [1] [0] [0 0 0] [0] [0] 7(5(x1)) = [0 0 1]x1 + [1] >= [1] = 1(0(x1)) [0 0 1] [0] [0] problem: DPs: 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 8#(9(7(x1))) 3#(5(x1)) -> 9#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) EDG Processor: DPs: 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 2#(3(x1)) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 8#(9(7(x1))) 3#(5(x1)) -> 9#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) SCC Processor: #sccs: 1 #rules: 12 #arcs: 51/169 DPs: 9#(x1) -> 2#(3(x1)) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 2#(x1) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 3#(x1) 3#(5(x1)) -> 9#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = x0, [7#](x0) = x0, [2#](x0) = x0, [3#](x0) = x0, [0](x0) = 2, [8](x0) = x0 + 8, [7](x0) = x0 + 4, [2](x0) = x0, [6](x0) = x0 + 0, [5](x0) = 1x0 + 8, [9](x0) = x0 + 8, [4](x0) = x0 + 0, [3](x0) = x0, [1](x0) = x0 + 8 orientation: 9#(x1) = x1 >= x1 = 2#(3(x1)) 2#(6(x1)) = x1 + 0 >= x1 = 3#(x1) 3#(9(x1)) = x1 + 8 >= x1 = 9#(3(x1)) 9#(x1) = x1 >= x1 = 2#(x1) 9#(x1) = x1 >= x1 = 3#(2(3(x1))) 3#(9(x1)) = x1 + 8 >= x1 = 3#(x1) 3#(8(x1)) = x1 + 8 >= x1 + 4 = 3#(2(7(x1))) 3#(8(x1)) = x1 + 8 >= x1 + 4 = 2#(7(x1)) 3#(8(x1)) = x1 + 8 >= x1 = 7#(x1) 7#(1(x1)) = x1 + 8 >= x1 = 9#(x1) 9#(x1) = x1 >= x1 = 3#(x1) 3#(5(x1)) = 1x1 + 8 >= x1 + 4 = 9#(7(x1)) 3(1(x1)) = x1 + 8 >= x1 + 8 = 4(1(x1)) 5(9(x1)) = 1x1 + 9 >= 1x1 + 8 = 2(6(5(x1))) 3(5(x1)) = 1x1 + 8 >= x1 + 8 = 8(9(7(x1))) 9(x1) = x1 + 8 >= x1 = 3(2(3(x1))) 8(4(x1)) = x1 + 8 >= x1 + 0 = 6(x1) 2(6(x1)) = x1 + 0 >= x1 + 0 = 4(3(x1)) 3(8(x1)) = x1 + 8 >= x1 + 4 = 3(2(7(x1))) 9(x1) = x1 + 8 >= 8 = 5(0(2(x1))) 8(8(4(x1))) = x1 + 8 >= x1 + 8 = 1(9(x1)) 7(1(x1)) = x1 + 8 >= x1 + 8 = 6(9(x1)) 3(9(x1)) = x1 + 8 >= x1 + 8 = 9(3(x1)) 7(5(x1)) = 1x1 + 8 >= 8 = 1(0(x1)) problem: DPs: 9#(x1) -> 2#(3(x1)) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 2#(x1) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 3#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) EDG Processor: DPs: 9#(x1) -> 2#(3(x1)) 2#(6(x1)) -> 3#(x1) 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 2#(x1) 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) 9#(x1) -> 3#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1))) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1)) 7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1))) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1)) 3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) Matrix Interpretation Processor: dim=4 interpretation: [9#](x0) = [0 0 1 1]x0, [7#](x0) = [0 0 1 0]x0 + [1], [2#](x0) = [0 0 1 0]x0, [3#](x0) = [0 0 0 1]x0, [0] [0] [0](x0) = [0] [0], [0 0 0 0] [1] [0 0 0 0] [1] [8](x0) = [1 0 1 0]x0 + [0] [0 0 1 0] [1], [0 1 0 0] [0] [0 0 1 0] [0] [7](x0) = [0 0 1 0]x0 + [1] [0 0 0 1] [0], [0 0 1 0] [0] [0 0 0 0] [1] [2](x0) = [0 0 1 1]x0 + [0] [0 0 1 0] [0], [0 0 0 0] [0 0 0 0] [6](x0) = [0 0 0 1]x0 [0 0 0 0] , [0 1 0 0] [0] [0 0 0 0] [1] [5](x0) = [0 1 0 0]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [1] [9](x0) = [0 0 0 0]x0 + [0] [0 0 0 1] [1], [0 0 0 1] [0 0 0 0] [4](x0) = [1 0 0 0]x0 [0 0 0 0] , [0 0 0 1] [0 1 0 0] [3](x0) = [0 0 0 0]x0 [0 0 0 1] , [0 0 0 0] [0] [0 0 0 0] [0] [1](x0) = [0 0 1 1]x0 + [0] [1 0 0 0] [1] orientation: 9#(x1) = [0 0 1 1]x1 >= [0] = 2#(3(x1)) 2#(6(x1)) = [0 0 0 1]x1 >= [0 0 0 1]x1 = 3#(x1) 3#(9(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 9#(3(x1)) 9#(x1) = [0 0 1 1]x1 >= [0 0 1 0]x1 = 2#(x1) 9#(x1) = [0 0 1 1]x1 >= [0] = 3#(2(3(x1))) 3#(9(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 3#(x1) 3#(8(x1)) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = 3#(2(7(x1))) 3#(8(x1)) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = 2#(7(x1)) 3#(8(x1)) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = 7#(x1) 7#(1(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 = 9#(x1) 9#(x1) = [0 0 1 1]x1 >= [0 0 0 1]x1 = 3#(x1) [1 0 0 0] [1] [1 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] 3(1(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 4(1(x1)) [1 0 0 0] [1] [0 0 0 0] [0] [1] [1] [1] [1] 5(9(x1)) = [1] >= [1] = 2(6(5(x1))) [1] [1] [1] [1] [1] [1] 3(5(x1)) = [0] >= [0] = 8(9(7(x1))) [1] [1] [0 0 0 0] [0] [0] [0 0 0 0] [1] [1] 9(x1) = [0 0 0 0]x1 + [0] >= [0] = 3(2(3(x1))) [0 0 0 1] [1] [0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] 8(4(x1)) = [1 0 0 1]x1 + [0] >= [0 0 0 1]x1 = 6(x1) [1 0 0 0] [1] [0 0 0 0] [0 0 0 1] [0] [0 0 0 1] [0 0 0 0] [1] [0 0 0 0] 2(6(x1)) = [0 0 0 1]x1 + [0] >= [0 0 0 1]x1 = 4(3(x1)) [0 0 0 1] [0] [0 0 0 0] [0 0 1 0] [1] [0 0 1 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] 3(8(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 3(2(7(x1))) [0 0 1 0] [1] [0 0 1 0] [1] [0 0 0 0] [0] [0] [0 0 0 0] [1] [1] 9(x1) = [0 0 0 0]x1 + [0] >= [0] = 5(0(2(x1))) [0 0 0 1] [1] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [0] 8(8(4(x1))) = [1 0 0 1]x1 + [1] >= [0 0 0 1]x1 + [1] = 1(9(x1)) [1 0 0 1] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 1 1] [0] [0 0 0 0] [0] 7(1(x1)) = [0 0 1 1]x1 + [1] >= [0 0 0 1]x1 + [1] = 6(9(x1)) [1 0 0 0] [1] [0 0 0 0] [0] [0 0 0 1] [1] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] 3(9(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 9(3(x1)) [0 0 0 1] [1] [0 0 0 1] [1] [0 0 0 0] [1] [0] [0 1 0 0] [0] [0] 7(5(x1)) = [0 1 0 0]x1 + [1] >= [0] = 1(0(x1)) [0 0 0 0] [1] [1] problem: DPs: 9#(x1) -> 2#(3(x1)) 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) 9#(x1) -> 3#(2(3(x1))) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) EDG Processor: DPs: 9#(x1) -> 2#(3(x1)) 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) 9#(x1) -> 3#(2(3(x1))) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1)) 2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 15/64 DPs: 2#(6(x1)) -> 3#(x1) 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Matrix Interpretation Processor: dim=3 interpretation: [2#](x0) = [0 0 1]x0, [3#](x0) = [0 0 1]x0, [0] [0](x0) = [0] [0], [1 0 0] [0] [8](x0) = [1 0 0]x0 + [1] [1 0 0] [0], [0 0 0] [1] [7](x0) = [0 0 0]x0 + [0] [1 0 0] [0], [0 0 1] [0] [2](x0) = [0 0 0]x0 + [1] [0 0 0] [0], [0 0 0] [0] [6](x0) = [0 0 0]x0 + [0] [0 0 1] [1], [0 1 1] [0] [5](x0) = [0 0 0]x0 + [1] [1 0 0] [0], [0 0 0] [0] [9](x0) = [1 0 1]x0 + [1] [0 0 0] [0], [0 0 1] [1] [4](x0) = [0 0 0]x0 + [1] [0 0 0] [0], [1 0 1] [3](x0) = [1 1 0]x0 [0 0 0] , [1] [1](x0) = [0] [0] orientation: 2#(6(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 = 3#(x1) 3#(8(x1)) = [1 0 0]x1 >= [0] = 3#(2(7(x1))) 3#(8(x1)) = [1 0 0]x1 >= [1 0 0]x1 = 2#(7(x1)) [1] [1] 3(1(x1)) = [1] >= [1] = 4(1(x1)) [0] [0] [1 0 1] [1] [1 0 0] [1] 5(9(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(6(5(x1))) [0 0 0] [0] [0 0 0] [0] [1 1 1] [0] [0] 3(5(x1)) = [0 1 1]x1 + [1] >= [1] = 8(9(7(x1))) [0 0 0] [0] [0] [0 0 0] [0] [0] 9(x1) = [1 0 1]x1 + [1] >= [1] = 3(2(3(x1))) [0 0 0] [0] [0] [0 0 1] [1] [0 0 0] [0] 8(4(x1)) = [0 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 6(x1) [0 0 1] [1] [0 0 1] [1] [0 0 1] [1] [1] 2(6(x1)) = [0 0 0]x1 + [1] >= [1] = 4(3(x1)) [0 0 0] [0] [0] [2 0 0] [0] [1 0 0] [0] 3(8(x1)) = [2 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 3(2(7(x1))) [0 0 0] [0] [0 0 0] [0] [0 0 0] [0] [0] 9(x1) = [1 0 1]x1 + [1] >= [1] = 5(0(2(x1))) [0 0 0] [0] [0] [0 0 1] [1] [1] 8(8(4(x1))) = [0 0 1]x1 + [2] >= [0] = 1(9(x1)) [0 0 1] [1] [0] [1] [0] 7(1(x1)) = [0] >= [0] = 6(9(x1)) [1] [1] [0 0 0] [0] [0 0 0] [0] 3(9(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = 9(3(x1)) [0 0 0] [0] [0 0 0] [0] [0 0 0] [1] [1] 7(5(x1)) = [0 0 0]x1 + [0] >= [0] = 1(0(x1)) [0 1 1] [0] [0] problem: DPs: 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) EDG Processor: DPs: 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 2#(7(x1)) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) graph: 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1))) 3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: 3#(8(x1)) -> 3#(2(7(x1))) TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [3#](x0) = 2x0 + 0, [0](x0) = 12, [8](x0) = 13, [7](x0) = x0 + 15, [2](x0) = 10, [6](x0) = 0, [5](x0) = x0 + 13, [9](x0) = 4x0 + 15, [4](x0) = 0, [3](x0) = x0 + 0, [1](x0) = 13 orientation: 3#(8(x1)) = 15 >= 12 = 3#(2(7(x1))) 3(1(x1)) = 13 >= 0 = 4(1(x1)) 5(9(x1)) = 4x1 + 15 >= 10 = 2(6(5(x1))) 3(5(x1)) = x1 + 13 >= 13 = 8(9(7(x1))) 9(x1) = 4x1 + 15 >= 10 = 3(2(3(x1))) 8(4(x1)) = 13 >= 0 = 6(x1) 2(6(x1)) = 10 >= 0 = 4(3(x1)) 3(8(x1)) = 13 >= 10 = 3(2(7(x1))) 9(x1) = 4x1 + 15 >= 13 = 5(0(2(x1))) 8(8(4(x1))) = 13 >= 13 = 1(9(x1)) 7(1(x1)) = 15 >= 0 = 6(9(x1)) 3(9(x1)) = 4x1 + 15 >= 4x1 + 15 = 9(3(x1)) 7(5(x1)) = x1 + 15 >= 13 = 1(0(x1)) problem: DPs: TRS: 3(1(x1)) -> 4(1(x1)) 5(9(x1)) -> 2(6(5(x1))) 3(5(x1)) -> 8(9(7(x1))) 9(x1) -> 3(2(3(x1))) 8(4(x1)) -> 6(x1) 2(6(x1)) -> 4(3(x1)) 3(8(x1)) -> 3(2(7(x1))) 9(x1) -> 5(0(2(x1))) 8(8(4(x1))) -> 1(9(x1)) 7(1(x1)) -> 6(9(x1)) 3(9(x1)) -> 9(3(x1)) 7(5(x1)) -> 1(0(x1)) Qed