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

  name                arity   strict-pos  binder-arity        
  ----                -----   -----       -----               
  \                   1       []          [1]                 
  fun                 1       [1]         [0]                 

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

===============================
Input Problem:
===============================
Gamma ={
  U1 =?= (fun U2),
  U2 =?= (fun U3),
  U3 =?= (fun U4),
  U4 =?= (fun U5),
  U5 =?= (\ x.(var x))}
Delta1=  {}
Delta2=  {}
Delta3=  {((var x),(_internal_f [.]))}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (fun (fun (fun (fun (\ x.(var x))))))
  =?=
  (fun (fun (fun (fun (\ x.(var x)))))),
  (fun (fun (fun (\ x.(var x))))) =?= (fun (fun (fun (\ x.(var x))))),
  (fun (fun (\ x.(var x)))) =?= (fun (fun (\ x.(var x)))),
  (fun (\ x.(var x))) =?= (fun (\ x.(var x))),
  (\ x.(var x)) =?= (\ x.(var x))
Sol = {
  U1 |-> (fun (fun (fun (fun (\ x.(var x)))))),
  U2 |-> (fun (fun (fun (\ x.(var x))))),
  U3 |-> (fun (fun (\ x.(var x)))),
  U4 |-> (fun (\ x.(var x))),
  U5 |-> (\ x.(var x))}
Delta1  = 
  {}
Delta2 = 
  {}
Delta3 = 
  {((var x),(_internal_f [.]))}