diff --git a/jvm/src/test/scala/cpstest/TestInferredByDefault.scala b/jvm/src/test/scala/cpstest/TestInferredByDefault.scala
index b96d7527..0202c01b 100644
--- a/jvm/src/test/scala/cpstest/TestInferredByDefault.scala
+++ b/jvm/src/test/scala/cpstest/TestInferredByDefault.scala
@@ -26,7 +26,8 @@ class TestInferredByDefault {
        println(s)
        s
      }
-     v match {
+
+     (v: @unchecked) match {
        case cf: CompletableFuture[?] =>
           println("CompletableFuture")
        case f: scala.concurrent.Future[?] =>
diff --git a/shared/src/test/scala/logic/unification1/Unifiable.scala b/shared/src/test/scala/logic/unification1/Unifiable.scala
index c0665be4..b60b3299 100644
--- a/shared/src/test/scala/logic/unification1/Unifiable.scala
+++ b/shared/src/test/scala/logic/unification1/Unifiable.scala
@@ -90,7 +90,6 @@ object Point {
               yrBindings
             }
           }
-        case _ => failure()
     }
 
   }
diff --git a/shared/src/test/scala/logic/unification1/examples/DBAccess1.scala b/shared/src/test/scala/logic/unification1/examples/DBAccess1.scala
index 40a67f6e..44e64f5b 100644
--- a/shared/src/test/scala/logic/unification1/examples/DBAccess1.scala
+++ b/shared/src/test/scala/logic/unification1/examples/DBAccess1.scala
@@ -64,6 +64,8 @@ object DBAccess1 {
               or(users.map(u => userFact.unify[R](u, term, bindings)))
             else
               failure()
+          case CheckedLogicalTerm(term, cast, check) =>
+            ???
       }
 
   }
@@ -116,6 +118,10 @@ object DBAccess2 {
               reflect(or(users.map(u => userFact.unify[R](u, term, bindings))))
             else
               reflect(failure())
+          case CheckedLogicalTerm(term, cast, check) =>
+
+              ???
+
       }
 
 
@@ -144,7 +150,7 @@ object DBAccess3 {
         term match
           case lv: LogicalVariable =>
             reflect(asyncOr(collection.asyncFind().map(u => bindings.bind(lv, QueryAllUsers(u)))))
-          case lc@LogicalConstant(value) =>
+          case _ =>
             ??? // logic similar to the previous example
       }
 
