(define (dp-prove premices/conclusions run-count)
  (define remove-implications-time 0)
  (define remove-implications-count 0)
  (define to-NNF-count 0)
  (define to-NNF-time 0)
  (define flatten-count 0)
  (define flatten-time 0)
  (define to-CNF-count 0)
  (define to-CNF-time 0)
  (define dp-sat?-count 0)
  (define dp-sat?-time 0)
  (define start-time 0)
  (define answer (if #f 1))
  
  (define (start-timer)
    (set! start-time (process-time-clock)))
  
  (define (timer-value)
    (- (process-time-clock) start-time))


  
  ;here are some predicate functions for recognizing patterns sentences
  (define (atomic? x) (not (list? x)))
  (define (literal? x) (or (atomic? x) (and (neg? x) (atomic? (second x)))))
  (define (neg? x) (and (list? x) (equal? (length x) 2) (equal? (first x) '~)))
  (define (conj? x) (and (list? x) (>= (length x) 2) (equal? (first x) '++)))   
  (define (disj? x) (and (list? x) (>= (length x) 2) (equal? (first x) '**)))
  (define (cond? x) (and (list? x) (= (length x) 3) (equal? (first x) '->)))
  (define (bicond? x) (and (list? x) (= (length x) 3) (equal? (first x) '<->)))
  
  ;three simple functions to create sentences
  (define (disj x y)
    (cond ((and (disj? x) (disj? y)) (append x (cdr y)))
	  ((disj? x) (append x (list y)))
	  ((disj? y) (append y (list x)))
	  (else (list '** x y))))

  (define (conj x y)
    (cond ((and (conj? x) (conj? y)) (append x (cdr y)))
	  ((conj? x) (append x (list y)))
	  ((conj? y) (append y (list x)))
	  (else (list '++ x y))))
  
  (define (dp-not x)
    (if (neg? x) (second x)
	(list '~ x)))
  
  ;this function removes all implications from a sentence
  (define (remove-implications x) 
    (set! remove-implications-count (+ 1 remove-implications-count))
    (cond ((literal? x) x)
	  ((cond? x) 
	   (list '** 
		 (list '~ (remove-implications (second x))) 
		 (remove-implications (third x))))
	  ((bicond? x) 
	   (list '++
		 (list '**
		       (list '~ (remove-implications (second x))) 
		       (remove-implications (third x)))
		 (list '** 
		       (list '~ (remove-implications (third x))) 
		       (remove-implications (second x)))))
	  (else (cons (first x) (map remove-implications (cdr x))))))
  
  ;converts a sentence (assumed to contain no implications) into negated normal form
  (define (to-NNF x)
    (set! to-NNF-count (+ 1 to-NNF-count))
    (cond ((literal? x) x)
	  ((and (neg? x) (neg? (second x))) (to-NNF (second (second x))))
	  ((conj? x) (cons '++ (map to-NNF (cdr x))))
	  ((disj? x) (cons '** (map to-NNF (cdr x))))
	  ((and (neg? x) (conj? (second x)))
	   (to-NNF (cons '** (map (lambda (element) (list '~ element))
				  (cdr (second x))))))	  
	  ((and (neg? x) (disj? (second x)))
	   (to-NNF (cons '++ (map (lambda (element) (list '~ element))
				  (cdr (second x))))))
	  (else (error '"Invalid formula format\n"))))
  
  ;takes a list and returns a list of two lists, where the first list is all the elements
  ;of lst where (rule lst) returned true and the second list is the remaining elements.
  (define (split-list lst rule)
    (if (not lst) '(() ())
	(let ((head (car lst))
	      (tail (split-list (cdr lst) rule)))
	  (if (rule head)
	      (list (cons head (first tail)) (second tail))
	      (list (first tail) (cons head (second tail)))))))
  
  
  ;takes a disjunction,x, and for every disjunt,y, if y is a disjunct, then the 
  ;elements of y are added to x and y is removed.
  (define (flatten-disjuncts x)
    (if (not x) '()
	(let ((first-disjunct (car x))
	      (remaining-disjuncts (cdr x)))
	  (cond ((not first-disjunct) '())
		((disj? first-disjunct) 
		 (append (flatten-disjuncts (cdr first-disjunct))
			 (flatten-disjuncts remaining-disjuncts)))
		(else (cons first-disjunct
			    (flatten-disjuncts remaining-disjuncts)))))))
  
  (define (flatten-conjuncts x)
    (if (not x) '()
	(let ((first-conjunct (car x))
	      (remaining-conjuncts (cdr x)))
	  (cond ((not first-conjunct) '())
		((conj? first-conjunct) 
		 (append (flatten-conjuncts (cdr first-conjunct))
			 (flatten-conjuncts remaining-conjuncts)))
		(else (cons first-conjunct
			    (flatten-conjuncts remaining-conjuncts)))))))
  
  ;takes a disjunction xx and returns an equivelent sentence,y, where y is either a disjunction containing only literals
  ;or y is a conjunction
  (define (distr x)
    (if (not (disj? x))
	(error "Sentence to distribute is not a disjunction")
	(let* ((flattened (flatten-disjuncts (cdr x)))
	       (seperated-by-lit (split-list flattened literal?))
	       (literals (first seperated-by-lit))
	       (conjunctions (second seperated-by-lit)))
	  (if (not conjunctions) (cons '** literals)
	      (let ((final-conjunction (if literals 
					   (map (lambda (y) (distr (disj y (cons '** literals)))) (cdr (first conjunctions)))
					   (cdr (first conjunctions)))))
		(do ((conjunctions (cdr conjunctions) (cdr conjunctions)))
		    ((not conjunctions) (cons '++ final-conjunction))
		  (set! final-conjunction
			(map (lambda (y) (distr (disj (first conjunctions) y))) final-conjunction))))))))

  ;converts an NNF to CNF
  (define (to-CNF x)
   (set! to-CNF-count (+ 1 to-CNF-count))
   (cond ((literal? x) x)
	 ((conj? x) (cons '++ (map to-CNF (cdr x))))
	 ((disj? x) (distr x))))

  
  
  (define (flatten x)
    (set! flatten-count (+ 1 flatten-count))
    (if (literal? x) x
	(let* ((operation (car x))
	       (elems (map flatten (cdr x)))
	       (split-elems  (split-list elems (lambda (c)
						 (and (list? c) (equal? operation (first c))))))
	       (same-elems (apply append (map cdr (first split-elems))))
	       (diff-elems (second split-elems)))
	  (cons operation (append same-elems diff-elems)))))
  
  (define (to-clausal-form x)
    (map (lambda (c) (if (literal? c) (list c) (cdr c))) (cdr x)))
  
  (define (dp-get-literal x)
    (if (not x) '()
	(let ((head (car x))
	      (tail (cdr x)))
	  (if head
	      (first head)
	      (dp-get-literal tail)))))
  
  (define (dp-remove-lit lit x)
    (if (not x) '()
	(let ((head (car x))
	      (tail (cdr x)))
	  (if (member lit head)
	      (dp-remove-lit lit tail)
	      (cons (delete (dp-not lit) head) 
		    (dp-remove-lit lit tail))))))
   
  (define (dp-sat? x)
    (set! dp-sat?-count (+ 1 dp-sat?-count))
    (cond ((not x) #t)
	  ((member '() x) #f)
	  (else
	   (let ((lit (dp-get-literal x)))
	     (or (dp-sat? (dp-remove-lit lit x))
		 (dp-sat? (dp-remove-lit (dp-not lit) x)))))))



  ;----------- start the program
 (define begin-time (process-time-clock))
 (do ((i run-count (- i 1)))
     ((= i 0) #t )
  
   (let* ((premices (case (length (first premices/conclusions))
		     ((0) '())
		     ((1) (first (first premices/conclusions)))
		     (else (cons '++ (first premices/conclusions)))))
	  (conclusions (case (length (second premices/conclusions))
			 ((0) '())
			 ((1)(list '~ (first (second premices/conclusions))))
			 (else (list '~ (cons '++ (second premices/conclusions))))))
	  (KB (if (and premices conclusions) 
		  (conj premices conclusions)
		  (append premices conclusions))))
     
     (start-timer)
     (set! KB (remove-implications KB))
     (set! remove-implications-time (+ remove-implications-time (timer-value)))
     
     (start-timer)
     (set! KB (to-NNF KB))
     (set! to-NNF-time (+ to-NNF-time (timer-value)))
   
     (start-timer)
     (set! KB (to-CNF KB))
     (set! to-CNF-time (+ to-CNF-time (timer-value)))
     
     (start-timer)
     (set! KB (flatten KB))
     (set! flatten-time (+ flatten-time (timer-value)))
     
     
     (set! KB (to-clausal-form KB))
     
     (start-timer)
     (set! answer (not (dp-sat? KB)))
     (set! dp-sat?-time (+ dp-sat?-time (timer-value)))))
  
   
   
   (define end-time (process-time-clock))
   (list (list answer 
	       (- end-time begin-time)
	       run-count)
	 (list remove-implications-time 
	       remove-implications-count)
	 (list to-NNF-time
	       to-NNF-count)
	 (list flatten-time 
	       flatten-count)
	 (list to-CNF-time
	       to-CNF-count)
	 (list dp-sat?-time
	       dp-sat?-count)))