(PDS (problem SQRT2-NOT-RAT)
  (in REAL)
 (declarations (type-variables )(type-constants )
    (constants  (K NUM) (N NUM) (M NUM))(meta-variables )(variables ))
   (conclusion SQRT2-NOT-RAT)
   (assumptions)
   (open-nodes)
   (support-nodes EVEN-COMMON-DIVISOR SQUARE-EVEN RAT-CRITERION)
   (nodes
     (L19 (L19) (AND (INT K) (= M (TIMES 2 K)))
      (0 ("HYP" () () "grounded" () ()))
      )
     (L22 (EVEN-COMMON-DIVISOR L19) (= M (TIMES 2 K))
      (0 ("ANDE" () (L19) "unexpanded" ()
          ("L21" "NONEXISTENT" "EXISTENT")))
      )
     (L21 (EVEN-COMMON-DIVISOR L19) (INT K)
      (0 ("ANDE" () (L19) "unexpanded" ()
          ("NONEXISTENT" "L22" "EXISTENT")))
      )
     (L8 (L8) (AND (INT M) (AND (= (TIMES (SQRT 2) N) M) (NOT (EXISTS-SORT (lam (VAR76 NUM) (COMMON-DIVISOR N M VAR76)) INT))))
      (0 ("HYP" () () "grounded" () ()))
      )
     (L12 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8) (NOT (EXISTS-SORT (lam (VAR76 NUM) (COMMON-DIVISOR N M VAR76)) INT))
      (0 ("ANDE*" () (L8) "unexpanded" ()
          ("L10" "L11" "NONEXISTENT" "EXISTENT")))
      )
     (L11 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8) (= (TIMES (SQRT 2) N) M)
      (0 ("ANDE*" () (L8) "unexpanded" ()
          ("L10" "NONEXISTENT" "L12" "EXISTENT")))
      )
     (L10 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8) (INT M)
      (0 ("ANDE*" () (L8) "unexpanded" ()
          ("NONEXISTENT" "L11" "L12" "EXISTENT")))
      )
     (L4 (L4) (AND (INT N) (EXISTS-SORT (lam (VAR79 NUM) (AND (= (TIMES (SQRT 2) N) VAR79) 
      (NOT (EXISTS-SORT (lam (VAR80 NUM) (COMMON-DIVISOR N VAR79 VAR80)) INT)))) INT))
      (0 ("HYP" () () "grounded" () ()))
      )
     (L7 (EVEN-COMMON-DIVISOR SQUARE-EVEN L4) (EXISTS-SORT (lam (VAR79 NUM) (AND (= (TIMES 
      (SQRT 2) N) VAR79) (NOT (EXISTS-SORT (lam (VAR80 NUM) (COMMON-DIVISOR N VAR79 VAR80)) INT)))) INT)
      (0 ("ANDE" () (L4) "unexpanded" ()
          ("L6" "NONEXISTENT" "EXISTENT")))
      )
     (L6 (EVEN-COMMON-DIVISOR SQUARE-EVEN L4) (INT N)
      (0 ("ANDE" () (L4) "unexpanded" ()
          ("NONEXISTENT" "L7" "EXISTENT")))
      )
     (L1 (L1) (RAT (SQRT 2))
      (0 ("HYP" () () "grounded" () ()))
      )
     (L2 (EVEN-COMMON-DIVISOR SQUARE-EVEN RAT-CRITERION L1) FALSE
      (0 ("EXISTSE-SORT" ((:pds-term N)) (L3 L5) "unexpanded" ()
          ("EXISTENT" "EXISTENT" "NONEXISTENT")))
      )
     (RAT-CRITERION (RAT-CRITERION) (FORALL-SORT (lam (VAR81 NUM) (EXISTS-SORT (lam (VAR82 NUM) 
      (EXISTS-SORT (lam (VAR83 NUM) (AND (= (TIMES VAR81 VAR82) VAR83) (NOT (EXISTS-SORT 
      (lam (VAR84 NUM) (COMMON-DIVISOR VAR82 VAR83 VAR84)) INT)))) INT)) INT)) RAT)
      (0 ("THM" () () "grounded" () ()))
      )
     (L9 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) FALSE
      (0 ("EXISTSE-SORT" ((:pds-term K)) (L18 L20) "unexpanded" ()
          ("EXISTENT" "EXISTENT" "NONEXISTENT")))
      )
     (L5 (EVEN-COMMON-DIVISOR SQUARE-EVEN L4 RAT-CRITERION L1) FALSE
      (0 ("EXISTSE-SORT" ((:pds-term M)) (L7 L9) "unexpanded" ()
          ("EXISTENT" "EXISTENT" "NONEXISTENT")))
      )
     (L3 (EVEN-COMMON-DIVISOR SQUARE-EVEN RAT-CRITERION L1) (EXISTS-SORT (lam (VAR85 NUM) 
      (EXISTS-SORT (lam (VAR86 NUM) (AND (= (TIMES (SQRT 2) VAR85) VAR86) (NOT (EXISTS-SORT 
      (lam (VAR87 NUM) (COMMON-DIVISOR VAR85 VAR86 VAR87)) INT)))) INT)) INT)
      (0 ("FORALLE-SORT" ((:pds-term (SQRT 2))) (RAT-CRITERION L1) "unexpanded"
          () ("NONEXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L13 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (= (POWER M 2) 
      (TIMES 2 (POWER N 2)))
      (0 ("BY-COMPUTATION" () (L11) "unexpanded" ()
          ("EXISTENT" "EXISTENT")))
      )
     (L15 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EXISTS-SORT (lam (VAR88 NUM) 
      (= (POWER M 2) (TIMES 2 VAR88))) INT)
      (0 ("EXISTSI-SORT" ((:pds-term (POWER N 2))((:pds-post-obj (position 2 2)))) (L13 L16) 
      "unexpanded"
          () ("EXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L14 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EVENP (POWER M 2))
      (0 ("DefnI" ((:pds-term EVENP)(:pds-term (lam (X NUM) (EXISTS-SORT (lam (Y NUM) 
      (= X (TIMES 2 Y))) INT)))(:pds-post-obj (position 0))) (L15) "grounded"
          () ("EXISTENT" "NONEXISTENT")))
      )
     (L16 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (INT (POWER N 2))
      (0 ("WELLSORTED" ((((:pds-term (POWER N (S (S ZERO))))(:pds-sort INT)(:pds-symbol 
       POWER-INT-CLOSED))((:pds-term (S (S ZERO)))(:pds-sort INT)(:pds-symbol NAT-INT))
       ((:pds-term (S (S ZERO)))(:pds-sort NAT)(:pds-symbol SUCC-NAT))((:pds-term (S ZERO))
       (:pds-sort NAT)(:pds-symbol SUCC-NAT))((:pds-term ZERO)(:pds-sort NAT)
       (:pds-symbol ZERO-NAT)))) (L6) "unexpanded"
          () ("EXISTENT" "EXISTENT")))
      )
     (SQUARE-EVEN (SQUARE-EVEN) (FORALL-SORT (lam (VAR89 NUM) (EQUIV (EVENP (POWER VAR89 2)) 
      (EVENP VAR89))) INT)
      (0 ("THM" () () "grounded" () ()))
      )
     (L20 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) FALSE
      (0 ("WEAKEN" () (L29) "grounded" () ("EXISTENT" "EXISTENT")))
      )
     (L17 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EVENP M)
      (0 ("ASSERT" ((:pds-term (EVENP M))(:pds-nil)) (SQUARE-EVEN L10 L14) "unexpanded"
          () ("NONEXISTENT" "EXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L18 (EVEN-COMMON-DIVISOR SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EXISTS-SORT (lam (VAR90 NUM) 
      (= M (TIMES 2 VAR90))) INT)
      (0 ("DefnE" ((:pds-term EVENP)(:pds-term (lam (X NUM) (EXISTS-SORT (lam (Y NUM) 
      (= X (TIMES 2 Y))) INT)))(:pds-post-obj (position 0))) (L17) "grounded"
          () ("NONEXISTENT" "EXISTENT")))
      )
     (L23 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (= (POWER N 2) (TIMES 2 (POWER K 2)))
      (0 ("BY-COMPUTATION" () (L13 L22) "unexpanded" ()
          ("EXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L25 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EXISTS-SORT (lam 
      (VAR91 NUM) (= (POWER N 2) (TIMES 2 VAR91))) INT)
      (0 ("EXISTSI-SORT" ((:pds-term (POWER K 2))((:pds-post-obj (position 2 2)))) (L23 L26) 
      "unexpanded"
          () ("EXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L24 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EVENP (POWER N 2))
      (0 ("DefnI" ((:pds-term EVENP)(:pds-term (lam (X NUM) (EXISTS-SORT (lam (Y NUM) 
      (= X (TIMES 2 Y))) INT)))(:pds-post-obj (position 0))) (L25) "grounded"
          () ("EXISTENT" "NONEXISTENT")))
      )
     (L27 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (EVENP N)
      (0 ("ASSERT" ((:pds-term (EVENP N))(:pds-nil)) (SQUARE-EVEN L6 L24) "unexpanded"
          () ("NONEXISTENT" "EXISTENT" "EXISTENT" "EXISTENT")))
      )
     (L26 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (INT (POWER K 2))
      (0 ("WELLSORTED" ((((:pds-term (POWER K (S (S ZERO))))(:pds-sort INT)(:pds-symbol POWER-INT-CLOSED))
      ((:pds-term (S (S ZERO)))(:pds-sort INT)(:pds-symbol NAT-INT))((:pds-term (S (S ZERO)))
      (:pds-sort NAT)(:pds-symbol SUCC-NAT))((:pds-term (S ZERO))(:pds-sort NAT)(:pds-symbol SUCC-NAT))
      ((:pds-term ZERO)(:pds-sort NAT)(:pds-symbol ZERO-NAT)))) (L21) "unexpanded"
          () ("EXISTENT" "EXISTENT")))
      )
     (EVEN-COMMON-DIVISOR (EVEN-COMMON-DIVISOR) (FORALL-SORT (lam (VAR92 NUM) (FORALL-SORT 
      (lam (VAR93 NUM) (IMPLIES (AND (EVENP VAR92) (EVENP VAR93)) (COMMON-DIVISOR VAR92 VAR93 2))) 
      INT)) INT)
      (0 ("THM" () () "grounded" () ()))
      )
     (L28 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) (INT 2)
      (0 ("WELLSORTED" ((((:pds-term (S (S ZERO)))(:pds-sort INT)(:pds-symbol NAT-INT))
      ((:pds-term (S (S ZERO)))(:pds-sort NAT)(:pds-symbol SUCC-NAT))((:pds-term (S ZERO))
      (:pds-sort NAT)(:pds-symbol SUCC-NAT))((:pds-term ZERO)(:pds-sort NAT)(:pds-symbol ZERO-NAT)))) 
      () "unexpanded"
          () ("EXISTENT")))
      )
     (L29 (EVEN-COMMON-DIVISOR L19 SQUARE-EVEN L8 L4 RAT-CRITERION L1) FALSE
      (0 ("ASSERT" ((:pds-term FALSE)(:pds-nil)) (EVEN-COMMON-DIVISOR L10 L6 L12 L17 L27 L28) 
       "unexpanded"
          ()
          ("NONEXISTENT" "EXISTENT" "EXISTENT" "EXISTENT" "EXISTENT" "EXISTENT" "EXISTENT" 
           "EXISTENT")))
      )
     (SQRT2-NOT-RAT (EVEN-COMMON-DIVISOR SQUARE-EVEN RAT-CRITERION) (NOT (RAT (SQRT 2)))
      (0 ("NOTI" () (L2) "grounded" () ("EXISTENT" "NONEXISTENT")))
      ))
   (lemmata)
   (agenda)
   (controls
     (L19 (() () () ()))
     (L22 (() () () ()))
     (L21 (() () () ()))
     (L8 (() () () ()))
     (L12 (() () () ()))
     (L11 (() () () ()))
     (L10 (() () () ()))
     (L4 (() () () ()))
     (L7 (() () () ()))
     (L6 (() () () ()))
     (L1 (() () () ()))
     (L2 ((L3 L1) () () ()))
     (RAT-CRITERION (() () () ()))
     (L9 ((L16 L6 L7 L4 L1 L3 L8 L12 L11 L10 L13 L14 L17 L18) (L5 L2 L17) () ()))
     (L5 ((L6 L7 L4 L1 L3) (L2) () ()))
     (L3 (() () () ()))
     (L13 ((L10 L11 L12 L8 L3 L1 L4 L7 L6) () () ()))
     (L15 ((L13 L10 L11 L12 L8 L3 L1 L4 L7 L6) () () ()))
     (L14 ((L13 L10 L11 L12 L8 L3 L1 L4 L7 L6) () () ()))
     (L16 ((L6 L7 L4 L1 L3 L8 L12 L11 L10 L13 L14) () () ()))
     (SQUARE-EVEN (() () () ()))
     (L20 ((L29 L28 L27 L24 L23 L21 L22 L19 L18 L14 L13 L10 L11 L12 L8 L3 L1 L4 L7 L6 L16 L26 L17) 
     (L9 L5 L2) () ()))
     (L17 ((L26 L16 L6 L7 L4 L1 L3 L8 L12 L11 L10 L13 L14 L17 L18 L19 L22 L21 L23 L24 L27 L28) 
     (L17 L2 L5 L9) () ()))
     (L18 (() () () ()))
     (L23 ((L21 L22 L19 L18 L14 L13 L10 L11 L12 L8 L3 L1 L4 L7 L6 L16) () () ()))
     (L25 ((L23 L21 L22 L19 L18 L14 L13 L10 L11 L12 L8 L3 L1 L4 L7 L6 L16) () () ()))
     (L24 ((L23 L21 L22 L19 L18 L14 L13 L10 L11 L12 L8 L3 L1 L4 L7 L6 L16) () () ()))
     (L27 (() () () ()))
     (L26 ((L16 L6 L7 L4 L1 L3 L8 L12 L11 L10 L13 L14 L18 L19 L22 L21 L23 L24) () () ()))
     (EVEN-COMMON-DIVISOR (() () () ()))
     (L28 ((L27 L24 L23 L21 L22 L19 L18 L14 L13 L10 L11 L12 L8 L3 L1 L4 L7 L6 L16 L26) () () ()))
     (L29 (() () () ()))
     (SQRT2-NOT-RAT (() () () ())))
   (plan-steps (SQRT2-NOT-RAT 0 L1 0 L2 0) (L3 0 RAT-CRITERION 0 L1 0)
     (L2 0 L4 0 L3 0 L5 0) (L6 0 L4 0) (L7 0 L4 0)
     (L5 0 L8 0 L7 0 L9 0) (L10 0 L8 0) (L11 0 L8 0) (L12 0 L8 0)
     (L13 0 L11 0) (L14 0 L15 0) (L16 0 L6 0) (L15 0 L13 0 L16 0)
     (L17 0 SQUARE-EVEN 0 L10 0 L14 0) (L18 0 L17 0)
     (L9 0 L19 0 L18 0 L20 0) (L21 0 L19 0) (L22 0 L19 0)
     (L23 0 L13 0 L22 0) (L24 0 L25 0) (L26 0 L21 0)
     (L25 0 L23 0 L26 0) (L27 0 SQUARE-EVEN 0 L6 0 L24 0) (L28 0)
     (L29 0 EVEN-COMMON-DIVISOR 0 L10 0 L6 0 L12 0 L17 0 L27 0 L28 0)
     (L20 0 L29 0) ))