Left Termination of the query pattern zebra_in_7(a, a, a, a, a, a, a) w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

zebra(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) :- ','(eq(Englishman, Red), ','(eq(Spaniard, Dog), ','(eq(Green, Coffee), ','(eq(Ukrainian, Tea), ','(to_the_right(Green, Ivory), ','(eq(Winston, Snails), ','(eq(Kool, Yellow), ','(eq(Milk, third), ','(eq(Norwegian, first), ','(next_to(Fox, Chesterfield), ','(next_to(Horse, Kool), ','(eq(Lucky, Juice), ','(eq(Japanese, Parliament), ','(next_to(Norwegian, Blue), ','(houses(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))), ','(houses(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))), ','(houses(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))), ','(houses(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))), houses(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))))))))))))))))))).
houses(Prop) :- domain(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))).
domain([], X1).
domain(.(X, Rest), Domain) :- ','(select(X, Domain, NewDomain), domain(Rest, NewDomain)).
select(X, .(X, R), R).
select(X, .(Y, R), .(Y, Rest)) :- select(X, R, Rest).
next_to(fifth, fourth).
next_to(fourth, fifth).
next_to(fourth, third).
next_to(third, fourth).
next_to(third, second).
next_to(second, third).
next_to(second, first).
next_to(first, second).
to_the_right(fifth, fourth).
to_the_right(fourth, third).
to_the_right(third, second).
to_the_right(second, first).
eq(X, X).

Queries:

zebra(a,a,a,a,a,a,a).

(1) PrologToPiTRSProof (SOUND transformation)

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

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x4)
houses_out_g(x1)  =  houses_out_g
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x4)
houses_out_g(x1)  =  houses_out_g
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)

