=========================================================
Recognized function symbols in input:

  name                arity   strict-pos  binder-arity        
  ----                -----   -----       -----               
  app                 2       [1]         [0,0]               

=========================================================

===============================
Input Problem:
===============================
Gamma ={
  (letrec {EE[Y1,(var Yn)]} in S1)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)}
Delta1=  {}
Delta2=  {}
Delta3=  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y2) (var y2))},
  Y1 |-> y1,
  EE_#3[.1,.2]|->{y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y3) (var y3))},
  X_#2 |-> y2,
  EE_#6[.1,.2]|->{y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y4) (var y4))},
  X_#5 |-> y3,
  EE_#9[.1,.2]|->{y5=(app [.2] (var y1));[.1]=(app (var y5) (var y5))},
  X_#8 |-> y4,
  EE_#12[.1,.2]|->{[.1]=(app [.2] (var y1))},
  X_#11 |-> y5,
  A_#13 |-> (app [.] (var y1)),
  A_#10 |-> (app [.] (var y5)),
  A_#7 |-> (app [.] (var y4)),
  A_#4 |-> (app [.] (var y3)),
  A_#1 |-> (app [.] (var y2)),
  A_#18 |-> [.],
  A_#17 |-> [.],
  A_#16 |-> [.],
  A_#15 |-> [.],
  A_#14 |-> [.],
  Yn |-> y1}
Delta1  = 
  {A_#1,A_#4,A_#7,A_#10,A_#13}
Delta2 = 
  {}
Delta3 = 
  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}


Solution 2:
------------------
Instantiated Expressions:
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y1=(app (var y2) (var y2));y2=(app [.2] (var y3));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1));[.1]=(app (var y4) (var y4))},
  X_#2 |-> y1,
  EE_#5[.1,.2]|->{[.1]=(app [.2] (var y3))},
  X_#3 |-> y2,
  EE_#4[.1,.2]|->{y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y4) (var y4))},
  Y1 |-> y3,
  EE_#9[.1,.2]|->{y5=(app [.2] (var y1));[.1]=(app (var y5) (var y5))},
  X_#8 |-> y4,
  EE_#12[.1,.2]|->{[.1]=(app [.2] (var y1))},
  X_#11 |-> y5,
  A_#13 |-> (app [.] (var y1)),
  A_#10 |-> (app [.] (var y5)),
  A_#7 |-> (app [.] (var y4)),
  A_#6 |-> (app [.] (var y3)),
  A_#1 |-> (app [.] (var y2)),
  A_#18 |-> [.],
  A_#17 |-> [.],
  Yn |-> y3,
  A_#16 |-> [.],
  A_#15 |-> [.],
  A_#14 |-> [.]}
Delta1  = 
  {A_#1,A_#6,A_#7,A_#10,A_#13}
Delta2 = 
  {}
Delta3 = 
  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}


Solution 3:
------------------
Instantiated Expressions:
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app [.2] (var y4));y5=(app (var y1) (var y1));[.1]=(app (var y5) (var y5))},
  X_#2 |-> y1,
  EE_#5[.1,.2]|->{y3=(app [.2] (var y4));[.1]=(app (var y3) (var y3))},
  X_#3 |-> y2,
  EE_#8[.1,.2]|->{[.1]=(app [.2] (var y4))},
  X_#7 |-> y3,
  EE_#4[.1,.2]|->{y5=(app [.2] (var y1));[.1]=(app (var y5) (var y5))},
  Y1 |-> y4,
  EE_#12[.1,.2]|->{[.1]=(app [.2] (var y1))},
  X_#11 |-> y5,
  A_#13 |-> (app [.] (var y1)),
  A_#10 |-> (app [.] (var y5)),
  A_#9 |-> (app [.] (var y4)),
  A_#6 |-> (app [.] (var y3)),
  A_#1 |-> (app [.] (var y2)),
  A_#18 |-> [.],
  A_#17 |-> [.],
  A_#16 |-> [.],
  Yn |-> y4,
  A_#15 |-> [.],
  A_#14 |-> [.]}
Delta1  = 
  {A_#1,A_#6,A_#9,A_#10,A_#13}
Delta2 = 
  {}
Delta3 = 
  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}


Solution 4:
------------------
Instantiated Expressions:
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app [.2] (var y5));[.1]=(app (var y1) (var y1))},
  X_#2 |-> y1,
  EE_#5[.1,.2]|->{y3=(app (var y4) (var y4));y4=(app [.2] (var y5));[.1]=(app (var y3) (var y3))},
  X_#3 |-> y2,
  EE_#8[.1,.2]|->{y4=(app [.2] (var y5));[.1]=(app (var y4) (var y4))},
  X_#7 |-> y3,
  EE_#11[.1,.2]|->{[.1]=(app [.2] (var y5))},
  X_#10 |-> y4,
  EE_#4[.1,.2]|->{[.1]=(app [.2] (var y1))},
  Y1 |-> y5,
  A_#13 |-> (app [.] (var y1)),
  A_#12 |-> (app [.] (var y5)),
  A_#9 |-> (app [.] (var y4)),
  A_#6 |-> (app [.] (var y3)),
  A_#1 |-> (app [.] (var y2)),
  A_#18 |-> [.],
  A_#17 |-> [.],
  A_#16 |-> [.],
  A_#15 |-> [.],
  Yn |-> y5,
  A_#14 |-> [.]}
Delta1  = 
  {A_#1,A_#6,A_#9,A_#12,A_#13}
Delta2 = 
  {}
Delta3 = 
  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}


Solution 5:
------------------
Instantiated Expressions:
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
  =?=
  (letrec {y1=(app (var y2) (var y2));y2=(app (var y3) (var y3));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1))} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y1=(app [.2] (var y2));y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app (var y1) (var y1));[.1]=(app (var y3) (var y3))},
  X_#2 |-> y1,
  EE_#3[.1,.2]|->{y3=(app (var y4) (var y4));y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y3) (var y3))},
  Y1 |-> y2,
  EE_#6[.1,.2]|->{y4=(app (var y5) (var y5));y5=(app [.2] (var y1));[.1]=(app (var y4) (var y4))},
  X_#5 |-> y3,
  EE_#9[.1,.2]|->{y5=(app [.2] (var y1));[.1]=(app (var y5) (var y5))},
  X_#8 |-> y4,
  EE_#12[.1,.2]|->{[.1]=(app [.2] (var y1))},
  X_#11 |-> y5,
  A_#13 |-> (app [.] (var y1)),
  A_#10 |-> (app [.] (var y5)),
  A_#7 |-> (app [.] (var y4)),
  A_#4 |-> (app [.] (var y3)),
  A_#1 |-> (app [.] (var y2)),
  A_#18 |-> [.],
  Yn |-> y2,
  A_#17 |-> [.],
  A_#16 |-> [.],
  A_#15 |-> [.],
  A_#14 |-> [.]}
Delta1  = 
  {A_#1,A_#4,A_#7,A_#10,A_#13}
Delta2 = 
  {}
Delta3 = 
  {((var y1),(app [.] (var y1))),((var y1),(app (var y1) [.])),((var y2),(app [.] (var y2))),((var y2),(app (var y2) [.])),((var y3),(app [.] (var y3))),((var y3),(app (var y3) [.])),((var y4),(app [.] (var y4))),((var y4),(app (var y4) [.])),((var y5),(app [.] (var y5))),((var y5),(app (var y5) [.]))}