==========================================
unify in FOO : f(X, Y) =? f(U, V) .

Solution 1
X --> #1:Foo
Y --> #2:Foo
U --> #1:Foo
V --> #2:Foo

Solution 2
X --> 1f
Y --> #1:Foo
U --> 1f
V --> #1:Foo

Solution 3
X --> 1f
Y --> f(#1:Foo, #2:Foo)
U --> #1:Foo
V --> #2:Foo

Solution 4
X --> 1f
Y --> #1:Foo
U --> 1f
V --> #1:Foo

Solution 5
X --> #1:Foo
Y --> #2:Foo
U --> 1f
V --> f(#1:Foo, #2:Foo)
==========================================
variant unify in FOO : f(X, Y) =? f(U, V)  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> %1:Foo
V --> %2:Foo

Unifier #2
rewrites: 0
X --> 1f
Y --> f(%1:Foo, %2:Foo)
U --> %1:Foo
V --> %2:Foo

Unifier #3
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> 1f
V --> f(%1:Foo, %2:Foo)

No more unifiers.
rewrites: 0
==========================================
unify in FOO : f(X, Y) =? X .

Solution 1
X --> 1f
Y --> 1f
==========================================
variant unify in FOO : f(X, Y) =? X  .

Unifier #1
rewrites: 0
X --> 1f
Y --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO : f(X, Y) =? Y .

Solution 1
X --> 1f
Y --> #1:Foo
==========================================
variant unify in FOO : f(X, Y) =? Y  .

Unifier #1
rewrites: 0
X --> 1f
Y --> %1:Foo

No more unifiers.
rewrites: 0
==========================================
unify in FOO2 : f(X, Y) =? f(U, V) .

Solution 1
X --> #1:Foo
Y --> #2:Foo
U --> #1:Foo
V --> #2:Foo

Solution 2
X --> #1:Foo
Y --> 1f
U --> #1:Foo
V --> 1f

Solution 3
X --> f(#1:Foo, #2:Foo)
Y --> 1f
U --> #1:Foo
V --> #2:Foo

Solution 4
X --> #1:Foo
Y --> 1f
U --> #1:Foo
V --> 1f

Solution 5
X --> #1:Foo
Y --> #2:Foo
U --> f(#1:Foo, #2:Foo)
V --> 1f
==========================================
variant unify in FOO2 : f(X, Y) =? f(U, V)  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> %1:Foo
V --> %2:Foo

Unifier #2
rewrites: 0
X --> f(%1:Foo, %2:Foo)
Y --> 1f
U --> %1:Foo
V --> %2:Foo

Unifier #3
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> f(%1:Foo, %2:Foo)
V --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO2 : f(X, Y) =? X .

Solution 1
X --> #1:Foo
Y --> 1f
==========================================
variant unify in FOO2 : f(X, Y) =? X  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO2 : f(X, Y) =? Y .

Solution 1
X --> 1f
Y --> 1f
==========================================
variant unify in FOO2 : f(X, Y) =? Y  .

Unifier #1
rewrites: 0
X --> 1f
Y --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO3 : f(X, Y) =? f(U, V) .

Solution 1
X --> #1:Foo
Y --> #2:Foo
U --> #1:Foo
V --> #2:Foo

Solution 2
X --> 1f
Y --> #1:Foo
U --> 1f
V --> #1:Foo

Solution 3
X --> 1f
Y --> #1:Foo
U --> #1:Foo
V --> 1f

Solution 4
X --> 1f
Y --> f(#1:Foo, #2:Foo)
U --> #1:Foo
V --> #2:Foo

Solution 5
X --> #1:Foo
Y --> 1f
U --> 1f
V --> #1:Foo

Solution 6
X --> #1:Foo
Y --> 1f
U --> #1:Foo
V --> 1f

Solution 7
X --> f(#1:Foo, #2:Foo)
Y --> 1f
U --> #1:Foo
V --> #2:Foo

Solution 8
X --> 1f
Y --> #1:Foo
U --> 1f
V --> #1:Foo

Solution 9
X --> #1:Foo
Y --> 1f
U --> 1f
V --> #1:Foo

Solution 10
X --> #1:Foo
Y --> #2:Foo
U --> 1f
V --> f(#1:Foo, #2:Foo)

Solution 11
X --> 1f
Y --> #1:Foo
U --> #1:Foo
V --> 1f

Solution 12
X --> #1:Foo
Y --> 1f
U --> #1:Foo
V --> 1f

Solution 13
X --> #1:Foo
Y --> #2:Foo
U --> f(#1:Foo, #2:Foo)
V --> 1f
==========================================
variant unify in FOO3 : f(X, Y) =? f(U, V)  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> %1:Foo
V --> %2:Foo

Unifier #2
rewrites: 0
X --> 1f
Y --> f(%1:Foo, %2:Foo)
U --> %1:Foo
V --> %2:Foo

Unifier #3
rewrites: 0
X --> f(%1:Foo, %2:Foo)
Y --> 1f
U --> %1:Foo
V --> %2:Foo

Unifier #4
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> 1f
V --> f(%1:Foo, %2:Foo)

Unifier #5
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
U --> f(%1:Foo, %2:Foo)
V --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO3 : f(X, Y) =? X .

Solution 1
X --> 1f
Y --> 1f

Solution 2
X --> #1:Foo
Y --> 1f
==========================================
variant unify in FOO3 : f(X, Y) =? X  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO3 : f(X, Y) =? Y .

Solution 1
X --> 1f
Y --> #1:Foo

Solution 2
X --> 1f
Y --> 1f
==========================================
variant unify in FOO3 : f(X, Y) =? Y  .

Unifier #1
rewrites: 0
X --> 1f
Y --> %1:Foo

No more unifiers.
rewrites: 0
==========================================
unify in FOO4 : f(X, Y) =? f(U, V) .

Solution 1
X --> #1:Foo
Y --> #2:Foo
V --> #1:Foo
U --> #2:Foo

Solution 2
X --> #2:Foo
Y --> #1:Foo
V --> #1:Foo
U --> #2:Foo

Solution 3
X --> 1f
Y --> #1:Foo
V --> 1f
U --> #1:Foo

Solution 4
X --> 1f
Y --> #1:Foo
V --> #1:Foo
U --> 1f

Solution 5
X --> 1f
Y --> f(#1:Foo, #2:Foo)
V --> #1:Foo
U --> #2:Foo

Solution 6
X --> #1:Foo
Y --> 1f
V --> 1f
U --> #1:Foo

Solution 7
X --> #1:Foo
Y --> 1f
V --> #1:Foo
U --> 1f

Solution 8
X --> f(#1:Foo, #2:Foo)
Y --> 1f
V --> #1:Foo
U --> #2:Foo

Solution 9
X --> 1f
Y --> #1:Foo
V --> 1f
U --> #1:Foo

Solution 10
X --> #1:Foo
Y --> 1f
V --> 1f
U --> #1:Foo

Solution 11
X --> #1:Foo
Y --> #2:Foo
V --> 1f
U --> f(#1:Foo, #2:Foo)

Solution 12
X --> 1f
Y --> #1:Foo
V --> #1:Foo
U --> 1f

Solution 13
X --> #1:Foo
Y --> 1f
V --> #1:Foo
U --> 1f

Solution 14
X --> #1:Foo
Y --> #2:Foo
V --> f(#1:Foo, #2:Foo)
U --> 1f
==========================================
variant unify in FOO4 : f(X, Y) =? f(U, V)  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
V --> %1:Foo
U --> %2:Foo

Unifier #2
rewrites: 0
X --> %2:Foo
Y --> %1:Foo
V --> %1:Foo
U --> %2:Foo

Unifier #3
rewrites: 0
X --> 1f
Y --> f(%1:Foo, %2:Foo)
V --> %1:Foo
U --> %2:Foo

Unifier #4
rewrites: 0
X --> f(%1:Foo, %2:Foo)
Y --> 1f
V --> %1:Foo
U --> %2:Foo

Unifier #5
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
V --> 1f
U --> f(%1:Foo, %2:Foo)

Unifier #6
rewrites: 0
X --> %1:Foo
Y --> %2:Foo
V --> f(%1:Foo, %2:Foo)
U --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO4 : f(X, Y) =? X .

Solution 1
X --> 1f
Y --> 1f

Solution 2
X --> #1:Foo
Y --> 1f
==========================================
variant unify in FOO4 : f(X, Y) =? X  .

Unifier #1
rewrites: 0
X --> %1:Foo
Y --> 1f

No more unifiers.
rewrites: 0
==========================================
unify in FOO4 : f(X, Y) =? Y .

Solution 1
X --> 1f
Y --> #1:Foo

Solution 2
X --> 1f
Y --> 1f
==========================================
variant unify in FOO4 : f(X, Y) =? Y  .

Unifier #1
rewrites: 0
X --> 1f
Y --> %1:Foo

No more unifiers.
rewrites: 0
Bye.