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



↳ PROLOG
  ↳ PrologToPiTRSProof

zebra7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) :- eq2(Englishman, Red), eq2(Spaniard, Dog), eq2(Green, Coffee), eq2(Ukrainian, Tea), totheright2(Green, Ivory), eq2(Winston, Snails), eq2(Kool, Yellow), eq2(Milk, third0), eq2(Norwegian, first0), nextto2(Fox, Chesterfield), nextto2(Horse, Kool), eq2(Lucky, Juice), eq2(Japanese, Parliament), nextto2(Norwegian, Blue), houses1(.2(Blue, .2(Green, .2(Red, .2(Yellow, .2(Ivory, {}0)))))), houses1(.2(Norwegian, .2(Englishman, .2(Spaniard, .2(Japanese, .2(Ukrainian, {}0)))))), houses1(.2(Dog, .2(Zebra, .2(Fox, .2(Snails, .2(Horse, {}0)))))), houses1(.2(Parliament, .2(Kool, .2(Lucky, .2(Chesterfield, .2(Winston, {}0)))))), houses1(.2(Milk, .2(Juice, .2(Water, .2(Tea, .2(Coffee, {}0)))))).
houses1(Prop) :- domain2(Prop, .2(first0, .2(second0, .2(third0, .2(fourth0, .2(fifth0, {}0)))))).
domain2({}0, underscore).
domain2(.2(X, Rest), Domain) :- select3(X, Domain, NewDomain), domain2(Rest, NewDomain).
select3(X, .2(X, R), R).
select3(X, .2(Y, R), .2(Y, Rest)) :- select3(X, R, Rest).
nextto2(fifth0, fourth0).
nextto2(fourth0, fifth0).
nextto2(fourth0, third0).
nextto2(third0, fourth0).
nextto2(third0, second0).
nextto2(second0, third0).
nextto2(second0, first0).
nextto2(first0, second0).
totheright2(fifth0, fourth0).
totheright2(fourth0, third0).
totheright2(third0, second0).
totheright2(second0, first0).
eq2(X, X).


With regard to the inferred argument filtering the predicates were used in the following modes:
zebra7: (f,f,f,f,f,f,f)
houses1: (f)
domain2: (f,b)
select3: (f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


zebra_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)

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_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)


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

ZEBRA_7_IN_AAAAAAA7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
ZEBRA_7_IN_AAAAAAA7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> EQ_2_IN_AA2(Englishman, Red)
IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> EQ_2_IN_AA2(Spaniard, Dog)
IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> EQ_2_IN_AA2(Green, Coffee)
IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> EQ_2_IN_AA2(Ukrainian, Tea)
IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> TO_THE_RIGHT_2_IN_AA2(Green, Ivory)
IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> EQ_2_IN_AA2(Winston, Snails)
IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> EQ_2_IN_AA2(Kool, Yellow)
IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> EQ_2_IN_AG2(Milk, third_0)
IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> EQ_2_IN_AG2(Norwegian, first_0)
IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> NEXT_TO_2_IN_AA2(Fox, Chesterfield)
IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> NEXT_TO_2_IN_AA2(Horse, Kool)
IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> EQ_2_IN_AA2(Lucky, Juice)
IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> EQ_2_IN_AA2(Japanese, Parliament)
IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_in_ga2(Norwegian, Blue))
IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> NEXT_TO_2_IN_GA2(Norwegian, Blue)
IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_out_ga2(Norwegian, Blue)) -> IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_out_ga2(Norwegian, Blue)) -> HOUSES_1_IN_A1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))
HOUSES_1_IN_A1(Prop) -> IF_HOUSES_1_IN_1_A2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
HOUSES_1_IN_A1(Prop) -> DOMAIN_2_IN_AG2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> SELECT_3_IN_AGA3(X, Domain, NewDomain)
SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> IF_SELECT_3_IN_1_AGA5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> SELECT_3_IN_AGA3(X, R, Rest)
IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> IF_DOMAIN_2_IN_2_AG5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> DOMAIN_2_IN_AG2(Rest, NewDomain)
IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> HOUSES_1_IN_A1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))
IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> HOUSES_1_IN_A1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))
IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> HOUSES_1_IN_A1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))
IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> IF_ZEBRA_7_IN_19_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> HOUSES_1_IN_A1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))

