Left Termination proof of ../tpdb/LP/talp/maria/zebra.pl

YES Left Termination proof of ../tpdb/LP/talp/maria/zebra.pl
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:

↳ Prolog

  ↳ PrologToPiTRSProof

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([], X).
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).

We use the technique of [30]. 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([], X) → domain_out_gg([], X)
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)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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([], X) → domain_out_gg([], X)
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)

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([], X) → domain_out_gg([], X)
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)
ZEBRA_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7) = ZEBRA_IN_AAAAAAA
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)
U3_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3_AAAAAAA(x10)
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)
DOMAIN_IN_GG(x1, x2) = DOMAIN_IN_GG(x1, x2)
U6_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = U6_AAAAAAA(x14)
U22_GG(x1, x2, x3, x4) = U22_GG(x4)
U21_GG(x1, x2, x3, x4) = U21_GG(x2, x4)
NEXT_TO_IN_GA(x1, x2) = NEXT_TO_IN_GA(x1)
U7_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U7_AAAAAAA(x16)
U4_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U4_AAAAAAA(x12)
U23_AGA(x1, x2, x3, x4, x5) = U23_AGA(x5)
EQ_IN_AA(x1, x2) = EQ_IN_AA
U9_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_AAAAAAA(x19)
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)
U5_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U5_AAAAAAA(x13)
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)
U20_G(x1, x2) = U20_G(x2)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U19_AAAAAAA(x5, x8)
SELECT_IN_AGA(x1, x2, x3) = SELECT_IN_AGA(x2)
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)
NEXT_TO_IN_AA(x1, x2) = NEXT_TO_IN_AA
U1_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U1_AAAAAAA(x8)
EQ_IN_AG(x1, x2) = EQ_IN_AG(x2)
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)
U8_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) = U8_AAAAAAA(x18)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U18_AAAAAAA(x5, x12)
U2_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2_AAAAAAA(x9)
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)
HOUSES_IN_G(x1) = HOUSES_IN_G(x1)
TO_THE_RIGHT_IN_AA(x1, x2) = TO_THE_RIGHT_IN_AA

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

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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([], X) → domain_out_gg([], X)
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)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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([], X) → domain_out_gg([], X)
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)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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.
By using the subterm criterion [20] together with the size-change analysis [32] 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

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, 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([], X) → domain_out_gg([], X)
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)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

DOMAIN_IN_GG(.(X, Rest), Domain) → U21_GG(X, Rest, Domain, select_in_aga(X, Domain, NewDomain))
U21_GG(X, Rest, Domain, select_out_aga(X, Domain, NewDomain)) → DOMAIN_IN_GG(Rest, 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(x3)
U23_aga(x1, x2, x3, x4, x5) = U23_aga(x5)
DOMAIN_IN_GG(x1, x2) = DOMAIN_IN_GG(x1, x2)
U21_GG(x1, x2, x3, x4) = U21_GG(x2, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

select_in_aga(x0)
U23_aga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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:

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