(0) Obligation:

Clauses:

subset(X, Y) :- subsetchecked(X, [], Y).
subsetchecked([], X1, X2).
subsetchecked(.(X, Xs), Ys, Zs) :- ','(member(X, Zs), ','(not_member(X, Ys), subsetchecked(Xs, .(X, Ys), Zs))).
member(X, .(X, X3)).
member(X, .(X4, Xs)) :- member(X, Xs).
not_member(X, Y) :- ','(member(X, Y), ','(!, failure(a))).
not_member(X5, X6).
failure(b).

Queries:

subset(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

member12(T53, .(T51, T52)) :- member12(T53, T52).
subsetchecked188(.(T1173, T1174), T1170, T1171, T1172) :- member12(T1173, T1172).
subsetchecked188(.(T1211, T1180), T1212, T1213, T1172) :- ','(memberc12(T1211, T1172), member12(T1211, .(T1212, T1213))).
subsetchecked188(.(T1179, T1180), T1170, T1171, T1172) :- ','(memberc12(T1179, T1172), ','(not_memberc210(T1179, T1170, T1171), subsetchecked188(T1180, T1179, .(T1170, T1171), T1172))).
p184(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990) :- member12(T984, T983).
p184(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990) :- ','(memberc12(T1077, T983), member12(T1077, .(T1078, .(T1079, .(T1080, .(T1081, .(T1082, .(T1083, .(T1084, []))))))))).
p184(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990) :- ','(memberc12(T995, T983), ','(not_memberc187(T995, T976, T977, T978, T979, T980, T981, T982), subsetchecked188(T996, T995, T990, T983))).
subset1(.(T22, T23), T21) :- member12(T22, T21).
subset1(.(T106, .(T108, T109)), T107) :- ','(memberc12(T106, T107), ','(not_memberc22(T106), member12(T108, T107))).
subset1(.(T137, .(T136, T115)), T107) :- ','(memberc12(T137, T107), ','(not_memberc22(T137), ','(memberc12(T136, T107), member12(T136, .(T137, []))))).
subset1(.(T182, .(T181, .(T184, T185))), T183) :- ','(memberc12(T182, T183), ','(not_memberc22(T182), ','(memberc12(T181, T183), ','(not_memberc48(T181, T182), member12(T184, T183))))).
subset1(.(T224, .(T223, .(T222, T191))), T183) :- ','(memberc12(T224, T183), ','(not_memberc22(T224), ','(memberc12(T223, T183), ','(not_memberc48(T223, T224), ','(memberc12(T222, T183), member12(T222, .(T223, .(T224, [])))))))).
subset1(.(T286, .(T285, .(T284, .(T288, T289)))), T287) :- ','(memberc12(T286, T287), ','(not_memberc22(T286), ','(memberc12(T285, T287), ','(not_memberc48(T285, T286), ','(memberc12(T284, T287), ','(not_memberc71(T284, T285, T286), member12(T288, T287))))))).
subset1(.(T339, .(T338, .(T337, .(T336, T295)))), T287) :- ','(memberc12(T339, T287), ','(not_memberc22(T339), ','(memberc12(T338, T287), ','(not_memberc48(T338, T339), ','(memberc12(T337, T287), ','(not_memberc71(T337, T338, T339), ','(memberc12(T336, T287), member12(T336, .(T337, .(T338, .(T339, []))))))))))).
subset1(.(T418, .(T417, .(T416, .(T415, .(T420, T421))))), T419) :- ','(memberc12(T418, T419), ','(not_memberc22(T418), ','(memberc12(T417, T419), ','(not_memberc48(T417, T418), ','(memberc12(T416, T419), ','(not_memberc71(T416, T417, T418), ','(memberc12(T415, T419), ','(not_memberc94(T415, T416, T417, T418), member12(T420, T419))))))))).
subset1(.(T482, .(T481, .(T480, .(T479, .(T478, T427))))), T419) :- ','(memberc12(T482, T419), ','(not_memberc22(T482), ','(memberc12(T481, T419), ','(not_memberc48(T481, T482), ','(memberc12(T480, T419), ','(not_memberc71(T480, T481, T482), ','(memberc12(T479, T419), ','(not_memberc94(T479, T480, T481, T482), ','(memberc12(T478, T419), member12(T478, .(T479, .(T480, .(T481, .(T482, [])))))))))))))).
subset1(.(T578, .(T577, .(T576, .(T575, .(T574, .(T580, T581)))))), T579) :- ','(memberc12(T578, T579), ','(not_memberc22(T578), ','(memberc12(T577, T579), ','(not_memberc48(T577, T578), ','(memberc12(T576, T579), ','(not_memberc71(T576, T577, T578), ','(memberc12(T575, T579), ','(not_memberc94(T575, T576, T577, T578), ','(memberc12(T574, T579), ','(not_memberc117(T574, T575, T576, T577, T578), member12(T580, T579))))))))))).
subset1(.(T653, .(T652, .(T651, .(T650, .(T649, .(T648, T587)))))), T579) :- ','(memberc12(T653, T579), ','(not_memberc22(T653), ','(memberc12(T652, T579), ','(not_memberc48(T652, T653), ','(memberc12(T651, T579), ','(not_memberc71(T651, T652, T653), ','(memberc12(T650, T579), ','(not_memberc94(T650, T651, T652, T653), ','(memberc12(T649, T579), ','(not_memberc117(T649, T650, T651, T652, T653), ','(memberc12(T648, T579), member12(T648, .(T649, .(T650, .(T651, .(T652, .(T653, []))))))))))))))))).
subset1(.(T766, .(T765, .(T764, .(T763, .(T762, .(T761, .(T768, T769))))))), T767) :- ','(memberc12(T766, T767), ','(not_memberc22(T766), ','(memberc12(T765, T767), ','(not_memberc48(T765, T766), ','(memberc12(T764, T767), ','(not_memberc71(T764, T765, T766), ','(memberc12(T763, T767), ','(not_memberc94(T763, T764, T765, T766), ','(memberc12(T762, T767), ','(not_memberc117(T762, T763, T764, T765, T766), ','(memberc12(T761, T767), ','(not_memberc140(T761, T762, T763, T764, T765, T766), member12(T768, T767))))))))))))).
subset1(.(T852, .(T851, .(T850, .(T849, .(T848, .(T847, .(T846, T775))))))), T767) :- ','(memberc12(T852, T767), ','(not_memberc22(T852), ','(memberc12(T851, T767), ','(not_memberc48(T851, T852), ','(memberc12(T850, T767), ','(not_memberc71(T850, T851, T852), ','(memberc12(T849, T767), ','(not_memberc94(T849, T850, T851, T852), ','(memberc12(T848, T767), ','(not_memberc117(T848, T849, T850, T851, T852), ','(memberc12(T847, T767), ','(not_memberc140(T847, T848, T849, T850, T851, T852), ','(memberc12(T846, T767), member12(T846, .(T847, .(T848, .(T849, .(T850, .(T851, .(T852, [])))))))))))))))))))).
subset1(.(T982, .(T981, .(T980, .(T979, .(T978, .(T977, .(T976, .(T984, T985)))))))), T983) :- ','(memberc12(T982, T983), ','(not_memberc22(T982), ','(memberc12(T981, T983), ','(not_memberc48(T981, T982), ','(memberc12(T980, T983), ','(not_memberc71(T980, T981, T982), ','(memberc12(T979, T983), ','(not_memberc94(T979, T980, T981, T982), ','(memberc12(T978, T983), ','(not_memberc117(T978, T979, T980, T981, T982), ','(memberc12(T977, T983), ','(not_memberc140(T977, T978, T979, T980, T981, T982), ','(memberc12(T976, T983), ','(not_memberc163(T976, T977, T978, T979, T980, T981, T982), p184(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, .(T976, .(T977, .(T978, .(T979, .(T980, .(T981, .(T982, [])))))))))))))))))))))).

Clauses:

memberc12(T42, .(T42, T43)).
memberc12(T53, .(T51, T52)) :- memberc12(T53, T52).
subsetcheckedc188([], T1155, T1156, T1157).
subsetcheckedc188(.(T1179, T1180), T1170, T1171, T1172) :- ','(memberc12(T1179, T1172), ','(not_memberc210(T1179, T1170, T1171), subsetcheckedc188(T1180, T1179, .(T1170, T1171), T1172))).
qc184(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990) :- ','(memberc12(T995, T983), ','(not_memberc187(T995, T976, T977, T978, T979, T980, T981, T982), subsetcheckedc188(T996, T995, T990, T983))).
not_memberc22(T81).
not_memberc48(T146, T147).
not_memberc71(T239, T240, T241).
not_memberc94(T360, T361, T362, T363).
not_memberc117(T509, T510, T511, T512, T513).
not_memberc140(T686, T687, T688, T689, T690, T691).
not_memberc163(T891, T892, T893, T894, T895, T896, T897).
not_memberc187(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136).
not_memberc210(T1228, T1229, T1230).

Afs:

subset1(x1, x2)  =  subset1(x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
subset1_in: (f,b)
member12_in: (f,b) (b,b)
memberc12_in: (f,b)
p184_in: (f,b,b,b,b,b,b,b,b,f,b)
subsetchecked188_in: (f,b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

SUBSET1_IN_AG(.(T22, T23), T21) → U14_AG(T22, T23, T21, member12_in_ag(T22, T21))
SUBSET1_IN_AG(.(T22, T23), T21) → MEMBER12_IN_AG(T22, T21)
MEMBER12_IN_AG(T53, .(T51, T52)) → U1_AG(T53, T51, T52, member12_in_ag(T53, T52))
MEMBER12_IN_AG(T53, .(T51, T52)) → MEMBER12_IN_AG(T53, T52)
SUBSET1_IN_AG(.(T106, .(T108, T109)), T107) → U15_AG(T106, T108, T109, T107, memberc12_in_ag(T106, T107))
U15_AG(T106, T108, T109, T107, memberc12_out_ag(T106, T107)) → U16_AG(T106, T108, T109, T107, not_memberc22_in_g(T106))
U16_AG(T106, T108, T109, T107, not_memberc22_out_g(T106)) → U17_AG(T106, T108, T109, T107, member12_in_ag(T108, T107))
U16_AG(T106, T108, T109, T107, not_memberc22_out_g(T106)) → MEMBER12_IN_AG(T108, T107)
SUBSET1_IN_AG(.(T137, .(T136, T115)), T107) → U18_AG(T137, T136, T115, T107, memberc12_in_ag(T137, T107))
U18_AG(T137, T136, T115, T107, memberc12_out_ag(T137, T107)) → U19_AG(T137, T136, T115, T107, not_memberc22_in_g(T137))
U19_AG(T137, T136, T115, T107, not_memberc22_out_g(T137)) → U20_AG(T137, T136, T115, T107, memberc12_in_ag(T136, T107))
U20_AG(T137, T136, T115, T107, memberc12_out_ag(T136, T107)) → U21_AG(T137, T136, T115, T107, member12_in_gg(T136, .(T137, [])))
U20_AG(T137, T136, T115, T107, memberc12_out_ag(T136, T107)) → MEMBER12_IN_GG(T136, .(T137, []))
MEMBER12_IN_GG(T53, .(T51, T52)) → U1_GG(T53, T51, T52, member12_in_gg(T53, T52))
MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)
SUBSET1_IN_AG(.(T182, .(T181, .(T184, T185))), T183) → U22_AG(T182, T181, T184, T185, T183, memberc12_in_ag(T182, T183))
U22_AG(T182, T181, T184, T185, T183, memberc12_out_ag(T182, T183)) → U23_AG(T182, T181, T184, T185, T183, not_memberc22_in_g(T182))
U23_AG(T182, T181, T184, T185, T183, not_memberc22_out_g(T182)) → U24_AG(T182, T181, T184, T185, T183, memberc12_in_ag(T181, T183))
U24_AG(T182, T181, T184, T185, T183, memberc12_out_ag(T181, T183)) → U25_AG(T182, T181, T184, T185, T183, not_memberc48_in_gg(T181, T182))
U25_AG(T182, T181, T184, T185, T183, not_memberc48_out_gg(T181, T182)) → U26_AG(T182, T181, T184, T185, T183, member12_in_ag(T184, T183))
U25_AG(T182, T181, T184, T185, T183, not_memberc48_out_gg(T181, T182)) → MEMBER12_IN_AG(T184, T183)
SUBSET1_IN_AG(.(T224, .(T223, .(T222, T191))), T183) → U27_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T224, T183))
U27_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T224, T183)) → U28_AG(T224, T223, T222, T191, T183, not_memberc22_in_g(T224))
U28_AG(T224, T223, T222, T191, T183, not_memberc22_out_g(T224)) → U29_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T223, T183))
U29_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T223, T183)) → U30_AG(T224, T223, T222, T191, T183, not_memberc48_in_gg(T223, T224))
U30_AG(T224, T223, T222, T191, T183, not_memberc48_out_gg(T223, T224)) → U31_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T222, T183))
U31_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T222, T183)) → U32_AG(T224, T223, T222, T191, T183, member12_in_gg(T222, .(T223, .(T224, []))))
U31_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T222, T183)) → MEMBER12_IN_GG(T222, .(T223, .(T224, [])))
SUBSET1_IN_AG(.(T286, .(T285, .(T284, .(T288, T289)))), T287) → U33_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T286, T287))
U33_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T286, T287)) → U34_AG(T286, T285, T284, T288, T289, T287, not_memberc22_in_g(T286))
U34_AG(T286, T285, T284, T288, T289, T287, not_memberc22_out_g(T286)) → U35_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T285, T287))
U35_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T285, T287)) → U36_AG(T286, T285, T284, T288, T289, T287, not_memberc48_in_gg(T285, T286))
U36_AG(T286, T285, T284, T288, T289, T287, not_memberc48_out_gg(T285, T286)) → U37_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T284, T287))
U37_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T284, T287)) → U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_in_ggg(T284, T285, T286))
U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_out_ggg(T284, T285, T286)) → U39_AG(T286, T285, T284, T288, T289, T287, member12_in_ag(T288, T287))
U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_out_ggg(T284, T285, T286)) → MEMBER12_IN_AG(T288, T287)
SUBSET1_IN_AG(.(T339, .(T338, .(T337, .(T336, T295)))), T287) → U40_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T339, T287))
U40_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T339, T287)) → U41_AG(T339, T338, T337, T336, T295, T287, not_memberc22_in_g(T339))
U41_AG(T339, T338, T337, T336, T295, T287, not_memberc22_out_g(T339)) → U42_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T338, T287))
U42_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T338, T287)) → U43_AG(T339, T338, T337, T336, T295, T287, not_memberc48_in_gg(T338, T339))
U43_AG(T339, T338, T337, T336, T295, T287, not_memberc48_out_gg(T338, T339)) → U44_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T337, T287))
U44_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T337, T287)) → U45_AG(T339, T338, T337, T336, T295, T287, not_memberc71_in_ggg(T337, T338, T339))
U45_AG(T339, T338, T337, T336, T295, T287, not_memberc71_out_ggg(T337, T338, T339)) → U46_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T336, T287))
U46_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T336, T287)) → U47_AG(T339, T338, T337, T336, T295, T287, member12_in_gg(T336, .(T337, .(T338, .(T339, [])))))
U46_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T336, T287)) → MEMBER12_IN_GG(T336, .(T337, .(T338, .(T339, []))))
SUBSET1_IN_AG(.(T418, .(T417, .(T416, .(T415, .(T420, T421))))), T419) → U48_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T418, T419))
U48_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T418, T419)) → U49_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc22_in_g(T418))
U49_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc22_out_g(T418)) → U50_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T417, T419))
U50_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T417, T419)) → U51_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc48_in_gg(T417, T418))
U51_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc48_out_gg(T417, T418)) → U52_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T416, T419))
U52_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T416, T419)) → U53_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc71_in_ggg(T416, T417, T418))
U53_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc71_out_ggg(T416, T417, T418)) → U54_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T415, T419))
U54_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T415, T419)) → U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_in_gggg(T415, T416, T417, T418))
U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_out_gggg(T415, T416, T417, T418)) → U56_AG(T418, T417, T416, T415, T420, T421, T419, member12_in_ag(T420, T419))
U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_out_gggg(T415, T416, T417, T418)) → MEMBER12_IN_AG(T420, T419)
SUBSET1_IN_AG(.(T482, .(T481, .(T480, .(T479, .(T478, T427))))), T419) → U57_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T482, T419))
U57_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T482, T419)) → U58_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc22_in_g(T482))
U58_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc22_out_g(T482)) → U59_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T481, T419))
U59_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T481, T419)) → U60_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc48_in_gg(T481, T482))
U60_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc48_out_gg(T481, T482)) → U61_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T480, T419))
U61_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T480, T419)) → U62_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc71_in_ggg(T480, T481, T482))
U62_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc71_out_ggg(T480, T481, T482)) → U63_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T479, T419))
U63_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T479, T419)) → U64_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc94_in_gggg(T479, T480, T481, T482))
U64_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc94_out_gggg(T479, T480, T481, T482)) → U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T478, T419))
U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T478, T419)) → U66_AG(T482, T481, T480, T479, T478, T427, T419, member12_in_gg(T478, .(T479, .(T480, .(T481, .(T482, []))))))
U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T478, T419)) → MEMBER12_IN_GG(T478, .(T479, .(T480, .(T481, .(T482, [])))))
SUBSET1_IN_AG(.(T578, .(T577, .(T576, .(T575, .(T574, .(T580, T581)))))), T579) → U67_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T578, T579))
U67_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T578, T579)) → U68_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc22_in_g(T578))
U68_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc22_out_g(T578)) → U69_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T577, T579))
U69_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T577, T579)) → U70_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc48_in_gg(T577, T578))
U70_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc48_out_gg(T577, T578)) → U71_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T576, T579))
U71_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T576, T579)) → U72_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc71_in_ggg(T576, T577, T578))
U72_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc71_out_ggg(T576, T577, T578)) → U73_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T575, T579))
U73_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T575, T579)) → U74_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc94_in_gggg(T575, T576, T577, T578))
U74_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc94_out_gggg(T575, T576, T577, T578)) → U75_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T574, T579))
U75_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T574, T579)) → U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_in_ggggg(T574, T575, T576, T577, T578))
U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_out_ggggg(T574, T575, T576, T577, T578)) → U77_AG(T578, T577, T576, T575, T574, T580, T581, T579, member12_in_ag(T580, T579))
U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_out_ggggg(T574, T575, T576, T577, T578)) → MEMBER12_IN_AG(T580, T579)
SUBSET1_IN_AG(.(T653, .(T652, .(T651, .(T650, .(T649, .(T648, T587)))))), T579) → U78_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T653, T579))
U78_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T653, T579)) → U79_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc22_in_g(T653))
U79_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc22_out_g(T653)) → U80_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T652, T579))
U80_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T652, T579)) → U81_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc48_in_gg(T652, T653))
U81_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc48_out_gg(T652, T653)) → U82_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T651, T579))
U82_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T651, T579)) → U83_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc71_in_ggg(T651, T652, T653))
U83_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc71_out_ggg(T651, T652, T653)) → U84_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T650, T579))
U84_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T650, T579)) → U85_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc94_in_gggg(T650, T651, T652, T653))
U85_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc94_out_gggg(T650, T651, T652, T653)) → U86_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T649, T579))
U86_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T649, T579)) → U87_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc117_in_ggggg(T649, T650, T651, T652, T653))
U87_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc117_out_ggggg(T649, T650, T651, T652, T653)) → U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T648, T579))
U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T648, T579)) → U89_AG(T653, T652, T651, T650, T649, T648, T587, T579, member12_in_gg(T648, .(T649, .(T650, .(T651, .(T652, .(T653, [])))))))
U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T648, T579)) → MEMBER12_IN_GG(T648, .(T649, .(T650, .(T651, .(T652, .(T653, []))))))
SUBSET1_IN_AG(.(T766, .(T765, .(T764, .(T763, .(T762, .(T761, .(T768, T769))))))), T767) → U90_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T766, T767))
U90_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T766, T767)) → U91_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc22_in_g(T766))
U91_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc22_out_g(T766)) → U92_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T765, T767))
U92_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T765, T767)) → U93_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc48_in_gg(T765, T766))
U93_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc48_out_gg(T765, T766)) → U94_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T764, T767))
U94_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T764, T767)) → U95_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc71_in_ggg(T764, T765, T766))
U95_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc71_out_ggg(T764, T765, T766)) → U96_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T763, T767))
U96_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T763, T767)) → U97_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc94_in_gggg(T763, T764, T765, T766))
U97_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc94_out_gggg(T763, T764, T765, T766)) → U98_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T762, T767))
U98_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T762, T767)) → U99_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc117_in_ggggg(T762, T763, T764, T765, T766))
U99_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc117_out_ggggg(T762, T763, T764, T765, T766)) → U100_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T761, T767))
U100_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T761, T767)) → U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_in_gggggg(T761, T762, T763, T764, T765, T766))
U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_out_gggggg(T761, T762, T763, T764, T765, T766)) → U102_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, member12_in_ag(T768, T767))
U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_out_gggggg(T761, T762, T763, T764, T765, T766)) → MEMBER12_IN_AG(T768, T767)
SUBSET1_IN_AG(.(T852, .(T851, .(T850, .(T849, .(T848, .(T847, .(T846, T775))))))), T767) → U103_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T852, T767))
U103_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T852, T767)) → U104_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc22_in_g(T852))
U104_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc22_out_g(T852)) → U105_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T851, T767))
U105_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T851, T767)) → U106_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc48_in_gg(T851, T852))
U106_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc48_out_gg(T851, T852)) → U107_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T850, T767))
U107_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T850, T767)) → U108_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc71_in_ggg(T850, T851, T852))
U108_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc71_out_ggg(T850, T851, T852)) → U109_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T849, T767))
U109_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T849, T767)) → U110_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc94_in_gggg(T849, T850, T851, T852))
U110_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc94_out_gggg(T849, T850, T851, T852)) → U111_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T848, T767))
U111_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T848, T767)) → U112_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc117_in_ggggg(T848, T849, T850, T851, T852))
U112_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc117_out_ggggg(T848, T849, T850, T851, T852)) → U113_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T847, T767))
U113_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T847, T767)) → U114_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc140_in_gggggg(T847, T848, T849, T850, T851, T852))
U114_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc140_out_gggggg(T847, T848, T849, T850, T851, T852)) → U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T846, T767))
U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T846, T767)) → U116_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, member12_in_gg(T846, .(T847, .(T848, .(T849, .(T850, .(T851, .(T852, []))))))))
U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T846, T767)) → MEMBER12_IN_GG(T846, .(T847, .(T848, .(T849, .(T850, .(T851, .(T852, [])))))))
SUBSET1_IN_AG(.(T982, .(T981, .(T980, .(T979, .(T978, .(T977, .(T976, .(T984, T985)))))))), T983) → U117_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T982, T983))
U117_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T982, T983)) → U118_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc22_in_g(T982))
U118_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc22_out_g(T982)) → U119_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T981, T983))
U119_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T981, T983)) → U120_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc48_in_gg(T981, T982))
U120_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc48_out_gg(T981, T982)) → U121_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T980, T983))
U121_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T980, T983)) → U122_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc71_in_ggg(T980, T981, T982))
U122_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc71_out_ggg(T980, T981, T982)) → U123_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T979, T983))
U123_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T979, T983)) → U124_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc94_in_gggg(T979, T980, T981, T982))
U124_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc94_out_gggg(T979, T980, T981, T982)) → U125_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T978, T983))
U125_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T978, T983)) → U126_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc117_in_ggggg(T978, T979, T980, T981, T982))
U126_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc117_out_ggggg(T978, T979, T980, T981, T982)) → U127_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T977, T983))
U127_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T977, T983)) → U128_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc140_in_gggggg(T977, T978, T979, T980, T981, T982))
U128_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc140_out_gggggg(T977, T978, T979, T980, T981, T982)) → U129_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T976, T983))
U129_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T976, T983)) → U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_in_ggggggg(T976, T977, T978, T979, T980, T981, T982))
U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_out_ggggggg(T976, T977, T978, T979, T980, T981, T982)) → U131_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, p184_in_aggggggggag(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, .(T976, .(T977, .(T978, .(T979, .(T980, .(T981, .(T982, [])))))))))
U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_out_ggggggg(T976, T977, T978, T979, T980, T981, T982)) → P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, .(T976, .(T977, .(T978, .(T979, .(T980, .(T981, .(T982, []))))))))
P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990) → U8_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990, member12_in_ag(T984, T983))
P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990) → MEMBER12_IN_AG(T984, T983)
P184_IN_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990) → U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_in_ag(T1077, T983))
U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_out_ag(T1077, T983)) → U10_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, member12_in_gg(T1077, .(T1078, .(T1079, .(T1080, .(T1081, .(T1082, .(T1083, .(T1084, [])))))))))
U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_out_ag(T1077, T983)) → MEMBER12_IN_GG(T1077, .(T1078, .(T1079, .(T1080, .(T1081, .(T1082, .(T1083, .(T1084, []))))))))
P184_IN_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990) → U11_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, memberc12_in_ag(T995, T983))
U11_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, memberc12_out_ag(T995, T983)) → U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_in_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982))
U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_out_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982)) → U13_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, subsetchecked188_in_aggg(T996, T995, T990, T983))
U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_out_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982)) → SUBSETCHECKED188_IN_AGGG(T996, T995, T990, T983)
SUBSETCHECKED188_IN_AGGG(.(T1173, T1174), T1170, T1171, T1172) → U2_AGGG(T1173, T1174, T1170, T1171, T1172, member12_in_ag(T1173, T1172))
SUBSETCHECKED188_IN_AGGG(.(T1173, T1174), T1170, T1171, T1172) → MEMBER12_IN_AG(T1173, T1172)
SUBSETCHECKED188_IN_AGGG(.(T1211, T1180), T1212, T1213, T1172) → U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_in_ag(T1211, T1172))
U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_out_ag(T1211, T1172)) → U4_AGGG(T1211, T1180, T1212, T1213, T1172, member12_in_gg(T1211, .(T1212, T1213)))
U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_out_ag(T1211, T1172)) → MEMBER12_IN_GG(T1211, .(T1212, T1213))
SUBSETCHECKED188_IN_AGGG(.(T1179, T1180), T1170, T1171, T1172) → U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_in_ag(T1179, T1172))
U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → U7_AGGG(T1179, T1180, T1170, T1171, T1172, subsetchecked188_in_aggg(T1180, T1179, .(T1170, T1171), T1172))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1180, T1179, .(T1170, T1171), T1172)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))
not_memberc22_in_g(T81) → not_memberc22_out_g(T81)
not_memberc48_in_gg(T146, T147) → not_memberc48_out_gg(T146, T147)
not_memberc71_in_ggg(T239, T240, T241) → not_memberc71_out_ggg(T239, T240, T241)
not_memberc94_in_gggg(T360, T361, T362, T363) → not_memberc94_out_gggg(T360, T361, T362, T363)
not_memberc117_in_ggggg(T509, T510, T511, T512, T513) → not_memberc117_out_ggggg(T509, T510, T511, T512, T513)
not_memberc140_in_gggggg(T686, T687, T688, T689, T690, T691) → not_memberc140_out_gggggg(T686, T687, T688, T689, T690, T691)
not_memberc163_in_ggggggg(T891, T892, T893, T894, T895, T896, T897) → not_memberc163_out_ggggggg(T891, T892, T893, T894, T895, T896, T897)
not_memberc187_in_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136) → not_memberc187_out_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136)
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)