The TRS R consists of the following rules:

zebra_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)
IF_DOMAIN_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_DOMAIN_2_IN_1_AG1(x4)
IF_ZEBRA_7_IN_19_AAAAAAA12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  IF_ZEBRA_7_IN_19_AAAAAAA7(x1, x2, x3, x4, x5, x6, x12)
IF_ZEBRA_7_IN_3_AAAAAAA10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  IF_ZEBRA_7_IN_3_AAAAAAA1(x10)
IF_ZEBRA_7_IN_12_AAAAAAA22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  IF_ZEBRA_7_IN_12_AAAAAAA2(x5, x22)
IF_ZEBRA_7_IN_11_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_11_AAAAAAA2(x5, x21)
HOUSES_1_IN_A1(x1)  =  HOUSES_1_IN_A
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA2(x2, x5)
IF_ZEBRA_7_IN_1_AAAAAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ZEBRA_7_IN_1_AAAAAAA1(x8)
IF_ZEBRA_7_IN_14_AAAAAAA25(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)  =  IF_ZEBRA_7_IN_14_AAAAAAA2(x5, x25)
IF_ZEBRA_7_IN_4_AAAAAAA12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  IF_ZEBRA_7_IN_4_AAAAAAA1(x12)
EQ_2_IN_AG2(x1, x2)  =  EQ_2_IN_AG1(x2)
DOMAIN_2_IN_AG2(x1, x2)  =  DOMAIN_2_IN_AG1(x2)
IF_ZEBRA_7_IN_8_AAAAAAA18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_ZEBRA_7_IN_8_AAAAAAA1(x18)
EQ_2_IN_AA2(x1, x2)  =  EQ_2_IN_AA
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)
IF_ZEBRA_7_IN_5_AAAAAAA13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  IF_ZEBRA_7_IN_5_AAAAAAA1(x13)
IF_ZEBRA_7_IN_9_AAAAAAA19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_ZEBRA_7_IN_9_AAAAAAA1(x19)
TO_THE_RIGHT_2_IN_AA2(x1, x2)  =  TO_THE_RIGHT_2_IN_AA
IF_DOMAIN_2_IN_2_AG5(x1, x2, x3, x4, x5)  =  IF_DOMAIN_2_IN_2_AG2(x1, x5)
ZEBRA_7_IN_AAAAAAA7(x1, x2, x3, x4, x5, x6, x7)  =  ZEBRA_7_IN_AAAAAAA
IF_HOUSES_1_IN_1_A2(x1, x2)  =  IF_HOUSES_1_IN_1_A1(x2)
IF_ZEBRA_7_IN_13_AAAAAAA24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_ZEBRA_7_IN_13_AAAAAAA2(x5, x24)
NEXT_TO_2_IN_GA2(x1, x2)  =  NEXT_TO_2_IN_GA1(x1)
IF_ZEBRA_7_IN_10_AAAAAAA19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_ZEBRA_7_IN_10_AAAAAAA2(x5, x19)
IF_ZEBRA_7_IN_15_AAAAAAA26(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, x26)  =  IF_ZEBRA_7_IN_15_AAAAAAA2(x5, x26)
IF_ZEBRA_7_IN_16_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_16_AAAAAAA2(x5, x21)
NEXT_TO_2_IN_AA2(x1, x2)  =  NEXT_TO_2_IN_AA
IF_ZEBRA_7_IN_18_AAAAAAA17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  IF_ZEBRA_7_IN_18_AAAAAAA7(x1, x2, x3, x4, x5, x6, x17)
IF_ZEBRA_7_IN_7_AAAAAAA16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  IF_ZEBRA_7_IN_7_AAAAAAA1(x16)
IF_ZEBRA_7_IN_17_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_17_AAAAAAA6(x1, x2, x3, x4, x5, x21)
IF_ZEBRA_7_IN_6_AAAAAAA14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  IF_ZEBRA_7_IN_6_AAAAAAA1(x14)
IF_ZEBRA_7_IN_2_AAAAAAA9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  IF_ZEBRA_7_IN_2_AAAAAAA1(x9)

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_7_IN_AAAAAAA7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
ZEBRA_7_IN_AAAAAAA7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> EQ_2_IN_AA2(Englishman, Red)
IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
IF_ZEBRA_7_IN_1_AAAAAAA8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> EQ_2_IN_AA2(Spaniard, Dog)
IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
IF_ZEBRA_7_IN_2_AAAAAAA9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> EQ_2_IN_AA2(Green, Coffee)
IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
IF_ZEBRA_7_IN_3_AAAAAAA10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> EQ_2_IN_AA2(Ukrainian, Tea)
IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
IF_ZEBRA_7_IN_4_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> TO_THE_RIGHT_2_IN_AA2(Green, Ivory)
IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
IF_ZEBRA_7_IN_5_AAAAAAA13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> EQ_2_IN_AA2(Winston, Snails)
IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
IF_ZEBRA_7_IN_6_AAAAAAA14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> EQ_2_IN_AA2(Kool, Yellow)
IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
IF_ZEBRA_7_IN_7_AAAAAAA16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> EQ_2_IN_AG2(Milk, third_0)
IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
IF_ZEBRA_7_IN_8_AAAAAAA18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> EQ_2_IN_AG2(Norwegian, first_0)
IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
IF_ZEBRA_7_IN_9_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> NEXT_TO_2_IN_AA2(Fox, Chesterfield)
IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
IF_ZEBRA_7_IN_10_AAAAAAA19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> NEXT_TO_2_IN_AA2(Horse, Kool)
IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
IF_ZEBRA_7_IN_11_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> EQ_2_IN_AA2(Lucky, Juice)
IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
IF_ZEBRA_7_IN_12_AAAAAAA22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> EQ_2_IN_AA2(Japanese, Parliament)
IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_in_ga2(Norwegian, Blue))
IF_ZEBRA_7_IN_13_AAAAAAA24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> NEXT_TO_2_IN_GA2(Norwegian, Blue)
IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_out_ga2(Norwegian, Blue)) -> IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
IF_ZEBRA_7_IN_14_AAAAAAA25(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_2_out_ga2(Norwegian, Blue)) -> HOUSES_1_IN_A1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))
HOUSES_1_IN_A1(Prop) -> IF_HOUSES_1_IN_1_A2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
HOUSES_1_IN_A1(Prop) -> DOMAIN_2_IN_AG2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> SELECT_3_IN_AGA3(X, Domain, NewDomain)
SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> IF_SELECT_3_IN_1_AGA5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> SELECT_3_IN_AGA3(X, R, Rest)
IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> IF_DOMAIN_2_IN_2_AG5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> DOMAIN_2_IN_AG2(Rest, NewDomain)
IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
IF_ZEBRA_7_IN_15_AAAAAAA26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> HOUSES_1_IN_A1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))
IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
IF_ZEBRA_7_IN_16_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> HOUSES_1_IN_A1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))
IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
IF_ZEBRA_7_IN_17_AAAAAAA21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> HOUSES_1_IN_A1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))
IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> IF_ZEBRA_7_IN_19_AAAAAAA12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
IF_ZEBRA_7_IN_18_AAAAAAA17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> HOUSES_1_IN_A1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))

