(define (egdp-prove premices/conclusions run-count)
  (define pl->eg-count 0)
  (define pl->eg-time 0)
  (define egdp-sat?-count 0)
  (define egdp-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))

;-----

  (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) '<->)))

  (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)))

  (define (pl->eg x)
    (set! pl->eg-count (+ 1 pl->eg-count))
    (cond ((not x) '())
	  ((atomic? x) (list x))
	  ((neg? x) (let ((elem (second x)))
		      (if (neg? elem)
			  (pl->eg (second elem))
			  (list (pl->eg elem)))))
	  ((conj? x) (apply append (map pl->eg (cdr x))))
	  ((disj? x) (pl->eg (list '~ 
				 (cons '++
				       (map (lambda (x) (list '~ x))
					    (cdr x))))))
	  ((cond? x) (let ((p (second x))
			   (q (third x)))
		       (pl->eg (list '~ 
				     (list '++ p 
					   (list '~ q))))))
	  ((bicond? x) (let ((p (second x))
			     (q (third x)))
			 (pl->eg (list '++ 
				       (list '-> p q)
				       (list '-> q p)))))))
  
  
  ;-------------egdp-sat? algorithm-------------------
  
  (define (egdp-remove-tauts lst)
    (if (literal? lst) lst
	(delete-matching-items (map egdp-remove-tauts lst) 
	  (lambda (x) (and (list? x) (member '() x))))))


  (define (egdp-get-literal x)
    (if (null? x) '()
	(let ((head (car x)) (tail (cdr x)))
	  (if (literal? head)
	      head
	      (or (egdp-get-literal head) (egdp-get-literal tail))))))
  
  (define (egdp-remove-literal l g)
    (if (or  (not (list? g)) (null? g) ) g
	(let ((head (car g)) (tail (cdr g)))
	  (cond ((equal? head l) (egdp-remove-literal l tail))
		((equal? (list head) l) (cons '() (egdp-remove-literal l tail)))
		(else (cons (egdp-remove-literal l head)
			    (egdp-remove-literal l tail)))))))
  (define (egdp-sat? x)
    (set! egdp-sat?-count (+ egdp-sat?-count 1))
    (let ((x-prime (egdp-remove-tauts x)))
      (cond ((equal? x-prime '()) #t)
	    ((member '() x-prime ) #f)
	    (else   
	     (let ((lit (egdp-get-literal x-prime)))
	       (begin 
		 (if (atomic? lit) 
		     (or (egdp-sat? (egdp-remove-literal lit x-prime))
			 (egdp-sat? (egdp-remove-literal (list lit) x-prime)))
		     (or (egdp-sat? (egdp-remove-literal lit x-prime))
			 (egdp-sat? (egdp-remove-literal (car lit) x-prime))))))))))
  
  ;--------

  (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 (pl->eg KB))
      (set! pl->eg-time (+ pl->eg-time (timer-value)))
      
      (start-timer)
      (set! answer (not (egdp-sat? KB)))
      (set! egdp-sat?-time (+ egdp-sat?-time (timer-value)))))
  
  (define end-time (process-time-clock))
  (list (list answer
	      (- end-time begin-time)
	      run-count)
	(list pl->eg-time
	      pl->eg-count)
	(list egdp-sat?-time
	      egdp-sat?-count)))