The argument filtering Pi contains the following mapping:
member12_in_ag(x1, x2)  =  member12_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc22_in_g(x1)  =  not_memberc22_in_g(x1)
not_memberc22_out_g(x1)  =  not_memberc22_out_g(x1)
member12_in_gg(x1, x2)  =  member12_in_gg(x1, x2)
[]  =  []
not_memberc48_in_gg(x1, x2)  =  not_memberc48_in_gg(x1, x2)
not_memberc48_out_gg(x1, x2)  =  not_memberc48_out_gg(x1, x2)
not_memberc71_in_ggg(x1, x2, x3)  =  not_memberc71_in_ggg(x1, x2, x3)
not_memberc71_out_ggg(x1, x2, x3)  =  not_memberc71_out_ggg(x1, x2, x3)
not_memberc94_in_gggg(x1, x2, x3, x4)  =  not_memberc94_in_gggg(x1, x2, x3, x4)
not_memberc94_out_gggg(x1, x2, x3, x4)  =  not_memberc94_out_gggg(x1, x2, x3, x4)
not_memberc117_in_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_in_ggggg(x1, x2, x3, x4, x5)
not_memberc117_out_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_out_ggggg(x1, x2, x3, x4, x5)
not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)
p184_in_aggggggggag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  p184_in_aggggggggag(x2, x3, x4, x5, x6, x7, x8, x9, x11)
not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
subsetchecked188_in_aggg(x1, x2, x3, x4)  =  subsetchecked188_in_aggg(x2, x3, x4)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
SUBSET1_IN_AG(x1, x2)  =  SUBSET1_IN_AG(x2)
U14_AG(x1, x2, x3, x4)  =  U14_AG(x3, x4)
MEMBER12_IN_AG(x1, x2)  =  MEMBER12_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x2, x3, x4)
U15_AG(x1, x2, x3, x4, x5)  =  U15_AG(x4, x5)
U16_AG(x1, x2, x3, x4, x5)  =  U16_AG(x4, x5)
U17_AG(x1, x2, x3, x4, x5)  =  U17_AG(x4, x5)
U18_AG(x1, x2, x3, x4, x5)  =  U18_AG(x4, x5)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x1, x4, x5)
U20_AG(x1, x2, x3, x4, x5)  =  U20_AG(x1, x4, x5)
U21_AG(x1, x2, x3, x4, x5)  =  U21_AG(x4, x5)
MEMBER12_IN_GG(x1, x2)  =  MEMBER12_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
U22_AG(x1, x2, x3, x4, x5, x6)  =  U22_AG(x5, x6)
U23_AG(x1, x2, x3, x4, x5, x6)  =  U23_AG(x1, x5, x6)
U24_AG(x1, x2, x3, x4, x5, x6)  =  U24_AG(x1, x5, x6)
U25_AG(x1, x2, x3, x4, x5, x6)  =  U25_AG(x5, x6)
U26_AG(x1, x2, x3, x4, x5, x6)  =  U26_AG(x5, x6)
U27_AG(x1, x2, x3, x4, x5, x6)  =  U27_AG(x5, x6)
U28_AG(x1, x2, x3, x4, x5, x6)  =  U28_AG(x1, x5, x6)
U29_AG(x1, x2, x3, x4, x5, x6)  =  U29_AG(x1, x5, x6)
U30_AG(x1, x2, x3, x4, x5, x6)  =  U30_AG(x1, x2, x5, x6)
U31_AG(x1, x2, x3, x4, x5, x6)  =  U31_AG(x1, x2, x5, x6)
U32_AG(x1, x2, x3, x4, x5, x6)  =  U32_AG(x5, x6)
U33_AG(x1, x2, x3, x4, x5, x6, x7)  =  U33_AG(x6, x7)
U34_AG(x1, x2, x3, x4, x5, x6, x7)  =  U34_AG(x1, x6, x7)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x1, x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x1, x2, x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x1, x2, x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7)  =  U39_AG(x6, x7)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x1, x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7)  =  U42_AG(x1, x6, x7)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x1, x2, x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x1, x2, x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7)  =  U45_AG(x1, x2, x3, x6, x7)
U46_AG(x1, x2, x3, x4, x5, x6, x7)  =  U46_AG(x1, x2, x3, x6, x7)
U47_AG(x1, x2, x3, x4, x5, x6, x7)  =  U47_AG(x6, x7)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U48_AG(x7, x8)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U49_AG(x1, x7, x8)
U50_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U50_AG(x1, x7, x8)
U51_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U51_AG(x1, x2, x7, x8)
U52_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U52_AG(x1, x2, x7, x8)
U53_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U53_AG(x1, x2, x3, x7, x8)
U54_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U54_AG(x1, x2, x3, x7, x8)
U55_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U55_AG(x7, x8)
U56_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U56_AG(x7, x8)
U57_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U57_AG(x7, x8)
U58_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U58_AG(x1, x7, x8)
U59_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U59_AG(x1, x7, x8)
U60_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U60_AG(x1, x2, x7, x8)
U61_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U61_AG(x1, x2, x7, x8)
U62_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U62_AG(x1, x2, x3, x7, x8)
U63_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U63_AG(x1, x2, x3, x7, x8)
U64_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U64_AG(x1, x2, x3, x4, x7, x8)
U65_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U65_AG(x1, x2, x3, x4, x7, x8)
U66_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U66_AG(x7, x8)
U67_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U67_AG(x8, x9)
U68_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U68_AG(x1, x8, x9)
U69_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U69_AG(x1, x8, x9)
U70_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U70_AG(x1, x2, x8, x9)
U71_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U71_AG(x1, x2, x8, x9)
U72_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U72_AG(x1, x2, x3, x8, x9)
U73_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U73_AG(x1, x2, x3, x8, x9)
U74_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U74_AG(x1, x2, x3, x4, x8, x9)
U75_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U75_AG(x1, x2, x3, x4, x8, x9)
U76_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U76_AG(x8, x9)
U77_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U77_AG(x8, x9)
U78_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U78_AG(x8, x9)
U79_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U79_AG(x1, x8, x9)
U80_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_AG(x1, x8, x9)
U81_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_AG(x1, x2, x8, x9)
U82_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_AG(x1, x2, x8, x9)
U83_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_AG(x1, x2, x3, x8, x9)
U84_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U84_AG(x1, x2, x3, x8, x9)
U85_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U85_AG(x1, x2, x3, x4, x8, x9)
U86_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U86_AG(x1, x2, x3, x4, x8, x9)
U87_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U87_AG(x1, x2, x3, x4, x5, x8, x9)
U88_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U88_AG(x1, x2, x3, x4, x5, x8, x9)
U89_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U89_AG(x8, x9)
U90_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U90_AG(x9, x10)
U91_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U91_AG(x1, x9, x10)
U92_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U92_AG(x1, x9, x10)
U93_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U93_AG(x1, x2, x9, x10)
U94_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U94_AG(x1, x2, x9, x10)
U95_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U95_AG(x1, x2, x3, x9, x10)
U96_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U96_AG(x1, x2, x3, x9, x10)
U97_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U97_AG(x1, x2, x3, x4, x9, x10)
U98_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U98_AG(x1, x2, x3, x4, x9, x10)
U99_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U99_AG(x1, x2, x3, x4, x5, x9, x10)
U100_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U100_AG(x1, x2, x3, x4, x5, x9, x10)
U101_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U101_AG(x9, x10)
U102_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U102_AG(x9, x10)
U103_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U103_AG(x9, x10)
U104_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U104_AG(x1, x9, x10)
U105_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U105_AG(x1, x9, x10)
U106_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U106_AG(x1, x2, x9, x10)
U107_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U107_AG(x1, x2, x9, x10)
U108_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U108_AG(x1, x2, x3, x9, x10)
U109_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U109_AG(x1, x2, x3, x9, x10)
U110_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U110_AG(x1, x2, x3, x4, x9, x10)
U111_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U111_AG(x1, x2, x3, x4, x9, x10)
U112_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U112_AG(x1, x2, x3, x4, x5, x9, x10)
U113_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U113_AG(x1, x2, x3, x4, x5, x9, x10)
U114_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U114_AG(x1, x2, x3, x4, x5, x6, x9, x10)
U115_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U115_AG(x1, x2, x3, x4, x5, x6, x9, x10)
U116_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U116_AG(x9, x10)
U117_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U117_AG(x10, x11)
U118_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U118_AG(x1, x10, x11)
U119_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U119_AG(x1, x10, x11)
U120_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U120_AG(x1, x2, x10, x11)
U121_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U121_AG(x1, x2, x10, x11)
U122_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U122_AG(x1, x2, x3, x10, x11)
U123_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U123_AG(x1, x2, x3, x10, x11)
U124_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U124_AG(x1, x2, x3, x4, x10, x11)
U125_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U125_AG(x1, x2, x3, x4, x10, x11)
U126_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U126_AG(x1, x2, x3, x4, x5, x10, x11)
U127_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U127_AG(x1, x2, x3, x4, x5, x10, x11)
U128_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U128_AG(x1, x2, x3, x4, x5, x6, x10, x11)
U129_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U129_AG(x1, x2, x3, x4, x5, x6, x10, x11)
U130_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U130_AG(x1, x2, x3, x4, x5, x6, x7, x10, x11)
U131_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U131_AG(x10, x11)
P184_IN_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  P184_IN_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11)
U8_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U8_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U9_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U9_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U10_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U10_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U11_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U11_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U12_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U12_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U13_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U13_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
SUBSETCHECKED188_IN_AGGG(x1, x2, x3, x4)  =  SUBSETCHECKED188_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5, x6)  =  U2_AGGG(x3, x4, x5, x6)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x3, x4, x5, x6)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x3, x4, x5, x6)
U5_AGGG(x1, x2, x3, x4, x5, x6)  =  U5_AGGG(x3, x4, x5, x6)
U6_AGGG(x1, x2, x3, x4, x5, x6)  =  U6_AGGG(x1, x3, x4, x5, x6)
U7_AGGG(x1, x2, x3, x4, x5, x6)  =  U7_AGGG(x3, x4, x5, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

SUBSET1_IN_AG(.(T22, T23), T21) → U14_AG(T22, T23, T21, member12_in_ag(T22, T21))
SUBSET1_IN_AG(.(T22, T23), T21) → MEMBER12_IN_AG(T22, T21)
MEMBER12_IN_AG(T53, .(T51, T52)) → U1_AG(T53, T51, T52, member12_in_ag(T53, T52))
MEMBER12_IN_AG(T53, .(T51, T52)) → MEMBER12_IN_AG(T53, T52)
SUBSET1_IN_AG(.(T106, .(T108, T109)), T107) → U15_AG(T106, T108, T109, T107, memberc12_in_ag(T106, T107))
U15_AG(T106, T108, T109, T107, memberc12_out_ag(T106, T107)) → U16_AG(T106, T108, T109, T107, not_memberc22_in_g(T106))
U16_AG(T106, T108, T109, T107, not_memberc22_out_g(T106)) → U17_AG(T106, T108, T109, T107, member12_in_ag(T108, T107))
U16_AG(T106, T108, T109, T107, not_memberc22_out_g(T106)) → MEMBER12_IN_AG(T108, T107)
SUBSET1_IN_AG(.(T137, .(T136, T115)), T107) → U18_AG(T137, T136, T115, T107, memberc12_in_ag(T137, T107))
U18_AG(T137, T136, T115, T107, memberc12_out_ag(T137, T107)) → U19_AG(T137, T136, T115, T107, not_memberc22_in_g(T137))
U19_AG(T137, T136, T115, T107, not_memberc22_out_g(T137)) → U20_AG(T137, T136, T115, T107, memberc12_in_ag(T136, T107))
U20_AG(T137, T136, T115, T107, memberc12_out_ag(T136, T107)) → U21_AG(T137, T136, T115, T107, member12_in_gg(T136, .(T137, [])))
U20_AG(T137, T136, T115, T107, memberc12_out_ag(T136, T107)) → MEMBER12_IN_GG(T136, .(T137, []))
MEMBER12_IN_GG(T53, .(T51, T52)) → U1_GG(T53, T51, T52, member12_in_gg(T53, T52))
MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)
SUBSET1_IN_AG(.(T182, .(T181, .(T184, T185))), T183) → U22_AG(T182, T181, T184, T185, T183, memberc12_in_ag(T182, T183))
U22_AG(T182, T181, T184, T185, T183, memberc12_out_ag(T182, T183)) → U23_AG(T182, T181, T184, T185, T183, not_memberc22_in_g(T182))
U23_AG(T182, T181, T184, T185, T183, not_memberc22_out_g(T182)) → U24_AG(T182, T181, T184, T185, T183, memberc12_in_ag(T181, T183))
U24_AG(T182, T181, T184, T185, T183, memberc12_out_ag(T181, T183)) → U25_AG(T182, T181, T184, T185, T183, not_memberc48_in_gg(T181, T182))
U25_AG(T182, T181, T184, T185, T183, not_memberc48_out_gg(T181, T182)) → U26_AG(T182, T181, T184, T185, T183, member12_in_ag(T184, T183))
U25_AG(T182, T181, T184, T185, T183, not_memberc48_out_gg(T181, T182)) → MEMBER12_IN_AG(T184, T183)
SUBSET1_IN_AG(.(T224, .(T223, .(T222, T191))), T183) → U27_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T224, T183))
U27_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T224, T183)) → U28_AG(T224, T223, T222, T191, T183, not_memberc22_in_g(T224))
U28_AG(T224, T223, T222, T191, T183, not_memberc22_out_g(T224)) → U29_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T223, T183))
U29_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T223, T183)) → U30_AG(T224, T223, T222, T191, T183, not_memberc48_in_gg(T223, T224))
U30_AG(T224, T223, T222, T191, T183, not_memberc48_out_gg(T223, T224)) → U31_AG(T224, T223, T222, T191, T183, memberc12_in_ag(T222, T183))
U31_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T222, T183)) → U32_AG(T224, T223, T222, T191, T183, member12_in_gg(T222, .(T223, .(T224, []))))
U31_AG(T224, T223, T222, T191, T183, memberc12_out_ag(T222, T183)) → MEMBER12_IN_GG(T222, .(T223, .(T224, [])))
SUBSET1_IN_AG(.(T286, .(T285, .(T284, .(T288, T289)))), T287) → U33_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T286, T287))
U33_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T286, T287)) → U34_AG(T286, T285, T284, T288, T289, T287, not_memberc22_in_g(T286))
U34_AG(T286, T285, T284, T288, T289, T287, not_memberc22_out_g(T286)) → U35_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T285, T287))
U35_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T285, T287)) → U36_AG(T286, T285, T284, T288, T289, T287, not_memberc48_in_gg(T285, T286))
U36_AG(T286, T285, T284, T288, T289, T287, not_memberc48_out_gg(T285, T286)) → U37_AG(T286, T285, T284, T288, T289, T287, memberc12_in_ag(T284, T287))
U37_AG(T286, T285, T284, T288, T289, T287, memberc12_out_ag(T284, T287)) → U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_in_ggg(T284, T285, T286))
U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_out_ggg(T284, T285, T286)) → U39_AG(T286, T285, T284, T288, T289, T287, member12_in_ag(T288, T287))
U38_AG(T286, T285, T284, T288, T289, T287, not_memberc71_out_ggg(T284, T285, T286)) → MEMBER12_IN_AG(T288, T287)
SUBSET1_IN_AG(.(T339, .(T338, .(T337, .(T336, T295)))), T287) → U40_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T339, T287))
U40_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T339, T287)) → U41_AG(T339, T338, T337, T336, T295, T287, not_memberc22_in_g(T339))
U41_AG(T339, T338, T337, T336, T295, T287, not_memberc22_out_g(T339)) → U42_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T338, T287))
U42_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T338, T287)) → U43_AG(T339, T338, T337, T336, T295, T287, not_memberc48_in_gg(T338, T339))
U43_AG(T339, T338, T337, T336, T295, T287, not_memberc48_out_gg(T338, T339)) → U44_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T337, T287))
U44_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T337, T287)) → U45_AG(T339, T338, T337, T336, T295, T287, not_memberc71_in_ggg(T337, T338, T339))
U45_AG(T339, T338, T337, T336, T295, T287, not_memberc71_out_ggg(T337, T338, T339)) → U46_AG(T339, T338, T337, T336, T295, T287, memberc12_in_ag(T336, T287))
U46_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T336, T287)) → U47_AG(T339, T338, T337, T336, T295, T287, member12_in_gg(T336, .(T337, .(T338, .(T339, [])))))
U46_AG(T339, T338, T337, T336, T295, T287, memberc12_out_ag(T336, T287)) → MEMBER12_IN_GG(T336, .(T337, .(T338, .(T339, []))))
SUBSET1_IN_AG(.(T418, .(T417, .(T416, .(T415, .(T420, T421))))), T419) → U48_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T418, T419))
U48_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T418, T419)) → U49_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc22_in_g(T418))
U49_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc22_out_g(T418)) → U50_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T417, T419))
U50_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T417, T419)) → U51_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc48_in_gg(T417, T418))
U51_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc48_out_gg(T417, T418)) → U52_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T416, T419))
U52_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T416, T419)) → U53_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc71_in_ggg(T416, T417, T418))
U53_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc71_out_ggg(T416, T417, T418)) → U54_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_in_ag(T415, T419))
U54_AG(T418, T417, T416, T415, T420, T421, T419, memberc12_out_ag(T415, T419)) → U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_in_gggg(T415, T416, T417, T418))
U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_out_gggg(T415, T416, T417, T418)) → U56_AG(T418, T417, T416, T415, T420, T421, T419, member12_in_ag(T420, T419))
U55_AG(T418, T417, T416, T415, T420, T421, T419, not_memberc94_out_gggg(T415, T416, T417, T418)) → MEMBER12_IN_AG(T420, T419)
SUBSET1_IN_AG(.(T482, .(T481, .(T480, .(T479, .(T478, T427))))), T419) → U57_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T482, T419))
U57_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T482, T419)) → U58_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc22_in_g(T482))
U58_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc22_out_g(T482)) → U59_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T481, T419))
U59_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T481, T419)) → U60_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc48_in_gg(T481, T482))
U60_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc48_out_gg(T481, T482)) → U61_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T480, T419))
U61_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T480, T419)) → U62_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc71_in_ggg(T480, T481, T482))
U62_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc71_out_ggg(T480, T481, T482)) → U63_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T479, T419))
U63_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T479, T419)) → U64_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc94_in_gggg(T479, T480, T481, T482))
U64_AG(T482, T481, T480, T479, T478, T427, T419, not_memberc94_out_gggg(T479, T480, T481, T482)) → U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_in_ag(T478, T419))
U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T478, T419)) → U66_AG(T482, T481, T480, T479, T478, T427, T419, member12_in_gg(T478, .(T479, .(T480, .(T481, .(T482, []))))))
U65_AG(T482, T481, T480, T479, T478, T427, T419, memberc12_out_ag(T478, T419)) → MEMBER12_IN_GG(T478, .(T479, .(T480, .(T481, .(T482, [])))))
SUBSET1_IN_AG(.(T578, .(T577, .(T576, .(T575, .(T574, .(T580, T581)))))), T579) → U67_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T578, T579))
U67_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T578, T579)) → U68_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc22_in_g(T578))
U68_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc22_out_g(T578)) → U69_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T577, T579))
U69_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T577, T579)) → U70_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc48_in_gg(T577, T578))
U70_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc48_out_gg(T577, T578)) → U71_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T576, T579))
U71_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T576, T579)) → U72_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc71_in_ggg(T576, T577, T578))
U72_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc71_out_ggg(T576, T577, T578)) → U73_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T575, T579))
U73_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T575, T579)) → U74_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc94_in_gggg(T575, T576, T577, T578))
U74_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc94_out_gggg(T575, T576, T577, T578)) → U75_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_in_ag(T574, T579))
U75_AG(T578, T577, T576, T575, T574, T580, T581, T579, memberc12_out_ag(T574, T579)) → U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_in_ggggg(T574, T575, T576, T577, T578))
U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_out_ggggg(T574, T575, T576, T577, T578)) → U77_AG(T578, T577, T576, T575, T574, T580, T581, T579, member12_in_ag(T580, T579))
U76_AG(T578, T577, T576, T575, T574, T580, T581, T579, not_memberc117_out_ggggg(T574, T575, T576, T577, T578)) → MEMBER12_IN_AG(T580, T579)
SUBSET1_IN_AG(.(T653, .(T652, .(T651, .(T650, .(T649, .(T648, T587)))))), T579) → U78_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T653, T579))
U78_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T653, T579)) → U79_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc22_in_g(T653))
U79_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc22_out_g(T653)) → U80_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T652, T579))
U80_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T652, T579)) → U81_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc48_in_gg(T652, T653))
U81_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc48_out_gg(T652, T653)) → U82_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T651, T579))
U82_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T651, T579)) → U83_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc71_in_ggg(T651, T652, T653))
U83_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc71_out_ggg(T651, T652, T653)) → U84_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T650, T579))
U84_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T650, T579)) → U85_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc94_in_gggg(T650, T651, T652, T653))
U85_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc94_out_gggg(T650, T651, T652, T653)) → U86_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T649, T579))
U86_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T649, T579)) → U87_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc117_in_ggggg(T649, T650, T651, T652, T653))
U87_AG(T653, T652, T651, T650, T649, T648, T587, T579, not_memberc117_out_ggggg(T649, T650, T651, T652, T653)) → U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_in_ag(T648, T579))
U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T648, T579)) → U89_AG(T653, T652, T651, T650, T649, T648, T587, T579, member12_in_gg(T648, .(T649, .(T650, .(T651, .(T652, .(T653, [])))))))
U88_AG(T653, T652, T651, T650, T649, T648, T587, T579, memberc12_out_ag(T648, T579)) → MEMBER12_IN_GG(T648, .(T649, .(T650, .(T651, .(T652, .(T653, []))))))
SUBSET1_IN_AG(.(T766, .(T765, .(T764, .(T763, .(T762, .(T761, .(T768, T769))))))), T767) → U90_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T766, T767))
U90_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T766, T767)) → U91_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc22_in_g(T766))
U91_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc22_out_g(T766)) → U92_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T765, T767))
U92_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T765, T767)) → U93_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc48_in_gg(T765, T766))
U93_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc48_out_gg(T765, T766)) → U94_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T764, T767))
U94_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T764, T767)) → U95_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc71_in_ggg(T764, T765, T766))
U95_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc71_out_ggg(T764, T765, T766)) → U96_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T763, T767))
U96_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T763, T767)) → U97_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc94_in_gggg(T763, T764, T765, T766))
U97_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc94_out_gggg(T763, T764, T765, T766)) → U98_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T762, T767))
U98_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T762, T767)) → U99_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc117_in_ggggg(T762, T763, T764, T765, T766))
U99_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc117_out_ggggg(T762, T763, T764, T765, T766)) → U100_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_in_ag(T761, T767))
U100_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, memberc12_out_ag(T761, T767)) → U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_in_gggggg(T761, T762, T763, T764, T765, T766))
U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_out_gggggg(T761, T762, T763, T764, T765, T766)) → U102_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, member12_in_ag(T768, T767))
U101_AG(T766, T765, T764, T763, T762, T761, T768, T769, T767, not_memberc140_out_gggggg(T761, T762, T763, T764, T765, T766)) → MEMBER12_IN_AG(T768, T767)
SUBSET1_IN_AG(.(T852, .(T851, .(T850, .(T849, .(T848, .(T847, .(T846, T775))))))), T767) → U103_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T852, T767))
U103_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T852, T767)) → U104_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc22_in_g(T852))
U104_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc22_out_g(T852)) → U105_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T851, T767))
U105_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T851, T767)) → U106_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc48_in_gg(T851, T852))
U106_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc48_out_gg(T851, T852)) → U107_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T850, T767))
U107_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T850, T767)) → U108_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc71_in_ggg(T850, T851, T852))
U108_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc71_out_ggg(T850, T851, T852)) → U109_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T849, T767))
U109_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T849, T767)) → U110_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc94_in_gggg(T849, T850, T851, T852))
U110_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc94_out_gggg(T849, T850, T851, T852)) → U111_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T848, T767))
U111_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T848, T767)) → U112_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc117_in_ggggg(T848, T849, T850, T851, T852))
U112_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc117_out_ggggg(T848, T849, T850, T851, T852)) → U113_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T847, T767))
U113_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T847, T767)) → U114_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc140_in_gggggg(T847, T848, T849, T850, T851, T852))
U114_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, not_memberc140_out_gggggg(T847, T848, T849, T850, T851, T852)) → U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_in_ag(T846, T767))
U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T846, T767)) → U116_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, member12_in_gg(T846, .(T847, .(T848, .(T849, .(T850, .(T851, .(T852, []))))))))
U115_AG(T852, T851, T850, T849, T848, T847, T846, T775, T767, memberc12_out_ag(T846, T767)) → MEMBER12_IN_GG(T846, .(T847, .(T848, .(T849, .(T850, .(T851, .(T852, [])))))))
SUBSET1_IN_AG(.(T982, .(T981, .(T980, .(T979, .(T978, .(T977, .(T976, .(T984, T985)))))))), T983) → U117_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T982, T983))
U117_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T982, T983)) → U118_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc22_in_g(T982))
U118_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc22_out_g(T982)) → U119_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T981, T983))
U119_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T981, T983)) → U120_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc48_in_gg(T981, T982))
U120_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc48_out_gg(T981, T982)) → U121_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T980, T983))
U121_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T980, T983)) → U122_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc71_in_ggg(T980, T981, T982))
U122_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc71_out_ggg(T980, T981, T982)) → U123_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T979, T983))
U123_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T979, T983)) → U124_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc94_in_gggg(T979, T980, T981, T982))
U124_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc94_out_gggg(T979, T980, T981, T982)) → U125_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T978, T983))
U125_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T978, T983)) → U126_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc117_in_ggggg(T978, T979, T980, T981, T982))
U126_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc117_out_ggggg(T978, T979, T980, T981, T982)) → U127_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T977, T983))
U127_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T977, T983)) → U128_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc140_in_gggggg(T977, T978, T979, T980, T981, T982))
U128_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc140_out_gggggg(T977, T978, T979, T980, T981, T982)) → U129_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_in_ag(T976, T983))
U129_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, memberc12_out_ag(T976, T983)) → U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_in_ggggggg(T976, T977, T978, T979, T980, T981, T982))
U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_out_ggggggg(T976, T977, T978, T979, T980, T981, T982)) → U131_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, p184_in_aggggggggag(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, .(T976, .(T977, .(T978, .(T979, .(T980, .(T981, .(T982, [])))))))))
U130_AG(T982, T981, T980, T979, T978, T977, T976, T984, T985, T983, not_memberc163_out_ggggggg(T976, T977, T978, T979, T980, T981, T982)) → P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, .(T976, .(T977, .(T978, .(T979, .(T980, .(T981, .(T982, []))))))))
P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990) → U8_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990, member12_in_ag(T984, T983))
P184_IN_AGGGGGGGGAG(T984, T983, T976, T977, T978, T979, T980, T981, T982, T985, T990) → MEMBER12_IN_AG(T984, T983)
P184_IN_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990) → U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_in_ag(T1077, T983))
U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_out_ag(T1077, T983)) → U10_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, member12_in_gg(T1077, .(T1078, .(T1079, .(T1080, .(T1081, .(T1082, .(T1083, .(T1084, [])))))))))
U9_AGGGGGGGGAG(T1077, T983, T1078, T1079, T1080, T1081, T1082, T1083, T1084, T996, T990, memberc12_out_ag(T1077, T983)) → MEMBER12_IN_GG(T1077, .(T1078, .(T1079, .(T1080, .(T1081, .(T1082, .(T1083, .(T1084, []))))))))
P184_IN_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990) → U11_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, memberc12_in_ag(T995, T983))
U11_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, memberc12_out_ag(T995, T983)) → U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_in_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982))
U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_out_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982)) → U13_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, subsetchecked188_in_aggg(T996, T995, T990, T983))
U12_AGGGGGGGGAG(T995, T983, T976, T977, T978, T979, T980, T981, T982, T996, T990, not_memberc187_out_gggggggg(T995, T976, T977, T978, T979, T980, T981, T982)) → SUBSETCHECKED188_IN_AGGG(T996, T995, T990, T983)
SUBSETCHECKED188_IN_AGGG(.(T1173, T1174), T1170, T1171, T1172) → U2_AGGG(T1173, T1174, T1170, T1171, T1172, member12_in_ag(T1173, T1172))
SUBSETCHECKED188_IN_AGGG(.(T1173, T1174), T1170, T1171, T1172) → MEMBER12_IN_AG(T1173, T1172)
SUBSETCHECKED188_IN_AGGG(.(T1211, T1180), T1212, T1213, T1172) → U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_in_ag(T1211, T1172))
U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_out_ag(T1211, T1172)) → U4_AGGG(T1211, T1180, T1212, T1213, T1172, member12_in_gg(T1211, .(T1212, T1213)))
U3_AGGG(T1211, T1180, T1212, T1213, T1172, memberc12_out_ag(T1211, T1172)) → MEMBER12_IN_GG(T1211, .(T1212, T1213))
SUBSETCHECKED188_IN_AGGG(.(T1179, T1180), T1170, T1171, T1172) → U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_in_ag(T1179, T1172))
U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → U7_AGGG(T1179, T1180, T1170, T1171, T1172, subsetchecked188_in_aggg(T1180, T1179, .(T1170, T1171), T1172))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1180, T1179, .(T1170, T1171), T1172)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))
not_memberc22_in_g(T81) → not_memberc22_out_g(T81)
not_memberc48_in_gg(T146, T147) → not_memberc48_out_gg(T146, T147)
not_memberc71_in_ggg(T239, T240, T241) → not_memberc71_out_ggg(T239, T240, T241)
not_memberc94_in_gggg(T360, T361, T362, T363) → not_memberc94_out_gggg(T360, T361, T362, T363)
not_memberc117_in_ggggg(T509, T510, T511, T512, T513) → not_memberc117_out_ggggg(T509, T510, T511, T512, T513)
not_memberc140_in_gggggg(T686, T687, T688, T689, T690, T691) → not_memberc140_out_gggggg(T686, T687, T688, T689, T690, T691)
not_memberc163_in_ggggggg(T891, T892, T893, T894, T895, T896, T897) → not_memberc163_out_ggggggg(T891, T892, T893, T894, T895, T896, T897)
not_memberc187_in_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136) → not_memberc187_out_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136)
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)

