FC:\{java.util.AbstractList<DHR>=Elem: Node(java.util.AbstractList<DHR>)
Prec: [java.util.Collection<DHR>, java.lang.Object, java.util.List<DHR>, java.lang.Iterable<DHR>, java.util.AbstractCollection<DHR>]
Desc: [java.util.Vector<DHR>]

, java.util.Collection<DHR>=Elem: Node(java.util.Collection<DHR>)
Prec: [java.lang.Object, java.lang.Iterable<DHR>]
Desc: [java.util.AbstractList<DHR>, java.util.List<DHR>, java.util.Vector<DHR>, java.util.AbstractCollection<DHR>]

, java.lang.Cloneable=Elem: Node(java.lang.Cloneable)
Prec: [java.lang.Object]
Desc: [java.util.Vector<DHR>]

, java.lang.Object=Elem: Node(java.lang.Object)
Prec: [java.lang.Object]
Desc: [java.util.AbstractList<DHR>, java.lang.Cloneable, java.util.Collection<DHR>, java.lang.Object, java.util.RandomAccess, Lambda, java.io.Serializable, java.util.List<DHR>, java.util.Vector<DHR>, java.lang.Iterable<DHR>, java.util.AbstractCollection<DHR>, Apply]

, java.util.RandomAccess=Elem: Node(java.util.RandomAccess)
Prec: [java.lang.Object]
Desc: [java.util.Vector<DHR>]

, java.util.List<DHR>=Elem: Node(java.util.List<DHR>)
Prec: [java.util.Collection<DHR>, java.lang.Object, java.lang.Iterable<DHR>]
Desc: [java.util.AbstractList<DHR>, java.util.Vector<DHR>]

, Lambda=Elem: Node(Lambda)
Prec: [java.lang.Object]
Desc: []

, java.io.Serializable=Elem: Node(java.io.Serializable)
Prec: [java.lang.Object]
Desc: [java.util.Vector<DHR>]

, java.util.Vector<DHR>=Elem: Node(java.util.Vector<DHR>)
Prec: [java.util.AbstractList<DHR>, java.lang.Cloneable, java.util.Collection<DHR>, java.lang.Object, java.util.RandomAccess, java.io.Serializable, java.util.List<DHR>, java.lang.Iterable<DHR>, java.util.AbstractCollection<DHR>]
Desc: []

, java.lang.Iterable<DHR>=Elem: Node(java.lang.Iterable<DHR>)
Prec: [java.lang.Object]
Desc: [java.util.AbstractList<DHR>, java.util.Collection<DHR>, java.util.List<DHR>, java.util.Vector<DHR>, java.util.AbstractCollection<DHR>]

, java.util.AbstractCollection<DHR>=Elem: Node(java.util.AbstractCollection<DHR>)
Prec: [java.util.Collection<DHR>, java.lang.Object, java.lang.Iterable<DHR>]
Desc: [java.util.AbstractList<DHR>, java.util.Vector<DHR>]

, Apply=Elem: Node(Apply)
Prec: [java.lang.Object]
Desc: []

}
class Apply {

  Apply()({
    super(());
  })::TPH M

}class Lambda {

  TPH X m()({
    TPH Y lam1;
    (lam1)::TPH Y = ((TPH Z x) -> ({
      return (x)::TPH Z;
    })::TPH AA)::TPH AD;
    return (lam1)::TPH Y;
  })::TPH AE

  Lambda()({
    super(());
  })::TPH AH

}0 AA: [(AA =. BFC, 1, -1)]
1 Unifikation: [(AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Z <. AA, 1, 1), (AD <. Y, -1, -1), (Y <. X, -1, -1)]
1 AA: [(AA =. BFC, 1, -1)]
2 Unifikation: [(Fun1<Z,BFC> <. Y, , -1), (AD =. Fun1<Z,BFC>, -1), (Z <. BFC, 1, -1), (AA =. BFC, 1, -1), (Y <. X, -1, -1)]
2 AA: [(AA =. BFC, 1, -1)]
3 Unifikation: [(Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (Fun1<gen_hv,gen_bf> <. X, , -1), (BFC <. gen_bf, -1, -1), (gen_hv <. Z, 1, 1)]
3 AA: [(AA =. BFC, 1, -1)]
4 Unifikation: [(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]
[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]
Result1 [[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]]
Result1 [[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]]
Result1 [[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]]
Result1 [[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]]
RES: [[(gen_ah <. gen_hv, 1, 1), (Z <. BFC, 1, -1), (AD =. Fun1<Z,BFC>, -1), (AA =. BFC, 1, -1), (Y =. Fun1<gen_hv,gen_bf>, -1), (gen_bf <. gen_sr, -1, -1), (BFC <. gen_bf, -1, -1), (X =. Fun1<gen_ah,gen_sr>, -1), (gen_hv <. Z, 1, 1)]]