YES Problem: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) Proof: DP Processor: DPs: 2#(8(x1)) -> 4#(x1) 5#(9(x1)) -> 0#(x1) 4#(x1) -> 2#(3(x1)) 4#(x1) -> 5#(2(3(x1))) 5#(3(x1)) -> 0#(x1) 5#(3(x1)) -> 6#(0(x1)) 2#(8(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(7(x1)) -> 5#(x1) 9#(7(x1)) -> 7#(5(x1)) 7#(2(x1)) -> 4#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 7#(x1) 9#(5(9(x1))) -> 5#(7(x1)) 4#(x1) -> 6#(x1) 4#(x1) -> 6#(6(x1)) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 9#(x1) -> 6#(7(x1)) 6#(2(x1)) -> 7#(x1) 6#(2(x1)) -> 7#(7(x1)) 2#(4(x1)) -> 7#(x1) 2#(4(x1)) -> 0#(7(x1)) 0#(3(x1)) -> 5#(3(x1)) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) TDG Processor: DPs: 2#(8(x1)) -> 4#(x1) 5#(9(x1)) -> 0#(x1) 4#(x1) -> 2#(3(x1)) 4#(x1) -> 5#(2(3(x1))) 5#(3(x1)) -> 0#(x1) 5#(3(x1)) -> 6#(0(x1)) 2#(8(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(7(x1)) -> 5#(x1) 9#(7(x1)) -> 7#(5(x1)) 7#(2(x1)) -> 4#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 7#(x1) 9#(5(9(x1))) -> 5#(7(x1)) 4#(x1) -> 6#(x1) 4#(x1) -> 6#(6(x1)) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 9#(x1) -> 6#(7(x1)) 6#(2(x1)) -> 7#(x1) 6#(2(x1)) -> 7#(7(x1)) 2#(4(x1)) -> 7#(x1) 2#(4(x1)) -> 0#(7(x1)) 0#(3(x1)) -> 5#(3(x1)) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(5(9(x1))) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(2(6(x1))) -> 2#(4(x1)) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(2(6(x1))) -> 4#(x1) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(3(x1)) -> 6#(0(x1)) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(3(x1)) -> 0#(x1) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(9(x1)) -> 0#(x1) 9#(7(x1)) -> 7#(5(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 9#(7(x1)) -> 7#(5(x1)) -> 7#(2(x1)) -> 4#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 2#(4(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 4#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(3(x1)) -> 6#(0(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(3(x1)) -> 0#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(9(x1)) -> 0#(x1) 9#(x1) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(x1) -> 6#(7(x1)) -> 6#(2(x1)) -> 7#(7(x1)) 9#(x1) -> 6#(7(x1)) -> 6#(2(x1)) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) -> 9#(x1) -> 6#(7(x1)) 7#(0(x1)) -> 9#(3(x1)) -> 9#(x1) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) -> 9#(5(9(x1))) -> 5#(7(x1)) 7#(0(x1)) -> 9#(3(x1)) -> 9#(5(9(x1))) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) -> 9#(7(x1)) -> 7#(5(x1)) 7#(0(x1)) -> 9#(3(x1)) -> 9#(7(x1)) -> 5#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) 6#(2(x1)) -> 7#(7(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 6#(2(x1)) -> 7#(7(x1)) -> 7#(2(x1)) -> 4#(x1) 6#(2(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 6#(2(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 0#(3(x1)) -> 5#(3(x1)) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 0#(3(x1)) -> 5#(3(x1)) -> 5#(2(6(x1))) -> 2#(4(x1)) 0#(3(x1)) -> 5#(3(x1)) -> 5#(2(6(x1))) -> 4#(x1) 0#(3(x1)) -> 5#(3(x1)) -> 5#(3(x1)) -> 6#(0(x1)) 0#(3(x1)) -> 5#(3(x1)) -> 5#(3(x1)) -> 0#(x1) 0#(3(x1)) -> 5#(3(x1)) -> 5#(9(x1)) -> 0#(x1) 5#(3(x1)) -> 6#(0(x1)) -> 6#(2(x1)) -> 7#(7(x1)) 5#(3(x1)) -> 6#(0(x1)) -> 6#(2(x1)) -> 7#(x1) 5#(3(x1)) -> 0#(x1) -> 0#(3(x1)) -> 5#(3(x1)) 5#(9(x1)) -> 0#(x1) -> 0#(3(x1)) -> 5#(3(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(7(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 0#(7(x1)) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(8(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(8(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 6#(7(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 5#(7(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 7#(5(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 5#(x1) 4#(x1) -> 6#(6(x1)) -> 6#(2(x1)) -> 7#(7(x1)) 4#(x1) -> 6#(6(x1)) -> 6#(2(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(7(x1)) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(x1) 4#(x1) -> 5#(2(3(x1))) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 4#(x1) -> 5#(2(3(x1))) -> 5#(2(6(x1))) -> 2#(4(x1)) 4#(x1) -> 5#(2(3(x1))) -> 5#(2(6(x1))) -> 4#(x1) 4#(x1) -> 5#(2(3(x1))) -> 5#(3(x1)) -> 6#(0(x1)) 4#(x1) -> 5#(2(3(x1))) -> 5#(3(x1)) -> 0#(x1) 4#(x1) -> 5#(2(3(x1))) -> 5#(9(x1)) -> 0#(x1) 4#(x1) -> 2#(3(x1)) -> 2#(4(x1)) -> 0#(7(x1)) 4#(x1) -> 2#(3(x1)) -> 2#(4(x1)) -> 7#(x1) 4#(x1) -> 2#(3(x1)) -> 2#(8(x1)) -> 7#(x1) 4#(x1) -> 2#(3(x1)) -> 2#(8(x1)) -> 4#(x1) 2#(4(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 2#(4(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 2#(4(x1)) -> 0#(7(x1)) -> 0#(3(x1)) -> 5#(3(x1)) 2#(8(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 2#(8(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) EDG Processor: DPs: 2#(8(x1)) -> 4#(x1) 5#(9(x1)) -> 0#(x1) 4#(x1) -> 2#(3(x1)) 4#(x1) -> 5#(2(3(x1))) 5#(3(x1)) -> 0#(x1) 5#(3(x1)) -> 6#(0(x1)) 2#(8(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(7(x1)) -> 5#(x1) 9#(7(x1)) -> 7#(5(x1)) 7#(2(x1)) -> 4#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 7#(x1) 9#(5(9(x1))) -> 5#(7(x1)) 4#(x1) -> 6#(x1) 4#(x1) -> 6#(6(x1)) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 9#(x1) -> 6#(7(x1)) 6#(2(x1)) -> 7#(x1) 6#(2(x1)) -> 7#(7(x1)) 2#(4(x1)) -> 7#(x1) 2#(4(x1)) -> 0#(7(x1)) 0#(3(x1)) -> 5#(3(x1)) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(5(9(x1))) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(5(9(x1))) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(9(x1)) -> 0#(x1) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(3(x1)) -> 0#(x1) 9#(5(9(x1))) -> 5#(7(x1)) -> 5#(3(x1)) -> 6#(0(x1)) 9#(7(x1)) -> 7#(5(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(9(x1)) -> 0#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(3(x1)) -> 0#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(3(x1)) -> 6#(0(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 4#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 2#(4(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(x1) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 7#(0(x1)) -> 9#(3(x1)) -> 9#(x1) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) -> 9#(x1) -> 6#(7(x1)) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 6#(2(x1)) -> 7#(7(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 6#(2(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 6#(2(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 0#(3(x1)) -> 5#(3(x1)) -> 5#(3(x1)) -> 0#(x1) 0#(3(x1)) -> 5#(3(x1)) -> 5#(3(x1)) -> 6#(0(x1)) 5#(3(x1)) -> 0#(x1) -> 0#(3(x1)) -> 5#(3(x1)) 5#(9(x1)) -> 0#(x1) -> 0#(3(x1)) -> 5#(3(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(7(x1)) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(8(x1)) -> 4#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(8(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 0#(7(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 5#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 7#(5(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 5#(7(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 6#(7(x1)) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(7(x1)) 2#(4(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 2#(4(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 2#(4(x1)) -> 0#(7(x1)) -> 0#(3(x1)) -> 5#(3(x1)) 2#(8(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 2#(8(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 2#(3(x1)) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 5#(2(3(x1))) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 6#(6(x1)) 2#(8(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) SCC Processor: #sccs: 2 #rules: 18 #arcs: 57/676 DPs: 9#(5(9(x1))) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(7(x1)) -> 7#(5(x1)) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(7(x1)) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 2#(8(x1)) -> 7#(x1) 2#(8(x1)) -> 4#(x1) 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = x0 + 0, [7#](x0) = 0, [6#](x0) = 0, [5#](x0) = 0, [4#](x0) = 0, [2#](x0) = x0 + 0, [6](x0) = 0, [3](x0) = 0, [0](x0) = 0, [5](x0) = x0 + 0, [9](x0) = 0, [4](x0) = 0, [1](x0) = -15x0 + 0, [8](x0) = 1, [2](x0) = x0 + 0, [7](x0) = 0 orientation: 9#(5(9(x1))) = 0 >= 0 = 7#(x1) 7#(0(x1)) = 0 >= 0 = 9#(3(x1)) 9#(x1) = x1 + 0 >= 0 = 7#(x1) 7#(2(x1)) = 0 >= 0 = 4#(x1) 4#(x1) = 0 >= 0 = 9#(6(6(x1))) 9#(7(x1)) = 0 >= 0 = 7#(5(x1)) 9#(7(x1)) = 0 >= 0 = 5#(x1) 5#(2(6(x1))) = 0 >= 0 = 6#(2(4(x1))) 6#(2(x1)) = 0 >= 0 = 7#(7(x1)) 6#(2(x1)) = 0 >= 0 = 7#(x1) 5#(2(6(x1))) = 0 >= 0 = 2#(4(x1)) 2#(4(x1)) = 0 >= 0 = 7#(x1) 2#(8(x1)) = 1 >= 0 = 7#(x1) 2#(8(x1)) = 1 >= 0 = 4#(x1) 4#(x1) = 0 >= 0 = 6#(x1) 5#(2(6(x1))) = 0 >= 0 = 4#(x1) 2(7(x1)) = 0 >= 0 = 1(8(x1)) 2(8(1(x1))) = 1 >= 1 = 8(x1) 2(8(x1)) = 1 >= 0 = 4(x1) 5(9(x1)) = 0 >= 0 = 0(x1) 4(x1) = 0 >= 0 = 5(2(3(x1))) 5(3(x1)) = 0 >= 0 = 6(0(x1)) 2(8(x1)) = 1 >= 0 = 7(x1) 4(7(x1)) = 0 >= 0 = 1(3(x1)) 5(2(6(x1))) = 0 >= 0 = 6(2(4(x1))) 9(7(x1)) = 0 >= 0 = 7(5(x1)) 7(2(x1)) = 0 >= 0 = 4(x1) 7(0(x1)) = 0 >= 0 = 9(3(x1)) 6(9(x1)) = 0 >= 0 = 9(x1) 9(5(9(x1))) = 0 >= 0 = 5(7(x1)) 4(x1) = 0 >= 0 = 9(6(6(x1))) 9(x1) = 0 >= 0 = 6(7(x1)) 6(2(x1)) = 0 >= 0 = 7(7(x1)) 2(4(x1)) = 0 >= 0 = 0(7(x1)) 6(6(x1)) = 0 >= 0 = 3(x1) 0(3(x1)) = 0 >= 0 = 5(3(x1)) problem: DPs: 9#(5(9(x1))) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(7(x1)) -> 7#(5(x1)) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(7(x1)) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 9#(5(9(x1))) -> 7#(x1) 7#(0(x1)) -> 9#(3(x1)) 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(7(x1)) -> 7#(5(x1)) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(7(x1)) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(5(9(x1))) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 9#(5(9(x1))) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(7(x1)) -> 7#(5(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 2#(4(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 4#(x1) 9#(x1) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 7#(0(x1)) -> 9#(3(x1)) -> 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 6#(2(x1)) -> 7#(7(x1)) -> 7#(0(x1)) -> 9#(3(x1)) 6#(2(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 6#(2(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(7(x1)) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 7#(5(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 5#(x1) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(7(x1)) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(x1) 2#(4(x1)) -> 7#(x1) -> 7#(0(x1)) -> 9#(3(x1)) 2#(4(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = x0 + 0, [7#](x0) = x0, [6#](x0) = x0 + 0, [5#](x0) = x0 + 8, [4#](x0) = x0 + 0, [2#](x0) = x0 + 0, [6](x0) = x0 + 0, [3](x0) = 0, [0](x0) = 4, [5](x0) = x0 + 4, [9](x0) = x0 + 8, [4](x0) = x0 + 8, [1](x0) = x0, [8](x0) = x0 + -14, [2](x0) = x0 + 8, [7](x0) = x0 + 8 orientation: 9#(5(9(x1))) = x1 + 8 >= x1 = 7#(x1) 7#(0(x1)) = 4 >= 0 = 9#(3(x1)) 9#(x1) = x1 + 0 >= x1 = 7#(x1) 7#(2(x1)) = x1 + 8 >= x1 + 0 = 4#(x1) 4#(x1) = x1 + 0 >= x1 + 0 = 9#(6(6(x1))) 9#(7(x1)) = x1 + 8 >= x1 + 4 = 7#(5(x1)) 9#(7(x1)) = x1 + 8 >= x1 + 8 = 5#(x1) 5#(2(6(x1))) = x1 + 8 >= x1 + 8 = 6#(2(4(x1))) 6#(2(x1)) = x1 + 8 >= x1 + 8 = 7#(7(x1)) 6#(2(x1)) = x1 + 8 >= x1 = 7#(x1) 5#(2(6(x1))) = x1 + 8 >= x1 + 8 = 2#(4(x1)) 2#(4(x1)) = x1 + 8 >= x1 = 7#(x1) 4#(x1) = x1 + 0 >= x1 + 0 = 6#(x1) 5#(2(6(x1))) = x1 + 8 >= x1 + 0 = 4#(x1) 2(7(x1)) = x1 + 8 >= x1 + -14 = 1(8(x1)) 2(8(1(x1))) = x1 + 8 >= x1 + -14 = 8(x1) 2(8(x1)) = x1 + 8 >= x1 + 8 = 4(x1) 5(9(x1)) = x1 + 8 >= 4 = 0(x1) 4(x1) = x1 + 8 >= 8 = 5(2(3(x1))) 5(3(x1)) = 4 >= 4 = 6(0(x1)) 2(8(x1)) = x1 + 8 >= x1 + 8 = 7(x1) 4(7(x1)) = x1 + 8 >= 0 = 1(3(x1)) 5(2(6(x1))) = x1 + 8 >= x1 + 8 = 6(2(4(x1))) 9(7(x1)) = x1 + 8 >= x1 + 8 = 7(5(x1)) 7(2(x1)) = x1 + 8 >= x1 + 8 = 4(x1) 7(0(x1)) = 8 >= 8 = 9(3(x1)) 6(9(x1)) = x1 + 8 >= x1 + 8 = 9(x1) 9(5(9(x1))) = x1 + 8 >= x1 + 8 = 5(7(x1)) 4(x1) = x1 + 8 >= x1 + 8 = 9(6(6(x1))) 9(x1) = x1 + 8 >= x1 + 8 = 6(7(x1)) 6(2(x1)) = x1 + 8 >= x1 + 8 = 7(7(x1)) 2(4(x1)) = x1 + 8 >= 4 = 0(7(x1)) 6(6(x1)) = x1 + 0 >= 0 = 3(x1) 0(3(x1)) = 4 >= 4 = 5(3(x1)) problem: DPs: 9#(5(9(x1))) -> 7#(x1) 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(7(x1)) -> 7#(5(x1)) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(7(x1)) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 9#(5(9(x1))) -> 7#(x1) 9#(x1) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(7(x1)) -> 7#(5(x1)) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(7(x1)) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(5(9(x1))) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 4#(x1) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 2#(4(x1)) 9#(7(x1)) -> 5#(x1) -> 5#(2(6(x1))) -> 6#(2(4(x1))) 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 6#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 6#(2(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(7(x1)) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 6#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 5#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(7(x1)) -> 7#(5(x1)) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(x1) 4#(x1) -> 6#(x1) -> 6#(2(x1)) -> 7#(7(x1)) 2#(4(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) SCC Processor: #sccs: 1 #rules: 11 #arcs: 20/169 DPs: 9#(5(9(x1))) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 9#(7(x1)) -> 5#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) 4#(x1) -> 6#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = 6x0 + 0, [7#](x0) = 6x0, [6#](x0) = 4x0 + 7, [5#](x0) = 4x0, [4#](x0) = 6x0 + 8, [2#](x0) = 6x0 + 0, [6](x0) = x0 + 2, [3](x0) = 0, [0](x0) = 2, [5](x0) = x0 + 2, [9](x0) = x0 + 2, [4](x0) = x0 + 2, [1](x0) = 2x0 + 2, [8](x0) = x0 + 2, [2](x0) = 2x0 + 2, [7](x0) = x0 + 2 orientation: 9#(5(9(x1))) = 6x1 + 8 >= 6x1 = 7#(x1) 7#(2(x1)) = 8x1 + 8 >= 6x1 + 8 = 4#(x1) 4#(x1) = 6x1 + 8 >= 6x1 + 8 = 9#(6(6(x1))) 9#(x1) = 6x1 + 0 >= 6x1 = 7#(x1) 9#(7(x1)) = 6x1 + 8 >= 4x1 = 5#(x1) 5#(2(6(x1))) = 6x1 + 8 >= 6x1 + 8 = 6#(2(4(x1))) 6#(2(x1)) = 6x1 + 7 >= 6x1 = 7#(x1) 5#(2(6(x1))) = 6x1 + 8 >= 6x1 + 8 = 2#(4(x1)) 2#(4(x1)) = 6x1 + 8 >= 6x1 = 7#(x1) 5#(2(6(x1))) = 6x1 + 8 >= 6x1 + 8 = 4#(x1) 4#(x1) = 6x1 + 8 >= 4x1 + 7 = 6#(x1) 2(7(x1)) = 2x1 + 4 >= 2x1 + 4 = 1(8(x1)) 2(8(1(x1))) = 4x1 + 4 >= x1 + 2 = 8(x1) 2(8(x1)) = 2x1 + 4 >= x1 + 2 = 4(x1) 5(9(x1)) = x1 + 2 >= 2 = 0(x1) 4(x1) = x1 + 2 >= 2 = 5(2(3(x1))) 5(3(x1)) = 2 >= 2 = 6(0(x1)) 2(8(x1)) = 2x1 + 4 >= x1 + 2 = 7(x1) 4(7(x1)) = x1 + 2 >= 2 = 1(3(x1)) 5(2(6(x1))) = 2x1 + 4 >= 2x1 + 4 = 6(2(4(x1))) 9(7(x1)) = x1 + 2 >= x1 + 2 = 7(5(x1)) 7(2(x1)) = 2x1 + 2 >= x1 + 2 = 4(x1) 7(0(x1)) = 2 >= 2 = 9(3(x1)) 6(9(x1)) = x1 + 2 >= x1 + 2 = 9(x1) 9(5(9(x1))) = x1 + 2 >= x1 + 2 = 5(7(x1)) 4(x1) = x1 + 2 >= x1 + 2 = 9(6(6(x1))) 9(x1) = x1 + 2 >= x1 + 2 = 6(7(x1)) 6(2(x1)) = 2x1 + 2 >= x1 + 2 = 7(7(x1)) 2(4(x1)) = 2x1 + 4 >= 2 = 0(7(x1)) 6(6(x1)) = x1 + 2 >= 0 = 3(x1) 0(3(x1)) = 2 >= 2 = 5(3(x1)) problem: DPs: 9#(5(9(x1))) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 9#(5(9(x1))) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 2#(4(x1)) 2#(4(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(5(9(x1))) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 6#(2(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 5#(2(6(x1))) -> 6#(2(4(x1))) -> 6#(2(x1)) -> 7#(x1) 5#(2(6(x1))) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 5#(2(6(x1))) -> 2#(4(x1)) -> 2#(4(x1)) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) 4#(x1) -> 9#(6(6(x1))) -> 9#(5(9(x1))) -> 7#(x1) 2#(4(x1)) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) SCC Processor: #sccs: 1 #rules: 4 #arcs: 10/81 DPs: 9#(5(9(x1))) -> 7#(x1) 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = 1x0 + 9, [7#](x0) = x0 + 9, [4#](x0) = 8x0 + 9, [6](x0) = x0 + 8, [3](x0) = 0, [0](x0) = 8, [5](x0) = 4x0 + 8, [9](x0) = 4x0 + 12, [4](x0) = 4x0 + 12, [1](x0) = 1x0 + 6, [8](x0) = x0 + 7, [2](x0) = 8x0 + 8, [7](x0) = 4x0 + 1 orientation: 9#(5(9(x1))) = 9x1 + 17 >= x1 + 9 = 7#(x1) 7#(2(x1)) = 8x1 + 9 >= 8x1 + 9 = 4#(x1) 4#(x1) = 8x1 + 9 >= 1x1 + 9 = 9#(6(6(x1))) 9#(x1) = 1x1 + 9 >= x1 + 9 = 7#(x1) 2(7(x1)) = 12x1 + 9 >= 1x1 + 8 = 1(8(x1)) 2(8(1(x1))) = 9x1 + 15 >= x1 + 7 = 8(x1) 2(8(x1)) = 8x1 + 15 >= 4x1 + 12 = 4(x1) 5(9(x1)) = 8x1 + 16 >= 8 = 0(x1) 4(x1) = 4x1 + 12 >= 12 = 5(2(3(x1))) 5(3(x1)) = 8 >= 8 = 6(0(x1)) 2(8(x1)) = 8x1 + 15 >= 4x1 + 1 = 7(x1) 4(7(x1)) = 8x1 + 12 >= 6 = 1(3(x1)) 5(2(6(x1))) = 12x1 + 20 >= 12x1 + 20 = 6(2(4(x1))) 9(7(x1)) = 8x1 + 12 >= 8x1 + 12 = 7(5(x1)) 7(2(x1)) = 12x1 + 12 >= 4x1 + 12 = 4(x1) 7(0(x1)) = 12 >= 12 = 9(3(x1)) 6(9(x1)) = 4x1 + 12 >= 4x1 + 12 = 9(x1) 9(5(9(x1))) = 12x1 + 20 >= 8x1 + 8 = 5(7(x1)) 4(x1) = 4x1 + 12 >= 4x1 + 12 = 9(6(6(x1))) 9(x1) = 4x1 + 12 >= 4x1 + 8 = 6(7(x1)) 6(2(x1)) = 8x1 + 8 >= 8x1 + 5 = 7(7(x1)) 2(4(x1)) = 12x1 + 20 >= 8 = 0(7(x1)) 6(6(x1)) = x1 + 8 >= 0 = 3(x1) 0(3(x1)) = 8 >= 8 = 5(3(x1)) problem: DPs: 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) 9#(x1) -> 7#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 9#(x1) -> 7#(x1) -> 7#(2(x1)) -> 4#(x1) 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) 4#(x1) -> 9#(6(6(x1))) -> 9#(x1) -> 7#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [9#](x0) = 8x0 + 0, [7#](x0) = x0, [4#](x0) = 8, [6](x0) = 0, [3](x0) = 0, [0](x0) = 0, [5](x0) = 0, [9](x0) = 0, [4](x0) = 0, [1](x0) = 0, [8](x0) = 15, [2](x0) = 9x0 + 8, [7](x0) = 0 orientation: 7#(2(x1)) = 9x1 + 8 >= 8 = 4#(x1) 4#(x1) = 8 >= 8 = 9#(6(6(x1))) 9#(x1) = 8x1 + 0 >= x1 = 7#(x1) 2(7(x1)) = 9 >= 0 = 1(8(x1)) 2(8(1(x1))) = 24 >= 15 = 8(x1) 2(8(x1)) = 24 >= 0 = 4(x1) 5(9(x1)) = 0 >= 0 = 0(x1) 4(x1) = 0 >= 0 = 5(2(3(x1))) 5(3(x1)) = 0 >= 0 = 6(0(x1)) 2(8(x1)) = 24 >= 0 = 7(x1) 4(7(x1)) = 0 >= 0 = 1(3(x1)) 5(2(6(x1))) = 0 >= 0 = 6(2(4(x1))) 9(7(x1)) = 0 >= 0 = 7(5(x1)) 7(2(x1)) = 0 >= 0 = 4(x1) 7(0(x1)) = 0 >= 0 = 9(3(x1)) 6(9(x1)) = 0 >= 0 = 9(x1) 9(5(9(x1))) = 0 >= 0 = 5(7(x1)) 4(x1) = 0 >= 0 = 9(6(6(x1))) 9(x1) = 0 >= 0 = 6(7(x1)) 6(2(x1)) = 0 >= 0 = 7(7(x1)) 2(4(x1)) = 9 >= 0 = 0(7(x1)) 6(6(x1)) = 0 >= 0 = 3(x1) 0(3(x1)) = 0 >= 0 = 5(3(x1)) problem: DPs: 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 7#(2(x1)) -> 4#(x1) 4#(x1) -> 9#(6(6(x1))) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: 7#(2(x1)) -> 4#(x1) -> 4#(x1) -> 9#(6(6(x1))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/4 DPs: 5#(3(x1)) -> 0#(x1) 0#(3(x1)) -> 5#(3(x1)) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0#](x0) = [1 0]x0, [5#](x0) = [0 1]x0 + [0], [0 0] [0] [6](x0) = [1 0]x0 + [1], [1 0 ] [0 ] [3](x0) = [-& -&]x0 + [-&], [2 2] [-&] [0](x0) = [3 1]x0 + [2 ], [2 -&] [2] [5](x0) = [3 -&]x0 + [3], [2 0] [1] [9](x0) = [2 1]x0 + [2], [3 2] [3] [4](x0) = [3 2]x0 + [3], [0 0] [1] [1](x0) = [0 0]x0 + [0], [0 0] [0] [8](x0) = [3 3]x0 + [3], [-& 3 ] [0] [2](x0) = [3 0 ]x0 + [3], [1 0] [1] [7](x0) = [1 0]x0 + [0] orientation: 5#(3(x1)) = [1 0]x1 + [0] >= [1 0]x1 = 0#(x1) 0#(3(x1)) = [2 1]x1 + [1] >= [1 0]x1 + [0] = 5#(3(x1)) [4 3] [3] [3 3] [3] 2(7(x1)) = [4 3]x1 + [4] >= [3 3]x1 + [3] = 1(8(x1)) [6 6] [7] [0 0] [0] 2(8(1(x1))) = [3 3]x1 + [4] >= [3 3]x1 + [3] = 8(x1) [6 6] [6] [3 2] [3] 2(8(x1)) = [3 3]x1 + [3] >= [3 2]x1 + [3] = 4(x1) [4 2] [3] [2 2] [-&] 5(9(x1)) = [5 3]x1 + [4] >= [3 1]x1 + [2 ] = 0(x1) [3 2] [3] [2] 4(x1) = [3 2]x1 + [3] >= [3] = 5(2(3(x1))) [3 2] [2] [3 2] [2] 5(3(x1)) = [4 3]x1 + [3] >= [3 3]x1 + [2] = 6(0(x1)) [6 6] [6] [1 0] [1] 2(8(x1)) = [3 3]x1 + [3] >= [1 0]x1 + [0] = 7(x1) [4 3] [4] [1 0] [1] 4(7(x1)) = [4 3]x1 + [4] >= [1 0]x1 + [0] = 1(3(x1)) [6 5] [6] [6 5] [6] 5(2(6(x1))) = [7 6]x1 + [7] >= [7 6]x1 + [7] = 6(2(4(x1))) [3 2] [3] [3 -&] [3] 9(7(x1)) = [3 2]x1 + [3] >= [3 -&]x1 + [3] = 7(5(x1)) [3 4] [3] [3 2] [3] 7(2(x1)) = [3 4]x1 + [3] >= [3 2]x1 + [3] = 4(x1) [3 3] [2] [3 2] [2] 7(0(x1)) = [3 3]x1 + [2] >= [3 2]x1 + [2] = 9(3(x1)) [2 1] [2] [2 0] [1] 6(9(x1)) = [3 1]x1 + [2] >= [2 1]x1 + [2] = 9(x1) [6 4] [5] [3 2] [3] 9(5(9(x1))) = [6 4]x1 + [5] >= [4 3]x1 + [4] = 5(7(x1)) [3 2] [3] [3 2] [3] 4(x1) = [3 2]x1 + [3] >= [3 2]x1 + [3] = 9(6(6(x1))) [2 0] [1] [1 0] [1] 9(x1) = [2 1]x1 + [2] >= [2 1]x1 + [2] = 6(7(x1)) [3 3] [3] [2 1] [2] 6(2(x1)) = [3 4]x1 + [3] >= [2 1]x1 + [2] = 7(7(x1)) [6 5] [6] [3 2] [3] 2(4(x1)) = [6 5]x1 + [6] >= [4 3]x1 + [4] = 0(7(x1)) [1 0] [1] [1 0 ] [0 ] 6(6(x1)) = [1 1]x1 + [1] >= [-& -&]x1 + [-&] = 3(x1) [3 2] [2] [3 2] [2] 0(3(x1)) = [4 3]x1 + [3] >= [4 3]x1 + [3] = 5(3(x1)) problem: DPs: 5#(3(x1)) -> 0#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) EDG Processor: DPs: 5#(3(x1)) -> 0#(x1) TRS: 2(7(x1)) -> 1(8(x1)) 2(8(1(x1))) -> 8(x1) 2(8(x1)) -> 4(x1) 5(9(x1)) -> 0(x1) 4(x1) -> 5(2(3(x1))) 5(3(x1)) -> 6(0(x1)) 2(8(x1)) -> 7(x1) 4(7(x1)) -> 1(3(x1)) 5(2(6(x1))) -> 6(2(4(x1))) 9(7(x1)) -> 7(5(x1)) 7(2(x1)) -> 4(x1) 7(0(x1)) -> 9(3(x1)) 6(9(x1)) -> 9(x1) 9(5(9(x1))) -> 5(7(x1)) 4(x1) -> 9(6(6(x1))) 9(x1) -> 6(7(x1)) 6(2(x1)) -> 7(7(x1)) 2(4(x1)) -> 0(7(x1)) 6(6(x1)) -> 3(x1) 0(3(x1)) -> 5(3(x1)) graph: Qed