The argument filtering Pi contains the following mapping:
member12_in_ag(x1, x2)  =  member12_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc22_in_g(x1)  =  not_memberc22_in_g(x1)
not_memberc22_out_g(x1)  =  not_memberc22_out_g(x1)
member12_in_gg(x1, x2)  =  member12_in_gg(x1, x2)
[]  =  []
not_memberc48_in_gg(x1, x2)  =  not_memberc48_in_gg(x1, x2)
not_memberc48_out_gg(x1, x2)  =  not_memberc48_out_gg(x1, x2)
not_memberc71_in_ggg(x1, x2, x3)  =  not_memberc71_in_ggg(x1, x2, x3)
not_memberc71_out_ggg(x1, x2, x3)  =  not_memberc71_out_ggg(x1, x2, x3)
not_memberc94_in_gggg(x1, x2, x3, x4)  =  not_memberc94_in_gggg(x1, x2, x3, x4)
not_memberc94_out_gggg(x1, x2, x3, x4)  =  not_memberc94_out_gggg(x1, x2, x3, x4)
not_memberc117_in_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_in_ggggg(x1, x2, x3, x4, x5)
not_memberc117_out_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_out_ggggg(x1, x2, x3, x4, x5)
not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)
p184_in_aggggggggag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  p184_in_aggggggggag(x2, x3, x4, x5, x6, x7, x8, x9, x11)
not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
subsetchecked188_in_aggg(x1, x2, x3, x4)  =  subsetchecked188_in_aggg(x2, x3, x4)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
SUBSET1_IN_AG(x1, x2)  =  SUBSET1_IN_AG(x2)
U14_AG(x1, x2, x3, x4)  =  U14_AG(x3, x4)
MEMBER12_IN_AG(x1, x2)  =  MEMBER12_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x2, x3, x4)
U15_AG(x1, x2, x3, x4, x5)  =  U15_AG(x4, x5)
U16_AG(x1, x2, x3, x4, x5)  =  U16_AG(x4, x5)
U17_AG(x1, x2, x3, x4, x5)  =  U17_AG(x4, x5)
U18_AG(x1, x2, x3, x4, x5)  =  U18_AG(x4, x5)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x1, x4, x5)
U20_AG(x1, x2, x3, x4, x5)  =  U20_AG(x1, x4, x5)
U21_AG(x1, x2, x3, x4, x5)  =  U21_AG(x4, x5)
MEMBER12_IN_GG(x1, x2)  =  MEMBER12_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
U22_AG(x1, x2, x3, x4, x5, x6)  =  U22_AG(x5, x6)
U23_AG(x1, x2, x3, x4, x5, x6)  =  U23_AG(x1, x5, x6)
U24_AG(x1, x2, x3, x4, x5, x6)  =  U24_AG(x1, x5, x6)
U25_AG(x1, x2, x3, x4, x5, x6)  =  U25_AG(x5, x6)
U26_AG(x1, x2, x3, x4, x5, x6)  =  U26_AG(x5, x6)
U27_AG(x1, x2, x3, x4, x5, x6)  =  U27_AG(x5, x6)
U28_AG(x1, x2, x3, x4, x5, x6)  =  U28_AG(x1, x5, x6)
U29_AG(x1, x2, x3, x4, x5, x6)  =  U29_AG(x1, x5, x6)
U30_AG(x1, x2, x3, x4, x5, x6)  =  U30_AG(x1, x2, x5, x6)
U31_AG(x1, x2, x3, x4, x5, x6)  =  U31_AG(x1, x2, x5, x6)
U32_AG(x1, x2, x3, x4, x5, x6)  =  U32_AG(x5, x6)
U33_AG(x1, x2, x3, x4, x5, x6, x7)  =  U33_AG(x6, x7)
U34_AG(x1, x2, x3, x4, x5, x6, x7)  =  U34_AG(x1, x6, x7)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x1, x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x1, x2, x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x1, x2, x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7)  =  U39_AG(x6, x7)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x1, x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7)  =  U42_AG(x1, x6, x7)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x1, x2, x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x1, x2, x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7)  =  U45_AG(x1, x2, x3, x6, x7)
U46_AG(x1, x2, x3, x4, x5, x6, x7)  =  U46_AG(x1, x2, x3, x6, x7)
U47_AG(x1, x2, x3, x4, x5, x6, x7)  =  U47_AG(x6, x7)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U48_AG(x7, x8)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U49_AG(x1, x7, x8)
U50_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U50_AG(x1, x7, x8)
U51_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U51_AG(x1, x2, x7, x8)
U52_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U52_AG(x1, x2, x7, x8)
U53_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U53_AG(x1, x2, x3, x7, x8)
U54_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U54_AG(x1, x2, x3, x7, x8)
U55_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U55_AG(x7, x8)
U56_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U56_AG(x7, x8)
U57_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U57_AG(x7, x8)
U58_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U58_AG(x1, x7, x8)
U59_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U59_AG(x1, x7, x8)
U60_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U60_AG(x1, x2, x7, x8)
U61_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U61_AG(x1, x2, x7, x8)
U62_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U62_AG(x1, x2, x3, x7, x8)
U63_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U63_AG(x1, x2, x3, x7, x8)
U64_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U64_AG(x1, x2, x3, x4, x7, x8)
U65_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U65_AG(x1, x2, x3, x4, x7, x8)
U66_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U66_AG(x7, x8)
U67_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U67_AG(x8, x9)
U68_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U68_AG(x1, x8, x9)
U69_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U69_AG(x1, x8, x9)
U70_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U70_AG(x1, x2, x8, x9)
U71_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U71_AG(x1, x2, x8, x9)
U72_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U72_AG(x1, x2, x3, x8, x9)
U73_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U73_AG(x1, x2, x3, x8, x9)
U74_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U74_AG(x1, x2, x3, x4, x8, x9)
U75_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U75_AG(x1, x2, x3, x4, x8, x9)
U76_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U76_AG(x8, x9)
U77_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U77_AG(x8, x9)
U78_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U78_AG(x8, x9)
U79_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U79_AG(x1, x8, x9)
U80_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_AG(x1, x8, x9)
U81_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_AG(x1, x2, x8, x9)
U82_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_AG(x1, x2, x8, x9)
U83_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_AG(x1, x2, x3, x8, x9)
U84_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U84_AG(x1, x2, x3, x8, x9)
U85_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U85_AG(x1, x2, x3, x4, x8, x9)
U86_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U86_AG(x1, x2, x3, x4, x8, x9)
U87_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U87_AG(x1, x2, x3, x4, x5, x8, x9)
U88_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U88_AG(x1, x2, x3, x4, x5, x8, x9)
U89_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U89_AG(x8, x9)
U90_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U90_AG(x9, x10)
U91_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U91_AG(x1, x9, x10)
U92_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U92_AG(x1, x9, x10)
U93_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U93_AG(x1, x2, x9, x10)
U94_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U94_AG(x1, x2, x9, x10)
U95_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U95_AG(x1, x2, x3, x9, x10)
U96_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U96_AG(x1, x2, x3, x9, x10)
U97_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U97_AG(x1, x2, x3, x4, x9, x10)
U98_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U98_AG(x1, x2, x3, x4, x9, x10)
U99_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U99_AG(x1, x2, x3, x4, x5, x9, x10)
U100_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U100_AG(x1, x2, x3, x4, x5, x9, x10)
U101_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U101_AG(x9, x10)
U102_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U102_AG(x9, x10)
U103_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U103_AG(x9, x10)
U104_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U104_AG(x1, x9, x10)
U105_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U105_AG(x1, x9, x10)
U106_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U106_AG(x1, x2, x9, x10)
U107_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U107_AG(x1, x2, x9, x10)
U108_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U108_AG(x1, x2, x3, x9, x10)
U109_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U109_AG(x1, x2, x3, x9, x10)
U110_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U110_AG(x1, x2, x3, x4, x9, x10)
U111_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U111_AG(x1, x2, x3, x4, x9, x10)
U112_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U112_AG(x1, x2, x3, x4, x5, x9, x10)
U113_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U113_AG(x1, x2, x3, x4, x5, x9, x10)
U114_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U114_AG(x1, x2, x3, x4, x5, x6, x9, x10)
U115_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U115_AG(x1, x2, x3, x4, x5, x6, x9, x10)
U116_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U116_AG(x9, x10)
U117_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U117_AG(x10, x11)
U118_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U118_AG(x1, x10, x11)
U119_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U119_AG(x1, x10, x11)
U120_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U120_AG(x1, x2, x10, x11)
U121_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U121_AG(x1, x2, x10, x11)
U122_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U122_AG(x1, x2, x3, x10, x11)
U123_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U123_AG(x1, x2, x3, x10, x11)
U124_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U124_AG(x1, x2, x3, x4, x10, x11)
U125_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U125_AG(x1, x2, x3, x4, x10, x11)
U126_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U126_AG(x1, x2, x3, x4, x5, x10, x11)
U127_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U127_AG(x1, x2, x3, x4, x5, x10, x11)
U128_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U128_AG(x1, x2, x3, x4, x5, x6, x10, x11)
U129_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U129_AG(x1, x2, x3, x4, x5, x6, x10, x11)
U130_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U130_AG(x1, x2, x3, x4, x5, x6, x7, x10, x11)
U131_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U131_AG(x10, x11)
P184_IN_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  P184_IN_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11)
U8_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U8_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U9_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U9_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U10_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U10_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U11_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U11_AGGGGGGGGAG(x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U12_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U12_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
U13_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U13_AGGGGGGGGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11, x12)
SUBSETCHECKED188_IN_AGGG(x1, x2, x3, x4)  =  SUBSETCHECKED188_IN_AGGG(x2, x3, x4)
U2_AGGG(x1, x2, x3, x4, x5, x6)  =  U2_AGGG(x3, x4, x5, x6)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x3, x4, x5, x6)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x3, x4, x5, x6)
U5_AGGG(x1, x2, x3, x4, x5, x6)  =  U5_AGGG(x3, x4, x5, x6)
U6_AGGG(x1, x2, x3, x4, x5, x6)  =  U6_AGGG(x1, x3, x4, x5, x6)
U7_AGGG(x1, x2, x3, x4, x5, x6)  =  U7_AGGG(x3, x4, x5, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))
not_memberc22_in_g(T81) → not_memberc22_out_g(T81)
not_memberc48_in_gg(T146, T147) → not_memberc48_out_gg(T146, T147)
not_memberc71_in_ggg(T239, T240, T241) → not_memberc71_out_ggg(T239, T240, T241)
not_memberc94_in_gggg(T360, T361, T362, T363) → not_memberc94_out_gggg(T360, T361, T362, T363)
not_memberc117_in_ggggg(T509, T510, T511, T512, T513) → not_memberc117_out_ggggg(T509, T510, T511, T512, T513)
not_memberc140_in_gggggg(T686, T687, T688, T689, T690, T691) → not_memberc140_out_gggggg(T686, T687, T688, T689, T690, T691)
not_memberc163_in_ggggggg(T891, T892, T893, T894, T895, T896, T897) → not_memberc163_out_ggggggg(T891, T892, T893, T894, T895, T896, T897)
not_memberc187_in_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136) → not_memberc187_out_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136)
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc22_in_g(x1)  =  not_memberc22_in_g(x1)
not_memberc22_out_g(x1)  =  not_memberc22_out_g(x1)
not_memberc48_in_gg(x1, x2)  =  not_memberc48_in_gg(x1, x2)
not_memberc48_out_gg(x1, x2)  =  not_memberc48_out_gg(x1, x2)
not_memberc71_in_ggg(x1, x2, x3)  =  not_memberc71_in_ggg(x1, x2, x3)
not_memberc71_out_ggg(x1, x2, x3)  =  not_memberc71_out_ggg(x1, x2, x3)
not_memberc94_in_gggg(x1, x2, x3, x4)  =  not_memberc94_in_gggg(x1, x2, x3, x4)
not_memberc94_out_gggg(x1, x2, x3, x4)  =  not_memberc94_out_gggg(x1, x2, x3, x4)
not_memberc117_in_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_in_ggggg(x1, x2, x3, x4, x5)
not_memberc117_out_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_out_ggggg(x1, x2, x3, x4, x5)
not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
MEMBER12_IN_GG(x1, x2)  =  MEMBER12_IN_GG(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)

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

