(0) Obligation:

Clauses:

goal(Name, Code) :- ','(eq(Name, .(First, Others)), ','(reduce(Others, s(0), First, Reduced), eq(Code, Reduced))).
reduce(X1, s(s(s(s(0)))), X2, []) :- !.
reduce([], X3, X4, []) :- !.
reduce(.(Current, Others), Count, Current, Code) :- ','(vowel_h_w_y(Current), ','(!, reduce(Others, Count, Current, Code))).
reduce(.(Letter, Others), Count, Letter, Code) :- ','(!, reduce(Others, Count, Letter, Code)).
reduce(.(Current, Others), Count, X5, .(Current, Code)) :- reduce(Others, s(Count), Current, Code).
vowel_h_w_y(97).
vowel_h_w_y(101).
vowel_h_w_y(105).
vowel_h_w_y(111).
vowel_h_w_y(117).
vowel_h_w_y(104).
vowel_h_w_y(119).
vowel_h_w_y(121).
eq(X, X).

Queries:

goal(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

reduce7([], T10, []).
reduce7(.(97, T12), 97, X29) :- reduce7(T12, 97, X29).
reduce7(.(101, T12), 101, X29) :- reduce7(T12, 101, X29).
reduce7(.(105, T12), 105, X29) :- reduce7(T12, 105, X29).
reduce7(.(111, T12), 111, X29) :- reduce7(T12, 111, X29).
reduce7(.(117, T12), 117, X29) :- reduce7(T12, 117, X29).
reduce7(.(104, T12), 104, X29) :- reduce7(T12, 104, X29).
reduce7(.(119, T12), 119, X29) :- reduce7(T12, 119, X29).
reduce7(.(121, T12), 121, X29) :- reduce7(T12, 121, X29).
reduce7(.(T13, T14), T13, X38) :- reduce7(T14, T13, X38).
reduce7(.(T15, T16), T15, X47) :- reduce7(T16, T15, X47).
reduce7(.(T20, []), T19, .(T20, [])).
reduce7(.(97, .(97, T22)), T19, .(97, X73)) :- reduce50(T22, 97, X73).
reduce7(.(101, .(101, T22)), T19, .(101, X73)) :- reduce50(T22, 101, X73).
reduce7(.(105, .(105, T22)), T19, .(105, X73)) :- reduce50(T22, 105, X73).
reduce7(.(111, .(111, T22)), T19, .(111, X73)) :- reduce50(T22, 111, X73).
reduce7(.(117, .(117, T22)), T19, .(117, X73)) :- reduce50(T22, 117, X73).
reduce7(.(104, .(104, T22)), T19, .(104, X73)) :- reduce50(T22, 104, X73).
reduce7(.(119, .(119, T22)), T19, .(119, X73)) :- reduce50(T22, 119, X73).
reduce7(.(121, .(121, T22)), T19, .(121, X73)) :- reduce50(T22, 121, X73).
reduce7(.(T23, .(T23, T24)), T19, .(T23, X130)) :- reduce50(T24, T23, X130).
reduce7(.(T25, .(T25, T26)), T19, .(T25, X145)) :- reduce50(T26, T25, X145).
reduce7(.(T29, .(T30, [])), T19, .(T29, .(T30, []))).
reduce7(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) :- reduce130(T32, 97, X177).
reduce7(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) :- reduce130(T32, 101, X177).
reduce7(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) :- reduce130(T32, 105, X177).
reduce7(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) :- reduce130(T32, 111, X177).
reduce7(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) :- reduce130(T32, 117, X177).
reduce7(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) :- reduce130(T32, 104, X177).
reduce7(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) :- reduce130(T32, 119, X177).
reduce7(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) :- reduce130(T32, 121, X177).
reduce7(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) :- reduce130(T34, T33, X234).
reduce7(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) :- reduce130(T36, T35, X249).
reduce7(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))).
reduce50([], T20, []).
reduce50(.(97, T22), 97, X73) :- reduce50(T22, 97, X73).
reduce50(.(101, T22), 101, X73) :- reduce50(T22, 101, X73).
reduce50(.(105, T22), 105, X73) :- reduce50(T22, 105, X73).
reduce50(.(111, T22), 111, X73) :- reduce50(T22, 111, X73).
reduce50(.(117, T22), 117, X73) :- reduce50(T22, 117, X73).
reduce50(.(104, T22), 104, X73) :- reduce50(T22, 104, X73).
reduce50(.(119, T22), 119, X73) :- reduce50(T22, 119, X73).
reduce50(.(121, T22), 121, X73) :- reduce50(T22, 121, X73).
reduce50(.(T23, T24), T23, X130) :- reduce50(T24, T23, X130).
reduce50(.(T25, T26), T25, X145) :- reduce50(T26, T25, X145).
reduce50(.(T30, []), T29, .(T30, [])).
reduce50(.(97, .(97, T32)), T29, .(97, X177)) :- reduce130(T32, 97, X177).
reduce50(.(101, .(101, T32)), T29, .(101, X177)) :- reduce130(T32, 101, X177).
reduce50(.(105, .(105, T32)), T29, .(105, X177)) :- reduce130(T32, 105, X177).
reduce50(.(111, .(111, T32)), T29, .(111, X177)) :- reduce130(T32, 111, X177).
reduce50(.(117, .(117, T32)), T29, .(117, X177)) :- reduce130(T32, 117, X177).
reduce50(.(104, .(104, T32)), T29, .(104, X177)) :- reduce130(T32, 104, X177).
reduce50(.(119, .(119, T32)), T29, .(119, X177)) :- reduce130(T32, 119, X177).
reduce50(.(121, .(121, T32)), T29, .(121, X177)) :- reduce130(T32, 121, X177).
reduce50(.(T33, .(T33, T34)), T29, .(T33, X234)) :- reduce130(T34, T33, X234).
reduce50(.(T35, .(T35, T36)), T29, .(T35, X249)) :- reduce130(T36, T35, X249).
reduce50(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))).
reduce130([], T30, []).
reduce130(.(97, T32), 97, X177) :- reduce130(T32, 97, X177).
reduce130(.(101, T32), 101, X177) :- reduce130(T32, 101, X177).
reduce130(.(105, T32), 105, X177) :- reduce130(T32, 105, X177).
reduce130(.(111, T32), 111, X177) :- reduce130(T32, 111, X177).
reduce130(.(117, T32), 117, X177) :- reduce130(T32, 117, X177).
reduce130(.(104, T32), 104, X177) :- reduce130(T32, 104, X177).
reduce130(.(119, T32), 119, X177) :- reduce130(T32, 119, X177).
reduce130(.(121, T32), 121, X177) :- reduce130(T32, 121, X177).
reduce130(.(T33, T34), T33, X234) :- reduce130(T34, T33, X234).
reduce130(.(T35, T36), T35, X249) :- reduce130(T36, T35, X249).
reduce130(.(T41, T40), T39, .(T41, [])).
goal1(.(T7, T8), T5) :- reduce7(T8, T7, X12).
goal1(.(T7, T8), T42) :- reduce7(T8, T7, T42).

Queries:

goal1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
goal1_in: (b,f)
reduce7_in: (b,b,f)
reduce50_in: (b,b,f)
reduce130_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_GA(.(T7, T8), T5) → U61_GA(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
GOAL1_IN_GA(.(T7, T8), T5) → REDUCE7_IN_GGA(T8, T7, X12)
REDUCE7_IN_GGA(.(97, T12), 97, X29) → U1_GGA(T12, X29, reduce7_in_gga(T12, 97, X29))
REDUCE7_IN_GGA(.(97, T12), 97, X29) → REDUCE7_IN_GGA(T12, 97, X29)
REDUCE7_IN_GGA(.(101, T12), 101, X29) → U2_GGA(T12, X29, reduce7_in_gga(T12, 101, X29))
REDUCE7_IN_GGA(.(101, T12), 101, X29) → REDUCE7_IN_GGA(T12, 101, X29)
REDUCE7_IN_GGA(.(105, T12), 105, X29) → U3_GGA(T12, X29, reduce7_in_gga(T12, 105, X29))
REDUCE7_IN_GGA(.(105, T12), 105, X29) → REDUCE7_IN_GGA(T12, 105, X29)
REDUCE7_IN_GGA(.(111, T12), 111, X29) → U4_GGA(T12, X29, reduce7_in_gga(T12, 111, X29))
REDUCE7_IN_GGA(.(111, T12), 111, X29) → REDUCE7_IN_GGA(T12, 111, X29)
REDUCE7_IN_GGA(.(117, T12), 117, X29) → U5_GGA(T12, X29, reduce7_in_gga(T12, 117, X29))
REDUCE7_IN_GGA(.(117, T12), 117, X29) → REDUCE7_IN_GGA(T12, 117, X29)
REDUCE7_IN_GGA(.(104, T12), 104, X29) → U6_GGA(T12, X29, reduce7_in_gga(T12, 104, X29))
REDUCE7_IN_GGA(.(104, T12), 104, X29) → REDUCE7_IN_GGA(T12, 104, X29)
REDUCE7_IN_GGA(.(119, T12), 119, X29) → U7_GGA(T12, X29, reduce7_in_gga(T12, 119, X29))
REDUCE7_IN_GGA(.(119, T12), 119, X29) → REDUCE7_IN_GGA(T12, 119, X29)
REDUCE7_IN_GGA(.(121, T12), 121, X29) → U8_GGA(T12, X29, reduce7_in_gga(T12, 121, X29))
REDUCE7_IN_GGA(.(121, T12), 121, X29) → REDUCE7_IN_GGA(T12, 121, X29)
REDUCE7_IN_GGA(.(T13, T14), T13, X38) → U9_GGA(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
REDUCE7_IN_GGA(.(T13, T14), T13, X38) → REDUCE7_IN_GGA(T14, T13, X38)
REDUCE7_IN_GGA(.(T15, T16), T15, X47) → U10_GGA(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
REDUCE7_IN_GGA(.(97, .(97, T22)), T19, .(97, X73)) → U11_GGA(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
REDUCE7_IN_GGA(.(97, .(97, T22)), T19, .(97, X73)) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(97, T22), 97, X73) → U31_GGA(T22, X73, reduce50_in_gga(T22, 97, X73))
REDUCE50_IN_GGA(.(97, T22), 97, X73) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(101, T22), 101, X73) → U32_GGA(T22, X73, reduce50_in_gga(T22, 101, X73))
REDUCE50_IN_GGA(.(101, T22), 101, X73) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE50_IN_GGA(.(105, T22), 105, X73) → U33_GGA(T22, X73, reduce50_in_gga(T22, 105, X73))
REDUCE50_IN_GGA(.(105, T22), 105, X73) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE50_IN_GGA(.(111, T22), 111, X73) → U34_GGA(T22, X73, reduce50_in_gga(T22, 111, X73))
REDUCE50_IN_GGA(.(111, T22), 111, X73) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE50_IN_GGA(.(117, T22), 117, X73) → U35_GGA(T22, X73, reduce50_in_gga(T22, 117, X73))
REDUCE50_IN_GGA(.(117, T22), 117, X73) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE50_IN_GGA(.(104, T22), 104, X73) → U36_GGA(T22, X73, reduce50_in_gga(T22, 104, X73))
REDUCE50_IN_GGA(.(104, T22), 104, X73) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE50_IN_GGA(.(119, T22), 119, X73) → U37_GGA(T22, X73, reduce50_in_gga(T22, 119, X73))
REDUCE50_IN_GGA(.(119, T22), 119, X73) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE50_IN_GGA(.(121, T22), 121, X73) → U38_GGA(T22, X73, reduce50_in_gga(T22, 121, X73))
REDUCE50_IN_GGA(.(121, T22), 121, X73) → REDUCE50_IN_GGA(T22, 121, X73)
REDUCE50_IN_GGA(.(T23, T24), T23, X130) → U39_GGA(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
REDUCE50_IN_GGA(.(T23, T24), T23, X130) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE50_IN_GGA(.(T25, T26), T25, X145) → U40_GGA(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
REDUCE50_IN_GGA(.(97, .(97, T32)), T29, .(97, X177)) → U41_GGA(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
REDUCE50_IN_GGA(.(97, .(97, T32)), T29, .(97, X177)) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(97, T32), 97, X177) → U51_GGA(T32, X177, reduce130_in_gga(T32, 97, X177))
REDUCE130_IN_GGA(.(97, T32), 97, X177) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(101, T32), 101, X177) → U52_GGA(T32, X177, reduce130_in_gga(T32, 101, X177))
REDUCE130_IN_GGA(.(101, T32), 101, X177) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE130_IN_GGA(.(105, T32), 105, X177) → U53_GGA(T32, X177, reduce130_in_gga(T32, 105, X177))
REDUCE130_IN_GGA(.(105, T32), 105, X177) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE130_IN_GGA(.(111, T32), 111, X177) → U54_GGA(T32, X177, reduce130_in_gga(T32, 111, X177))
REDUCE130_IN_GGA(.(111, T32), 111, X177) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE130_IN_GGA(.(117, T32), 117, X177) → U55_GGA(T32, X177, reduce130_in_gga(T32, 117, X177))
REDUCE130_IN_GGA(.(117, T32), 117, X177) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE130_IN_GGA(.(104, T32), 104, X177) → U56_GGA(T32, X177, reduce130_in_gga(T32, 104, X177))
REDUCE130_IN_GGA(.(104, T32), 104, X177) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE130_IN_GGA(.(119, T32), 119, X177) → U57_GGA(T32, X177, reduce130_in_gga(T32, 119, X177))
REDUCE130_IN_GGA(.(119, T32), 119, X177) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE130_IN_GGA(.(121, T32), 121, X177) → U58_GGA(T32, X177, reduce130_in_gga(T32, 121, X177))
REDUCE130_IN_GGA(.(121, T32), 121, X177) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE130_IN_GGA(.(T33, T34), T33, X234) → U59_GGA(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
REDUCE130_IN_GGA(.(T33, T34), T33, X234) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE130_IN_GGA(.(T35, T36), T35, X249) → U60_GGA(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
REDUCE50_IN_GGA(.(101, .(101, T32)), T29, .(101, X177)) → U42_GGA(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
REDUCE50_IN_GGA(.(101, .(101, T32)), T29, .(101, X177)) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE50_IN_GGA(.(105, .(105, T32)), T29, .(105, X177)) → U43_GGA(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
REDUCE50_IN_GGA(.(105, .(105, T32)), T29, .(105, X177)) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE50_IN_GGA(.(111, .(111, T32)), T29, .(111, X177)) → U44_GGA(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
REDUCE50_IN_GGA(.(111, .(111, T32)), T29, .(111, X177)) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE50_IN_GGA(.(117, .(117, T32)), T29, .(117, X177)) → U45_GGA(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
REDUCE50_IN_GGA(.(117, .(117, T32)), T29, .(117, X177)) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE50_IN_GGA(.(104, .(104, T32)), T29, .(104, X177)) → U46_GGA(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
REDUCE50_IN_GGA(.(104, .(104, T32)), T29, .(104, X177)) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE50_IN_GGA(.(119, .(119, T32)), T29, .(119, X177)) → U47_GGA(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
REDUCE50_IN_GGA(.(119, .(119, T32)), T29, .(119, X177)) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE50_IN_GGA(.(121, .(121, T32)), T29, .(121, X177)) → U48_GGA(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
REDUCE50_IN_GGA(.(121, .(121, T32)), T29, .(121, X177)) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE50_IN_GGA(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_GGA(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
REDUCE50_IN_GGA(.(T33, .(T33, T34)), T29, .(T33, X234)) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE50_IN_GGA(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_GGA(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
REDUCE7_IN_GGA(.(101, .(101, T22)), T19, .(101, X73)) → U12_GGA(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
REDUCE7_IN_GGA(.(101, .(101, T22)), T19, .(101, X73)) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE7_IN_GGA(.(105, .(105, T22)), T19, .(105, X73)) → U13_GGA(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
REDUCE7_IN_GGA(.(105, .(105, T22)), T19, .(105, X73)) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE7_IN_GGA(.(111, .(111, T22)), T19, .(111, X73)) → U14_GGA(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
REDUCE7_IN_GGA(.(111, .(111, T22)), T19, .(111, X73)) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE7_IN_GGA(.(117, .(117, T22)), T19, .(117, X73)) → U15_GGA(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
REDUCE7_IN_GGA(.(117, .(117, T22)), T19, .(117, X73)) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE7_IN_GGA(.(104, .(104, T22)), T19, .(104, X73)) → U16_GGA(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
REDUCE7_IN_GGA(.(104, .(104, T22)), T19, .(104, X73)) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE7_IN_GGA(.(119, .(119, T22)), T19, .(119, X73)) → U17_GGA(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
REDUCE7_IN_GGA(.(119, .(119, T22)), T19, .(119, X73)) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE7_IN_GGA(.(121, .(121, T22)), T19, .(121, X73)) → U18_GGA(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
REDUCE7_IN_GGA(.(121, .(121, T22)), T19, .(121, X73)) → REDUCE50_IN_GGA(T22, 121, X73)
REDUCE7_IN_GGA(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_GGA(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
REDUCE7_IN_GGA(.(T23, .(T23, T24)), T19, .(T23, X130)) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE7_IN_GGA(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_GGA(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
REDUCE7_IN_GGA(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
REDUCE7_IN_GGA(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE7_IN_GGA(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
REDUCE7_IN_GGA(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE7_IN_GGA(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
REDUCE7_IN_GGA(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE7_IN_GGA(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
REDUCE7_IN_GGA(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE7_IN_GGA(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
REDUCE7_IN_GGA(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE7_IN_GGA(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
REDUCE7_IN_GGA(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE7_IN_GGA(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
REDUCE7_IN_GGA(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE7_IN_GGA(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
REDUCE7_IN_GGA(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE7_IN_GGA(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_GGA(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
REDUCE7_IN_GGA(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE7_IN_GGA(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_GGA(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
GOAL1_IN_GA(.(T7, T8), T42) → U62_GA(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
GOAL1_IN_GA(.(T7, T8), T42) → REDUCE7_IN_GGA(T8, T7, T42)

The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)
GOAL1_IN_GA(x1, x2)  =  GOAL1_IN_GA(x1)
U61_GA(x1, x2, x3, x4)  =  U61_GA(x4)
REDUCE7_IN_GGA(x1, x2, x3)  =  REDUCE7_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x3)
U2_GGA(x1, x2, x3)  =  U2_GGA(x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x3)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x4)
REDUCE50_IN_GGA(x1, x2, x3)  =  REDUCE50_IN_GGA(x1, x2)
U31_GGA(x1, x2, x3)  =  U31_GGA(x3)
U32_GGA(x1, x2, x3)  =  U32_GGA(x3)
U33_GGA(x1, x2, x3)  =  U33_GGA(x3)
U34_GGA(x1, x2, x3)  =  U34_GGA(x3)
U35_GGA(x1, x2, x3)  =  U35_GGA(x3)
U36_GGA(x1, x2, x3)  =  U36_GGA(x3)
U37_GGA(x1, x2, x3)  =  U37_GGA(x3)
U38_GGA(x1, x2, x3)  =  U38_GGA(x3)
U39_GGA(x1, x2, x3, x4)  =  U39_GGA(x4)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x4)
U41_GGA(x1, x2, x3, x4)  =  U41_GGA(x4)
REDUCE130_IN_GGA(x1, x2, x3)  =  REDUCE130_IN_GGA(x1, x2)
U51_GGA(x1, x2, x3)  =  U51_GGA(x3)
U52_GGA(x1, x2, x3)  =  U52_GGA(x3)
U53_GGA(x1, x2, x3)  =  U53_GGA(x3)
U54_GGA(x1, x2, x3)  =  U54_GGA(x3)
U55_GGA(x1, x2, x3)  =  U55_GGA(x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x3)
U57_GGA(x1, x2, x3)  =  U57_GGA(x3)
U58_GGA(x1, x2, x3)  =  U58_GGA(x3)
U59_GGA(x1, x2, x3, x4)  =  U59_GGA(x4)
U60_GGA(x1, x2, x3, x4)  =  U60_GGA(x4)
U42_GGA(x1, x2, x3, x4)  =  U42_GGA(x4)
U43_GGA(x1, x2, x3, x4)  =  U43_GGA(x4)
U44_GGA(x1, x2, x3, x4)  =  U44_GGA(x4)
U45_GGA(x1, x2, x3, x4)  =  U45_GGA(x4)
U46_GGA(x1, x2, x3, x4)  =  U46_GGA(x4)
U47_GGA(x1, x2, x3, x4)  =  U47_GGA(x4)
U48_GGA(x1, x2, x3, x4)  =  U48_GGA(x4)
U49_GGA(x1, x2, x3, x4, x5)  =  U49_GGA(x1, x5)
U50_GGA(x1, x2, x3, x4, x5)  =  U50_GGA(x1, x5)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
U19_GGA(x1, x2, x3, x4, x5)  =  U19_GGA(x1, x5)
U20_GGA(x1, x2, x3, x4, x5)  =  U20_GGA(x1, x5)
U21_GGA(x1, x2, x3, x4, x5)  =  U21_GGA(x1, x5)
U22_GGA(x1, x2, x3, x4, x5)  =  U22_GGA(x1, x5)
U23_GGA(x1, x2, x3, x4, x5)  =  U23_GGA(x1, x5)
U24_GGA(x1, x2, x3, x4, x5)  =  U24_GGA(x1, x5)
U25_GGA(x1, x2, x3, x4, x5)  =  U25_GGA(x1, x5)
U26_GGA(x1, x2, x3, x4, x5)  =  U26_GGA(x1, x5)
U27_GGA(x1, x2, x3, x4, x5)  =  U27_GGA(x1, x5)
U28_GGA(x1, x2, x3, x4, x5)  =  U28_GGA(x1, x5)
U29_GGA(x1, x2, x3, x4, x5, x6)  =  U29_GGA(x1, x2, x6)
U30_GGA(x1, x2, x3, x4, x5, x6)  =  U30_GGA(x1, x2, x6)
U62_GA(x1, x2, x3, x4)  =  U62_GA(x4)

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

(6) Obligation:

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

GOAL1_IN_GA(.(T7, T8), T5) → U61_GA(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
GOAL1_IN_GA(.(T7, T8), T5) → REDUCE7_IN_GGA(T8, T7, X12)
REDUCE7_IN_GGA(.(97, T12), 97, X29) → U1_GGA(T12, X29, reduce7_in_gga(T12, 97, X29))
REDUCE7_IN_GGA(.(97, T12), 97, X29) → REDUCE7_IN_GGA(T12, 97, X29)
REDUCE7_IN_GGA(.(101, T12), 101, X29) → U2_GGA(T12, X29, reduce7_in_gga(T12, 101, X29))
REDUCE7_IN_GGA(.(101, T12), 101, X29) → REDUCE7_IN_GGA(T12, 101, X29)
REDUCE7_IN_GGA(.(105, T12), 105, X29) → U3_GGA(T12, X29, reduce7_in_gga(T12, 105, X29))
REDUCE7_IN_GGA(.(105, T12), 105, X29) → REDUCE7_IN_GGA(T12, 105, X29)
REDUCE7_IN_GGA(.(111, T12), 111, X29) → U4_GGA(T12, X29, reduce7_in_gga(T12, 111, X29))
REDUCE7_IN_GGA(.(111, T12), 111, X29) → REDUCE7_IN_GGA(T12, 111, X29)
REDUCE7_IN_GGA(.(117, T12), 117, X29) → U5_GGA(T12, X29, reduce7_in_gga(T12, 117, X29))
REDUCE7_IN_GGA(.(117, T12), 117, X29) → REDUCE7_IN_GGA(T12, 117, X29)
REDUCE7_IN_GGA(.(104, T12), 104, X29) → U6_GGA(T12, X29, reduce7_in_gga(T12, 104, X29))
REDUCE7_IN_GGA(.(104, T12), 104, X29) → REDUCE7_IN_GGA(T12, 104, X29)
REDUCE7_IN_GGA(.(119, T12), 119, X29) → U7_GGA(T12, X29, reduce7_in_gga(T12, 119, X29))
REDUCE7_IN_GGA(.(119, T12), 119, X29) → REDUCE7_IN_GGA(T12, 119, X29)
REDUCE7_IN_GGA(.(121, T12), 121, X29) → U8_GGA(T12, X29, reduce7_in_gga(T12, 121, X29))
REDUCE7_IN_GGA(.(121, T12), 121, X29) → REDUCE7_IN_GGA(T12, 121, X29)
REDUCE7_IN_GGA(.(T13, T14), T13, X38) → U9_GGA(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
REDUCE7_IN_GGA(.(T13, T14), T13, X38) → REDUCE7_IN_GGA(T14, T13, X38)
REDUCE7_IN_GGA(.(T15, T16), T15, X47) → U10_GGA(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
REDUCE7_IN_GGA(.(97, .(97, T22)), T19, .(97, X73)) → U11_GGA(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
REDUCE7_IN_GGA(.(97, .(97, T22)), T19, .(97, X73)) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(97, T22), 97, X73) → U31_GGA(T22, X73, reduce50_in_gga(T22, 97, X73))
REDUCE50_IN_GGA(.(97, T22), 97, X73) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(101, T22), 101, X73) → U32_GGA(T22, X73, reduce50_in_gga(T22, 101, X73))
REDUCE50_IN_GGA(.(101, T22), 101, X73) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE50_IN_GGA(.(105, T22), 105, X73) → U33_GGA(T22, X73, reduce50_in_gga(T22, 105, X73))
REDUCE50_IN_GGA(.(105, T22), 105, X73) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE50_IN_GGA(.(111, T22), 111, X73) → U34_GGA(T22, X73, reduce50_in_gga(T22, 111, X73))
REDUCE50_IN_GGA(.(111, T22), 111, X73) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE50_IN_GGA(.(117, T22), 117, X73) → U35_GGA(T22, X73, reduce50_in_gga(T22, 117, X73))
REDUCE50_IN_GGA(.(117, T22), 117, X73) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE50_IN_GGA(.(104, T22), 104, X73) → U36_GGA(T22, X73, reduce50_in_gga(T22, 104, X73))
REDUCE50_IN_GGA(.(104, T22), 104, X73) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE50_IN_GGA(.(119, T22), 119, X73) → U37_GGA(T22, X73, reduce50_in_gga(T22, 119, X73))
REDUCE50_IN_GGA(.(119, T22), 119, X73) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE50_IN_GGA(.(121, T22), 121, X73) → U38_GGA(T22, X73, reduce50_in_gga(T22, 121, X73))
REDUCE50_IN_GGA(.(121, T22), 121, X73) → REDUCE50_IN_GGA(T22, 121, X73)
REDUCE50_IN_GGA(.(T23, T24), T23, X130) → U39_GGA(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
REDUCE50_IN_GGA(.(T23, T24), T23, X130) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE50_IN_GGA(.(T25, T26), T25, X145) → U40_GGA(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
REDUCE50_IN_GGA(.(97, .(97, T32)), T29, .(97, X177)) → U41_GGA(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
REDUCE50_IN_GGA(.(97, .(97, T32)), T29, .(97, X177)) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(97, T32), 97, X177) → U51_GGA(T32, X177, reduce130_in_gga(T32, 97, X177))
REDUCE130_IN_GGA(.(97, T32), 97, X177) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(101, T32), 101, X177) → U52_GGA(T32, X177, reduce130_in_gga(T32, 101, X177))
REDUCE130_IN_GGA(.(101, T32), 101, X177) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE130_IN_GGA(.(105, T32), 105, X177) → U53_GGA(T32, X177, reduce130_in_gga(T32, 105, X177))
REDUCE130_IN_GGA(.(105, T32), 105, X177) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE130_IN_GGA(.(111, T32), 111, X177) → U54_GGA(T32, X177, reduce130_in_gga(T32, 111, X177))
REDUCE130_IN_GGA(.(111, T32), 111, X177) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE130_IN_GGA(.(117, T32), 117, X177) → U55_GGA(T32, X177, reduce130_in_gga(T32, 117, X177))
REDUCE130_IN_GGA(.(117, T32), 117, X177) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE130_IN_GGA(.(104, T32), 104, X177) → U56_GGA(T32, X177, reduce130_in_gga(T32, 104, X177))
REDUCE130_IN_GGA(.(104, T32), 104, X177) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE130_IN_GGA(.(119, T32), 119, X177) → U57_GGA(T32, X177, reduce130_in_gga(T32, 119, X177))
REDUCE130_IN_GGA(.(119, T32), 119, X177) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE130_IN_GGA(.(121, T32), 121, X177) → U58_GGA(T32, X177, reduce130_in_gga(T32, 121, X177))
REDUCE130_IN_GGA(.(121, T32), 121, X177) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE130_IN_GGA(.(T33, T34), T33, X234) → U59_GGA(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
REDUCE130_IN_GGA(.(T33, T34), T33, X234) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE130_IN_GGA(.(T35, T36), T35, X249) → U60_GGA(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
REDUCE50_IN_GGA(.(101, .(101, T32)), T29, .(101, X177)) → U42_GGA(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
REDUCE50_IN_GGA(.(101, .(101, T32)), T29, .(101, X177)) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE50_IN_GGA(.(105, .(105, T32)), T29, .(105, X177)) → U43_GGA(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
REDUCE50_IN_GGA(.(105, .(105, T32)), T29, .(105, X177)) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE50_IN_GGA(.(111, .(111, T32)), T29, .(111, X177)) → U44_GGA(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
REDUCE50_IN_GGA(.(111, .(111, T32)), T29, .(111, X177)) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE50_IN_GGA(.(117, .(117, T32)), T29, .(117, X177)) → U45_GGA(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
REDUCE50_IN_GGA(.(117, .(117, T32)), T29, .(117, X177)) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE50_IN_GGA(.(104, .(104, T32)), T29, .(104, X177)) → U46_GGA(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
REDUCE50_IN_GGA(.(104, .(104, T32)), T29, .(104, X177)) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE50_IN_GGA(.(119, .(119, T32)), T29, .(119, X177)) → U47_GGA(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
REDUCE50_IN_GGA(.(119, .(119, T32)), T29, .(119, X177)) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE50_IN_GGA(.(121, .(121, T32)), T29, .(121, X177)) → U48_GGA(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
REDUCE50_IN_GGA(.(121, .(121, T32)), T29, .(121, X177)) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE50_IN_GGA(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_GGA(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
REDUCE50_IN_GGA(.(T33, .(T33, T34)), T29, .(T33, X234)) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE50_IN_GGA(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_GGA(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
REDUCE7_IN_GGA(.(101, .(101, T22)), T19, .(101, X73)) → U12_GGA(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
REDUCE7_IN_GGA(.(101, .(101, T22)), T19, .(101, X73)) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE7_IN_GGA(.(105, .(105, T22)), T19, .(105, X73)) → U13_GGA(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
REDUCE7_IN_GGA(.(105, .(105, T22)), T19, .(105, X73)) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE7_IN_GGA(.(111, .(111, T22)), T19, .(111, X73)) → U14_GGA(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
REDUCE7_IN_GGA(.(111, .(111, T22)), T19, .(111, X73)) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE7_IN_GGA(.(117, .(117, T22)), T19, .(117, X73)) → U15_GGA(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
REDUCE7_IN_GGA(.(117, .(117, T22)), T19, .(117, X73)) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE7_IN_GGA(.(104, .(104, T22)), T19, .(104, X73)) → U16_GGA(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
REDUCE7_IN_GGA(.(104, .(104, T22)), T19, .(104, X73)) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE7_IN_GGA(.(119, .(119, T22)), T19, .(119, X73)) → U17_GGA(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
REDUCE7_IN_GGA(.(119, .(119, T22)), T19, .(119, X73)) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE7_IN_GGA(.(121, .(121, T22)), T19, .(121, X73)) → U18_GGA(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
REDUCE7_IN_GGA(.(121, .(121, T22)), T19, .(121, X73)) → REDUCE50_IN_GGA(T22, 121, X73)
REDUCE7_IN_GGA(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_GGA(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
REDUCE7_IN_GGA(.(T23, .(T23, T24)), T19, .(T23, X130)) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE7_IN_GGA(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_GGA(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
REDUCE7_IN_GGA(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
REDUCE7_IN_GGA(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE7_IN_GGA(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
REDUCE7_IN_GGA(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE7_IN_GGA(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
REDUCE7_IN_GGA(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE7_IN_GGA(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
REDUCE7_IN_GGA(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE7_IN_GGA(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
REDUCE7_IN_GGA(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE7_IN_GGA(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
REDUCE7_IN_GGA(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE7_IN_GGA(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
REDUCE7_IN_GGA(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE7_IN_GGA(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_GGA(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
REDUCE7_IN_GGA(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → REDUCE130_IN_GGA(T32, 121, X177)
REDUCE7_IN_GGA(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_GGA(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
REDUCE7_IN_GGA(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE7_IN_GGA(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_GGA(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
GOAL1_IN_GA(.(T7, T8), T42) → U62_GA(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
GOAL1_IN_GA(.(T7, T8), T42) → REDUCE7_IN_GGA(T8, T7, T42)

The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)
GOAL1_IN_GA(x1, x2)  =  GOAL1_IN_GA(x1)
U61_GA(x1, x2, x3, x4)  =  U61_GA(x4)
REDUCE7_IN_GGA(x1, x2, x3)  =  REDUCE7_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x3)
U2_GGA(x1, x2, x3)  =  U2_GGA(x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x3)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x4)
REDUCE50_IN_GGA(x1, x2, x3)  =  REDUCE50_IN_GGA(x1, x2)
U31_GGA(x1, x2, x3)  =  U31_GGA(x3)
U32_GGA(x1, x2, x3)  =  U32_GGA(x3)
U33_GGA(x1, x2, x3)  =  U33_GGA(x3)
U34_GGA(x1, x2, x3)  =  U34_GGA(x3)
U35_GGA(x1, x2, x3)  =  U35_GGA(x3)
U36_GGA(x1, x2, x3)  =  U36_GGA(x3)
U37_GGA(x1, x2, x3)  =  U37_GGA(x3)
U38_GGA(x1, x2, x3)  =  U38_GGA(x3)
U39_GGA(x1, x2, x3, x4)  =  U39_GGA(x4)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x4)
U41_GGA(x1, x2, x3, x4)  =  U41_GGA(x4)
REDUCE130_IN_GGA(x1, x2, x3)  =  REDUCE130_IN_GGA(x1, x2)
U51_GGA(x1, x2, x3)  =  U51_GGA(x3)
U52_GGA(x1, x2, x3)  =  U52_GGA(x3)
U53_GGA(x1, x2, x3)  =  U53_GGA(x3)
U54_GGA(x1, x2, x3)  =  U54_GGA(x3)
U55_GGA(x1, x2, x3)  =  U55_GGA(x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x3)
U57_GGA(x1, x2, x3)  =  U57_GGA(x3)
U58_GGA(x1, x2, x3)  =  U58_GGA(x3)
U59_GGA(x1, x2, x3, x4)  =  U59_GGA(x4)
U60_GGA(x1, x2, x3, x4)  =  U60_GGA(x4)
U42_GGA(x1, x2, x3, x4)  =  U42_GGA(x4)
U43_GGA(x1, x2, x3, x4)  =  U43_GGA(x4)
U44_GGA(x1, x2, x3, x4)  =  U44_GGA(x4)
U45_GGA(x1, x2, x3, x4)  =  U45_GGA(x4)
U46_GGA(x1, x2, x3, x4)  =  U46_GGA(x4)
U47_GGA(x1, x2, x3, x4)  =  U47_GGA(x4)
U48_GGA(x1, x2, x3, x4)  =  U48_GGA(x4)
U49_GGA(x1, x2, x3, x4, x5)  =  U49_GGA(x1, x5)
U50_GGA(x1, x2, x3, x4, x5)  =  U50_GGA(x1, x5)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
U19_GGA(x1, x2, x3, x4, x5)  =  U19_GGA(x1, x5)
U20_GGA(x1, x2, x3, x4, x5)  =  U20_GGA(x1, x5)
U21_GGA(x1, x2, x3, x4, x5)  =  U21_GGA(x1, x5)
U22_GGA(x1, x2, x3, x4, x5)  =  U22_GGA(x1, x5)
U23_GGA(x1, x2, x3, x4, x5)  =  U23_GGA(x1, x5)
U24_GGA(x1, x2, x3, x4, x5)  =  U24_GGA(x1, x5)
U25_GGA(x1, x2, x3, x4, x5)  =  U25_GGA(x1, x5)
U26_GGA(x1, x2, x3, x4, x5)  =  U26_GGA(x1, x5)
U27_GGA(x1, x2, x3, x4, x5)  =  U27_GGA(x1, x5)
U28_GGA(x1, x2, x3, x4, x5)  =  U28_GGA(x1, x5)
U29_GGA(x1, x2, x3, x4, x5, x6)  =  U29_GGA(x1, x2, x6)
U30_GGA(x1, x2, x3, x4, x5, x6)  =  U30_GGA(x1, x2, x6)
U62_GA(x1, x2, x3, x4)  =  U62_GA(x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 91 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

REDUCE130_IN_GGA(.(T33, T34), T33, X234) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE130_IN_GGA(.(97, T32), 97, X177) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(101, T32), 101, X177) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE130_IN_GGA(.(105, T32), 105, X177) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE130_IN_GGA(.(111, T32), 111, X177) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE130_IN_GGA(.(117, T32), 117, X177) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE130_IN_GGA(.(104, T32), 104, X177) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE130_IN_GGA(.(119, T32), 119, X177) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE130_IN_GGA(.(121, T32), 121, X177) → REDUCE130_IN_GGA(T32, 121, X177)

The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)
REDUCE130_IN_GGA(x1, x2, x3)  =  REDUCE130_IN_GGA(x1, x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

REDUCE130_IN_GGA(.(T33, T34), T33, X234) → REDUCE130_IN_GGA(T34, T33, X234)
REDUCE130_IN_GGA(.(97, T32), 97, X177) → REDUCE130_IN_GGA(T32, 97, X177)
REDUCE130_IN_GGA(.(101, T32), 101, X177) → REDUCE130_IN_GGA(T32, 101, X177)
REDUCE130_IN_GGA(.(105, T32), 105, X177) → REDUCE130_IN_GGA(T32, 105, X177)
REDUCE130_IN_GGA(.(111, T32), 111, X177) → REDUCE130_IN_GGA(T32, 111, X177)
REDUCE130_IN_GGA(.(117, T32), 117, X177) → REDUCE130_IN_GGA(T32, 117, X177)
REDUCE130_IN_GGA(.(104, T32), 104, X177) → REDUCE130_IN_GGA(T32, 104, X177)
REDUCE130_IN_GGA(.(119, T32), 119, X177) → REDUCE130_IN_GGA(T32, 119, X177)
REDUCE130_IN_GGA(.(121, T32), 121, X177) → REDUCE130_IN_GGA(T32, 121, X177)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCE130_IN_GGA(x1, x2, x3)  =  REDUCE130_IN_GGA(x1, x2)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

REDUCE130_IN_GGA(.(T33, T34), T33) → REDUCE130_IN_GGA(T34, T33)
REDUCE130_IN_GGA(.(97, T32), 97) → REDUCE130_IN_GGA(T32, 97)
REDUCE130_IN_GGA(.(101, T32), 101) → REDUCE130_IN_GGA(T32, 101)
REDUCE130_IN_GGA(.(105, T32), 105) → REDUCE130_IN_GGA(T32, 105)
REDUCE130_IN_GGA(.(111, T32), 111) → REDUCE130_IN_GGA(T32, 111)
REDUCE130_IN_GGA(.(117, T32), 117) → REDUCE130_IN_GGA(T32, 117)
REDUCE130_IN_GGA(.(104, T32), 104) → REDUCE130_IN_GGA(T32, 104)
REDUCE130_IN_GGA(.(119, T32), 119) → REDUCE130_IN_GGA(T32, 119)
REDUCE130_IN_GGA(.(121, T32), 121) → REDUCE130_IN_GGA(T32, 121)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • REDUCE130_IN_GGA(.(T33, T34), T33) → REDUCE130_IN_GGA(T34, T33)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(97, T32), 97) → REDUCE130_IN_GGA(T32, 97)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(101, T32), 101) → REDUCE130_IN_GGA(T32, 101)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(105, T32), 105) → REDUCE130_IN_GGA(T32, 105)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(111, T32), 111) → REDUCE130_IN_GGA(T32, 111)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(117, T32), 117) → REDUCE130_IN_GGA(T32, 117)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(104, T32), 104) → REDUCE130_IN_GGA(T32, 104)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(119, T32), 119) → REDUCE130_IN_GGA(T32, 119)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE130_IN_GGA(.(121, T32), 121) → REDUCE130_IN_GGA(T32, 121)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(15) TRUE

(16) Obligation:

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

REDUCE50_IN_GGA(.(T23, T24), T23, X130) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE50_IN_GGA(.(97, T22), 97, X73) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(101, T22), 101, X73) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE50_IN_GGA(.(105, T22), 105, X73) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE50_IN_GGA(.(111, T22), 111, X73) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE50_IN_GGA(.(117, T22), 117, X73) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE50_IN_GGA(.(104, T22), 104, X73) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE50_IN_GGA(.(119, T22), 119, X73) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE50_IN_GGA(.(121, T22), 121, X73) → REDUCE50_IN_GGA(T22, 121, X73)

The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)
REDUCE50_IN_GGA(x1, x2, x3)  =  REDUCE50_IN_GGA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

REDUCE50_IN_GGA(.(T23, T24), T23, X130) → REDUCE50_IN_GGA(T24, T23, X130)
REDUCE50_IN_GGA(.(97, T22), 97, X73) → REDUCE50_IN_GGA(T22, 97, X73)
REDUCE50_IN_GGA(.(101, T22), 101, X73) → REDUCE50_IN_GGA(T22, 101, X73)
REDUCE50_IN_GGA(.(105, T22), 105, X73) → REDUCE50_IN_GGA(T22, 105, X73)
REDUCE50_IN_GGA(.(111, T22), 111, X73) → REDUCE50_IN_GGA(T22, 111, X73)
REDUCE50_IN_GGA(.(117, T22), 117, X73) → REDUCE50_IN_GGA(T22, 117, X73)
REDUCE50_IN_GGA(.(104, T22), 104, X73) → REDUCE50_IN_GGA(T22, 104, X73)
REDUCE50_IN_GGA(.(119, T22), 119, X73) → REDUCE50_IN_GGA(T22, 119, X73)
REDUCE50_IN_GGA(.(121, T22), 121, X73) → REDUCE50_IN_GGA(T22, 121, X73)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCE50_IN_GGA(x1, x2, x3)  =  REDUCE50_IN_GGA(x1, x2)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

REDUCE50_IN_GGA(.(T23, T24), T23) → REDUCE50_IN_GGA(T24, T23)
REDUCE50_IN_GGA(.(97, T22), 97) → REDUCE50_IN_GGA(T22, 97)
REDUCE50_IN_GGA(.(101, T22), 101) → REDUCE50_IN_GGA(T22, 101)
REDUCE50_IN_GGA(.(105, T22), 105) → REDUCE50_IN_GGA(T22, 105)
REDUCE50_IN_GGA(.(111, T22), 111) → REDUCE50_IN_GGA(T22, 111)
REDUCE50_IN_GGA(.(117, T22), 117) → REDUCE50_IN_GGA(T22, 117)
REDUCE50_IN_GGA(.(104, T22), 104) → REDUCE50_IN_GGA(T22, 104)
REDUCE50_IN_GGA(.(119, T22), 119) → REDUCE50_IN_GGA(T22, 119)
REDUCE50_IN_GGA(.(121, T22), 121) → REDUCE50_IN_GGA(T22, 121)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • REDUCE50_IN_GGA(.(T23, T24), T23) → REDUCE50_IN_GGA(T24, T23)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(97, T22), 97) → REDUCE50_IN_GGA(T22, 97)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(101, T22), 101) → REDUCE50_IN_GGA(T22, 101)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(105, T22), 105) → REDUCE50_IN_GGA(T22, 105)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(111, T22), 111) → REDUCE50_IN_GGA(T22, 111)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(117, T22), 117) → REDUCE50_IN_GGA(T22, 117)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(104, T22), 104) → REDUCE50_IN_GGA(T22, 104)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(119, T22), 119) → REDUCE50_IN_GGA(T22, 119)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE50_IN_GGA(.(121, T22), 121) → REDUCE50_IN_GGA(T22, 121)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(22) TRUE

(23) Obligation:

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

REDUCE7_IN_GGA(.(T13, T14), T13, X38) → REDUCE7_IN_GGA(T14, T13, X38)
REDUCE7_IN_GGA(.(97, T12), 97, X29) → REDUCE7_IN_GGA(T12, 97, X29)
REDUCE7_IN_GGA(.(101, T12), 101, X29) → REDUCE7_IN_GGA(T12, 101, X29)
REDUCE7_IN_GGA(.(105, T12), 105, X29) → REDUCE7_IN_GGA(T12, 105, X29)
REDUCE7_IN_GGA(.(111, T12), 111, X29) → REDUCE7_IN_GGA(T12, 111, X29)
REDUCE7_IN_GGA(.(117, T12), 117, X29) → REDUCE7_IN_GGA(T12, 117, X29)
REDUCE7_IN_GGA(.(104, T12), 104, X29) → REDUCE7_IN_GGA(T12, 104, X29)
REDUCE7_IN_GGA(.(119, T12), 119, X29) → REDUCE7_IN_GGA(T12, 119, X29)
REDUCE7_IN_GGA(.(121, T12), 121, X29) → REDUCE7_IN_GGA(T12, 121, X29)

The TRS R consists of the following rules:

goal1_in_ga(.(T7, T8), T5) → U61_ga(T7, T8, T5, reduce7_in_gga(T8, T7, X12))
reduce7_in_gga([], T10, []) → reduce7_out_gga([], T10, [])
reduce7_in_gga(.(97, T12), 97, X29) → U1_gga(T12, X29, reduce7_in_gga(T12, 97, X29))
reduce7_in_gga(.(101, T12), 101, X29) → U2_gga(T12, X29, reduce7_in_gga(T12, 101, X29))
reduce7_in_gga(.(105, T12), 105, X29) → U3_gga(T12, X29, reduce7_in_gga(T12, 105, X29))
reduce7_in_gga(.(111, T12), 111, X29) → U4_gga(T12, X29, reduce7_in_gga(T12, 111, X29))
reduce7_in_gga(.(117, T12), 117, X29) → U5_gga(T12, X29, reduce7_in_gga(T12, 117, X29))
reduce7_in_gga(.(104, T12), 104, X29) → U6_gga(T12, X29, reduce7_in_gga(T12, 104, X29))
reduce7_in_gga(.(119, T12), 119, X29) → U7_gga(T12, X29, reduce7_in_gga(T12, 119, X29))
reduce7_in_gga(.(121, T12), 121, X29) → U8_gga(T12, X29, reduce7_in_gga(T12, 121, X29))
reduce7_in_gga(.(T13, T14), T13, X38) → U9_gga(T13, T14, X38, reduce7_in_gga(T14, T13, X38))
reduce7_in_gga(.(T15, T16), T15, X47) → U10_gga(T15, T16, X47, reduce7_in_gga(T16, T15, X47))
reduce7_in_gga(.(T20, []), T19, .(T20, [])) → reduce7_out_gga(.(T20, []), T19, .(T20, []))
reduce7_in_gga(.(97, .(97, T22)), T19, .(97, X73)) → U11_gga(T22, T19, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga([], T20, []) → reduce50_out_gga([], T20, [])
reduce50_in_gga(.(97, T22), 97, X73) → U31_gga(T22, X73, reduce50_in_gga(T22, 97, X73))
reduce50_in_gga(.(101, T22), 101, X73) → U32_gga(T22, X73, reduce50_in_gga(T22, 101, X73))
reduce50_in_gga(.(105, T22), 105, X73) → U33_gga(T22, X73, reduce50_in_gga(T22, 105, X73))
reduce50_in_gga(.(111, T22), 111, X73) → U34_gga(T22, X73, reduce50_in_gga(T22, 111, X73))
reduce50_in_gga(.(117, T22), 117, X73) → U35_gga(T22, X73, reduce50_in_gga(T22, 117, X73))
reduce50_in_gga(.(104, T22), 104, X73) → U36_gga(T22, X73, reduce50_in_gga(T22, 104, X73))
reduce50_in_gga(.(119, T22), 119, X73) → U37_gga(T22, X73, reduce50_in_gga(T22, 119, X73))
reduce50_in_gga(.(121, T22), 121, X73) → U38_gga(T22, X73, reduce50_in_gga(T22, 121, X73))
reduce50_in_gga(.(T23, T24), T23, X130) → U39_gga(T23, T24, X130, reduce50_in_gga(T24, T23, X130))
reduce50_in_gga(.(T25, T26), T25, X145) → U40_gga(T25, T26, X145, reduce50_in_gga(T26, T25, X145))
reduce50_in_gga(.(T30, []), T29, .(T30, [])) → reduce50_out_gga(.(T30, []), T29, .(T30, []))
reduce50_in_gga(.(97, .(97, T32)), T29, .(97, X177)) → U41_gga(T32, T29, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga([], T30, []) → reduce130_out_gga([], T30, [])
reduce130_in_gga(.(97, T32), 97, X177) → U51_gga(T32, X177, reduce130_in_gga(T32, 97, X177))
reduce130_in_gga(.(101, T32), 101, X177) → U52_gga(T32, X177, reduce130_in_gga(T32, 101, X177))
reduce130_in_gga(.(105, T32), 105, X177) → U53_gga(T32, X177, reduce130_in_gga(T32, 105, X177))
reduce130_in_gga(.(111, T32), 111, X177) → U54_gga(T32, X177, reduce130_in_gga(T32, 111, X177))
reduce130_in_gga(.(117, T32), 117, X177) → U55_gga(T32, X177, reduce130_in_gga(T32, 117, X177))
reduce130_in_gga(.(104, T32), 104, X177) → U56_gga(T32, X177, reduce130_in_gga(T32, 104, X177))
reduce130_in_gga(.(119, T32), 119, X177) → U57_gga(T32, X177, reduce130_in_gga(T32, 119, X177))
reduce130_in_gga(.(121, T32), 121, X177) → U58_gga(T32, X177, reduce130_in_gga(T32, 121, X177))
reduce130_in_gga(.(T33, T34), T33, X234) → U59_gga(T33, T34, X234, reduce130_in_gga(T34, T33, X234))
reduce130_in_gga(.(T35, T36), T35, X249) → U60_gga(T35, T36, X249, reduce130_in_gga(T36, T35, X249))
reduce130_in_gga(.(T41, T40), T39, .(T41, [])) → reduce130_out_gga(.(T41, T40), T39, .(T41, []))
U60_gga(T35, T36, X249, reduce130_out_gga(T36, T35, X249)) → reduce130_out_gga(.(T35, T36), T35, X249)
U59_gga(T33, T34, X234, reduce130_out_gga(T34, T33, X234)) → reduce130_out_gga(.(T33, T34), T33, X234)
U58_gga(T32, X177, reduce130_out_gga(T32, 121, X177)) → reduce130_out_gga(.(121, T32), 121, X177)
U57_gga(T32, X177, reduce130_out_gga(T32, 119, X177)) → reduce130_out_gga(.(119, T32), 119, X177)
U56_gga(T32, X177, reduce130_out_gga(T32, 104, X177)) → reduce130_out_gga(.(104, T32), 104, X177)
U55_gga(T32, X177, reduce130_out_gga(T32, 117, X177)) → reduce130_out_gga(.(117, T32), 117, X177)
U54_gga(T32, X177, reduce130_out_gga(T32, 111, X177)) → reduce130_out_gga(.(111, T32), 111, X177)
U53_gga(T32, X177, reduce130_out_gga(T32, 105, X177)) → reduce130_out_gga(.(105, T32), 105, X177)
U52_gga(T32, X177, reduce130_out_gga(T32, 101, X177)) → reduce130_out_gga(.(101, T32), 101, X177)
U51_gga(T32, X177, reduce130_out_gga(T32, 97, X177)) → reduce130_out_gga(.(97, T32), 97, X177)
U41_gga(T32, T29, X177, reduce130_out_gga(T32, 97, X177)) → reduce50_out_gga(.(97, .(97, T32)), T29, .(97, X177))
reduce50_in_gga(.(101, .(101, T32)), T29, .(101, X177)) → U42_gga(T32, T29, X177, reduce130_in_gga(T32, 101, X177))
U42_gga(T32, T29, X177, reduce130_out_gga(T32, 101, X177)) → reduce50_out_gga(.(101, .(101, T32)), T29, .(101, X177))
reduce50_in_gga(.(105, .(105, T32)), T29, .(105, X177)) → U43_gga(T32, T29, X177, reduce130_in_gga(T32, 105, X177))
U43_gga(T32, T29, X177, reduce130_out_gga(T32, 105, X177)) → reduce50_out_gga(.(105, .(105, T32)), T29, .(105, X177))
reduce50_in_gga(.(111, .(111, T32)), T29, .(111, X177)) → U44_gga(T32, T29, X177, reduce130_in_gga(T32, 111, X177))
U44_gga(T32, T29, X177, reduce130_out_gga(T32, 111, X177)) → reduce50_out_gga(.(111, .(111, T32)), T29, .(111, X177))
reduce50_in_gga(.(117, .(117, T32)), T29, .(117, X177)) → U45_gga(T32, T29, X177, reduce130_in_gga(T32, 117, X177))
U45_gga(T32, T29, X177, reduce130_out_gga(T32, 117, X177)) → reduce50_out_gga(.(117, .(117, T32)), T29, .(117, X177))
reduce50_in_gga(.(104, .(104, T32)), T29, .(104, X177)) → U46_gga(T32, T29, X177, reduce130_in_gga(T32, 104, X177))
U46_gga(T32, T29, X177, reduce130_out_gga(T32, 104, X177)) → reduce50_out_gga(.(104, .(104, T32)), T29, .(104, X177))
reduce50_in_gga(.(119, .(119, T32)), T29, .(119, X177)) → U47_gga(T32, T29, X177, reduce130_in_gga(T32, 119, X177))
U47_gga(T32, T29, X177, reduce130_out_gga(T32, 119, X177)) → reduce50_out_gga(.(119, .(119, T32)), T29, .(119, X177))
reduce50_in_gga(.(121, .(121, T32)), T29, .(121, X177)) → U48_gga(T32, T29, X177, reduce130_in_gga(T32, 121, X177))
U48_gga(T32, T29, X177, reduce130_out_gga(T32, 121, X177)) → reduce50_out_gga(.(121, .(121, T32)), T29, .(121, X177))
reduce50_in_gga(.(T33, .(T33, T34)), T29, .(T33, X234)) → U49_gga(T33, T34, T29, X234, reduce130_in_gga(T34, T33, X234))
U49_gga(T33, T34, T29, X234, reduce130_out_gga(T34, T33, X234)) → reduce50_out_gga(.(T33, .(T33, T34)), T29, .(T33, X234))
reduce50_in_gga(.(T35, .(T35, T36)), T29, .(T35, X249)) → U50_gga(T35, T36, T29, X249, reduce130_in_gga(T36, T35, X249))
U50_gga(T35, T36, T29, X249, reduce130_out_gga(T36, T35, X249)) → reduce50_out_gga(.(T35, .(T35, T36)), T29, .(T35, X249))
reduce50_in_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, []))) → reduce50_out_gga(.(T39, .(T41, T40)), T29, .(T39, .(T41, [])))
U40_gga(T25, T26, X145, reduce50_out_gga(T26, T25, X145)) → reduce50_out_gga(.(T25, T26), T25, X145)
U39_gga(T23, T24, X130, reduce50_out_gga(T24, T23, X130)) → reduce50_out_gga(.(T23, T24), T23, X130)
U38_gga(T22, X73, reduce50_out_gga(T22, 121, X73)) → reduce50_out_gga(.(121, T22), 121, X73)
U37_gga(T22, X73, reduce50_out_gga(T22, 119, X73)) → reduce50_out_gga(.(119, T22), 119, X73)
U36_gga(T22, X73, reduce50_out_gga(T22, 104, X73)) → reduce50_out_gga(.(104, T22), 104, X73)
U35_gga(T22, X73, reduce50_out_gga(T22, 117, X73)) → reduce50_out_gga(.(117, T22), 117, X73)
U34_gga(T22, X73, reduce50_out_gga(T22, 111, X73)) → reduce50_out_gga(.(111, T22), 111, X73)
U33_gga(T22, X73, reduce50_out_gga(T22, 105, X73)) → reduce50_out_gga(.(105, T22), 105, X73)
U32_gga(T22, X73, reduce50_out_gga(T22, 101, X73)) → reduce50_out_gga(.(101, T22), 101, X73)
U31_gga(T22, X73, reduce50_out_gga(T22, 97, X73)) → reduce50_out_gga(.(97, T22), 97, X73)
U11_gga(T22, T19, X73, reduce50_out_gga(T22, 97, X73)) → reduce7_out_gga(.(97, .(97, T22)), T19, .(97, X73))
reduce7_in_gga(.(101, .(101, T22)), T19, .(101, X73)) → U12_gga(T22, T19, X73, reduce50_in_gga(T22, 101, X73))
U12_gga(T22, T19, X73, reduce50_out_gga(T22, 101, X73)) → reduce7_out_gga(.(101, .(101, T22)), T19, .(101, X73))
reduce7_in_gga(.(105, .(105, T22)), T19, .(105, X73)) → U13_gga(T22, T19, X73, reduce50_in_gga(T22, 105, X73))
U13_gga(T22, T19, X73, reduce50_out_gga(T22, 105, X73)) → reduce7_out_gga(.(105, .(105, T22)), T19, .(105, X73))
reduce7_in_gga(.(111, .(111, T22)), T19, .(111, X73)) → U14_gga(T22, T19, X73, reduce50_in_gga(T22, 111, X73))
U14_gga(T22, T19, X73, reduce50_out_gga(T22, 111, X73)) → reduce7_out_gga(.(111, .(111, T22)), T19, .(111, X73))
reduce7_in_gga(.(117, .(117, T22)), T19, .(117, X73)) → U15_gga(T22, T19, X73, reduce50_in_gga(T22, 117, X73))
U15_gga(T22, T19, X73, reduce50_out_gga(T22, 117, X73)) → reduce7_out_gga(.(117, .(117, T22)), T19, .(117, X73))
reduce7_in_gga(.(104, .(104, T22)), T19, .(104, X73)) → U16_gga(T22, T19, X73, reduce50_in_gga(T22, 104, X73))
U16_gga(T22, T19, X73, reduce50_out_gga(T22, 104, X73)) → reduce7_out_gga(.(104, .(104, T22)), T19, .(104, X73))
reduce7_in_gga(.(119, .(119, T22)), T19, .(119, X73)) → U17_gga(T22, T19, X73, reduce50_in_gga(T22, 119, X73))
U17_gga(T22, T19, X73, reduce50_out_gga(T22, 119, X73)) → reduce7_out_gga(.(119, .(119, T22)), T19, .(119, X73))
reduce7_in_gga(.(121, .(121, T22)), T19, .(121, X73)) → U18_gga(T22, T19, X73, reduce50_in_gga(T22, 121, X73))
U18_gga(T22, T19, X73, reduce50_out_gga(T22, 121, X73)) → reduce7_out_gga(.(121, .(121, T22)), T19, .(121, X73))
reduce7_in_gga(.(T23, .(T23, T24)), T19, .(T23, X130)) → U19_gga(T23, T24, T19, X130, reduce50_in_gga(T24, T23, X130))
U19_gga(T23, T24, T19, X130, reduce50_out_gga(T24, T23, X130)) → reduce7_out_gga(.(T23, .(T23, T24)), T19, .(T23, X130))
reduce7_in_gga(.(T25, .(T25, T26)), T19, .(T25, X145)) → U20_gga(T25, T26, T19, X145, reduce50_in_gga(T26, T25, X145))
U20_gga(T25, T26, T19, X145, reduce50_out_gga(T26, T25, X145)) → reduce7_out_gga(.(T25, .(T25, T26)), T19, .(T25, X145))
reduce7_in_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, []))) → reduce7_out_gga(.(T29, .(T30, [])), T19, .(T29, .(T30, [])))
reduce7_in_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177))) → U21_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 97, X177))
U21_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 97, X177)) → reduce7_out_gga(.(T29, .(97, .(97, T32))), T19, .(T29, .(97, X177)))
reduce7_in_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177))) → U22_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 101, X177))
U22_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 101, X177)) → reduce7_out_gga(.(T29, .(101, .(101, T32))), T19, .(T29, .(101, X177)))
reduce7_in_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177))) → U23_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 105, X177))
U23_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 105, X177)) → reduce7_out_gga(.(T29, .(105, .(105, T32))), T19, .(T29, .(105, X177)))
reduce7_in_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177))) → U24_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 111, X177))
U24_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 111, X177)) → reduce7_out_gga(.(T29, .(111, .(111, T32))), T19, .(T29, .(111, X177)))
reduce7_in_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177))) → U25_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 117, X177))
U25_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 117, X177)) → reduce7_out_gga(.(T29, .(117, .(117, T32))), T19, .(T29, .(117, X177)))
reduce7_in_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177))) → U26_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 104, X177))
U26_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 104, X177)) → reduce7_out_gga(.(T29, .(104, .(104, T32))), T19, .(T29, .(104, X177)))
reduce7_in_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177))) → U27_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 119, X177))
U27_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 119, X177)) → reduce7_out_gga(.(T29, .(119, .(119, T32))), T19, .(T29, .(119, X177)))
reduce7_in_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177))) → U28_gga(T29, T32, T19, X177, reduce130_in_gga(T32, 121, X177))
U28_gga(T29, T32, T19, X177, reduce130_out_gga(T32, 121, X177)) → reduce7_out_gga(.(T29, .(121, .(121, T32))), T19, .(T29, .(121, X177)))
reduce7_in_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234))) → U29_gga(T29, T33, T34, T19, X234, reduce130_in_gga(T34, T33, X234))
U29_gga(T29, T33, T34, T19, X234, reduce130_out_gga(T34, T33, X234)) → reduce7_out_gga(.(T29, .(T33, .(T33, T34))), T19, .(T29, .(T33, X234)))
reduce7_in_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249))) → U30_gga(T29, T35, T36, T19, X249, reduce130_in_gga(T36, T35, X249))
U30_gga(T29, T35, T36, T19, X249, reduce130_out_gga(T36, T35, X249)) → reduce7_out_gga(.(T29, .(T35, .(T35, T36))), T19, .(T29, .(T35, X249)))
reduce7_in_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, [])))) → reduce7_out_gga(.(T29, .(T39, .(T41, T40))), T19, .(T29, .(T39, .(T41, []))))
U10_gga(T15, T16, X47, reduce7_out_gga(T16, T15, X47)) → reduce7_out_gga(.(T15, T16), T15, X47)
U9_gga(T13, T14, X38, reduce7_out_gga(T14, T13, X38)) → reduce7_out_gga(.(T13, T14), T13, X38)
U8_gga(T12, X29, reduce7_out_gga(T12, 121, X29)) → reduce7_out_gga(.(121, T12), 121, X29)
U7_gga(T12, X29, reduce7_out_gga(T12, 119, X29)) → reduce7_out_gga(.(119, T12), 119, X29)
U6_gga(T12, X29, reduce7_out_gga(T12, 104, X29)) → reduce7_out_gga(.(104, T12), 104, X29)
U5_gga(T12, X29, reduce7_out_gga(T12, 117, X29)) → reduce7_out_gga(.(117, T12), 117, X29)
U4_gga(T12, X29, reduce7_out_gga(T12, 111, X29)) → reduce7_out_gga(.(111, T12), 111, X29)
U3_gga(T12, X29, reduce7_out_gga(T12, 105, X29)) → reduce7_out_gga(.(105, T12), 105, X29)
U2_gga(T12, X29, reduce7_out_gga(T12, 101, X29)) → reduce7_out_gga(.(101, T12), 101, X29)
U1_gga(T12, X29, reduce7_out_gga(T12, 97, X29)) → reduce7_out_gga(.(97, T12), 97, X29)
U61_ga(T7, T8, T5, reduce7_out_gga(T8, T7, X12)) → goal1_out_ga(.(T7, T8), T5)
goal1_in_ga(.(T7, T8), T42) → U62_ga(T7, T8, T42, reduce7_in_gga(T8, T7, T42))
U62_ga(T7, T8, T42, reduce7_out_gga(T8, T7, T42)) → goal1_out_ga(.(T7, T8), T42)

The argument filtering Pi contains the following mapping:
goal1_in_ga(x1, x2)  =  goal1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U61_ga(x1, x2, x3, x4)  =  U61_ga(x4)
reduce7_in_gga(x1, x2, x3)  =  reduce7_in_gga(x1, x2)
[]  =  []
reduce7_out_gga(x1, x2, x3)  =  reduce7_out_gga(x3)
97  =  97
U1_gga(x1, x2, x3)  =  U1_gga(x3)
101  =  101
U2_gga(x1, x2, x3)  =  U2_gga(x3)
105  =  105
U3_gga(x1, x2, x3)  =  U3_gga(x3)
111  =  111
U4_gga(x1, x2, x3)  =  U4_gga(x3)
117  =  117
U5_gga(x1, x2, x3)  =  U5_gga(x3)
104  =  104
U6_gga(x1, x2, x3)  =  U6_gga(x3)
119  =  119
U7_gga(x1, x2, x3)  =  U7_gga(x3)
121  =  121
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
reduce50_in_gga(x1, x2, x3)  =  reduce50_in_gga(x1, x2)
reduce50_out_gga(x1, x2, x3)  =  reduce50_out_gga(x3)
U31_gga(x1, x2, x3)  =  U31_gga(x3)
U32_gga(x1, x2, x3)  =  U32_gga(x3)
U33_gga(x1, x2, x3)  =  U33_gga(x3)
U34_gga(x1, x2, x3)  =  U34_gga(x3)
U35_gga(x1, x2, x3)  =  U35_gga(x3)
U36_gga(x1, x2, x3)  =  U36_gga(x3)
U37_gga(x1, x2, x3)  =  U37_gga(x3)
U38_gga(x1, x2, x3)  =  U38_gga(x3)
U39_gga(x1, x2, x3, x4)  =  U39_gga(x4)
U40_gga(x1, x2, x3, x4)  =  U40_gga(x4)
U41_gga(x1, x2, x3, x4)  =  U41_gga(x4)
reduce130_in_gga(x1, x2, x3)  =  reduce130_in_gga(x1, x2)
reduce130_out_gga(x1, x2, x3)  =  reduce130_out_gga(x3)
U51_gga(x1, x2, x3)  =  U51_gga(x3)
U52_gga(x1, x2, x3)  =  U52_gga(x3)
U53_gga(x1, x2, x3)  =  U53_gga(x3)
U54_gga(x1, x2, x3)  =  U54_gga(x3)
U55_gga(x1, x2, x3)  =  U55_gga(x3)
U56_gga(x1, x2, x3)  =  U56_gga(x3)
U57_gga(x1, x2, x3)  =  U57_gga(x3)
U58_gga(x1, x2, x3)  =  U58_gga(x3)
U59_gga(x1, x2, x3, x4)  =  U59_gga(x4)
U60_gga(x1, x2, x3, x4)  =  U60_gga(x4)
U42_gga(x1, x2, x3, x4)  =  U42_gga(x4)
U43_gga(x1, x2, x3, x4)  =  U43_gga(x4)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x4)
U46_gga(x1, x2, x3, x4)  =  U46_gga(x4)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x4)
U48_gga(x1, x2, x3, x4)  =  U48_gga(x4)
U49_gga(x1, x2, x3, x4, x5)  =  U49_gga(x1, x5)
U50_gga(x1, x2, x3, x4, x5)  =  U50_gga(x1, x5)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U14_gga(x1, x2, x3, x4)  =  U14_gga(x4)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x5)
U20_gga(x1, x2, x3, x4, x5)  =  U20_gga(x1, x5)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x5)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x5)
U23_gga(x1, x2, x3, x4, x5)  =  U23_gga(x1, x5)
U24_gga(x1, x2, x3, x4, x5)  =  U24_gga(x1, x5)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x5)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x5)
U27_gga(x1, x2, x3, x4, x5)  =  U27_gga(x1, x5)
U28_gga(x1, x2, x3, x4, x5)  =  U28_gga(x1, x5)
U29_gga(x1, x2, x3, x4, x5, x6)  =  U29_gga(x1, x2, x6)
U30_gga(x1, x2, x3, x4, x5, x6)  =  U30_gga(x1, x2, x6)
goal1_out_ga(x1, x2)  =  goal1_out_ga
U62_ga(x1, x2, x3, x4)  =  U62_ga(x4)
REDUCE7_IN_GGA(x1, x2, x3)  =  REDUCE7_IN_GGA(x1, x2)

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

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

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

REDUCE7_IN_GGA(.(T13, T14), T13, X38) → REDUCE7_IN_GGA(T14, T13, X38)
REDUCE7_IN_GGA(.(97, T12), 97, X29) → REDUCE7_IN_GGA(T12, 97, X29)
REDUCE7_IN_GGA(.(101, T12), 101, X29) → REDUCE7_IN_GGA(T12, 101, X29)
REDUCE7_IN_GGA(.(105, T12), 105, X29) → REDUCE7_IN_GGA(T12, 105, X29)
REDUCE7_IN_GGA(.(111, T12), 111, X29) → REDUCE7_IN_GGA(T12, 111, X29)
REDUCE7_IN_GGA(.(117, T12), 117, X29) → REDUCE7_IN_GGA(T12, 117, X29)
REDUCE7_IN_GGA(.(104, T12), 104, X29) → REDUCE7_IN_GGA(T12, 104, X29)
REDUCE7_IN_GGA(.(119, T12), 119, X29) → REDUCE7_IN_GGA(T12, 119, X29)
REDUCE7_IN_GGA(.(121, T12), 121, X29) → REDUCE7_IN_GGA(T12, 121, X29)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
97  =  97
101  =  101
105  =  105
111  =  111
117  =  117
104  =  104
119  =  119
121  =  121
REDUCE7_IN_GGA(x1, x2, x3)  =  REDUCE7_IN_GGA(x1, x2)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

REDUCE7_IN_GGA(.(T13, T14), T13) → REDUCE7_IN_GGA(T14, T13)
REDUCE7_IN_GGA(.(97, T12), 97) → REDUCE7_IN_GGA(T12, 97)
REDUCE7_IN_GGA(.(101, T12), 101) → REDUCE7_IN_GGA(T12, 101)
REDUCE7_IN_GGA(.(105, T12), 105) → REDUCE7_IN_GGA(T12, 105)
REDUCE7_IN_GGA(.(111, T12), 111) → REDUCE7_IN_GGA(T12, 111)
REDUCE7_IN_GGA(.(117, T12), 117) → REDUCE7_IN_GGA(T12, 117)
REDUCE7_IN_GGA(.(104, T12), 104) → REDUCE7_IN_GGA(T12, 104)
REDUCE7_IN_GGA(.(119, T12), 119) → REDUCE7_IN_GGA(T12, 119)
REDUCE7_IN_GGA(.(121, T12), 121) → REDUCE7_IN_GGA(T12, 121)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • REDUCE7_IN_GGA(.(T13, T14), T13) → REDUCE7_IN_GGA(T14, T13)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(97, T12), 97) → REDUCE7_IN_GGA(T12, 97)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(101, T12), 101) → REDUCE7_IN_GGA(T12, 101)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(105, T12), 105) → REDUCE7_IN_GGA(T12, 105)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(111, T12), 111) → REDUCE7_IN_GGA(T12, 111)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(117, T12), 117) → REDUCE7_IN_GGA(T12, 117)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(104, T12), 104) → REDUCE7_IN_GGA(T12, 104)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(119, T12), 119) → REDUCE7_IN_GGA(T12, 119)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

  • REDUCE7_IN_GGA(.(121, T12), 121) → REDUCE7_IN_GGA(T12, 121)
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 2

(29) TRUE