YES Problem: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Proof: DP Processor: DPs: a13#(a13(x1)) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(x1)) a13#(a13(x1)) -> a23#(a12(a12(x1))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) a14#(a14(x1)) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(x1)) a14#(a14(x1)) -> a23#(a12(a12(x1))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15#(a15(x1)) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(x1)) a15#(a15(x1)) -> a23#(a12(a12(x1))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a15#(a15(x1)) -> a45#(a34(a34(a23(a23(a12(a12(x1))))))) a15#(a15(x1)) -> a45#(a45(a34(a34(a23(a23(a12(a12(x1)))))))) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16#(a16(x1)) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(x1)) a16#(a16(x1)) -> a23#(a12(a12(x1))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a16#(a16(x1)) -> a45#(a34(a34(a23(a23(a12(a12(x1))))))) a16#(a16(x1)) -> a45#(a45(a34(a34(a23(a23(a12(a12(x1)))))))) a16#(a16(x1)) -> a56#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) a16#(a16(x1)) -> a56#(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) a16#(a16(x1)) -> a45#(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) a16#(a16(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24#(a24(x1)) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(x1)) a24#(a24(x1)) -> a34#(a23(a23(x1))) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) a25#(a25(x1)) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(x1)) a25#(a25(x1)) -> a34#(a23(a23(x1))) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) a25#(a25(x1)) -> a45#(a34(a34(a23(a23(x1))))) a25#(a25(x1)) -> a45#(a45(a34(a34(a23(a23(x1)))))) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26#(a26(x1)) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(x1)) a26#(a26(x1)) -> a34#(a23(a23(x1))) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) a26#(a26(x1)) -> a45#(a34(a34(a23(a23(x1))))) a26#(a26(x1)) -> a45#(a45(a34(a34(a23(a23(x1)))))) a26#(a26(x1)) -> a56#(a45(a45(a34(a34(a23(a23(x1))))))) a26#(a26(x1)) -> a56#(a56(a45(a45(a34(a34(a23(a23(x1)))))))) a26#(a26(x1)) -> a45#(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))) a26#(a26(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35#(a35(x1)) -> a34#(x1) a35#(a35(x1)) -> a34#(a34(x1)) a35#(a35(x1)) -> a45#(a34(a34(x1))) a35#(a35(x1)) -> a45#(a45(a34(a34(x1)))) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) a36#(a36(x1)) -> a34#(x1) a36#(a36(x1)) -> a34#(a34(x1)) a36#(a36(x1)) -> a45#(a34(a34(x1))) a36#(a36(x1)) -> a45#(a45(a34(a34(x1)))) a36#(a36(x1)) -> a56#(a45(a45(a34(a34(x1))))) a36#(a36(x1)) -> a56#(a56(a45(a45(a34(a34(x1)))))) a36#(a36(x1)) -> a45#(a56(a56(a45(a45(a34(a34(x1))))))) a36#(a36(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(x1)))))))) a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46#(a46(x1)) -> a45#(x1) a46#(a46(x1)) -> a45#(a45(x1)) a46#(a46(x1)) -> a56#(a45(a45(x1))) a46#(a46(x1)) -> a56#(a56(a45(a45(x1)))) a46#(a46(x1)) -> a45#(a56(a56(a45(a45(x1))))) a46#(a46(x1)) -> a45#(a45(a56(a56(a45(a45(x1)))))) a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a34#(a34(a56(a56(x1)))) -> a34#(x1) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) TDG Processor: DPs: a13#(a13(x1)) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(x1)) a13#(a13(x1)) -> a23#(a12(a12(x1))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) a14#(a14(x1)) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(x1)) a14#(a14(x1)) -> a23#(a12(a12(x1))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15#(a15(x1)) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(x1)) a15#(a15(x1)) -> a23#(a12(a12(x1))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a15#(a15(x1)) -> a45#(a34(a34(a23(a23(a12(a12(x1))))))) a15#(a15(x1)) -> a45#(a45(a34(a34(a23(a23(a12(a12(x1)))))))) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16#(a16(x1)) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(x1)) a16#(a16(x1)) -> a23#(a12(a12(x1))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) a16#(a16(x1)) -> a45#(a34(a34(a23(a23(a12(a12(x1))))))) a16#(a16(x1)) -> a45#(a45(a34(a34(a23(a23(a12(a12(x1)))))))) a16#(a16(x1)) -> a56#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) a16#(a16(x1)) -> a56#(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) a16#(a16(x1)) -> a45#(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) a16#(a16(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24#(a24(x1)) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(x1)) a24#(a24(x1)) -> a34#(a23(a23(x1))) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) a25#(a25(x1)) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(x1)) a25#(a25(x1)) -> a34#(a23(a23(x1))) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) a25#(a25(x1)) -> a45#(a34(a34(a23(a23(x1))))) a25#(a25(x1)) -> a45#(a45(a34(a34(a23(a23(x1)))))) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26#(a26(x1)) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(x1)) a26#(a26(x1)) -> a34#(a23(a23(x1))) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) a26#(a26(x1)) -> a45#(a34(a34(a23(a23(x1))))) a26#(a26(x1)) -> a45#(a45(a34(a34(a23(a23(x1)))))) a26#(a26(x1)) -> a56#(a45(a45(a34(a34(a23(a23(x1))))))) a26#(a26(x1)) -> a56#(a56(a45(a45(a34(a34(a23(a23(x1)))))))) a26#(a26(x1)) -> a45#(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))) a26#(a26(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35#(a35(x1)) -> a34#(x1) a35#(a35(x1)) -> a34#(a34(x1)) a35#(a35(x1)) -> a45#(a34(a34(x1))) a35#(a35(x1)) -> a45#(a45(a34(a34(x1)))) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) a36#(a36(x1)) -> a34#(x1) a36#(a36(x1)) -> a34#(a34(x1)) a36#(a36(x1)) -> a45#(a34(a34(x1))) a36#(a36(x1)) -> a45#(a45(a34(a34(x1)))) a36#(a36(x1)) -> a56#(a45(a45(a34(a34(x1))))) a36#(a36(x1)) -> a56#(a56(a45(a45(a34(a34(x1)))))) a36#(a36(x1)) -> a45#(a56(a56(a45(a45(a34(a34(x1))))))) a36#(a36(x1)) -> a45#(a45(a56(a56(a45(a45(a34(a34(x1)))))))) a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46#(a46(x1)) -> a45#(x1) a46#(a46(x1)) -> a45#(a45(x1)) a46#(a46(x1)) -> a56#(a45(a45(x1))) a46#(a46(x1)) -> a56#(a56(a45(a45(x1)))) a46#(a46(x1)) -> a45#(a56(a56(a45(a45(x1))))) a46#(a46(x1)) -> a45#(a45(a56(a56(a45(a45(x1)))))) a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a34#(a34(a56(a56(x1)))) -> a34#(x1) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) graph: a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a36#(a36(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a36#(a36(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a36#(a36(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a36#(a36(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a36#(a36(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a36#(a36(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a36#(a36(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a36#(a36(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a36#(a36(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a36#(a36(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a35#(a35(x1)) -> a34#(a45(a45(a34(a34(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a35#(a35(x1)) -> a34#(a34(a45(a45(a34(a34(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a35#(a35(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a35#(a35(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a35#(a35(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a35#(a35(x1)) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a35#(a35(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a35#(a35(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a35#(a35(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a35#(a35(x1)) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a34#(a34(a56(a56(x1)))) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a34#(a34(a56(a56(x1)))) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a34#(a34(a56(a56(x1)))) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a34#(a34(a56(a56(x1)))) -> a34#(x1) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a26#(a26(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a26#(a26(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a26#(a26(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a26#(a26(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a26#(a26(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a26#(a26(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a26#(a26(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a26#(a26(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a25#(a25(x1)) -> a34#(a45(a45(a34(a34(a23(a23(x1))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a25#(a25(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(x1)))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a25#(a25(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a25#(a25(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a25#(a25(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a25#(a25(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a25#(a25(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a25#(a25(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a24#(a24(x1)) -> a34#(a34(a23(a23(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a24#(a24(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a24#(a24(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a24#(a24(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a24#(a24(x1)) -> a34#(a23(a23(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a34(a34(a23(a23(x1))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a23(a34(a34(a23(a23(x1)))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a24#(a24(x1)) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a45(a45(x1)))) -> a23#(x1) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a16#(a16(x1)) -> a34#(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a16#(a16(x1)) -> a34#(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a16#(a16(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a16#(a16(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a16#(a16(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a16#(a16(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a15#(a15(x1)) -> a34#(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a15#(a15(x1)) -> a34#(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a15#(a15(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a15#(a15(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a15#(a15(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a15#(a15(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a14#(a14(x1)) -> a34#(a34(a23(a23(a12(a12(x1)))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a14#(a14(x1)) -> a34#(a23(a23(a12(a12(x1))))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a34(a34(a23(a23(a12(a12(x1))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a23(a34(a34(a23(a23(a12(a12(x1)))))))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a14#(a14(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a14#(a14(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a13#(a13(x1)) -> a23#(a23(a12(a12(x1)))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a56(a23(a23(x1)))) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a56#(a23(a23(x1))) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a56(a56(x1)))) -> a23#(x1) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a45(a23(a23(x1)))) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a45#(a23(a23(x1))) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a13#(a13(x1)) -> a23#(a12(a12(x1))) -> a23#(a23(a45(a45(x1)))) -> a23#(x1) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a23(a23(a12(a12(x1))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(a23(a23(a12(a12(x1)))))) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a13#(a13(x1)) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a56(a34(a34(x1)))) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) -> a34#(a34(a56(a56(x1)))) -> a56#(a34(a34(x1))) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) -> a34#(a34(a56(a56(x1)))) -> a34#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a56(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a56#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a45(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a45#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a34(a12(a12(x1)))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a34#(a12(a12(x1))) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a34(a34(x1)))) -> a12#(x1) -> a12#(a12(a34(a34(x1)))) -> a12#(x1) SCC Processor: #sccs: 3 #rules: 12 #arcs: 632/15376 DPs: a12#(a12(a34(a34(x1)))) -> a12#(x1) a12#(a12(a34(a34(x1)))) -> a12#(a12(x1)) a12#(a12(a45(a45(x1)))) -> a12#(x1) a12#(a12(a45(a45(x1)))) -> a12#(a12(x1)) a12#(a12(a56(a56(x1)))) -> a12#(x1) a12#(a12(a56(a56(x1)))) -> a12#(a12(x1)) TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Matrix Interpretation Processor: dim=1 interpretation: [a12#](x0) = x0, [a56](x0) = x0 + 2, [a46](x0) = x0 + 10, [a45](x0) = x0 + 1, [a36](x0) = x0 + 6, [a35](x0) = x0 + 3, [a34](x0) = x0 + 1, [a26](x0) = 2x0 + 4, [a25](x0) = x0 + 4, [a24](x0) = 2x0 + 1, [a23](x0) = x0, [a16](x0) = x0 + 8, [a15](x0) = x0 + 3, [a14](x0) = 2x0 + 4, [a13](x0) = x0, [a12](x0) = x0 orientation: a12#(a12(a34(a34(x1)))) = x1 + 2 >= x1 = a12#(x1) a12#(a12(a34(a34(x1)))) = x1 + 2 >= x1 = a12#(a12(x1)) a12#(a12(a45(a45(x1)))) = x1 + 2 >= x1 = a12#(x1) a12#(a12(a45(a45(x1)))) = x1 + 2 >= x1 = a12#(a12(x1)) a12#(a12(a56(a56(x1)))) = x1 + 4 >= x1 = a12#(x1) a12#(a12(a56(a56(x1)))) = x1 + 4 >= x1 = a12#(a12(x1)) a12(a12(a12(a12(x1)))) = x1 >= x1 = x1 a13(a13(a13(a13(x1)))) = x1 >= x1 = x1 a14(a14(a14(a14(x1)))) = 16x1 + 60 >= x1 = x1 a15(a15(a15(a15(x1)))) = x1 + 12 >= x1 = x1 a16(a16(a16(a16(x1)))) = x1 + 32 >= x1 = x1 a23(a23(a23(a23(x1)))) = x1 >= x1 = x1 a24(a24(a24(a24(x1)))) = 16x1 + 15 >= x1 = x1 a25(a25(a25(a25(x1)))) = x1 + 16 >= x1 = x1 a26(a26(a26(a26(x1)))) = 16x1 + 60 >= x1 = x1 a34(a34(a34(a34(x1)))) = x1 + 4 >= x1 = x1 a35(a35(a35(a35(x1)))) = x1 + 12 >= x1 = x1 a36(a36(a36(a36(x1)))) = x1 + 24 >= x1 = x1 a45(a45(a45(a45(x1)))) = x1 + 4 >= x1 = x1 a46(a46(a46(a46(x1)))) = x1 + 40 >= x1 = x1 a56(a56(a56(a56(x1)))) = x1 + 8 >= x1 = x1 a13(a13(x1)) = x1 >= x1 = a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) = 4x1 + 12 >= x1 + 2 = a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) = x1 + 6 >= x1 + 6 = a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) = x1 + 16 >= x1 + 12 = a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) = 4x1 + 3 >= x1 + 2 = a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) = x1 + 8 >= x1 + 6 = a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) = 4x1 + 12 >= x1 + 12 = a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) = x1 + 6 >= x1 + 6 = a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) = x1 + 12 >= x1 + 12 = a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) = x1 + 20 >= x1 + 8 = a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) = x1 >= x1 = x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) = x1 + 6 >= x1 = x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) = x1 + 12 >= x1 = x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) = x1 + 18 >= x1 = x1 a12(a12(a34(a34(x1)))) = x1 + 2 >= x1 + 2 = a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) = x1 + 2 >= x1 + 2 = a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) = x1 + 4 >= x1 + 4 = a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) = x1 + 2 >= x1 + 2 = a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) = x1 + 4 >= x1 + 4 = a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) = x1 + 6 >= x1 + 6 = a56(a56(a34(a34(x1)))) problem: DPs: TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Qed DPs: a23#(a23(a45(a45(x1)))) -> a23#(x1) a23#(a23(a45(a45(x1)))) -> a23#(a23(x1)) a23#(a23(a56(a56(x1)))) -> a23#(x1) a23#(a23(a56(a56(x1)))) -> a23#(a23(x1)) TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Matrix Interpretation Processor: dim=1 interpretation: [a23#](x0) = 4x0, [a56](x0) = x0 + 1, [a46](x0) = x0 + 8, [a45](x0) = x0 + 2, [a36](x0) = x0 + 11, [a35](x0) = 2x0 + 4, [a34](x0) = x0, [a26](x0) = x0 + 8, [a25](x0) = x0 + 8, [a24](x0) = x0, [a23](x0) = x0, [a16](x0) = x0 + 8, [a15](x0) = 2x0 + 2, [a14](x0) = x0, [a13](x0) = x0, [a12](x0) = x0 orientation: a23#(a23(a45(a45(x1)))) = 4x1 + 16 >= 4x1 = a23#(x1) a23#(a23(a45(a45(x1)))) = 4x1 + 16 >= 4x1 = a23#(a23(x1)) a23#(a23(a56(a56(x1)))) = 4x1 + 8 >= 4x1 = a23#(x1) a23#(a23(a56(a56(x1)))) = 4x1 + 8 >= 4x1 = a23#(a23(x1)) a12(a12(a12(a12(x1)))) = x1 >= x1 = x1 a13(a13(a13(a13(x1)))) = x1 >= x1 = x1 a14(a14(a14(a14(x1)))) = x1 >= x1 = x1 a15(a15(a15(a15(x1)))) = 16x1 + 30 >= x1 = x1 a16(a16(a16(a16(x1)))) = x1 + 32 >= x1 = x1 a23(a23(a23(a23(x1)))) = x1 >= x1 = x1 a24(a24(a24(a24(x1)))) = x1 >= x1 = x1 a25(a25(a25(a25(x1)))) = x1 + 32 >= x1 = x1 a26(a26(a26(a26(x1)))) = x1 + 32 >= x1 = x1 a34(a34(a34(a34(x1)))) = x1 >= x1 = x1 a35(a35(a35(a35(x1)))) = 16x1 + 60 >= x1 = x1 a36(a36(a36(a36(x1)))) = x1 + 44 >= x1 = x1 a45(a45(a45(a45(x1)))) = x1 + 8 >= x1 = x1 a46(a46(a46(a46(x1)))) = x1 + 32 >= x1 = x1 a56(a56(a56(a56(x1)))) = x1 + 4 >= x1 = x1 a13(a13(x1)) = x1 >= x1 = a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) = x1 >= x1 = a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) = 4x1 + 6 >= x1 + 4 = a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) = x1 + 16 >= x1 + 10 = a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) = x1 >= x1 = a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) = x1 + 16 >= x1 + 4 = a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) = x1 + 16 >= x1 + 10 = a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) = 4x1 + 12 >= x1 + 4 = a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) = x1 + 22 >= x1 + 10 = a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) = x1 + 16 >= x1 + 10 = a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) = x1 >= x1 = x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) = x1 >= x1 = x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) = x1 + 12 >= x1 = x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) = x1 + 18 >= x1 = x1 a12(a12(a34(a34(x1)))) = x1 >= x1 = a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) = x1 + 4 >= x1 + 4 = a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) = x1 + 2 >= x1 + 2 = a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) = x1 + 4 >= x1 + 4 = a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) = x1 + 2 >= x1 + 2 = a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) = x1 + 2 >= x1 + 2 = a56(a56(a34(a34(x1)))) problem: DPs: TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Qed DPs: a34#(a34(a56(a56(x1)))) -> a34#(x1) a34#(a34(a56(a56(x1)))) -> a34#(a34(x1)) TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) KBO Processor: argument filtering: pi(a12) = 0 pi(a13) = 0 pi(a14) = 0 pi(a15) = 0 pi(a16) = [0] pi(a23) = 0 pi(a24) = 0 pi(a25) = [0] pi(a26) = [0] pi(a34) = 0 pi(a35) = 0 pi(a36) = [0] pi(a45) = 0 pi(a46) = [0] pi(a56) = [0] pi(a34#) = 0 weight function: w0 = 1 w(a34#) = w(a56) = w(a46) = w(a45) = w(a36) = w(a26) = w(a25) = w( a16) = w(a13) = 1 w(a35) = w(a34) = w(a24) = w(a23) = w(a15) = w(a14) = w(a12) = 0 precedence: a26 ~ a25 ~ a14 > a36 > a46 > a16 > a34# ~ a56 ~ a45 ~ a35 ~ a34 ~ a24 ~ a23 ~ a15 ~ a13 ~ a12 problem: DPs: TRS: a12(a12(a12(a12(x1)))) -> x1 a13(a13(a13(a13(x1)))) -> x1 a14(a14(a14(a14(x1)))) -> x1 a15(a15(a15(a15(x1)))) -> x1 a16(a16(a16(a16(x1)))) -> x1 a23(a23(a23(a23(x1)))) -> x1 a24(a24(a24(a24(x1)))) -> x1 a25(a25(a25(a25(x1)))) -> x1 a26(a26(a26(a26(x1)))) -> x1 a34(a34(a34(a34(x1)))) -> x1 a35(a35(a35(a35(x1)))) -> x1 a36(a36(a36(a36(x1)))) -> x1 a45(a45(a45(a45(x1)))) -> x1 a46(a46(a46(a46(x1)))) -> x1 a56(a56(a56(a56(x1)))) -> x1 a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) a14(a14(x1)) -> a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) a15(a15(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) a16(a16(x1)) -> a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) a25(a25(x1)) -> a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) a26(a26(x1)) -> a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) a36(a36(x1)) -> a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> x1 a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> x1 a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> x1 a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> x1 a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) Qed