(12) 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:

  • MEMBER12_IN_GG(T53, .(T51, T52)) → MEMBER12_IN_GG(T53, T52)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

MEMBER12_IN_AG(T53, .(T51, T52)) → MEMBER12_IN_AG(T53, T52)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))
not_memberc22_in_g(T81) → not_memberc22_out_g(T81)
not_memberc48_in_gg(T146, T147) → not_memberc48_out_gg(T146, T147)
not_memberc71_in_ggg(T239, T240, T241) → not_memberc71_out_ggg(T239, T240, T241)
not_memberc94_in_gggg(T360, T361, T362, T363) → not_memberc94_out_gggg(T360, T361, T362, T363)
not_memberc117_in_ggggg(T509, T510, T511, T512, T513) → not_memberc117_out_ggggg(T509, T510, T511, T512, T513)
not_memberc140_in_gggggg(T686, T687, T688, T689, T690, T691) → not_memberc140_out_gggggg(T686, T687, T688, T689, T690, T691)
not_memberc163_in_ggggggg(T891, T892, T893, T894, T895, T896, T897) → not_memberc163_out_ggggggg(T891, T892, T893, T894, T895, T896, T897)
not_memberc187_in_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136) → not_memberc187_out_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136)
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc22_in_g(x1)  =  not_memberc22_in_g(x1)
not_memberc22_out_g(x1)  =  not_memberc22_out_g(x1)
not_memberc48_in_gg(x1, x2)  =  not_memberc48_in_gg(x1, x2)
not_memberc48_out_gg(x1, x2)  =  not_memberc48_out_gg(x1, x2)
not_memberc71_in_ggg(x1, x2, x3)  =  not_memberc71_in_ggg(x1, x2, x3)
not_memberc71_out_ggg(x1, x2, x3)  =  not_memberc71_out_ggg(x1, x2, x3)
not_memberc94_in_gggg(x1, x2, x3, x4)  =  not_memberc94_in_gggg(x1, x2, x3, x4)
not_memberc94_out_gggg(x1, x2, x3, x4)  =  not_memberc94_out_gggg(x1, x2, x3, x4)
not_memberc117_in_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_in_ggggg(x1, x2, x3, x4, x5)
not_memberc117_out_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_out_ggggg(x1, x2, x3, x4, x5)
not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
MEMBER12_IN_AG(x1, x2)  =  MEMBER12_IN_AG(x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

MEMBER12_IN_AG(T53, .(T51, T52)) → MEMBER12_IN_AG(T53, T52)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
MEMBER12_IN_AG(x1, x2)  =  MEMBER12_IN_AG(x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

MEMBER12_IN_AG(.(T51, T52)) → MEMBER12_IN_AG(T52)

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

(19) 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:

  • MEMBER12_IN_AG(.(T51, T52)) → MEMBER12_IN_AG(T52)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

SUBSETCHECKED188_IN_AGGG(.(T1179, T1180), T1170, T1171, T1172) → U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_in_ag(T1179, T1172))
U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1180, T1179, .(T1170, T1171), T1172)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))
not_memberc22_in_g(T81) → not_memberc22_out_g(T81)
not_memberc48_in_gg(T146, T147) → not_memberc48_out_gg(T146, T147)
not_memberc71_in_ggg(T239, T240, T241) → not_memberc71_out_ggg(T239, T240, T241)
not_memberc94_in_gggg(T360, T361, T362, T363) → not_memberc94_out_gggg(T360, T361, T362, T363)
not_memberc117_in_ggggg(T509, T510, T511, T512, T513) → not_memberc117_out_ggggg(T509, T510, T511, T512, T513)
not_memberc140_in_gggggg(T686, T687, T688, T689, T690, T691) → not_memberc140_out_gggggg(T686, T687, T688, T689, T690, T691)
not_memberc163_in_ggggggg(T891, T892, T893, T894, T895, T896, T897) → not_memberc163_out_ggggggg(T891, T892, T893, T894, T895, T896, T897)
not_memberc187_in_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136) → not_memberc187_out_gggggggg(T1129, T1130, T1131, T1132, T1133, T1134, T1135, T1136)
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc22_in_g(x1)  =  not_memberc22_in_g(x1)
not_memberc22_out_g(x1)  =  not_memberc22_out_g(x1)
not_memberc48_in_gg(x1, x2)  =  not_memberc48_in_gg(x1, x2)
not_memberc48_out_gg(x1, x2)  =  not_memberc48_out_gg(x1, x2)
not_memberc71_in_ggg(x1, x2, x3)  =  not_memberc71_in_ggg(x1, x2, x3)
not_memberc71_out_ggg(x1, x2, x3)  =  not_memberc71_out_ggg(x1, x2, x3)
not_memberc94_in_gggg(x1, x2, x3, x4)  =  not_memberc94_in_gggg(x1, x2, x3, x4)
not_memberc94_out_gggg(x1, x2, x3, x4)  =  not_memberc94_out_gggg(x1, x2, x3, x4)
not_memberc117_in_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_in_ggggg(x1, x2, x3, x4, x5)
not_memberc117_out_ggggg(x1, x2, x3, x4, x5)  =  not_memberc117_out_ggggg(x1, x2, x3, x4, x5)
not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_in_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)  =  not_memberc140_out_gggggg(x1, x2, x3, x4, x5, x6)
not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_in_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)  =  not_memberc163_out_ggggggg(x1, x2, x3, x4, x5, x6, x7)
not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_in_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)  =  not_memberc187_out_gggggggg(x1, x2, x3, x4, x5, x6, x7, x8)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
SUBSETCHECKED188_IN_AGGG(x1, x2, x3, x4)  =  SUBSETCHECKED188_IN_AGGG(x2, x3, x4)
U5_AGGG(x1, x2, x3, x4, x5, x6)  =  U5_AGGG(x3, x4, x5, x6)
U6_AGGG(x1, x2, x3, x4, x5, x6)  =  U6_AGGG(x1, x3, x4, x5, x6)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