The TRS R consists of the following rules:

zebra_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)
IF_DOMAIN_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_DOMAIN_2_IN_1_AG1(x4)
IF_ZEBRA_7_IN_19_AAAAAAA12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  IF_ZEBRA_7_IN_19_AAAAAAA7(x1, x2, x3, x4, x5, x6, x12)
IF_ZEBRA_7_IN_3_AAAAAAA10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  IF_ZEBRA_7_IN_3_AAAAAAA1(x10)
IF_ZEBRA_7_IN_12_AAAAAAA22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  IF_ZEBRA_7_IN_12_AAAAAAA2(x5, x22)
IF_ZEBRA_7_IN_11_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_11_AAAAAAA2(x5, x21)
HOUSES_1_IN_A1(x1)  =  HOUSES_1_IN_A
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA2(x2, x5)
IF_ZEBRA_7_IN_1_AAAAAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ZEBRA_7_IN_1_AAAAAAA1(x8)
IF_ZEBRA_7_IN_14_AAAAAAA25(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)  =  IF_ZEBRA_7_IN_14_AAAAAAA2(x5, x25)
IF_ZEBRA_7_IN_4_AAAAAAA12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  IF_ZEBRA_7_IN_4_AAAAAAA1(x12)
EQ_2_IN_AG2(x1, x2)  =  EQ_2_IN_AG1(x2)
DOMAIN_2_IN_AG2(x1, x2)  =  DOMAIN_2_IN_AG1(x2)
IF_ZEBRA_7_IN_8_AAAAAAA18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_ZEBRA_7_IN_8_AAAAAAA1(x18)
EQ_2_IN_AA2(x1, x2)  =  EQ_2_IN_AA
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)
IF_ZEBRA_7_IN_5_AAAAAAA13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  IF_ZEBRA_7_IN_5_AAAAAAA1(x13)
IF_ZEBRA_7_IN_9_AAAAAAA19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_ZEBRA_7_IN_9_AAAAAAA1(x19)
TO_THE_RIGHT_2_IN_AA2(x1, x2)  =  TO_THE_RIGHT_2_IN_AA
IF_DOMAIN_2_IN_2_AG5(x1, x2, x3, x4, x5)  =  IF_DOMAIN_2_IN_2_AG2(x1, x5)
ZEBRA_7_IN_AAAAAAA7(x1, x2, x3, x4, x5, x6, x7)  =  ZEBRA_7_IN_AAAAAAA
IF_HOUSES_1_IN_1_A2(x1, x2)  =  IF_HOUSES_1_IN_1_A1(x2)
IF_ZEBRA_7_IN_13_AAAAAAA24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_ZEBRA_7_IN_13_AAAAAAA2(x5, x24)
NEXT_TO_2_IN_GA2(x1, x2)  =  NEXT_TO_2_IN_GA1(x1)
IF_ZEBRA_7_IN_10_AAAAAAA19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_ZEBRA_7_IN_10_AAAAAAA2(x5, x19)
IF_ZEBRA_7_IN_15_AAAAAAA26(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, x26)  =  IF_ZEBRA_7_IN_15_AAAAAAA2(x5, x26)
IF_ZEBRA_7_IN_16_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_16_AAAAAAA2(x5, x21)
NEXT_TO_2_IN_AA2(x1, x2)  =  NEXT_TO_2_IN_AA
IF_ZEBRA_7_IN_18_AAAAAAA17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  IF_ZEBRA_7_IN_18_AAAAAAA7(x1, x2, x3, x4, x5, x6, x17)
IF_ZEBRA_7_IN_7_AAAAAAA16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  IF_ZEBRA_7_IN_7_AAAAAAA1(x16)
IF_ZEBRA_7_IN_17_AAAAAAA21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  IF_ZEBRA_7_IN_17_AAAAAAA6(x1, x2, x3, x4, x5, x21)
IF_ZEBRA_7_IN_6_AAAAAAA14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  IF_ZEBRA_7_IN_6_AAAAAAA1(x14)
IF_ZEBRA_7_IN_2_AAAAAAA9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  IF_ZEBRA_7_IN_2_AAAAAAA1(x9)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 2 SCCs with 43 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

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

SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> SELECT_3_IN_AGA3(X, R, Rest)

The TRS R consists of the following rules:

zebra_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

SELECT_3_IN_AGA3(X, ._22(Y, R), ._22(Y, Rest)) -> SELECT_3_IN_AGA3(X, R, Rest)

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

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem 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_3_IN_AGA1(._22(Y, R)) -> SELECT_3_IN_AGA1(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SELECT_3_IN_AGA1}.
By using the subterm criterion together with the size-change analysis 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: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

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

IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> DOMAIN_2_IN_AG2(Rest, NewDomain)
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))

The TRS R consists of the following rules:

zebra_7_in_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) -> if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_in_aa2(Englishman, Red))
eq_2_in_aa2(X, X) -> eq_2_out_aa2(X, X)
if_zebra_7_in_1_aaaaaaa8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_2_out_aa2(Englishman, Red)) -> if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_in_aa2(Spaniard, Dog))
if_zebra_7_in_2_aaaaaaa9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_2_out_aa2(Spaniard, Dog)) -> if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_in_aa2(Green, Coffee))
if_zebra_7_in_3_aaaaaaa10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_2_out_aa2(Green, Coffee)) -> if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_in_aa2(Ukrainian, Tea))
if_zebra_7_in_4_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_2_out_aa2(Ukrainian, Tea)) -> if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_in_aa2(Green, Ivory))
to_the_right_2_in_aa2(fifth_0, fourth_0) -> to_the_right_2_out_aa2(fifth_0, fourth_0)
to_the_right_2_in_aa2(fourth_0, third_0) -> to_the_right_2_out_aa2(fourth_0, third_0)
to_the_right_2_in_aa2(third_0, second_0) -> to_the_right_2_out_aa2(third_0, second_0)
to_the_right_2_in_aa2(second_0, first_0) -> to_the_right_2_out_aa2(second_0, first_0)
if_zebra_7_in_5_aaaaaaa13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_2_out_aa2(Green, Ivory)) -> if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_in_aa2(Winston, Snails))
if_zebra_7_in_6_aaaaaaa14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_2_out_aa2(Winston, Snails)) -> if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_in_aa2(Kool, Yellow))
if_zebra_7_in_7_aaaaaaa16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_2_out_aa2(Kool, Yellow)) -> if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_in_ag2(Milk, third_0))
eq_2_in_ag2(X, X) -> eq_2_out_ag2(X, X)
if_zebra_7_in_8_aaaaaaa18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_2_out_ag2(Milk, third_0)) -> if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_in_ag2(Norwegian, first_0))
if_zebra_7_in_9_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_2_out_ag2(Norwegian, first_0)) -> if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_in_aa2(Fox, Chesterfield))
next_to_2_in_aa2(fifth_0, fourth_0) -> next_to_2_out_aa2(fifth_0, fourth_0)
next_to_2_in_aa2(fourth_0, fifth_0) -> next_to_2_out_aa2(fourth_0, fifth_0)
next_to_2_in_aa2(fourth_0, third_0) -> next_to_2_out_aa2(fourth_0, third_0)
next_to_2_in_aa2(third_0, fourth_0) -> next_to_2_out_aa2(third_0, fourth_0)
next_to_2_in_aa2(third_0, second_0) -> next_to_2_out_aa2(third_0, second_0)
next_to_2_in_aa2(second_0, third_0) -> next_to_2_out_aa2(second_0, third_0)
next_to_2_in_aa2(second_0, first_0) -> next_to_2_out_aa2(second_0, first_0)
next_to_2_in_aa2(first_0, second_0) -> next_to_2_out_aa2(first_0, second_0)
if_zebra_7_in_10_aaaaaaa19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_2_out_aa2(Fox, Chesterfield)) -> if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_in_aa2(Horse, Kool))
if_zebra_7_in_11_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_2_out_aa2(Horse, Kool)) -> if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_in_aa2(Lucky, Juice))
if_zebra_7_in_12_aaaaaaa22(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_2_out_aa2(Lucky, Juice)) -> if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_in_aa2(Japanese, Parliament))
if_zebra_7_in_13_aaaaaaa24(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_2_out_aa2(Japanese, Parliament)) -> if_zebra_7_in_14_aaaaaaa25(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_2_in_ga2(Norwegian, Blue))
next_to_2_in_ga2(fifth_0, fourth_0) -> next_to_2_out_ga2(fifth_0, fourth_0)
next_to_2_in_ga2(fourth_0, fifth_0) -> next_to_2_out_ga2(fourth_0, fifth_0)
next_to_2_in_ga2(fourth_0, third_0) -> next_to_2_out_ga2(fourth_0, third_0)
next_to_2_in_ga2(third_0, fourth_0) -> next_to_2_out_ga2(third_0, fourth_0)
next_to_2_in_ga2(third_0, second_0) -> next_to_2_out_ga2(third_0, second_0)
next_to_2_in_ga2(second_0, third_0) -> next_to_2_out_ga2(second_0, third_0)
next_to_2_in_ga2(second_0, first_0) -> next_to_2_out_ga2(second_0, first_0)
next_to_2_in_ga2(first_0, second_0) -> next_to_2_out_ga2(first_0, second_0)
if_zebra_7_in_14_aaaaaaa25(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_2_out_ga2(Norwegian, Blue)) -> if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_in_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0)))))))
houses_1_in_a1(Prop) -> if_houses_1_in_1_a2(Prop, domain_2_in_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0)))))))
domain_2_in_ag2([]_0, underscore) -> domain_2_out_ag2([]_0, underscore)
domain_2_in_ag2(._22(X, Rest), Domain) -> if_domain_2_in_1_ag4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))
select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))
if_domain_2_in_1_ag4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_in_ag2(Rest, NewDomain))
if_domain_2_in_2_ag5(X, Rest, Domain, NewDomain, domain_2_out_ag2(Rest, NewDomain)) -> domain_2_out_ag2(._22(X, Rest), Domain)
if_houses_1_in_1_a2(Prop, domain_2_out_ag2(Prop, ._22(first_0, ._22(second_0, ._22(third_0, ._22(fourth_0, ._22(fifth_0, []_0))))))) -> houses_1_out_a1(Prop)
if_zebra_7_in_15_aaaaaaa26(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, Blue, houses_1_out_a1(._22(Blue, ._22(Green, ._22(Red, ._22(Yellow, ._22(Ivory, []_0))))))) -> if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0)))))))
if_zebra_7_in_16_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Norwegian, ._22(Englishman, ._22(Spaniard, ._22(Japanese, ._22(Ukrainian, []_0))))))) -> if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_in_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0)))))))
if_zebra_7_in_17_aaaaaaa21(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_1_out_a1(._22(Dog, ._22(Zebra, ._22(Fox, ._22(Snails, ._22(Horse, []_0))))))) -> if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_in_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0)))))))
if_zebra_7_in_18_aaaaaaa17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_1_out_a1(._22(Parliament, ._22(Kool, ._22(Lucky, ._22(Chesterfield, ._22(Winston, []_0))))))) -> if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_in_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0)))))))
if_zebra_7_in_19_aaaaaaa12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_1_out_a1(._22(Milk, ._22(Juice, ._22(Water, ._22(Tea, ._22(Coffee, []_0))))))) -> zebra_7_out_aaaaaaa7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_7_in_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_in_aaaaaaa
third_0  =  third_0
first_0  =  first_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
second_0  =  second_0
fourth_0  =  fourth_0
fifth_0  =  fifth_0
if_zebra_7_in_1_aaaaaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_zebra_7_in_1_aaaaaaa1(x8)
eq_2_in_aa2(x1, x2)  =  eq_2_in_aa
eq_2_out_aa2(x1, x2)  =  eq_2_out_aa
if_zebra_7_in_2_aaaaaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_zebra_7_in_2_aaaaaaa1(x9)
if_zebra_7_in_3_aaaaaaa10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  if_zebra_7_in_3_aaaaaaa1(x10)
if_zebra_7_in_4_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_4_aaaaaaa1(x12)
if_zebra_7_in_5_aaaaaaa13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  if_zebra_7_in_5_aaaaaaa1(x13)
to_the_right_2_in_aa2(x1, x2)  =  to_the_right_2_in_aa
to_the_right_2_out_aa2(x1, x2)  =  to_the_right_2_out_aa2(x1, x2)
if_zebra_7_in_6_aaaaaaa14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)  =  if_zebra_7_in_6_aaaaaaa1(x14)
if_zebra_7_in_7_aaaaaaa16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16)  =  if_zebra_7_in_7_aaaaaaa1(x16)
if_zebra_7_in_8_aaaaaaa18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_zebra_7_in_8_aaaaaaa1(x18)
eq_2_in_ag2(x1, x2)  =  eq_2_in_ag1(x2)
eq_2_out_ag2(x1, x2)  =  eq_2_out_ag1(x1)
if_zebra_7_in_9_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_9_aaaaaaa1(x19)
if_zebra_7_in_10_aaaaaaa19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_zebra_7_in_10_aaaaaaa2(x5, x19)
next_to_2_in_aa2(x1, x2)  =  next_to_2_in_aa
next_to_2_out_aa2(x1, x2)  =  next_to_2_out_aa2(x1, x2)
if_zebra_7_in_11_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_11_aaaaaaa2(x5, x21)
if_zebra_7_in_12_aaaaaaa22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_zebra_7_in_12_aaaaaaa2(x5, x22)
if_zebra_7_in_13_aaaaaaa24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_zebra_7_in_13_aaaaaaa2(x5, x24)
if_zebra_7_in_14_aaaaaaa25(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)  =  if_zebra_7_in_14_aaaaaaa2(x5, x25)
next_to_2_in_ga2(x1, x2)  =  next_to_2_in_ga1(x1)
next_to_2_out_ga2(x1, x2)  =  next_to_2_out_ga1(x2)
if_zebra_7_in_15_aaaaaaa26(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, x26)  =  if_zebra_7_in_15_aaaaaaa2(x5, x26)
houses_1_in_a1(x1)  =  houses_1_in_a
if_houses_1_in_1_a2(x1, x2)  =  if_houses_1_in_1_a1(x2)
domain_2_in_ag2(x1, x2)  =  domain_2_in_ag1(x2)
domain_2_out_ag2(x1, x2)  =  domain_2_out_ag1(x1)
if_domain_2_in_1_ag4(x1, x2, x3, x4)  =  if_domain_2_in_1_ag1(x4)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_domain_2_in_2_ag5(x1, x2, x3, x4, x5)  =  if_domain_2_in_2_ag2(x1, x5)
houses_1_out_a1(x1)  =  houses_1_out_a1(x1)
if_zebra_7_in_16_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_16_aaaaaaa2(x5, x21)
if_zebra_7_in_17_aaaaaaa21(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  if_zebra_7_in_17_aaaaaaa6(x1, x2, x3, x4, x5, x21)
if_zebra_7_in_18_aaaaaaa17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  if_zebra_7_in_18_aaaaaaa7(x1, x2, x3, x4, x5, x6, x17)
if_zebra_7_in_19_aaaaaaa12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  if_zebra_7_in_19_aaaaaaa7(x1, x2, x3, x4, x5, x6, x12)
zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)  =  zebra_7_out_aaaaaaa7(x1, x2, x3, x4, x5, x6, x7)
IF_DOMAIN_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_DOMAIN_2_IN_1_AG1(x4)
DOMAIN_2_IN_AG2(x1, x2)  =  DOMAIN_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

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

IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_out_aga3(X, Domain, NewDomain)) -> DOMAIN_2_IN_AG2(Rest, NewDomain)
DOMAIN_2_IN_AG2(._22(X, Rest), Domain) -> IF_DOMAIN_2_IN_1_AG4(X, Rest, Domain, select_3_in_aga3(X, Domain, NewDomain))

The TRS R consists of the following rules:

select_3_in_aga3(X, ._22(X, R), R) -> select_3_out_aga3(X, ._22(X, R), R)
select_3_in_aga3(X, ._22(Y, R), ._22(Y, Rest)) -> if_select_3_in_1_aga5(X, Y, R, Rest, select_3_in_aga3(X, R, Rest))
if_select_3_in_1_aga5(X, Y, R, Rest, select_3_out_aga3(X, R, Rest)) -> select_3_out_aga3(X, ._22(Y, R), ._22(Y, Rest))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
IF_DOMAIN_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_DOMAIN_2_IN_1_AG1(x4)
DOMAIN_2_IN_AG2(x1, x2)  =  DOMAIN_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem 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:

IF_DOMAIN_2_IN_1_AG1(select_3_out_aga2(X, NewDomain)) -> DOMAIN_2_IN_AG1(NewDomain)
DOMAIN_2_IN_AG1(Domain) -> IF_DOMAIN_2_IN_1_AG1(select_3_in_aga1(Domain))