(3) PrologToPiTRSProof (SOUND transformation)

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

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN_AA(Englishman, Red)
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → EQ_IN_AA(Spaniard, Dog)
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → EQ_IN_AA(Green, Coffee)
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → EQ_IN_AA(Ukrainian, Tea)
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → TO_THE_RIGHT_IN_AA(Green, Ivory)
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → EQ_IN_AA(Winston, Snails)
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → EQ_IN_AA(Kool, Yellow)
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → EQ_IN_AG(Milk, third)
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → EQ_IN_AG(Norwegian, first)
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → NEXT_TO_IN_AA(Fox, Chesterfield)
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → NEXT_TO_IN_AA(Horse, Kool)
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → EQ_IN_AA(Lucky, Juice)
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → EQ_IN_AA(Japanese, Parliament)
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → NEXT_TO_IN_GA(Norwegian, Blue)
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → HOUSES_IN_G(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN_G(Prop) → U20_G(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN_G(Prop) → DOMAIN_IN_GG(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
DOMAIN_IN_GG(.(X, Rest), Domain) → SELECT_IN_AGA(X, Domain, NewDomain)
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → U23_AGA(X, Y, R, Rest, select_in_aga(X, R, Rest))
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_GG(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN_G(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN_G(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN_G(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN_G(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)
ZEBRA_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  ZEBRA_IN_AAAAAAA
U1_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAAA(x8)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U2_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_AAAAAAA(x9)
U3_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_AAAAAAA(x10)
U4_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_AAAAAAA(x12)
U5_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_AAAAAAA(x13)
TO_THE_RIGHT_IN_AA(x1, x2)  =  TO_THE_RIGHT_IN_AA
U6_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_AAAAAAA(x14)
U7_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_AAAAAAA(x16)
U8_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_AAAAAAA(x18)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U9_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_AAAAAAA(x19)
U10_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_AAAAAAA(x5, x19)
NEXT_TO_IN_AA(x1, x2)  =  NEXT_TO_IN_AA
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_AAAAAAA(x5, x21)
U12_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_AAAAAAA(x5, x22)
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_AAAAAAA(x5, x24)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_AAAAAAA(x5, x25)
NEXT_TO_IN_GA(x1, x2)  =  NEXT_TO_IN_GA(x1)
U15_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_AAAAAAA(x5, x21)
HOUSES_IN_G(x1)  =  HOUSES_IN_G(x1)
U20_G(x1, x2)  =  U20_G(x1, x2)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U21_GG(x1, x2, x3, x4)  =  U21_GG(x2, x3, x4)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U23_AGA(x1, x2, x3, x4, x5)  =  U23_AGA(x3, x5)
U22_GG(x1, x2, x3, x4)  =  U22_GG(x2, x3, x4)
U16_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_AAAAAAA(x5, x21)
U17_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_AAAAAAA(x5, x17)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_AAAAAAA(x5, x12)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAAAA(x5, x8)

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

(6) Obligation:

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

ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
ZEBRA_IN_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN_AA(Englishman, Red)
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U1_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → EQ_IN_AA(Spaniard, Dog)
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U2_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → EQ_IN_AA(Green, Coffee)
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U3_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → EQ_IN_AA(Ukrainian, Tea)
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
U4_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → TO_THE_RIGHT_IN_AA(Green, Ivory)
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U5_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → EQ_IN_AA(Winston, Snails)
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U6_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → EQ_IN_AA(Kool, Yellow)
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
U7_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → EQ_IN_AG(Milk, third)
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U8_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → EQ_IN_AG(Norwegian, first)
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
U9_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → NEXT_TO_IN_AA(Fox, Chesterfield)
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U10_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → NEXT_TO_IN_AA(Horse, Kool)
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U11_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → EQ_IN_AA(Lucky, Juice)
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U12_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → EQ_IN_AA(Japanese, Parliament)
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
U13_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → NEXT_TO_IN_GA(Norwegian, Blue)
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → HOUSES_IN_G(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN_G(Prop) → U20_G(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN_G(Prop) → DOMAIN_IN_GG(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
DOMAIN_IN_GG(.(X, Rest), Domain) → SELECT_IN_AGA(X, Domain, NewDomain)
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → U23_AGA(X, Y, R, Rest, select_in_aga(X, R, Rest))
SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_GG(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN_G(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN_G(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN_G(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18_AAAAAAA(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN_G(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)
ZEBRA_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  ZEBRA_IN_AAAAAAA
U1_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAAA(x8)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U2_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_AAAAAAA(x9)
U3_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_AAAAAAA(x10)
U4_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_AAAAAAA(x12)
U5_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_AAAAAAA(x13)
TO_THE_RIGHT_IN_AA(x1, x2)  =  TO_THE_RIGHT_IN_AA
U6_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_AAAAAAA(x14)
U7_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_AAAAAAA(x16)
U8_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_AAAAAAA(x18)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U9_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_AAAAAAA(x19)
U10_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_AAAAAAA(x5, x19)
NEXT_TO_IN_AA(x1, x2)  =  NEXT_TO_IN_AA
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_AAAAAAA(x5, x21)
U12_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_AAAAAAA(x5, x22)
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_AAAAAAA(x5, x24)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_AAAAAAA(x5, x25)
NEXT_TO_IN_GA(x1, x2)  =  NEXT_TO_IN_GA(x1)
U15_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_AAAAAAA(x5, x21)
HOUSES_IN_G(x1)  =  HOUSES_IN_G(x1)
U20_G(x1, x2)  =  U20_G(x1, x2)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U21_GG(x1, x2, x3, x4)  =  U21_GG(x2, x3, x4)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U23_AGA(x1, x2, x3, x4, x5)  =  U23_AGA(x3, x5)
U22_GG(x1, x2, x3, x4)  =  U22_GG(x2, x3, x4)
U16_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_AAAAAAA(x5, x21)
U17_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_AAAAAAA(x5, x17)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_AAAAAAA(x5, x12)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAAAA(x5, x8)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 43 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

SELECT_IN_AGA(X, .(Y, R), .(Y, Rest)) → SELECT_IN_AGA(X, R, Rest)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

SELECT_IN_AGA(.(R)) → SELECT_IN_AGA(R)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• SELECT_IN_AGA(.(R)) → SELECT_IN_AGA(R)
  The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))

The TRS R consists of the following rules:

zebra_in_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in_aa(Englishman, Red))
eq_in_aa(X, X) → eq_out_aa(X, X)
U1_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out_aa(Englishman, Red)) → U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in_aa(Spaniard, Dog))
U2_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out_aa(Spaniard, Dog)) → U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in_aa(Green, Coffee))
U3_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out_aa(Green, Coffee)) → U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in_aa(Ukrainian, Tea))
U4_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out_aa(Ukrainian, Tea)) → U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in_aa(Green, Ivory))
to_the_right_in_aa(fifth, fourth) → to_the_right_out_aa(fifth, fourth)
to_the_right_in_aa(fourth, third) → to_the_right_out_aa(fourth, third)
to_the_right_in_aa(third, second) → to_the_right_out_aa(third, second)
to_the_right_in_aa(second, first) → to_the_right_out_aa(second, first)
U5_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out_aa(Green, Ivory)) → U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in_aa(Winston, Snails))
U6_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out_aa(Winston, Snails)) → U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in_aa(Kool, Yellow))
U7_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out_aa(Kool, Yellow)) → U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in_ag(Milk, third))
eq_in_ag(X, X) → eq_out_ag(X, X)
U8_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out_ag(Milk, third)) → U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in_ag(Norwegian, first))
U9_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out_ag(Norwegian, first)) → U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in_aa(Fox, Chesterfield))
next_to_in_aa(fifth, fourth) → next_to_out_aa(fifth, fourth)
next_to_in_aa(fourth, fifth) → next_to_out_aa(fourth, fifth)
next_to_in_aa(fourth, third) → next_to_out_aa(fourth, third)
next_to_in_aa(third, fourth) → next_to_out_aa(third, fourth)
next_to_in_aa(third, second) → next_to_out_aa(third, second)
next_to_in_aa(second, third) → next_to_out_aa(second, third)
next_to_in_aa(second, first) → next_to_out_aa(second, first)
next_to_in_aa(first, second) → next_to_out_aa(first, second)
U10_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out_aa(Fox, Chesterfield)) → U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in_aa(Horse, Kool))
U11_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out_aa(Horse, Kool)) → U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in_aa(Lucky, Juice))
U12_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out_aa(Lucky, Juice)) → U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in_aa(Japanese, Parliament))
U13_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out_aa(Japanese, Parliament)) → U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in_ga(Norwegian, Blue))
next_to_in_ga(fifth, fourth) → next_to_out_ga(fifth, fourth)
next_to_in_ga(fourth, fifth) → next_to_out_ga(fourth, fifth)
next_to_in_ga(fourth, third) → next_to_out_ga(fourth, third)
next_to_in_ga(third, fourth) → next_to_out_ga(third, fourth)
next_to_in_ga(third, second) → next_to_out_ga(third, second)
next_to_in_ga(second, third) → next_to_out_ga(second, third)
next_to_in_ga(second, first) → next_to_out_ga(second, first)
next_to_in_ga(first, second) → next_to_out_ga(first, second)
U14_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out_ga(Norwegian, Blue)) → U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in_g(Prop) → U20_g(Prop, domain_in_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in_gg([], X1) → domain_out_gg([], X1)
domain_in_gg(.(X, Rest), Domain) → U21_gg(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))
U21_gg(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → U22_gg(X, Rest, Domain, domain_in_gg(Rest, NewDomain))
U22_gg(X, Rest, Domain, domain_out_gg(Rest, NewDomain)) → domain_out_gg(.(X, Rest), Domain)
U20_g(Prop, domain_out_gg(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out_g(Prop)
U15_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out_g(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out_g(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out_g(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out_g(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out_aaaaaaa(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_in_aaaaaaa
U1_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_aaaaaaa(x8)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
U2_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U2_aaaaaaa(x9)
U3_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U3_aaaaaaa(x10)
U4_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U4_aaaaaaa(x12)
U5_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U5_aaaaaaa(x13)
to_the_right_in_aa(x1, x2)  =  to_the_right_in_aa
to_the_right_out_aa(x1, x2)  =  to_the_right_out_aa(x1, x2)
U6_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  U6_aaaaaaa(x14)
U7_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  U7_aaaaaaa(x16)
U8_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  U8_aaaaaaa(x18)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
third  =  third
U9_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U9_aaaaaaa(x19)
first  =  first
U10_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U10_aaaaaaa(x5, x19)
next_to_in_aa(x1, x2)  =  next_to_in_aa
next_to_out_aa(x1, x2)  =  next_to_out_aa(x1, x2)
U11_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U11_aaaaaaa(x5, x21)
U12_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  U12_aaaaaaa(x5, x22)
U13_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  U13_aaaaaaa(x5, x24)
U14_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25)  =  U14_aaaaaaa(x5, x25)
next_to_in_ga(x1, x2)  =  next_to_in_ga(x1)
fifth  =  fifth
next_to_out_ga(x1, x2)  =  next_to_out_ga(x1, x2)
fourth  =  fourth
second  =  second
U15_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U15_aaaaaaa(x5, x21)
houses_in_g(x1)  =  houses_in_g(x1)
.(x1, x2)  =  .(x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg(x1, x2)
U21_gg(x1, x2, x3, x4)  =  U21_gg(x2, x3, x4)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
U22_gg(x1, x2, x3, x4)  =  U22_gg(x2, x3, x4)
houses_out_g(x1)  =  houses_out_g(x1)
U16_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U16_aaaaaaa(x5, x21)
U17_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U17_aaaaaaa(x5, x17)
U18_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U18_aaaaaaa(x5, x12)
U19_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_aaaaaaa(x5, x8)
zebra_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  zebra_out_aaaaaaa(x5)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U21_GG(x1, x2, x3, x4)  =  U21_GG(x2, x3, x4)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))

The TRS R consists of the following rules:

select_in_aga(X, .(X, R), R) → select_out_aga(X, .(X, R), R)
select_in_aga(X, .(Y, R), .(Y, Rest)) → U23_aga(X, Y, R, Rest, select_in_aga(X, R, Rest))
U23_aga(X, Y, R, Rest, select_out_aga(X, R, Rest)) → select_out_aga(X, .(Y, R), .(Y, Rest))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U23_aga(x1, x2, x3, x4, x5)  =  U23_aga(x3, x5)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U21_GG(x1, x2, x3, x4)  =  U21_GG(x2, x3, x4)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

U21_GG(Rest, Domain, select_out_aga(Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
DOMAIN_IN_GG(.(Rest), Domain) → U21_GG(Rest, Domain, select_in_aga(Domain))

The TRS R consists of the following rules:

select_in_aga(.(R)) → select_out_aga(.(R), R)
select_in_aga(.(R)) → U23_aga(R, select_in_aga(R))
U23_aga(R, select_out_aga(R, Rest)) → select_out_aga(.(R), .(Rest))

The set Q consists of the following terms:

select_in_aga(x0)
U23_aga(x0, x1)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• DOMAIN_IN_GG(.(Rest), Domain) → U21_GG(Rest, Domain, select_in_aga(Domain))
  The graph contains the following edges 1 > 1, 2 >= 2

• U21_GG(Rest, Domain, select_out_aga(Domain, NewDomain)) → DOMAIN_IN_GG(Rest, NewDomain)
  The graph contains the following edges 1 >= 1, 3 > 2

(22) TRUE