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

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

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

===============================
Input Problem:
===============================
Gamma ={
  (app (\ X1.(var X1)) S1) =?= (app S2 (\ X2.(var X2))),
  S1 =?= S2}
Delta1=  {}
Delta2=  {}
Delta3=  {((var X1),(_internal_f [.])),((var X2),(_internal_f [.]))}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (app (\ X2.(var X2)) (\ X2.(var X2)))
  =?=
  (app (\ X2.(var X2)) (\ X2.(var X2))),
  (\ X2.(var X2)) =?= (\ X2.(var X2))
Sol = {
  S1 |-> (\ X2.(var X2)),
  S2 |-> (\ X2.(var X2)),
  X1 |-> X2,
  X2 |-> X2}
Delta1  = 
  {}
Delta2 = 
  {}
Delta3 = 
  {((var X2),(_internal_f [.])),((var X2),(_internal_f [.]))}