Why doesn't the expression terminate?

gistfile1.clj

(defn segmento [left middle right all]
  (fresh [xs]
    (appendo left middle xs)
    (appendo xs right all)))


user> (run* [q] 
        (segmento [1 2] [3 4] [5 6] [1 2 3 4 5 6]))
(_.0)

user> (run* [q] 
        (segmento [1 2] [3 4] [5 6] q))
((1 2 3 4 5 6))

user> (run* [q] 
        (segmento [1 2] [3 4] q [1 2 3 4 5 6]))
((5 6))

user> (run* [q] 
        (segmento [1 2] q [5 6] [1 2 3 4 5 6]))
((3 4))

user> (run* [q] 
        (fresh [xs ys] 
          (segmento [1 2] xs ys [1 2 3 4 5 6]) 
          (== q [xs ys])))
([() (3 4 5 6)] 
 [(3) (4 5 6)] 
 [(3 4) (5 6)] 
 [(3 4 5) (6)] 
 [(3 4 5 6) ()])

;; Does not terminate.
;; user> (run* [q] (segmento q [3 4] [5 6] [1 2 3 4 5 6]))
; Evaluation aborted.

;; Changing the order of the clauses yields "expected" results:

(defn segmento [left middle right all]
  (fresh [xs]
    (appendo xs right all)
    (appendo left middle xs)))


user> (run* [q]
        (fresh [a b c]
          (segmento a b c [1 2 3 4 5 6])
          (== q [a b c])))
([() () [1 2 3 4 5 6]]
 [() (1) (2 3 4 5 6)]
 [(1) () (2 3 4 5 6)]
 [() (1 2) (3 4 5 6)]
 [(1) (2) (3 4 5 6)]
 [() (1 2 3) (4 5 6)]
 [(1 2) () (3 4 5 6)]
 [(1) (2 3) (4 5 6)]
 [() (1 2 3 4) (5 6)]
 [(1 2) (3) (4 5 6)]
 [(1 2 3) () (4 5 6)]
 [(1) (2 3 4) (5 6)]
 [() (1 2 3 4 5) (6)]
 [(1 2) (3 4) (5 6)]
 [(1 2 3) (4) (5 6)]
 [(1) (2 3 4 5) (6)]
 [(1 2 3 4) () (5 6)]
 [() (1 2 3 4 5 6) ()]
 [(1 2) (3 4 5) (6)]
 [(1) (2 3 4 5 6) ()]
 [(1 2 3) (4 5) (6)]
 [(1 2) (3 4 5 6) ()]
 [(1 2 3 4) (5) (6)]
 [(1 2 3) (4 5 6) ()]
 [(1 2 3 4 5) () (6)]
 [(1 2 3 4) (5 6) ()]
 [(1 2 3 4 5) (6) ()]
 [(1 2 3 4 5 6) () ()])

You have to be very careful with recursive goals. It best to ground variables before calling recursive goals.

@swannodette - Both calls to appendo are (implicitly) recursive, yet the two definitions behave very differently. I thought that since appendo always (seems to) terminates I could build bigger abstractions on top of it.

Is it immediately clear for an experienced logic programmer to realize why the second definition of segmento always terminates while the first one doesn't?

It's important to consider which one receives ground vars and which one does not

I'll understand what that means when I get my version of TRS :) (it's on its way!)