(load "resolution.scm")

(define positive-clauseo
  (lambda (cl)
    (fresh (a d res)
      (conde
        [(== `() cl)]
        [(== `(,a . ,d) cl)
         (conde
           [(never-pairo a)]
           [(fresh (aa dd)
              (== `(,aa . ,dd) a)
              (never-equalo aa 'not))])
         (positive-clauseo d)]))))

(define proof-loop
  (lambda (given cls proof out)
    (fresh (cl ncl cl-f given-f lit1 lit2 neg res1 res2 res-cl cl-copy given-copy)
      (membero cl cls)
      (copy-termo cl cl-copy)
      (copy-termo given given-copy)

      (factor-clauseo cl-copy cl-f)
      (factor-clauseo given-copy given-f)

      (rembero lit1 cl-f res1)
      (rembero lit2 given-f res2)

      (negateo lit2 neg)
      (~~ lit1 neg)
            
      (appendo res1 res2 res-cl)

      (conde
        [(positive-clauseo given)]
        [(positive-clauseo cl)])

      (conda
       [(tautologyo res-cl)
        fail]
       [succeed])

      (conde
        [(== '() res-cl) (== `(() ,cl . ,proof) out)]
        [(proof-loop res-cl `(,given . ,cls) `(,res-cl ,cl . ,proof) out)]))))