diff --git a/engine/builtin.go b/engine/builtin.go
index 277b209..66e6af1 100644
--- a/engine/builtin.go
+++ b/engine/builtin.go
@@ -146,7 +146,7 @@ func CallNth(vm *VM, goal, nth Term, k Cont, env *Env) *Promise {
 
 // Unify unifies x and y without occurs check (i.e., X = f(X) is allowed).
 func Unify(_ *VM, x, y Term, k Cont, env *Env) *Promise {
-	env, ok := env.Unify(x, y, false)
+	env, ok := env.Unify(x, y)
 	if !ok {
 		return Bool(false)
 	}
@@ -155,7 +155,7 @@ func Unify(_ *VM, x, y Term, k Cont, env *Env) *Promise {
 
 // UnifyWithOccursCheck unifies x and y with occurs check (i.e., X = f(X) is not allowed).
 func UnifyWithOccursCheck(_ *VM, x, y Term, k Cont, env *Env) *Promise {
-	env, ok := env.Unify(x, y, true)
+	env, ok := env.unifyWithOccursCheck(x, y)
 	if !ok {
 		return Bool(false)
 	}
@@ -164,7 +164,7 @@ func UnifyWithOccursCheck(_ *VM, x, y Term, k Cont, env *Env) *Promise {
 
 // SubsumesTerm succeeds if general and specific are unifiable without binding variables in specific.
 func SubsumesTerm(_ *VM, general, specific Term, k Cont, env *Env) *Promise {
-	theta, ok := env.Unify(general, specific, true)
+	theta, ok := env.unifyWithOccursCheck(general, specific)
 	if !ok {
 		return Bool(false)
 	}
@@ -739,7 +739,7 @@ func collectionOf(vm *VM, agg func([]Term, *Env) Term, template, goal, instances
 			ks = append(ks, func(context.Context) *Promise {
 				env := env
 				for _, w = range wList {
-					env, _ = env.Unify(witness, w, false)
+					env, _ = env.Unify(witness, w)
 				}
 				return Unify(vm, agg(tList, env), instances, k, env)
 			})
@@ -932,7 +932,7 @@ func Catch(vm *VM, goal, catcher, recover Term, k Cont, env *Env) *Promise {
 			e = Exception{term: atomError.Apply(NewAtom("system_error"), NewAtom(err.Error()))}
 		}
 
-		env, ok := env.Unify(catcher, e.term, false)
+		env, ok := env.Unify(catcher, e.term)
 		if !ok {
 			return nil
 		}
diff --git a/engine/builtin_test.go b/engine/builtin_test.go
index 91233e6..0aadc4d 100644
--- a/engine/builtin_test.go
+++ b/engine/builtin_test.go
@@ -370,7 +370,7 @@ func TestUnify(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := Unify(nil, tt.x, tt.y, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -424,7 +424,7 @@ func TestUnifyWithOccursCheck(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := UnifyWithOccursCheck(nil, tt.x, tt.y, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -609,7 +609,7 @@ func TestFunctor(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := Functor(nil, tt.term, tt.name, tt.arity, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -1468,7 +1468,7 @@ func TestBagOf(t *testing.T) {
 			}
 			_, err := BagOf(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
 				for k, v := range tt.env[0] {
-					_, ok := env.Unify(v, k, false)
+					_, ok := env.Unify(v, k)
 					assert.True(t, ok)
 				}
 				tt.env = tt.env[1:]
@@ -1860,7 +1860,7 @@ func TestSetOf(t *testing.T) {
 			}
 			_, err := SetOf(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
 				for k, v := range tt.env[0] {
-					_, ok := env.Unify(v, k, false)
+					_, ok := env.Unify(v, k)
 					assert.True(t, ok)
 				}
 				tt.env = tt.env[1:]
@@ -1923,7 +1923,7 @@ func TestFindAll(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := FindAll(&vm, tt.template, tt.goal, tt.instances, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(v, k, false)
+					_, ok := env.Unify(v, k)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -3739,7 +3739,7 @@ func TestClose(t *testing.T) {
 			t.Run("force but the argument is a variable", func(t *testing.T) {
 				var vm VM
 				_, err := Close(&vm, &Stream{}, List(atomForce.Apply(NewVariable())), Success, nil).Force(context.Background())
-				_, ok := NewEnv().Unify(domainError(validDomainStreamOption, atomForce.Apply(NewVariable()), nil).term, err.(Exception).term, false)
+				_, ok := NewEnv().Unify(domainError(validDomainStreamOption, atomForce.Apply(NewVariable()), nil).term, err.(Exception).term)
 				assert.True(t, ok)
 			})
 
@@ -3913,7 +3913,7 @@ func TestWriteTerm(t *testing.T) {
 			if tt.err == nil {
 				assert.NoError(t, err)
 			} else if te, ok := tt.err.(*Exception); ok {
-				_, ok := NewEnv().Unify(te.term, err.(*Exception).term, false)
+				_, ok := NewEnv().Unify(te.term, err.(*Exception).term)
 				assert.True(t, ok)
 			}
 			if tt.outputPattern == nil {
@@ -5662,7 +5662,7 @@ func TestAtomChars(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := AtomChars(nil, tt.atom, tt.list, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -5727,7 +5727,7 @@ func TestAtomCodes(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := AtomCodes(nil, tt.atom, tt.list, func(env *Env) *Promise {
 				for k, v := range tt.env {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				return Bool(true)
@@ -5821,7 +5821,7 @@ func TestNumberChars(t *testing.T) {
 
 		t.Run("list-ish", func(t *testing.T) {
 			_, err := NumberChars(nil, Integer(0), PartialList(NewAtom("b"), NewVariable()), Success, nil).Force(context.Background())
-			_, ok := NewEnv().Unify(err.(Exception).Term(), typeError(validTypeList, PartialList(NewAtom("b"), NewVariable()), nil).Term(), false)
+			_, ok := NewEnv().Unify(err.(Exception).Term(), typeError(validTypeList, PartialList(NewAtom("b"), NewVariable()), nil).Term())
 			assert.True(t, ok)
 		})
 	})
@@ -6054,7 +6054,7 @@ func TestStreamProperty(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := StreamProperty(&vm, tt.stream, tt.property, func(env *Env) *Promise {
 				for k, v := range tt.env[0] {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				tt.env = tt.env[1:]
@@ -7359,7 +7359,7 @@ func TestAppend(t *testing.T) {
 		t.Run(tt.title, func(t *testing.T) {
 			ok, err := Append(nil, tt.xs, tt.ys, tt.zs, func(env *Env) *Promise {
 				for k, v := range tt.env[0] {
-					_, ok := env.Unify(k, v, false)
+					_, ok := env.Unify(k, v)
 					assert.True(t, ok)
 				}
 				tt.env = tt.env[1:]
diff --git a/engine/env.go b/engine/env.go
index c8e21a8..d3de6f4 100644
--- a/engine/env.go
+++ b/engine/env.go
@@ -264,7 +264,16 @@ func (e *Env) appendFreeVariables(fvs variables, t Term) variables {
 	return fvs
 }
 
-func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
+// Unify unifies 2 terms.
+func (e *Env) Unify(x, y Term) (*Env, bool) {
+	return e.unify(x, y, false)
+}
+
+func (e *Env) unifyWithOccursCheck(x, y Term) (*Env, bool) {
+	return e.unify(x, y, true)
+}
+
+func (e *Env) unify(x, y Term, occursCheck bool) (*Env, bool) {
 	x, y = e.Resolve(x), e.Resolve(y)
 	switch x := x.(type) {
 	case Variable:
@@ -279,7 +288,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
 	case Compound:
 		switch y := y.(type) {
 		case Variable:
-			return e.Unify(y, x, occursCheck)
+			return e.unify(y, x, occursCheck)
 		case Compound:
 			if x.Functor() != y.Functor() {
 				return e, false
@@ -289,7 +298,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
 			}
 			var ok bool
 			for i := 0; i < x.Arity(); i++ {
-				e, ok = e.Unify(x.Arg(i), y.Arg(i), occursCheck)
+				e, ok = e.unify(x.Arg(i), y.Arg(i), occursCheck)
 				if !ok {
 					return e, false
 				}
@@ -301,7 +310,7 @@ func (e *Env) Unify(x, y Term, occursCheck bool) (*Env, bool) {
 	default: // atomic
 		switch y := y.(type) {
 		case Variable:
-			return e.Unify(y, x, occursCheck)
+			return e.unify(y, x, occursCheck)
 		default:
 			return e, x == y
 		}
diff --git a/engine/text_test.go b/engine/text_test.go
index 095f1ea..acc4a5d 100644
--- a/engine/text_test.go
+++ b/engine/text_test.go
@@ -366,7 +366,7 @@ func TestVM_Consult(t *testing.T) {
 			ok, err := Consult(&vm, tt.files, Success, nil).Force(context.Background())
 			assert.Equal(t, tt.ok, ok)
 			if e, ok := tt.err.(Exception); ok {
-				_, ok := NewEnv().Unify(e.Term(), err.(Exception).Term(), false)
+				_, ok := NewEnv().Unify(e.Term(), err.(Exception).Term())
 				assert.True(t, ok)
 			} else {
 				assert.Equal(t, tt.err, err)
diff --git a/engine/vm.go b/engine/vm.go
index 30afde7..2a68b2a 100644
--- a/engine/vm.go
+++ b/engine/vm.go
@@ -229,7 +229,7 @@ func (*VM) execConst(r *registers) *Promise {
 	x := r.xr[r.pc[0].operand]
 	arest := NewVariable()
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, Cons(x, arest), false)
+	r.env, ok = r.env.Unify(r.args, Cons(x, arest))
 	if !ok {
 		return Bool(false)
 	}
@@ -242,7 +242,7 @@ func (*VM) execVar(r *registers) *Promise {
 	v := r.vars[r.pc[0].operand]
 	arest := NewVariable()
 	var ok bool
-	r.env, ok = r.env.Unify(Cons(v, arest), r.args, false)
+	r.env, ok = r.env.Unify(Cons(v, arest), r.args)
 	if !ok {
 		return Bool(false)
 	}
@@ -255,7 +255,7 @@ func (vm *VM) execFunctor(r *registers) *Promise {
 	pi := r.xr[r.pc[0].operand].(procedureIndicator)
 	arg, arest := NewVariable(), NewVariable()
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
+	r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
 	if !ok {
 		return Bool(false)
 	}
@@ -281,13 +281,13 @@ func (vm *VM) execFunctor(r *registers) *Promise {
 
 func (*VM) execPop(r *registers) *Promise {
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, List(), false)
+	r.env, ok = r.env.Unify(r.args, List())
 	if !ok {
 		return Bool(false)
 	}
 	r.pc = r.pc[1:]
 	a, arest := NewVariable(), NewVariable()
-	r.env, ok = r.env.Unify(r.astack, Cons(a, arest), false)
+	r.env, ok = r.env.Unify(r.astack, Cons(a, arest))
 	if !ok {
 		return Bool(false)
 	}
@@ -298,11 +298,11 @@ func (*VM) execPop(r *registers) *Promise {
 
 func (*VM) execEnter(r *registers) *Promise {
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, List(), false)
+	r.env, ok = r.env.Unify(r.args, List())
 	if !ok {
 		return Bool(false)
 	}
-	r.env, ok = r.env.Unify(r.astack, List(), false)
+	r.env, ok = r.env.Unify(r.astack, List())
 	if !ok {
 		return Bool(false)
 	}
@@ -316,7 +316,7 @@ func (*VM) execEnter(r *registers) *Promise {
 func (vm *VM) execCall(r *registers) *Promise {
 	pi := r.xr[r.pc[0].operand].(procedureIndicator)
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, List(), false)
+	r.env, ok = r.env.Unify(r.args, List())
 	if !ok {
 		return Bool(false)
 	}
@@ -361,7 +361,7 @@ func (vm *VM) execList(r *registers) *Promise {
 	l := r.xr[r.pc[0].operand].(Integer)
 	arg, arest := NewVariable(), NewVariable()
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
+	r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
 	if !ok {
 		return Bool(false)
 	}
@@ -376,7 +376,7 @@ func (vm *VM) execPartial(r *registers) *Promise {
 	l := r.xr[r.pc[0].operand].(Integer)
 	arg, arest := NewVariable(), NewVariable()
 	var ok bool
-	r.env, ok = r.env.Unify(r.args, Cons(arg, arest), false)
+	r.env, ok = r.env.Unify(r.args, Cons(arg, arest))
 	if !ok {
 		return Bool(false)
 	}
diff --git a/examples/call_go_from_prolog/main.go b/examples/call_go_from_prolog/main.go
index 89c118f..8dc4a99 100644
--- a/examples/call_go_from_prolog/main.go
+++ b/examples/call_go_from_prolog/main.go
@@ -26,7 +26,7 @@ func main() {
 		}
 
 		// Return values by unification with the output arguments.
-		env, ok = env.Unify(status, engine.Integer(resp.StatusCode), false)
+		env, ok = env.Unify(status, engine.Integer(resp.StatusCode))
 		if !ok {
 			return engine.Bool(false)
 		}
diff --git a/solutions_test.go b/solutions_test.go
index b96dffc..acef35b 100644
--- a/solutions_test.go
+++ b/solutions_test.go
@@ -20,7 +20,7 @@ func TestSolutions_Close(t *testing.T) {
 func TestSolutions_Next(t *testing.T) {
 	t.Run("ok", func(t *testing.T) {
 		v := engine.NewVariable()
-		env, _ := engine.NewEnv().Unify(v, engine.NewAtom("foo"), false)
+		env, _ := engine.NewEnv().Unify(v, engine.NewAtom("foo"))
 		more := make(chan bool, 1)
 		defer close(more)
 		next := make(chan *engine.Env, 1)
@@ -68,7 +68,7 @@ func TestSolutions_Scan(t *testing.T) {
 		varBar:     engine.NewAtom("bar"),
 		varBaz:     engine.NewAtom("baz"),
 	} {
-		env, _ = env.Unify(k, v, false)
+		env, _ = env.Unify(k, v)
 	}
 
 	sols := Solutions{