YES Problem: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) Proof: DP Processor: DPs: 0#(0(1(x1))) -> 0#(2(3(0(1(x1))))) 0#(0(1(x1))) -> 5#(4(1(x1))) 0#(0(1(x1))) -> 0#(5(4(1(x1)))) 0#(0(1(x1))) -> 0#(4(0(5(4(1(x1)))))) 0#(0(1(x1))) -> 0#(3(4(x1))) 0#(0(1(x1))) -> 0#(0(3(4(x1)))) 0#(0(1(x1))) -> 1#(0(0(3(4(x1))))) 0#(0(1(x1))) -> 5#(4(0(1(x1)))) 0#(0(1(x1))) -> 0#(5(4(0(1(x1))))) 0#(1(0(x1))) -> 1#(2(x1)) 0#(1(0(x1))) -> 0#(2(1(2(x1)))) 0#(1(0(x1))) -> 0#(0(2(1(2(x1))))) 0#(1(0(x1))) -> 5#(4(x1)) 0#(1(0(x1))) -> 0#(5(4(x1))) 0#(1(0(x1))) -> 0#(0(5(4(x1)))) 0#(1(0(x1))) -> 1#(0(0(5(4(x1))))) 0#(1(0(x1))) -> 1#(x1) 0#(1(0(x1))) -> 5#(4(1(x1))) 0#(1(0(x1))) -> 0#(2(5(4(1(x1))))) 0#(1(0(x1))) -> 0#(0(2(5(4(1(x1)))))) 0#(1(1(x1))) -> 0#(3(4(1(x1)))) 0#(1(1(x1))) -> 1#(0(3(4(1(x1))))) 0#(1(1(x1))) -> 0#(3(4(1(1(x1))))) 0#(1(1(x1))) -> 5#(0(3(4(1(1(x1)))))) 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(0(1(x1))) -> 1#(2(x1)) 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(1(0(x1))) -> 1#(x1) 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(1(0(x1))) -> 5#(x1) 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(1(1(x1))) -> 5#(4(x1)) 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 0#(1(3(0(x1)))) -> 1#(3(x1)) 0#(1(3(0(x1)))) -> 0#(2(1(3(x1)))) 0#(1(3(0(x1)))) -> 0#(2(0(2(1(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) 0#(1(5(0(x1)))) -> 1#(5(x1)) 0#(1(5(0(x1)))) -> 5#(4(1(5(x1)))) 0#(1(5(0(x1)))) -> 0#(5(4(1(5(x1))))) 0#(1(5(0(x1)))) -> 0#(0(5(4(1(5(x1)))))) 0#(1(5(0(x1)))) -> 1#(0(x1)) 0#(1(5(0(x1)))) -> 5#(4(2(1(0(x1))))) 0#(1(5(0(x1)))) -> 0#(5(4(2(1(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) 0#(3(0(1(x1)))) -> 1#(3(0(x1))) 0#(3(0(1(x1)))) -> 0#(4(1(3(0(x1))))) 0#(3(0(1(x1)))) -> 0#(0(4(1(3(0(x1)))))) 0#(3(1(0(x1)))) -> 1#(x1) 0#(3(1(0(x1)))) -> 0#(2(3(1(x1)))) 0#(3(1(0(x1)))) -> 0#(0(2(3(1(x1))))) 0#(3(1(1(x1)))) -> 0#(3(4(x1))) 0#(3(1(1(x1)))) -> 1#(0(3(4(x1)))) 0#(3(1(1(x1)))) -> 1#(1(0(3(4(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(1(2(0(x1)))) -> 1#(x1) 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 0#(1(2(5(0(x1))))) -> 0#(2(0(x1))) 0#(1(2(5(0(x1))))) -> 5#(4(0(2(0(x1))))) 0#(1(2(5(0(x1))))) -> 1#(5(4(0(2(0(x1)))))) 0#(1(4(2(0(x1))))) -> 0#(4(2(3(0(x1))))) 0#(1(4(2(0(x1))))) -> 1#(0(4(2(3(0(x1)))))) 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) TDG Processor: DPs: 0#(0(1(x1))) -> 0#(2(3(0(1(x1))))) 0#(0(1(x1))) -> 5#(4(1(x1))) 0#(0(1(x1))) -> 0#(5(4(1(x1)))) 0#(0(1(x1))) -> 0#(4(0(5(4(1(x1)))))) 0#(0(1(x1))) -> 0#(3(4(x1))) 0#(0(1(x1))) -> 0#(0(3(4(x1)))) 0#(0(1(x1))) -> 1#(0(0(3(4(x1))))) 0#(0(1(x1))) -> 5#(4(0(1(x1)))) 0#(0(1(x1))) -> 0#(5(4(0(1(x1))))) 0#(1(0(x1))) -> 1#(2(x1)) 0#(1(0(x1))) -> 0#(2(1(2(x1)))) 0#(1(0(x1))) -> 0#(0(2(1(2(x1))))) 0#(1(0(x1))) -> 5#(4(x1)) 0#(1(0(x1))) -> 0#(5(4(x1))) 0#(1(0(x1))) -> 0#(0(5(4(x1)))) 0#(1(0(x1))) -> 1#(0(0(5(4(x1))))) 0#(1(0(x1))) -> 1#(x1) 0#(1(0(x1))) -> 5#(4(1(x1))) 0#(1(0(x1))) -> 0#(2(5(4(1(x1))))) 0#(1(0(x1))) -> 0#(0(2(5(4(1(x1)))))) 0#(1(1(x1))) -> 0#(3(4(1(x1)))) 0#(1(1(x1))) -> 1#(0(3(4(1(x1))))) 0#(1(1(x1))) -> 0#(3(4(1(1(x1))))) 0#(1(1(x1))) -> 5#(0(3(4(1(1(x1)))))) 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(0(1(x1))) -> 1#(2(x1)) 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(1(0(x1))) -> 1#(x1) 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(1(0(x1))) -> 5#(x1) 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(1(1(x1))) -> 5#(4(x1)) 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 0#(1(3(0(x1)))) -> 1#(3(x1)) 0#(1(3(0(x1)))) -> 0#(2(1(3(x1)))) 0#(1(3(0(x1)))) -> 0#(2(0(2(1(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) 0#(1(5(0(x1)))) -> 1#(5(x1)) 0#(1(5(0(x1)))) -> 5#(4(1(5(x1)))) 0#(1(5(0(x1)))) -> 0#(5(4(1(5(x1))))) 0#(1(5(0(x1)))) -> 0#(0(5(4(1(5(x1)))))) 0#(1(5(0(x1)))) -> 1#(0(x1)) 0#(1(5(0(x1)))) -> 5#(4(2(1(0(x1))))) 0#(1(5(0(x1)))) -> 0#(5(4(2(1(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) 0#(3(0(1(x1)))) -> 1#(3(0(x1))) 0#(3(0(1(x1)))) -> 0#(4(1(3(0(x1))))) 0#(3(0(1(x1)))) -> 0#(0(4(1(3(0(x1)))))) 0#(3(1(0(x1)))) -> 1#(x1) 0#(3(1(0(x1)))) -> 0#(2(3(1(x1)))) 0#(3(1(0(x1)))) -> 0#(0(2(3(1(x1))))) 0#(3(1(1(x1)))) -> 0#(3(4(x1))) 0#(3(1(1(x1)))) -> 1#(0(3(4(x1)))) 0#(3(1(1(x1)))) -> 1#(1(0(3(4(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(1(2(0(x1)))) -> 1#(x1) 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 0#(1(2(5(0(x1))))) -> 0#(2(0(x1))) 0#(1(2(5(0(x1))))) -> 5#(4(0(2(0(x1))))) 0#(1(2(5(0(x1))))) -> 1#(5(4(0(2(0(x1)))))) 0#(1(4(2(0(x1))))) -> 0#(4(2(3(0(x1))))) 0#(1(4(2(0(x1))))) -> 1#(0(4(2(3(0(x1)))))) 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) graph: ... EDG Processor: DPs: 0#(0(1(x1))) -> 0#(2(3(0(1(x1))))) 0#(0(1(x1))) -> 5#(4(1(x1))) 0#(0(1(x1))) -> 0#(5(4(1(x1)))) 0#(0(1(x1))) -> 0#(4(0(5(4(1(x1)))))) 0#(0(1(x1))) -> 0#(3(4(x1))) 0#(0(1(x1))) -> 0#(0(3(4(x1)))) 0#(0(1(x1))) -> 1#(0(0(3(4(x1))))) 0#(0(1(x1))) -> 5#(4(0(1(x1)))) 0#(0(1(x1))) -> 0#(5(4(0(1(x1))))) 0#(1(0(x1))) -> 1#(2(x1)) 0#(1(0(x1))) -> 0#(2(1(2(x1)))) 0#(1(0(x1))) -> 0#(0(2(1(2(x1))))) 0#(1(0(x1))) -> 5#(4(x1)) 0#(1(0(x1))) -> 0#(5(4(x1))) 0#(1(0(x1))) -> 0#(0(5(4(x1)))) 0#(1(0(x1))) -> 1#(0(0(5(4(x1))))) 0#(1(0(x1))) -> 1#(x1) 0#(1(0(x1))) -> 5#(4(1(x1))) 0#(1(0(x1))) -> 0#(2(5(4(1(x1))))) 0#(1(0(x1))) -> 0#(0(2(5(4(1(x1)))))) 0#(1(1(x1))) -> 0#(3(4(1(x1)))) 0#(1(1(x1))) -> 1#(0(3(4(1(x1))))) 0#(1(1(x1))) -> 0#(3(4(1(1(x1))))) 0#(1(1(x1))) -> 5#(0(3(4(1(1(x1)))))) 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(0(1(x1))) -> 1#(2(x1)) 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(1(0(x1))) -> 1#(x1) 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(1(0(x1))) -> 5#(x1) 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(1(1(x1))) -> 5#(4(x1)) 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 0#(1(3(0(x1)))) -> 1#(3(x1)) 0#(1(3(0(x1)))) -> 0#(2(1(3(x1)))) 0#(1(3(0(x1)))) -> 0#(2(0(2(1(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) 0#(1(5(0(x1)))) -> 1#(5(x1)) 0#(1(5(0(x1)))) -> 5#(4(1(5(x1)))) 0#(1(5(0(x1)))) -> 0#(5(4(1(5(x1))))) 0#(1(5(0(x1)))) -> 0#(0(5(4(1(5(x1)))))) 0#(1(5(0(x1)))) -> 1#(0(x1)) 0#(1(5(0(x1)))) -> 5#(4(2(1(0(x1))))) 0#(1(5(0(x1)))) -> 0#(5(4(2(1(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) 0#(3(0(1(x1)))) -> 1#(3(0(x1))) 0#(3(0(1(x1)))) -> 0#(4(1(3(0(x1))))) 0#(3(0(1(x1)))) -> 0#(0(4(1(3(0(x1)))))) 0#(3(1(0(x1)))) -> 1#(x1) 0#(3(1(0(x1)))) -> 0#(2(3(1(x1)))) 0#(3(1(0(x1)))) -> 0#(0(2(3(1(x1))))) 0#(3(1(1(x1)))) -> 0#(3(4(x1))) 0#(3(1(1(x1)))) -> 1#(0(3(4(x1)))) 0#(3(1(1(x1)))) -> 1#(1(0(3(4(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(1(2(0(x1)))) -> 1#(x1) 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 0#(1(2(5(0(x1))))) -> 0#(2(0(x1))) 0#(1(2(5(0(x1))))) -> 5#(4(0(2(0(x1))))) 0#(1(2(5(0(x1))))) -> 1#(5(4(0(2(0(x1)))))) 0#(1(4(2(0(x1))))) -> 0#(4(2(3(0(x1))))) 0#(1(4(2(0(x1))))) -> 1#(0(4(2(3(0(x1)))))) 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) graph: 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(5(1(0(0(x1))))) -> 1#(0(x1)) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 5#(5(1(0(0(x1))))) -> 1#(0(x1)) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 1#(2(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 1#(x1) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 5#(x1) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 5#(4(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 1#(x1) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(0(x1)) -> 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(2(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(x1) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(x1) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(x1) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(3(1(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(2(3(0(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 5#(4(1(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(4(0(5(4(1(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(3(4(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(0(3(4(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 1#(0(0(3(4(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(0(1(x1))) -> 0#(5(4(0(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 1#(2(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(2(1(2(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(0(2(1(2(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 5#(4(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(5(4(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(0(5(4(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 1#(0(0(5(4(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 1#(x1) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 5#(4(1(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(2(5(4(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(0(x1))) -> 0#(0(2(5(4(1(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(1(x1))) -> 0#(3(4(1(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(1(x1))) -> 1#(0(3(4(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(1(x1))) -> 0#(3(4(1(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(1(x1))) -> 5#(0(3(4(1(1(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(3(0(x1)))) -> 1#(3(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(3(0(x1)))) -> 0#(2(1(3(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(3(0(x1)))) -> 0#(2(0(2(1(3(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 5#(x1) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 1#(5(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 5#(4(1(5(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 0#(5(4(1(5(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 0#(0(5(4(1(5(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 1#(0(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 5#(4(2(1(0(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(5(0(x1)))) -> 0#(5(4(2(1(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(0(1(x1)))) -> 0#(x1) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(0(1(x1)))) -> 1#(3(0(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(0(1(x1)))) -> 0#(4(1(3(0(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(0(1(x1)))) -> 0#(0(4(1(3(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(0(x1)))) -> 1#(x1) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(0(x1)))) -> 0#(2(3(1(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(0(x1)))) -> 0#(0(2(3(1(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(1(x1)))) -> 0#(3(4(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(1(x1)))) -> 1#(0(3(4(x1)))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(1(x1)))) -> 1#(1(0(3(4(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(2(5(0(x1))))) -> 0#(2(0(x1))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(2(5(0(x1))))) -> 5#(4(0(2(0(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(2(5(0(x1))))) -> 1#(5(4(0(2(0(x1)))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(4(2(0(x1))))) -> 0#(4(2(3(0(x1))))) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) -> 0#(1(4(2(0(x1))))) -> 1#(0(4(2(3(0(x1)))))) 5#(1(2(0(x1)))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 5#(1(2(0(x1)))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(1(0(x1))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 5#(1(0(x1))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(2(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(4(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(4(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(x1) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(4(1(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(2(3(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(x1) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(5(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(4(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(4(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 1#(3(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(x1) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(x1) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 5#(1(0(x1))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 5#(1(0(x1))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 5#(1(0(x1))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(2(3(0(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 5#(4(1(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(5(4(1(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(4(0(5(4(1(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(3(4(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(0(3(4(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 1#(0(0(3(4(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 5#(4(0(1(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(0(1(x1))) -> 0#(5(4(0(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 1#(2(x1)) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(2(1(2(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(0(2(1(2(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 5#(4(x1)) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(5(4(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(0(5(4(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 1#(0(0(5(4(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 1#(x1) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 5#(4(1(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(2(5(4(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(0(x1))) -> 0#(0(2(5(4(1(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(1(x1))) -> 0#(3(4(1(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(1(x1))) -> 1#(0(3(4(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(1(x1))) -> 0#(3(4(1(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(1(x1))) -> 5#(0(3(4(1(1(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(3(0(x1)))) -> 1#(3(x1)) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(3(0(x1)))) -> 0#(2(1(3(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(3(0(x1)))) -> 0#(2(0(2(1(3(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 5#(x1) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 1#(5(x1)) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 5#(4(1(5(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 0#(5(4(1(5(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 0#(0(5(4(1(5(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 1#(0(x1)) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 5#(4(2(1(0(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(5(0(x1)))) -> 0#(5(4(2(1(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(0(1(x1)))) -> 0#(x1) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(0(1(x1)))) -> 1#(3(0(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(0(1(x1)))) -> 0#(4(1(3(0(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(0(1(x1)))) -> 0#(0(4(1(3(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(0(x1)))) -> 1#(x1) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(0(x1)))) -> 0#(2(3(1(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(0(x1)))) -> 0#(0(2(3(1(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(1(x1)))) -> 0#(3(4(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(1(x1)))) -> 1#(0(3(4(x1)))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(1(x1)))) -> 1#(1(0(3(4(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(2(5(0(x1))))) -> 0#(2(0(x1))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(2(5(0(x1))))) -> 5#(4(0(2(0(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(2(5(0(x1))))) -> 1#(5(4(0(2(0(x1)))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(4(2(0(x1))))) -> 0#(4(2(3(0(x1))))) 0#(3(0(1(x1)))) -> 0#(x1) -> 0#(1(4(2(0(x1))))) -> 1#(0(4(2(3(0(x1)))))) 0#(3(1(0(x1)))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 0#(3(1(0(x1)))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 5#(4(x1)) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(5(4(x1))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 5#(4(4(x1))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 0#(3(1(1(x1)))) -> 5#(1(1(0(3(4(x1)))))) -> 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 0#(1(5(0(x1)))) -> 1#(5(x1)) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 0#(1(5(0(x1)))) -> 1#(5(x1)) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 0#(1(5(0(x1)))) -> 1#(0(x1)) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 0#(1(5(0(x1)))) -> 1#(0(x1)) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(0(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(2(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(2(1(2(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(2(1(2(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(4(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(5(4(4(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(1(4(5(4(4(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 1#(4(4(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(4(1(4(4(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(5(4(1(4(4(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 0#(4(3(0(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(x1))) -> 5#(0(4(3(0(1(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(x1) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(2(2(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(2(2(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(4(1(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(4(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(5(4(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(0(2(2(1(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(2(3(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(5(2(3(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(4(0(5(2(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(4(2(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(0(4(4(2(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(5(0(4(4(2(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 5#(x1) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 0#(4(5(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(0(x1))) -> 1#(0(4(5(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(4(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(5(4(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(1(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(3(4(1(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(5(3(4(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(4(4(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(4(5(4(4(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(1(4(5(4(4(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 5#(2(3(1(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(1(x1))) -> 1#(2(1(5(4(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 1#(3(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(4(1(3(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 0#(0(4(1(3(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(0(x1)))) -> 5#(0(0(4(1(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(4(2(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(5(4(2(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(4(0(5(4(2(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 1#(x1) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 0#(4(2(2(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(2(0(x1)))) -> 5#(0(4(2(2(1(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 0#(2(3(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(4(0(2(3(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(5(4(0(2(3(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 1#(3(0(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(4(0(x1)))) -> 5#(2(1(3(0(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(1(5(1(x1)))) -> 5#(4(1(5(1(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 5#(2(3(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 1#(5(2(3(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(0(1(x1)))) -> 0#(1(5(2(3(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(4(3(5(0(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(x1))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(0(4(3(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(5(0(4(3(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(4(3(1(0(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 5#(x1) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 0#(4(3(5(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(0(x1)))) -> 1#(3(0(4(3(5(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 5#(3(3(4(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(5(3(3(4(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(3(1(1(x1)))) -> 1#(1(5(3(3(4(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 5#(4(0(0(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(0(1(4(0(x1))))) -> 1#(4(5(4(0(0(x1)))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 1#(0(x1)) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 0#(4(1(0(x1)))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(0(4(1(0(x1))))) 0#(1(5(0(x1)))) -> 5#(x1) -> 5#(5(1(0(0(x1))))) -> 5#(5(0(4(1(0(x1)))))) 0#(1(0(x1))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) 0#(1(0(x1))) -> 1#(x1) -> 1#(4(5(1(0(x1))))) -> 5#(4(2(1(1(0(x1)))))) SCC Processor: #sccs: 2 #rules: 7 #arcs: 445/17424 DPs: 5#(3(1(0(x1)))) -> 5#(0(x1)) 5#(0(1(4(0(x1))))) -> 0#(0(x1)) 0#(3(0(1(x1)))) -> 0#(x1) 0#(1(5(0(x1)))) -> 5#(x1) 5#(3(1(0(x1)))) -> 5#(x1) 5#(1(0(x1))) -> 5#(x1) TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) KBO Processor: argument filtering: pi(1) = [0] pi(0) = 0 pi(3) = 0 pi(2) = 0 pi(4) = 0 pi(5) = 0 pi(0#) = 0 pi(5#) = 0 usable rules: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) weight function: w0 = 1 w(5#) = w(0#) = w(4) = w(0) = 1 w(5) = w(2) = w(3) = w(1) = 0 precedence: 5# ~ 0# ~ 5 ~ 4 ~ 2 ~ 3 ~ 0 ~ 1 problem: DPs: TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) Qed DPs: 1#(4(5(1(0(x1))))) -> 1#(1(0(x1))) TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: f90() -> 2* 1{#,0}(4) -> 1* 10(661) -> 662* 10(60) -> 61* 10(257) -> 258* 10(656) -> 657* 10(40) -> 41* 10(636) -> 637* 10(414) -> 415* 10(586) -> 587* 10(167) -> 168* 10(364) -> 365* 10(329) -> 330* 10(309) -> 310* 10(506) -> 507* 10(97) -> 98* 10(688) -> 689* 10(673) -> 674* 10(466) -> 467* 10(254) -> 255* 10(451) -> 452* 10(426) -> 427* 10(598) -> 599* 10(553) -> 554* 10(104) -> 105* 10(690) -> 691* 10(660) -> 661* 10(620) -> 621* 10(398) -> 399* 10(580) -> 581* 10(530) -> 531* 10(303) -> 304* 10(445) -> 446* 10(213) -> 214* 10(11) -> 12* 10(380) -> 381* 10(173) -> 174* 10(168) -> 169* 10(148) -> 149* 10(340) -> 341* 10(330) -> 331* 10(325) -> 326* 10(704) -> 705* 10(68) -> 69* 10(442) -> 443* 10(432) -> 433* 10(230) -> 231* 10(225) -> 226* 10(3) -> 4* 10(347) -> 348* 10(125) -> 126* 10(85) -> 86* 00(80) -> 81* 00(277) -> 278* 00(272) -> 273* 00(464) -> 465* 00(459) -> 460* 00(45) -> 46* 00(222) -> 223* 00(15) -> 16* 00(374) -> 375* 00(324) -> 325* 00(723) -> 724* 00(703) -> 704* 00(289) -> 290* 00(67) -> 68* 00(62) -> 63* 00(229) -> 230* 00(618) -> 619* 00(12) -> 13* 00(2) -> 3* 00(578) -> 579* 00(134) -> 135* 00(129) -> 130* 00(720) -> 721* 00(301) -> 302* 00(84) -> 85* 00(39) -> 40* 00(19) -> 20* 00(378) -> 379* 00(373) -> 374* 00(156) -> 157* 00(151) -> 152* 00(106) -> 107* 00(505) -> 506* 00(702) -> 703* 00(81) -> 82* 00(66) -> 67* 00(21) -> 22* 00(395) -> 396* 00(128) -> 129* 00(108) -> 109* 00(492) -> 493* 00(684) -> 685* 00(63) -> 64* 00(260) -> 261* 00(255) -> 256* 00(654) -> 655* 00(38) -> 39* 00(634) -> 635* 00(427) -> 428* 00(392) -> 393* 00(579) -> 580* 00(564) -> 565* 00(155) -> 156* 00(150) -> 151* 00(736) -> 737* 00(307) -> 308* 00(100) -> 101* 40(621) -> 622* 40(20) -> 21* 40(616) -> 617* 40(606) -> 607* 40(197) -> 198* 40(379) -> 380* 40(576) -> 577* 40(132) -> 133* 40(491) -> 492* 40(653) -> 654* 40(633) -> 634* 40(431) -> 432* 40(17) -> 18* 40(411) -> 412* 40(396) -> 397* 40(391) -> 392* 40(179) -> 180* 40(750) -> 751* 40(149) -> 150* 40(538) -> 539* 40(735) -> 736* 40(528) -> 529* 40(326) -> 327* 40(508) -> 509* 40(306) -> 307* 40(700) -> 701* 40(685) -> 686* 40(675) -> 676* 40(271) -> 272* 40(453) -> 454* 40(251) -> 252* 40(171) -> 172* 40(540) -> 541* 40(535) -> 536* 40(126) -> 127* 40(323) -> 324* 40(520) -> 521* 40(712) -> 713* 40(490) -> 491* 40(687) -> 688* 40(465) -> 466* 40(258) -> 259* 40(253) -> 254* 40(46) -> 47* 40(36) -> 37* 40(228) -> 229* 40(223) -> 224* 40(415) -> 416* 40(183) -> 184* 40(582) -> 583* 40(365) -> 366* 40(562) -> 563* 40(754) -> 755* 40(744) -> 745* 40(507) -> 508* 40(305) -> 306* 40(98) -> 99* 40(43) -> 44* 40(639) -> 640* 40(195) -> 196* 40(372) -> 373* 40(327) -> 328* 40(706) -> 707* 40(504) -> 505* 40(302) -> 303* 20(227) -> 228* 20(212) -> 213* 20(409) -> 410* 20(107) -> 108* 20(501) -> 502* 20(299) -> 300* 20(239) -> 240* 20(608) -> 609* 20(154) -> 155* 20(79) -> 80* 20(276) -> 277* 20(59) -> 60* 20(443) -> 444* 20(221) -> 222* 20(14) -> 15* 20(363) -> 364* 20(560) -> 561* 20(742) -> 743* 20(131) -> 132* 20(495) -> 496* 20(61) -> 62* 20(41) -> 42* 20(552) -> 553* 20(350) -> 351* 20(714) -> 715* 20(275) -> 276* 20(674) -> 675* 20(462) -> 463* 20(200) -> 201* 20(599) -> 600* 20(105) -> 106* 20(489) -> 490* 30(479) -> 480* 30(202) -> 203* 30(349) -> 350* 30(147) -> 148* 30(536) -> 537* 30(461) -> 462* 30(658) -> 659* 30(638) -> 639* 30(37) -> 38* 30(199) -> 200* 30(184) -> 185* 30(99) -> 100* 30(655) -> 656* 30(550) -> 551* 30(722) -> 723* 30(652) -> 653* 30(430) -> 431* 30(592) -> 593* 30(577) -> 578* 30(153) -> 154* 30(103) -> 104* 30(83) -> 84* 30(477) -> 478* 30(13) -> 14* 30(352) -> 353* 50(686) -> 687* 50(676) -> 677* 50(65) -> 66* 50(252) -> 253* 50(429) -> 430* 50(596) -> 597* 50(172) -> 173* 50(339) -> 340* 50(738) -> 739* 50(127) -> 128* 50(259) -> 260* 50(224) -> 225* 50(416) -> 417* 50(169) -> 170* 50(563) -> 564* 50(351) -> 352* 50(124) -> 125* 50(518) -> 519* 50(503) -> 504* 50(493) -> 494* 50(463) -> 464* 50(44) -> 45* 50(241) -> 242* 50(640) -> 641* 50(635) -> 636* 50(413) -> 414* 50(201) -> 202* 50(196) -> 197* 50(393) -> 394* 50(737) -> 738* 50(308) -> 309* 50(101) -> 102* 50(278) -> 279* 50(273) -> 274* 50(622) -> 623* 50(617) -> 618* 50(410) -> 411* 50(375) -> 376* 50(133) -> 134* 50(724) -> 725* 50(300) -> 301* 50(659) -> 660* 50(18) -> 19* 50(397) -> 398* 50(185) -> 186* 50(377) -> 378* 50(549) -> 550* 50(539) -> 540* 50(337) -> 338* 50(529) -> 530* 50(701) -> 702* 50(287) -> 288* 2 -> 124,103,59,36,11 3 -> 684,429,221,147 4 -> 735,673,638,131 12 -> 413,275,153,97,17 13 -> 43* 14 -> 271* 15 -> 549* 16 -> 685,3 18 -> 83* 19 -> 79* 20 -> 460,459,582,287,125 22 -> 685,3 37 -> 251,65 38 -> 658* 39 -> 167* 42 -> 685,3 44 -> 722* 45 -> 430,239 47 -> 685,170,3 60 -> 305* 63 -> 241* 64 -> 13,3 66 -> 329* 67 -> 700,503,489,461,442 69 -> 13,170,3 82 -> 13,3 84 -> 712,501,479,451,339 86 -> 13,3 98 -> 349* 99 -> 337* 102 -> 13,170,3 104 -> 633,299 105 -> 372* 109 -> 13,3 125 -> 652,323 130 -> 13,3 134 -> 714* 135 -> 13,3 148 -> 227* 149 -> 409* 152 -> 3* 157 -> 3* 167 -> 171* 168 -> 183* 169 -> 199,179 170 -> 3* 172 -> 195* 173 -> 528* 174 -> 535,212,68 180 -> 101* 186 -> 68* 198 -> 173* 203 -> 170,3,147 214 -> 46* 226 -> 13,3 229 -> 706,518,495,477,445 231 -> 13,3 240 -> 460,459,582,125 242 -> 460,459,582,125 252 -> 257* 254 -> 750* 255 -> 744,347 256 -> 460,459,582,125 261 -> 460,459,582,125 274 -> 460,459,582,125 277 -> 391* 279 -> 414,289,125 288 -> 414,125 290 -> 414,125 300 -> 395* 301 -> 426* 304 -> 414,125 306 -> 377* 310 -> 414,125 328 -> 414,125 330 -> 363* 331 -> 414,125 338 -> 414,125 340 -> 520* 341 -> 414,125 348 -> 414,125 353 -> 414,125 366 -> 414,125 376 -> 460,459,582,125 381 -> 414,125 394 -> 414,125 399 -> 414,125 412 -> 414,125 417 -> 414,125 428 -> 125* 430 -> 460,459 431 -> 560* 433 -> 125* 443 -> 453* 444 -> 14* 446 -> 443* 452 -> 443* 454 -> 133* 460 -> 582,430 466 -> 576* 467 -> 562,430 478 -> 462* 480 -> 462* 490 -> 690* 492 -> 596* 493 -> 598* 494 -> 466* 496 -> 490* 502 -> 490* 509 -> 460,430 519 -> 504* 521 -> 505* 529 -> 538* 531 -> 552,466 537 -> 720,493 541 -> 530* 551 -> 430* 554 -> 508* 561 -> 460,430,459 563 -> 592* 565 -> 508* 578 -> 620,616,608 579 -> 586* 581 -> 560* 583 -> 563* 586 -> 606* 587 -> 460,430,459 593 -> 2* 597 -> 68* 600 -> 43* 607 -> 577* 609 -> 580* 619 -> 578* 623 -> 560* 637 -> 125* 641 -> 125* 653 -> 742* 657 -> 125* 662 -> 125* 677 -> 12,97 688 -> 754* 689 -> 460,459,582,125 691 -> 14* 705 -> 685* 707 -> 701* 713 -> 701* 715 -> 2* 721 -> 704* 725 -> 685* 739 -> 125* 743 -> 19* 745 -> 563* 751 -> 577* 755 -> 577* problem: DPs: TRS: 0(0(1(x1))) -> 0(2(3(0(1(x1))))) 0(0(1(x1))) -> 0(4(0(5(4(1(x1)))))) 0(0(1(x1))) -> 2(1(0(0(3(4(x1)))))) 0(0(1(x1))) -> 4(0(5(4(0(1(x1)))))) 0(1(0(x1))) -> 0(0(2(1(2(x1))))) 0(1(0(x1))) -> 1(0(0(5(4(x1))))) 0(1(0(x1))) -> 0(0(2(5(4(1(x1)))))) 0(1(1(x1))) -> 1(0(3(4(1(x1))))) 0(1(1(x1))) -> 5(0(3(4(1(1(x1)))))) 5(0(1(x1))) -> 0(5(4(1(x1)))) 5(0(1(x1))) -> 2(5(4(0(1(x1))))) 5(0(1(x1))) -> 5(0(2(1(2(x1))))) 5(0(1(x1))) -> 0(1(4(5(4(4(x1)))))) 5(0(1(x1))) -> 0(5(4(1(4(4(x1)))))) 5(0(1(x1))) -> 5(0(4(3(0(1(x1)))))) 5(1(0(x1))) -> 5(0(2(2(1(x1))))) 5(1(0(x1))) -> 5(0(5(4(1(x1))))) 5(1(0(x1))) -> 0(5(0(2(2(1(x1)))))) 5(1(0(x1))) -> 1(4(0(5(2(3(x1)))))) 5(1(0(x1))) -> 1(5(0(4(4(2(x1)))))) 5(1(0(x1))) -> 4(4(1(0(4(5(x1)))))) 5(1(1(x1))) -> 1(1(5(4(x1)))) 5(1(1(x1))) -> 5(4(1(1(x1)))) 5(1(1(x1))) -> 1(5(3(4(1(x1))))) 5(1(1(x1))) -> 1(1(4(5(4(4(x1)))))) 5(1(1(x1))) -> 3(5(2(3(1(1(x1)))))) 5(1(1(x1))) -> 4(1(2(1(5(4(x1)))))) 0(1(3(0(x1)))) -> 0(2(0(2(1(3(x1)))))) 0(1(5(0(x1)))) -> 0(0(5(4(1(5(x1)))))) 0(1(5(0(x1)))) -> 0(5(4(2(1(0(x1)))))) 0(3(0(1(x1)))) -> 0(0(4(1(3(0(x1)))))) 0(3(1(0(x1)))) -> 0(0(2(3(1(x1))))) 0(3(1(1(x1)))) -> 5(1(1(0(3(4(x1)))))) 5(0(1(0(x1)))) -> 5(0(0(4(1(3(x1)))))) 5(1(2(0(x1)))) -> 1(4(0(5(4(2(x1)))))) 5(1(2(0(x1)))) -> 5(0(4(2(2(1(x1)))))) 5(1(4(0(x1)))) -> 1(5(4(0(2(3(x1)))))) 5(1(4(0(x1)))) -> 4(5(2(1(3(0(x1)))))) 5(1(5(1(x1)))) -> 5(4(1(5(1(x1))))) 5(3(0(1(x1)))) -> 0(1(5(2(3(x1))))) 5(3(1(0(x1)))) -> 1(4(3(5(0(x1))))) 5(3(1(0(x1)))) -> 1(5(0(4(3(x1))))) 5(3(1(0(x1)))) -> 5(4(3(1(0(x1))))) 5(3(1(0(x1)))) -> 1(3(0(4(3(5(x1)))))) 5(3(1(1(x1)))) -> 1(1(5(3(3(4(x1)))))) 0(1(2(5(0(x1))))) -> 1(5(4(0(2(0(x1)))))) 0(1(4(2(0(x1))))) -> 1(0(4(2(3(0(x1)))))) 1(4(5(1(0(x1))))) -> 5(4(2(1(1(0(x1)))))) 5(0(1(4(0(x1))))) -> 1(4(5(4(0(0(x1)))))) 5(5(1(0(0(x1))))) -> 5(5(0(4(1(0(x1)))))) Qed