0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 175 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 29 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QDPSizeChangeProof (⇔, 0 ms)
↳16 YES
↳17 QDP
↳18 UsableRulesProof (⇔, 0 ms)
↳19 QDP
↳20 QDPSizeChangeProof (⇔, 0 ms)
↳21 YES
↳22 QDP
↳23 QDPOrderProof (⇔, 132 ms)
↳24 QDP
↳25 DependencyGraphProof (⇔, 0 ms)
↳26 TRUE
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
F3_IN(T22, T23) → U11(f20_in(T22, T23), T22, T23)
F3_IN(T22, T23) → F20_IN(T22, T23)
F3_IN(T108, T109) → U21(f119_in(T108, T109), T108, T109)
F3_IN(T108, T109) → F119_IN(T108, T109)
F24_IN(s(T38), s(T39)) → U31(f24_in(T38, T39), s(T38), s(T39))
F24_IN(s(T38), s(T39)) → F24_IN(T38, T39)
F91_IN(s(T89), s(T90)) → U41(f91_in(T89, T90), s(T89), s(T90))
F91_IN(s(T89), s(T90)) → F91_IN(T89, T90)
F26_IN(s(T60), T61) → U51(f78_in(T60, T61), s(T60), T61)
F26_IN(s(T60), T61) → F78_IN(T60, T61)
F125_IN(s(T124), s(T125)) → U61(f125_in(T124, T125), s(T124), s(T125))
F125_IN(s(T124), s(T125)) → F125_IN(T124, T125)
F82_IN(T77, s(T78)) → U71(f91_in(T77, T78), T77, s(T78))
F82_IN(T77, s(T78)) → F91_IN(T77, T78)
F20_IN(T22, T23) → U81(f24_in(T22, T23), T22, T23)
F20_IN(T22, T23) → F24_IN(T22, T23)
U81(f24_out1, T22, T23) → U91(f26_in(T22, T23), T22, T23)
U81(f24_out1, T22, T23) → F26_IN(T22, T23)
F78_IN(T60, T61) → U101(f82_in(T60, T61), T60, T61)
F78_IN(T60, T61) → F82_IN(T60, T61)
U101(f82_out1(T66), T60, T61) → U111(f3_in(s(T60), T66), T60, T61, T66)
U101(f82_out1(T66), T60, T61) → F3_IN(s(T60), T66)
F119_IN(T108, T109) → U121(f125_in(T108, T109), T108, T109)
F119_IN(T108, T109) → F125_IN(T108, T109)
U121(f125_out1, T108, T109) → U131(f26_in(T109, T108), T108, T109)
U121(f125_out1, T108, T109) → F26_IN(T109, T108)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
F125_IN(s(T124), s(T125)) → F125_IN(T124, T125)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
F125_IN(s(T124), s(T125)) → F125_IN(T124, T125)
From the DPs we obtained the following set of size-change graphs:
F91_IN(s(T89), s(T90)) → F91_IN(T89, T90)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
F91_IN(s(T89), s(T90)) → F91_IN(T89, T90)
From the DPs we obtained the following set of size-change graphs:
F24_IN(s(T38), s(T39)) → F24_IN(T38, T39)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
F24_IN(s(T38), s(T39)) → F24_IN(T38, T39)
From the DPs we obtained the following set of size-change graphs:
F3_IN(T22, T23) → F20_IN(T22, T23)
F20_IN(T22, T23) → U81(f24_in(T22, T23), T22, T23)
U81(f24_out1, T22, T23) → F26_IN(T22, T23)
F26_IN(s(T60), T61) → F78_IN(T60, T61)
F78_IN(T60, T61) → U101(f82_in(T60, T61), T60, T61)
U101(f82_out1(T66), T60, T61) → F3_IN(s(T60), T66)
F3_IN(T108, T109) → F119_IN(T108, T109)
F119_IN(T108, T109) → U121(f125_in(T108, T109), T108, T109)
U121(f125_out1, T108, T109) → F26_IN(T109, T108)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F78_IN(T60, T61) → U101(f82_in(T60, T61), T60, T61)
POL(0) = 0
POL(F119_IN(x1, x2)) = x1 + x2
POL(F20_IN(x1, x2)) = x1 + x2
POL(F26_IN(x1, x2)) = x1 + x2
POL(F3_IN(x1, x2)) = x1 + x2
POL(F78_IN(x1, x2)) = 1 + x1 + x2
POL(U101(x1, x2, x3)) = x1 + x2
POL(U121(x1, x2, x3)) = x2 + x3
POL(U3(x1, x2, x3)) = 0
POL(U4(x1, x2, x3)) = x1
POL(U6(x1, x2, x3)) = 0
POL(U7(x1, x2, x3)) = 1 + x1
POL(U81(x1, x2, x3)) = x2 + x3
POL(f125_in(x1, x2)) = 0
POL(f125_out1) = 0
POL(f24_in(x1, x2)) = 0
POL(f24_out1) = 0
POL(f82_in(x1, x2)) = x2
POL(f82_out1(x1)) = 1 + x1
POL(f91_in(x1, x2)) = x2
POL(f91_out1(x1)) = x1
POL(s(x1)) = 1 + x1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
f91_in(0, T95) → f91_out1(T95)
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
F3_IN(T22, T23) → F20_IN(T22, T23)
F20_IN(T22, T23) → U81(f24_in(T22, T23), T22, T23)
U81(f24_out1, T22, T23) → F26_IN(T22, T23)
F26_IN(s(T60), T61) → F78_IN(T60, T61)
U101(f82_out1(T66), T60, T61) → F3_IN(s(T60), T66)
F3_IN(T108, T109) → F119_IN(T108, T109)
F119_IN(T108, T109) → U121(f125_in(T108, T109), T108, T109)
U121(f125_out1, T108, T109) → F26_IN(T109, T108)
f3_in(T22, T23) → U1(f20_in(T22, T23), T22, T23)
U1(f20_out1(T25), T22, T23) → f3_out1(T25)
f3_in(T108, T109) → U2(f119_in(T108, T109), T108, T109)
U2(f119_out1(T111), T108, T109) → f3_out1(T111)
f24_in(s(T38), s(T39)) → U3(f24_in(T38, T39), s(T38), s(T39))
U3(f24_out1, s(T38), s(T39)) → f24_out1
f24_in(0, s(T46)) → f24_out1
f24_in(0, 0) → f24_out1
f91_in(s(T89), s(T90)) → U4(f91_in(T89, T90), s(T89), s(T90))
U4(f91_out1(X110), s(T89), s(T90)) → f91_out1(X110)
f91_in(0, T95) → f91_out1(T95)
f26_in(0, T53) → f26_out1(T53)
f26_in(s(T60), T61) → U5(f78_in(T60, T61), s(T60), T61)
U5(f78_out1(X58, T63), s(T60), T61) → f26_out1(T63)
f125_in(s(T124), s(T125)) → U6(f125_in(T124, T125), s(T124), s(T125))
U6(f125_out1, s(T124), s(T125)) → f125_out1
f125_in(s(T130), 0) → f125_out1
f82_in(T77, s(T78)) → U7(f91_in(T77, T78), T77, s(T78))
U7(f91_out1(X86), T77, s(T78)) → f82_out1(X86)
f20_in(T22, T23) → U8(f24_in(T22, T23), T22, T23)
U8(f24_out1, T22, T23) → U9(f26_in(T22, T23), T22, T23)
U9(f26_out1(T25), T22, T23) → f20_out1(T25)
f78_in(T60, T61) → U10(f82_in(T60, T61), T60, T61)
U10(f82_out1(T66), T60, T61) → U11(f3_in(s(T60), T66), T60, T61, T66)
U11(f3_out1(T63), T60, T61, T66) → f78_out1(T66, T63)
f119_in(T108, T109) → U12(f125_in(T108, T109), T108, T109)
U12(f125_out1, T108, T109) → U13(f26_in(T109, T108), T108, T109)
U13(f26_out1(T111), T108, T109) → f119_out1(T111)