YES
Problem:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
Proof:
DP Processor:
DPs:
0#(1(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(1(x1))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1))
0#(0(4(5(x1)))) -> 4#(x1)
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(1(4(5(x1)))) -> 4#(x1)
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(1(5(1(x1)))) -> 0#(1(x1))
0#(1(5(3(x1)))) -> 3#(2(1(x1)))
0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(2(4(5(x1)))) -> 4#(x1)
0#(2(4(5(x1)))) -> 0#(4(x1))
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(3(1(5(x1)))) -> 3#(x1)
0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(3(1(5(x1)))) -> 4#(x1)
0#(3(1(5(x1)))) -> 0#(4(x1))
0#(3(1(5(x1)))) -> 3#(0(4(x1)))
0#(3(5(1(x1)))) -> 0#(x1)
0#(3(5(1(x1)))) -> 3#(0(x1))
0#(3(5(1(x1)))) -> 3#(x1)
0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(1(5(x1)))) -> 4#(x1)
0#(4(1(5(x1)))) -> 0#(4(x1))
0#(4(3(5(x1)))) -> 4#(x1)
0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(4(5(1(x1)))) -> 0#(1(x1))
0#(4(5(1(x1)))) -> 4#(0(1(x1)))
0#(4(5(1(x1)))) -> 4#(4(0(1(x1))))
3#(0(1(5(x1)))) -> 4#(x1)
3#(0(1(5(x1)))) -> 0#(5(4(x1)))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1))))
3#(0(1(5(x1)))) -> 3#(1(4(0(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1)
3#(0(3(1(x1)))) -> 3#(2(0(x1)))
3#(0(3(1(x1)))) -> 3#(3(2(0(x1))))
3#(0(3(5(x1)))) -> 3#(x1)
3#(0(3(5(x1)))) -> 0#(2(3(x1)))
3#(0(3(5(x1)))) -> 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1)
3#(3(0(1(x1)))) -> 3#(2(2(3(x1))))
3#(3(0(1(x1)))) -> 0#(1(3(2(2(3(x1))))))
3#(4(5(1(x1)))) -> 4#(2(1(x1)))
3#(4(5(1(x1)))) -> 3#(2(5(4(2(1(x1))))))
4#(1(3(5(x1)))) -> 4#(x1)
4#(1(3(5(x1)))) -> 4#(4(x1))
4#(1(3(5(x1)))) -> 3#(4(4(x1)))
4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
4#(4(1(5(x1)))) -> 4#(x1)
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(1(4(5(5(x1))))) -> 4#(2(5(x1)))
0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(2(1(4(5(x1))))) -> 4#(x1)
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(4(5(4(3(x1))))) -> 4#(4(3(x1)))
0#(4(5(4(3(x1))))) -> 0#(4(4(3(x1))))
0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(5(2(1(5(x1))))) -> 4#(x1)
0#(5(2(1(5(x1))))) -> 0#(4(x1))
0#(5(2(4(1(x1))))) -> 0#(x1)
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(0(1(4(1(x1))))) -> 4#(1(3(1(x1))))
3#(0(1(4(1(x1))))) -> 4#(4(1(3(1(x1)))))
3#(0(1(4(1(x1))))) -> 0#(4(4(1(3(1(x1))))))
3#(0(1(4(1(x1))))) -> 0#(1(1(x1)))
3#(0(1(4(1(x1))))) -> 3#(2(0(1(1(x1)))))
3#(0(1(4(1(x1))))) -> 4#(3(2(0(1(1(x1))))))
3#(0(3(5(5(x1))))) -> 0#(5(x1))
3#(0(3(5(5(x1))))) -> 3#(2(5(0(5(x1)))))
3#(0(3(5(5(x1))))) -> 3#(3(2(5(0(5(x1))))))
3#(0(5(3(1(x1))))) -> 3#(2(5(x1)))
3#(0(5(3(1(x1))))) -> 3#(3(2(5(x1))))
3#(0(5(3(1(x1))))) -> 0#(3(3(2(5(x1)))))
4#(0(1(4(1(x1))))) -> 3#(1(x1))
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
4#(0(1(5(1(x1))))) -> 4#(1(x1))
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
4#(0(2(4(5(x1))))) -> 4#(x1)
4#(0(2(4(5(x1))))) -> 0#(4(x1))
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
4#(1(1(5(1(x1))))) -> 4#(1(x1))
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
4#(5(4(3(1(x1))))) -> 4#(x1)
4#(5(4(3(1(x1))))) -> 3#(4(x1))
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
4#(5(5(3(1(x1))))) -> 4#(x1)
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
TDG Processor:
DPs:
0#(1(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(1(x1))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1))
0#(0(4(5(x1)))) -> 4#(x1)
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(1(4(5(x1)))) -> 4#(x1)
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(1(5(1(x1)))) -> 0#(1(x1))
0#(1(5(3(x1)))) -> 3#(2(1(x1)))
0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(2(4(5(x1)))) -> 4#(x1)
0#(2(4(5(x1)))) -> 0#(4(x1))
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(3(1(5(x1)))) -> 3#(x1)
0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(3(1(5(x1)))) -> 4#(x1)
0#(3(1(5(x1)))) -> 0#(4(x1))
0#(3(1(5(x1)))) -> 3#(0(4(x1)))
0#(3(5(1(x1)))) -> 0#(x1)
0#(3(5(1(x1)))) -> 3#(0(x1))
0#(3(5(1(x1)))) -> 3#(x1)
0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(1(5(x1)))) -> 4#(x1)
0#(4(1(5(x1)))) -> 0#(4(x1))
0#(4(3(5(x1)))) -> 4#(x1)
0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(4(5(1(x1)))) -> 0#(1(x1))
0#(4(5(1(x1)))) -> 4#(0(1(x1)))
0#(4(5(1(x1)))) -> 4#(4(0(1(x1))))
3#(0(1(5(x1)))) -> 4#(x1)
3#(0(1(5(x1)))) -> 0#(5(4(x1)))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1))))
3#(0(1(5(x1)))) -> 3#(1(4(0(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1)
3#(0(3(1(x1)))) -> 3#(2(0(x1)))
3#(0(3(1(x1)))) -> 3#(3(2(0(x1))))
3#(0(3(5(x1)))) -> 3#(x1)
3#(0(3(5(x1)))) -> 0#(2(3(x1)))
3#(0(3(5(x1)))) -> 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1)
3#(3(0(1(x1)))) -> 3#(2(2(3(x1))))
3#(3(0(1(x1)))) -> 0#(1(3(2(2(3(x1))))))
3#(4(5(1(x1)))) -> 4#(2(1(x1)))
3#(4(5(1(x1)))) -> 3#(2(5(4(2(1(x1))))))
4#(1(3(5(x1)))) -> 4#(x1)
4#(1(3(5(x1)))) -> 4#(4(x1))
4#(1(3(5(x1)))) -> 3#(4(4(x1)))
4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
4#(4(1(5(x1)))) -> 4#(x1)
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(1(4(5(5(x1))))) -> 4#(2(5(x1)))
0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(2(1(4(5(x1))))) -> 4#(x1)
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(4(5(4(3(x1))))) -> 4#(4(3(x1)))
0#(4(5(4(3(x1))))) -> 0#(4(4(3(x1))))
0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(5(2(1(5(x1))))) -> 4#(x1)
0#(5(2(1(5(x1))))) -> 0#(4(x1))
0#(5(2(4(1(x1))))) -> 0#(x1)
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(0(1(4(1(x1))))) -> 4#(1(3(1(x1))))
3#(0(1(4(1(x1))))) -> 4#(4(1(3(1(x1)))))
3#(0(1(4(1(x1))))) -> 0#(4(4(1(3(1(x1))))))
3#(0(1(4(1(x1))))) -> 0#(1(1(x1)))
3#(0(1(4(1(x1))))) -> 3#(2(0(1(1(x1)))))
3#(0(1(4(1(x1))))) -> 4#(3(2(0(1(1(x1))))))
3#(0(3(5(5(x1))))) -> 0#(5(x1))
3#(0(3(5(5(x1))))) -> 3#(2(5(0(5(x1)))))
3#(0(3(5(5(x1))))) -> 3#(3(2(5(0(5(x1))))))
3#(0(5(3(1(x1))))) -> 3#(2(5(x1)))
3#(0(5(3(1(x1))))) -> 3#(3(2(5(x1))))
3#(0(5(3(1(x1))))) -> 0#(3(3(2(5(x1)))))
4#(0(1(4(1(x1))))) -> 3#(1(x1))
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
4#(0(1(5(1(x1))))) -> 4#(1(x1))
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
4#(0(2(4(5(x1))))) -> 4#(x1)
4#(0(2(4(5(x1))))) -> 0#(4(x1))
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
4#(1(1(5(1(x1))))) -> 4#(1(x1))
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
4#(5(4(3(1(x1))))) -> 4#(x1)
4#(5(4(3(1(x1))))) -> 3#(4(x1))
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
4#(5(5(3(1(x1))))) -> 4#(x1)
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
graph:
...
Arctic Interpretation Processor:
dimension: 1
interpretation:
[4#](x0) = x0,
[3#](x0) = x0,
[0#](x0) = x0,
[5](x0) = 1x0,
[4](x0) = x0,
[3](x0) = x0,
[2](x0) = x0,
[0](x0) = x0,
[1](x0) = x0
orientation:
0#(1(1(x1))) = x1 >= x1 = 0#(x1)
0#(3(1(x1))) = x1 >= x1 = 0#(x1)
0#(3(1(x1))) = x1 >= x1 = 3#(2(2(0(x1))))
0#(3(1(x1))) = x1 >= x1 = 3#(2(1(2(0(x1)))))
0#(3(1(x1))) = x1 >= x1 = 3#(2(0(x1)))
0#(3(1(x1))) = x1 >= x1 = 3#(3(2(0(x1))))
0#(3(1(x1))) = x1 >= x1 = 3#(3(3(2(0(x1)))))
0#(4(1(x1))) = x1 >= x1 = 4#(x1)
0#(4(1(x1))) = x1 >= x1 = 0#(4(x1))
0#(0(4(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(0(4(5(x1)))) = 1x1 >= 1x1 = 0#(2(5(4(x1))))
0#(0(4(5(x1)))) = 1x1 >= 1x1 = 0#(0(2(5(4(x1)))))
0#(1(4(1(x1)))) = x1 >= x1 = 0#(1(2(2(4(1(x1))))))
0#(1(4(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(1(4(5(x1)))) = 1x1 >= 1x1 = 0#(1(2(5(4(x1)))))
0#(1(4(5(x1)))) = 1x1 >= 1x1 = 4#(0(1(2(5(4(x1))))))
0#(1(5(1(x1)))) = 1x1 >= x1 = 0#(1(x1))
0#(1(5(3(x1)))) = 1x1 >= x1 = 3#(2(1(x1)))
0#(1(5(3(x1)))) = 1x1 >= 1x1 = 0#(5(3(2(1(x1)))))
0#(2(4(1(x1)))) = x1 >= x1 = 4#(x1)
0#(2(4(1(x1)))) = x1 >= x1 = 0#(4(x1))
0#(2(4(1(x1)))) = x1 >= x1 = 3#(2(0(4(x1))))
0#(2(4(1(x1)))) = x1 >= x1 = 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) = x1 >= x1 = 4#(2(1(2(0(4(x1))))))
0#(2(4(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(2(4(5(x1)))) = 1x1 >= x1 = 0#(4(x1))
0#(2(4(5(x1)))) = 1x1 >= 1x1 = 0#(2(2(5(0(4(x1))))))
0#(3(1(5(x1)))) = 1x1 >= x1 = 3#(x1)
0#(3(1(5(x1)))) = 1x1 >= 1x1 = 0#(1(2(5(3(x1)))))
0#(3(1(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(3(1(5(x1)))) = 1x1 >= x1 = 0#(4(x1))
0#(3(1(5(x1)))) = 1x1 >= x1 = 3#(0(4(x1)))
0#(3(5(1(x1)))) = 1x1 >= x1 = 0#(x1)
0#(3(5(1(x1)))) = 1x1 >= x1 = 3#(0(x1))
0#(3(5(1(x1)))) = 1x1 >= x1 = 3#(x1)
0#(3(5(1(x1)))) = 1x1 >= 1x1 = 0#(5(2(1(2(3(x1))))))
0#(3(5(5(x1)))) = 2x1 >= 2x1 = 3#(2(5(5(x1))))
0#(3(5(5(x1)))) = 2x1 >= 2x1 = 0#(3(2(5(5(x1)))))
0#(4(0(1(x1)))) = x1 >= x1 = 4#(4(0(1(x1))))
0#(4(0(1(x1)))) = x1 >= x1 = 0#(4(4(0(1(x1)))))
0#(4(1(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(4(1(5(x1)))) = 1x1 >= x1 = 0#(4(x1))
0#(4(3(5(x1)))) = 1x1 >= x1 = 4#(x1)
0#(4(3(5(x1)))) = 1x1 >= 1x1 = 3#(2(5(4(x1))))
0#(4(3(5(x1)))) = 1x1 >= 1x1 = 4#(3(2(5(4(x1)))))
0#(4(3(5(x1)))) = 1x1 >= 1x1 = 0#(4(3(2(5(4(x1))))))
0#(4(5(1(x1)))) = 1x1 >= x1 = 0#(1(x1))
0#(4(5(1(x1)))) = 1x1 >= x1 = 4#(0(1(x1)))
0#(4(5(1(x1)))) = 1x1 >= x1 = 4#(4(0(1(x1))))
3#(0(1(5(x1)))) = 1x1 >= x1 = 4#(x1)
3#(0(1(5(x1)))) = 1x1 >= 1x1 = 0#(5(4(x1)))
3#(0(1(5(x1)))) = 1x1 >= 1x1 = 4#(0(5(4(x1))))
3#(0(1(5(x1)))) = 1x1 >= 1x1 = 3#(1(4(0(5(4(x1))))))
3#(0(3(1(x1)))) = x1 >= x1 = 0#(x1)
3#(0(3(1(x1)))) = x1 >= x1 = 3#(2(0(x1)))
3#(0(3(1(x1)))) = x1 >= x1 = 3#(3(2(0(x1))))
3#(0(3(5(x1)))) = 1x1 >= x1 = 3#(x1)
3#(0(3(5(x1)))) = 1x1 >= x1 = 0#(2(3(x1)))
3#(0(3(5(x1)))) = 1x1 >= 1x1 = 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) = x1 >= x1 = 3#(x1)
3#(3(0(1(x1)))) = x1 >= x1 = 3#(2(2(3(x1))))
3#(3(0(1(x1)))) = x1 >= x1 = 0#(1(3(2(2(3(x1))))))
3#(4(5(1(x1)))) = 1x1 >= x1 = 4#(2(1(x1)))
3#(4(5(1(x1)))) = 1x1 >= 1x1 = 3#(2(5(4(2(1(x1))))))
4#(1(3(5(x1)))) = 1x1 >= x1 = 4#(x1)
4#(1(3(5(x1)))) = 1x1 >= x1 = 4#(4(x1))
4#(1(3(5(x1)))) = 1x1 >= x1 = 3#(4(4(x1)))
4#(1(5(1(x1)))) = 1x1 >= 1x1 = 4#(5(1(2(1(x1)))))
4#(1(5(1(x1)))) = 1x1 >= 1x1 = 4#(4(5(1(2(1(x1))))))
4#(4(1(5(x1)))) = 1x1 >= x1 = 4#(x1)
4#(4(1(5(x1)))) = 1x1 >= 1x1 = 4#(1(2(5(4(x1)))))
0#(1(4(5(5(x1))))) = 2x1 >= 1x1 = 4#(2(5(x1)))
0#(1(4(5(5(x1))))) = 2x1 >= 2x1 = 0#(5(1(4(2(5(x1))))))
0#(2(1(4(5(x1))))) = 1x1 >= x1 = 4#(x1)
0#(2(1(4(5(x1))))) = 1x1 >= 1x1 = 0#(1(2(5(4(x1)))))
0#(2(1(4(5(x1))))) = 1x1 >= 1x1 = 0#(0(1(2(5(4(x1))))))
0#(2(1(5(5(x1))))) = 2x1 >= 2x1 = 0#(1(2(2(5(5(x1))))))
0#(4(2(4(1(x1))))) = x1 >= x1 = 4#(x1)
0#(4(2(4(1(x1))))) = x1 >= x1 = 4#(4(x1))
0#(4(2(4(1(x1))))) = x1 >= x1 = 0#(4(4(x1)))
0#(4(2(4(1(x1))))) = x1 >= x1 = 3#(2(0(4(4(x1)))))
0#(4(5(4(3(x1))))) = 1x1 >= x1 = 4#(4(3(x1)))
0#(4(5(4(3(x1))))) = 1x1 >= x1 = 0#(4(4(3(x1))))
0#(5(1(5(1(x1))))) = 2x1 >= 2x1 = 0#(5(1(1(2(5(x1))))))
0#(5(2(1(5(x1))))) = 2x1 >= x1 = 4#(x1)
0#(5(2(1(5(x1))))) = 2x1 >= x1 = 0#(4(x1))
0#(5(2(4(1(x1))))) = 1x1 >= x1 = 0#(x1)
0#(5(2(4(1(x1))))) = 1x1 >= 1x1 = 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) = x1 >= x1 = 3#(1(x1))
3#(0(1(4(1(x1))))) = x1 >= x1 = 4#(1(3(1(x1))))
3#(0(1(4(1(x1))))) = x1 >= x1 = 4#(4(1(3(1(x1)))))
3#(0(1(4(1(x1))))) = x1 >= x1 = 0#(4(4(1(3(1(x1))))))
3#(0(1(4(1(x1))))) = x1 >= x1 = 0#(1(1(x1)))
3#(0(1(4(1(x1))))) = x1 >= x1 = 3#(2(0(1(1(x1)))))
3#(0(1(4(1(x1))))) = x1 >= x1 = 4#(3(2(0(1(1(x1))))))
3#(0(3(5(5(x1))))) = 2x1 >= 1x1 = 0#(5(x1))
3#(0(3(5(5(x1))))) = 2x1 >= 2x1 = 3#(2(5(0(5(x1)))))
3#(0(3(5(5(x1))))) = 2x1 >= 2x1 = 3#(3(2(5(0(5(x1))))))
3#(0(5(3(1(x1))))) = 1x1 >= 1x1 = 3#(2(5(x1)))
3#(0(5(3(1(x1))))) = 1x1 >= 1x1 = 3#(3(2(5(x1))))
3#(0(5(3(1(x1))))) = 1x1 >= 1x1 = 0#(3(3(2(5(x1)))))
4#(0(1(4(1(x1))))) = x1 >= x1 = 3#(1(x1))
4#(0(1(4(1(x1))))) = x1 >= x1 = 0#(1(3(1(x1))))
4#(0(1(4(1(x1))))) = x1 >= x1 = 4#(0(1(3(1(x1)))))
4#(0(1(4(1(x1))))) = x1 >= x1 = 4#(4(0(1(3(1(x1))))))
4#(0(1(5(1(x1))))) = 1x1 >= x1 = 4#(1(x1))
4#(0(1(5(1(x1))))) = 1x1 >= 1x1 = 0#(1(2(5(4(1(x1))))))
4#(0(2(4(5(x1))))) = 1x1 >= x1 = 4#(x1)
4#(0(2(4(5(x1))))) = 1x1 >= x1 = 0#(4(x1))
4#(0(2(4(5(x1))))) = 1x1 >= 1x1 = 0#(2(5(0(4(x1)))))
4#(0(2(4(5(x1))))) = 1x1 >= 1x1 = 4#(0(2(5(0(4(x1))))))
4#(1(1(5(1(x1))))) = 1x1 >= x1 = 4#(1(x1))
4#(5(1(4(1(x1))))) = 1x1 >= 1x1 = 4#(1(2(1(5(x1)))))
4#(5(1(4(1(x1))))) = 1x1 >= 1x1 = 4#(4(1(2(1(5(x1))))))
4#(5(2(3(1(x1))))) = 1x1 >= 1x1 = 3#(1(2(2(5(x1)))))
4#(5(2(3(1(x1))))) = 1x1 >= 1x1 = 4#(3(1(2(2(5(x1))))))
4#(5(4(3(1(x1))))) = 1x1 >= x1 = 4#(x1)
4#(5(4(3(1(x1))))) = 1x1 >= x1 = 3#(4(x1))
4#(5(4(3(1(x1))))) = 1x1 >= 1x1 = 4#(1(2(5(3(4(x1))))))
4#(5(5(3(1(x1))))) = 2x1 >= x1 = 4#(x1)
4#(5(5(3(1(x1))))) = 2x1 >= 2x1 = 3#(2(5(5(4(x1)))))
0(1(1(x1))) = x1 >= x1 = 1(2(1(2(0(x1)))))
0(3(1(x1))) = x1 >= x1 = 1(3(2(2(0(x1)))))
0(3(1(x1))) = x1 >= x1 = 3(2(1(2(0(x1)))))
0(3(1(x1))) = x1 >= x1 = 1(3(3(3(2(0(x1))))))
0(4(1(x1))) = x1 >= x1 = 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) = 1x1 >= 1x1 = 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) = x1 >= x1 = 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) = 1x1 >= 1x1 = 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) = 1x1 >= 1x1 = 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) = 1x1 >= 1x1 = 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) = x1 >= x1 = 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) = x1 >= x1 = 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) = 1x1 >= 1x1 = 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) = 1x1 >= 1x1 = 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) = 1x1 >= 1x1 = 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) = 1x1 >= 1x1 = 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) = 1x1 >= 1x1 = 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) = 2x1 >= 2x1 = 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) = x1 >= x1 = 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) = 1x1 >= 1x1 = 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) = 1x1 >= 1x1 = 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) = 1x1 >= 1x1 = 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) = 1x1 >= 1x1 = 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) = x1 >= x1 = 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) = 1x1 >= 1x1 = 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) = x1 >= x1 = 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) = 1x1 >= 1x1 = 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) = 1x1 >= 1x1 = 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) = 1x1 >= 1x1 = 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) = 1x1 >= 1x1 = 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) = 2x1 >= 2x1 = 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) = 1x1 >= 1x1 = 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) = 2x1 >= 2x1 = 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) = x1 >= x1 = 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) = 1x1 >= 1x1 = 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) = 2x1 >= 2x1 = 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) = 2x1 >= 2x1 = 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) = 1x1 >= 1x1 = 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) = x1 >= x1 = 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) = x1 >= x1 = 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) = 2x1 >= 2x1 = 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) = 1x1 >= 1x1 = 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) = x1 >= x1 = 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) = 1x1 >= 1x1 = 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) = 1x1 >= 1x1 = 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) = 1x1 >= 1x1 = 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) = 1x1 >= 1x1 = 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) = 1x1 >= 1x1 = 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) = 1x1 >= 1x1 = 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) = 2x1 >= 2x1 = 1(3(2(5(5(4(x1))))))
problem:
DPs:
0#(1(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(1(x1))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1))
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
3#(0(1(5(x1)))) -> 0#(5(4(x1)))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1))))
3#(0(1(5(x1)))) -> 3#(1(4(0(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1)
3#(0(3(1(x1)))) -> 3#(2(0(x1)))
3#(0(3(1(x1)))) -> 3#(3(2(0(x1))))
3#(0(3(5(x1)))) -> 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1)
3#(3(0(1(x1)))) -> 3#(2(2(3(x1))))
3#(3(0(1(x1)))) -> 0#(1(3(2(2(3(x1))))))
3#(4(5(1(x1)))) -> 3#(2(5(4(2(1(x1))))))
4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(0(1(4(1(x1))))) -> 4#(1(3(1(x1))))
3#(0(1(4(1(x1))))) -> 4#(4(1(3(1(x1)))))
3#(0(1(4(1(x1))))) -> 0#(4(4(1(3(1(x1))))))
3#(0(1(4(1(x1))))) -> 0#(1(1(x1)))
3#(0(1(4(1(x1))))) -> 3#(2(0(1(1(x1)))))
3#(0(1(4(1(x1))))) -> 4#(3(2(0(1(1(x1))))))
3#(0(3(5(5(x1))))) -> 3#(2(5(0(5(x1)))))
3#(0(3(5(5(x1))))) -> 3#(3(2(5(0(5(x1))))))
3#(0(5(3(1(x1))))) -> 3#(2(5(x1)))
3#(0(5(3(1(x1))))) -> 3#(3(2(5(x1))))
3#(0(5(3(1(x1))))) -> 0#(3(3(2(5(x1)))))
4#(0(1(4(1(x1))))) -> 3#(1(x1))
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
EDG Processor:
DPs:
0#(1(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(1(x1))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1))
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
3#(0(1(5(x1)))) -> 0#(5(4(x1)))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1))))
3#(0(1(5(x1)))) -> 3#(1(4(0(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1)
3#(0(3(1(x1)))) -> 3#(2(0(x1)))
3#(0(3(1(x1)))) -> 3#(3(2(0(x1))))
3#(0(3(5(x1)))) -> 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1)
3#(3(0(1(x1)))) -> 3#(2(2(3(x1))))
3#(3(0(1(x1)))) -> 0#(1(3(2(2(3(x1))))))
3#(4(5(1(x1)))) -> 3#(2(5(4(2(1(x1))))))
4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(0(1(4(1(x1))))) -> 4#(1(3(1(x1))))
3#(0(1(4(1(x1))))) -> 4#(4(1(3(1(x1)))))
3#(0(1(4(1(x1))))) -> 0#(4(4(1(3(1(x1))))))
3#(0(1(4(1(x1))))) -> 0#(1(1(x1)))
3#(0(1(4(1(x1))))) -> 3#(2(0(1(1(x1)))))
3#(0(1(4(1(x1))))) -> 4#(3(2(0(1(1(x1))))))
3#(0(3(5(5(x1))))) -> 3#(2(5(0(5(x1)))))
3#(0(3(5(5(x1))))) -> 3#(3(2(5(0(5(x1))))))
3#(0(5(3(1(x1))))) -> 3#(2(5(x1)))
3#(0(5(3(1(x1))))) -> 3#(3(2(5(x1))))
3#(0(5(3(1(x1))))) -> 0#(3(3(2(5(x1)))))
4#(0(1(4(1(x1))))) -> 3#(1(x1))
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
graph:
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(1(5(x1)))) -> 0#(5(4(x1)))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(1(5(x1)))) -> 4#(0(5(4(x1))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(1(5(x1)))) -> 3#(1(4(0(5(4(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(3(1(x1)))) -> 0#(x1)
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(3(1(x1)))) -> 3#(2(0(x1)))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(3(1(x1)))) -> 3#(3(2(0(x1))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(3(5(x1)))) -> 3#(2(5(0(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(3(0(1(x1)))) -> 3#(x1)
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(3(0(1(x1)))) -> 3#(2(2(3(x1))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(3(0(1(x1)))) -> 0#(1(3(2(2(3(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(4(5(1(x1)))) -> 3#(2(5(4(2(1(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(1(4(1(x1))))) -> 4#(1(3(1(x1))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(1(4(1(x1))))) -> 4#(4(1(3(1(x1)))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(1(4(1(x1))))) -> 0#(4(4(1(3(1(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(1(4(1(x1))))) -> 0#(1(1(x1)))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(1(4(1(x1))))) -> 3#(2(0(1(1(x1)))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(1(4(1(x1))))) -> 4#(3(2(0(1(1(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(3(5(5(x1))))) -> 3#(2(5(0(5(x1)))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(3(5(5(x1))))) -> 3#(3(2(5(0(5(x1))))))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(5(3(1(x1))))) -> 3#(2(5(x1)))
3#(3(0(1(x1)))) -> 3#(x1) -> 3#(0(5(3(1(x1))))) -> 3#(3(2(5(x1))))
3#(3(0(1(x1)))) -> 3#(x1) ->
3#(0(5(3(1(x1))))) -> 0#(3(3(2(5(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(1(1(x1))) -> 0#(x1)
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 0#(x1)
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(2(0(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(0(x1)))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(2(0(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(1(x1))) -> 4#(x1)
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(1(x1))) -> 0#(4(x1))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 4#(x1)
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 0#(4(x1))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(x1)
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(4(x1))
3#(0(3(1(x1)))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
3#(0(3(1(x1)))) -> 0#(x1) ->
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(1(4(1(x1))))) -> 3#(1(x1))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
3#(0(1(5(x1)))) -> 4#(0(5(4(x1)))) ->
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
3#(0(1(5(x1)))) -> 0#(5(4(x1))) ->
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
3#(0(1(4(1(x1))))) -> 0#(1(1(x1))) -> 0#(1(1(x1))) -> 0#(x1)
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(1(4(1(x1))))) -> 3#(1(x1))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
0#(4(2(4(1(x1))))) -> 4#(4(x1)) ->
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 3#(1(x1))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
0#(4(2(4(1(x1))))) -> 4#(x1) ->
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(1(1(x1))) -> 0#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 0#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(1(x1))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(1(x1))) -> 0#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(1(x1)))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(2(4(1(x1))))) -> 0#(4(4(x1))) ->
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(1(4(1(x1))))) -> 3#(1(x1))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
0#(4(0(1(x1)))) -> 4#(4(0(1(x1)))) ->
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(1(1(x1))) -> 0#(x1)
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 0#(x1)
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 3#(2(0(x1)))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(1(x1))) -> 4#(x1)
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(1(x1))) -> 0#(4(x1))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(1(x1)))) -> 4#(x1)
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) ->
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 3#(1(x1))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
0#(4(1(x1))) -> 4#(x1) -> 4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(1(1(x1))) -> 0#(x1)
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 0#(x1)
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(2(0(x1)))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(1(x1))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(1(x1))) -> 0#(4(x1))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 0#(4(x1))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(4(1(x1))) -> 0#(4(x1)) ->
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 4#(x1)
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(1(x1))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 0#(x1)
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(0(x1)))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(1(x1))) -> 4#(x1)
0#(3(1(x1))) -> 0#(x1) -> 0#(4(1(x1))) -> 0#(4(x1))
0#(3(1(x1))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 4#(x1)
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 0#(4(x1))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(x1)
0#(3(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(3(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(3(1(x1))) -> 0#(x1) -> 0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(3(1(x1))) -> 0#(x1) ->
0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) -> 4#(1(5(1(x1)))) -> 4#(5(1(2(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(1(5(1(x1)))) -> 4#(4(5(1(2(1(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) -> 4#(4(1(5(x1)))) -> 4#(1(2(5(4(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 3#(1(x1))
0#(2(4(1(x1)))) -> 4#(x1) -> 4#(0(1(4(1(x1))))) -> 0#(1(3(1(x1))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(0(1(4(1(x1))))) -> 4#(0(1(3(1(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(0(1(4(1(x1))))) -> 4#(4(0(1(3(1(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(0(1(5(1(x1))))) -> 0#(1(2(5(4(1(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(0(2(4(5(x1))))) -> 0#(2(5(0(4(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(0(2(4(5(x1))))) -> 4#(0(2(5(0(4(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(1(4(1(x1))))) -> 4#(1(2(1(5(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(1(4(1(x1))))) -> 4#(4(1(2(1(5(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(2(3(1(x1))))) -> 3#(1(2(2(5(x1)))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(2(3(1(x1))))) -> 4#(3(1(2(2(5(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(4(3(1(x1))))) -> 4#(1(2(5(3(4(x1))))))
0#(2(4(1(x1)))) -> 4#(x1) ->
4#(5(5(3(1(x1))))) -> 3#(2(5(5(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(1(1(x1))) -> 0#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 0#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(2(0(x1)))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(4(1(x1))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(4(1(x1))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(2(4(1(x1)))) -> 0#(4(x1))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 4#(x1)
0#(2(4(1(x1)))) -> 0#(4(x1)) -> 0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(2(4(1(x1)))) -> 0#(4(x1)) ->
0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(1(x1))) -> 0#(x1)
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 0#(x1)
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(2(0(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(1(2(0(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(2(0(x1)))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(2(0(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(x1))) -> 3#(3(3(2(0(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(1(x1))) -> 4#(x1)
0#(1(1(x1))) -> 0#(x1) -> 0#(4(1(x1))) -> 0#(4(x1))
0#(1(1(x1))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(2(5(4(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(0(4(5(x1)))) -> 0#(0(2(5(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(4(1(x1)))) -> 0#(1(2(2(4(1(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(4(5(x1)))) -> 0#(1(2(5(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(4(5(x1)))) -> 4#(0(1(2(5(4(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(5(3(x1)))) -> 0#(5(3(2(1(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 4#(x1)
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 0#(4(x1))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(2(0(4(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 3#(3(2(0(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(1(x1)))) -> 4#(2(1(2(0(4(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(4(5(x1)))) -> 0#(2(2(5(0(4(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(1(5(x1)))) -> 0#(1(2(5(3(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(5(1(x1)))) -> 0#(5(2(1(2(3(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 3#(2(5(5(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(3(5(5(x1)))) -> 0#(3(2(5(5(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 4#(4(0(1(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 3#(2(5(4(x1))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 4#(3(2(5(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(3(5(x1)))) -> 0#(4(3(2(5(4(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(1(4(5(5(x1))))) -> 0#(5(1(4(2(5(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(1(4(5(x1))))) -> 0#(1(2(5(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(1(4(5(x1))))) -> 0#(0(1(2(5(4(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(2(1(5(5(x1))))) -> 0#(1(2(2(5(5(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(x1)
0#(1(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 4#(4(x1))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(1(1(x1))) -> 0#(x1) -> 0#(4(2(4(1(x1))))) -> 3#(2(0(4(4(x1)))))
0#(1(1(x1))) -> 0#(x1) -> 0#(5(1(5(1(x1))))) -> 0#(5(1(1(2(5(x1))))))
0#(1(1(x1))) -> 0#(x1) -> 0#(5(2(4(1(x1))))) -> 4#(5(2(1(2(0(x1))))))
SCC Processor:
#sccs: 2
#rules: 7
#arcs: 330/6241
DPs:
3#(3(0(1(x1)))) -> 3#(x1)
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
Arctic Interpretation Processor:
dimension: 1
interpretation:
[3#](x0) = x0,
[5](x0) = x0,
[4](x0) = x0,
[3](x0) = x0,
[2](x0) = x0,
[0](x0) = x0,
[1](x0) = 1x0
orientation:
3#(3(0(1(x1)))) = 1x1 >= x1 = 3#(x1)
0(1(1(x1))) = 2x1 >= 2x1 = 1(2(1(2(0(x1)))))
0(3(1(x1))) = 1x1 >= 1x1 = 1(3(2(2(0(x1)))))
0(3(1(x1))) = 1x1 >= 1x1 = 3(2(1(2(0(x1)))))
0(3(1(x1))) = 1x1 >= 1x1 = 1(3(3(3(2(0(x1))))))
0(4(1(x1))) = 1x1 >= 1x1 = 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) = x1 >= x1 = 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) = 2x1 >= 2x1 = 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) = 1x1 >= 1x1 = 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) = 2x1 >= 2x1 = 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) = 1x1 >= 1x1 = 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) = 1x1 >= 1x1 = 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) = 1x1 >= 1x1 = 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) = x1 >= x1 = 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) = 1x1 >= 1x1 = 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) = 1x1 >= 1x1 = 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) = 1x1 >= 1x1 = 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) = 1x1 >= 1x1 = 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) = x1 >= x1 = 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) = 1x1 >= 1x1 = 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) = 1x1 >= 1x1 = 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) = x1 >= x1 = 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) = 1x1 >= 1x1 = 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) = 1x1 >= 1x1 = 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) = 1x1 >= 1x1 = 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) = x1 >= x1 = 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) = 1x1 >= 1x1 = 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) = 1x1 >= 1x1 = 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) = 1x1 >= 1x1 = 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) = 2x1 >= 2x1 = 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) = 1x1 >= 1x1 = 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) = 1x1 >= 1x1 = 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) = 1x1 >= 1x1 = 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) = 1x1 >= 1x1 = 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) = 1x1 >= 1x1 = 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) = x1 >= x1 = 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) = 2x1 >= 2x1 = 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) = 1x1 >= 1x1 = 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) = 1x1 >= 1x1 = 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) = 2x1 >= 2x1 = 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) = 2x1 >= 2x1 = 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) = x1 >= x1 = 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) = 1x1 >= 1x1 = 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) = 2x1 >= 2x1 = 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) = 2x1 >= 2x1 = 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) = x1 >= x1 = 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) = 3x1 >= 3x1 = 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) = 2x1 >= 2x1 = 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) = 1x1 >= 1x1 = 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) = 1x1 >= 1x1 = 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) = 1x1 >= 1x1 = 1(3(2(5(5(4(x1))))))
problem:
DPs:
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
Qed
DPs:
0#(1(1(x1))) -> 0#(x1)
0#(4(2(4(1(x1))))) -> 0#(4(4(x1)))
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
0#(2(4(1(x1)))) -> 0#(4(x1))
0#(4(1(x1))) -> 0#(4(x1))
0#(3(1(x1))) -> 0#(x1)
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
KBO Processor:
argument filtering:
pi(1) = [0]
pi(0) = 0
pi(2) = 0
pi(3) = 0
pi(4) = 0
pi(5) = 0
pi(0#) = 0
weight function:
w0 = 1
w(0#) = w(5) = w(4) = w(3) = w(2) = w(0) = w(1) = 0
precedence:
0# ~ 5 ~ 4 ~ 3 ~ 2 ~ 0 ~ 1
problem:
DPs:
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
EDG Processor:
DPs:
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
graph:
0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1))))) -> 0#(4(0(1(x1)))) -> 0#(4(4(0(1(x1)))))
Matrix Interpretation Processor: dim=4
interpretation:
[0#](x0) = [0 0 1 1]x0,
[1]
[0]
[5](x0) = [0]
[0],
[0 0 0 0]
[0 0 0 0]
[4](x0) = [1 0 0 0]x0
[0 0 1 0] ,
[0 0 0 0]
[0 0 1 0]
[3](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[0 0 0 0]
[0 1 0 0]
[2](x0) = [0 0 0 0]x0
[0 1 0 0] ,
[0 0 1 1] [0]
[0 0 0 0] [0]
[0](x0) = [0 0 0 0]x0 + [1]
[0 1 0 0] [0],
[0 0 0 0]
[0 0 1 0]
[1](x0) = [1 0 0 0]x0
[0 0 0 0]
orientation:
0#(4(0(1(x1)))) = [1 0 0 0]x1 + [1] >= [1 0 0 0]x1 = 0#(4(4(0(1(x1)))))
[0 0 0 0] [0] [0]
[0 0 0 0] [0] [0]
0(1(1(x1))) = [0 0 0 0]x1 + [1] >= [0] = 1(2(1(2(0(x1)))))
[1 0 0 0] [0] [0]
[1 0 0 0] [0] [0]
[0 0 0 0] [0] [0]
0(3(1(x1))) = [0 0 0 0]x1 + [1] >= [0] = 1(3(2(2(0(x1)))))
[1 0 0 0] [0] [0]
[1 0 0 0] [0] [0]
[0 0 0 0] [0] [0]
0(3(1(x1))) = [0 0 0 0]x1 + [1] >= [0] = 3(2(1(2(0(x1)))))
[1 0 0 0] [0] [0]
[1 0 0 0] [0] [0]
[0 0 0 0] [0] [0]
0(3(1(x1))) = [0 0 0 0]x1 + [1] >= [0] = 1(3(3(3(2(0(x1))))))
[1 0 0 0] [0] [0]
[1 0 0 0] [0] [0]
[0 0 0 0] [0] [0]
0(4(1(x1))) = [0 0 0 0]x1 + [1] >= [0] = 2(1(2(0(4(x1)))))
[0 0 0 0] [0] [0]
[1] [1]
[0] [0]
0(0(4(5(x1)))) = [1] >= [1] = 0(0(2(5(4(x1)))))
[0] [0]
[0] [0]
[0] [0]
0(1(4(1(x1)))) = [1] >= [1] = 0(1(2(2(4(1(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(1(4(5(x1)))) = [1] >= [0] = 4(0(1(2(5(4(x1))))))
[1] [1]
[1] [0]
[0] [0]
0(1(5(1(x1)))) = [1] >= [0] = 1(2(2(5(0(1(x1))))))
[0] [0]
[1] [0]
[0] [0]
0(1(5(3(x1)))) = [1] >= [1] = 0(5(3(2(1(x1)))))
[0] [0]
[0] [0]
[0] [0]
0(2(4(1(x1)))) = [1] >= [0] = 1(3(3(2(0(4(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(2(4(1(x1)))) = [1] >= [0] = 4(2(1(2(0(4(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(2(4(5(x1)))) = [1] >= [1] = 0(2(2(5(0(4(x1))))))
[0] [0]
[1] [0]
[0] [0]
0(3(1(5(x1)))) = [1] >= [1] = 0(1(2(5(3(x1)))))
[1] [0]
[1] [0]
[0] [0]
0(3(1(5(x1)))) = [1] >= [0] = 1(2(5(3(0(4(x1))))))
[1] [0]
[0] [0]
[0] [0]
0(3(5(1(x1)))) = [1] >= [0] = 1(2(5(3(0(x1)))))
[0] [0]
[0] [0]
[0] [0]
0(3(5(1(x1)))) = [1] >= [1] = 0(5(2(1(2(3(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(3(5(5(x1)))) = [1] >= [1] = 0(3(2(5(5(x1)))))
[0] [0]
[1 0 0 0] [1] [0]
[0 0 0 0] [0] [0]
0(4(0(1(x1)))) = [0 0 0 0]x1 + [1] >= [0] = 2(0(4(4(0(1(x1))))))
[0 0 0 0] [0] [0]
[1] [0]
[0] [0]
0(4(1(5(x1)))) = [1] >= [0] = 1(2(5(0(4(x1)))))
[0] [0]
[0] [0]
[0] [0]
0(4(3(5(x1)))) = [1] >= [1] = 0(4(3(2(5(4(x1))))))
[0] [0]
[1] [0]
[0] [0]
0(4(5(1(x1)))) = [1] >= [0] = 2(5(4(4(0(1(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(0(1(5(x1)))) = [1] >= [0] = 3(1(4(0(5(4(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(0(3(1(x1)))) = [1] >= [0] = 1(3(3(2(0(x1)))))
[0] [0]
[0] [0]
[1] [0]
3(0(3(5(x1)))) = [1] >= [0] = 3(2(5(0(2(3(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(3(0(1(x1)))) = [1] >= [1] = 0(1(3(2(2(3(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(4(5(1(x1)))) = [1] >= [0] = 3(2(5(4(2(1(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(1(3(5(x1)))) = [0] >= [0] = 1(2(5(3(4(4(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(1(5(1(x1)))) = [0] >= [0] = 4(4(5(1(2(1(x1))))))
[1] [1]
[0] [0]
[0] [0]
4(4(1(5(x1)))) = [0] >= [0] = 4(1(2(5(4(x1)))))
[0] [0]
[0] [0]
[0] [0]
0(1(4(5(5(x1))))) = [1] >= [1] = 0(5(1(4(2(5(x1))))))
[1] [0]
[1] [1]
[0] [0]
0(2(1(4(5(x1))))) = [1] >= [1] = 0(0(1(2(5(4(x1))))))
[1] [0]
[0] [0]
[0] [0]
0(2(1(5(5(x1))))) = [1] >= [1] = 0(1(2(2(5(5(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(4(2(4(1(x1))))) = [1] >= [0] = 1(3(2(0(4(4(x1))))))
[0] [0]
[1] [0]
[0] [0]
0(4(5(4(3(x1))))) = [1] >= [0] = 2(5(0(4(4(3(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(5(1(5(1(x1))))) = [1] >= [1] = 0(5(1(1(2(5(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(5(2(1(5(x1))))) = [1] >= [0] = 1(2(5(5(0(4(x1))))))
[0] [0]
[0] [0]
[0] [0]
0(5(2(4(1(x1))))) = [1] >= [1] = 4(5(2(1(2(0(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(0(1(4(1(x1))))) = [1] >= [1] = 0(4(4(1(3(1(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(0(1(4(1(x1))))) = [1] >= [0] = 4(3(2(0(1(1(x1))))))
[0] [0]
[0] [0]
[1] [0]
3(0(3(5(5(x1))))) = [1] >= [0] = 3(3(2(5(0(5(x1))))))
[0] [0]
[0] [0]
[1] [1]
3(0(5(3(1(x1))))) = [1] >= [0] = 1(0(3(3(2(5(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(0(1(4(1(x1))))) = [0] >= [0] = 4(4(0(1(3(1(x1))))))
[1] [0]
[0] [0]
[0] [0]
4(0(1(5(1(x1))))) = [1] >= [1] = 0(1(2(5(4(1(x1))))))
[1] [0]
[0] [0]
[0] [0]
4(0(2(4(5(x1))))) = [0] >= [0] = 4(0(2(5(0(4(x1))))))
[1] [1]
[0] [0]
[0] [0]
4(1(1(5(1(x1))))) = [0] >= [0] = 1(1(2(5(4(1(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(5(1(4(1(x1))))) = [1] >= [0] = 4(4(1(2(1(5(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(5(2(3(1(x1))))) = [1] >= [0] = 4(3(1(2(2(5(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(5(4(3(1(x1))))) = [1] >= [0] = 4(1(2(5(3(4(x1))))))
[0] [0]
[0] [0]
[0] [0]
4(5(5(3(1(x1))))) = [1] >= [0] = 1(3(2(5(5(4(x1))))))
[0] [0]
problem:
DPs:
TRS:
0(1(1(x1))) -> 1(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(2(2(0(x1)))))
0(3(1(x1))) -> 3(2(1(2(0(x1)))))
0(3(1(x1))) -> 1(3(3(3(2(0(x1))))))
0(4(1(x1))) -> 2(1(2(0(4(x1)))))
0(0(4(5(x1)))) -> 0(0(2(5(4(x1)))))
0(1(4(1(x1)))) -> 0(1(2(2(4(1(x1))))))
0(1(4(5(x1)))) -> 4(0(1(2(5(4(x1))))))
0(1(5(1(x1)))) -> 1(2(2(5(0(1(x1))))))
0(1(5(3(x1)))) -> 0(5(3(2(1(x1)))))
0(2(4(1(x1)))) -> 1(3(3(2(0(4(x1))))))
0(2(4(1(x1)))) -> 4(2(1(2(0(4(x1))))))
0(2(4(5(x1)))) -> 0(2(2(5(0(4(x1))))))
0(3(1(5(x1)))) -> 0(1(2(5(3(x1)))))
0(3(1(5(x1)))) -> 1(2(5(3(0(4(x1))))))
0(3(5(1(x1)))) -> 1(2(5(3(0(x1)))))
0(3(5(1(x1)))) -> 0(5(2(1(2(3(x1))))))
0(3(5(5(x1)))) -> 0(3(2(5(5(x1)))))
0(4(0(1(x1)))) -> 2(0(4(4(0(1(x1))))))
0(4(1(5(x1)))) -> 1(2(5(0(4(x1)))))
0(4(3(5(x1)))) -> 0(4(3(2(5(4(x1))))))
0(4(5(1(x1)))) -> 2(5(4(4(0(1(x1))))))
3(0(1(5(x1)))) -> 3(1(4(0(5(4(x1))))))
3(0(3(1(x1)))) -> 1(3(3(2(0(x1)))))
3(0(3(5(x1)))) -> 3(2(5(0(2(3(x1))))))
3(3(0(1(x1)))) -> 0(1(3(2(2(3(x1))))))
3(4(5(1(x1)))) -> 3(2(5(4(2(1(x1))))))
4(1(3(5(x1)))) -> 1(2(5(3(4(4(x1))))))
4(1(5(1(x1)))) -> 4(4(5(1(2(1(x1))))))
4(4(1(5(x1)))) -> 4(1(2(5(4(x1)))))
0(1(4(5(5(x1))))) -> 0(5(1(4(2(5(x1))))))
0(2(1(4(5(x1))))) -> 0(0(1(2(5(4(x1))))))
0(2(1(5(5(x1))))) -> 0(1(2(2(5(5(x1))))))
0(4(2(4(1(x1))))) -> 1(3(2(0(4(4(x1))))))
0(4(5(4(3(x1))))) -> 2(5(0(4(4(3(x1))))))
0(5(1(5(1(x1))))) -> 0(5(1(1(2(5(x1))))))
0(5(2(1(5(x1))))) -> 1(2(5(5(0(4(x1))))))
0(5(2(4(1(x1))))) -> 4(5(2(1(2(0(x1))))))
3(0(1(4(1(x1))))) -> 0(4(4(1(3(1(x1))))))
3(0(1(4(1(x1))))) -> 4(3(2(0(1(1(x1))))))
3(0(3(5(5(x1))))) -> 3(3(2(5(0(5(x1))))))
3(0(5(3(1(x1))))) -> 1(0(3(3(2(5(x1))))))
4(0(1(4(1(x1))))) -> 4(4(0(1(3(1(x1))))))
4(0(1(5(1(x1))))) -> 0(1(2(5(4(1(x1))))))
4(0(2(4(5(x1))))) -> 4(0(2(5(0(4(x1))))))
4(1(1(5(1(x1))))) -> 1(1(2(5(4(1(x1))))))
4(5(1(4(1(x1))))) -> 4(4(1(2(1(5(x1))))))
4(5(2(3(1(x1))))) -> 4(3(1(2(2(5(x1))))))
4(5(4(3(1(x1))))) -> 4(1(2(5(3(4(x1))))))
4(5(5(3(1(x1))))) -> 1(3(2(5(5(4(x1))))))
Qed