(0) Obligation:

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Queries:

q(g,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

q16(f(T656)) :- p407(f(T656)).
p162(T228, T229) :- q1(f(T228), T229).
p162(T254, f(T255)) :- ','(qc1(f(T254), f(T255)), p162(T254, T255)).
p162(T260, f(T260)) :- ','(qc1(f(T260), f(T260)), t175(T260)).
q46(f(f(T75))) :- p63(T75).
p183(T270) :- q46(f(T270)).
p183(f(T281)) :- ','(qc46(f(f(T281))), p183(T281)).
t175(T270) :- p183(T270).
p151(T228, T229) :- p162(T228, T229).
p151(T285, T285) :- t175(T285).
p151(T303, f(T304)) :- ','(rc152(T303, f(T304)), p151(T303, T304)).
p144(T200, T201) :- p151(T200, T201).
r134(f(f(f(T336)))) :- p144(f(f(f(f(f(f(f(f(T336)))))))), T336).
r134(f(f(T356))) :- ','(qc214(f(T356)), p162(f(f(f(f(f(f(f(T356))))))), T356)).
p123(f(T375)) :- r134(f(T375)).
p123(f(f(T389))) :- ','(rc134(f(f(T389))), p151(f(f(f(f(f(f(f(T389))))))), T389)).
p132(f(f(T179))) :- p144(f(f(f(f(f(f(f(T179))))))), T179).
p132(T165) :- ','(qc133(T165), r134(T165)).
r105(f(f(f(T423)))) :- p123(f(T423)).
r105(f(f(T440))) :- ','(qc269(f(T440)), p132(T440)).
p121(T165) :- p132(T165).
p121(T151) :- ','(rc122(T151), p123(T151)).
p94(f(T456)) :- r105(f(T456)).
p94(f(f(T470))) :- ','(rc105(f(f(T470))), p121(T470)).
p103(f(f(T151))) :- p121(T151).
p103(T127) :- ','(qc104(T127), r105(T127)).
r76(f(f(f(T501)))) :- p94(f(T501)).
r76(f(f(T518))) :- ','(qc321(f(T518)), p103(T518)).
p92(T127) :- p103(T127).
p92(T113) :- ','(rc93(T113), p94(T113)).
p65(f(T534)) :- r76(f(T534)).
p65(f(f(T548))) :- ','(rc76(f(f(T548))), p92(T548)).
p74(f(f(T113))) :- p92(T113).
p74(T89) :- ','(qc75(T89), r76(T89)).
r36(T51) :- q46(T51).
r36(T51) :- ','(qc46(T51), r47(T51)).
r47(f(f(f(T579)))) :- p65(f(T579)).
r47(f(f(T596))) :- ','(qc373(f(T596)), p74(T596)).
r47(f(T601)) :- t175(T601).
p63(T89) :- p74(T89).
p63(T75) :- ','(rc64(T75), p65(T75)).
p407(f(T628)) :- r47(f(T628)).
p407(f(f(T642))) :- ','(rc47(f(f(T642))), p63(T642)).
p454(T710, T711) :- q1(T710, T711).
p454(T736, f(T737)) :- ','(qc1(T736, f(T737)), p454(T736, T737)).
p454(f(T742), f(T742)) :- ','(qc1(f(T742), f(T742)), t175(T742)).
p443(T710, T711) :- p454(T710, T711).
p443(f(T746), T746) :- t175(T746).
p443(T764, f(T765)) :- ','(rc444(T764, f(T765)), p443(T764, T765)).
q1(T36, f(f(T36))) :- q16(T36).
q1(T36, f(f(T36))) :- ','(qc16(T36), r36(T36)).
q1(T614, f(f(T614))) :- ','(rc24(T614), r36(T614)).
q1(T614, f(f(T614))) :- ','(rc24(T614), ','(rc36(T614), p407(T614))).
q1(T11, f(f(T11))) :- ','(pc15(T11), q16(T11)).
q1(T682, f(f(T683))) :- p443(T682, T683).

Clauses:

qc16(f(T656)) :- pc407(f(T656)).
qc1(a, b).
qc1(T11, f(f(T11))) :- ','(pc15(T11), qc16(T11)).
qc1(T682, f(f(T683))) :- qc443(T682, T683).
qc162(T254, f(T255)) :- ','(qc1(f(T254), f(T255)), qc162(T254, T255)).
qc162(T260, f(T260)) :- ','(qc1(f(T260), f(T260)), tc175(T260)).
qc46(f(f(T75))) :- qc63(T75).
qc183(f(T281)) :- ','(qc46(f(f(T281))), qc183(T281)).
tc175(T270) :- qc183(T270).
qc151(T303, f(T304)) :- ','(rc152(T303, f(T304)), qc151(T303, T304)).
pc144(T200, T201) :- qc151(T200, T201).
rc134(f(f(T356))) :- ','(qc214(f(T356)), qc162(f(f(f(f(f(f(f(T356))))))), T356)).
pc123(f(f(T389))) :- ','(rc134(f(f(T389))), qc151(f(f(f(f(f(f(f(T389))))))), T389)).
qc132(T165) :- ','(qc133(T165), rc134(T165)).
rc105(f(f(T440))) :- ','(qc269(f(T440)), qc132(T440)).
qc121(T151) :- ','(rc122(T151), pc123(T151)).
pc94(f(f(T470))) :- ','(rc105(f(f(T470))), qc121(T470)).
qc103(T127) :- ','(qc104(T127), rc105(T127)).
rc76(f(f(T518))) :- ','(qc321(f(T518)), qc103(T518)).
qc92(T113) :- ','(rc93(T113), pc94(T113)).
pc65(f(f(T548))) :- ','(rc76(f(f(T548))), qc92(T548)).
qc74(T89) :- ','(qc75(T89), rc76(T89)).
rc36(T51) :- ','(qc46(T51), rc47(T51)).
rc47(f(f(T596))) :- ','(qc373(f(T596)), qc74(T596)).
rc47(f(T601)) :- tc175(T601).
qc63(T75) :- ','(rc64(T75), pc65(T75)).
pc407(f(f(T642))) :- ','(rc47(f(f(T642))), qc63(T642)).
qc454(a, b) :- qc1(a, b).
qc454(T736, f(T737)) :- ','(qc1(T736, f(T737)), qc454(T736, T737)).
qc454(f(T742), f(T742)) :- ','(qc1(f(T742), f(T742)), tc175(T742)).
qc443(a, b) :- rc444(a, b).
qc443(T764, f(T765)) :- ','(rc444(T764, f(T765)), qc443(T764, T765)).
pc15(T614) :- ','(rc24(T614), ','(rc36(T614), pc407(T614))).
rc24(T36) :- ','(qc16(T36), rc36(T36)).
rc64(T89) :- qc74(T89).
qc75(f(f(T113))) :- qc92(T113).
rc93(T127) :- qc103(T127).
qc104(f(f(T151))) :- qc121(T151).
rc122(T165) :- qc132(T165).
qc133(f(f(T179))) :- pc144(f(f(f(f(f(f(f(T179))))))), T179).
rc152(T228, T229) :- qc162(T228, T229).
rc152(T285, T285) :- tc175(T285).
qc214(f(f(T336))) :- pc144(f(f(f(f(f(f(f(f(T336)))))))), T336).
qc269(f(f(T423))) :- pc123(f(T423)).
qc321(f(f(T501))) :- pc94(f(T501)).
qc373(f(f(T579))) :- pc65(f(T579)).
rc444(T710, T711) :- qc454(T710, T711).
rc444(f(T746), T746) :- tc175(T746).

Afs:

q1(x1, x2)  =  q1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
q1_in: (b,b)
q16_in: (b)
p407_in: (b)
r47_in: (b)
p65_in: (b)
r76_in: (b)
p94_in: (b)
r105_in: (b)
p123_in: (b)
r134_in: (b)
p144_in: (b,b)
p151_in: (b,b)
p162_in: (b,b)
qc16_in: (b)
pc407_in: (b)
rc47_in: (b)
qc373_in: (b)
pc65_in: (b)
rc76_in: (b)
qc321_in: (b)
pc94_in: (b)
rc105_in: (b)
qc269_in: (b)
pc123_in: (b)
rc134_in: (b)
qc214_in: (b)
pc144_in: (b,b)
qc151_in: (b,b)
rc152_in: (b,b)
qc162_in: (b,b)
qc1_in: (b,b)
pc15_in: (b)
rc24_in: (b)
rc36_in: (b)
qc46_in: (b)
qc63_in: (b)
rc64_in: (b)
qc74_in: (b)
qc75_in: (b)
qc92_in: (b)
rc93_in: (b)
qc103_in: (b)
qc104_in: (b)
qc121_in: (b)
rc122_in: (b)
qc132_in: (b)
qc133_in: (b)
tc175_in: (b)
qc183_in: (b)
qc443_in: (b,b)
rc444_in: (b,b)
qc454_in: (b,b)
r36_in: (b)
q46_in: (b)
p63_in: (b)
p74_in: (b)
p92_in: (b)
p103_in: (b)
p121_in: (b)
p132_in: (b)
t175_in: (b)
p183_in: (b)
p443_in: (b,b)
p454_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

Q1_IN_GG(T36, f(f(T36))) → U72_GG(T36, q16_in_g(T36))
Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
Q16_IN_G(f(T656)) → U1_G(T656, p407_in_g(f(T656)))
Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → U60_G(T628, r47_in_g(f(T628)))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
R47_IN_G(f(f(f(T579)))) → U53_G(T579, p65_in_g(f(T579)))
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → U44_G(T534, r76_in_g(f(T534)))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → U38_G(T501, p94_in_g(f(T501)))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
P94_IN_G(f(T456)) → U32_G(T456, r105_in_g(f(T456)))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
R105_IN_G(f(f(f(T423)))) → U26_G(T423, p123_in_g(f(T423)))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
P123_IN_G(f(T375)) → U20_G(T375, r134_in_g(f(T375)))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
R134_IN_G(f(f(f(T336)))) → U17_G(T336, p144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P144_IN_GG(T200, T201) → U16_GG(T200, T201, p151_in_gg(T200, T201))
P144_IN_GG(T200, T201) → P151_IN_GG(T200, T201)
P151_IN_GG(T228, T229) → U12_GG(T228, T229, p162_in_gg(T228, T229))
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
P162_IN_GG(T228, T229) → U2_GG(T228, T229, q1_in_gg(f(T228), T229))
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → U74_GG(T36, r36_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → U50_G(T51, q46_in_g(T51))
R36_IN_G(T51) → Q46_IN_G(T51)
Q46_IN_G(f(f(T75))) → U7_G(T75, p63_in_g(T75))
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → U57_G(T89, p74_in_g(T89))
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → U47_G(T113, p92_in_g(T113))
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P92_IN_G(T127) → U41_G(T127, p103_in_g(T127))
P92_IN_G(T127) → P103_IN_G(T127)
P103_IN_G(f(f(T151))) → U35_G(T151, p121_in_g(T151))
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P121_IN_G(T165) → U29_G(T165, p132_in_g(T165))
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(f(f(T179))) → U23_G(T179, p144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → U25_G(T165, r134_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
U18_G(T356, qc214_out_g(f(T356))) → U19_G(T356, p162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → U4_GG(T254, T255, p162_in_gg(T254, T255))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → U6_GG(T260, t175_in_g(T260))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → U11_G(T270, p183_in_g(T270))
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → U8_G(T270, q46_in_g(f(T270)))
P183_IN_G(T270) → Q46_IN_G(f(T270))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
U9_G(T281, qc46_out_g(f(f(T281)))) → U10_G(T281, p183_in_g(T281))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → U31_G(T151, p123_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
U21_G(T389, rc134_out_g(f(f(T389)))) → U22_G(T389, p151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → U13_GG(T285, t175_in_g(T285))
P151_IN_GG(T285, T285) → T175_IN_G(T285)
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → U15_GG(T303, T304, p151_in_gg(T303, T304))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → U37_G(T127, r105_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
U27_G(T440, qc269_out_g(f(T440))) → U28_G(T440, p132_in_g(T440))
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → U43_G(T113, p94_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
U33_G(T470, rc105_out_g(f(f(T470)))) → U34_G(T470, p121_in_g(T470))
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → U49_G(T89, r76_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → U40_G(T518, p103_in_g(T518))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → U59_G(T75, p65_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
U45_G(T548, rc76_out_g(f(f(T548)))) → U46_G(T548, p92_in_g(T548))
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → U52_G(T51, r47_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
U54_G(T596, qc373_out_g(f(T596))) → U55_G(T596, p74_in_g(T596))
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → U56_G(T601, t175_in_g(T601))
R47_IN_G(f(T601)) → T175_IN_G(T601)
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → U76_GG(T614, r36_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → U78_GG(T614, p407_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
U61_G(T642, rc47_out_g(f(f(T642)))) → U62_G(T642, p63_in_g(T642))
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → U80_GG(T11, q16_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
Q1_IN_GG(T682, f(f(T683))) → U81_GG(T682, T683, p443_in_gg(T682, T683))
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → U68_GG(T710, T711, p454_in_gg(T710, T711))
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T710, T711) → U63_GG(T710, T711, q1_in_gg(T710, T711))
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → U65_GG(T736, T737, p454_in_gg(T736, T737))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → U67_GG(T742, t175_in_g(T742))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → U69_GG(T746, t175_in_g(T746))
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → U71_GG(T764, T765, p443_in_gg(T764, T765))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

Pi is empty.
We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

Q1_IN_GG(T36, f(f(T36))) → U72_GG(T36, q16_in_g(T36))
Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
Q16_IN_G(f(T656)) → U1_G(T656, p407_in_g(f(T656)))
Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → U60_G(T628, r47_in_g(f(T628)))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
R47_IN_G(f(f(f(T579)))) → U53_G(T579, p65_in_g(f(T579)))
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → U44_G(T534, r76_in_g(f(T534)))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → U38_G(T501, p94_in_g(f(T501)))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
P94_IN_G(f(T456)) → U32_G(T456, r105_in_g(f(T456)))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
R105_IN_G(f(f(f(T423)))) → U26_G(T423, p123_in_g(f(T423)))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
P123_IN_G(f(T375)) → U20_G(T375, r134_in_g(f(T375)))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
R134_IN_G(f(f(f(T336)))) → U17_G(T336, p144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P144_IN_GG(T200, T201) → U16_GG(T200, T201, p151_in_gg(T200, T201))
P144_IN_GG(T200, T201) → P151_IN_GG(T200, T201)
P151_IN_GG(T228, T229) → U12_GG(T228, T229, p162_in_gg(T228, T229))
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
P162_IN_GG(T228, T229) → U2_GG(T228, T229, q1_in_gg(f(T228), T229))
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → U74_GG(T36, r36_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → U50_G(T51, q46_in_g(T51))
R36_IN_G(T51) → Q46_IN_G(T51)
Q46_IN_G(f(f(T75))) → U7_G(T75, p63_in_g(T75))
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → U57_G(T89, p74_in_g(T89))
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → U47_G(T113, p92_in_g(T113))
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P92_IN_G(T127) → U41_G(T127, p103_in_g(T127))
P92_IN_G(T127) → P103_IN_G(T127)
P103_IN_G(f(f(T151))) → U35_G(T151, p121_in_g(T151))
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P121_IN_G(T165) → U29_G(T165, p132_in_g(T165))
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(f(f(T179))) → U23_G(T179, p144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → U25_G(T165, r134_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
U18_G(T356, qc214_out_g(f(T356))) → U19_G(T356, p162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → U4_GG(T254, T255, p162_in_gg(T254, T255))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → U6_GG(T260, t175_in_g(T260))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → U11_G(T270, p183_in_g(T270))
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → U8_G(T270, q46_in_g(f(T270)))
P183_IN_G(T270) → Q46_IN_G(f(T270))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
U9_G(T281, qc46_out_g(f(f(T281)))) → U10_G(T281, p183_in_g(T281))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → U31_G(T151, p123_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
U21_G(T389, rc134_out_g(f(f(T389)))) → U22_G(T389, p151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → U13_GG(T285, t175_in_g(T285))
P151_IN_GG(T285, T285) → T175_IN_G(T285)
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → U15_GG(T303, T304, p151_in_gg(T303, T304))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → U37_G(T127, r105_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
U27_G(T440, qc269_out_g(f(T440))) → U28_G(T440, p132_in_g(T440))
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → U43_G(T113, p94_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
U33_G(T470, rc105_out_g(f(f(T470)))) → U34_G(T470, p121_in_g(T470))
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → U49_G(T89, r76_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → U40_G(T518, p103_in_g(T518))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → U59_G(T75, p65_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
U45_G(T548, rc76_out_g(f(f(T548)))) → U46_G(T548, p92_in_g(T548))
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → U52_G(T51, r47_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
U54_G(T596, qc373_out_g(f(T596))) → U55_G(T596, p74_in_g(T596))
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → U56_G(T601, t175_in_g(T601))
R47_IN_G(f(T601)) → T175_IN_G(T601)
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → U76_GG(T614, r36_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → U78_GG(T614, p407_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
U61_G(T642, rc47_out_g(f(f(T642)))) → U62_G(T642, p63_in_g(T642))
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → U80_GG(T11, q16_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
Q1_IN_GG(T682, f(f(T683))) → U81_GG(T682, T683, p443_in_gg(T682, T683))
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → U68_GG(T710, T711, p454_in_gg(T710, T711))
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T710, T711) → U63_GG(T710, T711, q1_in_gg(T710, T711))
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → U65_GG(T736, T737, p454_in_gg(T736, T737))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → U67_GG(T742, t175_in_g(T742))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → U69_GG(T746, t175_in_g(T746))
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → U71_GG(T764, T765, p443_in_gg(T764, T765))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 55 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P144_IN_GG(T200, T201) → P151_IN_GG(T200, T201)
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → Q46_IN_G(T51)
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P92_IN_G(T127) → P103_IN_G(T127)
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → Q46_IN_G(f(T270))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → T175_IN_G(T285)
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → T175_IN_G(T601)
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P144_IN_GG(T200, T201) → P151_IN_GG(T200, T201)
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → Q46_IN_G(T51)
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P92_IN_G(T127) → P103_IN_G(T127)
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → Q46_IN_G(f(T270))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → T175_IN_G(T285)
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → T175_IN_G(T601)
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

The set Q consists of the following terms:

qc16_in_g(x0)
pc407_in_g(x0)
rc47_in_g(x0)
qc373_in_g(x0)
pc65_in_g(x0)
rc76_in_g(x0)
qc321_in_g(x0)
pc94_in_g(x0)
rc105_in_g(x0)
qc269_in_g(x0)
pc123_in_g(x0)
rc134_in_g(x0)
qc214_in_g(x0)
pc144_in_gg(x0, x1)
qc151_in_gg(x0, x1)
rc152_in_gg(x0, x1)
qc162_in_gg(x0, x1)
qc1_in_gg(x0, x1)
pc15_in_g(x0)
rc24_in_g(x0)
U140_g(x0, x1)
rc36_in_g(x0)
qc46_in_g(x0)
qc63_in_g(x0)
rc64_in_g(x0)
qc74_in_g(x0)
qc75_in_g(x0)
qc92_in_g(x0)
rc93_in_g(x0)
qc103_in_g(x0)
qc104_in_g(x0)
qc121_in_g(x0)
rc122_in_g(x0)
qc132_in_g(x0)
qc133_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tc175_in_g(x0)
qc183_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qc443_in_gg(x0, x1)
rc444_in_gg(x0, x1)
qc454_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(9) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule P144_IN_GG(T200, T201) → P151_IN_GG(T200, T201) we obtained the following new rules [LPAR04]:

P144_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
P144_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → Q46_IN_G(T51)
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P92_IN_G(T127) → P103_IN_G(T127)
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → Q46_IN_G(f(T270))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → T175_IN_G(T285)
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → T175_IN_G(T601)
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)
P144_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
P144_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

The set Q consists of the following terms:

qc16_in_g(x0)
pc407_in_g(x0)
rc47_in_g(x0)
qc373_in_g(x0)
pc65_in_g(x0)
rc76_in_g(x0)
qc321_in_g(x0)
pc94_in_g(x0)
rc105_in_g(x0)
qc269_in_g(x0)
pc123_in_g(x0)
rc134_in_g(x0)
qc214_in_g(x0)
pc144_in_gg(x0, x1)
qc151_in_gg(x0, x1)
rc152_in_gg(x0, x1)
qc162_in_gg(x0, x1)
qc1_in_gg(x0, x1)
pc15_in_g(x0)
rc24_in_g(x0)
U140_g(x0, x1)
rc36_in_g(x0)
qc46_in_g(x0)
qc63_in_g(x0)
rc64_in_g(x0)
qc74_in_g(x0)
qc75_in_g(x0)
qc92_in_g(x0)
rc93_in_g(x0)
qc103_in_g(x0)
qc104_in_g(x0)
qc121_in_g(x0)
rc122_in_g(x0)
qc132_in_g(x0)
qc133_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tc175_in_g(x0)
qc183_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qc443_in_gg(x0, x1)
rc444_in_gg(x0, x1)
qc454_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


Q1_IN_GG(T36, f(f(T36))) → Q16_IN_G(T36)
R47_IN_G(f(f(f(T579)))) → P65_IN_G(f(T579))
P65_IN_G(f(T534)) → R76_IN_G(f(T534))
R76_IN_G(f(f(f(T501)))) → P94_IN_G(f(T501))
R105_IN_G(f(f(f(T423)))) → P123_IN_G(f(T423))
R134_IN_G(f(f(f(T336)))) → P144_IN_GG(f(f(f(f(f(f(f(f(T336)))))))), T336)
P151_IN_GG(T228, T229) → P162_IN_GG(T228, T229)
Q1_IN_GG(T36, f(f(T36))) → U73_GG(T36, qc16_in_g(T36))
Q46_IN_G(f(f(T75))) → P63_IN_G(T75)
P63_IN_G(T89) → P74_IN_G(T89)
P74_IN_G(f(f(T113))) → P92_IN_G(T113)
P103_IN_G(f(f(T151))) → P121_IN_G(T151)
P132_IN_G(f(f(T179))) → P144_IN_GG(f(f(f(f(f(f(f(T179))))))), T179)
R134_IN_G(f(f(T356))) → U18_G(T356, qc214_in_g(f(T356)))
P162_IN_GG(T254, f(T255)) → U3_GG(T254, T255, qc1_in_gg(f(T254), f(T255)))
P183_IN_G(f(T281)) → U9_G(T281, qc46_in_g(f(f(T281))))
P123_IN_G(f(f(T389))) → U21_G(T389, rc134_in_g(f(f(T389))))
P151_IN_GG(T303, f(T304)) → U14_GG(T303, T304, rc152_in_gg(T303, f(T304)))
R105_IN_G(f(f(T440))) → U27_G(T440, qc269_in_g(f(T440)))
P94_IN_G(f(f(T470))) → U33_G(T470, rc105_in_g(f(f(T470))))
R76_IN_G(f(f(T518))) → U39_G(T518, qc321_in_g(f(T518)))
U39_G(T518, qc321_out_g(f(T518))) → P103_IN_G(T518)
P65_IN_G(f(f(T548))) → U45_G(T548, rc76_in_g(f(f(T548))))
R47_IN_G(f(f(T596))) → U54_G(T596, qc373_in_g(f(T596)))
Q1_IN_GG(T614, f(f(T614))) → U75_GG(T614, rc24_in_g(T614))
P407_IN_G(f(f(T642))) → U61_G(T642, rc47_in_g(f(f(T642))))
Q1_IN_GG(T11, f(f(T11))) → U79_GG(T11, pc15_in_g(T11))
Q1_IN_GG(T682, f(f(T683))) → P443_IN_GG(T682, T683)
P443_IN_GG(T710, T711) → P454_IN_GG(T710, T711)
P454_IN_GG(T736, f(T737)) → U64_GG(T736, T737, qc1_in_gg(T736, f(T737)))
P443_IN_GG(T764, f(T765)) → U70_GG(T764, T765, rc444_in_gg(T764, f(T765)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P103_IN_G(x1)) = x1   
POL(P121_IN_G(x1)) = 1 + x1   
POL(P123_IN_G(x1)) = 1 + x1   
POL(P132_IN_G(x1)) = 1 + x1   
POL(P144_IN_GG(x1, x2)) = 1 + x2   
POL(P151_IN_GG(x1, x2)) = 1 + x2   
POL(P162_IN_GG(x1, x2)) = x2   
POL(P183_IN_G(x1)) = 1 + x1   
POL(P407_IN_G(x1)) = x1   
POL(P443_IN_GG(x1, x2)) = 1 + x2   
POL(P454_IN_GG(x1, x2)) = x2   
POL(P63_IN_G(x1)) = 1 + x1   
POL(P65_IN_G(x1)) = 1 + x1   
POL(P74_IN_G(x1)) = x1   
POL(P92_IN_G(x1)) = x1   
POL(P94_IN_G(x1)) = x1   
POL(Q16_IN_G(x1)) = x1   
POL(Q1_IN_GG(x1, x2)) = x2   
POL(Q46_IN_G(x1)) = x1   
POL(R105_IN_G(x1)) = x1   
POL(R134_IN_G(x1)) = 1 + x1   
POL(R36_IN_G(x1)) = x1   
POL(R47_IN_G(x1)) = x1   
POL(R76_IN_G(x1)) = x1   
POL(T175_IN_G(x1)) = 1 + x1   
POL(U100_g(x1, x2)) = 0   
POL(U101_g(x1, x2)) = 0   
POL(U102_g(x1, x2)) = 0   
POL(U103_g(x1, x2)) = 0   
POL(U104_g(x1, x2)) = 0   
POL(U105_g(x1, x2)) = 0   
POL(U106_g(x1, x2)) = 0   
POL(U107_g(x1, x2)) = 0   
POL(U108_g(x1, x2)) = 0   
POL(U109_g(x1, x2)) = 0   
POL(U110_g(x1, x2)) = 0   
POL(U111_g(x1, x2)) = 0   
POL(U112_g(x1, x2)) = 0   
POL(U113_g(x1, x2)) = 0   
POL(U114_g(x1, x2)) = 0   
POL(U115_g(x1, x2)) = 0   
POL(U116_g(x1, x2)) = 0   
POL(U117_g(x1, x2)) = 0   
POL(U118_g(x1, x2)) = 0   
POL(U119_g(x1, x2)) = 0   
POL(U120_g(x1, x2)) = 0   
POL(U121_g(x1, x2)) = 0   
POL(U122_g(x1, x2)) = 0   
POL(U123_g(x1, x2)) = 0   
POL(U124_g(x1, x2)) = 0   
POL(U125_g(x1, x2)) = 0   
POL(U126_g(x1, x2)) = 0   
POL(U127_g(x1, x2)) = 0   
POL(U128_g(x1, x2)) = 0   
POL(U129_gg(x1)) = 0   
POL(U130_gg(x1, x2, x3)) = 0   
POL(U131_gg(x1, x2, x3)) = 0   
POL(U132_gg(x1, x2)) = 0   
POL(U133_gg(x1, x2)) = 0   
POL(U134_gg(x1)) = 0   
POL(U135_gg(x1, x2, x3)) = 0   
POL(U136_gg(x1, x2, x3)) = 0   
POL(U137_g(x1, x2)) = 0   
POL(U138_g(x1, x2)) = 0   
POL(U139_g(x1, x2)) = 0   
POL(U140_g(x1, x2)) = 0   
POL(U141_g(x1, x2)) = 0   
POL(U142_g(x1, x2)) = 0   
POL(U143_g(x1, x2)) = 0   
POL(U144_g(x1, x2)) = 0   
POL(U145_g(x1, x2)) = 0   
POL(U146_g(x1, x2)) = 0   
POL(U147_g(x1, x2)) = 0   
POL(U148_gg(x1, x2, x3)) = 0   
POL(U149_gg(x1, x2)) = 0   
POL(U14_GG(x1, x2, x3)) = 1 + x2   
POL(U150_g(x1, x2)) = 0   
POL(U151_g(x1, x2)) = 0   
POL(U152_g(x1, x2)) = 0   
POL(U153_g(x1, x2)) = 0   
POL(U154_gg(x1, x2, x3)) = 0   
POL(U155_gg(x1, x2)) = 0   
POL(U18_G(x1, x2)) = x1   
POL(U21_G(x1, x2)) = 1 + x1   
POL(U24_G(x1, x2)) = 1 + x1   
POL(U27_G(x1, x2)) = 1 + x1   
POL(U30_G(x1, x2)) = 1 + x1   
POL(U33_G(x1, x2)) = 1 + x1   
POL(U36_G(x1, x2)) = x1   
POL(U39_G(x1, x2)) = 1 + x1   
POL(U3_GG(x1, x2, x3)) = x2   
POL(U42_G(x1, x2)) = x1   
POL(U45_G(x1, x2)) = x1   
POL(U48_G(x1, x2)) = x1   
POL(U51_G(x1, x2)) = x1   
POL(U54_G(x1, x2)) = x1   
POL(U58_G(x1, x2)) = 1 + x1   
POL(U5_GG(x1, x2)) = 1 + x1   
POL(U61_G(x1, x2)) = 1 + x1   
POL(U64_GG(x1, x2, x3)) = x2   
POL(U66_GG(x1, x2)) = 1 + x1   
POL(U70_GG(x1, x2, x3)) = 1 + x2   
POL(U73_GG(x1, x2)) = x1   
POL(U75_GG(x1, x2)) = x1   
POL(U77_GG(x1, x2)) = x1   
POL(U79_GG(x1, x2)) = x1   
POL(U83_g(x1, x2)) = 0   
POL(U84_gg(x1, x2)) = 0   
POL(U85_gg(x1, x2)) = 0   
POL(U86_gg(x1, x2, x3)) = 0   
POL(U87_gg(x1, x2, x3)) = 0   
POL(U88_gg(x1, x2, x3)) = 0   
POL(U89_gg(x1, x2)) = 0   
POL(U90_gg(x1, x2)) = 0   
POL(U91_g(x1, x2)) = 0   
POL(U92_g(x1, x2)) = 0   
POL(U93_g(x1, x2)) = 0   
POL(U94_g(x1, x2)) = 0   
POL(U95_gg(x1, x2, x3)) = 0   
POL(U96_gg(x1, x2, x3)) = 0   
POL(U97_gg(x1, x2, x3)) = 0   
POL(U98_g(x1, x2)) = 0   
POL(U99_g(x1, x2)) = 0   
POL(U9_G(x1, x2)) = 1 + x1   
POL(a) = 0   
POL(b) = 0   
POL(f(x1)) = 1 + x1   
POL(pc123_in_g(x1)) = 0   
POL(pc123_out_g(x1)) = 0   
POL(pc144_in_gg(x1, x2)) = 0   
POL(pc144_out_gg(x1, x2)) = 0   
POL(pc15_in_g(x1)) = 0   
POL(pc15_out_g(x1)) = 0   
POL(pc407_in_g(x1)) = 0   
POL(pc407_out_g(x1)) = 0   
POL(pc65_in_g(x1)) = 0   
POL(pc65_out_g(x1)) = 0   
POL(pc94_in_g(x1)) = 0   
POL(pc94_out_g(x1)) = 0   
POL(qc103_in_g(x1)) = 0   
POL(qc103_out_g(x1)) = 0   
POL(qc104_in_g(x1)) = 0   
POL(qc104_out_g(x1)) = 0   
POL(qc121_in_g(x1)) = 0   
POL(qc121_out_g(x1)) = 0   
POL(qc132_in_g(x1)) = 0   
POL(qc132_out_g(x1)) = 0   
POL(qc133_in_g(x1)) = 0   
POL(qc133_out_g(x1)) = 0   
POL(qc151_in_gg(x1, x2)) = 0   
POL(qc151_out_gg(x1, x2)) = 0   
POL(qc162_in_gg(x1, x2)) = 0   
POL(qc162_out_gg(x1, x2)) = 0   
POL(qc16_in_g(x1)) = 0   
POL(qc16_out_g(x1)) = 0   
POL(qc183_in_g(x1)) = 0   
POL(qc183_out_g(x1)) = 0   
POL(qc1_in_gg(x1, x2)) = 0   
POL(qc1_out_gg(x1, x2)) = 0   
POL(qc214_in_g(x1)) = 0   
POL(qc214_out_g(x1)) = 0   
POL(qc269_in_g(x1)) = 0   
POL(qc269_out_g(x1)) = 0   
POL(qc321_in_g(x1)) = 0   
POL(qc321_out_g(x1)) = 0   
POL(qc373_in_g(x1)) = 0   
POL(qc373_out_g(x1)) = 0   
POL(qc443_in_gg(x1, x2)) = 0   
POL(qc443_out_gg(x1, x2)) = 0   
POL(qc454_in_gg(x1, x2)) = 0   
POL(qc454_out_gg(x1, x2)) = 0   
POL(qc46_in_g(x1)) = 0   
POL(qc46_out_g(x1)) = 0   
POL(qc63_in_g(x1)) = 0   
POL(qc63_out_g(x1)) = 0   
POL(qc74_in_g(x1)) = 0   
POL(qc74_out_g(x1)) = 0   
POL(qc75_in_g(x1)) = 0   
POL(qc75_out_g(x1)) = 0   
POL(qc92_in_g(x1)) = 0   
POL(qc92_out_g(x1)) = 0   
POL(rc105_in_g(x1)) = 0   
POL(rc105_out_g(x1)) = 0   
POL(rc122_in_g(x1)) = 0   
POL(rc122_out_g(x1)) = 0   
POL(rc134_in_g(x1)) = 0   
POL(rc134_out_g(x1)) = 0   
POL(rc152_in_gg(x1, x2)) = 0   
POL(rc152_out_gg(x1, x2)) = 0   
POL(rc24_in_g(x1)) = 0   
POL(rc24_out_g(x1)) = 0   
POL(rc36_in_g(x1)) = 0   
POL(rc36_out_g(x1)) = 0   
POL(rc444_in_gg(x1, x2)) = 0   
POL(rc444_out_gg(x1, x2)) = 0   
POL(rc47_in_g(x1)) = 0   
POL(rc47_out_g(x1)) = 0   
POL(rc64_in_g(x1)) = 0   
POL(rc64_out_g(x1)) = 0   
POL(rc76_in_g(x1)) = 0   
POL(rc76_out_g(x1)) = 0   
POL(rc93_in_g(x1)) = 0   
POL(rc93_out_g(x1)) = 0   
POL(tc175_in_g(x1)) = 0   
POL(tc175_out_g(x1)) = 0   

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

Q16_IN_G(f(T656)) → P407_IN_G(f(T656))
P407_IN_G(f(T628)) → R47_IN_G(f(T628))
P94_IN_G(f(T456)) → R105_IN_G(f(T456))
P123_IN_G(f(T375)) → R134_IN_G(f(T375))
P162_IN_GG(T228, T229) → Q1_IN_GG(f(T228), T229)
U73_GG(T36, qc16_out_g(T36)) → R36_IN_G(T36)
R36_IN_G(T51) → Q46_IN_G(T51)
P92_IN_G(T127) → P103_IN_G(T127)
P121_IN_G(T165) → P132_IN_G(T165)
P132_IN_G(T165) → U24_G(T165, qc133_in_g(T165))
U24_G(T165, qc133_out_g(T165)) → R134_IN_G(T165)
U18_G(T356, qc214_out_g(f(T356))) → P162_IN_GG(f(f(f(f(f(f(f(T356))))))), T356)
U3_GG(T254, T255, qc1_out_gg(f(T254), f(T255))) → P162_IN_GG(T254, T255)
P162_IN_GG(T260, f(T260)) → U5_GG(T260, qc1_in_gg(f(T260), f(T260)))
U5_GG(T260, qc1_out_gg(f(T260), f(T260))) → T175_IN_G(T260)
T175_IN_G(T270) → P183_IN_G(T270)
P183_IN_G(T270) → Q46_IN_G(f(T270))
U9_G(T281, qc46_out_g(f(f(T281)))) → P183_IN_G(T281)
P121_IN_G(T151) → U30_G(T151, rc122_in_g(T151))
U30_G(T151, rc122_out_g(T151)) → P123_IN_G(T151)
U21_G(T389, rc134_out_g(f(f(T389)))) → P151_IN_GG(f(f(f(f(f(f(f(T389))))))), T389)
P151_IN_GG(T285, T285) → T175_IN_G(T285)
U14_GG(T303, T304, rc152_out_gg(T303, f(T304))) → P151_IN_GG(T303, T304)
P103_IN_G(T127) → U36_G(T127, qc104_in_g(T127))
U36_G(T127, qc104_out_g(T127)) → R105_IN_G(T127)
U27_G(T440, qc269_out_g(f(T440))) → P132_IN_G(T440)
P92_IN_G(T113) → U42_G(T113, rc93_in_g(T113))
U42_G(T113, rc93_out_g(T113)) → P94_IN_G(T113)
U33_G(T470, rc105_out_g(f(f(T470)))) → P121_IN_G(T470)
P74_IN_G(T89) → U48_G(T89, qc75_in_g(T89))
U48_G(T89, qc75_out_g(T89)) → R76_IN_G(T89)
P63_IN_G(T75) → U58_G(T75, rc64_in_g(T75))
U58_G(T75, rc64_out_g(T75)) → P65_IN_G(T75)
U45_G(T548, rc76_out_g(f(f(T548)))) → P92_IN_G(T548)
R36_IN_G(T51) → U51_G(T51, qc46_in_g(T51))
U51_G(T51, qc46_out_g(T51)) → R47_IN_G(T51)
U54_G(T596, qc373_out_g(f(T596))) → P74_IN_G(T596)
R47_IN_G(f(T601)) → T175_IN_G(T601)
U75_GG(T614, rc24_out_g(T614)) → R36_IN_G(T614)
U75_GG(T614, rc24_out_g(T614)) → U77_GG(T614, rc36_in_g(T614))
U77_GG(T614, rc36_out_g(T614)) → P407_IN_G(T614)
U61_G(T642, rc47_out_g(f(f(T642)))) → P63_IN_G(T642)
U79_GG(T11, pc15_out_g(T11)) → Q16_IN_G(T11)
P454_IN_GG(T710, T711) → Q1_IN_GG(T710, T711)
U64_GG(T736, T737, qc1_out_gg(T736, f(T737))) → P454_IN_GG(T736, T737)
P454_IN_GG(f(T742), f(T742)) → U66_GG(T742, qc1_in_gg(f(T742), f(T742)))
U66_GG(T742, qc1_out_gg(f(T742), f(T742))) → T175_IN_G(T742)
P443_IN_GG(f(T746), T746) → T175_IN_G(T746)
U70_GG(T764, T765, rc444_out_gg(T764, f(T765))) → P443_IN_GG(T764, T765)
P144_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(f(z0)))))))), z0)
P144_IN_GG(f(f(f(f(f(f(f(z0))))))), z0) → P151_IN_GG(f(f(f(f(f(f(f(z0))))))), z0)

The TRS R consists of the following rules:

qc16_in_g(f(T656)) → U83_g(T656, pc407_in_g(f(T656)))
pc407_in_g(f(f(T642))) → U127_g(T642, rc47_in_g(f(f(T642))))
rc47_in_g(f(f(T596))) → U122_g(T596, qc373_in_g(f(T596)))
qc373_in_g(f(f(T579))) → U153_g(T579, pc65_in_g(f(T579)))
pc65_in_g(f(f(T548))) → U116_g(T548, rc76_in_g(f(f(T548))))
rc76_in_g(f(f(T518))) → U112_g(T518, qc321_in_g(f(T518)))
qc321_in_g(f(f(T501))) → U152_g(T501, pc94_in_g(f(T501)))
pc94_in_g(f(f(T470))) → U108_g(T470, rc105_in_g(f(f(T470))))
rc105_in_g(f(f(T440))) → U104_g(T440, qc269_in_g(f(T440)))
qc269_in_g(f(f(T423))) → U151_g(T423, pc123_in_g(f(T423)))
pc123_in_g(f(f(T389))) → U100_g(T389, rc134_in_g(f(f(T389))))
rc134_in_g(f(f(T356))) → U98_g(T356, qc214_in_g(f(T356)))
qc214_in_g(f(f(T336))) → U150_g(T336, pc144_in_gg(f(f(f(f(f(f(f(f(T336)))))))), T336))
pc144_in_gg(T200, T201) → U97_gg(T200, T201, qc151_in_gg(T200, T201))
qc151_in_gg(T303, f(T304)) → U95_gg(T303, T304, rc152_in_gg(T303, f(T304)))
rc152_in_gg(T228, T229) → U148_gg(T228, T229, qc162_in_gg(T228, T229))
qc162_in_gg(T254, f(T255)) → U87_gg(T254, T255, qc1_in_gg(f(T254), f(T255)))
qc1_in_gg(a, b) → qc1_out_gg(a, b)
qc1_in_gg(T11, f(f(T11))) → U84_gg(T11, pc15_in_g(T11))
pc15_in_g(T614) → U137_g(T614, rc24_in_g(T614))
rc24_in_g(T36) → U140_g(T36, qc16_in_g(T36))
U140_g(T36, qc16_out_g(T36)) → U141_g(T36, rc36_in_g(T36))
rc36_in_g(T51) → U120_g(T51, qc46_in_g(T51))
qc46_in_g(f(f(T75))) → U91_g(T75, qc63_in_g(T75))
qc63_in_g(T75) → U125_g(T75, rc64_in_g(T75))
rc64_in_g(T89) → U142_g(T89, qc74_in_g(T89))
qc74_in_g(T89) → U118_g(T89, qc75_in_g(T89))
qc75_in_g(f(f(T113))) → U143_g(T113, qc92_in_g(T113))
qc92_in_g(T113) → U114_g(T113, rc93_in_g(T113))
rc93_in_g(T127) → U144_g(T127, qc103_in_g(T127))
qc103_in_g(T127) → U110_g(T127, qc104_in_g(T127))
qc104_in_g(f(f(T151))) → U145_g(T151, qc121_in_g(T151))
qc121_in_g(T151) → U106_g(T151, rc122_in_g(T151))
rc122_in_g(T165) → U146_g(T165, qc132_in_g(T165))
qc132_in_g(T165) → U102_g(T165, qc133_in_g(T165))
qc133_in_g(f(f(T179))) → U147_g(T179, pc144_in_gg(f(f(f(f(f(f(f(T179))))))), T179))
U147_g(T179, pc144_out_gg(f(f(f(f(f(f(f(T179))))))), T179)) → qc133_out_g(f(f(T179)))
U102_g(T165, qc133_out_g(T165)) → U103_g(T165, rc134_in_g(T165))
U103_g(T165, rc134_out_g(T165)) → qc132_out_g(T165)
U146_g(T165, qc132_out_g(T165)) → rc122_out_g(T165)
U106_g(T151, rc122_out_g(T151)) → U107_g(T151, pc123_in_g(T151))
U107_g(T151, pc123_out_g(T151)) → qc121_out_g(T151)
U145_g(T151, qc121_out_g(T151)) → qc104_out_g(f(f(T151)))
U110_g(T127, qc104_out_g(T127)) → U111_g(T127, rc105_in_g(T127))
U111_g(T127, rc105_out_g(T127)) → qc103_out_g(T127)
U144_g(T127, qc103_out_g(T127)) → rc93_out_g(T127)
U114_g(T113, rc93_out_g(T113)) → U115_g(T113, pc94_in_g(T113))
U115_g(T113, pc94_out_g(T113)) → qc92_out_g(T113)
U143_g(T113, qc92_out_g(T113)) → qc75_out_g(f(f(T113)))
U118_g(T89, qc75_out_g(T89)) → U119_g(T89, rc76_in_g(T89))
U119_g(T89, rc76_out_g(T89)) → qc74_out_g(T89)
U142_g(T89, qc74_out_g(T89)) → rc64_out_g(T89)
U125_g(T75, rc64_out_g(T75)) → U126_g(T75, pc65_in_g(T75))
U126_g(T75, pc65_out_g(T75)) → qc63_out_g(T75)
U91_g(T75, qc63_out_g(T75)) → qc46_out_g(f(f(T75)))
U120_g(T51, qc46_out_g(T51)) → U121_g(T51, rc47_in_g(T51))
rc47_in_g(f(T601)) → U124_g(T601, tc175_in_g(T601))
tc175_in_g(T270) → U94_g(T270, qc183_in_g(T270))
qc183_in_g(f(T281)) → U92_g(T281, qc46_in_g(f(f(T281))))
U92_g(T281, qc46_out_g(f(f(T281)))) → U93_g(T281, qc183_in_g(T281))
U93_g(T281, qc183_out_g(T281)) → qc183_out_g(f(T281))
U94_g(T270, qc183_out_g(T270)) → tc175_out_g(T270)
U124_g(T601, tc175_out_g(T601)) → rc47_out_g(f(T601))
U121_g(T51, rc47_out_g(T51)) → rc36_out_g(T51)
U141_g(T36, rc36_out_g(T36)) → rc24_out_g(T36)
U137_g(T614, rc24_out_g(T614)) → U138_g(T614, rc36_in_g(T614))
U138_g(T614, rc36_out_g(T614)) → U139_g(T614, pc407_in_g(T614))
U139_g(T614, pc407_out_g(T614)) → pc15_out_g(T614)
U84_gg(T11, pc15_out_g(T11)) → U85_gg(T11, qc16_in_g(T11))
U85_gg(T11, qc16_out_g(T11)) → qc1_out_gg(T11, f(f(T11)))
qc1_in_gg(T682, f(f(T683))) → U86_gg(T682, T683, qc443_in_gg(T682, T683))
qc443_in_gg(a, b) → U134_gg(rc444_in_gg(a, b))
rc444_in_gg(T710, T711) → U154_gg(T710, T711, qc454_in_gg(T710, T711))
qc454_in_gg(a, b) → U129_gg(qc1_in_gg(a, b))
U129_gg(qc1_out_gg(a, b)) → qc454_out_gg(a, b)
qc454_in_gg(T736, f(T737)) → U130_gg(T736, T737, qc1_in_gg(T736, f(T737)))
U130_gg(T736, T737, qc1_out_gg(T736, f(T737))) → U131_gg(T736, T737, qc454_in_gg(T736, T737))
qc454_in_gg(f(T742), f(T742)) → U132_gg(T742, qc1_in_gg(f(T742), f(T742)))
U132_gg(T742, qc1_out_gg(f(T742), f(T742))) → U133_gg(T742, tc175_in_g(T742))
U133_gg(T742, tc175_out_g(T742)) → qc454_out_gg(f(T742), f(T742))
U131_gg(T736, T737, qc454_out_gg(T736, T737)) → qc454_out_gg(T736, f(T737))
U154_gg(T710, T711, qc454_out_gg(T710, T711)) → rc444_out_gg(T710, T711)
rc444_in_gg(f(T746), T746) → U155_gg(T746, tc175_in_g(T746))
U155_gg(T746, tc175_out_g(T746)) → rc444_out_gg(f(T746), T746)
U134_gg(rc444_out_gg(a, b)) → qc443_out_gg(a, b)
qc443_in_gg(T764, f(T765)) → U135_gg(T764, T765, rc444_in_gg(T764, f(T765)))
U135_gg(T764, T765, rc444_out_gg(T764, f(T765))) → U136_gg(T764, T765, qc443_in_gg(T764, T765))
U136_gg(T764, T765, qc443_out_gg(T764, T765)) → qc443_out_gg(T764, f(T765))
U86_gg(T682, T683, qc443_out_gg(T682, T683)) → qc1_out_gg(T682, f(f(T683)))
U87_gg(T254, T255, qc1_out_gg(f(T254), f(T255))) → U88_gg(T254, T255, qc162_in_gg(T254, T255))
qc162_in_gg(T260, f(T260)) → U89_gg(T260, qc1_in_gg(f(T260), f(T260)))
U89_gg(T260, qc1_out_gg(f(T260), f(T260))) → U90_gg(T260, tc175_in_g(T260))
U90_gg(T260, tc175_out_g(T260)) → qc162_out_gg(T260, f(T260))
U88_gg(T254, T255, qc162_out_gg(T254, T255)) → qc162_out_gg(T254, f(T255))
U148_gg(T228, T229, qc162_out_gg(T228, T229)) → rc152_out_gg(T228, T229)
rc152_in_gg(T285, T285) → U149_gg(T285, tc175_in_g(T285))
U149_gg(T285, tc175_out_g(T285)) → rc152_out_gg(T285, T285)
U95_gg(T303, T304, rc152_out_gg(T303, f(T304))) → U96_gg(T303, T304, qc151_in_gg(T303, T304))
U96_gg(T303, T304, qc151_out_gg(T303, T304)) → qc151_out_gg(T303, f(T304))
U97_gg(T200, T201, qc151_out_gg(T200, T201)) → pc144_out_gg(T200, T201)
U150_g(T336, pc144_out_gg(f(f(f(f(f(f(f(f(T336)))))))), T336)) → qc214_out_g(f(f(T336)))
U98_g(T356, qc214_out_g(f(T356))) → U99_g(T356, qc162_in_gg(f(f(f(f(f(f(f(T356))))))), T356))
U99_g(T356, qc162_out_gg(f(f(f(f(f(f(f(T356))))))), T356)) → rc134_out_g(f(f(T356)))
U100_g(T389, rc134_out_g(f(f(T389)))) → U101_g(T389, qc151_in_gg(f(f(f(f(f(f(f(T389))))))), T389))
U101_g(T389, qc151_out_gg(f(f(f(f(f(f(f(T389))))))), T389)) → pc123_out_g(f(f(T389)))
U151_g(T423, pc123_out_g(f(T423))) → qc269_out_g(f(f(T423)))
U104_g(T440, qc269_out_g(f(T440))) → U105_g(T440, qc132_in_g(T440))
U105_g(T440, qc132_out_g(T440)) → rc105_out_g(f(f(T440)))
U108_g(T470, rc105_out_g(f(f(T470)))) → U109_g(T470, qc121_in_g(T470))
U109_g(T470, qc121_out_g(T470)) → pc94_out_g(f(f(T470)))
U152_g(T501, pc94_out_g(f(T501))) → qc321_out_g(f(f(T501)))
U112_g(T518, qc321_out_g(f(T518))) → U113_g(T518, qc103_in_g(T518))
U113_g(T518, qc103_out_g(T518)) → rc76_out_g(f(f(T518)))
U116_g(T548, rc76_out_g(f(f(T548)))) → U117_g(T548, qc92_in_g(T548))
U117_g(T548, qc92_out_g(T548)) → pc65_out_g(f(f(T548)))
U153_g(T579, pc65_out_g(f(T579))) → qc373_out_g(f(f(T579)))
U122_g(T596, qc373_out_g(f(T596))) → U123_g(T596, qc74_in_g(T596))
U123_g(T596, qc74_out_g(T596)) → rc47_out_g(f(f(T596)))
U127_g(T642, rc47_out_g(f(f(T642)))) → U128_g(T642, qc63_in_g(T642))
U128_g(T642, qc63_out_g(T642)) → pc407_out_g(f(f(T642)))
U83_g(T656, pc407_out_g(f(T656))) → qc16_out_g(f(T656))

The set Q consists of the following terms:

qc16_in_g(x0)
pc407_in_g(x0)
rc47_in_g(x0)
qc373_in_g(x0)
pc65_in_g(x0)
rc76_in_g(x0)
qc321_in_g(x0)
pc94_in_g(x0)
rc105_in_g(x0)
qc269_in_g(x0)
pc123_in_g(x0)
rc134_in_g(x0)
qc214_in_g(x0)
pc144_in_gg(x0, x1)
qc151_in_gg(x0, x1)
rc152_in_gg(x0, x1)
qc162_in_gg(x0, x1)
qc1_in_gg(x0, x1)
pc15_in_g(x0)
rc24_in_g(x0)
U140_g(x0, x1)
rc36_in_g(x0)
qc46_in_g(x0)
qc63_in_g(x0)
rc64_in_g(x0)
qc74_in_g(x0)
qc75_in_g(x0)
qc92_in_g(x0)
rc93_in_g(x0)
qc103_in_g(x0)
qc104_in_g(x0)
qc121_in_g(x0)
rc122_in_g(x0)
qc132_in_g(x0)
qc133_in_g(x0)
U147_g(x0, x1)
U102_g(x0, x1)
U103_g(x0, x1)
U146_g(x0, x1)
U106_g(x0, x1)
U107_g(x0, x1)
U145_g(x0, x1)
U110_g(x0, x1)
U111_g(x0, x1)
U144_g(x0, x1)
U114_g(x0, x1)
U115_g(x0, x1)
U143_g(x0, x1)
U118_g(x0, x1)
U119_g(x0, x1)
U142_g(x0, x1)
U125_g(x0, x1)
U126_g(x0, x1)
U91_g(x0, x1)
U120_g(x0, x1)
tc175_in_g(x0)
qc183_in_g(x0)
U92_g(x0, x1)
U93_g(x0, x1)
U94_g(x0, x1)
U124_g(x0, x1)
U121_g(x0, x1)
U141_g(x0, x1)
U137_g(x0, x1)
U138_g(x0, x1)
U139_g(x0, x1)
U84_gg(x0, x1)
U85_gg(x0, x1)
qc443_in_gg(x0, x1)
rc444_in_gg(x0, x1)
qc454_in_gg(x0, x1)
U129_gg(x0)
U130_gg(x0, x1, x2)
U132_gg(x0, x1)
U133_gg(x0, x1)
U131_gg(x0, x1, x2)
U154_gg(x0, x1, x2)
U155_gg(x0, x1)
U134_gg(x0)
U135_gg(x0, x1, x2)
U136_gg(x0, x1, x2)
U86_gg(x0, x1, x2)
U87_gg(x0, x1, x2)
U89_gg(x0, x1)
U90_gg(x0, x1)
U88_gg(x0, x1, x2)
U148_gg(x0, x1, x2)
U149_gg(x0, x1)
U95_gg(x0, x1, x2)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)
U150_g(x0, x1)
U98_g(x0, x1)
U99_g(x0, x1)
U100_g(x0, x1)
U101_g(x0, x1)
U151_g(x0, x1)
U104_g(x0, x1)
U105_g(x0, x1)
U108_g(x0, x1)
U109_g(x0, x1)
U152_g(x0, x1)
U112_g(x0, x1)
U113_g(x0, x1)
U116_g(x0, x1)
U117_g(x0, x1)
U153_g(x0, x1)
U122_g(x0, x1)
U123_g(x0, x1)
U127_g(x0, x1)
U128_g(x0, x1)
U83_g(x0, x1)

We have to consider all (P,Q,R)-chains.

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 51 less nodes.

(14) TRUE