(define (ot h c) 
  (otter h c))


(define (p P)
  (dmatch P
    ((and P1 P2) (!both (!p P1) (!p P2)))
    ((or P1 P2) (try (!or-imp (assume (not P1) (!p P2)))
		     (!or-imp (assume (not P2) (!p P1)))))
    (
