swannodette

(define (matches n)
  (run #f (q)
    (fresh (a b c d s1 s2)
       (domfd a b c d s1 s2 (range 1 n)) 
       (all-differentfd `(,a ,b ,c ,d))
       (== a 1)
       (<=fd a b) (<=fd b c) (<=fd c d)
       (plusfd a b s1) (plusfd s1 c s2) (plusfd s2 d n)
       (checko `(,a ,b ,c ,d) () () n)
       (== q `(,a ,b ,c ,d)))))