SUBSETCHECKED188_IN_AGGG(.(T1179, T1180), T1170, T1171, T1172) → U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_in_ag(T1179, T1172))
U5_AGGG(T1179, T1180, T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171))
U6_AGGG(T1179, T1180, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1180, T1179, .(T1170, T1171), T1172)

The TRS R consists of the following rules:

memberc12_in_ag(T42, .(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(T53, .(T51, T52)) → U133_ag(T53, T51, T52, memberc12_in_ag(T53, T52))
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)
U133_ag(T53, T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
memberc12_in_ag(x1, x2)  =  memberc12_in_ag(x2)
memberc12_out_ag(x1, x2)  =  memberc12_out_ag(x1, x2)
U133_ag(x1, x2, x3, x4)  =  U133_ag(x2, x3, x4)
not_memberc210_in_ggg(x1, x2, x3)  =  not_memberc210_in_ggg(x1, x2, x3)
not_memberc210_out_ggg(x1, x2, x3)  =  not_memberc210_out_ggg(x1, x2, x3)
SUBSETCHECKED188_IN_AGGG(x1, x2, x3, x4)  =  SUBSETCHECKED188_IN_AGGG(x2, x3, x4)
U5_AGGG(x1, x2, x3, x4, x5, x6)  =  U5_AGGG(x3, x4, x5, x6)
U6_AGGG(x1, x2, x3, x4, x5, x6)  =  U6_AGGG(x1, x3, x4, x5, x6)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

SUBSETCHECKED188_IN_AGGG(T1170, T1171, T1172) → U5_AGGG(T1170, T1171, T1172, memberc12_in_ag(T1172))
U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171))
U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
not_memberc210_in_ggg(x0, x1, x2)
U133_ag(x0, x1, x2)

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

