March 3, 1997

156ers,

   This is a transcript of a test of my version of Assignment 2.  The
results of your test should look something like this.  Of course you
needn't use the same conventions for constructing your new variable
names.
                    
  -- JDS


OK
[3] (pp d1)

((FORALL ?X)
 (IMPLIES (IMPLIES (P ?X) (Q ?X)) (R ?X)))
[4] (pp (convert d1))

(((P ?X_0_1) (R ?X_0_1))
 ((NOT (Q ?X_0_2)) (R ?X_0_2)))
[5] (pp d2)

((FORALL ?X)
 (IMPLIES (P ?X) (IMPLIES (Q ?X) (R ?X))))
[6] (pp (convert d2))

(((NOT (P ?X_3_4)) (NOT (Q ?X_3_4)) (R ?X_3_4)))
[7] (pp (convert d3))

(((MALE ?X_5_7) (FEMALE ?X_6_8)))
[8] (pp d3)

(OR ((FORALL ?X) (MALE ?X))
    ((FORALL ?X) (FEMALE ?X)))
[9] (pp d4)

((FORALL ?Z)
 (NOT ((FORALL ?Y) (IMPLIES (P ?Y ?Z) (Q ?Y ?Z)))))
[10] (pp (convert d4))

(((P (SK_Y_10 ?Z_9_11) ?Z_9_11))
 ((NOT (Q (SK_Y_10 ?Z_9_12) ?Z_9_12))))
[11] (pp d5)

(IMPLIES
   ((FORALL ?X) (IMPLIES (NOT (P ?X)) (NOT (Q ?X))))
   ((FORALL ?X) (IMPLIES (P ?X) (Q ?X))))
[12] (pp (convert d5))

(((NOT (P (SK_X_13)))
  (NOT (P ?X_14_15))
  (Q ?X_14_15))
 ((Q (SK_X_13))
  (NOT (P ?X_14_16))
  (Q ?X_14_16)))
[13] (pp d6)

(AND ((FORALL ?X)
      (IMPLIES (P ?X) ((EXISTS ?Y) (Q ?X ?Y))))
     ((FORALL ?X)
      (IMPLIES ((EXISTS ?Y) (Q ?X ?Y)) (P ?X))))
[14] (pp (convert d6))

(((NOT (P ?X_17_21))
  (Q ?X_17_21 (SK_Y_18 ?X_17_21)))
 ((NOT (Q ?X_19_23 ?Y_20_22)) (P ?X_19_23)))
[15] (pp d7)

(OR (NOT ((FORALL ?X)
          (IMPLIES (P ?X) ((EXISTS ?Y) (Q ?X ?Y)))))
    (NOT ((FORALL ?X)
          (IMPLIES ((EXISTS ?Y) (Q ?X ?Y)) (P ?X)))))
[16] (pp (convert d7))

(((P (SK_X_24))
  (Q (SK_X_26 ?Y_25_28) (SK_Y_27 ?Y_25_28)))
 ((NOT (Q (SK_X_24) ?Y_25_29))
  (Q (SK_X_26 ?Y_25_29) (SK_Y_27 ?Y_25_29)))
 ((P (SK_X_24)) (NOT (P (SK_X_26 ?Y_25_30))))
 ((NOT (Q (SK_X_24) ?Y_25_31))
  (NOT (P (SK_X_26 ?Y_25_31)))))
[17] (pp d8)

((FORALL ?A)
 ((FORALL ?B)
  ((FORALL ?C)
   (NOT ((FORALL ?D)
         (IMPLIES (P ?A ?B) (OR (Q ?C) (R ?D))))))))
[18] (pp (convert d8))

(((P ?A_32_36 ?B_33_37))
 ((NOT (Q ?C_34_38)))
 ((NOT (R (SK_D_35 ?C_34_39 ?B_33_40 ?A_32_41)))))
[19] (pp d9)

((EXISTS ?A)
 ((FORALL ?B)
  ((EXISTS ?C)
   ((FORALL ?D)
    ((EXISTS ?E)
     (AND (AND (P ?A ?B) (Q ?C ?D)) (R ?E F)))))))
[20] (pp (convert d9))

(((P (SK_A_42) ?B_43_47))
 ((Q (SK_C_44 ?B_43_48) ?D_45_49))
 ((R (SK_E_46 ?D_45_50 ?B_43_51) F)))
[21] (transcript-off)