NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Mixed_SRS/s6-split.srs

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 NonTerminationProof (⇒, 1183 ms)
↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Begin(a12(x)) → Wait(Right1(x))
Begin(a13(x)) → Wait(Right2(x))
Begin(a14(x)) → Wait(Right3(x))
Begin(a15(x)) → Wait(Right4(x))
Begin(a16(x)) → Wait(Right5(x))
Begin(a23(x)) → Wait(Right6(x))
Begin(a24(x)) → Wait(Right7(x))
Begin(a25(x)) → Wait(Right8(x))
Begin(a26(x)) → Wait(Right9(x))
Begin(a34(x)) → Wait(Right10(x))
Begin(a35(x)) → Wait(Right11(x))
Begin(a36(x)) → Wait(Right12(x))
Begin(a45(x)) → Wait(Right13(x))
Begin(a46(x)) → Wait(Right14(x))
Begin(a56(x)) → Wait(Right15(x))
Begin(a23(a12(a23(a12(a23(x)))))) → Wait(Right16(x))
Begin(a12(a23(a12(a23(x))))) → Wait(Right17(x))
Begin(a23(a12(a23(x)))) → Wait(Right18(x))
Begin(a12(a23(x))) → Wait(Right19(x))
Begin(a23(x)) → Wait(Right20(x))
Begin(a34(a23(a34(a23(a34(x)))))) → Wait(Right21(x))
Begin(a23(a34(a23(a34(x))))) → Wait(Right22(x))
Begin(a34(a23(a34(x)))) → Wait(Right23(x))
Begin(a23(a34(x))) → Wait(Right24(x))
Begin(a34(x)) → Wait(Right25(x))
Begin(a45(a34(a45(a34(a45(x)))))) → Wait(Right26(x))
Begin(a34(a45(a34(a45(x))))) → Wait(Right27(x))
Begin(a45(a34(a45(x)))) → Wait(Right28(x))
Begin(a34(a45(x))) → Wait(Right29(x))
Begin(a45(x)) → Wait(Right30(x))
Begin(a56(a45(a56(a45(a56(x)))))) → Wait(Right31(x))
Begin(a45(a56(a45(a56(x))))) → Wait(Right32(x))
Begin(a56(a45(a56(x)))) → Wait(Right33(x))
Begin(a45(a56(x))) → Wait(Right34(x))
Begin(a56(x)) → Wait(Right35(x))
Begin(a34(x)) → Wait(Right36(x))
Begin(a45(x)) → Wait(Right37(x))
Begin(a56(x)) → Wait(Right38(x))
Begin(a45(x)) → Wait(Right39(x))
Begin(a56(x)) → Wait(Right40(x))
Begin(a56(x)) → Wait(Right41(x))
Right1(a12(End(x))) → Left(End(x))
Right2(a13(End(x))) → Left(End(x))
Right3(a14(End(x))) → Left(End(x))
Right4(a15(End(x))) → Left(End(x))
Right5(a16(End(x))) → Left(End(x))
Right6(a23(End(x))) → Left(End(x))
Right7(a24(End(x))) → Left(End(x))
Right8(a25(End(x))) → Left(End(x))
Right9(a26(End(x))) → Left(End(x))
Right10(a34(End(x))) → Left(End(x))
Right11(a35(End(x))) → Left(End(x))
Right12(a36(End(x))) → Left(End(x))
Right13(a45(End(x))) → Left(End(x))
Right14(a46(End(x))) → Left(End(x))
Right15(a56(End(x))) → Left(End(x))
Right16(a12(End(x))) → Left(End(x))
Right17(a12(a23(End(x)))) → Left(End(x))
Right18(a12(a23(a12(End(x))))) → Left(End(x))
Right19(a12(a23(a12(a23(End(x)))))) → Left(End(x))
Right20(a12(a23(a12(a23(a12(End(x))))))) → Left(End(x))
Right21(a23(End(x))) → Left(End(x))
Right22(a23(a34(End(x)))) → Left(End(x))
Right23(a23(a34(a23(End(x))))) → Left(End(x))
Right24(a23(a34(a23(a34(End(x)))))) → Left(End(x))
Right25(a23(a34(a23(a34(a23(End(x))))))) → Left(End(x))
Right26(a34(End(x))) → Left(End(x))
Right27(a34(a45(End(x)))) → Left(End(x))
Right28(a34(a45(a34(End(x))))) → Left(End(x))
Right29(a34(a45(a34(a45(End(x)))))) → Left(End(x))
Right30(a34(a45(a34(a45(a34(End(x))))))) → Left(End(x))
Right31(a45(End(x))) → Left(End(x))
Right32(a45(a56(End(x)))) → Left(End(x))
Right33(a45(a56(a45(End(x))))) → Left(End(x))
Right34(a45(a56(a45(a56(End(x)))))) → Left(End(x))
Right35(a45(a56(a45(a56(a45(End(x))))))) → Left(End(x))
Right36(a12(End(x))) → Left(a34(a12(End(x))))
Right37(a12(End(x))) → Left(a45(a12(End(x))))
Right38(a12(End(x))) → Left(a56(a12(End(x))))
Right39(a23(End(x))) → Left(a45(a23(End(x))))
Right40(a23(End(x))) → Left(a56(a23(End(x))))
Right41(a34(End(x))) → Left(a56(a34(End(x))))
Right1(a12(x)) → Aa12(Right1(x))
Right2(a12(x)) → Aa12(Right2(x))
Right3(a12(x)) → Aa12(Right3(x))
Right4(a12(x)) → Aa12(Right4(x))
Right5(a12(x)) → Aa12(Right5(x))
Right6(a12(x)) → Aa12(Right6(x))
Right7(a12(x)) → Aa12(Right7(x))
Right8(a12(x)) → Aa12(Right8(x))
Right9(a12(x)) → Aa12(Right9(x))
Right10(a12(x)) → Aa12(Right10(x))
Right11(a12(x)) → Aa12(Right11(x))
Right12(a12(x)) → Aa12(Right12(x))
Right13(a12(x)) → Aa12(Right13(x))
Right14(a12(x)) → Aa12(Right14(x))
Right15(a12(x)) → Aa12(Right15(x))
Right16(a12(x)) → Aa12(Right16(x))
Right17(a12(x)) → Aa12(Right17(x))
Right18(a12(x)) → Aa12(Right18(x))
Right19(a12(x)) → Aa12(Right19(x))
Right20(a12(x)) → Aa12(Right20(x))
Right21(a12(x)) → Aa12(Right21(x))
Right22(a12(x)) → Aa12(Right22(x))
Right23(a12(x)) → Aa12(Right23(x))
Right24(a12(x)) → Aa12(Right24(x))
Right25(a12(x)) → Aa12(Right25(x))
Right26(a12(x)) → Aa12(Right26(x))
Right27(a12(x)) → Aa12(Right27(x))
Right28(a12(x)) → Aa12(Right28(x))
Right29(a12(x)) → Aa12(Right29(x))
Right30(a12(x)) → Aa12(Right30(x))
Right31(a12(x)) → Aa12(Right31(x))
Right32(a12(x)) → Aa12(Right32(x))
Right33(a12(x)) → Aa12(Right33(x))
Right34(a12(x)) → Aa12(Right34(x))
Right35(a12(x)) → Aa12(Right35(x))
Right36(a12(x)) → Aa12(Right36(x))
Right37(a12(x)) → Aa12(Right37(x))
Right38(a12(x)) → Aa12(Right38(x))
Right39(a12(x)) → Aa12(Right39(x))
Right40(a12(x)) → Aa12(Right40(x))
Right41(a12(x)) → Aa12(Right41(x))
Right1(a13(x)) → Aa13(Right1(x))
Right2(a13(x)) → Aa13(Right2(x))
Right3(a13(x)) → Aa13(Right3(x))
Right4(a13(x)) → Aa13(Right4(x))
Right5(a13(x)) → Aa13(Right5(x))
Right6(a13(x)) → Aa13(Right6(x))
Right7(a13(x)) → Aa13(Right7(x))
Right8(a13(x)) → Aa13(Right8(x))
Right9(a13(x)) → Aa13(Right9(x))
Right10(a13(x)) → Aa13(Right10(x))
Right11(a13(x)) → Aa13(Right11(x))
Right12(a13(x)) → Aa13(Right12(x))
Right13(a13(x)) → Aa13(Right13(x))
Right14(a13(x)) → Aa13(Right14(x))
Right15(a13(x)) → Aa13(Right15(x))
Right16(a13(x)) → Aa13(Right16(x))
Right17(a13(x)) → Aa13(Right17(x))
Right18(a13(x)) → Aa13(Right18(x))
Right19(a13(x)) → Aa13(Right19(x))
Right20(a13(x)) → Aa13(Right20(x))
Right21(a13(x)) → Aa13(Right21(x))
Right22(a13(x)) → Aa13(Right22(x))
Right23(a13(x)) → Aa13(Right23(x))
Right24(a13(x)) → Aa13(Right24(x))
Right25(a13(x)) → Aa13(Right25(x))
Right26(a13(x)) → Aa13(Right26(x))
Right27(a13(x)) → Aa13(Right27(x))
Right28(a13(x)) → Aa13(Right28(x))
Right29(a13(x)) → Aa13(Right29(x))
Right30(a13(x)) → Aa13(Right30(x))
Right31(a13(x)) → Aa13(Right31(x))
Right32(a13(x)) → Aa13(Right32(x))
Right33(a13(x)) → Aa13(Right33(x))
Right34(a13(x)) → Aa13(Right34(x))
Right35(a13(x)) → Aa13(Right35(x))
Right36(a13(x)) → Aa13(Right36(x))
Right37(a13(x)) → Aa13(Right37(x))
Right38(a13(x)) → Aa13(Right38(x))
Right39(a13(x)) → Aa13(Right39(x))
Right40(a13(x)) → Aa13(Right40(x))
Right41(a13(x)) → Aa13(Right41(x))
Right1(a14(x)) → Aa14(Right1(x))
Right2(a14(x)) → Aa14(Right2(x))
Right3(a14(x)) → Aa14(Right3(x))
Right4(a14(x)) → Aa14(Right4(x))
Right5(a14(x)) → Aa14(Right5(x))
Right6(a14(x)) → Aa14(Right6(x))
Right7(a14(x)) → Aa14(Right7(x))
Right8(a14(x)) → Aa14(Right8(x))
Right9(a14(x)) → Aa14(Right9(x))
Right10(a14(x)) → Aa14(Right10(x))
Right11(a14(x)) → Aa14(Right11(x))
Right12(a14(x)) → Aa14(Right12(x))
Right13(a14(x)) → Aa14(Right13(x))
Right14(a14(x)) → Aa14(Right14(x))
Right15(a14(x)) → Aa14(Right15(x))
Right16(a14(x)) → Aa14(Right16(x))
Right17(a14(x)) → Aa14(Right17(x))
Right18(a14(x)) → Aa14(Right18(x))
Right19(a14(x)) → Aa14(Right19(x))
Right20(a14(x)) → Aa14(Right20(x))
Right21(a14(x)) → Aa14(Right21(x))
Right22(a14(x)) → Aa14(Right22(x))
Right23(a14(x)) → Aa14(Right23(x))
Right24(a14(x)) → Aa14(Right24(x))
Right25(a14(x)) → Aa14(Right25(x))
Right26(a14(x)) → Aa14(Right26(x))
Right27(a14(x)) → Aa14(Right27(x))
Right28(a14(x)) → Aa14(Right28(x))
Right29(a14(x)) → Aa14(Right29(x))
Right30(a14(x)) → Aa14(Right30(x))
Right31(a14(x)) → Aa14(Right31(x))
Right32(a14(x)) → Aa14(Right32(x))
Right33(a14(x)) → Aa14(Right33(x))
Right34(a14(x)) → Aa14(Right34(x))
Right35(a14(x)) → Aa14(Right35(x))
Right36(a14(x)) → Aa14(Right36(x))
Right37(a14(x)) → Aa14(Right37(x))
Right38(a14(x)) → Aa14(Right38(x))
Right39(a14(x)) → Aa14(Right39(x))
Right40(a14(x)) → Aa14(Right40(x))
Right41(a14(x)) → Aa14(Right41(x))
Right1(a15(x)) → Aa15(Right1(x))
Right2(a15(x)) → Aa15(Right2(x))
Right3(a15(x)) → Aa15(Right3(x))
Right4(a15(x)) → Aa15(Right4(x))
Right5(a15(x)) → Aa15(Right5(x))
Right6(a15(x)) → Aa15(Right6(x))
Right7(a15(x)) → Aa15(Right7(x))
Right8(a15(x)) → Aa15(Right8(x))
Right9(a15(x)) → Aa15(Right9(x))
Right10(a15(x)) → Aa15(Right10(x))
Right11(a15(x)) → Aa15(Right11(x))
Right12(a15(x)) → Aa15(Right12(x))
Right13(a15(x)) → Aa15(Right13(x))
Right14(a15(x)) → Aa15(Right14(x))
Right15(a15(x)) → Aa15(Right15(x))
Right16(a15(x)) → Aa15(Right16(x))
Right17(a15(x)) → Aa15(Right17(x))
Right18(a15(x)) → Aa15(Right18(x))
Right19(a15(x)) → Aa15(Right19(x))
Right20(a15(x)) → Aa15(Right20(x))
Right21(a15(x)) → Aa15(Right21(x))
Right22(a15(x)) → Aa15(Right22(x))
Right23(a15(x)) → Aa15(Right23(x))
Right24(a15(x)) → Aa15(Right24(x))
Right25(a15(x)) → Aa15(Right25(x))
Right26(a15(x)) → Aa15(Right26(x))
Right27(a15(x)) → Aa15(Right27(x))
Right28(a15(x)) → Aa15(Right28(x))
Right29(a15(x)) → Aa15(Right29(x))
Right30(a15(x)) → Aa15(Right30(x))
Right31(a15(x)) → Aa15(Right31(x))
Right32(a15(x)) → Aa15(Right32(x))
Right33(a15(x)) → Aa15(Right33(x))
Right34(a15(x)) → Aa15(Right34(x))
Right35(a15(x)) → Aa15(Right35(x))
Right36(a15(x)) → Aa15(Right36(x))
Right37(a15(x)) → Aa15(Right37(x))
Right38(a15(x)) → Aa15(Right38(x))
Right39(a15(x)) → Aa15(Right39(x))
Right40(a15(x)) → Aa15(Right40(x))
Right41(a15(x)) → Aa15(Right41(x))
Right1(a16(x)) → Aa16(Right1(x))
Right2(a16(x)) → Aa16(Right2(x))
Right3(a16(x)) → Aa16(Right3(x))
Right4(a16(x)) → Aa16(Right4(x))
Right5(a16(x)) → Aa16(Right5(x))
Right6(a16(x)) → Aa16(Right6(x))
Right7(a16(x)) → Aa16(Right7(x))
Right8(a16(x)) → Aa16(Right8(x))
Right9(a16(x)) → Aa16(Right9(x))
Right10(a16(x)) → Aa16(Right10(x))
Right11(a16(x)) → Aa16(Right11(x))
Right12(a16(x)) → Aa16(Right12(x))
Right13(a16(x)) → Aa16(Right13(x))
Right14(a16(x)) → Aa16(Right14(x))
Right15(a16(x)) → Aa16(Right15(x))
Right16(a16(x)) → Aa16(Right16(x))
Right17(a16(x)) → Aa16(Right17(x))
Right18(a16(x)) → Aa16(Right18(x))
Right19(a16(x)) → Aa16(Right19(x))
Right20(a16(x)) → Aa16(Right20(x))
Right21(a16(x)) → Aa16(Right21(x))
Right22(a16(x)) → Aa16(Right22(x))
Right23(a16(x)) → Aa16(Right23(x))
Right24(a16(x)) → Aa16(Right24(x))
Right25(a16(x)) → Aa16(Right25(x))
Right26(a16(x)) → Aa16(Right26(x))
Right27(a16(x)) → Aa16(Right27(x))
Right28(a16(x)) → Aa16(Right28(x))
Right29(a16(x)) → Aa16(Right29(x))
Right30(a16(x)) → Aa16(Right30(x))
Right31(a16(x)) → Aa16(Right31(x))
Right32(a16(x)) → Aa16(Right32(x))
Right33(a16(x)) → Aa16(Right33(x))
Right34(a16(x)) → Aa16(Right34(x))
Right35(a16(x)) → Aa16(Right35(x))
Right36(a16(x)) → Aa16(Right36(x))
Right37(a16(x)) → Aa16(Right37(x))
Right38(a16(x)) → Aa16(Right38(x))
Right39(a16(x)) → Aa16(Right39(x))
Right40(a16(x)) → Aa16(Right40(x))
Right41(a16(x)) → Aa16(Right41(x))
Right1(a23(x)) → Aa23(Right1(x))
Right2(a23(x)) → Aa23(Right2(x))
Right3(a23(x)) → Aa23(Right3(x))
Right4(a23(x)) → Aa23(Right4(x))
Right5(a23(x)) → Aa23(Right5(x))
Right6(a23(x)) → Aa23(Right6(x))
Right7(a23(x)) → Aa23(Right7(x))
Right8(a23(x)) → Aa23(Right8(x))
Right9(a23(x)) → Aa23(Right9(x))
Right10(a23(x)) → Aa23(Right10(x))
Right11(a23(x)) → Aa23(Right11(x))
Right12(a23(x)) → Aa23(Right12(x))
Right13(a23(x)) → Aa23(Right13(x))
Right14(a23(x)) → Aa23(Right14(x))
Right15(a23(x)) → Aa23(Right15(x))
Right16(a23(x)) → Aa23(Right16(x))
Right17(a23(x)) → Aa23(Right17(x))
Right18(a23(x)) → Aa23(Right18(x))
Right19(a23(x)) → Aa23(Right19(x))
Right20(a23(x)) → Aa23(Right20(x))
Right21(a23(x)) → Aa23(Right21(x))
Right22(a23(x)) → Aa23(Right22(x))
Right23(a23(x)) → Aa23(Right23(x))
Right24(a23(x)) → Aa23(Right24(x))
Right25(a23(x)) → Aa23(Right25(x))
Right26(a23(x)) → Aa23(Right26(x))
Right27(a23(x)) → Aa23(Right27(x))
Right28(a23(x)) → Aa23(Right28(x))
Right29(a23(x)) → Aa23(Right29(x))
Right30(a23(x)) → Aa23(Right30(x))
Right31(a23(x)) → Aa23(Right31(x))
Right32(a23(x)) → Aa23(Right32(x))
Right33(a23(x)) → Aa23(Right33(x))
Right34(a23(x)) → Aa23(Right34(x))
Right35(a23(x)) → Aa23(Right35(x))
Right36(a23(x)) → Aa23(Right36(x))
Right37(a23(x)) → Aa23(Right37(x))
Right38(a23(x)) → Aa23(Right38(x))
Right39(a23(x)) → Aa23(Right39(x))
Right40(a23(x)) → Aa23(Right40(x))
Right41(a23(x)) → Aa23(Right41(x))
Right1(a24(x)) → Aa24(Right1(x))
Right2(a24(x)) → Aa24(Right2(x))
Right3(a24(x)) → Aa24(Right3(x))
Right4(a24(x)) → Aa24(Right4(x))
Right5(a24(x)) → Aa24(Right5(x))
Right6(a24(x)) → Aa24(Right6(x))
Right7(a24(x)) → Aa24(Right7(x))
Right8(a24(x)) → Aa24(Right8(x))
Right9(a24(x)) → Aa24(Right9(x))
Right10(a24(x)) → Aa24(Right10(x))
Right11(a24(x)) → Aa24(Right11(x))
Right12(a24(x)) → Aa24(Right12(x))
Right13(a24(x)) → Aa24(Right13(x))
Right14(a24(x)) → Aa24(Right14(x))
Right15(a24(x)) → Aa24(Right15(x))
Right16(a24(x)) → Aa24(Right16(x))
Right17(a24(x)) → Aa24(Right17(x))
Right18(a24(x)) → Aa24(Right18(x))
Right19(a24(x)) → Aa24(Right19(x))
Right20(a24(x)) → Aa24(Right20(x))
Right21(a24(x)) → Aa24(Right21(x))
Right22(a24(x)) → Aa24(Right22(x))
Right23(a24(x)) → Aa24(Right23(x))
Right24(a24(x)) → Aa24(Right24(x))
Right25(a24(x)) → Aa24(Right25(x))
Right26(a24(x)) → Aa24(Right26(x))
Right27(a24(x)) → Aa24(Right27(x))
Right28(a24(x)) → Aa24(Right28(x))
Right29(a24(x)) → Aa24(Right29(x))
Right30(a24(x)) → Aa24(Right30(x))
Right31(a24(x)) → Aa24(Right31(x))
Right32(a24(x)) → Aa24(Right32(x))
Right33(a24(x)) → Aa24(Right33(x))
Right34(a24(x)) → Aa24(Right34(x))
Right35(a24(x)) → Aa24(Right35(x))
Right36(a24(x)) → Aa24(Right36(x))
Right37(a24(x)) → Aa24(Right37(x))
Right38(a24(x)) → Aa24(Right38(x))
Right39(a24(x)) → Aa24(Right39(x))
Right40(a24(x)) → Aa24(Right40(x))
Right41(a24(x)) → Aa24(Right41(x))
Right1(a25(x)) → Aa25(Right1(x))
Right2(a25(x)) → Aa25(Right2(x))
Right3(a25(x)) → Aa25(Right3(x))
Right4(a25(x)) → Aa25(Right4(x))
Right5(a25(x)) → Aa25(Right5(x))
Right6(a25(x)) → Aa25(Right6(x))
Right7(a25(x)) → Aa25(Right7(x))
Right8(a25(x)) → Aa25(Right8(x))
Right9(a25(x)) → Aa25(Right9(x))
Right10(a25(x)) → Aa25(Right10(x))
Right11(a25(x)) → Aa25(Right11(x))
Right12(a25(x)) → Aa25(Right12(x))
Right13(a25(x)) → Aa25(Right13(x))
Right14(a25(x)) → Aa25(Right14(x))
Right15(a25(x)) → Aa25(Right15(x))
Right16(a25(x)) → Aa25(Right16(x))
Right17(a25(x)) → Aa25(Right17(x))
Right18(a25(x)) → Aa25(Right18(x))
Right19(a25(x)) → Aa25(Right19(x))
Right20(a25(x)) → Aa25(Right20(x))
Right21(a25(x)) → Aa25(Right21(x))
Right22(a25(x)) → Aa25(Right22(x))
Right23(a25(x)) → Aa25(Right23(x))
Right24(a25(x)) → Aa25(Right24(x))
Right25(a25(x)) → Aa25(Right25(x))
Right26(a25(x)) → Aa25(Right26(x))
Right27(a25(x)) → Aa25(Right27(x))
Right28(a25(x)) → Aa25(Right28(x))
Right29(a25(x)) → Aa25(Right29(x))
Right30(a25(x)) → Aa25(Right30(x))
Right31(a25(x)) → Aa25(Right31(x))
Right32(a25(x)) → Aa25(Right32(x))
Right33(a25(x)) → Aa25(Right33(x))
Right34(a25(x)) → Aa25(Right34(x))
Right35(a25(x)) → Aa25(Right35(x))
Right36(a25(x)) → Aa25(Right36(x))
Right37(a25(x)) → Aa25(Right37(x))
Right38(a25(x)) → Aa25(Right38(x))
Right39(a25(x)) → Aa25(Right39(x))
Right40(a25(x)) → Aa25(Right40(x))
Right41(a25(x)) → Aa25(Right41(x))
Right1(a26(x)) → Aa26(Right1(x))
Right2(a26(x)) → Aa26(Right2(x))
Right3(a26(x)) → Aa26(Right3(x))
Right4(a26(x)) → Aa26(Right4(x))
Right5(a26(x)) → Aa26(Right5(x))
Right6(a26(x)) → Aa26(Right6(x))
Right7(a26(x)) → Aa26(Right7(x))
Right8(a26(x)) → Aa26(Right8(x))
Right9(a26(x)) → Aa26(Right9(x))
Right10(a26(x)) → Aa26(Right10(x))
Right11(a26(x)) → Aa26(Right11(x))
Right12(a26(x)) → Aa26(Right12(x))
Right13(a26(x)) → Aa26(Right13(x))
Right14(a26(x)) → Aa26(Right14(x))
Right15(a26(x)) → Aa26(Right15(x))
Right16(a26(x)) → Aa26(Right16(x))
Right17(a26(x)) → Aa26(Right17(x))
Right18(a26(x)) → Aa26(Right18(x))
Right19(a26(x)) → Aa26(Right19(x))
Right20(a26(x)) → Aa26(Right20(x))
Right21(a26(x)) → Aa26(Right21(x))
Right22(a26(x)) → Aa26(Right22(x))
Right23(a26(x)) → Aa26(Right23(x))
Right24(a26(x)) → Aa26(Right24(x))
Right25(a26(x)) → Aa26(Right25(x))
Right26(a26(x)) → Aa26(Right26(x))
Right27(a26(x)) → Aa26(Right27(x))
Right28(a26(x)) → Aa26(Right28(x))
Right29(a26(x)) → Aa26(Right29(x))
Right30(a26(x)) → Aa26(Right30(x))
Right31(a26(x)) → Aa26(Right31(x))
Right32(a26(x)) → Aa26(Right32(x))
Right33(a26(x)) → Aa26(Right33(x))
Right34(a26(x)) → Aa26(Right34(x))
Right35(a26(x)) → Aa26(Right35(x))
Right36(a26(x)) → Aa26(Right36(x))
Right37(a26(x)) → Aa26(Right37(x))
Right38(a26(x)) → Aa26(Right38(x))
Right39(a26(x)) → Aa26(Right39(x))
Right40(a26(x)) → Aa26(Right40(x))
Right41(a26(x)) → Aa26(Right41(x))
Right1(a34(x)) → Aa34(Right1(x))
Right2(a34(x)) → Aa34(Right2(x))
Right3(a34(x)) → Aa34(Right3(x))
Right4(a34(x)) → Aa34(Right4(x))
Right5(a34(x)) → Aa34(Right5(x))
Right6(a34(x)) → Aa34(Right6(x))
Right7(a34(x)) → Aa34(Right7(x))
Right8(a34(x)) → Aa34(Right8(x))
Right9(a34(x)) → Aa34(Right9(x))
Right10(a34(x)) → Aa34(Right10(x))
Right11(a34(x)) → Aa34(Right11(x))
Right12(a34(x)) → Aa34(Right12(x))
Right13(a34(x)) → Aa34(Right13(x))
Right14(a34(x)) → Aa34(Right14(x))
Right15(a34(x)) → Aa34(Right15(x))
Right16(a34(x)) → Aa34(Right16(x))
Right17(a34(x)) → Aa34(Right17(x))
Right18(a34(x)) → Aa34(Right18(x))
Right19(a34(x)) → Aa34(Right19(x))
Right20(a34(x)) → Aa34(Right20(x))
Right21(a34(x)) → Aa34(Right21(x))
Right22(a34(x)) → Aa34(Right22(x))
Right23(a34(x)) → Aa34(Right23(x))
Right24(a34(x)) → Aa34(Right24(x))
Right25(a34(x)) → Aa34(Right25(x))
Right26(a34(x)) → Aa34(Right26(x))
Right27(a34(x)) → Aa34(Right27(x))
Right28(a34(x)) → Aa34(Right28(x))
Right29(a34(x)) → Aa34(Right29(x))
Right30(a34(x)) → Aa34(Right30(x))
Right31(a34(x)) → Aa34(Right31(x))
Right32(a34(x)) → Aa34(Right32(x))
Right33(a34(x)) → Aa34(Right33(x))
Right34(a34(x)) → Aa34(Right34(x))
Right35(a34(x)) → Aa34(Right35(x))
Right36(a34(x)) → Aa34(Right36(x))
Right37(a34(x)) → Aa34(Right37(x))
Right38(a34(x)) → Aa34(Right38(x))
Right39(a34(x)) → Aa34(Right39(x))
Right40(a34(x)) → Aa34(Right40(x))
Right41(a34(x)) → Aa34(Right41(x))
Right1(a35(x)) → Aa35(Right1(x))
Right2(a35(x)) → Aa35(Right2(x))
Right3(a35(x)) → Aa35(Right3(x))
Right4(a35(x)) → Aa35(Right4(x))
Right5(a35(x)) → Aa35(Right5(x))
Right6(a35(x)) → Aa35(Right6(x))
Right7(a35(x)) → Aa35(Right7(x))
Right8(a35(x)) → Aa35(Right8(x))
Right9(a35(x)) → Aa35(Right9(x))
Right10(a35(x)) → Aa35(Right10(x))
Right11(a35(x)) → Aa35(Right11(x))
Right12(a35(x)) → Aa35(Right12(x))
Right13(a35(x)) → Aa35(Right13(x))
Right14(a35(x)) → Aa35(Right14(x))
Right15(a35(x)) → Aa35(Right15(x))
Right16(a35(x)) → Aa35(Right16(x))
Right17(a35(x)) → Aa35(Right17(x))
Right18(a35(x)) → Aa35(Right18(x))
Right19(a35(x)) → Aa35(Right19(x))
Right20(a35(x)) → Aa35(Right20(x))
Right21(a35(x)) → Aa35(Right21(x))
Right22(a35(x)) → Aa35(Right22(x))
Right23(a35(x)) → Aa35(Right23(x))
Right24(a35(x)) → Aa35(Right24(x))
Right25(a35(x)) → Aa35(Right25(x))
Right26(a35(x)) → Aa35(Right26(x))
Right27(a35(x)) → Aa35(Right27(x))
Right28(a35(x)) → Aa35(Right28(x))
Right29(a35(x)) → Aa35(Right29(x))
Right30(a35(x)) → Aa35(Right30(x))
Right31(a35(x)) → Aa35(Right31(x))
Right32(a35(x)) → Aa35(Right32(x))
Right33(a35(x)) → Aa35(Right33(x))
Right34(a35(x)) → Aa35(Right34(x))
Right35(a35(x)) → Aa35(Right35(x))
Right36(a35(x)) → Aa35(Right36(x))
Right37(a35(x)) → Aa35(Right37(x))
Right38(a35(x)) → Aa35(Right38(x))
Right39(a35(x)) → Aa35(Right39(x))
Right40(a35(x)) → Aa35(Right40(x))
Right41(a35(x)) → Aa35(Right41(x))
Right1(a36(x)) → Aa36(Right1(x))
Right2(a36(x)) → Aa36(Right2(x))
Right3(a36(x)) → Aa36(Right3(x))
Right4(a36(x)) → Aa36(Right4(x))
Right5(a36(x)) → Aa36(Right5(x))
Right6(a36(x)) → Aa36(Right6(x))
Right7(a36(x)) → Aa36(Right7(x))
Right8(a36(x)) → Aa36(Right8(x))
Right9(a36(x)) → Aa36(Right9(x))
Right10(a36(x)) → Aa36(Right10(x))
Right11(a36(x)) → Aa36(Right11(x))
Right12(a36(x)) → Aa36(Right12(x))
Right13(a36(x)) → Aa36(Right13(x))
Right14(a36(x)) → Aa36(Right14(x))
Right15(a36(x)) → Aa36(Right15(x))
Right16(a36(x)) → Aa36(Right16(x))
Right17(a36(x)) → Aa36(Right17(x))
Right18(a36(x)) → Aa36(Right18(x))
Right19(a36(x)) → Aa36(Right19(x))
Right20(a36(x)) → Aa36(Right20(x))
Right21(a36(x)) → Aa36(Right21(x))
Right22(a36(x)) → Aa36(Right22(x))
Right23(a36(x)) → Aa36(Right23(x))
Right24(a36(x)) → Aa36(Right24(x))
Right25(a36(x)) → Aa36(Right25(x))
Right26(a36(x)) → Aa36(Right26(x))
Right27(a36(x)) → Aa36(Right27(x))
Right28(a36(x)) → Aa36(Right28(x))
Right29(a36(x)) → Aa36(Right29(x))
Right30(a36(x)) → Aa36(Right30(x))
Right31(a36(x)) → Aa36(Right31(x))
Right32(a36(x)) → Aa36(Right32(x))
Right33(a36(x)) → Aa36(Right33(x))
Right34(a36(x)) → Aa36(Right34(x))
Right35(a36(x)) → Aa36(Right35(x))
Right36(a36(x)) → Aa36(Right36(x))
Right37(a36(x)) → Aa36(Right37(x))
Right38(a36(x)) → Aa36(Right38(x))
Right39(a36(x)) → Aa36(Right39(x))
Right40(a36(x)) → Aa36(Right40(x))
Right41(a36(x)) → Aa36(Right41(x))
Right1(a45(x)) → Aa45(Right1(x))
Right2(a45(x)) → Aa45(Right2(x))
Right3(a45(x)) → Aa45(Right3(x))
Right4(a45(x)) → Aa45(Right4(x))
Right5(a45(x)) → Aa45(Right5(x))
Right6(a45(x)) → Aa45(Right6(x))
Right7(a45(x)) → Aa45(Right7(x))
Right8(a45(x)) → Aa45(Right8(x))
Right9(a45(x)) → Aa45(Right9(x))
Right10(a45(x)) → Aa45(Right10(x))
Right11(a45(x)) → Aa45(Right11(x))
Right12(a45(x)) → Aa45(Right12(x))
Right13(a45(x)) → Aa45(Right13(x))
Right14(a45(x)) → Aa45(Right14(x))
Right15(a45(x)) → Aa45(Right15(x))
Right16(a45(x)) → Aa45(Right16(x))
Right17(a45(x)) → Aa45(Right17(x))
Right18(a45(x)) → Aa45(Right18(x))
Right19(a45(x)) → Aa45(Right19(x))
Right20(a45(x)) → Aa45(Right20(x))
Right21(a45(x)) → Aa45(Right21(x))
Right22(a45(x)) → Aa45(Right22(x))
Right23(a45(x)) → Aa45(Right23(x))
Right24(a45(x)) → Aa45(Right24(x))
Right25(a45(x)) → Aa45(Right25(x))
Right26(a45(x)) → Aa45(Right26(x))
Right27(a45(x)) → Aa45(Right27(x))
Right28(a45(x)) → Aa45(Right28(x))
Right29(a45(x)) → Aa45(Right29(x))
Right30(a45(x)) → Aa45(Right30(x))
Right31(a45(x)) → Aa45(Right31(x))
Right32(a45(x)) → Aa45(Right32(x))
Right33(a45(x)) → Aa45(Right33(x))
Right34(a45(x)) → Aa45(Right34(x))
Right35(a45(x)) → Aa45(Right35(x))
Right36(a45(x)) → Aa45(Right36(x))
Right37(a45(x)) → Aa45(Right37(x))
Right38(a45(x)) → Aa45(Right38(x))
Right39(a45(x)) → Aa45(Right39(x))
Right40(a45(x)) → Aa45(Right40(x))
Right41(a45(x)) → Aa45(Right41(x))
Right1(a46(x)) → Aa46(Right1(x))
Right2(a46(x)) → Aa46(Right2(x))
Right3(a46(x)) → Aa46(Right3(x))
Right4(a46(x)) → Aa46(Right4(x))
Right5(a46(x)) → Aa46(Right5(x))
Right6(a46(x)) → Aa46(Right6(x))
Right7(a46(x)) → Aa46(Right7(x))
Right8(a46(x)) → Aa46(Right8(x))
Right9(a46(x)) → Aa46(Right9(x))
Right10(a46(x)) → Aa46(Right10(x))
Right11(a46(x)) → Aa46(Right11(x))
Right12(a46(x)) → Aa46(Right12(x))
Right13(a46(x)) → Aa46(Right13(x))
Right14(a46(x)) → Aa46(Right14(x))
Right15(a46(x)) → Aa46(Right15(x))
Right16(a46(x)) → Aa46(Right16(x))
Right17(a46(x)) → Aa46(Right17(x))
Right18(a46(x)) → Aa46(Right18(x))
Right19(a46(x)) → Aa46(Right19(x))
Right20(a46(x)) → Aa46(Right20(x))
Right21(a46(x)) → Aa46(Right21(x))
Right22(a46(x)) → Aa46(Right22(x))
Right23(a46(x)) → Aa46(Right23(x))
Right24(a46(x)) → Aa46(Right24(x))
Right25(a46(x)) → Aa46(Right25(x))
Right26(a46(x)) → Aa46(Right26(x))
Right27(a46(x)) → Aa46(Right27(x))
Right28(a46(x)) → Aa46(Right28(x))
Right29(a46(x)) → Aa46(Right29(x))
Right30(a46(x)) → Aa46(Right30(x))
Right31(a46(x)) → Aa46(Right31(x))
Right32(a46(x)) → Aa46(Right32(x))
Right33(a46(x)) → Aa46(Right33(x))
Right34(a46(x)) → Aa46(Right34(x))
Right35(a46(x)) → Aa46(Right35(x))
Right36(a46(x)) → Aa46(Right36(x))
Right37(a46(x)) → Aa46(Right37(x))
Right38(a46(x)) → Aa46(Right38(x))
Right39(a46(x)) → Aa46(Right39(x))
Right40(a46(x)) → Aa46(Right40(x))
Right41(a46(x)) → Aa46(Right41(x))
Right1(a56(x)) → Aa56(Right1(x))
Right2(a56(x)) → Aa56(Right2(x))
Right3(a56(x)) → Aa56(Right3(x))
Right4(a56(x)) → Aa56(Right4(x))
Right5(a56(x)) → Aa56(Right5(x))
Right6(a56(x)) → Aa56(Right6(x))
Right7(a56(x)) → Aa56(Right7(x))
Right8(a56(x)) → Aa56(Right8(x))
Right9(a56(x)) → Aa56(Right9(x))
Right10(a56(x)) → Aa56(Right10(x))
Right11(a56(x)) → Aa56(Right11(x))
Right12(a56(x)) → Aa56(Right12(x))
Right13(a56(x)) → Aa56(Right13(x))
Right14(a56(x)) → Aa56(Right14(x))
Right15(a56(x)) → Aa56(Right15(x))
Right16(a56(x)) → Aa56(Right16(x))
Right17(a56(x)) → Aa56(Right17(x))
Right18(a56(x)) → Aa56(Right18(x))
Right19(a56(x)) → Aa56(Right19(x))
Right20(a56(x)) → Aa56(Right20(x))
Right21(a56(x)) → Aa56(Right21(x))
Right22(a56(x)) → Aa56(Right22(x))
Right23(a56(x)) → Aa56(Right23(x))
Right24(a56(x)) → Aa56(Right24(x))
Right25(a56(x)) → Aa56(Right25(x))
Right26(a56(x)) → Aa56(Right26(x))
Right27(a56(x)) → Aa56(Right27(x))
Right28(a56(x)) → Aa56(Right28(x))
Right29(a56(x)) → Aa56(Right29(x))
Right30(a56(x)) → Aa56(Right30(x))
Right31(a56(x)) → Aa56(Right31(x))
Right32(a56(x)) → Aa56(Right32(x))
Right33(a56(x)) → Aa56(Right33(x))
Right34(a56(x)) → Aa56(Right34(x))
Right35(a56(x)) → Aa56(Right35(x))
Right36(a56(x)) → Aa56(Right36(x))
Right37(a56(x)) → Aa56(Right37(x))
Right38(a56(x)) → Aa56(Right38(x))
Right39(a56(x)) → Aa56(Right39(x))
Right40(a56(x)) → Aa56(Right40(x))
Right41(a56(x)) → Aa56(Right41(x))
Aa12(Left(x)) → Left(a12(x))
Aa13(Left(x)) → Left(a13(x))
Aa14(Left(x)) → Left(a14(x))
Aa15(Left(x)) → Left(a15(x))
Aa16(Left(x)) → Left(a16(x))
Aa23(Left(x)) → Left(a23(x))
Aa24(Left(x)) → Left(a24(x))
Aa25(Left(x)) → Left(a25(x))
Aa26(Left(x)) → Left(a26(x))
Aa34(Left(x)) → Left(a34(x))
Aa35(Left(x)) → Left(a35(x))
Aa36(Left(x)) → Left(a36(x))
Aa45(Left(x)) → Left(a45(x))
Aa46(Left(x)) → Left(a46(x))
Aa56(Left(x)) → Left(a56(x))
Wait(Left(x)) → Begin(x)
a12(a12(x)) → x
a13(a13(x)) → x
a14(a14(x)) → x
a15(a15(x)) → x
a16(a16(x)) → x
a23(a23(x)) → x
a24(a24(x)) → x
a25(a25(x)) → x
a26(a26(x)) → x
a34(a34(x)) → x
a35(a35(x)) → x
a36(a36(x)) → x
a45(a45(x)) → x
a46(a46(x)) → x
a56(a56(x)) → x
a13(x) → a12(a23(a12(x)))
a14(x) → a12(a23(a34(a23(a12(x)))))
a15(x) → a12(a23(a34(a45(a34(a23(a12(x)))))))
a16(x) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x)))))))))
a24(x) → a23(a34(a23(x)))
a25(x) → a23(a34(a45(a34(a23(x)))))
a26(x) → a23(a34(a45(a56(a45(a34(a23(x)))))))
a35(x) → a34(a45(a34(x)))
a36(x) → a34(a45(a56(a45(a34(x)))))
a46(x) → a45(a56(a45(x)))
a12(a23(a12(a23(a12(a23(x)))))) → x
a23(a34(a23(a34(a23(a34(x)))))) → x
a34(a45(a34(a45(a34(a45(x)))))) → x
a45(a56(a45(a56(a45(a56(x)))))) → x
a12(a34(x)) → a34(a12(x))
a12(a45(x)) → a45(a12(x))
a12(a56(x)) → a56(a12(x))
a23(a45(x)) → a45(a23(x))
a23(a56(x)) → a56(a23(x))
a34(a56(x)) → a56(a34(x))

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:
Wait Left a56 a34 End → Wait Left a56 a34 End

Wait Left a56 a34 End → Wait Left a56 a34 End
by OverlapClosure OC 2
Wait Left a56 → Wait Right41
by OverlapClosure OC 2
Wait Left → Begin
by original rule (OC 1)
Begin a56 → Wait Right41
by original rule (OC 1)
Right41 a34 End → Left a56 a34 End
by original rule (OC 1)

(2) NO