(26) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_in_ggg(T1179, T1170, T1171)) at position [4] we obtained the following new rules [LPAR04]:

U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171))

(27) Obligation:

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

SUBSETCHECKED188_IN_AGGG(T1170, T1171, T1172) → U5_AGGG(T1170, T1171, T1172, memberc12_in_ag(T1172))
U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)
U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
not_memberc210_in_ggg(T1228, T1229, T1230) → not_memberc210_out_ggg(T1228, T1229, T1230)
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
not_memberc210_in_ggg(x0, x1, x2)
U133_ag(x0, x1, x2)

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

(28) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(29) Obligation:

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

SUBSETCHECKED188_IN_AGGG(T1170, T1171, T1172) → U5_AGGG(T1170, T1171, T1172, memberc12_in_ag(T1172))
U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)
U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
not_memberc210_in_ggg(x0, x1, x2)
U133_ag(x0, x1, x2)

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

(30) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

not_memberc210_in_ggg(x0, x1, x2)

(31) Obligation:

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

SUBSETCHECKED188_IN_AGGG(T1170, T1171, T1172) → U5_AGGG(T1170, T1171, T1172, memberc12_in_ag(T1172))
U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)
U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(32) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(T1170, T1171, T1172) → U5_AGGG(T1170, T1171, T1172, memberc12_in_ag(T1172)) at position [3] we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), memberc12_out_ag(x0, .(x0, x1)))
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1)))

