(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(DEFN OPPOSITE-COLOR
      (X Y)
      (OR (AND (NUMBERP X) (NOT (NUMBERP Y)))
          (AND (NUMBERP Y) (NOT (NUMBERP X)))))

     Note that (OR (FALSEP (OPPOSITE-COLOR X Y)) (TRUEP (OPPOSITE-COLOR X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

OPPOSITE-COLOR


(DEFN ALTERNATING-COLORS
      (X)
      (IF (OR (NLISTP X) (NLISTP (CDR X)))
          T
          (AND (OPPOSITE-COLOR (CAR X) (CADR X))
               (ALTERNATING-COLORS (CDR X)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of OR and NLISTP inform us that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
ALTERNATING-COLORS is accepted under the definitional principle.  Note that:
      (OR (FALSEP (ALTERNATING-COLORS X))
          (TRUEP (ALTERNATING-COLORS X)))
is a theorem.




[ 0.0 0.0 0.0 ]

ALTERNATING-COLORS


(DEFN PAIRED-COLORS
      (X)
      (IF (OR (NLISTP X) (NLISTP (CDR X)))
          T
          (AND (OPPOSITE-COLOR (CAR X) (CADR X))
               (PAIRED-COLORS (CDDR X)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of OR and NLISTP inform us that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
PAIRED-COLORS is accepted under the definitional principle.  Observe that:
      (OR (FALSEP (PAIRED-COLORS X))
          (TRUEP (PAIRED-COLORS X)))
is a theorem.




[ 0.0 0.0 0.0 ]

PAIRED-COLORS


(DEFN PLISTP
      (X)
      (IF (NLISTP X)
          (EQUAL X NIL)
          (PLISTP (CDR X))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, PLISTP is accepted under the principle of definition.  From the
definition we can conclude that (OR (FALSEP (PLISTP X)) (TRUEP (PLISTP X))) is
a theorem.




[ 0.0 0.0 0.0 ]

PLISTP


(DEFN SHUFFLEP
      (X Y Z)
      (IF (NLISTP Z)
          (AND (EQUAL X NIL)
               (EQUAL Y NIL)
               (EQUAL Z NIL))
          (IF (NLISTP X)
              (AND (EQUAL X NIL)
                   (EQUAL Y Z)
                   (PLISTP Y))
              (IF (NLISTP Y)
                  (AND (EQUAL Y NIL)
                       (EQUAL X Z)
                       (PLISTP X))
                  (OR (AND (EQUAL (CAR X) (CAR Z))
                           (SHUFFLEP (CDR X) Y (CDR Z)))
                      (AND (EQUAL (CAR Y) (CAR Z))
                           (SHUFFLEP X (CDR Y) (CDR Z))))))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, SHUFFLEP is accepted under the definitional principle.  From the
definition we can conclude that:
      (OR (FALSEP (SHUFFLEP X Y Z))
          (TRUEP (SHUFFLEP X Y Z)))
is a theorem.




[ 0.0 0.0 0.0 ]

SHUFFLEP


(DEFN EVEN-LENGTH
      (L)
      (IF (NLISTP L)
          T
          (IF (NLISTP (CDR L))
              F
              (EVEN-LENGTH (CDDR L)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, EVEN-LENGTH
is accepted under the principle of definition.  From the definition we can
conclude that (OR (FALSEP (EVEN-LENGTH L)) (TRUEP (EVEN-LENGTH L))) is a
theorem.




[ 0.0 0.0 0.0 ]

EVEN-LENGTH


(PROVE-LEMMA AL->PP
             (REWRITE)
             (IMPLIES (ALTERNATING-COLORS X)
                      (PAIRED-COLORS X)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (OR (NLISTP X) (NLISTP (CDR X)))
                    (p X))
           (IMPLIES (AND (NOT (OR (NLISTP X) (NLISTP (CDR X))))
                         (p (CDDR X)))
                    (p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions
of OR and NLISTP establish that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces the following three new goals:

Case 3. (IMPLIES (AND (OR (NLISTP X) (NLISTP (CDR X)))
                      (ALTERNATING-COLORS X))
                 (PAIRED-COLORS X)).

  This simplifies, expanding the definitions of NLISTP, OR, ALTERNATING-COLORS,
  and PAIRED-COLORS, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (NLISTP X) (NLISTP (CDR X))))
                      (NOT (ALTERNATING-COLORS (CDDR X)))
                      (ALTERNATING-COLORS X))
                 (PAIRED-COLORS X)).

  This simplifies, expanding NLISTP, OR, ALTERNATING-COLORS, OPPOSITE-COLOR,
  and PAIRED-COLORS, to the following two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP X)
                        (LISTP (CDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NUMBERP (CAR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X))))
                   (PAIRED-COLORS (CDDR X))).

    But this further simplifies, expanding ALTERNATING-COLORS, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP X)
                        (LISTP (CDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (NUMBERP (CAR X)))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X))))
                   (PAIRED-COLORS (CDDR X))),

    which further simplifies, expanding the definition of ALTERNATING-COLORS,
    to:

          T.

Case 1. (IMPLIES (AND (NOT (OR (NLISTP X) (NLISTP (CDR X))))
                      (PAIRED-COLORS (CDDR X))
                      (ALTERNATING-COLORS X))
                 (PAIRED-COLORS X)),

  which simplifies, opening up the functions NLISTP, OR, ALTERNATING-COLORS,
  OPPOSITE-COLOR, and PAIRED-COLORS, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

AL->PP


(DEFN SILLY
      (X Y Z)
      (IF (NLISTP Z)
          T
          (LIST (SILLY (CDDR X) Y (CDDR Z))
                (SILLY (CDR X) (CDR Y) (CDDR Z))
                (SILLY X (CDDR Y) (CDDR Z)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT Z) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
SILLY is accepted under the principle of definition.  Observe that:
      (OR (TRUEP (SILLY X Y Z))
          (LISTP (SILLY X Y Z)))
is a theorem.




[ 0.0 0.0 0.0 ]

SILLY


(PROVE-LEMMA MAIN
             (REWRITE)
             (IMPLIES (AND (SHUFFLEP X Y Z)
                           (ALTERNATING-COLORS X)
                           (ALTERNATING-COLORS Y)
                           (LISTP X)
                           (LISTP Y)
                           (OPPOSITE-COLOR (CAR X) (CAR Y)))
                      (PAIRED-COLORS Z))
             ((INDUCT (SILLY X Y Z))))

WARNING:  Note that MAIN contains the free variables Y and X which will be
chosen by instantiating the hypothesis (SHUFFLEP X Y Z).


This formula can be simplified, using the abbreviations IMPLIES, NLISTP, NOT,
OR, and AND, to the following two new formulas:

Case 2. (IMPLIES (AND (NOT (LISTP Z))
                      (SHUFFLEP X Y Z)
                      (ALTERNATING-COLORS X)
                      (ALTERNATING-COLORS Y)
                      (LISTP X)
                      (LISTP Y)
                      (OPPOSITE-COLOR (CAR X) (CAR Y)))
                 (PAIRED-COLORS Z)).

  This simplifies, expanding the definition of SHUFFLEP, to:

        T.

Case 1. (IMPLIES (AND (LISTP Z)
                      (IMPLIES (AND (SHUFFLEP X (CDDR Y) (CDDR Z))
                                    (ALTERNATING-COLORS X)
                                    (ALTERNATING-COLORS (CDDR Y))
                                    (LISTP X)
                                    (LISTP (CDDR Y))
                                    (OPPOSITE-COLOR (CAR X) (CADDR Y)))
                               (PAIRED-COLORS (CDDR Z)))
                      (IMPLIES (AND (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                                    (ALTERNATING-COLORS (CDR X))
                                    (ALTERNATING-COLORS (CDR Y))
                                    (LISTP (CDR X))
                                    (LISTP (CDR Y))
                                    (OPPOSITE-COLOR (CADR X) (CADR Y)))
                               (PAIRED-COLORS (CDDR Z)))
                      (IMPLIES (AND (SHUFFLEP (CDDR X) Y (CDDR Z))
                                    (ALTERNATING-COLORS (CDDR X))
                                    (ALTERNATING-COLORS Y)
                                    (LISTP (CDDR X))
                                    (LISTP Y)
                                    (OPPOSITE-COLOR (CADDR X) (CAR Y)))
                               (PAIRED-COLORS (CDDR Z)))
                      (SHUFFLEP X Y Z)
                      (ALTERNATING-COLORS X)
                      (ALTERNATING-COLORS Y)
                      (LISTP X)
                      (LISTP Y)
                      (OPPOSITE-COLOR (CAR X) (CAR Y)))
                 (PAIRED-COLORS Z)).

  This simplifies, applying AL->PP and CDR-NLISTP, and unfolding the
  definitions of OPPOSITE-COLOR, ALTERNATING-COLORS, AND, IMPLIES, SHUFFLEP,
  PLISTP, PAIRED-COLORS, LISTP, EQUAL, CAR, and NUMBERP, to 572 new
  conjectures:

  Case 1.572.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP, and opening up the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.571.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and unfolding the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.570.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and unfolding the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.569.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and unfolding the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.568.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and opening up CAR, NUMBERP,
    and LISTP, to:

          T.

  Case 1.567.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, appealing to the lemma CDR-NLISTP, and
    opening up the functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.566.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CDR-NLISTP, and unfolding the definitions
    of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.565.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP, and unfolding the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.564.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and expanding CAR,
    NUMBERP, and LISTP, to:

          T.

  Case 1.563.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and opening up the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.562.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and opening up the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.561.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying the lemma CDR-NLISTP, and unfolding
    the definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.560.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP, and opening up the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.559.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, appealing to the lemma CDR-NLISTP, and
    expanding the functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.558.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP, and unfolding CAR,
    NUMBERP, and LISTP, to:

          T.

  Case 1.557.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and opening up CAR, NUMBERP,
    and LISTP, to:

          T.

  Case 1.556.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CDR-NLISTP, and opening up the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.555.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and unfolding the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.554.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying the lemma CDR-NLISTP, and unfolding the
    functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.553.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP, and expanding the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.552.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CDR-NLISTP, and expanding the
    definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.551.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying the lemma CDR-NLISTP, and
    expanding the functions CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.550.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CDR-NLISTP, and unfolding the functions
    CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.549.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying the lemma CDR-NLISTP, and
    unfolding the definitions of CAR, NUMBERP, and LISTP, to:

          T.

  Case 1.548.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    opening up the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.547.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    unfolding the functions NUMBERP and LISTP, to:

          T.

  Case 1.546.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP,
    and opening up the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.545.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and
    expanding the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.544.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, appealing to the lemmas CAR-NLISTP and
    CDR-NLISTP, and unfolding NUMBERP and LISTP, to:

          T.

  Case 1.543.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP and CDR-NLISTP, and unfolding
    the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.542.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, appealing to the lemmas CAR-NLISTP and CDR-NLISTP,
    and opening up NUMBERP and LISTP, to:

          T.

  Case 1.541.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP, and
    opening up NUMBERP and LISTP, to:

          T.

  Case 1.540.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    opening up NUMBERP and LISTP, to:

          T.

  Case 1.539.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (LISTP (CDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and
    unfolding the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.538.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (LISTP (CDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    opening up the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.537.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (LISTP (CDR Y))
                        (NUMBERP (CADR Y))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and opening
    up NUMBERP and LISTP, to:

          T.

  Case 1.536.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with the lemmas CAR-NLISTP and
    CDR-NLISTP, and opening up the functions NUMBERP and LISTP, to:

          T.

  Case 1.535.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with the lemmas CAR-NLISTP and
    CDR-NLISTP, and opening up the functions NUMBERP and LISTP, to:

          T.

  Case 1.534.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with the lemmas CAR-NLISTP and
    CDR-NLISTP, and opening up the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.533.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP, and
    expanding the functions NUMBERP and LISTP, to:

          T.

  Case 1.532.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    unfolding the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.531.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying the lemmas CAR-NLISTP and
    CDR-NLISTP, and opening up the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.530.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP, and
    expanding the functions NUMBERP and LISTP, to:

          T.

  Case 1.529.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    unfolding the definitions of NUMBERP and LISTP, to:

          T.

  Case 1.528.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (LISTP (CDDR X))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CAR-NLISTP and CDR-NLISTP, and unfolding
    NUMBERP and LISTP, to:

          T.

  Case 1.527.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with the lemmas CAR-NLISTP and
    CDR-NLISTP, and expanding the functions NUMBERP, PLISTP, SHUFFLEP, and CAR,
    to:

          T.

  Case 1.526.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP, and expanding the function
    NUMBERP, to:

          T.

  Case 1.525.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP,
    and unfolding the functions NUMBERP, PLISTP, SHUFFLEP, and CAR, to:

          T.

  Case 1.524.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, appealing to the lemma CAR-NLISTP, and
    expanding NUMBERP, to:

          T.

  Case 1.523.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, appealing to the lemmas CDR-NLISTP and CAR-NLISTP,
    and unfolding the functions CAR, NUMBERP, PLISTP, and SHUFFLEP, to:

          T.

  Case 1.522.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP, and unfolding the function
    NUMBERP, to:

          T.

  Case 1.521.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP, CDR-NLISTP, and AL->PP,
    and unfolding the functions NUMBERP, PLISTP, SHUFFLEP, EQUAL, LISTP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.520.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CAR-NLISTP and AL->PP, and opening
    up NUMBERP, PLISTP, SHUFFLEP, LISTP, ALTERNATING-COLORS, OPPOSITE-COLOR,
    and CAR, to:

          T.

  Case 1.519.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP and AL->PP, and opening up
    the definitions of NUMBERP, PLISTP, SHUFFLEP, CAR, LISTP,
    ALTERNATING-COLORS, and OPPOSITE-COLOR, to:

          T.

  Case 1.518.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying the lemmas CAR-NLISTP, CDR-NLISTP,
    and AL->PP, and unfolding NUMBERP, PLISTP, SHUFFLEP, EQUAL, LISTP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.517.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP and AL->PP, and expanding the
    functions NUMBERP, PLISTP, SHUFFLEP, LISTP, ALTERNATING-COLORS,
    OPPOSITE-COLOR, and CAR, to:

          T.

  Case 1.516.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CAR-NLISTP and AL->PP, and
    opening up the definitions of NUMBERP, PLISTP, SHUFFLEP, CAR, LISTP,
    ALTERNATING-COLORS, and OPPOSITE-COLOR, to:

          T.

  Case 1.515.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and
    unfolding NUMBERP, PLISTP, SHUFFLEP, and ALTERNATING-COLORS, to:

          T.

  Case 1.514.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying the lemma CAR-NLISTP, and unfolding
    the definitions of NUMBERP and ALTERNATING-COLORS, to:

          T.

  Case 1.513.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP and CDR-NLISTP, and opening up
    the definitions of NUMBERP, PLISTP, SHUFFLEP, and ALTERNATING-COLORS, to:

          T.

  Case 1.512.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CAR-NLISTP, and expanding the functions
    NUMBERP and ALTERNATING-COLORS, to:

          T.

  Case 1.511.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP, and expanding the
    definitions of CAR, NUMBERP, PLISTP, SHUFFLEP, and ALTERNATING-COLORS, to:

          T.

  Case 1.510.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CAR-NLISTP, and unfolding the
    definitions of NUMBERP and ALTERNATING-COLORS, to:

          T.

  Case 1.509.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CAR-NLISTP, CDR-NLISTP, and AL->PP,
    and expanding the functions NUMBERP, PLISTP, SHUFFLEP, LISTP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.508.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CAR-NLISTP and AL->PP, and
    expanding NUMBERP, PLISTP, SHUFFLEP, LISTP, ALTERNATING-COLORS,
    OPPOSITE-COLOR, and CAR, to:

          T.

  Case 1.507.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, appealing to the lemmas CAR-NLISTP, CDR-NLISTP, and
    AL->PP, and opening up NUMBERP, PLISTP, SHUFFLEP, LISTP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.506.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (SHUFFLEP (CDR X) (CDR Y) (CDDR Z)))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying the lemmas CAR-NLISTP and AL->PP, and
    expanding the definitions of NUMBERP, PLISTP, SHUFFLEP, LISTP,
    ALTERNATING-COLORS, OPPOSITE-COLOR, and CAR, to:

          T.

  Case 1.505.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (LISTP (CDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP and AL->PP, and expanding
    NUMBERP, PLISTP, SHUFFLEP, LISTP, and ALTERNATING-COLORS, to:

          T.

  Case 1.504.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (LISTP (CDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CAR-NLISTP and AL->PP, and
    expanding the definitions of NUMBERP, PLISTP, SHUFFLEP, LISTP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.503.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (LISTP (CDR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP and CAR-NLISTP, and
    expanding CAR and NUMBERP, to:

          T.

  Case 1.502.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (LISTP (CDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (LISTP (CDDR X)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and expanding the
    definitions of CAR, NUMBERP, and ALTERNATING-COLORS, to:

          T.

  Case 1.501.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP and CAR-NLISTP, and expanding
    CAR and NUMBERP, to:

          T.

  Case 1.500.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    unfolding the definitions of CAR and NUMBERP, to:

          T.

  Case 1.499.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    expanding the definitions of CAR and NUMBERP, to:

          T.

  Case 1.498.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with the lemmas CDR-NLISTP and
    CAR-NLISTP, and unfolding CAR and NUMBERP, to:

          T.

  Case 1.497.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    opening up the functions CAR and NUMBERP, to:

          T.

  Case 1.496.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    expanding the functions CAR and NUMBERP, to:

          T.

  Case 1.495.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADDR X))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying the lemmas CDR-NLISTP and CAR-NLISTP,
    and expanding the functions CAR and NUMBERP, to:

          T.

  Case 1.494.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, appealing to the lemmas CDR-NLISTP and CAR-NLISTP,
    and unfolding CAR and NUMBERP, to:

          T.

  Case 1.493.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with the lemmas CDR-NLISTP and
    CAR-NLISTP, and expanding the functions CAR and NUMBERP, to:

          T.

  Case 1.492.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying the lemmas CDR-NLISTP and CAR-NLISTP, and
    opening up the definitions of CAR and NUMBERP, to:

          T.

  Case 1.491.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    opening up the functions CAR and NUMBERP, to:

          T.

  Case 1.490.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NOT (NUMBERP (CADR X)))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NOT (NUMBERP (CAR Y))))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
    opening up the functions CAR and NUMBERP, to:

          T.

  Case 1.489.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and opening
    up the functions NUMBERP and CAR, to:

          T.

  Case 1.488.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and
    expanding the functions NUMBERP and CAR, to:

          T.

  Case 1.487.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CAR-NLISTP and CDR-NLISTP, and unfolding
    the definitions of NUMBERP and CAR, to:

          T.

  Case 1.486.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CAR-NLISTP, CDR-NLISTP, and
    AL->PP, and expanding the definitions of NUMBERP, EQUAL, LISTP, SHUFFLEP,
    PLISTP, and ALTERNATING-COLORS, to:

          T.

  Case 1.485.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CAR-NLISTP, CDR-NLISTP, and
    AL->PP, and expanding the functions NUMBERP, EQUAL, LISTP, SHUFFLEP,
    PLISTP, and ALTERNATING-COLORS, to:

          T.

  Case 1.484.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CAR-NLISTP, CDR-NLISTP, and
    AL->PP, and opening up the definitions of NUMBERP, EQUAL, LISTP, SHUFFLEP,
    PLISTP, and ALTERNATING-COLORS, to:

          T.

  Case 1.483.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, appealing to the lemmas CAR-NLISTP and
    CDR-NLISTP, and opening up the definitions of NUMBERP and
    ALTERNATING-COLORS, to:

          T.

  Case 1.482.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CAR-NLISTP and CDR-NLISTP, and unfolding
    NUMBERP and ALTERNATING-COLORS, to:

          T.

  Case 1.481.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP, and
    opening up the functions NUMBERP and ALTERNATING-COLORS, to:

          T.

  Case 1.480.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, appealing to the lemmas CAR-NLISTP, CDR-NLISTP,
    and AL->PP, and expanding NUMBERP, LISTP, PLISTP, SHUFFLEP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.479.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (EQUAL (CADR Y) (CAR X))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CAR-NLISTP, CDR-NLISTP, and AL->PP,
    and opening up the definitions of NUMBERP, LISTP, PLISTP, SHUFFLEP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.478.
          (IMPLIES (AND (LISTP Z)
                        (NUMBERP (CAR X))
                        (NUMBERP (CADDR Y))
                        (NUMBERP (CADR X))
                        (NUMBERP (CADR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (EQUAL (CAR X) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NOT (NUMBERP (CAR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CAR-NLISTP, CDR-NLISTP, and AL->PP, and
    unfolding the functions NUMBERP, LISTP, PLISTP, SHUFFLEP, and
    ALTERNATING-COLORS, to:

          T.

  Case 1.477.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and expanding the
    definitions of CAR and NUMBERP, to:

          T.

  Case 1.476.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and expanding CAR
    and NUMBERP, to:

          T.

  Case 1.475.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and opening up the definitions
    of CAR and NUMBERP, to:

          T.

  Case 1.474.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and unfolding CAR and
    NUMBERP, to:

          T.

  Case 1.473.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with the lemma CDR-NLISTP, and
    expanding CAR and NUMBERP, to:

          T.

  Case 1.472.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (NUMBERP (CADDR X)))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with the lemma CDR-NLISTP, and unfolding
    the functions CAR and NUMBERP, to:

          T.

  Case 1.471.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CDR-NLISTP, and opening up CAR and
    NUMBERP, to:

          T.

  Case 1.470.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and opening up the
    functions CAR and NUMBERP, to:

          T.

  Case 1.469.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, rewriting with CDR-NLISTP, and expanding
    CAR and NUMBERP, to:

          T.

  Case 1.468.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP, and unfolding the
    functions CAR and NUMBERP, to:

          T.

  Case 1.467.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and unfolding the
    functions CAR and NUMBERP, to:

          T.

  Case 1.466.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (ALTERNATING-COLORS (CDDR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and opening up CAR and
    NUMBERP, to:

          T.

  Case 1.465.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying CDR-NLISTP, and unfolding CAR and
    NUMBERP, to:

          T.

  Case 1.464.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CDR-NLISTP, and unfolding CAR and
    NUMBERP, to:

          T.

  Case 1.463.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NUMBERP (CADDR X))
                        (NUMBERP (CAR Y))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and opening up the definitions
    of CAR and NUMBERP, to:

          T.

  Case 1.462.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (NUMBERP (CADDR X)))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with CDR-NLISTP, and opening up the
    definitions of CAR and NUMBERP, to:

          T.

  Case 1.461.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    However this again simplifies, applying CDR-NLISTP, and unfolding the
    definitions of CAR and NUMBERP, to:

          T.

  Case 1.460.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (NUMBERP (CADDR X)))
                        (ALTERNATING-COLORS (CDDR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying the lemma CDR-NLISTP, and opening up
    CAR and NUMBERP, to:

          T.

  Case 1.459.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (SHUFFLEP (CDDR X) Y (CDDR Z)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, applying CDR-NLISTP, and expanding CAR and NUMBERP,
    to:

          T.

  Case 1.458.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (SHUFFLEP (CDDR X) Y (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, rewriting with CDR-NLISTP, and expanding the
    functions CAR and NUMBERP, to:

          T.

  Case 1.457.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, rewriting with the lemma CDR-NLISTP, and
    unfolding the functions CAR and NUMBERP, to:

          T.

  Case 1.456.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDDR X)))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))),

    which again simplifies, rewriting with CDR-NLISTP, and opening up the
    definitions of CAR and NUMBERP, to:

          T.

  Case 1.455.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (EQUAL (CADR X) (CADR Z))
                        (EQUAL (CAR Y) (CADR X))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CAR Y))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and expanding the definitions
    of CAR and NUMBERP, to:

          T.

  Case 1.454.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (LISTP (CDDR X)))
                        (EQUAL (CAR X) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR X))
                        (NOT (EQUAL (CADR X) (CADR Z)))
                        (EQUAL (CAR Y) (CADR Z))
                        (SHUFFLEP (CDR X) (CDR Y) (CDDR Z))
                        (NUMBERP (CADR X))
                        (NOT (LISTP (CDR Y)))
                        (LISTP X)
                        (LISTP Y)
                        (NUMBERP (CAR Y)))
                   (PAIRED-COLORS (CDDR Z))).

    This again simplifies, applying CDR-NLISTP, and opening up the functions
    CAR and NUMBERP, to:

          T.

  Case 1.453.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))
                        (LISTP (CDR Z))
                        (LISTP (CDR Y))
                        (NOT (EQUAL (CAR X) (CADR Z)))
                        (EQUAL (CADR Y) (CADR Z))
                        (SHUFFLEP X (CDDR Y) (CDDR Z))
                        (NOT (LISTP (CDR X)))
                        (NUMBERP (CAR Y))
                        (NOT (NUMBERP (CADR Y)))
                        (NOT (LISTP (CDDR Y)))
                        (LISTP X)
                        (LISTP Y))
                   (PAIRED-COLORS (CDDR Z))).

    But this again simplifies, applying the lemma CAR-NLISTP, and expanding
    the definition of NUMBERP, to:

          T.

  Case 1.452.
          (IMPLIES (AND (LISTP Z)
                        (NOT (NUMBERP (CAR X)))
                        (NOT (NUMBERP (CADDR Y)))
                        (LISTP (CDDR X))
                        (NOT (ALTERNATING-COLORS (CDDR X)))
                        (NOT (EQUAL (CAR X) (CAR Z)))
                        (EQUAL (CAR Y) (CAR Z))