let rec unify term1 term2 acc =
    match term1 with
    | Atom(x) -> match term2 with
                                | Atom(y) -> (x=y, acc)
                                | Variable(y) -> (true, acc + y + " "+x+";")
                                | _ -> (false, acc)

    | Variable(x) -> match term2 with
                                | Atom(y) -> (true, acc + x + " "+y+";")
                                | Variable(y) -> (true, acc + x + " "+y+";")
                                | Structure(n, l) -> (true, acc + x + " "+string(Structure(n, l))+";")
                                | _ -> (false, acc)

    | Structure(nx, x) -> match term2 with
                                | Variable(y) -> (true, acc + y + " "+string(Structure(nx, x))+";")
                                | Structure(ny, y) -> if x.Length <> y.Length then (false, acc) else (Seq.zip x y)
                                                                                                                |> Seq.map(fun s -> unify (fst s) (snd s) "")
                                                                                                                |> Seq.reduce(fun (s1, s2) (acc1, acc2)-> (s1&&acc1, s2+acc2))
                                | _ -> (false, acc)

    | _ -> (false, acc)