!(set-env
  (letrec
      (

       (a-and-b
        (conj
         (call/fresh (lambda (a) (== a 7)))
         (call/fresh
          (lambda (b)
            (disj
             (== b 5)
             (== b 6))))))

       (fives
        (lambda (x)
          (disj
           (== x 5)
           (lambda (a/c)
             (lambda ()
               ((fives x) a/c))))))

       (appendo
        (lambda (l s out)
          (disj
           (conj (== '() l) (== s out))
           (call/fresh
            (lambda (a)
              (call/fresh
               (lambda (d)
                 (conj
                  (== (cons a d) l)
                  (call/fresh
                   (lambda (res)
                     (conj
                      (== (cons a res) out)
                      (lambda (s/c)
                        (lambda ()
                          ((appendo d s res) s/c))))))))))))))

       (appendo2
        (lambda (l s out)
          (disj
           (conj (== '() l) (== s out))
           (call/fresh
            (lambda (a)
              (call/fresh
               (lambda (d)
                 (conj
                  (== (cons a d) l)
                  (call/fresh
                   (lambda (res)
                     (conj
                      (lambda (s/c)
                        (lambda ()
                          ((appendo2 d s res) s/c)))
                      (== (cons a res) out))))))))))))

       (call-appendo
        (call/fresh
         (lambda (q)
           (call/fresh
            (lambda (l)
              (call/fresh
               (lambda (s)
                 (call/fresh
                  (lambda (out)
                    (conj
                     (appendo l s out)
                     (== (cons l (cons s (cons out '()))) q)))))))))))

       (call-appendo2
        (call/fresh
         (lambda (q)
           (call/fresh
            (lambda (l)
              (call/fresh
               (lambda (s)
                 (call/fresh
                  (lambda (out)
                    (conj
                     (appendo2 l s out)
                     (== (cons l (cons s (cons out '()))) q)))))))))))

       )
    (current-env)
    ))