(33) Obligation:

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

U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)
U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171))
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), memberc12_out_ag(x0, .(x0, x1)))
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(34) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AGGG(T1170, T1171, T1172, memberc12_out_ag(T1179, T1172)) → U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) we obtained the following new rules [LPAR04]:

U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))

(35) Obligation:

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

U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172)
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), memberc12_out_ag(x0, .(x0, x1)))
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1)))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(36) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_AGGG(T1179, T1170, T1171, T1172, not_memberc210_out_ggg(T1179, T1170, T1171)) → SUBSETCHECKED188_IN_AGGG(T1179, .(T1170, T1171), T1172) we obtained the following new rules [LPAR04]:

U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))

(37) Obligation:

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

SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), memberc12_out_ag(x0, .(x0, x1)))
SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1)))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))
U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(38) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), memberc12_out_ag(x0, .(x0, x1))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))

(39) Obligation:

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

SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1)))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))
U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(40) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(y0, y1, .(x0, x1)) → U5_AGGG(y0, y1, .(x0, x1), U133_ag(x0, x1, memberc12_in_ag(x1))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))

(41) Obligation:

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

U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1))
U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))
U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(42) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(z2, .(z2, z3))) → U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) we obtained the following new rules [LPAR04]:

U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))

(43) Obligation:

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

