0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 342 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 38 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 15 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 23 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
fA_in_gga([], [], []) → fA_out_gga([], [], [])
fA_in_gga(.(T21, T22), [], T24) → U1_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gC_in_ggga([], T404, T405, .(T404, T405)) → gC_out_ggga([], T404, T405, .(T404, T405))
gC_in_ggga(.(T416, T417), T418, T419, T421) → U4_ggga(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
U4_ggga(T416, T417, T418, T419, T421, gC_out_ggga(T417, T416, .(T418, T419), T421)) → gC_out_ggga(.(T416, T417), T418, T419, T421)
U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U1_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fA_out_gga(.(T21, T22), [], T24)
fA_in_gga(.(T472, T473), .(T471, []), T475) → U2_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U2_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fA_out_gga(.(T472, T473), .(T471, []), T475)
fA_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_gga(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U3_gga(T489, T490, T488, T491, T492, T494, fA_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fA_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FA_IN_GGA(.(T21, T22), [], T24) → U1_GGA(T21, T22, T24, gB_in_gga(T22, T21, T24))
FA_IN_GGA(.(T21, T22), [], T24) → GB_IN_GGA(T22, T21, T24)
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → GC_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → U4_GGGA(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → GC_IN_GGGA(T417, T416, .(T418, T419), T421)
FA_IN_GGA(.(T472, T473), .(T471, []), T475) → U2_GGA(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
FA_IN_GGA(.(T472, T473), .(T471, []), T475) → GB_IN_GGA(.(T472, T473), T471, T475)
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_GGA(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FA_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fA_in_gga([], [], []) → fA_out_gga([], [], [])
fA_in_gga(.(T21, T22), [], T24) → U1_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gC_in_ggga([], T404, T405, .(T404, T405)) → gC_out_ggga([], T404, T405, .(T404, T405))
gC_in_ggga(.(T416, T417), T418, T419, T421) → U4_ggga(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
U4_ggga(T416, T417, T418, T419, T421, gC_out_ggga(T417, T416, .(T418, T419), T421)) → gC_out_ggga(.(T416, T417), T418, T419, T421)
U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U1_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fA_out_gga(.(T21, T22), [], T24)
fA_in_gga(.(T472, T473), .(T471, []), T475) → U2_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U2_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fA_out_gga(.(T472, T473), .(T471, []), T475)
fA_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_gga(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U3_gga(T489, T490, T488, T491, T492, T494, fA_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fA_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FA_IN_GGA(.(T21, T22), [], T24) → U1_GGA(T21, T22, T24, gB_in_gga(T22, T21, T24))
FA_IN_GGA(.(T21, T22), [], T24) → GB_IN_GGA(T22, T21, T24)
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → GC_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → U4_GGGA(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → GC_IN_GGGA(T417, T416, .(T418, T419), T421)
FA_IN_GGA(.(T472, T473), .(T471, []), T475) → U2_GGA(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
FA_IN_GGA(.(T472, T473), .(T471, []), T475) → GB_IN_GGA(.(T472, T473), T471, T475)
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_GGA(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FA_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fA_in_gga([], [], []) → fA_out_gga([], [], [])
fA_in_gga(.(T21, T22), [], T24) → U1_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gC_in_ggga([], T404, T405, .(T404, T405)) → gC_out_ggga([], T404, T405, .(T404, T405))
gC_in_ggga(.(T416, T417), T418, T419, T421) → U4_ggga(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
U4_ggga(T416, T417, T418, T419, T421, gC_out_ggga(T417, T416, .(T418, T419), T421)) → gC_out_ggga(.(T416, T417), T418, T419, T421)
U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U1_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fA_out_gga(.(T21, T22), [], T24)
fA_in_gga(.(T472, T473), .(T471, []), T475) → U2_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U2_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fA_out_gga(.(T472, T473), .(T471, []), T475)
fA_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_gga(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U3_gga(T489, T490, T488, T491, T492, T494, fA_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fA_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → GC_IN_GGGA(T417, T416, .(T418, T419), T421)
fA_in_gga([], [], []) → fA_out_gga([], [], [])
fA_in_gga(.(T21, T22), [], T24) → U1_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gC_in_ggga([], T404, T405, .(T404, T405)) → gC_out_ggga([], T404, T405, .(T404, T405))
gC_in_ggga(.(T416, T417), T418, T419, T421) → U4_ggga(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
U4_ggga(T416, T417, T418, T419, T421, gC_out_ggga(T417, T416, .(T418, T419), T421)) → gC_out_ggga(.(T416, T417), T418, T419, T421)
U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U1_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fA_out_gga(.(T21, T22), [], T24)
fA_in_gga(.(T472, T473), .(T471, []), T475) → U2_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U2_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fA_out_gga(.(T472, T473), .(T471, []), T475)
fA_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_gga(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U3_gga(T489, T490, T488, T491, T492, T494, fA_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fA_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
GC_IN_GGGA(.(T416, T417), T418, T419, T421) → GC_IN_GGGA(T417, T416, .(T418, T419), T421)
GC_IN_GGGA(.(T416, T417), T418, T419) → GC_IN_GGGA(T417, T416, .(T418, T419))
From the DPs we obtained the following set of size-change graphs:
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FA_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fA_in_gga([], [], []) → fA_out_gga([], [], [])
fA_in_gga(.(T21, T22), [], T24) → U1_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gC_in_ggga([], T404, T405, .(T404, T405)) → gC_out_ggga([], T404, T405, .(T404, T405))
gC_in_ggga(.(T416, T417), T418, T419, T421) → U4_ggga(T416, T417, T418, T419, T421, gC_in_ggga(T417, T416, .(T418, T419), T421))
U4_ggga(T416, T417, T418, T419, T421, gC_out_ggga(T417, T416, .(T418, T419), T421)) → gC_out_ggga(.(T416, T417), T418, T419, T421)
U5_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gC_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U1_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fA_out_gga(.(T21, T22), [], T24)
fA_in_gga(.(T472, T473), .(T471, []), T475) → U2_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U2_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fA_out_gga(.(T472, T473), .(T471, []), T475)
fA_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U3_gga(T489, T490, T488, T491, T492, T494, fA_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U3_gga(T489, T490, T488, T491, T492, T494, fA_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fA_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FA_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
FA_IN_GGA(.(T489, T490), .(T488, .(T491, T492))) → FA_IN_GGA(.(T491, .(T488, .(T489, T490))), T492)
From the DPs we obtained the following set of size-change graphs: