(clear-all)
(setf tpl:*print-length* nil)

(undefine-module graphical)

(defparameter *graphical-busy* nil)
(defvar *graphical-error*)
(setf *graphical-error* nil)

;; CREATE-CHUNK
;; Creates a new chunk in the specified buffer, according to the specified
;; description. It also set the BUSY parameter to nil
;;

(defparameter *graph-time* 1)
(defparameter *retrieval-time* 1.0)
(defparameter *imaginal-time* .2)
(defparameter *wait* nil)

(defun create-chunk (buffer-name chunk-description busy)
    ;  (format t "~%Called CREATE-CHUNK in buffer ~A and with description = ~A~%" buffer-name chunk-description)
    (set busy nil)
    (create-new-buffer-chunk buffer-name chunk-description))


(defun request-graphical-chunk (instance buffer-name chunk-spec)
     (declare (ignore instance))
     (let* ((specs      (chunk-spec-to-chunk-def chunk-spec))
            (type (get-value specs 'type))
            (cat (get-value specs 'isa))
            (mode (get-value specs 'mode))
            (relation (get-value specs 'relation))
            (arg1 (get-value specs 'arg1))
            (arg2 (get-value specs 'arg2))
            (arg3 (get-value specs 'arg3))
            (description (if (eq cat 'look)
                           (list 'isa 'statement 'mode mode 'arg1 arg1 'relation relation 'arg2 arg2)
                           (append (list 'isa type 'mode mode) (encode mode arg1 arg2 arg3))))
            (delay  (if (eq mode 'to-prove) *graph-time* (* .2 *graph-time*))))         ;; End of let*
       (setf *graphical-busy*  t)
       (setf *graphical-error* nil)
       (cond (description (schedule-event-relative delay
                                                   'create-chunk
                                                   :params (list buffer-name description '*graphical-busy*)))
             (t (schedule-event-relative delay
                                         'create-graphical-error
                                         :module buffer-name
                                         :priority -100)))))

(defun encode (mode arg1 arg2 arg3)
    (case mode
      (to-prove (list 'arg1 (second *goal*) 'relation (first *goal*) 'arg2 (third *goal*)))
      (corresponding-parts (corresponding-parts arg1 arg2))
      (check (cond ((find-givens arg1 arg2) (list 'arg1 arg1 'relation 'given-congruent 'arg2 arg2))
                   ((eq (car arg1) 'angle)
                    (cond ((vertical-angles (cdr arg1) (cdr arg2))
                           (list 'arg1 arg1 'relation 'vertical-angles 'arg2 arg2))
                          ((and (check-right arg1) (check-right arg2))
                           (list 'arg1 arg1 'relation 'right-angles 'arg2 arg2))))
                   ((eq (car arg1) 'segment)
                    (if (g-eq arg1 arg2)
                      (list 'arg1 arg1 'relation 'reflexive 'arg2 arg2)))))
      (label-parts (list 'value (label_yk (chunk-slot-value-fct arg1 'arg1)
                                       (chunk-slot-value-fct arg2 'arg1)
                                       (chunk-slot-value-fct arg3 'arg1))))
      (alt-angles (if (alt-angles arg1 arg2)
                    (list 'arg1 arg1 'relation 'congruent 'arg2 arg2)
                    (list 'arg1 arg1 'relation 'none 'arg2 arg2)))
      (corr-angles (if (corr-angles arg1 arg2)
                    (list 'arg1 arg1 'relation 'congruent 'arg2 arg2)
                    (list 'arg1 arg1 'relation 'none 'arg2 arg2)))
      (find-third-part (find-third-part arg1 arg2))
      (isoceles (isoceles arg1 arg2))
      (find-part (find-part))
      (vertical-angles (if (vertical-angles (cdr arg1) (cdr arg2))
                    (list 'arg1 arg1 'relation 'congruent 'arg2 arg2)
                    (list 'arg1 arg1 'relation 'none 'arg2 arg2)))
      (t '(relation none))))

(defun iso-angle (pair1 pair2)
    (let ((inter (car (intersection pair1 pair2))))
      (append (list 'angle (If (eq inter (first pair1)) (second pair1) 
(first pair1)))
              (if (eq inter (first pair2)) (reverse pair2) pair2))))

(defun isoceles (a b)
    (case (car a)
      (segment (if (and (intersection (cdr a) (cdr b))
                        (not (apply 'linep (union (cdr a) (cdr b))))
                     (find-givens (iso-angle (cdr a) (cdr b))
                                  (iso-angle (cdr b) (cdr a))))
                 (list 'arg1 a 'relation 'congruent 'arg2 b)
                 (list 'arg1 a 'relation 'none 'arg2 b)))
      (angle (let ((apex (intersection (cdr (remove (third a) a )) 
(cdr (remove (third b) b)))))
               (if (and (find-givens (list 'segment (car apex) (third a))
                            (list 'segment (car apex) (third b))) 
(linep (third a) (third b) (third a)))
               (list 'arg1 a 'relation 'congruent 'arg2 b)
               (list 'arg1 a 'relation 'none 'arg2 b))))))

(defun alt-angles (ang1 ang2)
   (if (assoc 'parallel *givens*)
    (let* ((parallel (assoc 'parallel *givens*))
          (result (or (transversal-configuration (cdr ang1) (cdr ang2)
                                                 (cdr (second parallel)) (cdr (third parallel)))
                      (transversal-configuration (cdr ang1) (cdr ang2)
                                                 (cdr(third parallel)) 
(cdr (second parallel)))))
          (v1 (third ang1))
          (v2 (third ang2))
          (pt1 (first result)) (pl1 (second result)) (pt2 (third result)) (pl2 (fourth result)))
      (and pt1 pl1 pt2 pl2 (linep v1 v2 v2)
           (not (equal (direction v1 v2) (direction pt1 pt2)))
           (not (equal (direction v1 pl1) (direction v2 pl2)))))))

(defun direction (v1 v2)
    (do ((temp *lines* (cdr temp)))
        ((null temp) nil)
      (if (and (member v1 (car temp)) (member v2 (car temp)))
        (return (if (member v2 (member v1 (car temp))) 'r 'l)))))

(defun transversal-configuration (ang1-points ang2-points line1-points line2-points)
   (let* ((v1 (second ang1-points))(v2 (second ang2-points))
          (pt1 (cond ((linep v1 v2 (first ang1-points)) (first ang1-points))
                     ((linep v1 v2 (third ang1-points)) (third ang1-points))))
          (pt2 (cond ((linep v1 v2 (first ang2-points)) (first ang2-points))
                     ((linep  v1 v2 (third ang2-points)) (third ang2-points))))
          (pl1 (cond ((apply 'linep (cons (first ang1-points) line1-points)) (first ang1-points))
                     ((apply 'linep (cons (third ang1-points) line1-points)) (third ang1-points))))
          (pl2 (cond ((apply 'linep (cons (first ang2-points) line2-points)) (first ang2-points))
                     ((apply 'linep (cons (third ang2-points) line2-points)) (third ang2-points)))))
     (list pt1 pl1 pt2 pl2)))

(defun corr-angles (ang1 ang2)
   (if (assoc 'parallel *givens*)
    (let* ((parallel (assoc 'parallel *givens*))
           (result (or (transversal-configuration (cdr ang1) (cdr ang2)
                                                 (cdr (second parallel)) (cdr (third parallel)))
                      (transversal-configuration (cdr ang1) (cdr ang2)
                                                 (cdr(third parallel)) 
(cdr (second parallel)))))
          (v1 (third ang1))
          (v2 (third ang2))
          (pt1 (first result)) (pl1 (second result)) (pt2 (third result)) (pl2 (fourth result)))
      (and pt1 pl1 pt2 pl2 (linep v1 v2 v2)
           (equal (direction v1 v2) (direction pt1 pt2))
           (equal (direction v1 pl1) (direction v2 pl2))))))

(defun find-third-part (a b)
    (let* ((a1 (chunk-slot-value-fct a 'arg1))
           (a2 (chunk-slot-value-fct a 'arg2))
           (b1 (chunk-slot-value-fct b 'arg1))
           (b2 (chunk-slot-value-fct b 'arg2)))
      (case (car a1)
        (segment (case (car b1)
                   (angle  (cond ((or (eq (third b1) (third a1)) (eq (second b1) (third a1)))
                                 (let ((c1 (list 'angle (third a1) (difference (cdr b1) (cdr a1)) (second a1)))
                                       (c2 (list 'angle (third a2) (difference (cdr b2) (cdr a2)) (second a2))))
                                   (list 'arg1 c1 'relation 'angle-congruent 'arg2 c2)))
                                 ((eq (second a1) (third b1))
                                 (let ((c1 (list 'angle (third b1) (fourth b1) (second b1)))
                                       (c2 (list 'angle (third b2) (fourth b2) (second b2))))
                                   (list 'arg1 c1 'relation 'angle-congruent 'arg2 c2))))))))))

(defun difference (large small) (car (set-difference large small)))

(defun label_yk (part1 part2 part3)
    (let ((set (sort (list part1 part2 part3) 'seg-ang :key 'car)))
      (cond ((eq (car (third set)) 'segment) 'sss)
            ((eq (car (second set)) 'segment)
             (if (check-right (third set))
                 (if (check-hl (first set) (second set) (third set)) 'hl 'right)
                 (if (check-sas (first set) (third set) (second set)) 'sas)))
            ((eq (car (first set)) 'segment)
             (if (check-asa (second set) (first set) (third set)) 'asa 'aas))
            (t nil))))

(defun check-right (angle)
    (do ((temp *givens* (cdr temp)))
        ((null temp) nil)
      (if (and (eq (first (car temp)) 'right-angle) (g-eq angle 
(second (car temp)))) (return t))))

(defun check-hl (s1 s2 r)
   (let ((v (third r)))
     (or (and (intersection s1 r)
              (not (member v s2)))
         (and (intersection s2 r)
              (not (member v s1))))))

(defun check-asa (a1 s a2)
    (let ((p1 (second s)) (p2 (third s))
          (v1 (third a1)) (v2 (third a2)))
      (or (and (eq p1 v1) (eq p2 v2)) (and (eq p1 v2) (eq p2 v1)))))

(defun check-sas (s1 a s2)
    (let ((v1 (third a)))
      (and (member v1 s1) (member v1 s2))))

(defun seg-ang (x y) (and (eq x 'segment) (eq y 'angle)))

(defun vertical-angles (points1 points2)
    (let ((point11 (first points1))
          (v1 (second points1))
          (point13 (third points1))
          (point21 (first points2))
          (v2 (second points2))
          (point23 (third points2)))
      (and (eq v1 v2)
           (eq (length (intersection points1 points2)) 1)
           (or (and (linep point11 v1 point21)
                    (linep point13 v2 point23))
               (and (linep point11 v1 point23)
                    (linep point21 v2 point13))))))

(defun linep (p1 p2 p3)
    (do ((temp *lines* (cdr temp)))
        ((null temp) nil)
      (if (and (member p1 (car temp)) (member p2 (car temp)) (member p3 (car temp))) (return t))))

(defun find-givens (arg1 arg2)
    (do ((temp *givens* (cdr temp)))
        ((null temp) nil)
      (if (and (eq (caar temp) 'congruent) (member arg1 (cdar temp) :test 'g-eq)
               (member arg2 (cdar temp) :test 'g-eq)) (return t))))

(defun g-eq (a b)
    (case (car a)
      (segment (and (eq (car b) 'segment) (member (second a) b) (member (third a) b)))
      (angle (and (eq (car b) 'angle) (setf a (rename-angle a)) (setf b (rename-angle b))
                  (eq (third a) (third b)) (member (second a) b) (member (fourth a) b)))))

(defun find-line (a b)
    (do ((temp *lines* (cdr temp)))
        ((null temp) nil)
      (if (and (member a (car temp)) (member b (car temp))) (return (car temp)))))

(defun rename-angle (angle)
    (let* ((p1 (second angle))
          (p2 (third angle))
          (p3 (fourth angle))
          (line1 (find-line p1 p2))
          (line2 (find-line p2 p3))
          (end1 (if (member p1 (member p2 line1)) (car (last line1)) (car line1)))
          (end2 (if (member p3 (member p2 line2)) (car (last line2)) (car line2))))
      (list 'angle end1 p2 end2)))

(defun find-part ()
    (let ((part (car *parts-list*)))
      (pop *parts-list*)
      (if part (list 'arg1 (first part) 'relation 'congruent 'arg2 (second part))
               '(relation done))))

(defvar *parts-list*)

(defun corresponding-parts (arg1 arg2)
    (let* ((result (if (eq (car arg1) 'segment) (car (last (find-parts (cdr arg1) (cdr arg2))))
                       (list (reverse (cdr arg1)) (reverse (cdr arg2)))))
           (point1 (first (first result)))
           (point2 (first (second result))))
      (setf *parts-list*
        (list (list (list 'segment (second arg1) (third arg1)) (list 'segment (second arg2) (third arg2)))
                   (list (list 'segment point1 (second arg1)) (list 'segment point2 (second arg2)))
                   (list (list 'segment point1 (third arg1)) (list 'segment point2 (third arg2)))
                   (list (cons 'angle (first result)) (cons 'angle (second result)))
                   (list (cons 'angle (forward (first result))) (cons 'angle (forward (second result))))
                   (list (cons 'angle (backward (first result))) (cons 'angle (backward (second result))))))
;    (print result)
     (if (= (length (intersection (first result) (second result))) 3)
       (list 'relation nil)
      (if (eq (car arg1) 'triangle) (list 'arg1 arg1 'relation 'congruent 'arg2 arg2)
        (list 'arg1 (cons 'triangle (first result)) 'relation 'congruent
            'arg2 (cons 'triangle (second result)))))))

(defun forward (lis) (append (cdr lis) (list (first lis))))
(defun backward (lis) (append (last lis) (reverse (cdr (reverse lis)))))

;; CREATE-GRAPHICAL-ERROR
;; When an error occurs processing a request, the parameters are updated
;; so that module results Free, but responds positively to Error queries
;;
(defun create-graphical-error ()
    (setf *graphical-busy* nil)
    (setf *graphical-error* t))


;; The QUERY Function
;; The module supports four (4) states: Busy if *graphical-busy* is non-nil,
;; Free otherwise, Error-Free if *graphical-error* is not-nil, and Error
;; otherwise.
;;
(defun graphical-query (instance buffer-name slot value)
    (declare (ignore buffer-name instance))
    (case slot
      (state
       (case value
         (busy       *graphical-busy*)
         (free       (not *graphical-busy*))
         (error-free (not  *graphical-error*))
         (error      *graphical-error*)
         (t (print-warning "Unknown state query ~S to goal module" value)
            nil)))))

;; THE RESET function
;;
(defun reset-graphical-2 (instance)
    (declare (ignore instance))
    (specify-compilation-buffer-type graphical perceptual))


;;; GRAPHICAL
;;; The graphical module is an input module
;;;
(define-module-fct 'graphical
    '(graphical)
    nil
    :version "0.2a"
    :documentation "A module for retrieving visual information about the screen"
    :query 'graphical-query
    :reset '(nil reset-graphical-2)
    :request 'request-graphical-chunk)

(defun get-value (lis elem)
    (second (member elem lis)))

(defvar *lines*)
(defvar *goal*)
(defvar *givens*)

(defparameter *allproblems*
    '(problem1-1 problem1-3 problem1-dnf problem2-1 problem2-3 problem2-dnf
                 problemAa1 problemAa3 problemAadnf problemB1 problemB3 problemBdnf
                 problemC1 problemC3 problemCdnf problemD1 problemD3 problemDdnf
                 problemE1 problemE3 problemEdnf problemF1 problemF3 problemFdnf
                 problemG1 problemG3 problemGdnf problemH1 problemH3 problemHdnf
                 problemI1 problemI3 problemIdnf problemJ1 problemJ3 problemJdnf
                 problemK1 problemK3 problemKdnf problemLl1 problemLl3 problemLldnf
                 problemM1 problemM3 problemMdnf problemN1 problemN3 problemNdnf
                 problemO1 problemO3 problemOdnf problemP1 problemP3 problemPdnf
                 problemQ1 problemQ3 problemQdnf problemR1 problemR3 problemRdnf
                 problemS1 problemS3 problemSdnf problemT1 problemT3 problemTdnf
                 problemU1 problemU3 problemUdnf problemV1 problemV3 problemVdnf
                 problemW1 problemW3 problemWdnf problemX1 problemX3 problemXdnf
                 problemY1 problemY3 problemYdnf problemZ1 problemZ3 problemZdnf))

(defparameter *train*
    '(problem1-1 problem1-3 problem1-dnf problemF1 problemF3 problemFdnf
                 problemG1 problemG3 problemGdnf problemI1 problemI3 problemIdnf
                 problemQ1 problemQ3 problemQdnf problemR1 problemR3 problemRdnf
                 problemW1 problemW3 problemWdnf problemZ1 problemZ3 
problemZdnf))

(defparameter *test*
    '(problem2-1 problem2-3 problem2-dnf problemAa1 problemAa3 problemAadnf
                 problemB1 problemB3 problemBdnf problemC1 problemC3 problemCdnf
                 problemD1 problemD3 problemDdnf problemE1 problemE3 problemEdnf
                 problemH1 problemH3 problemHdnf problemJ1 problemJ3 problemJdnf
                 problemK1 problemK3 problemKdnf problemLl1 problemLl3 problemLldnf
                 problemM1 problemM3 problemMdnf problemN1 problemN3 problemNdnf
                 problemO1 problemO3 problemOdnf problemP1 problemP3 problemPdnf
                 problemS1 problemS3 problemSdnf problemT1 problemT3 problemTdnf
                 problemU1 problemU3 problemUdnf problemV1 problemV3 problemVdnf
                 problemX1 problemX3 problemXdnf problemY1 problemY3 problemYdnf))

(defparameter *1*
    '(problem1-1 problem1-3 problem1-dnf))

(defparameter *2*
    '(problem2-1 problem2-3 problem2-dnf))

(defparameter *a*
    '(problemAa1 problemAa3 problemAadnf))

(defparameter *b*
    '(problemB1 problemB3 problemBdnf))

(defparameter *c*
    '(problemC1 problemC3 problemCdnf))

(defparameter *d*
    '(problemD1 problemD3 problemDdnf))

(defparameter *e*
    '(problemE1 problemE3 problemEdnf))

(defparameter *f*
    '(problemF1 problemF3 problemFdnf))

(defparameter *g*
    '(problemG1 problemG3 problemGdnf))

(defparameter *h*
    '(problemH1 problemH3 problemHdnf))

(defparameter *i*
    '(problemI1 problemI3 problemIdnf))

(defparameter *j*
    '(problemJ1 problemJ3 problemJdnf))

(defparameter *k*
    '(problemK1 problemK3 problemKdnf))

(defparameter *l*
    '(problemLl1 problemLl3 problemLldnf))

(defparameter *m*
    '(problemM1 problemM3 problemMdnf))

(defparameter *n*
    '(problemN1 problemN3 problemNdnf))

(defparameter *o*
    '(problemO1 problemO3 problemOdnf))

(defparameter *p*
    '(problemP1 problemP3 problemPdnf))

(defparameter *q*
    '(problemQ1 problemQ3 problemQdnf))

(defparameter *r*
    '(problemR1 problemR3 problemRdnf))

(defparameter *s*
    '(problemS1 problemS3 problemSdnf))

(defparameter *t*
    '(problemT1 problemT3 problemTdnf))

(defparameter *u*
    '(problemU1 problemU3 problemUdnf))

(defparameter *v*
    '(problemV1 problemV3 problemVdnf))

(defparameter *w*
    '(problemW1 problemW3 problemWdnf))

(defparameter *x*
    '(problemX1 problemX3 problemXdnf))

(defparameter *y*
    '(problemY1 problemY3 problemYdnf))

(defparameter *z*
    '(problemZ1 problemZ3 problemZdnf))

(defun problem1-1 ()
    (setf *lines* '((G H B) (G F D C) (E F H A) (E D B) (C B) (A B))
          *goal* '(triangle-congruent (triangle A B E) (triangle C B G))
          *givens* '((congruent (segment A B) (segment C B))
                    (congruent (angle B A E) (angle B C G))
                    (congruent (angle A E B) (angle C G B)))))

(defun problem1-3 ()
    (setf *lines* '((G H B) (G F D C) (E F H A) (E D B) (C B) (A B))
          *goal* '(segment-congruent (segment H F) (segment D F))
          *givens* '((congruent (segment H G) (segment D E))
                    (congruent (angle C G B) (angle A E B))
                    (congruent (angle F H B) (segment F D B)))))

(defun problem1-dnf ()
    (setf *lines* '((G H B) (G F D C) (E F H A) (E D B) (C B) (A B))
          *goal* '(angle-congruent (angle C G B) (angle A E B))
          *givens* '((congruent (segment A H) (segment C D))
                    (congruent (angle A B H) (angle C B D))
                     (congruent (angle A F C) (angle G F E)))))

(defun problem2-1 ()
    (setf *lines* '((A B C) (C E) (A D) (D E) (A X Z E) (C Y Z D) (B X D) (B Y E))
          *goal* '(angle-congruent (angle A X B) (angle D X Z))
          *givens* '((congruent (segment X Z) (segment Y Z))
                     (congruent (angle Z D) (angle Z E)))))

(defun problem2-3 ()
    (setf *lines* '((A B C) (C E) (A D) (D E) (A X Z E) (C Y Z D) (B X D) (B Y E))
          *goal* '(triangle-congruent (triangle A D B) (triangle C E B))
          *givens* '((congruent (segment A B) (segment C B))
                     (congruent (angle A D) (angle C E)))))

(defun problem2-dnf ()
    (setf *lines* '((A B C) (C E) (A D) (D E) (A X Z E) (C Y Z D) (B X D) (B Y E))
          *goal* '(segment-congruent (segment B D) (segment B E))
          *givens* '((congruent (segment A B) (segment D E))
                    (congruent (angle A D) (angle C E)))))

(defun problemAa1 ()
    (setf *lines* '((P Q R) (Z Y R) (Z X P) (Q Y) (Q X) (Q Z))
          *goal* '(segment-congruent (segment P X) (segment Q X))
          *givens* '((congruent (angle X P Q) (angle X Q P))
                    (congruent (angle Y Q R) (angle Y R Q)))))

(defun problemAa3 ()
    (setf *lines* '((P Q R) (Z Y R) (Z X P) (Q Y) (Q X) (Q Z))
          *goal* '(segment-congruent (segment P Q) (segment R Q))
          *givens* '((congruent (angle Q Z P) (angle Q Z R))
                    (congruent (angle Q P Z) (angle Q R Z)))))

(defun problemAadnf ()
    (setf *lines* '((P Q R) (Z Y R) (Z X P) (Q Y) (Q X) (Q Z))
          *goal* '(segment-congruent (segment P X) (segment R Y))
          *givens* '((congruent (angle X Q Z) (angle Y Q Z))
                    (congruent (angle Q Z X) (angle Q Z Y)))))

(defun problemB1 ()
    (setf *lines* '((A B C) (A F E) (B O E) (F O C) (C D E))
          *goal* '(triangle-congruent (triangle C O D) (triangle E O D))
          *givens* '((congruent (segment O C) (segment O E))
                     (congruent (segment C D) (segment E D))
                     (right-angle (angle O D C))
                     (right-angle (angle O D E)))))

(defun problemB3 ()
    (setf *lines* '((A B C) (A F E) (B O E) (F O C) (C D E))
          *goal* '(segment-congruent (segment F C) (segment B E))
          *givens* '((congruent (segment A B) (segment A F))
                     (congruent (segment O C) (segment O E))
                     (congruent (angle B C O) (angle F E O)))))

(defun problemBdnf ()
    (setf *lines* '((A B C) (A F E) (B O E) (F O C) (C D E))
          *goal* '(angle-congruent (angle O D C) (angle O D E))
          *givens* '((congruent (segment A B) (segment A F))
                     (congruent (segment B C) (segment F E))
                     (congruent (angle A B O) (angle A F O)))))

(defun problemC1 ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C))
          *goal* '(angle-congruent (angle B O E) (angle C O D))
          *givens* '((congruent (segment A B) (segment A E))
                     (congruent (angle A B O) (angle A E O)))))

(defun problemC3 ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C))
          *goal* '(segment-congruent (segment B C) (segment E D))
          *givens* '((congruent (segment B O) (segment E O))
                     (congruent (angle B C O) (angle E D O)))))

(defun problemCdnf ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C))
          *goal* '(angle-congruent (angle A B O) (angle A E O))
          *givens* '((congruent (segment O C) (segment O D))
                     (congruent (angle O C D) (angle O D C)))))

(defun problemD1 ()
    (setf *lines* '((A B) (A E) (B C D E) (A C) (A D))
          *goal* '(segment-congruent (segment A B) (segment A E))
          *givens* '((congruent (segment B C) (segment D E))
                    (congruent (angle A B C) (angle A E D))
                     (congruent (angle A C D) (angle A D C)))))

(defun problemD3 ()
    (setf *lines* '((A B) (A E) (B C D E) (A C) (A D))
          *goal* '(angle-congruent (angle A C D) (segment A D C))
          *givens* '((congruent (angle A B C) (angle A E D))
                    (congruent (angle B A C) (angle E A D))
                    (congruent (segment A B) (segment A E)))))

(defun problemDdnf ()
    (setf *lines* '((A B) (A E) (B C D E) (A C) (A D))
          *goal* '(segment-congruent (segment A B) (segment A E))
          *givens* '((congruent (segment A B) (segment A D))
                    (congruent (angle A B C) (angle A D C))
                     (congruent (angle B A C) (angle E A D)))))

(defun problemE1 ()
    (setf *lines* '((A B) (A C) (A D) (B D C))
          *goal* '(segment-congruent (segment A B) (segment A C))
          *givens* '((congruent (angle A B D) (angle A C D))
                     (right-angle (angle A D B))
                     (right-angle (angle A D C)))))

(defun problemE3 ()
    (setf *lines* '((A B) (A C) (A D) (B D C))
          *goal* '(angle-congruent (angle A B D) (angle A C D))
          *givens* '((congruent (angle B A D) (angle C A D))
                     (right-angle (angle A D B))
                     (right-angle (angle A D C)))))

(defun problemEdnf ()
    (setf *lines* '((A B) (A C) (A D) (B D C))
          *goal* '(segment-congruent (segment A B) (segment B C))
          *givens* '((congruent (angle A B D) (angle A C D))
                     (congruent (segment B D) (segment C D)))))

(defun problemF1 ()
    (setf *lines* '((A B C D) (A G F) (D E F) (B G) (C E))
          *goal* '(triangle-congruent (triangle A B G) (triangle D C E))
          *givens* '((congruent (angle B A G) (angle C D E))
                     (congruent (angle A B G) (angle D C E))
                     (congruent (segment B G) (segment C E)))))

(defun problemF3 ()
    (setf *lines* '((A B C D) (A G F) (D E F) (B G) (C E))
          *goal* '(segment-congruent (segment A F) (segment D F))
          *givens* '((congruent (angle A G B) (angle D E C))
                     (congruent (angle A B G) (angle D C E))
                     (congruent (segment A B) (segment C D)))))

(defun problemFdnf ()
    (setf *lines* '((A B C D) (A G F) (D E F) (B G) (C E))
          *goal* '(angle-congruent (angle G B C) (angle C E F))
          *givens* '((congruent (angle A G B) (angle D E C))
                     (congruent (angle B A G) (angle C D E))
                     (congruent (segment G F) (segment E F)))))

(defun problemG1 ()
    (setf *lines* '((A B C) (A F E) (C D E) (B F) (B D) (F D))
          *goal* '(angle-congruent (angle B C D) (angle F D E))
          *givens* '((congruent (angle C B D) (angle B C D))
                     (parallel (segment A B) (segment F D)))))

(defun problemG3 ()
    (setf *lines* '((A B C) (A F E) (C D E) (B F) (B D) (F D))
          *goal* '(segment-congruent (segment B F) (segment B D))
          *givens* '((congruent (angle A B F) (angle C B D))
                     (parallel (segment A B) (segment F D)))))

(defun problemGdnf ()
    (setf *lines* '((A B C) (A F E) (C D E) (B F) (B D) (F D))
          *goal* '(angle-congruent (angle A B F) (angle C B D))
          *givens* '((congruent (angle A F B) (angle C D B))
                     (parallel (segment A B) (segment F D)))))

(defun problemH1 ()
    (setf *lines* '((A B) (B C) (A C) (A O) (B O) (C O))
          *goal* '(segment-congruent (segment O B) (segment O C))
          *givens* '((congruent (angle B A O) (angle C A O))
                     (congruent (angle O B C) (angle O C B)))))

(defun problemH3 ()
    (setf *lines* '((A B) (B C) (A C) (A O) (B O) (C O))
          *goal* '(triangle-congruent (triangle A B O) (triangle A C O))
          *givens* '((congruent (angle A O B) (angle A O C))
                     (congruent (angle O B C) (angle O C B)))))

(defun problemHdnf ()
    (setf *lines* '((A B) (B C) (A C) (A O) (B O) (C O))
          *goal* '(angle-congruent (angle O A C) (angle O C A))
          *givens* '((congruent (angle A O B) (angle A O C))
                     (congruent (angle A B O) (angle A C O)))))

(defun problemI1 ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C) (A O))
          *goal* '(angle-congruent (angle O C D) (angle O D C))
          *givens* '((congruent (segment B C) (segment E D))
                     (congruent (segment O C) (segment O D)))))

(defun problemI3 ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C) (A O))
          *goal* '(angle-congruent (angle A B O) (angle A E O))
          *givens* '((congruent (segment A B) (segment A E))
                     (congruent (segment B O) (segment E O)))))

(defun problemIdnf ()
    (setf *lines* '((A B C) (A E D) (C D) (B O D) (E O C) (A O))
          *goal* '(segment-congruent (segment A B) (segment A E))
          *givens* '((congruent (segment B O) (segment E O))
                     (congruent (segment B C) (segment E D)))))

(defun problemJ1 ()
    (setf *lines* '((A B C) (A E D) (C O E) (D O B))
          *goal* '(angle-congruent (angle C O B) (angle D O E))
          *givens* '((congruent (angle B C O) (angle E D O))
                     (segment (segment O B) (segment O E)))))

(defun problemJ3 ()
    (setf *lines* '((A B C) (A E D) (C O E) (D O B))
          *goal* '(segment-congruent (segment C E) (segment D B))
          *givens* '((congruent (angle O B A) (angle O E A))
                     (congruent (segment B A) (segment E A)))))

(defun problemJdnf ()
    (setf *lines* '((A B C) (A E D) (C O E) (D O B))
          *goal* '(segment-congruent (segment C A) (segment D B))
          *givens* '((congruent (angle C B O) (angle D E O))
                     (segment (segment C O) (segment D O)))))

(defun problemK1 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A C))
          *goal* '(segment-congruent (segment A C) (segment C D))
          *givens* '((congruent (angle C A B) (angle C B A))
                     (congruent (angle C A D) (angle C D A)))))

(defun problemK3 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A C))
          *goal* '(segment-congruent (segment A B) (segment A D))
          *givens* '((congruent (angle B A C) (angle D A C))
                     (congruent (angle B C A) (angle D C A)))))

(defun problemKdnf ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A C))
          *goal* '(segment-congruent (segment A C) (segment B C))
          *givens* '((congruent (angle B A C) (angle D A C))
                     (congruent (angle A B C) (angle A D C)))))

(defun problemLl1 ()
    (setf *lines* '((X Y) (P X Q) (R Y Q) (R O X) (P O Y))
          *goal* '(segment-congruent (segment X Q) (segment Y Q))
          *givens* '((congruent (segment P X) (segment R Y))
                    (congruent (angle Q X Y) (angle Q Y X)))))

(defun problemLl3 ()
    (setf *lines* '((X Y) (P X Q) (R Y Q) (R O X) (P O Y))
          *goal* '(segment-congruent (segment P X) (segment R Y))
          *givens* '((congruent (segment P O) (segment R O))
                    (congruent (angle O R Y) (angle O P X)))))

(defun problemLldnf ()
    (setf *lines* '((X Y) (P X Q) (R Y Q) (R O X) (P O Y))
          *goal* '(triangle-congruent (triangle X P O) (segment Y R O))
          *givens* '((congruent (segment X Q) (segment Y Q))
                     (congruent (angle P X O) (angle R Y O)))))

(defun problemM1 ()
    (setf *lines* '((A B C D) (W X Y Z) (A W) (A X) (B X) (C Y) (C Z) (D Z))
          *goal* '(angle-congruent (angle B C Y) (angle C Y Z))
          *givens* '((congruent (segment B X) (segment C Y))
                     (parallel (segment A B) (segment X Y))
                     (congruent (angle A W X) (congruent Z D C)))))

(defun problemM3 ()
    (setf *lines* '((A B C D) (W X Y Z) (A W) (A X) (B X) (C Y) (C Z) (D Z))
          *goal* '(segment-congruent (segment A B) (segment C D))
          *givens* '((congruent (segment A X) (segment C Z))
                     (parallel (segment B X) (segment D Z))
                     (right-angle (angle B A X))
                     (right-angle (angle D C Z)))))

(defun problemMdnf ()
    (setf *lines* '((A B C D) (W X Y Z) (A W) (A X) (B X) (C Y) (C Z) (D Z))
          *goal* '(triangle-congruent (triangle A W Z) (triangle Z D C))
          *givens* '((congruent (segment A B) (segment Y Z))
                     (parallel (segment B C) (segment X Y))
                     (right-angle (angle A X W))
                     (right-angle (angle Z C D)))))

(defun problemN1 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(angle-congruent (angle A B O) (angle C D O))
          *givens* '((congruent (segment A B) (segment C D))
                     (parallel (segment A B) (segment C D)))))

(defun problemN3 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(triangle-congruent (triangle A D O) (triangle C B O))
          *givens* '((congruent (segment A O) (segment C O))
                     (parallel (segment A D) (segment B C)))))

(defun problemNdnf ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(angle-congruent (angle D A O) (angle C B O))
          *givens* '((congruent (segment A B) (segment C D))
                    (parallel (segment A D) (segment B C)))))

(defun problemO1 ()
    (setf *lines* '((B E D F) (A E) (C F) (A B) (C D) (B C) (D A))
          *goal* '(triangle-congruent (triangle A D E) (triangle C B F))
          *givens* '((congruent (segment A D) (segment C B))
                    (congruent (segment D E) (segment B F))
                    (congruent (angle A E D) (angle C F B))
                    (right-angle (angle A E D))
                    (right-angle (angle C F B)))))

(defun problemO3 ()
    (setf *lines* '((B E D F) (A E) (C F) (A B) (C D) (B C) (D A))
          *goal* '(segment-congruent (segment B E) (segment D F))
          *givens* '((congruent (segment A E) (segment C F))
                    (congruent (angle A E B) (angle C F D))
                    (parallel (segment A B) (segment C D)))))

(defun problemOdnf ()
    (setf *lines* '((B E D F) (A E) (C F) (A B) (C D) (B C) (D A))
          *goal* '(angle-congruent (angle D A E) (angle B C F))
          *givens* '((congruent (segment B F) (segment D E))
                    (congruent (angle A D E) (angle C B F))
                    (congruent (segment A B) (segment C D)))))

(defun problemP1 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(angle-congruent (angle A O D) (angle B O C))
          *givens* '((congruent (segment A D) (segment B C))
                     (congruent (segment O D) (segment O C)))))

(defun problemP3 ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(angle-congruent (angle D A O) (angle C B O))
          *givens* '((congruent (segment A O) (segment B O))
                     (congruent (segment O D) (segment O C)))))

(defun problemPdnf ()
    (setf *lines* '((A B) (B C) (C D) (A D) (A O C) (B O D))
          *goal* '(angle-congruent (angle A D O) (angle B C O))
          *givens* '((congruent (segment A O) (segment B O))
                     (congruent (segment A D) (segment B C)))))

(defun problemQ1 ()
    (setf *lines* '((A B) (A W) (B Z) (A O Y) (B O X) (W X Y Z))
          *goal* '(angle-congruent (angle O X Y) (angle O Y X))
         *givens* '((congruent (segment A O) (segment B O))
                     (congruent (segment O X) (segment O Y)))))

(defun problemQ3 ()
    (setf *lines* '((A B) (A W) (B Z) (A O Y) (B O X) (W X Y Z))
          *goal* '(triangle-congruent (triangle A B O) (triangle Y X O))
          *givens* '((congruent (segment A B) (segment X Y))
                     (parallel (segment A B) (segment X Y)))))

(defun problemQdnf ()
    (setf *lines* '((A B) (A W) (B Z) (A O Y) (B O X) (W X Y Z))
          *goal* '(angle-congruent (angle A W X) (angle B Z Y))
          *givens* '((congruent (segment A W) (segment B Z))
                     (parallel (segment A B) (segment X Y)))))

(defun problemR1 ()
    (setf *lines* '((A W) (A O Y) (B Z) (B O X) (W X Y Z))
          *goal* '(angle-congruent (angle A O B) (angle Y O X))
          *givens* '((congruent (segment A O) (segment B O))
                     (congruent (segment W X) (segment Y Z))
                     (congruent (angle O X Y) (angle O Y X)))))

(defun problemR3 ()
    (setf *lines* '((A W) (A O Y) (B Z) (B O X) (W X Y Z))
          *goal* '(segment-congruent (segment A Y) (segment B X))
          *givens* '((congruent (segment A W) (segment B Z))
                     (congruent (segment O X) (segment O Y))
                     (congruent (angle W A O) (angle Z B O)))))

(defun problemRdnf ()
    (setf *lines* '((A W) (A O Y) (B Z) (B O X) (W X Y Z))
          *goal* '(segment-congruent (segment A W) (segment B Z))
          *givens* '((congruent (segment W X) (segment Y Z))
                     (congruent (segment O X) (segment O Y))
                     (congruent (angle O X Y) (angle O Y X)))))

(defun problemS1 ()
    (setf *lines* '((A B) (A O C) (A D) (B O D) (C D))
          *goal* '(angle-congruent (angle A O B) (angle D O C))
          *givens* '((congruent (segment A B) (segment D C))
                     (congruent (angle O A D) (angle O D A)))))

(defun problemS3 ()
    (setf *lines* '((A B) (A O C) (A D) (B O D) (C D))
          *goal* '(angle-congruent (angle A B O) (angle D C O))
          *givens* '((congruent (segment B O) (segment C O))
                     (congruent (angle B A O) (angle C D O)))))

(defun problemSdnf ()
    (setf *lines* '((A B) (A O C) (A D) (B O D) (C D))
          *goal* '(angle-congruent (angle D A O) (angle A D O))
          *givens* '((congruent (segment A B) (segment D C))
                     (congruent (angle B A O) (angle A B O)))))

(defun problemT1 ()
    (setf *lines* '((A B) (A C) (B D) (C D) (A O D) (O B) (O C))
          *goal* '(triangle-congruent (triangle B O D) (triangle C O D))
          *givens* '((congruent (segment O B) (segment O C))
                     (congruent (angle B A O) (angle C A O))
                     (right-angle (angle O B D))
                     (right-angle (angle O C D)))))

(defun problemT3 ()
    (setf *lines* '((A B) (A C) (B D) (C D) (A O D) (O B) (O C))
          *goal* '(segment-congruent (segment B D) (segment C D))
          *givens* '((congruent (segment A B) (segment A C))
                     (congruent (angle B O D) (angle C O D))
                     (congruent (angle B D O) (angle C D O)))))

(defun problemTdnf ()
    (setf *lines* '((A B) (A C) (B D) (C D) (A O D) (O B) (O C))
          *goal* '(segment-congruent (segment A B) (segment A C))
          *givens* '((congruent (segment A O) (segment O D))
                     (congruent (angle A B O) (angle O B D))
                     (congruent (angle A C O) (angle O C D)))))

(defun problemU1 ()
    (setf *lines* '((A B) (B Z) (Z C) (C W) (W A) (W X Y Z) (A X C) (B Y C))
          *goal* '(angle-congruent (angle A B Y) (angle B Y Z))
          *givens* '((parallel (segment A B) (segment X Y))
                     (congruent (angle A W X) (angle B Z Y)))))

(defun problemU3 ()
    (setf *lines* '((A B) (Z C) (C W) (B Z) (W A) (W X Y Z) (A X C) (B Y C))
          *goal* '(segment-congruent (segment W X) (segment Z Y))
          *givens* '((congruent (segment W C) (segment Z C))
                     (congruent (angle W C X) (angle Z C Y)))))

(defun problemUdnf ()
    (setf *lines* '((A B) (B Z) (Z C) (C W) (W A) (W X Y Z) (A X C) (B Y C))
          *goal* '(triangle-congruent (triangle A W X) (angle B Z Y))
          *givens* '((congruent (segment A X) (segment B Y))
                     (congruent (angle Y X C) (angle X Y C)))))

(defun problemV1 ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B O D) (E O C))
          *goal* '(angle-congruent (angle A B E) (angle A E B))
          *givens* '((congruent (segment A B) (segment A E))
                     (congruent (segment B C) (segment E D))
                     (congruent (angle O C D) (angle O D C)))))

(defun problemV3 ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B O D) (E O C))
          *goal* '(segment-congruent (segment B E) (segment C D))
          *givens* '((congruent (segment B O) (segment C O))
                     (congruent (segment E O) (segment D O))
                     (congruent (angle B A E) (angle C O D)))))

(defun problemVdnf ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B O D) (E O C))
          *goal* '(triangle-congruent (triangle A B E) (triangle O C D))
          *givens* '((congruent (segment A B) (segment O D))
                     (congruent (segment B E) (segment C D))
                     (congruent (angle A E B) (angle O C D)))))

(defun problemW1 ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B D))
          *goal* '(angle-congruent (angle A E B) (angle A B E))
          *givens* '((congruent (segment A E) (segment A B))
                     (congruent (angle E A B) (angle B C D))
                     (congruent (angle B E D) (angle B D E)))))

(defun problemW3 ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B D))
          *goal* '(angle-congruent (angle B E D) (angle B D E))
          *givens* '((congruent (segment A B) (segment B C))
                     (congruent (angle E A B) (angle B C D))
                     (congruent (angle A B E) (angle C B D)))))

(defun problemWdnf ()
    (setf *lines* '((A B) (B C) (C D) (D E) (A E) (B E) (B D))
          *goal* '(angle-congruent (angle A B D) (angle E D B))
          *givens* '((congruent (segment A E) (segment A B))
                     (congruent (angle E A B) (angle B C D))
                     (congruent (angle A E B) (angle A B E)))))

(defun problemX1 ()
    (setf *lines* '((A O D) (B O C) (A B) (C D))
          *goal* '(angle-congruent (angle A O C) (angle B O D))
          *givens* '((congruent (segment B O) (segment C O))
                     (congruent (angle A B O) (angle D C O)))))

(defun problemX3 ()
    (setf *lines* '((A O D) (B O C) (A B) (C D))
          *goal* '(segment-congruent (segment A B) (segment D C))
          *givens* '((congruent (segment A O) (segment D O))
                     (congruent (angle B A O) (angle C D O)))))

(defun problemXdnf ()
    (setf *lines* '((A O D) (B O C) (A B) (C D))
          *goal* '(angle-congruent (angle B A O) (angle C D O))
          *givens* '((congruent (segment A O) (segment C O))
                     (congruent (angle A B O) (angle D C O)))))

(defun problemY1 ()
    (setf *lines* '((A B C) (D E F) (A O D) (C O F) (B O E))
          *goal* '(angle-congruent (angle A O C) (angle D O F))
          *givens* '((congruent (segment B O) (segment E O))
                     (congruent (angle B A O) (angle E D O)))))

(defun problemY3 ()
    (setf *lines* '((A B C) (D E F) (A O D) (C O F) (B O E))
          *goal* '(segment-congruent (segment B O) (segment E O))
          *givens* '((congruent (segment A O) (segment D O))
                     (congruent (angle A B O) (angle D E O)))))

(defun problemYdnf ()
    (setf *lines* '((A B C) (D E F) (A O D) (C O F) (B O E))
          *goal* '(segment-congruent (segment A B) (segment D E))
          *givens* '((congruent (segment A O) (segment B O))
                     (congruent (angle O E D) (angle O D E)))))

(defun problemZ1 ()
    (setf *lines* '((A B E) (A C) (A D) (B C D) (C E))
          *goal* '(angle-congruent (angle A B C) (angle A C B))
          *givens* '((congruent (segment A B) (segment A C))
                     (congruent (segment A D) (segment C E))
                     (congruent (angle A D C) (angle B C E))
                     (congruent (angle D A C) (angle B E D)))))

(defun problemZ3 ()
    (setf *lines* '((A B E) (A C) (A D) (B C D) (C E))
          *goal* '(segment-congruent (segment A D) (segment E C))
          *givens* '((congruent (segment A B) (segment B E))
                     (congruent (segment B C) (segment C D))
                     (congruent (angle A B C) (angle A C B))
                     (congruent (angle A C D) (angle C B E)))))

(defun problemZdnf ()
    (setf *lines* '((A B E) (A C) (A D) (B C D) (C E))
          *goal* '(segment-congruent (segment A C) (segment E C))
          *givens* '((congruent (segment A B) (segment B E))
                     (congruent (segment A D) (segment C E))
                     (congruent (angle D A C) (angle B E C))
                     (congruent (angle A C D) (angle C B E)))))

(defun find-parts (seg1 seg2)
   (let* ((point11 (first seg1))
           (point12 (second seg1))
           (points13 (triangle-point point11 point12))
           (point21 (first seg2))
           (point22 (second seg2))
           (points23 (triangle-point point21 point22)))
      (do ((temp1 points13 (cdr temp1))
           (temp2 points23 (cdr temp2))
           (result nil (cons (list (list (car temp1) point11 point12)
                               (list (car temp2) point21 point22)) result)))
          ((null temp1) result))))


(defun triangle-point (p1 p2)
    (let (result results)
    (do ((temp1 *lines* (cdr temp1)))
        ((null temp1) (reverse results))
      (if (and (member p1 (car temp1)) (not (member p2 (car temp1))))
        (do ((temp2 (remove p1 (car temp1)) (cdr temp2)))
            ((null temp2) nil)
          (do ((temp3 *lines* (cdr temp3)))
              ((null temp3) nil)
            (if (and (member (car temp2) (car temp3)) (member p2 (car temp3)))
              (setf results (cons (car temp2) results)))))))))


(defvar *response*)
(setf *graphical-busy* nil)

(defun part-method (method) (member method '(corresponding-parts match-parts)))

(defun present-problem (problem)
    (let ((window (open-exp-window "Proof Experiment" :visible t)))
      (setf *graphical-busy* nil  *response* nil
            *feedback* nil *delay* nil)
      (reset)
      (apply problem nil)
      (add-dm (goal isa goal step start))
      (goal-focus goal)
      (install-device window)
      (add-text-to-exp-window :text "*" :x 150 :y 150 :width 25)
      (proc-display :clear t)
      (run 30)
     (schedule-event-relative 0 'feedback)
     (schedule-event-relative 0 'delay-bold)
      (run-full-time 17)
      (cons problem *response*)))

(defvar *feedback*)
(defun feedback () (setf *feedback* t))
(defvar *delay*)
(defun delay-bold () (setf *delay* t))

(defmethod rpm-window-key-event-handler ((win rpm-window) key)
      (setf *response* (list (get-time) key)))

(defun wait ()
   (setf *wait* t)
   (schedule-event-relative  (* 0.8 (no-output (car (sgp :lf)))) 'wait-done))

(defun wait-done ()  (setf *wait* nil))

(define-model proof


(sgp :do-not-harvest graphical :do-not-harvest imaginal :ncnar nil
:model-warnings nil :trace-detail low :esc t :rt -0.6 :v nil
      :DECLARATIVE-NUM-FINSTS   10 :DECLARATIVE-FINST-span     20.0 :ans .12)

(sgp :save-buffer-trace t :traced-buffers (graphical production goal retrieval imaginal manual))
(sgp :bold-inc 2 :bold-exp 5 :bold-scale 1.0)

(setf *graph-time* (+ .1 (random 0.6)))
(setf *retrieval-time* (+ .1 (random 2.4)))
(setf *imaginal-time* (+ .1 (random 0.8)))
(eval `(sgp :lf ,*retrieval-time* :Imaginal-delay ,*imaginal-time*))

(chunk-type goal step)
(chunk-type statement mode arg1 relation arg2)
(chunk-type encode type mode arg1 arg2 arg3)
(chunk-type proof method goal subgoal part1 part2 part3 relation step-count)
(chunk-type schema relation method inferences)
(chunk-type label mode value)
(chunk-type inference label)
(chunk-type look type mode arg1 relation arg2)

(add-dm (corresponding-parts1 isa schema relation segment-congruent method corresponding-parts inferences 1)
          (corresponding-parts2 isa schema relation angle-congruent method corresponding-parts inferences 1)
          (vertical-angles-schema isa schema relation angle-congruent method vertical-angles inferences 1)
          (isoceles1 isa schema relation segment-congruent method isoceles inferences 1)
          (isoceles2 isa schema relation angle-congruent method isoceles inferences 1)
          (alt-angles isa schema relation angle-congruent method alt-angles inferences 1)
          (corr-angles isa schema relation angle-congruent method corr-angles inferences 1)
          (another1 isa schema relation angle-congruent method another1 inferences 1)
          (another2 isa schema relation segment-congruent method another2 inferences 1)
          (another3 isa schema relation triangle-congruent method another3 inferences 1)
          (guess1 isa schema relation angle-congruent method guess inferences 3)
          (guess2 isa schema relation segment-congruent method guess inferences 3)
          (asa isa inference label asa)
          (sas isa inference label sas)
          (sss isa inference label sss)
          (aas isa inference label aas)
          (hl isa inference label hl)
          (isoceles isa inference label isoceles)
          (alt-angles1 isa inference label alt-angles)
          (corr-angles1 isa inference label corr-angles)
          (reflexive isa inference label reflexive)
          (vertical-angles isa inference label vertical-angles)
          (right-angles isa inference label right-angles)
          (right isa inference label right)
          (congruent-triangles isa schema relation triangle-congruent method match-parts inferences 0))

(sdp another1 :base-level -.6)
(sdp another2 :base-level -.6)
(sdp another3 :base-level -.6)
(sdp guess1 :base-level -.76)
(sdp guess2 :base-level -.76)


(p read-goal
     =goal>
       isa goal
       step start
    ?graphical>
        state free
==>
    +goal>
       step reading
     +graphical>
       isa encode
       type statement
        mode to-prove)

(p spin
   =goal>
      isa goal
    ?retrieval>
       state busy
    =imaginal>
       isa proof
    =graphical>
       isa statement
       mode =mode
       arg1 =arg1
       relation =relation
       arg2 =arg2
!eval! (not  *wait*)
==>
!eval! (wait)
    +graphical>
       isa look
       mode =mode
       arg1 =arg1
       relation =relation
       arg2 =arg2
   +imaginal> =imaginal)

(p spin1
  =goal>
     isa goal
   ?retrieval>
      state busy
   =imaginal>
      isa proof
   =graphical>
      isa statement
      mode nil
      arg1 nil
      arg2 nil
      relation none
!eval! (not  *wait*)
==>
!eval! (wait)
   +graphical>
      isa look
      mode nil
      arg1 nil
      relation none
      arg2 nil
  +imaginal> =imaginal)

(p encode-goal
     =goal>
       isa goal
       step reading
    =graphical>
        isa statement
        mode to-prove
        arg1 =arg1
        relation =relation
        arg2  =arg2
==>
    =goal>
       step retrieving
     +retrieval>
       isa schema
        relation =relation
        :recently-retrieved nil)

(p simple-inference
     =goal>
       isa goal
       step retrieving
    =retrieval>
        isa schema
        method =method
        relation =relation
        inferences =count
    =graphical>
        isa statement
        arg1 =arg1
        arg2 =arg2
!eval! (not (part-method =method))
==>
!output! (trying =method)
    +goal>
       step proving-inference
    +imaginal>
        isa proof
        method =method
        goal =graphical
        relation =relation
        step-count =count
     +graphical>
       isa encode
       type statement
        mode =method
        arg1 =arg1
        arg2 =arg2)

(p proved-inference
     =goal>
       isa goal
       step proving-inference
     =graphical>
        isa statement
        - relation none
        - relation nil
==>
    +goal>
       step done)

(p start-corresponding-parts
     =goal>
       isa goal
       step retrieving
    =retrieval>
        isa schema
        method =method
        relation =relation
        inferences =count
    =graphical>
        isa statement
        arg1 =arg1
        arg2 =arg2
   ?imaginal>
   state free
   !eval! (part-method =method)
==>
!output! (trying =method)
    +goal>
       step corresponding-parts
    +imaginal>
        isa proof
        method =method
        goal =graphical
        relation =relation
        step-count =count
     +graphical>
       isa encode
       type statement
        mode corresponding-parts
        arg1 =arg1
        arg2 =arg2)

(p try-part
     =goal>
       isa goal
       step corresponding-parts
    =graphical>
        isa statement
        arg1 =arg1
        arg2 =arg2
    =imaginal>
        isa proof
        method =method
!eval! (part-method =method)
==>
    +goal>
       step find-part
    =imaginal>
        subgoal =graphical
     +graphical>
       isa encode
       type statement
        mode find-part)

(p check-given
     =goal>
       isa goal
       step find-part
    =graphical>
        isa statement
        arg1 =arg1
        arg2 =arg2
    ?imaginal>
        state free
    =imaginal>
        isa proof
        method =method
!eval! (part-method =method)
==>
    =goal>
       step check-given
     +graphical>
       isa encode
       type statement
        mode check
        arg1 =arg1
        arg2 =arg2)

(p assess-given
     =goal>
       isa goal
       step assess-part
    ?imaginal>
        state free
    =graphical>
        isa statement
        relation given-congruent
==>
    +goal>
       step find-part
     +graphical>
       isa encode
       type statement
        mode find-part)

(p assess-inference
     =goal>
       isa goal
       step assess-part
    ?imaginal>
        state free
    =graphical>
        isa statement
      -  relation given-congruent
        relation =label
==>
    =goal>
       step check-inference
    +retrieval>
       isa inference
       label =label)

(p check-inference
    =goal>
       isa goal
       step check-inference
    =retrieval>
       isa inference
       label =label
    =imaginal>
        isa proof
        step-count =count
==>
!output! (inferring =label)
!bind! =new (1+ =count)
    +goal>
       step find-part
    +imaginal>
        step-count =new
     +graphical>
       isa encode
       type statement
        mode find-part)

(p note-part1-given
     =goal>
       isa goal
       step check-given
    =graphical>
        isa statement
      -  relation nil
    =imaginal>
        isa proof
        method =method
        part1 nil
!eval! (part-method =method)
==>
    =goal>
       step assess-part
    +imaginal>
        part1 =graphical)

(p note-part2-given
     =goal>
       isa goal
       step check-given
    =graphical>
        isa statement
      -  relation nil
    =imaginal>
        isa proof
        method =method
        part1 =part
        part2 nil
!eval! (part-method =method)
==>
    =goal>
       step assess-part
    +imaginal>
        part2 =graphical)

(p note-part3-given
     =goal>
       isa goal
       step check-given
    =graphical>
        isa statement
      -  relation nil
    =imaginal>
        isa proof
        method =method
        part1 =part1
        part2 =part2
        part3 nil
!eval! (part-method =method)
==>
    =goal>
       step label-parts
    +imaginal>
        part3 =graphical
     +graphical>
       isa encode
       type label
        mode label-parts
        arg1 =part1
        arg2 =part2
        arg3 =graphical)

(p check-next
     =goal>
       isa goal
       step check-given
    =graphical>
        isa statement
        relation nil
==>
    +goal>
       step find-part
     +graphical>
       isa encode
       type statement
        mode find-part)

(p try-another-method
     =goal>
       isa goal
       step find-part
    =graphical>
        isa statement
        relation done
    ?imaginal>
        state free
    =imaginal>
        isa proof
        goal =statement
        method =method
        relation =relation
        part2 nil
!eval! (part-method =method)
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
         :recently-retrieved nil)

(p try-another-method1
     =goal>
       isa goal
       step RETRIEVING-SUB-SCHEMA
    ?retrieval>
       state error
    =imaginal>
        isa proof
        goal =statement
        method =method
        relation =relation
        part1 =part1
        part2 =part2
        part3 nil
!eval! (part-method =method)
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
         :recently-retrieved nil)

(p try-another-method2
     =goal>
       isa goal
       step proving-inference
    =graphical>
        isa statement
        relation none
    =imaginal>
        isa proof
        goal =statement
        method =method
        relation =relation
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
         :recently-retrieved nil)

(p try-another-method3
     =goal>
       isa goal
       step find-third-part
    =graphical>
        isa statement
        relation nil
    =imaginal>
        isa proof
        goal =statement
        method =method
        relation =relation
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
         :recently-retrieved nil)

(p try-another-method4
     =goal>
       isa goal
       step corresponding-parts
    =graphical>
        isa statement
        relation nil
    =imaginal>
        isa proof
        goal =statement
        relation =relation
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
         :recently-retrieved nil)

(p try-another-method5
     =goal>
       isa goal
       step label-parts
    =graphical>
        isa label
        MODE  LABEL-PARTS
        VALUE  NIL
    ?imaginal>
        state free
    =imaginal>
        isa proof
        goal =statement
        relation =relation
==>
     =graphical> =statement
     =GOAL>
         STEP RETRIEVING
     +RETRIEVAL>
         ISA SCHEMA
         RELATION =RELATION
    :recently-retrieved nil)

(p assess-corresponding-parts
     =goal>
       isa goal
       step find-part
    =graphical>
        isa statement
        relation done
    ?imaginal>
        state free
    =imaginal>
        isa proof
        method =method
        part1 =part1
        part2 =part2
        part3 =part3
!eval! (part-method =method)
==>
    =goal>
       step label-parts
     +graphical>
       isa encode
       type label
        mode label-parts
        arg1 =part1
        arg2 =part2
        arg3 =part3)

(p find-part-to-subgoal
     =goal>
       isa goal
       step find-part
    =graphical>
        isa statement
        relation done
    ?imaginal>
        state free
    =imaginal>
        isa proof
        method =method
        part1 =part1
        part2 =part2
        part3 nil
!eval! (part-method =method)
==>
    +goal>
       step find-third-part
     +graphical>
       isa encode
       type statement
        mode find-third-part
        arg1 =part1
        arg2 =part2)

(p find-sub-schema
     =goal>
       isa goal
       step find-third-part
    =graphical>
        isa statement
        relation =relation
    =imaginal>
        isa proof
        method =method
==>
    =goal>
       step retrieving-sub-schema
     +retrieval>
       isa schema
       relation =relation
      - method corresponding-parts
         :recently-retrieved nil)

(p try-another-schema
     =goal>
       isa goal
       step proving-third-part
    =graphical>
        isa statement
         relation none
         mode =mode
    =retrieval>
       isa schema
       relation =relation
==>
    =goal>
       step retrieving-sub-schema
     +retrieval>
       isa schema
       relation =relation
      - method corresponding-parts
         :recently-retrieved nil)

(p found-part-three
     =goal>
       isa goal
       step proving-third-part
    =graphical>
        isa statement
     -   relation none
         mode =method
==>
     =goal>
        step checking-step-three
     +retrieval>
        isa inference
        label =method)

(p done-part-three
     =goal>
        isa goal
        step checking-step-three
     =retrieval>
        isa inference
        label =method
    =imaginal>
        isa proof
        part1 =part1
        part2 =part2
        step-count =count
    =graphical>
        isa statement
==>
!output! (inferring =method)
!bind! =new (1+ =count)
    +imaginal>
        part3 =graphical
        step-count =new
    =goal>
       step label-parts
     +graphical>
       isa encode
       type label
        mode label-parts
        arg1 =part1
        arg2 =part2
   arg3 =graphical)

(p corresponding-chain
     =goal>
       isa goal
       step  retrieving-sub-schema
    =retrieval>
        isa schema
        method =method
    =imaginal>
        isa proof
        method =test
    =graphical>
        isa statement
        arg1 =arg1
        arg2 =arg2
!eval! (member =test '(corresponding-parts match-parts))
==>
     =retrieval>
    +goal>
       step proving-third-part
     +graphical>
       isa encode
       type statement
        mode  =method
        arg1 =arg1
   arg2 =arg2)

(p corresponding-parts-3
     =goal>
       isa goal
       step label-parts
    ?imaginal>
        state free
    =graphical>
        isa label
         value =label
==>
     =goal>
       step checking-parts
     +retrieval>
        isa inference
        label =label)

(p triangle-proved
     =goal>
       isa goal
       step checking-parts
     =retrieval>
        isa inference
        label =label
     =imaginal>
       isa proof
       step-count =count
    ?imaginal>
        state free
==>
!output! (inferring =label)
!bind! =new (1+ =count)
    +imaginal>
       step-count =new
    +goal>
       step done)


(p stuck
    =goal>
       isa goal
       step retrieving
    =graphical>
       isa statement
       relation =relation
    ?retrieval>
       state error
==>
    +graphical>
     isa encode
     type statement
    +imaginal>
       isa proof
       step-count 5
     +retrieval>
       isa schema
       relation =relation
     :recently-retrieved nil
     +goal>
   step confirm-dnf)

(p stuck2
    =goal>
       isa goal
       step retrieving-sub-schema
    =graphical>
       isa statement
       relation =relation
    ?retrieval>
       state error
==>
    +graphical>
     isa encode
     type statement
    +imaginal>
       isa proof
       step-count 5
     +retrieval>
       isa schema
       relation =relation
     :recently-retrieved nil
     +goal>
   step confirm-dnf)

(p stuck3
    =goal>
       isa goal
       step check-inference
   =graphical>
       isa statement
       relation =relation
    ?retrieval>
       state error
==>
    +graphical>
     isa encode
     type statement
    +imaginal>
       isa proof
       step-count 5
     +retrieval>
       isa schema
       relation =relation
     :recently-retrieved nil
     +goal>
       step confirm-dnf)


(p give-up
    =goal>
       isa goal
       step confirm-dnf
    ?retrieval>
       state free
    ?imaginal>
       state free
    ?graphical>
       state free
==>
    +imaginal>
       isa proof
       step-count 5
    +goal>
       step done)

(p guess
   =goal>
       isa goal
       step retrieving
    =retrieval>
       isa schema
       method guess
==>
    +imaginal>
     isa proof
     step-count 3
    +goal>
   step done)

(p press-five
     =goal>
       isa goal
       step done
     =imaginal>
       isa proof
       step-count 5
    ?imaginal>
     state free
==>
    +retrieval>
     isa proof
     +goal>
        step feedback
     +manual>
         isa press-key
         key "5")

(p press-three
     =goal>
       isa goal
       step done
     =imaginal>
       isa proof
       step-count 3
     ?imaginal>
       state free
==>
    +retrieval>
     isa proof
     +goal>
        step feedback
     +manual>
         isa press-key
     key "3")

(p press-three2
     =goal>
       isa goal
       step done
     =imaginal>
       isa proof
       step-count 2
     ?imaginal>
       state free
==>
    +retrieval>
     isa proof
     +goal>
        step feedback
     +manual>
         isa press-key
     key "3")

(p press-three4
     =goal>
       isa goal
       step done
     =imaginal>
       isa proof
       step-count 4
     ?imaginal>
       state free
==>
    +retrieval>
     isa proof
     +goal>
        step feedback
     +manual>
         isa press-key
     key "3")

(p press-one
     =goal>
       isa goal
       step done
     =imaginal>
       isa proof
       step-count 1
     ?imaginal>
       state free
==>
    +retrieval>
     isa proof
     +goal>
        step feedback
     +manual>
         isa press-key
         key "1")

(p process-feedback
    =goal>
     isa goal
     step feedback
!eval! *feedback*
==>
    +goal>
     step fixation
    +graphical>
     isa encode
     type statement
    +imaginal>
     isa proof

)

(p iti
    =goal>
     isa goal
    step fixation
    ?graphical>
     state free
    ?imaginal>
     state free
    ?retrieval>
     state free
!eval! *delay*
==>
    +goal>
     step stop
    +graphical>
     isa encode
     type statement
    )

)