The TRS R consists of the following rules:

select_3_in_aga1(._22(X, R)) -> select_3_out_aga2(X, R)
select_3_in_aga1(._22(Y, R)) -> if_select_3_in_1_aga2(Y, select_3_in_aga1(R))
if_select_3_in_1_aga2(Y, select_3_out_aga2(X, Rest)) -> select_3_out_aga2(X, ._22(Y, Rest))

The set Q consists of the following terms:

select_3_in_aga1(x0)
if_select_3_in_1_aga2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DOMAIN_2_IN_AG1, IF_DOMAIN_2_IN_1_AG1}.
We used the following order together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Polynomial interpretation:


POL(._22(x1, x2)) = 1 + x2   
POL(select_3_out_aga2(x1, x2)) = 1 + x2   
POL(if_select_3_in_1_aga2(x1, x2)) = 1 + x2   
POL(select_3_in_aga1(x1)) = x1   

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

We oriented the following set of usable rules.


select_3_in_aga1(._22(X, R)) -> select_3_out_aga2(X, R)
select_3_in_aga1(._22(Y, R)) -> if_select_3_in_1_aga2(Y, select_3_in_aga1(R))
if_select_3_in_1_aga2(Y, select_3_out_aga2(X, Rest)) -> select_3_out_aga2(X, ._22(Y, Rest))