(define tests
  (test-suite
   "Tests"
   (check-equal? (check-proof?
                  '(cnf (clause (lit #f p) (lit #t q))
                        (clause (lit #t p) (lit #t q))
                        (clause (lit #f q) (lit #t r))
                        (clause (lit #f q) (lit #f r)))
                  '(res q
                        (res p (axiom (clause (lit #t p) (lit #t q)))
                             (axiom (clause (lit #f p) (lit #t q))))
                        (res r (axiom (clause (lit #f q) (lit #t r)))
                             (axiom (clause (lit #f q) (lit #f r)))))) true
                                                                       "Test 1 failed")
   (check-equal? (check-proof?
                  '(cnf (clause (lit #f q))
                        (clause (lit #t q)))
                  '(res q
                        (axiom (clause (lit #t q)))
                        (axiom (clause (lit #f q))))) true
                                                      "Test 4 failed")))