diff --git a/shared/src/test/scala/logic/unification2/Access.scala b/shared/src/test/scala/logic/unification2/Access.scala
new file mode 100644
index 00000000..bdf69f56
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/Access.scala
@@ -0,0 +1,7 @@
+package logic.unification2
+
+trait Access[-T] {
+
+  def get[S<:T]: S
+  
+}
diff --git a/shared/src/test/scala/logic/unification2/LogicalTerm.scala b/shared/src/test/scala/logic/unification2/LogicalTerm.scala
new file mode 100644
index 00000000..856eee2e
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/LogicalTerm.scala
@@ -0,0 +1,45 @@
+package logic.unification2
+
+import logic.CpsLogicMonad
+
+sealed trait LogicalExpression
+
+
+sealed trait LogicalTerm extends LogicalExpression {
+
+   type Type
+   def symbol: Unifiable[Type]
+  
+}
+
+object LogicalTerm {
+
+  type Aux[T] = LogicalTerm { type Type = T }
+
+}
+
+sealed trait TypedLogicalTerm[T:Unifiable] extends LogicalTerm {
+
+  type Type = T
+
+  def symbol = summon[Unifiable[T]]
+
+}
+
+case class LogicalVariable[T:Unifiable](id:Long, name: String) extends TypedLogicalTerm[T] 
+
+
+case class LogicalConstant[T:Unifiable](value: T) extends TypedLogicalTerm[T]
+
+
+case class LogicalFunctionalTerm[T:Unifiable](args: IndexedSeq[LogicalTerm]) extends TypedLogicalTerm[T] {
+
+  
+  
+}
+
+
+
+
+
+
diff --git a/shared/src/test/scala/logic/unification2/Unifiable.scala b/shared/src/test/scala/logic/unification2/Unifiable.scala
new file mode 100644
index 00000000..fdbace3b
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/Unifiable.scala
@@ -0,0 +1,73 @@
+package logic.unification2
+
+import cps.*
+import logic.CpsLogicMonad
+
+
+trait Unifiable[T]  {
+
+  type Environment[M[_]] <: UnificationEnvironment[M]
+
+  type InstanceData = Any
+
+  def unify[M[_]:Environment](a: M[T], b: M[T])(using data: Access[InstanceData]): M[T]
+  
+  def fromTerm(term: LogicalTerm): Option[T]
+
+  def className: String
+
+  lazy val classNameHash: Int = className.hashCode
+
+  // don;t use Environment,  becase when we cast, we don;t have in code exact type of term
+  // and can't deduce Environment.
+  def  castTo[M[_]:UnificationEnvironment, S:Unifiable](t: LogicalTerm): M[TypedLogicalTerm[S]] =
+    if (summon[Unifiable[S]] == this) then
+      summon[UnificationEnvironment[M]].pure(t.asInstanceOf[TypedLogicalTerm[S]])
+    else
+      summon[UnificationEnvironment[M]].mzero
+
+}
+
+object Unifiable {
+
+  given Ordering[Unifiable[?]] with
+    def compare(x: Unifiable[?], y: Unifiable[?]): Int =
+      x.classNameHash - y.classNameHash
+
+  given Equiv[Unifiable[?]] with
+    def equiv(x: Unifiable[?], y: Unifiable[?]): Boolean =
+      x.className == y.className
+
+  given Unifiable[Int] with
+    type Environment[M[_]] = UnificationEnvironment[M]
+
+    override def unify[M[_]:Environment](a: M[Int], b: M[Int])(using data: Access[InstanceData]): M[Int] = reify[M] {
+      a.toTerm match
+        case lc: LogicalConstant[?] => ???
+          /*
+          b.toTerm match
+            case lc2: LogicalConstant[Int] =>
+              if lc2 == lc then reflect(a) else failure[M,Int]
+            case lv: LogicalVariable[Int] =>
+              lv.bind(a.toTerm)
+            case fun: FunctionalTerm[?] =>
+              ???
+
+           */
+
+    }
+
+    override def fromTerm(term: LogicalTerm): Option[Int] = term match
+      case lc: LogicalConstant[?] =>
+        if (lc.symbol == summon[Unifiable[Int]]) then
+          Some(lc.value.asInstanceOf[Int])
+        else
+          None
+      case _ => None
+
+    //override def compare(x: Int, y: Int): Int = x - y
+
+    override def className: String = "Int"
+
+
+}
\ No newline at end of file
diff --git a/shared/src/test/scala/logic/unification2/UnificationEnvironment.scala b/shared/src/test/scala/logic/unification2/UnificationEnvironment.scala
new file mode 100644
index 00000000..28929bdf
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/UnificationEnvironment.scala
@@ -0,0 +1,95 @@
+package logic.unification2
+
+import cps.*
+import logic.*
+import logic.CpsLogicMonad
+
+
+trait UnificationEnvironment[M[_]] extends CpsLogicMonad[M] {
+
+  override type Context <: UnificationEnvironmentContext[M]
+
+  def toTerm[A:Unifiable](ma: M[A]): M[TypedLogicalTerm[A]]
+
+  def fromTerm[A:Unifiable](t:TypedLogicalTerm[A]): M[A]
+
+  def bindTerm[A:Unifiable](v:LogicalVariable[A], t:TypedLogicalTerm[A]): M[A]
+
+  def bind[A:Unifiable](v:LogicalVariable[A], ma: M[A]): M[A] 
+  
+}
+
+trait UnificationEnvironmentContext[M[_]] extends CpsLogicMonadContext[M] {
+
+  override def monad: UnificationEnvironment[M]
+
+}
+
+extension [M[_],A](ma:M[A])(using env: UnificationEnvironmentContext[M], ua: Unifiable[A])  {
+
+  def _toTerm: M[TypedLogicalTerm[A]] =
+    env.monad.toTerm(ma)
+
+  transparent inline def toTerm: TypedLogicalTerm[A] =
+    reflect(env.monad.toTerm(ma))
+  
+}
+
+extension [M[_],A](lv:LogicalVariable[A])(using env: UnificationEnvironmentContext[M], ua: Unifiable[A])  {
+
+  def _bindTerm(t:TypedLogicalTerm[A]): M[A] =
+    env.monad.bindTerm(lv, t)
+
+  transparent inline def bindTerm(t:TypedLogicalTerm[A]): A =
+    reflect(env.monad.bindTerm(lv, t))
+    
+  def _bind(ma:M[A]): M[A] =
+    env.monad.bind(lv, ma)
+    
+  transparent inline def bind(ma:M[A]): A =
+    reflect(env.monad.bind(lv, ma))  
+
+}
+
+extension [M[_],A](t:TypedLogicalTerm[A])(using ua: Unifiable[A], ctx: UnificationEnvironmentContext[M])  {
+
+  def _fromTerm: M[A] =
+    ctx.monad.fromTerm(t)
+
+  transparent inline def fromTerm: A =
+    reflect(ctx.monad.fromTerm(t))
+
+  
+}
+
+
+extension [M[_]](t: LogicalTerm)(using ctx: UnificationEnvironmentContext[M], env: UnificationEnvironment[M])  {
+
+
+  def _castToTerm[S: Unifiable]: M[TypedLogicalTerm[S]] =
+    t.symbol.castTo[M, S](t)
+
+  transparent inline def castToTerm[S: Unifiable]: TypedLogicalTerm[S] =
+    reflect(t.symbol.castTo[M, S](t))
+
+  def castToM[S: Unifiable]: M[S] =
+    ctx.monad.flatMap(t.symbol.castTo[M, S](t))(ctx.monad.fromTerm(_))
+
+
+}
+
+
+transparent inline def failure[M[_],A](using env: UnificationEnvironmentContext[M]): A =
+  reflect(env.monad.mzero[A])
+  
+transparent inline def success[M[_],A](a:A)(using env: UnificationEnvironmentContext[M]): A =
+  reflect(env.monad.pure(a))
+
+
+
+object UnificationEnvironment {
+
+
+
+
+}
diff --git a/shared/src/test/scala/logic/unification2/UnificationEnvironmentCompileProblem.scala b/shared/src/test/scala/logic/unification2/UnificationEnvironmentCompileProblem.scala
new file mode 100644
index 00000000..71ed794d
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/UnificationEnvironmentCompileProblem.scala
@@ -0,0 +1,478 @@
+package logic.unification2
+
+
+import cps.CpsTryMonad
+import logic.{CpsLogicMonad, CpsLogicMonadInstanceContext}
+
+import scala.collection.immutable.LongMap
+import scala.collection.immutable.Queue
+import scala.util.*
+import scala.util.control.NonFatal
+import scala.util.boundary.*
+
+import cps.*
+
+sealed trait UniWrapperCP1[F[_]:CpsTryMonad,A] {
+
+  type _R = A
+
+  def flatMapTry[B](f: Try[A] => UniWrapperCP1[F,B]): UniWrapperCP1[F,B]
+
+  /**
+   * Called in case of FlatMap is delated and put into FlatMapQueus
+   * and then we apply flatMapTry accross all queue whe evaluating.
+   *
+   * (the same as flatMap fpr early evaluation.)
+   */
+  def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B]
+
+  def mplus(other: =>UniWrapperCP1[F,A]): UniWrapperCP1[F,A]
+
+  def fsplit: F[Option[(Try[A], UniWrapperCP1[F,A])]]
+
+}
+
+
+
+object UniWrapperCP1 {
+
+  case class Zero[F[_]:CpsTryMonad,A]() extends UniWrapperCP1[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      this.asInstanceOf[Zero[F,B]]
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      this.asInstanceOf[Zero[F,B]]
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      other
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      summon[CpsTryMonad[F]].pure(None)
+
+  }
+
+  case class Pure[F[_]:CpsTryMonad, A](a: A) extends UniWrapperCP1[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      f(Success(a))
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      f(Success(a))
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      Cons[F,A](Success(a), Susp(() => other))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      summon[CpsTryMonad[F]].pure(Some((Success(a), Zero[F,A]())))
+
+  }
+
+
+
+
+  case class Cons[F[_]:CpsTryMonad,A](head: Try[A], tail: UniWrapperCP1[F,A]) extends UniWrapperCP1[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      applyFlatMapTryToHead(f).mplus(tail.flatMapTry(f))
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      applyFlatMapTryToHead(f).mplus(tail.flatMapTry(f))
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      summon[CpsTryMonad[F]].pure(Some((head, tail)))
+
+    private final def applyFlatMapTryToHead[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      try
+        f(head)
+      catch
+        case NonFatal(ex) =>
+          WaitF[F,B](summon[CpsTryMonad[F]].error(ex))
+
+  }
+
+
+  case class Susp[F[_]:CpsTryMonad,A](susp: () => UniWrapperCP1[F,A]) extends UniWrapperCP1[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      // TODO: use type-aligned queue or trampolined function
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapperCP1[F,?]]))
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      val next = summon[CpsTryMonad[F]].map(susp().flatMapTry(f).fsplit){
+        case None => Zero[F,B]()
+        case Some((head,tail)) => Cons[F,B](head,tail)
+      }
+      WaitF(next)
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      susp().fsplit
+
+
+
+  }
+
+
+  case class FlatMapQueue[F[_]:CpsTryMonad,A,R](start: UniWrapperCP1[F,A], queue: Queue[Try[?] => UniWrapperCP1[F,?]]) extends UniWrapperCP1[F,R] {
+
+    override def flatMapTry[B](f: Try[R] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      FlatMapQueue[F,A,B](start, queue.enqueue(f.asInstanceOf[Try[?] => UniWrapperCP1[F,?]]))
+
+    override def applyFlatMapTry[B](f: Try[R] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      applyFlatMaps().applyFlatMapTry(f)
+
+    override def mplus(other: => UniWrapperCP1[F, R]): UniWrapperCP1[F, R] =
+      MPlusQueue[F,R](Queue(this,Susp(()=>other)))
+
+
+    override def fsplit: F[Option[(Try[R], UniWrapperCP1[F, R])]] =
+      summon[CpsTryMonad[F]].flatMap(start.fsplit) {
+        case None => summon[CpsTryMonad[F]].pure(None)
+        case Some((startHead,startTail)) =>
+          val startHeadUniWrapperCP1 = FlatMapQueue[F,A,R](fromTry(startHead), queue).applyFlatMaps()
+          summon[CpsTryMonad[F]].flatMap(startHeadUniWrapperCP1.fsplit) {
+            case None => FlatMapQueue(startTail, queue).fsplit
+            case Some((startHeadApplyHead, startHeadApplyTail)) =>
+              val next = Susp(() => startHeadApplyTail mplus FlatMapQueue(startTail, queue))
+              summon[CpsTryMonad[F]].pure(Some((startHeadApplyHead, next)))
+          }
+      }
+
+
+    def applyFlatMaps(): UniWrapperCP1[F,R] =
+      val s0: UniWrapperCP1[F,?] = start.asInstanceOf[UniWrapperCP1[F,?]]
+      val r = queue.foldLeft(s0){ (s,e) =>
+        s.applyFlatMapTry(e.asInstanceOf[Try[s._R] => UniWrapperCP1[F,Any]])
+      }
+      r.asInstanceOf[UniWrapperCP1[F,R]]
+
+  }
+
+
+
+  case class WaitF[F[_]:CpsTryMonad,A](fa: F[UniWrapperCP1[F,A]]) extends UniWrapperCP1[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      WaitF(
+        summon[CpsTryMonad[F]].map(fa)(_.flatMapTry(f))
+      )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      WaitF(
+        summon[CpsTryMonad[F]].map(fa)(_.applyFlatMapTry(f))
+      )
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      summon[CpsTryMonad[F]].flatMap(fa)(_.fsplit)
+
+
+  }
+
+
+  case class MPlusQueue[F[_]:CpsTryMonad,A](queue: Queue[UniWrapperCP1[F,A]]) extends UniWrapperCP1[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      if (queue.isEmpty)
+        Zero[F,B]()
+      else
+        MPlusQueue(queue.map(_.flatMapTry(f)))
+
+    /**
+     * BFS - apply only head
+     * @param f
+     * @tparam B
+     * @return
+     */
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      queue.dequeueOption match
+        case None => Zero[F,B]()
+        case Some((head,tail)) =>
+          head.applyFlatMapTry(f)  match
+            case Zero() =>
+              if (tail.isEmpty)
+                Zero[F,B]()
+              else
+                MPlusQueue(tail).applyFlatMapTry(f)
+            case other => other.mplus(MPlusQueue(tail).flatMapTry(f))
+
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](queue.enqueue(other))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      queue.dequeueOption match
+        case None => summon[CpsTryMonad[F]].pure(None)
+        case Some((head,tail)) =>
+          summon[CpsTryMonad[F]].flatMap(head.fsplit) {
+            case None => MPlusQueue(tail).fsplit
+            case Some((headHead,headTail)) =>
+              val next = Susp(() => headTail mplus MPlusQueue(tail))
+              summon[CpsTryMonad[F]].pure(Some((headHead, next)))
+          }
+
+
+  }
+
+  case class LVNew[F[_]:CpsTryMonad,A](lv: LogicalVariable[A]) extends UniWrapperCP1[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapperCP1[F,?]]) )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      // lv can participate in the rerursie expression
+      LTerm[F,A](lv,LongMap.empty).applyFlatMapTry(f)
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      summon[CpsTryMonad[F]].pure(None)
+
+  }
+
+  case class LVBind[F[_]:CpsTryMonad,A](lv: LogicalVariable[A], v: UniWrapperCP1[F,A]) extends UniWrapperCP1[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapperCP1[F,?]]) )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] = {
+      toLTerm().applyFlatMapTry(f)
+    }
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] =
+      toLTerm().fsplit
+
+    def toLTerm(): LTerm[F,A] =
+      LTerm[F,A](lv,LongMap(lv.id -> LVarBingingRecord(lv,v)))
+
+  }
+
+
+
+  case class LVarBingingRecord[F[_],T](lv: LogicalVariable[T], v: UniWrapperCP1[F,T]) {
+    type Tp = T
+  }
+
+  case class SplittedLVarBingingRecord[F[_],T](lv: LogicalVariable[T],
+                                               currentValue: Option[Try[T]],
+                                               next: UniWrapperCP1[F,T])
+
+
+  case class LTerm[F[_]:CpsTryMonad,A](t: TypedLogicalTerm[A], bindings: LongMap[LVarBingingRecord[F,?]]) extends UniWrapperCP1[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapperCP1[F,?]]) )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapperCP1[F, B]): UniWrapperCP1[F, B] =
+      WaitF(summon[CpsTryMonad[F]].map(fsplit){
+        case None => Zero[F,B]()
+        case Some((head,tail)) =>
+          val resHead = try {
+            f(head)
+          } catch {
+            case NonFatal(ex) =>
+              WaitF[F, B](summon[CpsTryMonad[F]].error(ex))
+          }
+          resHead.mplus(tail.flatMapTry(f))
+      })
+
+    override def mplus(other: => UniWrapperCP1[F, A]): UniWrapperCP1[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapperCP1[F, A])]] = reify[F]{
+      val optNext = reflect(fsplitInBinding(t, bindings))
+      optNext match
+        case None => None
+        case Some((head, nextBindings)) =>
+          head match
+            case Success(t) =>
+              Some((Success(t), buildNextBindings(nextBindings)))
+            case Failure(ex) =>
+              Some((Failure(ex), buildNextBindings(nextBindings)))
+    }
+
+
+
+    private def fsplitInBinding[A](t: TypedLogicalTerm[A],
+                                   oldBinding: LongMap[LVarBingingRecord[F,?]],
+                                   changedBinding: LongMap[SplittedLVarBingingRecord[F,?]] = LongMap.empty
+                                  ): F[Option[(Try[A], LongMap[SplittedLVarBingingRecord[F,?]])]] = {
+
+      def getVarBinding(id: Long, currentBinding: LongMap[SplittedLVarBingingRecord[F,?]]):
+      F[(Option[Try[?]],LongMap[SplittedLVarBingingRecord[F,?]])] = {
+        currentBinding.get(id) match
+          case Some(r)  => summon[CpsTryMonad[F]].pure((r.currentValue, currentBinding))
+          case None => oldBinding.get(id) match
+            case None => summon[CpsTryMonad[F]].error(new RuntimeException(s"unbound variable $id"))
+            case Some(LVarBingingRecord(lv,v)) =>
+              summon[CpsTryMonad[F]].flatMap(v.fsplit) {
+                case None =>
+                  val nextBinding = currentBinding.updated(id, SplittedLVarBingingRecord(lv,None,Zero[F,lv.Type]()))
+                  summon[CpsTryMonad[F]].pure((None, nextBinding))
+                case Some((head,tail)) =>
+                  val nextBinding = currentBinding.updated(id, SplittedLVarBingingRecord(lv,Some(head),tail))
+                  summon[CpsTryMonad[F]].pure((Some(head), nextBinding))
+              }
+      }
+
+
+      def fetchTerm(term:LogicalTerm, currentBinding: LongMap[SplittedLVarBingingRecord[F,?]]):
+      F[(Option[Try[LogicalTerm]],LongMap[SplittedLVarBingingRecord[F,?]])] = {
+
+        term match
+          case l: LogicalVariable[t] =>
+            reify[F] {
+              val (optTryA, nextBinding) = reflect(getVarBinding(l.id, currentBinding))
+              val optTerm: Option[Try[LogicalTerm]] = optTryA.map(_.map(a =>
+                LogicalConstant[t](a.asInstanceOf[t])(using l.symbol)
+              ))
+              (optTerm, nextBinding)
+            }
+          case l: LogicalConstant[t] =>
+            summon[CpsTryMonad[F]].pure(Some(Success(l:LogicalTerm)), currentBinding)
+          case l: LogicalFunctionalTerm[t] =>
+            val s0: (IndexedSeq[LogicalTerm], LongMap[SplittedLVarBingingRecord[F, ?]]) = (IndexedSeq.empty, currentBinding)
+            ???
+            // error here.
+            /*
+            reify[F] {
+              boundary[(Option[Try[LogicalTerm]], LongMap[SplittedLVarBingingRecord[F, ?]])] {
+                val s = l.args.foldLeft(s0) { (s, e) =>
+                  val (args, currentBinding) = s
+                  val (optTryArg, nextBinding) = reflect(fetchTerm(e, currentBinding))
+                  val s1 = optTryArg match
+                    case None =>
+                      break((None, nextBinding))
+                    case Some(tryArg) =>
+                      tryArg match
+                        case Failure(ex) =>
+                          break((Some(Failure(ex)), currentBinding))
+                        case Success(arg) =>
+                          (args :+ arg) -> nextBinding
+                  s1
+                }
+                val (nextArgs, nextBinding) = s
+                val lt: LogicalTerm = LogicalFunctionalTerm(nextArgs)(using l.symbol)
+                (Some(Success(lt)), nextBinding)
+              }
+            }
+            */
+
+
+      }
+
+      reify[F] {
+        val (optTryTerm, bindings) = reflect(fetchTerm(t, changedBinding))
+        val optTryA = optTryTerm.map(_.map(term => 
+          term.symbol.fromTerm(term).getOrElse(
+            throw new IllegalStateException(s"Term is not fully constructed  ($term) ")
+          ).asInstanceOf[A]
+        ))
+        optTryA.map(tryA => (tryA, bindings))
+      }
+
+
+    }
+
+    private def buildNextBindings(nextBindings: LongMap[SplittedLVarBingingRecord[F,?]]): UniWrapperCP1[F,A] =
+      ???
+
+
+  }
+
+  def fromTry[F[_]:CpsTryMonad,A](t: Try[A]): UniWrapperCP1[F,A] =
+    t match
+      case Success(a) => Pure[F,A](a)
+      case Failure(ex) => WaitF(summon[CpsTryMonad[F]].error(ex))
+
+  def error[F[_]:CpsTryMonad,A](msg: String): UniWrapperCP1[F,A] =
+    WaitF(summon[CpsTryMonad[F]].error(new RuntimeException(msg)))
+
+  class UniWrapperCP1Environment[ F[_]:CpsTryMonad] extends UnificationEnvironment[[T]=>>UniWrapperCP1[F,T]] {
+
+    thisUnificationEnvironment =>
+
+    class LContext extends UnificationEnvironmentContext[[T]=>>UniWrapperCP1[F,T]] {
+      override def monad: UnificationEnvironment[[T] =>> UniWrapperCP1[F, T]] = thisUnificationEnvironment
+    }
+
+    override type Context = LContext
+
+    override type Observer[X] = F[X]
+
+    def pure[A](a:A): UniWrapperCP1[F,A] =
+      Pure[F,A](a)
+
+    def map[A,B](fa: UniWrapperCP1[F,A])(f: A=>B): UniWrapperCP1[F,B] = ???
+
+    def flatMap[A,B](fa: UniWrapperCP1[F,A])(f: A=>UniWrapperCP1[F,B]): UniWrapperCP1[F,B] = ???
+
+    def flatMapTry[A,B](fa: UniWrapperCP1[F,A])(f: Try[A]=>UniWrapperCP1[F,B]): UniWrapperCP1[F,B] =
+      fa.flatMapTry(f)
+
+    override def error[A](e: Throwable): UniWrapperCP1[F, A] = ???
+
+    override def mzero[A]: UniWrapperCP1[F, A] = ???
+
+    override def mplus[A](x: UniWrapperCP1[F, A], y: =>UniWrapperCP1[F, A]): UniWrapperCP1[F, A] = ???
+
+    override def apply[T](op: LContext => UniWrapperCP1[F, T]): UniWrapperCP1[F, T] = {
+      op(new LContext)
+    }
+
+    override def msplit[A](c: UniWrapperCP1[F, A]): UniWrapperCP1[F, Option[(Try[A], UniWrapperCP1[F, A])]] = ???
+
+    override def observerCpsMonad: CpsTryMonad[F] = summon[CpsTryMonad[F]]
+
+    override def mObserveOne[A](ma: UniWrapperCP1[F, A]): F[Option[A]] = ???
+
+    override def mFoldLeft[A, B](ma: UniWrapperCP1[F, A], zero: F[B])(op: (F[B], F[A]) => F[B]): F[B] = ???
+
+    override def mFoldLeftN[A, B](ma: UniWrapperCP1[F, A], zero: F[B], n: Int)(op: (F[B], F[A]) => F[B]): F[B] = ???
+
+    //TODO: change to bind with M[A] instead of term
+    override def bindTerm[A:Unifiable](lv: LogicalVariable[A], t: TypedLogicalTerm[A]): UniWrapperCP1[F, A] = ???
+
+    override def bind[A:Unifiable](lv: LogicalVariable[A], v: UniWrapperCP1[F, A]): UniWrapperCP1[F, A] = ???
+
+    override def fromTerm[A: Unifiable](t: TypedLogicalTerm[A]): UniWrapperCP1[F, A] = ???
+
+    override def toTerm[A: Unifiable](ma: UniWrapperCP1[F, A]): UniWrapperCP1[F, TypedLogicalTerm[A]] = ???
+
+
+    def cons[T](head: Try[T], tail: UniWrapperCP1[F,T]): UniWrapperCP1[F,T] =
+      Cons[F,T](head,tail)
+
+    def susp[T](susp: () => UniWrapperCP1[F,T]): UniWrapperCP1[F,T] =
+      Susp[F,T](susp)
+
+    def waitF[T](fa: F[UniWrapperCP1[F,T]]): UniWrapperCP1[F,T] =
+      WaitF[F,T](fa)
+
+    def mplusQueue[T](queue: Queue[UniWrapperCP1[F,T]]): UniWrapperCP1[F,T] =
+      MPlusQueue[F,T](queue)
+
+    def lvBind[T](lv: LogicalVariable[T], v: UniWrapperCP1[F,T]): UniWrapperCP1[F,T] =
+      LVBind[F,T](lv,v)
+
+    def lTerm[T](t: TypedLogicalTerm[T], bindings: LongMap[LVarBingingRecord[F,?]]): UniWrapperCP1[F,T] =
+      LTerm[F,T](t,bindings)
+
+  }
+
+
+}
+
diff --git a/shared/src/test/scala/logic/unification2/UnificationEnvironmentImpl.scala b/shared/src/test/scala/logic/unification2/UnificationEnvironmentImpl.scala
new file mode 100644
index 00000000..0ef5319c
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/UnificationEnvironmentImpl.scala
@@ -0,0 +1,549 @@
+package logic.unification2
+
+import cps.CpsTryMonad
+import logic.unification1.LogicalFunctionSymbol
+import logic.{CpsLogicMonad, CpsLogicMonadInstanceContext}
+
+import scala.collection.immutable.LongMap
+import scala.collection.immutable.Queue
+import scala.util.*
+import scala.util.control.NonFatal
+import scala.util.boundary.*
+
+import cps.*
+
+sealed trait UniWrapper[F[_]:CpsTryMonad,A] {
+
+   type _R = A
+
+   def flatMapTry[B](f: Try[A] => UniWrapper[F,B]): UniWrapper[F,B]
+
+  /**
+   * Called in case of FlatMap is delated and put into FlatMapQueus
+   * and then we apply flatMapTry accross all queue whe evaluating.
+   *
+   * (the same as flatMap fpr early evaluation.)
+   */
+   def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B]
+
+   def mplus(other: =>UniWrapper[F,A]): UniWrapper[F,A]
+
+   def fsplit: F[Option[(Try[A], UniWrapper[F,A])]]
+
+}
+
+
+
+object UniWrapper {
+
+  case class Zero[F[_]:CpsTryMonad,A]() extends UniWrapper[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      this.asInstanceOf[Zero[F,B]]
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      this.asInstanceOf[Zero[F,B]]
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      other
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      summon[CpsTryMonad[F]].pure(None)
+
+  }
+
+  case class Pure[F[_]:CpsTryMonad, A](a: A) extends UniWrapper[F,A] {
+
+      override def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+        f(Success(a))
+
+      override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+        f(Success(a))
+
+      override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+        Cons[F,A](Success(a), Susp(() => other))
+
+      override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+        summon[CpsTryMonad[F]].pure(Some((Success(a), Zero[F,A]())))
+
+  }
+
+
+
+
+  case class Cons[F[_]:CpsTryMonad,A](head: Try[A], tail: UniWrapper[F,A]) extends UniWrapper[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+          applyFlatMapTryToHead(f).mplus(tail.flatMapTry(f))
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+          applyFlatMapTryToHead(f).mplus(tail.flatMapTry(f))
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+          MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+          summon[CpsTryMonad[F]].pure(Some((head, tail)))
+
+    private final def applyFlatMapTryToHead[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+          try
+            f(head)
+          catch
+            case NonFatal(ex) =>
+              WaitF[F,B](summon[CpsTryMonad[F]].error(ex))
+
+  }
+
+
+  case class Susp[F[_]:CpsTryMonad,A](susp: () => UniWrapper[F,A]) extends UniWrapper[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      // TODO: use type-aligned queue or trampolined function
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapper[F,?]]))
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      val next = summon[CpsTryMonad[F]].map(susp().flatMapTry(f).fsplit){
+        case None => Zero[F,B]()
+        case Some((head,tail)) => Cons[F,B](head,tail)
+      }
+      WaitF(next)
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      susp().fsplit
+
+
+
+  }
+
+
+  case class FlatMapQueue[F[_]:CpsTryMonad,A,R](start: UniWrapper[F,A], queue: Queue[Try[?] => UniWrapper[F,?]]) extends UniWrapper[F,R] {
+
+    override def flatMapTry[B](f: Try[R] => UniWrapper[F, B]): UniWrapper[F, B] =
+      FlatMapQueue[F,A,B](start, queue.enqueue(f.asInstanceOf[Try[?] => UniWrapper[F,?]]))
+
+    override def applyFlatMapTry[B](f: Try[R] => UniWrapper[F, B]): UniWrapper[F, B] =
+      applyFlatMaps().applyFlatMapTry(f)
+
+    override def mplus(other: => UniWrapper[F, R]): UniWrapper[F, R] =
+      MPlusQueue[F,R](Queue(this,Susp(()=>other)))
+
+
+    override def fsplit: F[Option[(Try[R], UniWrapper[F, R])]] =
+      summon[CpsTryMonad[F]].flatMap(start.fsplit) {
+        case None => summon[CpsTryMonad[F]].pure(None)
+        case Some((startHead,startTail)) =>
+          val startHeadUniWrapper = FlatMapQueue[F,A,R](fromTry(startHead), queue).applyFlatMaps()
+          summon[CpsTryMonad[F]].flatMap(startHeadUniWrapper.fsplit) {
+            case None => FlatMapQueue(startTail, queue).fsplit
+            case Some((startHeadApplyHead, startHeadApplyTail)) =>
+              val next = Susp(() => startHeadApplyTail mplus FlatMapQueue(startTail, queue))
+              summon[CpsTryMonad[F]].pure(Some((startHeadApplyHead, next)))
+          }
+      }
+
+
+    def applyFlatMaps(): UniWrapper[F,R] =
+      val s0: UniWrapper[F,?] = start.asInstanceOf[UniWrapper[F,?]]
+      val r = queue.foldLeft(s0){ (s,e) =>
+        s.applyFlatMapTry(e.asInstanceOf[Try[s._R] => UniWrapper[F,Any]])
+      }
+      r.asInstanceOf[UniWrapper[F,R]]
+
+  }
+
+
+
+  case class WaitF[F[_]:CpsTryMonad,A](fa: F[UniWrapper[F,A]]) extends UniWrapper[F,A] {
+
+    override def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      WaitF(
+        summon[CpsTryMonad[F]].map(fa)(_.flatMapTry(f))
+      )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      WaitF(
+        summon[CpsTryMonad[F]].map(fa)(_.applyFlatMapTry(f))
+      )
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      summon[CpsTryMonad[F]].flatMap(fa)(_.fsplit)
+
+
+  }
+
+
+  case class MPlusQueue[F[_]:CpsTryMonad,A](queue: Queue[UniWrapper[F,A]]) extends UniWrapper[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      if (queue.isEmpty)
+        Zero[F,B]()
+      else
+        MPlusQueue(queue.map(_.flatMapTry(f)))
+
+    /**
+     * BFS - apply only head
+     * @param f
+     * @tparam B
+     * @return
+     */
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+       queue.dequeueOption match
+         case None => Zero[F,B]()
+         case Some((head,tail)) =>
+            head.applyFlatMapTry(f)  match
+              case Zero() =>
+                if (tail.isEmpty)
+                  Zero[F,B]()
+                else
+                  MPlusQueue(tail).applyFlatMapTry(f)
+              case other => other.mplus(MPlusQueue(tail).flatMapTry(f))
+
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      MPlusQueue[F,A](queue.enqueue(other))
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      queue.dequeueOption match
+        case None => summon[CpsTryMonad[F]].pure(None)
+        case Some((head,tail)) =>
+          summon[CpsTryMonad[F]].flatMap(head.fsplit) {
+            case None => MPlusQueue(tail).fsplit
+            case Some((headHead,headTail)) =>
+              val next = Susp(() => headTail mplus MPlusQueue(tail))
+              summon[CpsTryMonad[F]].pure(Some((headHead, next)))
+          }
+
+
+  }
+
+  case class LVNew[F[_]:CpsTryMonad,A](lv: LogicalVariable[A]) extends UniWrapper[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapper[F,?]]) )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      // lv can participate in the rerursie expression
+      LTerm[F,A](lv,LongMap.empty).applyFlatMapTry(f)
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      summon[CpsTryMonad[F]].pure(None)
+
+  }
+
+  case class LVBind[F[_]:CpsTryMonad,A](lv: LogicalVariable[A], v: UniWrapper[F,A]) extends UniWrapper[F,A] {
+
+    def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+      FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapper[F,?]]) )
+
+    override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] = {
+      toLTerm().applyFlatMapTry(f)
+    }
+
+    override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+      MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+    override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] =
+      toLTerm().fsplit
+
+    def toLTerm(): LTerm[F,A] =
+      LTerm[F,A](lv,LongMap(lv.id -> LVarBingingRecord(lv,v)))
+
+  }
+
+
+
+  case class LVarBingingRecord[F[_],T](lv: LogicalVariable[T], v: UniWrapper[F,T]) {
+    type Tp = T
+  }
+
+  case class SplittedLVarBingingRecord[F[_],T](lv: LogicalVariable[T],
+                                                currentValue: Option[Try[T]],
+                                                next: UniWrapper[F,T])
+
+
+  case class LTerm[F[_]:CpsTryMonad,A](t: TypedLogicalTerm[A], bindings: LongMap[LVarBingingRecord[F,?]]) extends UniWrapper[F,A] {
+
+      def flatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+        FlatMapQueue(this, Queue(f.asInstanceOf[Try[?] => UniWrapper[F,?]]) )
+
+      override def applyFlatMapTry[B](f: Try[A] => UniWrapper[F, B]): UniWrapper[F, B] =
+        WaitF(summon[CpsTryMonad[F]].map(fsplit){
+           case None => Zero[F,B]()
+           case Some((head,tail)) =>
+             val resHead = try {
+                f(head)
+              } catch {
+               case NonFatal(ex) =>
+                 WaitF[F, B](summon[CpsTryMonad[F]].error(ex))
+              }
+             resHead.mplus(tail.flatMapTry(f))
+        })
+
+      override def mplus(other: => UniWrapper[F, A]): UniWrapper[F, A] =
+          MPlusQueue[F,A](Queue(this,Susp(()=>other)))
+
+      override def fsplit: F[Option[(Try[A], UniWrapper[F, A])]] = reify[F]{
+          val optNext = reflect(fsplitInBinding(t, bindings))
+          optNext match
+            case None => None
+            case Some((head, nextBindings)) =>
+              head match
+                case Success(t) =>
+                  Some((Success(t), buildNextBindings(nextBindings.values.toIndexedSeq)))
+                case Failure(ex) =>
+                  Some((Failure(ex), buildNextBindings(nextBindings.values.toIndexedSeq)))
+      }
+
+
+
+      private def fsplitInBinding[A](t: TypedLogicalTerm[A],
+                                     oldBinding: LongMap[LVarBingingRecord[F,?]],
+                                     changedBinding: LongMap[SplittedLVarBingingRecord[F,?]] = LongMap.empty
+                                    ): F[Option[(Try[A], LongMap[SplittedLVarBingingRecord[F,?]])]] = {
+
+        def getVarBinding(id: Long, currentBinding: LongMap[SplittedLVarBingingRecord[F,?]]):
+                                 F[(Option[Try[?]],LongMap[SplittedLVarBingingRecord[F,?]])] = {
+            currentBinding.get(id) match
+              case Some(r)  => summon[CpsTryMonad[F]].pure((r.currentValue, currentBinding))
+              case None => oldBinding.get(id) match
+                case None => summon[CpsTryMonad[F]].error(new RuntimeException(s"unbound variable $id"))
+                case Some(LVarBingingRecord(lv,v)) =>
+                  summon[CpsTryMonad[F]].flatMap(v.fsplit) {
+                    case None =>
+                      val nextBinding = currentBinding.updated(id, SplittedLVarBingingRecord(lv,None,Zero[F,lv.Type]()))
+                      summon[CpsTryMonad[F]].pure((None, nextBinding))
+                    case Some((head,tail)) =>
+                      val nextBinding = currentBinding.updated(id, SplittedLVarBingingRecord(lv,Some(head),tail))
+                      summon[CpsTryMonad[F]].pure((Some(head), nextBinding))
+                  }
+        }
+
+
+        def fetchTerm(term:LogicalTerm, currentBinding: LongMap[SplittedLVarBingingRecord[F,?]]):
+                                 F[(Option[Try[LogicalTerm]],LongMap[SplittedLVarBingingRecord[F,?]])] = {
+
+            term match
+              case l: LogicalVariable[t] =>
+                reify[F] {
+                  val (optTryA, nextBinding) = reflect(getVarBinding(l.id, currentBinding))
+                  val optTerm: Option[Try[LogicalTerm]] = optTryA.map(_.map(a =>
+                    LogicalConstant[t](a.asInstanceOf[t])(using l.symbol)
+                  ))
+                  (optTerm, nextBinding)
+                }
+              case l: LogicalConstant[t] =>
+                summon[CpsTryMonad[F]].pure(Some(Success(l:LogicalTerm)), currentBinding)
+              case l: LogicalFunctionalTerm[t] =>
+                val s0: (IndexedSeq[LogicalTerm], LongMap[SplittedLVarBingingRecord[F, ?]]) = (IndexedSeq.empty, currentBinding)
+                reify[F] {
+                  var done = false
+                  var retval: Option[Try[LogicalTerm]] = None
+                  var i = 0
+                  var s = s0
+                  while(!done && i<l.args.size) {
+                    val (args, currentBinding) = s0
+                    val (optTryArg, nextBinding) = reflect(fetchTerm(l.args(i), currentBinding))
+                    optTryArg match
+                      case None =>
+                        retval = None
+                        done = true
+                      case Some(tryArg) =>
+                        tryArg match
+                          case Failure(ex) =>
+                             retval = Some(Failure(ex))
+                             done = true                         
+                          case Success(arg) =>
+                             s = (args :+ arg) -> nextBinding
+                    i = i+1        
+                  }
+                  val (nextArgs, nextBindings) = s
+                  if (!done) {
+                    val lt: LogicalTerm = LogicalFunctionalTerm(nextArgs)(using l.symbol)
+                    (Some(Success(lt)), nextBindings)
+                  } else {
+                    (retval, nextBindings)
+                  }
+                }
+          
+        }
+
+        reify[F] {
+          val (optTryTerm, bindings) = reflect(fetchTerm(t, changedBinding))
+          val optTryA = optTryTerm.map(_.map(term =>
+            term.symbol.fromTerm(term).getOrElse(
+              throw new IllegalStateException(s"Term is not fully constructed  ($term) ")
+            ).asInstanceOf[A]
+          ))
+          optTryA.map((_,bindings))
+        }
+
+
+      }
+
+
+      private def buildNextBindings(nextBindings: Seq[SplittedLVarBingingRecord[F,?]]): UniWrapper[F,A] = {
+        // here is logical term with already evaluated variables is emitted,  now we need to emit
+        // rest of possible variants.
+        // Generally, the order of emitting can be defined by configurable strategy.
+        // For now, we follow BFS strategy.
+
+        // let <n> is number of variables in term, represent 2^n as a set of bits, where 1 means that
+        // we should emit next variant of variable, 0 - we should emit current value.
+        // then, first variant is 0..0  (emitted before call of nextBinfdings), last is 1..1
+
+
+
+        def buildVariant(bits:Int): UniWrapper[F,A] = {
+          val argsBuilder = IndexedSeq.newBuilder[LogicalTerm]
+          var newBindings = LongMap[LVarBingingRecord[F, ?]]()
+          var i = 0
+          var currentBit = 1
+          var done = false
+          var empty = false
+          var retval: UniWrapper[F, A] = UniWrapper.Zero[F, A]()
+          while (i < nextBindings.size && !done && !empty) {
+            val lvr = nextBindings(i)
+            val lv = lvr.lv
+            val bit = (bits & currentBit) != 0
+            if (bit) {
+              newBindings = newBindings.updated(i, LVarBingingRecord(lv, lvr.next))
+              argsBuilder.addOne(lv)
+            } else {
+              lvr.currentValue match
+                case None =>
+                  empty = true
+                  done = true
+                case Some(tryA) =>
+                  tryA match
+                    case Failure(ex) =>
+                      //we should have only one Failure, so
+                      // check - if this is a minimal variant, then we should return it
+                      //  otherwise - Zero to omitt duplicates
+                      if (bits == currentBit - 1) {
+                        retval = UniWrapper.WaitF[F, A](summon[CpsTryMonad[F]].error(ex))
+                      } else {
+                        retval = UniWrapper.Zero[F, A]()
+                      }
+                      done = true
+                    case Success(a) =>
+                      argsBuilder.addOne(LogicalConstant[lv.Type](a)(using lv.symbol))
+            }
+            i = i + 1
+            currentBit = currentBit << 1
+          }
+          if (done) {
+            retval
+          } else if (empty) {
+            UniWrapper.Zero[F, A]()
+          } else {
+            val args = argsBuilder.result()
+            val term = LogicalFunctionalTerm(args)(using t.symbol)
+            val nextTerm = LTerm[F, A](term, newBindings)
+            if (bits + 1 == (1 << nextBindings.size))
+              nextTerm
+            else
+              nextTerm.mplus(buildVariant(bits + 1))
+          }
+
+        }
+
+        buildVariant(1)
+
+      }
+
+
+  }
+
+  def fromTry[F[_]:CpsTryMonad,A](t: Try[A]): UniWrapper[F,A] =
+    t match
+      case Success(a) => Pure[F,A](a)
+      case Failure(ex) => WaitF(summon[CpsTryMonad[F]].error(ex))
+
+  def error[F[_]:CpsTryMonad,A](msg: String): UniWrapper[F,A] =
+    WaitF(summon[CpsTryMonad[F]].error(new RuntimeException(msg)))
+
+  class UniWrapperEnvironment[ F[_]:CpsTryMonad] extends UnificationEnvironment[[T]=>>UniWrapper[F,T]] {
+
+    thisUnificationEnvironment =>
+
+    class LContext extends UnificationEnvironmentContext[[T]=>>UniWrapper[F,T]] {
+      override def monad: UnificationEnvironment[[T] =>> UniWrapper[F, T]] = thisUnificationEnvironment
+    }
+
+    override type Context = LContext
+
+    override type Observer[X] = F[X]
+
+    def pure[A](a:A): UniWrapper[F,A] =
+      Pure[F,A](a)
+
+    def map[A,B](fa: UniWrapper[F,A])(f: A=>B): UniWrapper[F,B] = ???
+
+    def flatMap[A,B](fa: UniWrapper[F,A])(f: A=>UniWrapper[F,B]): UniWrapper[F,B] = ???
+
+    def flatMapTry[A,B](fa: UniWrapper[F,A])(f: Try[A]=>UniWrapper[F,B]): UniWrapper[F,B] =
+      fa.flatMapTry(f)
+
+    override def error[A](e: Throwable): UniWrapper[F, A] = ???
+
+    override def mzero[A]: UniWrapper[F, A] = ???
+
+    override def mplus[A](x: UniWrapper[F, A], y: =>UniWrapper[F, A]): UniWrapper[F, A] = ???
+
+    override def apply[T](op: LContext => UniWrapper[F, T]): UniWrapper[F, T] = {
+      op(new LContext)
+    }
+
+    override def msplit[A](c: UniWrapper[F, A]): UniWrapper[F, Option[(Try[A], UniWrapper[F, A])]] = ???
+
+    override def observerCpsMonad: CpsTryMonad[F] = summon[CpsTryMonad[F]]
+
+    override def mObserveOne[A](ma: UniWrapper[F, A]): F[Option[A]] = ???
+
+    override def mFoldLeft[A, B](ma: UniWrapper[F, A], zero: F[B])(op: (F[B], F[A]) => F[B]): F[B] = ???
+
+    override def mFoldLeftN[A, B](ma: UniWrapper[F, A], zero: F[B], n: Int)(op: (F[B], F[A]) => F[B]): F[B] = ???
+
+    //TODO: change to bind with M[A] instead of term
+    override def bindTerm[A:Unifiable](lv: LogicalVariable[A], t: TypedLogicalTerm[A]): UniWrapper[F, A] = ???
+
+    override def bind[A:Unifiable](lv: LogicalVariable[A], v: UniWrapper[F, A]): UniWrapper[F, A] = ???
+
+    override def fromTerm[A: Unifiable](t: TypedLogicalTerm[A]): UniWrapper[F, A] = ???
+
+    override def toTerm[A: Unifiable](ma: UniWrapper[F, A]): UniWrapper[F, TypedLogicalTerm[A]] = ???
+
+
+    def cons[T](head: Try[T], tail: UniWrapper[F,T]): UniWrapper[F,T] =
+      Cons[F,T](head,tail)
+
+    def susp[T](susp: () => UniWrapper[F,T]): UniWrapper[F,T] =
+      Susp[F,T](susp)
+
+    def waitF[T](fa: F[UniWrapper[F,T]]): UniWrapper[F,T] =
+      WaitF[F,T](fa)
+
+    def mplusQueue[T](queue: Queue[UniWrapper[F,T]]): UniWrapper[F,T] =
+      MPlusQueue[F,T](queue)
+
+    def lvBind[T](lv: LogicalVariable[T], v: UniWrapper[F,T]): UniWrapper[F,T] =
+      LVBind[F,T](lv,v)
+
+    def lTerm[T](t: TypedLogicalTerm[T], bindings: LongMap[LVarBingingRecord[F,?]]): UniWrapper[F,T] =
+      LTerm[F,T](t,bindings)
+
+  }
+
+
+}
+
diff --git a/shared/src/test/scala/logic/unification2/examples/Point.scala b/shared/src/test/scala/logic/unification2/examples/Point.scala
new file mode 100644
index 00000000..bc23705e
--- /dev/null
+++ b/shared/src/test/scala/logic/unification2/examples/Point.scala
@@ -0,0 +1,69 @@
+package logic.unification2.examples
+
+import cps.*
+import logic.*
+
+import logic.unification2.*
+
+case class Point(x: Int, y: Int)
+
+object Point {
+
+  given Unifiable[Point] with {
+
+    override type Environment[M[_]] = UnificationEnvironment[M]
+
+    override def unify[M[_]:Environment](a: M[Point], b: M[Point])(using Access[Any]): M[Point] = reify[M] {
+
+      a.toTerm match
+        case alv: LogicalVariable[Point] =>
+           alv.bind(b)
+        case aft: LogicalFunctionalTerm[Point] =>
+           b.toTerm match
+             case blv: LogicalVariable[Point] =>
+                blv.bind(a)
+             case bft: LogicalFunctionalTerm[Point] =>
+                guard(aft.symbol == bft.symbol)
+                val x = reflect(summon[Unifiable[Int]].unify(aft.args(0).castToM[Int], bft.args(0).castToM[Int]))
+                val y = reflect(summon[Unifiable[Int]].unify(aft.args(1).castToM[Int], bft.args(1).castToM[Int]))
+                Point(x,y)
+    }
+
+    override def fromTerm(term: LogicalTerm): Option[Point] = {
+      term match
+        case lft: LogicalFunctionalTerm[?] =>
+          if lft.symbol == this then
+            val x = summon[Unifiable[Int]].fromTerm(lft.args(0))
+            val y = summon[Unifiable[Int]].fromTerm(lft.args(1))
+            (x,y) match
+              case (Some(x), Some(y)) => Some(Point(x,y))
+              case _ => None
+          else
+            None
+        case lc: LogicalConstant[?] =>
+          if (lc.symbol == this) then
+            lc.value match
+              case p: Point => Some(p)
+              case _ => None
+          else
+            None
+        case lv: LogicalVariable[?] => 
+          None
+    }
+    
+    
+    /*
+    TODO: eable
+    override def compare(x: Point, y: Point): Int = {
+      x.x - y.x match
+        case 0 => x.y - y.y
+        case other => other
+    }
+    
+     */
+
+    override def className: String = classOf[Point].getCanonicalName
+
+  }
+
+}