U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1))
U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(44) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AGGG(z0, z1, .(z2, z3), memberc12_out_ag(x3, .(z2, z3))) → U6_AGGG(x3, z0, z1, .(z2, z3), not_memberc210_out_ggg(x3, z0, z1)) we obtained the following new rules [LPAR04]:

U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))

(45) Obligation:

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

U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3))
U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(46) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_AGGG(z2, z0, z1, .(z2, z3), not_memberc210_out_ggg(z2, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z2, .(z0, z1), .(z2, z3)) we obtained the following new rules [LPAR04]:

U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))

(47) Obligation:

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

U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(48) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_AGGG(z4, z0, z1, .(z2, z3), not_memberc210_out_ggg(z4, z0, z1)) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, z1), .(z2, z3)) we obtained the following new rules [LPAR04]:

U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))

(49) Obligation:

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

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(50) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))

(51) Obligation:

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

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(52) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), memberc12_out_ag(z1, .(z1, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), memberc12_out_ag(z4, .(z4, z5)))

(53) Obligation:

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

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), memberc12_out_ag(z1, .(z1, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), memberc12_out_ag(z4, .(z4, z5)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(54) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z0, z3)) → U5_AGGG(z0, .(z1, z2), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), U133_ag(z0, z4, memberc12_in_ag(z4)))

(55) Obligation:

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

SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), memberc12_out_ag(z1, .(z1, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), memberc12_out_ag(z4, .(z4, z5)))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), U133_ag(z0, z4, memberc12_in_ag(z4)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(56) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED188_IN_AGGG(z0, .(z1, z2), .(z3, z4)) → U5_AGGG(z0, .(z1, z2), .(z3, z4), U133_ag(z3, z4, memberc12_in_ag(z4))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), U133_ag(z0, z4, memberc12_in_ag(z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), U133_ag(z1, z4, memberc12_in_ag(z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), U133_ag(z4, z5, memberc12_in_ag(z5)))

(57) Obligation:

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

U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(z3, .(z3, z4))) → U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(x4, .(z0, z3))) → U6_AGGG(x4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U5_AGGG(z0, .(z1, z2), .(z3, z4), memberc12_out_ag(x4, .(z3, z4))) → U6_AGGG(x4, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(x4, z0, .(z1, z2)))
U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z3, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z3, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z3, .(z0, .(z1, z2)), .(z3, z4))
U6_AGGG(z4, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z4, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z4, .(z0, .(z1, z2)), .(z0, z3))
U6_AGGG(z5, z0, .(z1, z2), .(z3, z4), not_memberc210_out_ggg(z5, z0, .(z1, z2))) → SUBSETCHECKED188_IN_AGGG(z5, .(z0, .(z1, z2)), .(z3, z4))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), memberc12_out_ag(z0, .(z0, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), memberc12_out_ag(z1, .(z1, z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), memberc12_out_ag(z4, .(z4, z5)))
SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3)) → U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), U133_ag(z0, z3, memberc12_in_ag(z3)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z0, z4), U133_ag(z0, z4, memberc12_in_ag(z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z1, z4), U133_ag(z1, z4, memberc12_in_ag(z4)))
SUBSETCHECKED188_IN_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5)) → U5_AGGG(z0, .(z1, .(z2, z3)), .(z4, z5), U133_ag(z4, z5, memberc12_in_ag(z5)))

The TRS R consists of the following rules:

memberc12_in_ag(.(T42, T43)) → memberc12_out_ag(T42, .(T42, T43))
memberc12_in_ag(.(T51, T52)) → U133_ag(T51, T52, memberc12_in_ag(T52))
U133_ag(T51, T52, memberc12_out_ag(T53, T52)) → memberc12_out_ag(T53, .(T51, T52))

The set Q consists of the following terms:

memberc12_in_ag(x0)
U133_ag(x0, x1, x2)

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

(58) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2))) evaluates to t =U6_AGGG(z0, z0, .(z0, .(z1, z2)), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z0, .(z1, z2))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [z1 / z0, z2 / .(z1, z2)]
  • Semiunifier: [ ]




Rewriting sequence

U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))
with rule U6_AGGG(z0', z0', .(z1', z2'), .(z0', z3'), not_memberc210_out_ggg(z0', z0', .(z1', z2'))) → SUBSETCHECKED188_IN_AGGG(z0', .(z0', .(z1', z2')), .(z0', z3')) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2, z3' / z3]

SUBSETCHECKED188_IN_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3))U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))
with rule SUBSETCHECKED188_IN_AGGG(z0', .(z0', .(z1', z2')), .(z0', z3')) → U5_AGGG(z0', .(z0', .(z1', z2')), .(z0', z3'), memberc12_out_ag(z0', .(z0', z3'))) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2, z3' / z3]

U5_AGGG(z0, .(z0, .(z1, z2)), .(z0, z3), memberc12_out_ag(z0, .(z0, z3)))U6_AGGG(z0, z0, .(z0, .(z1, z2)), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z0, .(z1, z2))))
with rule U5_AGGG(z0, .(z1, z2), .(z0, z3), memberc12_out_ag(z0, .(z0, z3))) → U6_AGGG(z0, z0, .(z1, z2), .(z0, z3), not_memberc210_out_ggg(z0, z0, .(z1, z2)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(59) NO