-------------------------------------------------------------------------------
Domain ALG = General Algebra (2 abstract problems, 4 problems)
-------------------------------------------------------------------------------
ALG001=CmpsnHomoms  (3) The composition of homomorphisms is a homomorphism
ALG002=OrdField     (1) In an ordered field, if X > 0 then X^-1 > 0
-------------------------------------------------------------------------------
Domain ANA = Analysis (5 abstract problems, 19 problems)
-------------------------------------------------------------------------------
ANA001=MinVal       (1) Attaining minimum (or maximum) value
ANA002=IntmedVal    (4) Intermediate value theorem
ANA003=SumContFuncLem1  (4) Lemma 1 for the sum of two continuous functions is continuous
ANA004=SumContFuncLem2  (5) Lemma 2 for the sum of two continuous functions is continuous
ANA005=SumContFunc  (5) The sum of two continuous functions is continuous
-------------------------------------------------------------------------------
Domain BOO = Boolean Algebra (19 abstract problems, 52 problems)
-------------------------------------------------------------------------------
BOO001=B3InvIvln    (1) In B3 algebra, inverse is an involution
BOO002=B3LId        (2) In B3 algebra, X * X^-1 * Y = Y
BOO003=MultIdem     (3) Multiplication is idempotent (X * X = X)
BOO004=AddIdem      (3) Addition is idempotent (X + X = X)
BOO005=AddBnd       (3) Addition is bounded (X + 1 = 1)
BOO006=MultBnd      (3) Multiplication is bounded (X * 0 = 0)
BOO007=ProdAssc     (3) Product is associative ( (X * Y) * Z = X * (Y * Z) )
BOO008=SumAssc      (4) Sum is associative ( (X + Y) + Z = X + (Y + Z) )
BOO009=MultAbsb     (3) Multiplication absorption (X * (X + Y) = X)
BOO010=AddAbsb      (3) Addition absorbtion (X + (X * Y) = X)
BOO011=InvAId       (3) Inverse of additive identity = Multiplicative identity
BOO012=InvIvln      (4) Inverse is an involution
BOO013=InvUnq       (4) The inverse of X is unique
BOO014=DeMorgan1    (4) DeMorgan for inverse and product (X+Y)^-1 = (X^-1) * (Y^-1)
BOO015=DeMorgan2    (3) DeMorgan for inverse and sum (X^-1 + Y^-1) = (X * Y)^-1
BOO016=ProdSum      (2) Relating product and sum (X * Y = Z -> X + Z = X)
BOO017=SumProd      (2) Relating sum and product (X + Y = Z -> X * Z = X)
BOO018=InvMId       (1) Inverse of multiplicative identity = Additive identity
BOO019=IndpAx       (1) Prove the independance of Ternary Boolean algebra axiom
-------------------------------------------------------------------------------
Domain CAT = Category Theory (20 abstract problems, 58 problems)
-------------------------------------------------------------------------------
CAT001=Monom1       (4) XY monomorphism => Y monomorphism
CAT002=Monom2       (4) X and Y monomorphisms, XY well-defined => XY monomorphism
CAT003=Epim1        (4) XY epimorphism => X epimorphism
CAT004=Epim2        (4) X and Y epimorphisms, XY well-defined => XY epimorphism
CAT005=DomUnqRId    (3) Domain is the unique right identity
CAT006=CodUnqLId    (3) Codomain is the unique left identity
CAT007=DomEqCod     (2) If domain(x) = codomain(y) then xy is defined
CAT008=DomXCodY     (1) If xy is defined then domain(x) = codomain(y)
CAT009=DomXYDomY    (3) If xy is defined, then domain(xy) = domain(y)
CAT010=CodXYCodX    (2) If xy is defined, then codomain(xy) = codomain(x)
CAT011=DomIdem      (4) domain(domain(x)) = domain(x)
CAT012=CodOfDom     (3) codomain(domain(x)) = domain(x)
CAT013=DomOfCod     (3) domain(codomain(x)) = codomain(x)
CAT014=CodIdem      (4) codomain(codomain(x)) = codomain(x)
CAT015=Exist        (2) Prove something exists
CAT016=DomEx        (2) If x exists, then domain(x) exists
CAT017=CodEx        (2) If x exists, then codomain(x) exists
CAT018=FactEx       (3) If xy and yz exist, then so does x(yz)
CAT019=Indisc       (5) Axiom of Indiscernibles
-------------------------------------------------------------------------------
Domain CID = Circuit Design (3 abstract problems, 4 problems)
-------------------------------------------------------------------------------
CID001=OrNand       (1) Design an OR gate using NAND gates
CID002=Intchg       (1) Interchange inputs to outputs
CID003=TwoInv       (2) Invert 3 inputs with 2 not gates
-------------------------------------------------------------------------------
Domain CIV = Circuit Verification (4 abstract problems, 4 problems)
-------------------------------------------------------------------------------
CIV001=Intchg       (1) Interchange inputs to outputs
CIV002=TwoInv       (1) Invert 3 inputs with 2 not gates
CIV003=Adder1       (1) One bit Full Adder
CIV004=Adder2       (1) Two bit Full Adder
-------------------------------------------------------------------------------
Domain COL = Combinatory Logic (81 abstract problems, 141 problems)
-------------------------------------------------------------------------------
COL001=WkFxdPtSK    (2) Weak fixed point for S and K
COL002=WkFxdPtSBCI  (3) Weak fixed point for S, B, C, and I
COL003=StrongFxdPtBW    (10) Strong fixed point for B and W
COL004=SK_U         (3) Find combinator equivalent to U from S and K
COL005=SWModel      (1) Find a model for S and W but not a weak fixed point
COL006=StrongFxdPtSK    (4) Strong fixed point for S and K
COL007=WkFxdPtL     (1) Weak fixed point for L
COL008=WkFxdPtMB    (1) Weak fixed point for M and B
COL009=WkFxdPtBL2   (1) Weak fixed point for B and L2
COL010=WkFxdPtBS2   (1) Weak fixed point for B and S2
COL011=WkFxdPtOQ1   (1) Weak fixed point for O and Q1
COL012=WkFxdPtU     (1) Weak fixed point for U
COL013=WkFxdPtSL    (1) Weak fixed point for S and L
COL014=WkFxdPtLO    (1) Weak fixed point for L and O
COL015=WkFxdPtQM    (1) Weak fixed point for Q and M
COL016=WkFxdPtBML   (1) Weak fixed point for B, M and L
COL017=WkFxdPtBMT   (1) Weak fixed point for B, M, and T
COL018=WkFxdPtWQL   (1) Weak fixed point for W, Q, and L
COL019=WkFxdPtBST   (1) Weak fixed point for B, S, and T
COL020=WkFxdPtBSC   (1) Weak fixed point for B, S, and C
COL021=WkFxdPtBMV   (1) Weak fixed point for B, M, and V
COL022=WkFxdPtBOM   (1) Weak fixed point for B, O, and M
COL023=WkFxdPtBN    (1) Weak fixed point for B and N
COL024=WkFxdPtBMC   (1) Weak fixed point for B, M, and C
COL025=WkFxdPtBW    (1) Weak fixed point for B and W
COL026=WkFxdPtBW1   (1) Weak fixed point for B and W1
COL027=WkFxdPtBH    (1) Weak fixed point for B and H
COL028=WkFxdPtBN    (1) Weak fixed point for B and N
COL029=StrongFxdPtU (1) Strong fixed point for U
COL030=StrongFxdPtSL    (1) Strong fixed point for S and L
COL031=StrongFxdPtLO    (1) Strong fixed point for L and O
COL032=StrongFxdPtQM    (1) Strong fixed point for Q and M
COL033=StrongFxdPtBML   (1) Strong fixed point for B, M and L
COL034=StrongFxdPtBMT   (1) Strong fixed point for B, M, and T
COL035=StrongFxdPtWQL   (1) Strong fixed point for W, Q, and L
COL036=StrongFxdPtBST   (1) Strong fixed point for B, S, and T
COL037=StrongFxdPtBSC   (1) Strong fixed point for B, S, and C
COL038=StrongFxdPtBMV   (1) Strong fixed point for B, M, and V
COL039=StrongFxdPtBOM   (1) Strong fixed point for B, O, and M
COL040=StrongFxdPtBN    (1) Strong fixed point for B and N
COL041=StrongFxdPtBMC   (1) Strong fixed point for B, M, and C
COL042=StrongFxdPtBW1   (5) Strong fixed point for B and W1
COL043=StrongFxdPtBH    (2) Strong fixed point for B and H
COL044=StrongFxdPtBN    (5) Strong fixed point for B and N
COL045=WkFxdPtBMS   (1) Weak fixed point for B, M and S
COL046=StrongFxdPtBMS   (1) Strong fixed point for B, M and S
COL047=LQModel      (1) Find a model for L and Q but not a strong fixed point
COL048=WkFxdPtBWM   (1) Weak fixed point for B, W, and M
COL049=StrongFxdPtBWM   (1) Strong fixed point for B, W, and M
COL050=MBird01      (1) The Significance of the Mockingbird
COL051=MBird02      (1) Egocentric mocking bird?
COL052=MBird03      (2) A Question on Agreeable Birds
COL053=MBird04      (1) An Exercise in Composition
COL054=MBird05      (1) Compatible Birds
COL055=MBird06      (1) Happy Birds
COL056=MBird07      (1) Normal Birds
COL057=StrongFxdPtSBCI  (1) Strong fixed point for S, B, C, and I
COL058=Lark1        (3) If there's a lark, then there's an egocentric bird.
COL059=Lark2        (1) L3 ((lark lark) lark) is not egocentric.
COL060=BT_Q         (3) Find combinator equivalent to Q from B and T
COL061=BT_Q1        (3) Find combinator equivalent to Q1 from B and T
COL062=BT_C         (3) Find combinator equivalent to C from B and T
COL063=BT_F         (6) Find combinator equivalent to F from B and T
COL064=BT_V         (11) Find combinator equivalent to V from B and T
COL065=BT_G         (1) Find combinator equivalent to G from B and T
COL066=BQW_P        (3) Find combinator equivalent to P from B, Q and W
COL067=StrongFxdPtBS    (1) Strong fixed point for B and S
COL068=WeakFxdPtBS  (1) Weak fixed point for B and S
COL069=StrongFxdPtBL    (1) Strong fixed point for B and L
COL070=WeakFxdPtBN1 (1) Weak fixed point for B and N1
COL071=StrongFxdPtNQ    (1) Strong fixed point for N and Q
COL072=StrongFxdPtBL    (1) Strong fixed point for B and L
COL073=StrongFxdPtBN1   (1) Strong fixed point for B and N1
COL074=UnSatTRC     (3) Unsatisfiable variant of TRC
COL075=UnSatTRCLem1 (2) Lemma 1 for showing the unsatisfiable variant of TRC
COL076=UnSatTRCLem2 (2) Lemma 2 for showing the unsatisfiable variant of TRC
COL077=TRC1a        (1) Abst Abst Abst Abst Abst Abst = Id
COL078=TRC1b        (2) Abst Abst Abst Abst = k(k(id))
COL079=TRC2a        (2) Abst(Abst(Abst X)) = Abst X
COL080=TRC2b        (2) Abst(Abst k(X)) = k(X)
COL081=TRC2c        (2) Abst k(k(X)) = k(k(X))
-------------------------------------------------------------------------------
Domain COM = Computing Theory (4 abstract problems, 6 problems)
-------------------------------------------------------------------------------
COM001=4StSp        (1) A program correctness theorem
COM002=8StSp        (2) A program correctness theorem
COM003=Halting      (2) The halting problem is undecidable
COM004=Resolution   (1) Part of completeness of resolution
-------------------------------------------------------------------------------
Domain GEO = Geometry (78 abstract problems, 165 problems)
-------------------------------------------------------------------------------
GEO001=BtwnSymm     (4) Betweenness is symmetric in its outer arguments
GEO002=XBtwnXY      (4) For all points x and y, x is between x and y
GEO003=YBtwnXY      (3) For all points x and y, y is between x and y
GEO004=MidPtEx      (2) Every line segment has a midpoint
GEO005=IsosTriEx    (2) Isosceles triangle based on line segment
GEO006=Btwn3Pts     (3) Betweenness for 3 points on a line
GEO007=Btwn4Pts     (3) Betweenness for 4 points on a line
GEO008=Btwn5Pts     (3) Betweenness for 5 points on a line (Five point theorem)
GEO009=1stInrConn   (3) First inner connectivity property of betweenness
GEO010=CollInvar    (3) Collinearity is invariant
GEO011=AxPtsNotColl (5) The axiom set points are not collinear
GEO012=Coll4Pts     (3) Collinearity for 4 points
GEO013=Coll5Pts     (3) Collinearity for 5 points
GEO014=EqidRefl     (1) Ordinary reflexivity of equidistance
GEO015=EqidSymm1    (2) Equidistance is symmetric between its argument pairs
GEO016=EqidSymm2    (2) Equidistance is symmetric within its argument pairs
GEO017=EqidSymmCor1 (2) Corollary 1 to symmetries of equidistance
GEO018=EqidSymmCor2 (2) Corollary 2 to symmetries of equidistance
GEO019=EqidSymmCor3 (2) Corollary 3 to symmetries of equidistance
GEO020=EqidSymmCor4 (2) Corollary 4 to symmetries of equidistance
GEO021=EqidSymmCor5 (2) Corollary 5 to symmetries of equidistance
GEO022=EqidTrans    (2) Ordinary transitivity of equidistance
GEO024=NullSegsCong (2) All null segments are congruent
GEO025=SumEqSeg     (2) Addition of equal segments
GEO026=ExtUnq       (2) Extension is unique
GEO027=ExtUnqCor1   (2) Corollary 1 to unique extension
GEO028=ExtUnqCor2   (2) Corollary 2 to unique extension
GEO029=ExtUnqCor3   (2) Corollary 3 to unique extension
GEO030=Out5SegCor   (2) Corollary to the outer five-segment axiom
GEO031=2ndInr5Seg   (2) Second inner five-segment theorem
GEO032=DiffEqSeg    (2) Equal difference between pairs of equal length line segments
GEO033=1stInr5Seg   (2) First inner five-segment theorem
GEO034=1stInr5SegCor    (2) Corollary to the first inner five-segment theorem
GEO035=NullExt      (2) A null extension does not extend a line
GEO036=AxPtsEx      (2) The 3 axiom set points are distinct
GEO037=ExtSegEx     (2) A segment can be extended
GEO038=SegConsCor1  (2) Corollary 1 to the segment contruction axiom
GEO039=IdBtwnCor    (2) Corollary the identity axiom for betweenness
GEO040=BtwnASym     (2) Antisymmetry of betweenness in its first two arguments
GEO041=BtwnASymCor  (2) Corollary to antisymmetry of betweenness in its first 2 arguments
GEO042=1stBtwnInrTrans  (2) First inner transitivity property of betweenness
GEO043=1stBtwnInrTransCor   (2) Corollary to first inner transitivity property of betweenness
GEO044=1stBtwnOutTrans  (2) First outer transitivity property for betweenness
GEO045=2ndBtwnOutTrans  (2) Second outer transitivity property of betweenness
GEO046=2ndBtwnInrTrans  (2) Second inner transitivity property of betweenness
GEO047=2ndBtwnInrTransCor   (2) Corollary to second inner inner transitivity of betweenness
GEO048=InrPtsTri    (2) Inner points of triangle
GEO049=SimSits      (2) Theorem of similar situations
GEO050=1stBtwnOutConn   (2) First outer connectivity property of betweenness
GEO051=2ndBtwnOutConn   (2) Second outer connectivity property of betweenness
GEO052=2ndBtwnInrConn   (2) Second inner connectivity property of betweenness
GEO053=EndPtUnq     (2) Unique endpoint
GEO054=SegConsCor2  (2) Corollary 2 to the segment construction axiom
GEO055=SegConsCor3  (2) Corollary 3 to the segment construction axiom
GEO056=NullExtCor1  (2) Corollary 1 to null extension
GEO057=NullExtCor2  (2) Corollary 2 of null extension
GEO058=ReflcFixPtUnq    (2) U is the only fixed point of reflection(U,V)
GEO059=DblReflcCong (2) Congruence for double reflection
GEO060=ReflcIvln    (1) Reflection is an involution
GEO061=PtIntsc      (2) Theorem of point insertion
GEO062=IntscId      (2) Insertion identity
GEO063=IntscCong    (2) Insertion respects congruence in its last two arguments
GEO064=CollCor1     (2) Corollary 1 to collinearity
GEO065=CollCor2     (2) Corollary 2 to collinearity
GEO066=CollCor3     (2) Corollary 3 to collinearity
GEO067=2PtsColl     (2) Any two points are collinear
GEO068=CollSimSits  (2) Theorem of similar situations for collinear U, V, W
GEO069=CollEqn3     (2) A property of collinearity
GEO070=PtsNotColl   (2) Non-collinear points in the bisecting diagonal theorem
GEO071=PtsNotCollCor1   (2) Corollary 1 to non-collinear points theorem
GEO072=PtsNotCollCor2   (2) Corollary 2 to non-collinear points theorem
GEO073=DiagBsct     (3) The diagonals of a non-degenerate rectancle bisect
GEO074=OutPasch     (1) Prove the Outer Pasch Axiom
GEO075=EqidRefl     (1) Show reflexivity for equidistance is dependent
GEO076=PtNotOnLines (1) There is no point on every line
GEO077=3PtsNotColl  (1) Three points not collinear if not on line
GEO078=3PlPtsNotColl    (2) Every plane contains 3 noncollinear points
GEO079=AltAngleEq   (1) The alternate interior angles in a trapezoid are equal
-------------------------------------------------------------------------------
Domain GRA = Graph Theory (1 abstract problems, 1 problems)
-------------------------------------------------------------------------------
GRA001=Labels       (1) Clauses from a labelled graph
-------------------------------------------------------------------------------
Domain GRP = Groups (194 abstract problems, 313 problems)
-------------------------------------------------------------------------------
GRP001=SqrComm      (5) X^2 = identity => commutativity
GRP002=O3CmtrEqId   (4) Commutator equals identity in groups of order 3
GRP003=LIdEqRId     (2) The left identity is also a right identity
GRP004=RInvEx       (2) Left inverse and identity => Right inverse exists
GRP005=SubSIdEl     (1) Identity is in this subset of a group
GRP006=InvEl        (1) Inverse is in this group
GRP007=IdUnq        (1) The identity element is unique
GRP008=Unknown      (1) Unknown meaning
GRP009=LInvUnq      (1) The left inverse of an element is unique
GRP010=InvSymm      (2) Inverse is a symmetric relationship
GRP011=LCanc        (1) Left cancellation
GRP012=InvOfProd    (4) Inverse of products = Product of inverses
GRP013=CmtrEqId     (1) Commutator equals identity in these conditions
GRP014=ProdAssc     (1) Product is associative in this group theory
GRP015=GroupEx      (1) x,<<x x,X> x,X> is a group
GRP016=ReflHomom    (1) There is a homomorphism from a group to itself
GRP017=InvUnq       (1) The inverse of each element is unique
GRP018=XTimesId     (1) X times identity is X
GRP019=IdTimesX     (1) Identity times X is X
GRP020=InvXTimesX   (1) Inverse of X times X is the identity
GRP021=XTimesInvX   (1) X times inverse of X is the identity
GRP022=InvIvln      (2) Inverse is an involution
GRP023=InvOfId      (2) The inverse of the identity is the identity
GRP024=CmtrAssc     (1) Associativity of commutator
GRP025=O2Isom       (4) All groups of order 2 are isomorphic
GRP026=O3Isom       (4) All groups of order 3 are isomorphic
GRP027=O5Cyclic     (2) All groups of order 5 are cyclic
GRP028=SemiGRIdEx1  (3) In semigroups, left and right solutions => right id exists
GRP029=SemiGRIdEx2  (2) In semigroups, left id and inverse => right id exists
GRP030=SemiGLIdEqRId    (1) In semigroups, left id and inverse => left id=right id
GRP031=SemiGRInvEx  (2) In semigroups, left inverse and id => right inverse exists
GRP032=SubGIdEx     (1) In subgroups, there is an identity
GRP033=SubGGrpIdEx  (2) In subgroups, the identity is the group identity
GRP034=SubGInvClsd  (2) In subgroups, inverse is closed
GRP035=SubGProdClsd (1) In subgroups, product is closed
GRP036=SubGIdUnq    (1) In subgroups, the identity element is unique
GRP037=SubGInvUnq   (1) In subgroups, the inverse of an element is unique
GRP038=SubGGrpEl    (1) In subgroups, if a and b are members, then a.b^-1 is a member
GRP039=SubGI2Norm   (7) Subgroups of index 2 are normal
GRP040=SubGO2InvIvln    (2) In subgroups of order 2, inverse is an involution
GRP041=EqRefl       (1) Reflexivity is dependent
GRP042=EqSymm       (1) Symmetry is dependent
GRP043=EqTrans      (1) Transitivity is dependent
GRP044=ProdSubs1    (1) Product subsitution 1 is dependent
GRP045=ProdSubs2    (1) Product subsitution 2 is dependent
GRP046=MultSubs1    (1) Multiply substitution 1 is dependent
GRP047=MultSubs2    (1) Multiply substitution 2 is dependent
GRP048=InvSubs      (1) Inverse substitution is dependent
GRP049=ProdInvAx1   (1) Single axiom for group theory, in product & inverse
GRP050=ProdInvAx2   (1) Single axiom for group theory, in product & inverse
GRP051=ProdInvAx3   (1) Single axiom for group theory, in product & inverse
GRP052=ProdInvAx4   (1) Single axiom for group theory, in product & inverse
GRP053=ProdInvAx5   (1) Single axiom for group theory, in product & inverse
GRP054=ProdInvAx6   (1) Single axiom for group theory, in product & inverse
GRP055=ProdInvAx7   (1) Single axiom for group theory, in product & inverse
GRP056=ProdInvAx8   (1) Single axiom for group theory, in product & inverse
GRP057=ProdInvAx9   (1) Single axiom for group theory, in product & inverse
GRP058=ProdInvAx10  (1) Single axiom for group theory, in product & inverse
GRP059=ProdInvAx11  (1) Single axiom for group theory, in product & inverse
GRP060=ProdInvAx12  (1) Single axiom for group theory, in product & inverse
GRP061=ProdInvAx13  (1) Single axiom for group theory, in product & inverse
GRP062=ProdInvAx14  (1) Single axiom for group theory, in product & inverse
GRP063=DivAx1       (1) Single axiom for group theory, in division
GRP064=DivAx2       (1) Single axiom for group theory, in division
GRP065=DivAx3       (1) Single axiom for group theory, in division
GRP066=DivIdAx1     (1) Single axiom for group theory, in division and identity
GRP067=DivIdAx2     (1) Single axiom for group theory, in division and identity
GRP068=DivIdAx3     (1) Single axiom for group theory, in division and identity
GRP069=DivIdAx4     (1) Single axiom for group theory, in division and identity
GRP070=DivInvAx1    (1) Single axiom for group theory, in division and inverse
GRP071=DivInvAx2    (1) Single axiom for group theory, in division and inverse
GRP072=DivInvAx3    (1) Single axiom for group theory, in division and inverse
GRP073=DivInvAx4    (1) Single axiom for group theory, in division and inverse
GRP074=DivInvAx5    (1) Single axiom for group theory, in division and inverse
GRP075=DblDivIdAx1  (1) Single axiom for group theory, in double division and identity
GRP076=DblDivIdAx2  (1) Single axiom for group theory, in double division and identity
GRP077=DblDivIdAx3  (1) Single axiom for group theory, in double division and identity
GRP078=DblDivIdAx4  (1) Single axiom for group theory, in double division and identity
GRP079=DblDivIdAx5  (1) Single axiom for group theory, in double division and identity
GRP080=DblDivIdAx6  (1) Single axiom for group theory, in double division and identity
GRP081=DblDivInvAx1 (1) Single axiom for group theory, in double division and inverse
GRP082=DblDivInvAx2 (1) Single axiom for group theory, in double division and inverse
GRP083=DblDivInvAx3 (1) Single axiom for group theory, in double division and inverse
GRP084=ProdInvAbnAx1    (1) Single axiom for Abelian group theory, in product and inverse
GRP085=ProdInvAbnAx2    (1) Single axiom for Abelian group theory, in product and inverse
GRP086=ProdInvAbnAx3    (1) Single axiom for Abelian group theory, in product and inverse
GRP087=ProdInvAbnAx4    (1) Single axiom for Abelian group theory, in product and inverse
GRP088=DivAbnAx1    (1) Single axiom for Abelian group theory, in division
GRP089=DivAbnAx2    (1) Single axiom for Abelian group theory, in division
GRP090=DivAbnAx3    (1) Single axiom for Abelian group theory, in division
GRP091=DivAbnAx4    (1) Single axiom for Abelian group theory, in division
GRP092=DivAbnAx5    (1) Single axiom for Abelian group theory, in division
GRP093=DivIdAbnAx1  (1) Single axiom for Abelian group theory, in division and identity
GRP094=DivIdAbnAx2  (1) Single axiom for Abelian group theory, in division and identity
GRP095=DivIdAbnAx3  (1) Single axiom for Abelian group theory, in division and identity
GRP096=DivInvAbnAx1 (1) Single axiom for Abelian group theory, in division and inverse
GRP097=DivInvAbnAx2 (1) Single axiom for Abelian group theory, in division and inverse
GRP098=DivInvAbnAx3 (1) Single axiom for Abelian group theory, in division and inverse
GRP099=DblDivIdAbnAx1   (1) Single axiom for Abelian group theory, in double div and id
GRP100=DblDivIdAbnAx2   (1) Single axiom for Abelian group theory, in double div and id
GRP101=DblDivIdAbnAx3   (1) Single axiom for Abelian group theory, in double div and id
GRP102=DblDivIdAbnAx4   (1) Single axiom for Abelian group theory, in double div and id
GRP103=DblDivIdAbnAx5   (1) Single axiom for Abelian group theory, in double div and id
GRP104=DblDivInvAbnAx1  (1) Single axiom for Abelian group theory, in double div and inv
GRP105=DblDivInvAbnAx2  (1) Single axiom for Abelian group theory, in double div and inv
GRP106=DblDivInvAbnAx3  (1) Single axiom for Abelian group theory, in double div and inv
GRP107=DblDivInvAbnAx4  (1) Single axiom for Abelian group theory, in double div and inv
GRP108=DblDivInvAbnAx5  (1) Single axiom for Abelian group theory, in double div and inv
GRP109=DblDivInvAbnAx6  (1) Single axiom for Abelian group theory, in double div and inv
GRP110=DblDivInvAbnAx7  (1) Single axiom for Abelian group theory, in double div and inv
GRP111=DblDivInvAbnAx8  (1) Single axiom for Abelian group theory, in double div and inv
GRP112=ProdInvAx15  (1) Single axiom for group theory, in product & inverse
GRP113=O4Eqn        (1) Lemma for proving all groups of order 4 are cyclic
GRP114=PosTimesNeg  (1) Product of positive and negative parts of X equals X
GRP115=O3AxO3       (1) Derive order 3 from a single axiom for groups order 3
GRP116=O3AxLId      (1) Derive left identity from a single axiom for groups order 3
GRP117=O3AxRId      (1) Derive right identity from a single axiom for groups order 3
GRP118=O3AxAssoc    (1) Derive associativity from a single axiom for groups order 3
GRP119=O4AxO4       (1) Derive order 4 from a single axiom for groups order 4
GRP120=O4AxLId      (1) Derive left identity from a single axiom for groups order 4
GRP121=O4AxRId      (1) Derive right identity from a single axiom for groups order 4
GRP122=O4AxAssoc    (1) Derive associativity from a single axiom for groups order 4
GRP123=321COILS     (8) (3,2,1) conjugate orthogonality
GRP124=312COILS     (8) (3,1,2) conjugate orthogonality
GRP125=Schroeder    (4) (a.b).(b.a) = a
GRP126=SteinLaw3    (4) (a.b).(b.a) = b
GRP127=QG5          (4) ((b.a).b).b) = a
GRP128=SchroederLaw1    (4) (a.b).b = a.(a.b)
GRP129=QG7          (4) a.(b.a) = (b.a).b
GRP130=QG8          (4) (a.(a.b)).b = a
GRP131=321COILSNoIdem   (2) (3,2,1) conjugate orthogonality, no idempotence
GRP132=312COILSNoIdem   (2) (3,1,2) conjugate orthogonality, no idempotence
GRP133=SchroederNoIdem  (2) (a.b).(b.a) = a, no idempotence
GRP134=SteinLaw3NoIdem  (2) (a.b).(b.a) = b, no idempotence
GRP135=QG5NoIdem    (2) ((b.a).b).b) = a, no idempotence
GRP136=ASymLub      (1) Prove anti-symmetry axiom using the LUB transformation
GRP137=ASymGlb      (1) Prove anti-symmetry axiom using the GLB transformation
GRP138=Glb1Lub      (1) Prove greatest lower-bound axiom using the LUB transformation
GRP139=Glb1Glb      (1) Prove greatest lower-bound axiom using the GLB transformation
GRP140=Glb1C        (1) Prove greatest lower-bound axiom using a transformation
GRP141=Glb1D        (1) Prove greatest lower-bound axiom using a transformation
GRP142=Glb2Lub      (1) Prove greatest lower-bound axiom using the LUB transformation
GRP143=Glb2Glb      (1) Prove greatest lower-bound axiom using the GLB transformation
GRP144=Glb3Lub      (1) Prove greatest lower-bound axiom using the LUB transformation
GRP145=Glb3Glb      (1) Prove greatest lower-bound axiom using the GLB transformation
GRP146=Lub1Lub      (1) Prove least upper-bound axiom using the LUB transformation
GRP147=Lub1Glb      (1) Prove least upper-bound axiom using the GLB transformation
GRP148=Lub3C        (1) Prove least upper-bound axiom using a transformation
GRP149=Lub3D        (1) Prove least upper-bound axiom using a transformation
GRP150=Lub2Lub      (1) Prove least upper-bound axiom using the LUB transformation
GRP151=Lub2Glb      (1) Prove least upper-bound axiom using the GLB transformation
GRP152=Lub3Lub      (1) Prove least upper-bound axiom using the LUB transformation
GRP153=Lub3Glb      (1) Prove least upper-bound axiom using the GLB transformation
GRP154=Mono1Lub     (1) Prove monotonicity axiom using the LUB transformation
GRP155=Mono1Glb     (1) Prove monotonicity axiom using the GLB transformation
GRP156=Mono1C       (1) Prove monotonicity axiom using a transformation
GRP157=Mono2Lub     (1) Prove monotonicity axiom using the LUB transformation
GRP158=Mono2Glb     (1) Prove monotonicity axiom using the GLB transformation
GRP159=Mono2C       (1) Prove monotonicity axiom using a transformation
GRP160=ReflLub      (1) Prove reflexivity axiom using the LUB transformation
GRP161=ReflGlb      (1) Prove reflexivity axiom using the GLB transformation
GRP162=TransLub     (1) Prove transitivity axiom using the LUB transformation
GRP163=TransGlb     (1) Prove transitivity axiom using the GLB transformation
GRP164=LOGLattDist  (2) The lattice of each LOG is distributive
GRP165=AppMono      (2) An application of monotonicity
GRP166=MultPosInc   (4) Multiplication with a positive element increases a value
GRP167=ProdPosNeg   (5) Product of positive and negative parts
GRP168=InrGrpAutoM  (2) Inner group automorphisms are order preserving
GRP169=InvRevEq     (2) Inverses reverse inequalities
GRP170=GenMono      (4) General form of monotonicity
GRP171=PosElSemiG   (2) Positive elements form a semigroup
GRP172=NegElSemiG   (2) Negative elements form a semigroup
GRP173=SubGNegEl    (1) Each subgroup of negative elements is trivial
GRP174=SubGPosEl    (1) Each subgroup of positive elements is trivial
GRP175=PosInrAutoM  (4) Positivity is preserved under inner automorphisms
GRP176=GenDist      (2) General form of distributivity
GRP177=LOGMono1     (2) A consequence of monotonicity
GRP178=LOGMono2     (2) A consequence of monotonicity
GRP179=GLBtoLUB     (3) For converting between GLB and LUB
GRP180=GLBtoLUB1    (2) Consequence of converting between GLB and LUB
GRP181=DistLatt     (4) Distributivity of a lattice
GRP182=PosNegId     (4) Positive part of the negative part is identity
GRP183=OrthElSubG   (4) Orthogonal elements form a subgroup with orthogonal parts
GRP184=OrthElComm   (4) Orthogonal elements commute and form a subgroup
GRP185=AppMonoDist  (4) Application of monotonicity and distributivity
GRP186=AppDistGrp   (4) Application of distributivity and group theory
GRP187=OrthElComm   (1) Orthogonal elements commute
GRP188=LOGLatt1     (2) Consequence of lattice theory
GRP189=LOGLatt2     (2) Consequence of lattice theory
GRP190=LOGEst1      (2) Something useful for estimations
GRP191=LOGEst2      (2) Something useful for estimations
GRP192=EvenElGrp    (1) Even elements implies trivial group
GRP193=LOGDistMono  (2) A combination of distributivity and monotonicity
-------------------------------------------------------------------------------
Domain HEN = Henkin Models (12 abstract problems, 64 problems)
-------------------------------------------------------------------------------
HEN001=XDivId       (3) X/identity = zero
HEN002=0DivX        (5) zero/X = zero
HEN003=XDivX        (5) X/X = zero
HEN004=XDiv0        (6) X/zero = X
HEN005=LeTrans      (6) The relation less_equal is transitive
HEN006=Eqn1         (7) X/Y <= Z => X/Z <= Y
HEN007=Eqn2         (6) X <= Y => Z/Y <= Z/X
HEN008=Eqn3         (6) X <= Y => X/Z <= Y/Z
HEN009=IdDivX1      (6) Define X' as identity/X. Then X' = X'''
HEN010=IdDivX2      (7) Define X' as identity/X. Then X' = X'/(identity/X')
HEN011=OpComm       (5) This operation is commutative
HEN012=XLeX         (2) X <= X
-------------------------------------------------------------------------------
Domain LAT = Lattices (5 abstract problems, 10 problems)
-------------------------------------------------------------------------------
LAT001=Eqn1         (1) If X' = U v V and Y' = U ^ V, then U' = X v (Y ^ V)
LAT002=ExEqn1       (1) If X' = U v V and Y' = U ^ V, then U' exists
LAT003=Eqn2         (1) A fairly complex equation to establish
LAT004=Eqn3         (1) A fairly complex equation to establish
LAT005=SAMsLem      (6) SAM's lemma
-------------------------------------------------------------------------------
Domain LCL = Logic Calculi (256 abstract problems, 278 problems)
-------------------------------------------------------------------------------
LCL001=WR_CAM       (1) The Whitehead-Russell system => the Meredith axiom
LCL002=CAM_AN1      (1) AN-CAMerideth => AN-1
LCL003=CAM_AN2      (1) AN-CAMerideth => AN-2
LCL004=CAM_AN3      (1) AN-CAMerideth => AN-3
LCL005=CAM_AN4      (1) AN-CAMerideth => AN-4
LCL006=Wj_EC1       (1) EC-1 depends on the Wajsberg system
LCL007=Wj_EC2       (1) EC-2 depends on the Wajsberg system
LCL008=YQL_EC4      (1) EC-4 depends on YQL
LCL009=YQL_EC5      (1) EC-5 depends on YQL
LCL010=YQF_YQL      (1) YQL depends on YQF
LCL011=YQJ_YQF      (1) YQF depends on YQJ
LCL012=UM_YQJ       (1) YQJ depends on UM
LCL013=XGF_UM       (1) UM depends on XGF
LCL014=WN_XGF       (1) XGF depends on WN
LCL015=YRM_WN       (1) WN depends on YRM
LCL016=YRO_YRM      (1) YRM depends on YRO
LCL017=PYO_YRO      (1) YRO depends on PYO
LCL018=PYM_PYO      (1) PYO depends on PYM
LCL019=XGK_PYM      (1) PYM depends on XGK
LCL020=XHK_XGK      (1) XGK depends on XHK
LCL021=XHN_XHK      (1) XHK depends on XHN
LCL022=YQL_EC1      (1) EC-1 depends on YQL
LCL023=YQL_EC2      (1) EC-2 depends on YQL
LCL024=XGK_PYO      (1) PYO depends on XGK
LCL025=Ch_C01       (1) C0-1 depends on the Church system
LCL026=Ch_C03       (1) C0-3 depends on the Church system
LCL027=Ch_C04       (1) C0-4 depends on the Church system
LCL028=Ch_CAM       (1) C0-CAMerideth depends on the Church system
LCL029=TB_C05       (1) C0-5 depends on the Tarski-Bernays system
LCL030=TB_C06       (1) C0-6 depends on the Tarski-Bernays system
LCL031=TB_CAM       (1) C0-CAMerideth depends on the Tarski-Bernays system
LCL032=CAM_C01      (1) C0-1 depends on the Merideth axiom
LCL033=CAM_C02      (1) C0-2 depends on the Merideth axiom
LCL034=CAM_C03      (1) C0-3 depends on the Merideth axiom
LCL035=CAM_C04      (1) C0-4 depends on the Merideth axiom
LCL036=CAM_C05      (1) C0-5 depends on the Merideth axiom
LCL037=CAM_C06      (1) C0-6 depends on the Merideth axiom
LCL038=Ov_C01       (1) C0-1 depends on a single axiom
LCL039=Modal        (1) A theorem from Morgan
LCL040=Fr_CN21      (1) CN-21 depends on the rest of Frege's system
LCL041=Hl_CN30      (1) CN-30 depends on the rest of Hilbert's system
LCL042=Hl_CN35      (1) CN-35 depends on Hilbert's system
LCL043=Hl_CN39      (1) CN-39 depends on Hilbert's system
LCL044=Hl_CN40      (1) CN-40 depends on Hilbert's system
LCL045=Hl_CN46      (1) CN-46 depends on Hilbert's system
LCL046=Lk_CN16      (1) CN-16 depends on the Lukasiewicz system
LCL047=Lk_CN18      (1) CN-18 depends on the Lukasiewicz system
LCL048=Lk_CN19      (1) CN-19 depends on the Lukasiewicz system
LCL049=Lk_CN20      (1) CN-20 depends on the Lukasiewicz system
LCL050=Lk_CN21      (1) CN-21 depends on the Lukasiewicz system
LCL051=Lk_CN22      (1) CN-22 depends on the Lukasiewicz system
LCL052=Lk_CN24      (1) CN-24 depends on the Lukasiewicz system
LCL053=Lk_CN30      (1) CN-30 depends on the Lukasiewicz system
LCL054=Lk_CN35      (1) CN-35 depends on the Lukasiewicz system
LCL055=Lk_CN37      (1) CN-37 depends on the Lukasiewicz system
LCL056=Lk_CN39      (1) CN-39 depends on the Lukasiewicz system
LCL057=Lk_CN40      (1) CN-40 depends on the Lukasiewicz system
LCL058=Lk_CN46      (1) CN-46 depends on the Lukasiewicz system
LCL059=Lk_CN49      (1) CN-49 depends on the Lukasiewicz system
LCL060=Lk_CN54      (1) CN-54 depends on the Lukasiewicz system
LCL061=Lk_CN59      (1) CN-59 depends on the Lukasiewicz system
LCL062=Lk_CN60      (1) CN-60 depends on the Lukasiewicz system
LCL063=Lk_CAM       (1) CN-CAMerideth depends on the Lukasiewicz system
LCL064=Ch_CN1       (2) CN-1 depends on the Church system
LCL065=Ch_CN2       (1) CN-2 depends on the Church system
LCL066=Ch_CN3       (1) CN-3 depends on the Church system
LCL067=Lk2_CN1      (1) CN-1 depends on the second Lukasiewicz system
LCL068=Lk2_CN2      (1) CN-2 depends on the second Lukasiewicz system
LCL069=Lk2_CN3      (1) CN-3 depends on the second Lukasiewicz system
LCL070=Ws_CN1       (1) CN-1 depends on the Wos system
LCL071=Ws_CN2       (1) CN-2 depends on the Wos system
LCL072=Ws_CN3       (1) CN-3 depends on the Wos system
LCL073=CAM_CN1      (1) CN-1 depends on the single Merideth axiom
LCL074=CAM_CN2      (1) CN-2 depends on the single Merideth axiom
LCL075=CAM_CN3      (1) CN-3 depends on the single Merideth axiom
LCL076=Ch_CN40      (3) CN-40 depends on the Church system
LCL077=Ch_CN39      (2) CN-39 depends on the Church system
LCL078=Ch1_CN40     (1) CN-40 depends on CN-18 CN-35 CN-46
LCL079=Ch_TR        (1) Transitivity can be derived from Church's system
LCL080=TB_Lk1       (2) The 1st Lukasiewicz axiom depends on Tarski-Bernays system
LCL081=Lk1_IC1      (1) IC-1 depends on the 1st Lukasiewicz axiom
LCL082=Lk1_IC2      (1) IC-2 depends on the 1st Lukasiewicz axiom
LCL083=Lk1_IC3      (2) IC-3 depends on the 1st Lukasiewicz axiom
LCL084=Lk1_IC4      (3) IC-4 depends on the 1st Lukasiewicz axiom
LCL085=Lk1_IC5      (1) IC-5 depends on the 1st Lukasiewicz axiom
LCL086=Lk4_IC1      (1) IC-1 depends on the 4th Lukasiewicz axiom
LCL087=Lk4_IC2      (1) IC-2 depends on the 4th Lukasiewicz axiom
LCL088=Lk4_IC3      (1) IC-3 depends on the 4th Lukasiewicz axiom
LCL089=Lk4_IC4      (1) IC-4 depends on the 4th Lukasiewicz axiom
LCL090=Lk5_IC1      (1) IC-1 depends on the 5th Lukasiewicz axiom
LCL091=Lk5_IC2      (1) IC-2 depends on the 5th Lukasiewicz axiom
LCL092=Lk5_IC3      (1) IC-3 depends on the 5th Lukasiewicz axiom
LCL093=Lk5_IC4      (1) IC-4 depends on the 5th Lukasiewicz axiom
LCL094=Lk4_IC5      (1) IC-5 depends on the 4th Lukasiewicz axiom
LCL095=Lk5_IC5      (1) IC-5 depends on the 5th Lukasiewicz axiom
LCL096=Kl_LG1       (1) LG-1 depends on LG-2, LG-3, LG-4
LCL097=Kl_LG4       (1) LG-4 depends on LG-2, LG-3
LCL098=LG3_LG4      (1) LG-4 depends on LG-3
LCL099=Mc1_LG5      (1) LG-5 depends on the 1st McCune system
LCL100=Mc2_LG3      (1) LG-3 depends on the 2nd McCune system
LCL101=Mc3_P1       (1) P-1 depends on the 3rd McCune system
LCL102=Mc4_P1       (1) P-1 depends on the 4th McCune system
LCL103=Mc5_LG2      (1) LG-2 depends on the 5th McCune system
LCL104=Mc6_P1       (1) P-1 depends on the 6th McCune system
LCL105=Mc7_LG2      (1) LG-2 depends on the 7th McCune system
LCL106=Q1Q4_Q2      (1) Q-2 depends on Q-1, Q-4
LCL107=McAx_P1      (1) P-1 depends on the single McCune axiom
LCL108=McAx_Q3      (1) Q-3 depends on the single McCune axiom
LCL109=CAM_MV4      (6) MV-4 depends on the Merideth system
LCL110=CAM_MV24     (2) MV-24 depnds on the Merideth system
LCL111=CAM_MV25     (2) MV-25 depends on the Merideth system
LCL112=CAM_MV29     (2) MV-29 depnds on the Merideth system
LCL113=CAM_MV33     (2) MV-33 depnds on the Merideth system
LCL114=CAM_MV36     (2) MV-36 depnds on the Merideth system
LCL115=CAM_MV39     (2) MV-39 depnds on the Merideth system
LCL116=CAM_MV50     (2) MV-50 depnds on the Merideth system
LCL117=YQM_QYF      (1) QYF depends on YQM
LCL118=WO_YQM       (1) YQM depends on WO
LCL119=XGJ_WO       (1) WO depends on XGJ
LCL120=QYF_XGJ      (1) XGJ depends on QYF
LCL121=LG2_LG1      (1) LG-1 depends on LG-2
LCL122=LG2_LG3      (1) LG-3 depends on LG-2
LCL123=LG2_LG4      (1) LG-4 depends on LG-2
LCL124=LG2_LG5      (1) LG-5 depends on LG-2
LCL125=Mc1_LG2      (1) LG-2 depends on the 1st McCune system
LCL126=Mc2_LG2      (1) Q-2 depends on the 2nd McCune system
LCL127=LG2_S2       (1) LG-2 depends on S-2
LCL128=LG2_S3       (1) LG-2 depends on S-3
LCL129=LG2_S4       (1) LG-2 depends on S-4
LCL130=LG2_P4       (1) LG-2 depends on P-4
LCL131=LG2_S6       (1) LG-2 depends on S-6
LCL132=WjAlg1Eqn1   (1) A lemma in Wajsberg algebras
LCL133=WjAlg1Eqn2   (1) A lemma in Wajsberg algebras
LCL134=WjAlg1Eqn3   (1) A lemma in Wajsberg algebras
LCL135=WjAlg1Eqn4   (1) A lemma in Wajsberg algebras
LCL136=WjAlg1Eqn5   (1) A lemma in Wajsberg algebras
LCL137=WjAlg1Eqn6   (1) A lemma in Wajsberg algebras
LCL138=WjAlg1Eqn7   (1) A lemma in Wajsberg algebras
LCL139=WjAlg1Eqn8   (1) A lemma in Wajsberg algebras
LCL140=WjAlg1Eqn9   (1) A lemma in Wajsberg algebras
LCL141=WjAlg1Eqn10  (1) A lemma in Wajsberg algebras
LCL142=WjLattEqn1   (1) A theorem in the lattice structure of Wajsberg algebras
LCL143=WjLattEqn2   (1) A theorem in the lattice structure of Wajsberg algebras
LCL144=WjLattEqn3   (1) A theorem in the lattice structure of Wajsberg algebras
LCL145=WjLattEqn4   (1) A theorem in the lattice structure of Wajsberg algebras
LCL146=WjLattEqn5   (1) A theorem in the lattice structure of Wajsberg algebras
LCL147=WjLattEqn6   (1) A theorem in the lattice structure of Wajsberg algebras
LCL148=WjLattEqn7   (1) A theorem in the lattice structure of Wajsberg algebras
LCL149=WjLattEqn9   (1) A theorem in the lattice structure of Wajsberg algebras
LCL150=WjLattEqn10  (1) A theorem in the lattice structure of Wajsberg algebras
LCL151=WjLattEqn11  (1) A theorem in the lattice structure of Wajsberg algebras
LCL152=WjLattEqn12  (1) A theorem in the lattice structure of Wajsberg algebras
LCL153=WjAlg2Ax1    (1) The 1st alternative Wajsberg algebra axiom
LCL154=WjAlg2Ax2    (1) The 2nd alternative Wajsberg algebra axiom
LCL155=WjAlg2Ax3    (1) The 3rd alternative Wajsberg algebra axiom
LCL156=WjAlg2Ax4    (1) The 4th alternative Wajsberg algebra axiom
LCL157=WjAlg2Ax5    (1) The 5th alternative Wajsberg algebra axiom
LCL158=WjAlg2Ax6    (1) The 6th alternative Wajsberg algebra axiom
LCL159=WjAlg2Ax7    (1) The 7th alternative Wajsberg algebra axiom
LCL160=WjAlg2Ax8    (1) The 8th alternative Wajsberg algebra axiom
LCL161=WjAlg1Ax1    (1) The 1st Wajsberg algebra axiom, from the alternative axioms
LCL162=WjAlg1Ax2    (1) The 2nd Wajsberg algebra axiom, from the alternative axioms
LCL163=WjAlg1Ax3    (1) The 3rd Wajsberg algebra axiom, from the alternative axioms
LCL164=WjAlg1Ax4    (1) The 4th Wajsberg algebra axiom, from the alternative axioms
LCL165=WjAlg1Eqn11  (1) A theorem in Wajsberg algebras
LCL166=XHN_UM       (1) UM depends on XHN
LCL167=XHK_YRO      (1) YRO depends on XHK
LCL168=XEHNotAx     (1) XEH is not a single axiom for the R-calculus
LCL169=PropEqn2.01  (1) Principia Mathematica 2.01
LCL170=PropEqn2.02  (1) Principia Mathematica 2.02
LCL171=PropEqn2.03  (1) Principia Mathematica 2.03
LCL172=PropEqn2.04  (1) Principia Mathematica 2.04
LCL173=PropEqn2.05  (1) Principia Mathematica 2.05
LCL174=PropEqn2.06  (1) Principia Mathematica 2.06
LCL175=PropEqn2.07  (1) Principia Mathematica 2.07
LCL176=PropEqn2.1   (1) Principia Mathematica 2.1 and 2.08
LCL177=PropEqn2.11  (1) Principia Mathematica 2.11
LCL178=PropEqn2.12  (1) Principia Mathematica 2.12
LCL179=PropEqn2.13  (1) Principia Mathematica 2.13
LCL180=PropEqn2.14  (1) Principia Mathematica 2.14
LCL181=PropEqn2.15  (2) Principia Mathematica 2.15
LCL182=PropEqn2.16  (1) Principia Mathematica 2.16
LCL183=PropEqn2.17  (1) Principia Mathematica 2.17
LCL184=PropEqn2.18  (1) Principia Mathematica 2.18
LCL185=PropEqn2.2   (1) Principia Mathematica 2.2
LCL186=PropEqn2.21  (1) Principia Mathematica 2.21
LCL187=PropEqn2.24  (1) Principia Mathematica 2.24
LCL188=PropEqn2.25  (1) Principia Mathematica 2.25
LCL189=PropEqn2.26  (1) Principia Mathematica 2.26 and 2.27
LCL190=PropEqn2.3   (1) Principia Mathematica 2.3
LCL191=PropEqn2.31  (1) Principia Mathematica 2.31
LCL192=PropEqn2.32  (1) Principia Mathematica 2.32 and 2.33
LCL193=PropEqn2.36  (1) Principia Mathematica 2.36
LCL194=PropEqn2.37  (1) Principia Mathematica 2.37
LCL195=PropEqn2.38  (1) Principia Mathematica 2.38
LCL196=PropEqn2.4   (1) Principia Mathematica 2.4
LCL197=PropEqn2.41  (1) Principia Mathematica 2.41
LCL198=PropEqn2.42  (1) Principia Mathematica 2.42 and 2.43
LCL199=PropEqn2.45  (1) Principia Mathematica 2.45
LCL200=PropEqn2.46  (1) Principia Mathematica 2.46
LCL201=PropEqn2.47  (1) Principia Mathematica 2.47
LCL202=PropEqn2.48  (1) Principia Mathematica 2.48
LCL203=PropEqn2.49  (1) Principia Mathematica 2.49
LCL204=PropEqn2.5   (1) Principia Mathematica 2.5
LCL205=PropEqn2.51  (1) Principia Mathematica 2.51
LCL206=PropEqn2.52  (1) Principia Mathematica 2.52
LCL207=PropEqn2.521 (1) Principia Mathematica 2.521
LCL208=PropEqn2.53  (1) Principia Mathematica 2.53
LCL209=PropEqn2.54  (1) Principia Mathematica 2.54
LCL210=PropEqn2.55  (1) Principia Mathematica 2.55
LCL211=PropEqn2.56  (1) Principia Mathematica 2.56
LCL212=PropEqn2.6   (1) Principia Mathematica 2.6
LCL213=PropEqn2.61  (1) Principia Mathematica 2.61
LCL214=PropEqn2.61  (1) Principia Mathematica 2.61
LCL215=PropEqn2.62  (1) Principia Mathematica 2.62 and 2.63
LCL216=PropEqn2.64  (1) Principia Mathematica 2.64
LCL217=PropEqn2.65  (1) Principia Mathematica 2.65
LCL218=PropEqn2.67  (1) Principia Mathematica 2.67
LCL219=PropEqn2.68  (1) Principia Mathematica 2.68
LCL220=PropEqn2.69  (1) Principia Mathematica 2.69
LCL221=PropEqn2.73  (1) Principia Mathematica 2.73
LCL222=PropEqn2.74  (1) Principia Mathematica 2.74
LCL223=PropEqn2.75  (1) Principia Mathematica 2.75
LCL224=PropEqn2.76  (1) Principia Mathematica 2.76
LCL225=PropEqn2.77  (1) Principia Mathematica 2.77
LCL226=PropEqn2.8   (1) Principia Mathematica 2.8
LCL227=PropEqn2.81  (1) Principia Mathematica 2.81
LCL228=PropEqn2.82  (1) Principia Mathematica 2.82
LCL229=PropEqn2.83  (1) Principia Mathematica 2.83
LCL230=PropEqn2.85  (2) Principia Mathematica 2.85
LCL231=PropEqn2.86  (1) Principia Mathematica 2.86
LCL232=PropEqn3.1   (1) Principia Mathematica 3.1
LCL233=PropEqn3.11  (1) Principia Mathematica 3.11
LCL234=PropEqn3.2   (1) Principia Mathematica 3.2 and 3.12
LCL235=PropEqn3.13  (1) Principia Mathematica 3.13
LCL236=PropEqn3.14  (1) Principia Mathematica 3.14
LCL237=PropEqn3.21  (1) Principia Mathematica 3.21
LCL238=PropEqn3.22  (1) Principia Mathematica 3.22
LCL239=PropEqn3.24  (1) Principia Mathematica 3.24
LCL240=PropEqn3.26  (1) Principia Mathematica 3.26
LCL241=PropEqn3.27  (1) Principia Mathematica 3.27
LCL242=PropEqn3.3   (1) Principia Mathematica 3.3
LCL243=PropEqn3.31  (1) Principia Mathematica 3.31
LCL244=PropEqn3.33  (1) Principia Mathematica 3.33
LCL245=PropEqn3.34  (1) Principia Mathematica 3.34
LCL246=PropEqn3.35  (1) Principia Mathematica 3.35
LCL247=PropEqn3.37  (1) Principia Mathematica 3.37
LCL248=PropEqn3.4   (1) Principia Mathematica 3.4
LCL249=PropEqn3.41  (1) Principia Mathematica 3.41
LCL250=PropEqn3.42  (1) Principia Mathematica 3.42
LCL251=PropEqn3.43  (1) Principia Mathematica 3.43
LCL252=PropEqn3.44  (1) Principia Mathematica 3.44
LCL253=PropEqn3.45  (1) Principia Mathematica 3.45
LCL254=PropEqn3.47  (1) Principia Mathematica 3.47
LCL255=PropEqn3.48  (1) Principia Mathematica 3.48
LCL256=Lk_NotNotImplies (1) A formula that can be derived from the Lukasiewicz system
-------------------------------------------------------------------------------
Domain LDA = Left Distributive (14 abstract problems, 23 problems)
-------------------------------------------------------------------------------
LDA001=LDAlgEqn1    (1) Verify 3*2*U = UUU, where U = 2*2
LDA002=LDAlgEqn2    (1) Verify 3*2(U2)(UU(UU)) = U1(U3)(UU(UU))
LDA003=LeftSegEqn1  (1) Show that 3 is a left segment of U = 2*2
LDA004=LeftSegEqn2  (1) Show that 3*2(U2) is a left segment of U1(U3)
LDA005=EmbdgAlgEqn1 (2) Let g=cr(t). Show that tt(tsg) < t(tsg) (for any s)
LDA006=EmbdgAlgEqn2 (2) Let g = cr(t). Show that tsg is not in the range of t
LDA007=EmbdgAlgEqn3 (3) Let g = cr(t). Show that t(tsg) = tt(ts)(tg)
LDA008=EmbdgAlgEqn4 (2) Let g = cr(t) = cr(T). If Ta < Tsg, then ta < tsg
LDA009=EmbdgAlgEqn5 (2) Let g = cr(t). If g < sg, then st(ts)g < stt(sg)
LDA010=EmbdgAlgEqn6 (2) Let g = cr(t). Show that stts(sttt)(stts)g < stt(sg)
LDA011=EmbdgAlgEqn7 (2) Let g = cr(t). Show that stts(sttt)(stts)stts(sttt)g < stt(sg)
LDA012=EmbdgAlgEqn8 (2) Let g = cr(t). Show that stts(sttt)g = g
LDA013=EmbdgAlgEqn9Base (1) Let g = cr(t). Show that aag <= ag, t=a
LDA014=EmbdgAlgEqn9Indn (1) Let g = cr(t). Show that aag <= ag, t=a
-------------------------------------------------------------------------------
Domain MSC = Miscellaneous (9 abstract problems, 12 problems)
-------------------------------------------------------------------------------
MSC001=BHand1       (1) A Blind Hand Problem
MSC002=BHand2       (2) A Blind Hand Problem
MSC003=HasParts1    (1) Show that the boy, John, has 2 hands
MSC004=HasParts2    (1) Show that the boy, John, has 10 fingers
MSC005=XOR          (1) The evaluation of XOR expressions
MSC006=NonObv       (1) A "non-obvious" problem
MSC007=Pigeon       (2) Cook pigeon-hole problem
MSC008=LatSq        (2) The (in)constructability of Graeco-Latin Squares
MSC009=FamilyTBox   (1) Definitions of a family structure
-------------------------------------------------------------------------------
Domain NUM = Number Theory (286 abstract problems, 309 problems)
-------------------------------------------------------------------------------
NUM001=SumAssc      (1) (A + B) + C = A + (B + C)
NUM002=SumDiff1     (1) (X - Y) + Z = X + (Z - Y)
NUM003=SumDiff2     (1) A + (B - C) = (A - C) + B
NUM004=SumDiff3     (1) (A + B) - C = A + (B - C)
NUM005=GCD          (1) Greatest Common Divisor
NUM006=Goldbach     (1) Goldbach conjecture
NUM007=LCM          (1) Least Common Multiple
NUM008=Peano1       (1) Peano axiom 0
NUM009=Peano2       (1) Peano axiom 1
NUM010=Peano3       (1) Peano axiom 2
NUM011=Peano4       (1) Peano axiom 3
NUM012=Peano5       (1) Peano axiom 4
NUM013=Peano6       (1) Peano axiom 5
NUM014=ValIsPrm     (1) If a is a prime and a = b^2/c^2 then a divides b
NUM015=PrmDivEx     (1) Any number greater than 1 has a prime divisor
NUM016=InfPrmEx     (2) There exist infinitely many primes
NUM017=SqRtPrmIrr   (2) Square root of this prime is irrational
NUM018=Inf2PrmEx    (1) There is an infinite number of twin prime numbers
NUM019=EqSymm       (1) Symmetry of equality can be derived
NUM020=SuccX        (1) a + 1 = successor(a)
NUM021=NotDiv       (1) If a <= b < c, then c cannot divide a
NUM022=LtDiv        (1) Numerator divisble by smaller denominators
NUM023=0LtX         (1) Zero is less than all successor numbers
NUM024=XNotLtX      (1) No number is less than itself
NUM025=LtASym       (2) If a<b then not b<a
NUM026=LtMult       (1) Less preserved over multiplication by a number
NUM027=Eqn1         (1) If a >= b and b*c <= a*c, then c = 0
NUM028=SymnEqn1     (1) Symmetrization property 1
NUM029=SymnEqn2     (1) Symmetrization property 2
NUM030=SymnEqn3     (1) Symmetrization property 3
NUM031=SymnEqn4     (1) Symmetrization property 4
NUM032=SymnEqn5     (1) Symmetrization property 5
NUM033=SymnEqn6     (1) Symmetrization property 6
NUM034=SymnIdem     (1) Symmetrization is idempotent
NUM035=DomEqRngSymn (1) Domain equals range of symmetrization
NUM036=SymnEqn7     (1) Symmetrization property 7
NUM037=SymnEqn8     (1) Symmetrization property 8
NUM038=SymnEqn9     (1) Symmetrization property 9
NUM039=IrreflClEqn1 (1) Irreflexive class property 1
NUM040=IrreflClEqn2 (1) Irreflexive class property 2
NUM041=IrreflClEqn3 (1) Irreflexive class property 3
NUM042=IrreflClEqn4 (1) Irreflexive class property 4
NUM043=IrreflClEqn5 (1) Irreflexive class property 5
NUM044=IrreflClEqn6 (1) Irreflexive class property 6
NUM045=IrreflClEqn7 (1) Irreflexive class property 7
NUM046=ConnClEqn1   (1) Connected class property 1
NUM047=ConnClEqn2   (1) Connected class property 2
NUM048=ConnClEqn3   (1) Connected class property 3
NUM049=ConnClEqn4   (1) Connected class property 4
NUM050=ConnClEqn5   (1) Connected class property 5
NUM051=ConnNullCl   (1) Everything is connected to the null class
NUM052=TransOrdEqn1 (1) Transitive ordering property 1
NUM053=TransOrdEqn2 (1) Transitive ordering property 2
NUM054=ASymClEqn1   (1) Asymmetric class property 1
NUM055=ASymClEqn2   (1) Asymmetric class property 2
NUM056=ASymClEqn3   (1) Asymmetric class property 3
NUM057=SegsEqn1     (1) Segments property 1
NUM058=SegsEqn2     (1) Segments property 2
NUM059=SegsEqn3     (1) Segments property 3
NUM060=SegsEqn4     (1) Segments property 4
NUM061=SegsEqn5     (1) Segments property 5
NUM062=SegsEqn6     (1) Segments property 6
NUM063=SegsEqn7     (1) Segments property 7
NUM064=LeastUnq     (1) Least(xr,u) is unique
NUM065=WellOrdEqn1  (1) Well ordering property 1
NUM066=WellOrdEqn1Cor   (1) Corollary to well ordering property 1
NUM067=WellOrdEqn2  (1) Well ordering property 2
NUM068=WellOrdEqn3  (1) Well ordering property 3
NUM069=WellOrdEqn3Cor   (1) Corollary to well ordering property 3
NUM070=WellOrdASym  (1) A well-order is asymmetric
NUM071=WellOrdIrrefl    (1) Well ordering is irreflexive
NUM072=WellOrdEqn4  (1) Well ordering property 4
NUM073=WellOrdEqn4Cor   (1) Corollary to well ordering property 4
NUM074=WellOrdEqn5  (1) Well ordering property 5
NUM075=WellOrdEqn6  (1) Well ordering property 6
NUM076=WellOrdEqn7  (1) Well ordering property 7
NUM077=WellOrdEqn7Cor1  (1) Corollary 1 to well ordering property 7
NUM078=WellOrdEqn7Cor2  (1) Corollary 2 to well ordering property 7
NUM079=WellOrdEqn8  (1) Well ordering property 8
NUM080=WellOrdEqn9  (1) Well ordering property 9
NUM081=WellOrdEqn9Cor   (1) Corollary to well ordering property 9
NUM082=LeastUnqInSubS   (1) Uniqueness of the least element of a non-empty subset
NUM083=TransClEqn1  (1) Transitive class property 1
NUM084=AltTransClDef1   (1) Alternate transitive class definition, part 1
NUM085=AltTransClDef2   (1) Alternate transitive class definition, part 2
NUM086=TransClEqn2  (1) Transitive class property 2
NUM087=TransClEqn3  (1) Transitive class property 3
NUM088=TransClEqn4  (1) Transitive class property 4
NUM089=SectsEqn1    (1) Sections property 1
NUM090=SectsEqn1Cor (1) Corollary to sections property 1
NUM091=SectsEqn2    (1) Sections property 2
NUM092=SectsEqn2Cor1    (1) Corollary 1 to sections property 2
NUM093=SectsEqn2Cor2    (1) Corollary 2 to sections property 2
NUM094=SectsEqn3    (1) Sections property 3
NUM095=SectsEqn4    (1) Sections property 4
NUM096=SectsEqn5    (1) Sections property 5
NUM097=SectsEqn5Cor (1) Corollary to sections property 5
NUM098=OrdlEqn1     (1) Ordinal property 1
NUM099=OrdlEqn1Cor  (1) Corollary to ordinal property 1
NUM100=OrdlEqn2     (1) Ordinal property 2
NUM101=OrdlEqn3     (1) Ordinal property 3
NUM102=OrdlEqn4     (1) Ordinal property 4
NUM103=OrdlEqn4Cor  (1) Corollary to ordinal property 4
NUM104=OrdlEqn5     (1) Ordinal property 5
NUM105=OrdlEqn6     (1) Ordinal property 6
NUM106=OrdlEqn7     (1) Ordinal property 7
NUM107=OrdlEqn8     (1) Ordinal property 8
NUM108=OrdlEqn9     (1) Ordinal property 9
NUM109=OrdlEqn10    (1) Ordinal property 10
NUM110=OrdlEqn10Cor (1) Corollary to ordinal property 10
NUM111=OrdlEqn11    (1) Ordinal property 11
NUM112=OrdlEqn12    (1) Ordinal property 12
NUM113=OrdlEqn13    (1) Ordinal property 13
NUM114=OrdlEqn13Cor (1) Corollary to ordinal property 13
NUM115=OrdClNotSet  (1) The class of ordinals is not a set.
NUM116=OrdClNotSetCor   (1) Corollary to the class of ordinals is not set
NUM117=OrdClNumCor  (1) Corollary to ordinal class and numbers
NUM118=OrdlEqn14    (1) Ordinal property 14
NUM119=TransClEqn4Cor   (1) Corollary to transitive class property 4
NUM120=TrnsfIndn1   (1) Transfinite induction, part 1
NUM121=TrnsfIndn2   (1) Transfinite induction, part 2
NUM122=TrnsfIndn3   (1) Transfinite induction, part 3
NUM123=AltTrnsfIndn3    (1) Alternate transfinite induction 3
NUM124=SmTrnsfInd   (1) Condensed statement of transfinite induction
NUM125=CmpltIndnOmega   (1) Complete induction upto omega
NUM126=Alt1TrnsfInd1    (1) Alternate 1 for transfinite induction, part 1
NUM127=Alt1TrnsfInd2    (1) Alternate 1 for transfinite induction, part 2
NUM128=Alt1TrnsfInd3    (1) Alternate 1 for transfinite induction, part 3
NUM129=Alt2TrnsfInd1    (1) Alternate 2 for transfinite induction, part 1
NUM130=Alt2TrnsfInd2    (1) Alternate 2 for transfinite induction, part 2
NUM131=Alt2TrnsfInd3    (1) Alternate 2 for transfinite induction, part 3
NUM132=UnionSuccRelOrdl (1) Union of successor relation ordinal
NUM133=UnionSuccRelOrdlCor  (1) Corollary to union of successor ordinal
NUM134=SuccRelOrdl  (1) Successor relation of an ordinal is an ordinal
NUM135=NullClSmOrdl (1) The null class is the smallest ordinal
NUM136=OrdlTrans    (1) Transitivity of ordinals
NUM137=Cond1CmpltIndn   (1) Condition 1 for complete induction
NUM138=Cond2CmpltIndn   (1) Condition 2 for complete induction
NUM139=Cond3CmpltIndn   (1) Condition 3 for complete induction
NUM140=SuccSet1     (1) The successor of a set is a set, part 1
NUM141=SuccSet2     (1) The successor of a set is a set, part 2
NUM142=SuccSet3     (1) The successor of a set is a set, part 3
NUM143=SuccSetCor   (1) Corollary to the successor of a set being a set
NUM144=SuccPprCl    (1) The successor of a proper class is a class
NUM145=SuccPprClCor (1) Corollary to the successor of a proper class being a class
NUM146=SuccTransSet (1) The successor of a transitive set is transitive
NUM147=SuccOrdl     (1) The successor of an ordinal is an ordinal
NUM148=PredOrdl     (1) The predecessor of an ordinal is an ordinal
NUM149=SuccEqn1     (1) Successor property 1
NUM150=SuccEqn1Cor1 (1) Corollary 1 to successor property 1
NUM151=SuccEqn1Cor2 (1) Corollary 2 to successor property 1
NUM152=SuccEqn1Cor3 (1) Corollary 3 to successor property 1
NUM153=SuccEqn1Cor4 (1) Corollary 4 to successor property 1
NUM154=SuccEqn1Cor5 (1) Corollary 5 to successor property 1
NUM155=NoOrdlBtwn   (1) There is no ordinal between x and x + 1
NUM156=Cond1K1Ordl  (1) Membership condition 1 for kind 1 ordinals
NUM157=Cond2K1Ordl  (1) Membership condition 2 for kind 1 ordinals
NUM158=Cond3K1Ordl  (1) Membership condition 3 for kind 1 ordinals
NUM159=Cond4K1Ordl  (1) Membership condition 4 for kind 1 ordinals
NUM160=K1OrdlCl     (1) Kind 1 ordinals is a class of ordinals
NUM161=K1OrdlClCor  (1) Corollary to kind 1 ordinals being a class of ordinals
NUM162=SuccEqn2     (1) Successor property 2
NUM163=IndvClsdUnion    (1) Inductive is closed under union
NUM164=IndvClsdIntsc    (1) Inductive is closed under intersection
NUM165=OmegaDefCor1 (1) Corollary to omega definition, part 1
NUM166=OmegaDefCor2 (1) Corollary to omega definition, part 2
NUM167=SuccEqn3     (1) Successor property 3
NUM168=SuccEqn3Cor  (1) Corollary to successor property 3
NUM169=SuccEqn4     (1) Successor property 4
NUM170=SuccEqn5     (1) Successor property 5
NUM171=SuccEqn6     (1) Successor property 6
NUM172=SuccRelSet   (1) The successor relation of a set is different from the set
NUM173=SuccEqn7     (1) Successor property 7
NUM174=SuccEqn8     (1) Successor property 8
NUM175=SuccEqn9     (1) Successor property 9
NUM176=SuccEqn10    (1) Successor property 10
NUM177=Cond1IndvCl  (1) Condition 1 for a class to be inductive
NUM178=Cond2IndvCl  (1) Condition 2 for a class to be inductive
NUM179=Cond3IndvCl  (1) Condition 3 for a class to be inductive
NUM180=LmtOrdl      (1) Limit ordinals are ordinals
NUM181=NullClNotLmt (1) The null class is not a limit ordinal
NUM182=LmtOrdlEqSucc    (1) Only limit ordinals equal their successors
NUM183=OrdlK1OrLmt  (1) Ordinals are either kind 1 or limit
NUM184=OrdlK1OrLmtCor   (1) Corollary to ordinals are either kind 1 or limit
NUM185=LmtOrdlNotMemb   (1) Limit ordinals are not members
NUM186=OmegaEqn1    (1) Omega property 1
NUM187=SuccEqn8Lem  (1) Lemma for successor property 8
NUM188=OmegaTrans   (1) Omega is transitive
NUM189=OmegaOrdl    (1) Omega is an ordinal
NUM190=OmegaNotNullCl   (1) Omega is not the null class
NUM191=OmegaLmtOrdl (1) Omega is a limit ordinal
NUM192=OmegaSmLmtOrdl   (1) Omega is the smallest limit ordinal
NUM193=SumOrdls     (1) The sum of ordinals is an ordinal
NUM194=UnionClOrdls (1) The union of a class of ordinals is a class of ordinals
NUM195=UnionClOrdlsTrans    (1) The union of a class of ordinals is transitive
NUM196=UnionSetOrdls    (1) The union of a set of ordinals is an ordinal
NUM197=UnionPprClOrdls  (1) The union of a proper class of ordinals is the class of ordinals
NUM198=UnionSetOrdlsGt  (1) The union of a set of ordinals is >= each ordinal in the set
NUM199=LubEqn1      (1) Least upper bound property 1
NUM200=LubEqn2      (1) If every element of x is <= y, then sum class(x) <= y
NUM201=LubEqn3      (1) Least upper bound property 3
NUM202=LubSuccRel   (1) If the lub of a set of ordinals is a successor, it's in the set
NUM203=LubSuccRelCor    (1) Corollary to least upper bound being a successor relation
NUM204=LubEqn5      (1) Least upper bound property 5
NUM205=LubEqn5Cor1  (1) Corollary 1 to least upper bound property 5
NUM206=LubEqn5Cor2  (1) Corollary 2 to least upper bound property 5
NUM207=LubEqn6      (1) Least upper bound property 6
NUM208=LubEqn7      (1) Least upper bound property 7
NUM209=LubEqn7Cor   (1) Corollary to least upper bound property 7
NUM210=LubEqn8Lem1  (1) Lemma 1 for least upper bound property 8
NUM211=LubEqn8Lem2  (1) Lemma 2 for least upper bound property 8
NUM212=LubEqn8Lem3  (1) Lemma 3 for least upper bound property 8
NUM213=Alt3TrnsfInd (1) Alternate 3 for transfinite induction
NUM214=IndnY        (1) Induction up to y
NUM215=IndnYCor     (1) Corollary to induction upto y
NUM216=RestDefCor1  (1) Corollary 1 to rest definition
NUM217=RestDefCor2  (1) Corollary 2 to rest definition
NUM218=RestFunc     (1) Rest of is a function
NUM219=DomRestOfEqDom   (1) The domain of rest_of(X) is the domain of X
NUM220=DomRestOfEqDomCor    (1) Corollary to the domain of rest_of(X) being the domain of X
NUM221=RestOfEqn1   (1) Rest_of property 1
NUM222=RestOfMono   (1) Rest_of is monotonic.
NUM223=RestRelFunc  (1) Rest relation is a function
NUM224=RestRelEqn1  (1) Rest relation property 1
NUM225=RestRelEqn2  (1) Rest relation property 2
NUM226=RestRelEqn3  (1) Rest relation property 3
NUM227=RestRelEqn4  (1) Rest relation property 4
NUM228=RecrEqnFuncDefCor    (1) Corollary to recursion equation functions definition
NUM229=TrnsfRecrLem0    (1) Transfinite recursion lemma 0
NUM230=TrnsfRecrLem1    (1) Transfinite recursion lemma 1
NUM231=TrnsfRecrLem2    (1) Transfinite recursion lemma 2
NUM232=TrnsfRecrLem3    (1) Transfinite recursion lemma 3
NUM233=TrnsfRecrLem4    (1) Transfinite recursion lemma 4
NUM234=TrnsfRecrLem5    (1) Transfinite recursion lemma 5
NUM235=TrnsfRecrLem6    (1) Transfinite recursion lemma 6
NUM236=TrnsfRecrLem6Cor1    (1) Corollary 1 to transfinite recursion lemma 6
NUM237=TrnsfRecrLem6Cor2    (1) Corollary 2 to transfinite recursion lemma 6
NUM238=TrnsfRecrLem7    (1) Transfinite recursion lemma 7
NUM239=TrnsfRecrLem8    (1) Transfinite recursion lemma 8
NUM240=TrnsfRecrLem9_1  (1) Transfinite recursion lemma 9.1
NUM241=TrnsfRecrLem9_2  (1) Transfinite recursion lemma 9.2
NUM242=TrnsfRecrLem9_3  (1) Transfinite recursion lemma 9.3
NUM243=TrnsfRecrLem10   (1) Transfinite recursion lemma 10
NUM244=TrnsfRecrLem11   (1) Transfinite recursion lemma 11
NUM245=TrnsfRecrEqn1    (2) Transfinite recursion property 1
NUM246=TrnsfRecrEqn2    (2) Transfinite recursion property 2
NUM247=TrnsfRecrEqn3    (2) Transfinite recursion property 3
NUM248=TrnsfRecrEqn4    (2) Transfinite recursion property 4
NUM249=TrnsfRecrEqn5    (2) Transfinite recursion property 5
NUM250=TrnsfRecrEqn6    (2) Transfinite recursion property 6
NUM251=TrnsfRecrEqn7    (2) Transfinite recursion property 7
NUM252=TrnsfRecrEqn8    (2) Transfinite recursion property 8
NUM253=TrnsfRecrEqn9    (2) Transfinite recursion property 9
NUM254=TrnsfRecrEqn10   (2) Transfinite recursion property 10
NUM255=TrnsfRecrEqn11   (2) Transfinite recursion property 11
NUM256=TrnsfRecrEqn12   (2) Transfinite recursion property 12
NUM257=TrnsfRecrEqn13   (2) Transfinite recursion property 13
NUM258=TrnsfRecrEqn14   (2) Transfinite recursion property 14
NUM259=TrndfRecrFuncUnq (2) The uniqueness of the function defined by transfinite recursion
NUM260=Alt4TrnsfIndn1   (2) Alternate 4 for transfinite induction, part 1
NUM261=Alt4TrnsfIndn2   (2) Alternate 4 for transfinite induction, part 2
NUM262=Alt4TrnsfIndn3   (2) Alternate 4 for transfinite induction, part 3
NUM263=Alt4TrnsfIndn4   (2) Alternate 4 for transfinite induction, part 4
NUM264=Alt4TrnsfIndn5   (2) Alternate 4 for transfinite induction, part 5
NUM265=OrdlAddEqn1  (1) Ordinal addition property 1
NUM266=OrdlAddEqn2  (1) Ordinal addition property 2
NUM267=OrdlAddEqn3  (1) Ordinal addition property 3
NUM268=OrdlAddEqn4  (1) Ordinal addition property 4
NUM269=OrdlAddEqn5  (1) Ordinal addition property 5
NUM270=OrdlAddEqn6  (1) Ordinal addition property 6
NUM271=OrdlAddEqn7Lem1  (1) Lemma 1 for ordinal addition property 7
NUM272=OrdlAddEqn7Lem2  (1) Lemma 2 for ordinal addition property 7
NUM273=OrdlAddEqn7Lem3  (1) Lemma 3 for ordinal addition property 7
NUM274=OrdlAddEqn7Lem4  (1) Lemma 4 for ordinal addition property 7
NUM275=OrdlAddEqn7Lem5  (1) Lemma 5 for ordinal addition property 7
NUM276=OrdlAddEqn7Lem6  (1) Lemma 6 for ordinal addition property 7
NUM277=OrdlAddEqn7_1    (2) Ordinal addition property 7_1
NUM278=OrdlAddEqn7_2    (1) Ordinal addition property 7_2
NUM279=OrdlAddEqn8  (1) Ordinal addition property 8
NUM280=OrdlMultEqn1 (1) Ordinal multiplication property 1
NUM281=OrdlMultEqn2 (1) Ordinal multiplication property 2
NUM282=OrdlMultEqn3 (1) Ordinal multiplication property 3
NUM283=Factorial    (1) Calculation of factorial
NUM284=Fibonacci    (1) Calculation of fibonacci numbers
NUM285=BiCond       (1) a0 + ... + a5 = b1 + ... + b5, expression in logic
-------------------------------------------------------------------------------
Domain PLA = Planning (23 abstract problems, 30 problems)
-------------------------------------------------------------------------------
PLA001=Bread        (1) Cheyenne to DesMoines, buying a loaf of bread on the way
PLA002=Going        (2) Getting from here to there, in all weather
PLA003=Monkey       (1) Monkey and Bananas Problem
PLA004=Blocks_CBA   (2) Block C on B on A
PLA005=Blocks_CA_DB (2) Block C on A and D on B
PLA006=Blocks_CTable    (1) Block C on Table
PLA007=Blocks_AD    (1) Block A on D
PLA008=Blocks_BD_AC (1) Block B on D and A on C
PLA009=Blocks_AB_D  (2) Block A on B and D clear
PLA010=Blocks_ADB   (1) Block A on D on B
PLA011=Blocks_DCB   (2) Block D on C on B
PLA012=Blocks_DBC   (1) Block D on B on C
PLA013=Blocks_ACB   (1) Block A on C on B
PLA014=Blocks_ABC   (2) Block A on B on C
PLA015=Blocks_ABD   (1) Block A on B on D
PLA016=Blocks_DA    (1) Block D on A
PLA017=Blocks_AC    (1) Block A on C
PLA018=Blocks_AB_DC (1) Block A on B and D on C
PLA019=Blocks_DC    (1) Block D on C
PLA020=Blocks_D     (1) Block D clear
PLA021=Blocks_BD_CA (1) Block B on D and C on A
PLA022=Blocks_ACD   (2) Block A on C on D
PLA023=Blocks_DAC   (1) Block D on A on C
-------------------------------------------------------------------------------
Domain PRV = Program Verification (9 abstract problems, 9 problems)
-------------------------------------------------------------------------------
PRV001=Unknown      (1) PV1
PRV002=Unknown      (1) E1
PRV003=Unknown      (1) E2
PRV004=Unknown      (1) E3
PRV005=Unknown      (1) E4
PRV006=Unknown      (1) E5
PRV007=Unknown      (1) E6
PRV008=Unknown      (1) E7
PRV009=FIND         (1) A condition from Hoare's FIND program
-------------------------------------------------------------------------------
Domain PUZ = Puzzles (35 abstract problems, 45 problems)
-------------------------------------------------------------------------------
PUZ001=Agatha       (3) Dreadbury Mansion
PUZ002=Animals      (1) The Animals Puzzle
PUZ003=Barber       (1) The Barber Puzzle
PUZ004=Letters      (1) The Letters Puzzle
PUZ005=LionU        (1) Lions and Unicorns
PUZ006=MarsVenus1   (1) Determine sex and race on Mars and Venus
PUZ007=MarsVenus2   (1) Mixed couples on Mars and Venus
PUZ008=MissCann     (3) Missionaries and Cannibals
PUZ009=Oona         (1) Looking for Oona
PUZ010=Zebra        (1) Who owns the zebra?
PUZ011=Borders1     (1) An ocean that borders on an African and an Asian country
PUZ012=Boxes        (1) The Mislabeled Boxes
PUZ013=Boys1        (1) The School Boys : Prove some monitors are awake
PUZ014=Boys2        (1) The School Boys : Prove that all monitors are awake
PUZ015=Checkers1    (2) Checkerboard and Dominoes : Opposing corners removed
PUZ016=Checkers2    (2) Checkerboard and Dominoes : Row 1, columns 2 and 3 removed
PUZ017=Houses       (1) The Houses
PUZ018=Interns      (2) The Interns
PUZ019=Jobs         (1) The Jobs Puzzles
PUZ020=KKnave1      (1) A knights & knaves problem, if he's a knight, so is she
PUZ021=KKnave2      (1) How to Win a Bride
PUZ022=Borders2     (1) An ocean that borders on two adjacent Australian states
PUZ023=KKnave27     (1) Knights and Knaves #27
PUZ024=KKnave31     (1) Knights and Knaves #31
PUZ025=KKnave35     (1) Knights and Knaves #35
PUZ026=KKnave39     (1) Knights and Knaves #39
PUZ027=KKnave42     (1) Knights and Knaves #42
PUZ028=Party        (4) People at a party
PUZ029=Pigs         (1) The pigs and balloons puzzle
PUZ030=SaltM        (2) Salt and Mustard Problem
PUZ031=SteamR       (1) Schubert's Steamroller
PUZ032=KKnave26     (1) Knights and Knaves #26
PUZ033=Winds        (1) The Winds and the Windows Puzzle
PUZ034=NQueens      (1) N queens problem
-------------------------------------------------------------------------------
Domain RNG = Rings (40 abstract problems, 100 problems)
-------------------------------------------------------------------------------
RNG001=XTimesAId    (5) X.additive_identity = additive_identity for any X
RNG002=AddRCanc     (1) Right cancellation for addition
RNG003=AddLCanc     (1) Left cancellation for addition
RNG004=ProdInv      (3) X*Y = -X*-Y
RNG005=SumEqAId     (2) (-X*Y) + (X*Y) = additive_identity
RNG006=Eqn1         (3) X*(Y+ -Z) = (X*Y) + -(X*Z)
RNG007=BoolInv      (3) In Boolean rings, X is its own inverse
RNG008=BoolComm     (7) Boolean rings are commutative
RNG009=CubeComm     (2) If X*X*X = X then the ring is commutative
RNG010=AuxSkewSymm  (5) Skew symmetry of the auxilliary function
RNG011=RAltEqn      (1) In a right alternative ring (((X,X,Y)*X)*(X,X,Y)) = Add Id
RNG012=ProdInv      (1) Product of inverses equal product
RNG013=InvProd1     (1) -X*Y = -(X*Y)
RNG014=InvProd2     (1) -X*Y = -(X*Y)
RNG015=DiffDist1    (1) X*(Y+ -Z) = (X*Y) + -(X*Z)
RNG016=DiffDist2    (1) (X+ -Y)*Z = (X*Z) + -(Y*Z)
RNG017=DiffDist3    (1) -X*(Y+Z) = -(X*Y) + -(X*Z)
RNG018=DiffDist4    (1) (X+Y)* -Z = -(X*Z) + -(Y*Z)
RNG019=LinAssr1     (2) First part of the linearised form of the associator
RNG020=LinAssr2     (2) Second part of the linearised form of the associator
RNG021=LinAssr3     (2) Third part of the linearised form of the associator
RNG023=LAlt         (2) Left alternative
RNG024=RAlt         (2) Right alternative
RNG025=FlexLaw      (7) Middle or Flexible Law
RNG026=TeichId      (2) Teichmuller Identity
RNG027=RMoufang     (7) Right Moufang identity
RNG028=LMoufang     (7) Left Moufang identity
RNG029=MMoufang     (5) Middle Moufang identity
RNG030=AssrEqn2     (2) 2*assr(X,X,Y)^3 = additive identity
RNG031=AssrEqn3     (2) (W*W)*X*(W*W) = additive identity
RNG032=AssrEqn4     (2) 6*assr(X,X,Y)^6 = additive identity
RNG033=AssrEqn5     (4) A fairly complex equation with associators
RNG034=AssrSkewSymm (1) A skew symmetry relation of the associator
RNG035=FourthComm   (1) If X*X*X*X = X then the ring is commutative
RNG036=FifthComm    (1) If X*X*X*X*X = X then the ring is commutative
RNG037=SumEqAId2    (2) (X* -Y) + (X*Y) = additive_identity
RNG038=RngEqn1      (2) Ring property 1
RNG039=RngEqn2      (2) Ring property 2
RNG040=RngEqn3      (2) Ring property 4
RNG041=RngEqn4      (1) Unknown
-------------------------------------------------------------------------------
Domain ROB = Robbins (27 abstract problems, 36 problems)
-------------------------------------------------------------------------------
ROB001=RobBool      (1) Is every Robbins algebra Boolean?
ROB002=RobBool1     (1) --X = X => Boolean
ROB003=RobBool2     (1) X + c=c => Boolean
ROB004=RobBool3     (1) c = -d, c + d=d, and c + c=c => Boolean
ROB005=RobBool4     (1) c + c=c => Boolean
ROB006=RobBool5     (3) c + d=d => Boolean
ROB007=RobBool6     (4) -(a + b)= -b => Boolean
ROB008=Eqn1         (1) If -(a + -(b + c)) = -(a + b + -c) then a+b=a
ROB009=Eqn2         (1) If -(a + -(b + c)) = -(b + -(a + c)) then a = b
ROB010=Eqn3         (1) If -(a + -b) = c then -(c + -(b + a)) = a
ROB011=Eqn3Base     (1) If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=1
ROB012=Eqn3Indn     (2) If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=k + 1
ROB013=Eqn4         (1) If -(a + b) = c then -(c + -(-b + a)) = a
ROB014=Eqn5Base     (2) If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e, k=1
ROB015=Eqn5Indn     (2) If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e, k=k+1
ROB016=Eqn6         (1) If -(d + e) = -e then -(e + k(d + -(d + -e))) = -e, for k>0
ROB017=Absb1        (1) If -(2f + h) = -(3f + h) = -h then 2f + h = 3f + h
ROB018=Absb2        (1) If -(d + e) = -e then e + 2(d + -(d + -e)) absorbs d + -(d + -e)
ROB019=Absb3        (1) A complex absorbtion condition
ROB020=RobBool7     (2) -(a + -b)=b => Boolean
ROB021=RobBool8     (1) (-X = -Y)=>(X = Y) => Boolean
ROB022=RobBool9     (1) c + -c=c => Boolean
ROB023=RobBool10    (1) X + X=X => Boolean
ROB024=RobBool11    (1) -(a + (a + b)) + -(a + -b) = a => Boolean
ROB025=RobBool12    (1) -(X + Y) = intersection(-X,-Y) => Boolean
ROB026=RobBool13    (1) c + d = c => Boolean
ROB027=RobBool14    (1) -(-c) = c => Boolean
-------------------------------------------------------------------------------
Domain SET = Set Theory (567 abstract problems, 695 problems)
-------------------------------------------------------------------------------
SET001=SupSEl       (1) Set members are superset members
SET002=UnionEqS     (1) A set union itself is itself
SET003=SubSUnion1   (1) A set is a subset of the union of itself with itself
SET004=SubSUnion2   (1) A set is a subset of the union of itself and another set
SET005=IntscAssc    (1) Associativity of set intersection
SET006=IntscSubS    (1) Intersection is a subset
SET007=IntscUnion   (1) Intersection distributes over union
SET008=DiffEl       (1) Difference contains no operand elements
SET009=SubSEqn      (1) If d is a subset of a, then b-a is a subset of b-d
SET010=UnionEqn     (1) c-a union c-b equals c-(the intersection of a and b)
SET011=Diff_Intsc   (1) A property of difference and intersection
SET012=CpmtIvln     (4) Complement is an involution
SET013=IntscComm    (4) The intersection of sets is commutative
SET014=UnionOfSubS  (3) Union of subsets is a subset
SET015=UnionComm    (4) The union of sets is commutative
SET016=1stCpntsEq   (4) First components of equal ordered pairs are equal
SET017=UOrdPrLCanc  (4) Left cancellation for non-ordered pairs
SET018=2ndCpntsEq   (5) Second components of equal ordered pairs are equal
SET019=SetsEq       (2) Two sets that contain one another are equal
SET020=1stUnq       (4) 1st is unique when x is an ordered pair of sets
SET021=2ndUnq       (4) 2nd is unique when x is an ordered pair of sets
SET022=1stCpntSet   (2) The first component of an ordered pair is a little set
SET023=2ndCpntSet   (2) The second component of an ordered pair is a little set
SET024=SetInSgtn    (4) A set belongs to its singleton
SET025=OrdPrSet     (6) Ordered pairs are little sets
SET027=SubSTrans    (4) Transitivity of subset
SET028=Apply_Img1   (2) Relationship between apply and image, part 1 of 2
SET029=Apply_Img2   (2) Relationship between apply and image, part 2 of 2
SET030=FuncValSet   (3) Function values are little sets
SET031=CpsnRel      (2) The composition of two sets is a relation
SET032=RngCpsn      (3) Range of composition
SET033=DomCpsn      (3) Domain of composition
SET034=CpsnFuncs    (3) The composition of functions is a function
SET035=MapCpsn      (3) Maps for composition
SET036=ApplyFunc1   (3) Properties of apply for functions, part 1 of 3
SET037=ApplyFunc2   (3) Properties of apply for functions, part 2 of 3
SET038=ApplyFunc3   (3) Properties of apply for functions, part 3 of 3
SET039=ApplyCpsn1   (2) Properties of apply for composition of functions, 1 of 3
SET040=ApplyCpsn2   (3) Properties of apply for composition of functions, 2 of 3
SET041=ApplyCpsn3   (3) Properties of apply for composition of functions, 3 of 3
SET042=OrdPrXProd   (2) Ordered pairs are in cross products
SET043=Russell      (1) Russell's Paradox
SET044=ARussellSet  (1) Anti-Russell Sets
SET045=NotUnivSet   (1) No Universal Set
SET046=NotCirc      (1) No set of non-circular sets
SET047=EqSymm       (1) Set equality is symmetric
SET050=UnOrdPrAxCor1    (1) Corollary to Unordered pair axiom
SET051=UnOrdPrAxCor2    (1) Corollary to Unordered pair axiom
SET052=XProdAxCor1  (1) Corollary to Cartesian product axiom
SET053=XProdAxCor2  (1) Corollary to Cartesian product axiom
SET054=SubCRefl     (2) Subclass is reflexive
SET055=EqRefl       (2) Equality is reflexive
SET056=EqDef1       (2) Expanded equality definition
SET057=EqDef2       (2) Expanded equality definition
SET058=EqDef3       (2) Expanded equality definition
SET059=EqDef4       (2) Expanded equality definition
SET060=IntscEmpty   (2) Nothing in the intersection of a set and its complement
SET061=NullClEx     (2) Existence of the null class
SET062=NullClSubCl  (2) The null class is a subclass of every class
SET063=NullClSubClCor1  (2) Corollary to the null class being a subclass of every class
SET064=NullClUnq    (2) The null class is unique
SET065=NullClSet    (2) The null class is a set
SET066=UOrdPrComm   (2) Unordered pair is commutative
SET067=UOrdPrArg1   (2) Proper class in an unordered pair, part 1
SET068=UOrdPrArg2   (2) Proper class in an unordered pair, part 2
SET069=UOrdPrArg3   (2) Proper class in an unordered pair, part 3
SET070=UOrdPrArg4   (2) Proper class in an unordered pair, part 4
SET071=NullUOrdPr   (2) Null unordered pair
SET072=UOrdPrRCanc  (2) Right cancellation for unordered pairs
SET073=UnOrdPrAxCor3    (2) Corollary to unordered pair axiom
SET074=UnOrdPrAxCor4    (2) Corollary to unordered pair axiom
SET075=UnOrdPrAxCor5    (2) Corollary to unordered pair axiom
SET076=UOrdPrSubS   (2) Unorderd pair is a subset
SET077=SgtnSet      (2) Every singleton is a set
SET078=SgtnSetCor1  (2) Corollary to every singleton is a set
SET079=SetInSgtnCor1    (2) Corollary to a set belongs to its singleton
SET080=SetInSgtnCor2    (2) Corollary to a set belongs to its singleton
SET081=ElOfSgtn     (2) Only the element can belong to its singleton
SET082=SngtOfNonSet (2) The singleton of a non-set is the null class
SET083=SgtnDepEl1   (2) A singleton set depends on its element, part 1
SET084=SgtnDepEl2   (2) A singleton set depends on its element, part 2
SET085=UOrdPrSgtn   (2) Unordered pair that is a singleton
SET086=SgtnEl1      (2) A singleton set has a member, part 1
SET087=SgtnEl2      (2) A singleton set has a member, part 2
SET088=SgtnEl3      (2) A singleton set has a member, part 3
SET089=SgtnEl4      (2) A singleton set has a member, part 4
SET090=SgtnElUnq    (2) The member of a singleton set is unique
SET091=MembUnq1     (2) Member_of(X) is unique if X is not a singleton, part 1
SET092=MembUnq2     (2) Member_of(X) is unique if X is not a singleton, part 2
SET093=SgtnSetCor2  (2) Corollary to every singleton is a set
SET094=SgtnEqn1     (2) Property 1 of singleton sets
SET095=SgtnEqn2     (2) Property 2 of singleton sets
SET096=SubSOfSgtn   (2) There are at most two subsets of a singleton set
SET097=ClElEx       (2) A class contains 0, 1, or at least 2 members
SET098=ClElExCor1   (2) Corollary 1 to a class contains 0, 1, or at least 2 members
SET099=ClElExCor2   (2) Corollary 2 to a class contains 0, 1, or at least 2 members
SET100=Sgtn_OrdPr   (2) The relationship of singleton sets to ordered pairs
SET101=SgtnElOrdPr  (2) Singleton of the first is a member of an ordered pair
SET102=OrdPrElOrdPr (2) Ordered pair member of ordered pair
SET103=OrdPrEl1     (2) Special member 1 of an ordered pair
SET104=OrdPrEl2     (2) Special member 2 of an ordered pair
SET105=OrdPrEl3     (2) Special member 3 of an ordered pair
SET108=1st2ndOrdPr  (2) 1st and 2nd make the ordered pair
SET109=1stOrdPr1    (2) 1st is the ordered pair, first condition
SET110=2ndOrdPr1    (2) 2nd is the ordered pair, first condition
SET111=1stOrdPr2    (2) 1st is the ordered pair, second condition
SET112=2ndOrdPr2    (2) 2nd is the ordered pair, second condition
SET113=1stUnq1      (2) 1st is unique if x is not an ordered pair of sets, part 1
SET114=2ndUnq1      (2) 2nd is unique if x is not an ordered pair of sets, part 1
SET115=1stUnq2      (2) 1st is unique if x is not an ordered pair of sets, part 2
SET116=2ndUnq2      (2) 2nd is unique if x is not an ordered pair of sets, part 2
SET117=OrdPrSetCor1 (2) Corollary 1 to every ordered pair being a set
SET118=OrdPrSetCor2 (2) Corollary 2 to every ordered pair being a set
SET119=OrdPrCpntsEqCor1 (2) Corollary 1 to components of equal ordered pairs being equal
SET120=OrdPrCpntsEqCor2 (2) Corollary 2 to components of equal ordered pairs being equal
SET121=OrdPrCpntsEqCor3 (2) Corollary 3 to components of equal ordered pairs being equal
SET122=OrdPrCpntsEqCor4 (2) Corollary 4 to components of equal ordered pairs being equal
SET123=SetBAltDef1  (1) Alternative definition of set builder, part 1
SET124=SetBAltDef2  (1) Alternative definition of set builder, part 2
SET125=SetBAltDef3  (1) Alternative definition of set builder, part 3
SET126=SetB_Sgtn    (1) Relation to singleton
SET127=SetB_UOrdPr  (1) Relation to unordered pair
SET128=SetB3        (1) Building a triple
SET129=SetB3El      (1) Membership in a built unordered triple
SET130=SetB3El1     (1) Membership in unordered triple, part 1
SET131=SetB3El2     (1) Membership in unordered triple, part 2
SET132=SetB3El3     (1) Membership in unordered triple, part 3
SET133=SetB3Cor1    (1) Corollary 1 to membership in unordered triple
SET134=SetB3Cor2    (1) Corollary 2 to membership in unordered triple
SET135=SetB3Cor3    (1) Corollary 3 to membership in unordered triple
SET136=SetB3Cor4    (1) Corollary 4 to membership in unordered triple
SET137=SetB3Fix1    (1) Kludge 1 to instantiate variables in unordered triples
SET138=SetB3Fix2    (1) Kludge 2 to instantiate variables in unordered triples
SET139=SetB3Rdcn1   (1) Triple reduction 1
SET140=SetB3Rdcn2   (1) Triple reduction 2
SET141=SetB3Rdcn3   (1) Triple reduction 3
SET142=SetBOrd      (1) Lexical ordering in unordered triples is irrelevant
SET143=IntscAssc    (1) Associativity of intersection
SET144=IntscComm1   (1) Commutativity of intersection
SET145=IntscComm2   (1) Commutativity outside intersection
SET146=IntscNull    (1) Intersection with null class
SET147=IntscId      (1) Universal class is identity for intersection
SET148=IntscIdem    (1) Idempotency of intersection
SET149=IntscIdemCor (1) Corollary to idempotency of intersection
SET150=CpmtIvln     (1) Complement is an involution
SET151=CpmtNull     (1) Complement of null class is universal class
SET152=CpmtUniv     (1) Complement of universal class is null class
SET153=IntscCpmt    (1) Intersection with complement is null class
SET154=UnionCpmt    (1) Union with complement is universal class
SET155=DeMorgan1    (1) De Morgans law 1
SET156=DeMorgan2    (1) De Morgans law 2
SET157=CpmtUnq      (1) Complement is unique
SET158=CpmtAxCor    (1) Corollary to complement axiom
SET159=UnionAssc    (1) Associativity of union
SET160=UnionComm1   (1) Commutativity of union
SET161=UnionComm2   (1) Commutativity outside union
SET162=UnionId      (1) Null class is identity for union
SET163=UnionUniv    (1) Union with universal class
SET164=UnionIdem    (1) Idempotency of union
SET165=UnionIdemCor (1) Corollary to idempotency of union
SET166=UnionEl1     (1) Members of union 1
SET167=UnionEl2     (1) Members of union 2
SET168=UnionEl3     (1) Members of union 3
SET169=IntscUnion1  (1) Distribution of intersection over union 1
SET170=IntscUnion2  (1) Distribution of intersection over union 2
SET171=UnionIntsc1  (1) Distribution of union over intersection 1
SET172=UnionIntsc2  (1) Distribution of union over intersection 2
SET173=IntscAbsb    (1) Absorbtion for intersection
SET174=IntscAbsbCor (1) Corollary to absorbtion for intersection
SET175=UnionAbsb    (1) Absorbtion for union
SET176=UnionAbsbCor (1) Corollary to absorbtion for union
SET177=DistEqn1     (1) Distribution property 1
SET178=DistEqn1Cor1 (1) Corollary 1 to distribution property 1
SET179=DistEqn1Cor2 (1) Corollary 2 to distribution property 1
SET180=DistEqn2     (1) Distribution property 2
SET181=DistEqn2Cor  (1) Corollary to distribution property 2
SET182=DistEqn3     (1) Distribution property 3
SET183=SubCEqn1     (1) Subclass property 1
SET184=SubCEqn2     (1) Subclass property 2
SET185=SubCEqn3     (1) Subclass property 3
SET186=SubCEqn4     (1) Subclass property 4
SET187=SubCEqn5     (1) Subclass property 5
SET188=SubCEqn6     (1) Subclass property 6
SET189=SubCEqn6Cor  (1) Corollary to subclass property 6
SET190=SubCEqn7     (1) Subclass property 7
SET191=SubCEqn8     (1) Subclass property 8
SET192=SubCEqn9     (1) Subclass property 9
SET193=SubCEqn10    (1) Subclass property 10
SET194=LattUpBnd1   (1) Lattice upper bound 1
SET195=LattUpBnd2   (1) Lattice upper bound 2
SET196=LattLowBnd1  (1) Lattice lower bound 1
SET197=LattLowBnd2  (1) Lattice lower bound 2
SET198=MinUpBnd     (1) Least upper bound
SET199=MaxLowBnd    (1) Greatest lower bound
SET200=UnionMono    (1) Union is monotonic
SET201=IntscMono    (1) Intersection is monotonic
SET202=XProdEqn1    (1) Cross product property 1
SET203=XProdEqn1Cor (1) Corollary to cross product product property 1
SET204=XProdEqn2    (1) Cross product property 2
SET205=XProdNull1   (1) Cross product with null class 1
SET206=XProdNull2   (1) Cross product with null class 2
SET207=XProdEqn3    (1) Cross product property 3
SET208=XProdMono1   (1) Cross product is monotonic 1
SET209=XProdMono2   (1) Cross product is monotonic 2
SET210=XProdMonoCor1    (1) Corollary 1 to cross product product monotonicity
SET211=XProdMonoCor2    (1) Corollary 2 to cross product product monotonicity
SET212=XProdMonoCor3    (1) Corollary 3 to cross product product monotonicity
SET213=XProdMonoCor4    (1) Corollary 4 to cross product product monotonicity
SET214=XProdMonoCor5    (1) Corollary 5 to cross product product monotonicity
SET215=XProdMonoCor6    (1) Corollary 6 to cross product product monotonicity
SET216=XProdMonoCor7    (1) Corollary 7 to cross product product monotonicity
SET217=XProdMonoCor8    (1) Corollary 8 to cross product product monotonicity
SET218=XProdUnion1  (1) Cross product distributes over union 1
SET219=XProdUnion2  (1) Cross product distributes over union 2
SET220=XProdIntsc1  (1) Cross product distributes over intersection 1
SET221=XProdIntsc2  (1) Cross product distributes over intersection 2
SET222=XProdEqn4    (1) Cross product property 4
SET223=XProdEqn5    (1) Cross product property 5
SET224=XProd2Dist   (1) Cross product double distribution for intersection
SET225=InvSqrXProd  (1) Inverse of cross product squared
SET226=XProdLCanc1  (1) Cross product left cancellation 1
SET227=XProdLCanc2  (1) Cross product left cancellation 2
SET228=XProdRCanc1  (1) Cross product right cancellation 1
SET229=XProdRCanc2  (1) Cross product right cancellation 2
SET230=XProdCancCor (1) Corollary to cross product cancellation
SET231=XProdEqn6    (1) Cross product property 6
SET232=XProdEqn7    (1) Cross product property 7
SET233=XProdEqn8    (1) Cross product property 8
SET234=XProdEqn9    (1) Cross product property 9
SET235=XProdEqn10   (1) Cross product property 10
SET236=XProdEqn11   (1) Cross product property 11
SET237=RstnAltDef1  (1) Restriction alternate definition 1
SET238=RstnAltDef1Cor   (1) Corollary to restriction alternate definition 1
SET239=RstnAltDef2  (1) Restriction alternate definition 2
SET240=RstnAltDef3  (1) Restriction alternate definition 3
SET241=RstnAltDef4  (1) Restriction alternate definition 4
SET242=RstnAltDef5  (1) Restriction alternate definition 5
SET243=RstnEqn1     (1) Restriction property 1
SET244=RstnUnivCl   (1) Restriction with universal class
SET245=RstnNullCl1  (1) Restriction with null class 1
SET246=RstnNullCl2  (1) Restriction with null class 2
SET247=RstnNullCl3  (1) Restriction with null class 3
SET248=RstnIntsc    (1) Restriction preserves intersections
SET249=RstnEqn2     (1) Restriction property 2
SET250=RstnEqn2Cor  (1) Corollary to restriction property 2
SET251=RstdElRel1   (1) Restriction of element relation, part 1
SET252=RstnEqn3     (1) Restriction property 3
SET253=RstnEqn4     (1) Restriction property 4
SET254=RstnMono1    (1) Monotonicity of restriction 1
SET255=RstnMono2    (1) Monotonicity of restriction 2
SET256=RstnMono3    (1) Monotonicity of restriction 3
SET257=RstnEqn5     (1) Restriction property 5
SET258=DomAltDef1   (1) Domain alternate definition 1
SET259=DomAltDef2   (1) Domain alternate definition 2
SET260=DomAltDef3   (1) Domain alternate definition 3
SET261=DomOfNullCl  (1) Domain of null class is the null class
SET262=DomOfUnivCl  (1) Domain of universal class is the universal class
SET263=DomUnion     (1) Domain preserves union
SET264=DomMono1     (1) Domain is monotonic 1
SET265=DomMono2     (1) Domain is monotonic 2
SET266=DomMono3     (1) Domain is monotonic 3
SET267=DomMono4     (1) Domain is monotonic 4
SET268=DomEqn1      (1) Domain property 1
SET269=DomPrs       (1) Domain only considers ordered pairs
SET270=DomEqn2      (1) Domain property 2
SET271=DomEqn2Cor   (1) Corollary to domain property 2
SET272=DomEqn3      (1) Domain property 3
SET273=DomEqn3Cor   (1) Corollary to domain property 3
SET274=DomEqn4      (1) Domain property 4
SET275=DomEqn4Cor1  (1) Corollary 1 to domain property 4
SET276=DomEqn4Cor2  (1) Corollary 2 to domain property 4
SET277=DomEqn4Cor3  (1) Corollary 3 to domain property 4
SET278=DomEqn4Cor4  (1) Corollary 4 to domain property 4
SET279=DomEqn5      (1) Domain property 5
SET280=DomEqn6      (1) Domain property 6
SET281=DomRelFunc   (1) Domain relation is a function
SET282=DomOfDomRel  (1) Domain of domain relation
SET283=ApplyDomRel  (1) Apply domain relation
SET284=ImgOfDomRel  (1) Image of domain relation
SET285=DomEqn7      (1) Domain property 7
SET286=DomEqn7Cor   (1) Corollary to domain property 7
SET287=DomEqn8      (1) Domain property 8
SET288=DomEqn9      (1) Domain property 9
SET289=GodelAx1     (1) Proof of Goedel's axiom B6, part 1
SET290=GodelAx2     (1) Proof of Goedel's axiom B6, part 2
SET291=GodelAx3     (1) Proof of Goedel's axiom B6, part 3
SET292=InvNullCl    (1) Inverse of null class is the null class
SET293=InvUnivCl    (1) Inverse of universal class is the universal class
SET294=InvUnion     (1) Inverse distributes over union
SET295=InvIntsc     (1) Inverse distributes over intersection
SET296=DomOfInv     (1) Domain of inverse
SET297=RngOfInv     (1) Range of inverse
SET298=InvOfCpmt    (1) Inverse of complement
SET299=InvOfProd    (1) Inverse of product
SET300=InvOfInv     (1) Inverse of inverse
SET301=IncRstn      (1) Inverse commutes with restriction
SET302=RngAltDef1   (1) Range alternate definition 1
SET303=RngAltDef2   (1) Range alternate definition 2
SET304=RngAltDef3   (1) Range alternate definition 3
SET305=RngOfNullCl  (1) Range of null class is the null class
SET306=RngOfUnivCl  (1) Range of universal class is the universal class
SET307=RngUnion     (1) Range preserves union
SET308=RngMono1     (1) Monotonicity of range 1
SET309=RngMono2     (1) Monotonicity of range 2
SET310=RngMono3     (1) Monotonicity of range 3
SET311=RngEqn1      (1) Range property 1
SET312=RngOrdPrs    (1) Range only considers ordered pairs
SET313=RngEqn2      (1) Range property 2
SET314=RngEqn3      (1) Range property 3
SET315=RngEqn3Cor   (1) Corollary to range property 3
SET316=RngEqn4      (1) Range property 4
SET317=RngEqn4Cor1  (1) Corollary 1 to range property 4
SET318=RngEqn4Cor2  (1) Corollary 2 to range property 4
SET319=RngEqn4Cor3  (1) Corollary 3 to range property 4
SET320=RngEqn4Cor4  (1) Corollary 4 to range property 4
SET321=RngEqn5      (1) Range property 5
SET322=RngEqn6      (1) Range property 6
SET323=RngEqn7      (1) Range property 7
SET324=ImgAltDef1   (1) Image alternate definition 1
SET325=ImgAltDef2   (1) Image alternate definition 2
SET326=ImgAltDef2Cor    (1) Corollary to image alternate definition 2
SET327=ImgAltDef3   (1) Image alternate definition 3
SET328=ImgAltDef3Cor    (1) Corollary to image alternate definition 3
SET329=ImgAltDef4   (1) Image alternate definition 4
SET330=ImgAltDef4Cor    (1) Corollary to image alternate definition 4
SET331=RngImgDom    (1) Range is image of the domain
SET332=RngImgDomCor (1) Corollary to range is image of domain
SET333=ImgMono1     (1) Monotonicity of image 1
SET334=ImgMono2     (1) Monotonicity of image 2
SET335=ImgEqn1      (1) Image property 1
SET336=ImgEqn1Cor1  (1) Corollary 1 image property 1
SET337=ImgEqn1Cor2  (1) Corollary 2 image property 1
SET338=ImgEqn1Cor3  (1) Corollary 3 image property 1
SET339=SubCAltDef1  (1) Subclass alternate definition 1
SET340=SubCAltDef2  (1) Subclass alternate definition 2
SET341=ImgUnivCl    (1) Image under universal class
SET342=ImgOfUnion   (1) Image of union
SET343=ImgOfIntsc   (1) Image of intersection
SET344=SumClAltDef1 (1) Sum class alternate definition 1
SET345=SumClAltDef2 (1) Sum class alternate definition 2
SET346=SumClAltDef3 (1) Sum class alternate definition 3
SET347=SumClOfNullCl    (1) Sum class of null class is null class
SET348=SumClOfUnivCl    (1) Sum class of universal class is universal class
SET349=SumClOfSgtnNull1 (1) Sum class of singleton null is null class 1
SET350=SumClOfSgtnNull2 (1) Sum class of singleton null is null class 2
SET351=SumClSgtn    (1) Sum of singleton
SET352=SumClPr      (1) Sum of pair
SET353=SumClPrCor   (1) Corollary to sum of pair
SET354=SumClOrdPr   (1) Sum of ordered pair
SET355=SubCUnion    (1) An element of a class is a subclass of union
SET356=SubCUnionCor (1) Corollary to subclass of union
SET357=SumClAltDef4 (1) Sum class alternate definition 4
SET358=SumClUnion   (1) Sum distributes over union
SET359=SumClEqn1    (1) Sum class property 1
SET360=DomSumClSqr  (1) Domain is sum squared
SET361=RngSumClSqr  (1) Range is sum squared
SET362=SumClMono    (1) Monotonicity of sum
SET363=PwrClAltDef1 (1) Power class alternative definition 1
SET364=PwrClAltDef2 (1) Power class alternative definition 2
SET365=PwrClMono    (1) Monotonicity of power
SET366=NullClElPwrCl    (1) Null class in power class
SET367=PwrClNotNull (1) Power class not in null class
SET368=PwrClOfUnivCl    (1) Power class of universal class is universal class
SET369=PwrClOfSet   (1) Power class of set
SET370=PwrClEqn1    (1) Power class property 1
SET371=PwrClEqn2    (1) Power class property 2
SET372=PwrClEqn3    (1) Power class property 3
SET373=PwrClEqn4    (1) Power class property 4
SET374=PwrClClsdUnion   (1) Power class is closed under union
SET375=PwrClClsdIntsc   (1) Power class is closed under intersection
SET376=PwrClSetB    (1) Power class set builder
SET377=PwrClSetBCor1    (1) Corollary 1 to power class set builder
SET378=PwrClSetBCor2    (1) Corollary 2 to power class set builder
SET379=PwrClSetBCor3    (1) Corollary 3 to power class set builder
SET380=RelEqn1      (1) Relation property 1
SET381=RelEqn2      (1) Relation property 2
SET382=RelEqn2Cor1  (1) Corollary 1 to relation property 2
SET383=RelEqn2Cor2  (1) Corollary 2 to relation property 2
SET384=RelEqn3Cor1  (1) Corollary 1 to relation property 3
SET385=RelEqn3Cor2  (1) Corollary 2 to relation property 3
SET386=RelEqn4      (1) Relation property 4
SET387=CmpsnAltDef1 (1) Composition alternate definition 1
SET388=CmpsnAltDef2 (1) Composition alternate definition 2
SET389=CmpsnAltDef3 (1) Composition alternate definition 3
SET390=CmpsnAltDef4 (1) Composition alternate definition 4
SET391=CmpsnEqn1    (1) Composition property 1
SET392=CmpsnRId     (1) Right identity for composition
SET393=CmpsnLId     (1) Left identity for composition
SET394=CmpsnEqn2    (1) Composition property 2
SET395=CmpsnImg     (1) Composition relates to image
SET396=DomOfCmpsn1  (1) Domain of composition 1
SET397=RngOfCmpsn   (1) Range of composition
SET398=CmpsnAssc    (1) Associativity of composition
SET399=LCmpsnNullCl (1) Left compose with null class
SET400=RCmpsnNullCl (1) Right compose with null class
SET401=LCmpsnUnicCl (1) Left compose with universal class
SET402=RCmpsnUnicCl (1) Right compose with universal class
SET403=DomOfCmpsn2  (1) Domain of composition 2
SET404=CmpsnMono1   (1) Monotonicity of composition 1
SET405=CmpsnMono2   (1) Monotonicity of composition 2
SET406=CmpsnMonoCor1    (1) Corollary 1 monotonicity of composition
SET407=CmpsnMonoCor2    (1) Corollary 2 monotonicity of composition
SET408=InvCmpsn     (1) Inverse of composition
SET409=CmpsnElRel1  (1) Composition of element relation 1
SET410=CmpsnElRel2  (1) Composition of element relation 2
SET411=CmpsnSgtnEl1 (1) Compose condition for singleton membership 1
SET412=CmpsnSgtnEl2 (1) Compose condition for singleton membership 2
SET413=CmpsnSgtnEl3 (1) Compose condition for singleton membership 3
SET414=CmpsnUnion   (1) Composition distributes over union
SET415=CmpsnSgtnFunc1   (1) Composition with singleton function 1
SET416=CmpsnSgtnFunc2   (1) Composition with singleton function 2
SET417=CmpsnEqn1    (1) Composition property 1
SET418=CmpsnEqn2    (1) Composition property 2
SET419=CmpsnEqn3    (1) Composition property 3
SET420=CmpsnEqn4    (1) Composition property 4
SET421=CmpsClFunc   (1) Compose class is a function
SET422=CmpsClApply  (1) Compose class and apply
SET423=SumCmpsCl    (1) Sum compose class
SET424=CmpsClCmpsn  (1) Compose class and composition function are related
SET425=SVClAltDef1  (1) Single valued class alternate definition 1
SET426=SVClAltDef2  (1) Single valued class alternate definition 2
SET427=SVClAltDef3  (1) Single valued class alternate definition 3
SET428=SVClAltDef4  (1) Single valued class alternate definition 4
SET429=SubClSVCl    (1) A subclass of a single-valued class is single-valued
SET430=SVClImg      (1) In a single-valued class, each image is a singleton
SET431=CmpsnSVCls   (1) The composition of single-valued classes is single-valued
SET432=FuncAltDef1  (1) Function alternate definition 1
SET433=FuncAltDef2  (1) Function alternate definition 2
SET434=FuncAltDef3  (1) Function alternate definition 3
SET435=FuncAltDef4  (1) Function alternate definition 4
SET436=SubClOfFunc1 (1) Subclass of function is a function, part 1
SET437=SubClOfFunc2 (1) Subclass of function is a function, part 2
SET438=FuncImg      (1) In a function, the image of each domain element is a singleton
SET439=NullClFunc   (1) Null class is a function
SET440=RstnFuncs    (1) The restriction of function is function
SET441=IntscFuncs   (1) The intersection of functions is a function
SET442=RstnFunc     (1) Restriction of function
SET443=DiffFuncs    (1) Difference of functions is a function
SET444=FuncEqn1     (1) Function property 1
SET445=FuncEqn2     (1) Corollary to function property 1
SET446=FuncEqn2Cor  (1) Function property 2
SET447=FuncEqn3     (1) Function property 3
SET448=FuncEqn4     (1) Function property 4
SET449=FuncSubS1    (1) Condition 1 for one function to be a subset of another
SET450=FuncSubS2    (1) Condition 2 for one function to be a subset of another
SET451=SubSRelAltDef1   (1) Subset relation alternate definition 1
SET452=SubSRelAltDef2   (1) Subset relation alternate definition 2
SET453=SubSRelAltDef3   (1) Subset relation alternate definition 3
SET454=IdAltDef1    (1) Identity alternate definition 1
SET455=IdAltDef2    (1) Identity alternate definition 2
SET456=IdAltDef3    (1) Identity alternate definition 3
SET457=IdFunc       (1) Identity is a function
SET458=IdFuncCor    (1) Corollary to identity is a function
SET459=IdDom        (1) Domain of identity is the universal class
SET460=IdRng        (1) Range of identity
SET461=RstdIdDom    (1) Domain of restricted identity
SET462=RstdIdRng    (1) Range of restricted identity
SET463=IdDomRngCor  (1) Corollary to domain and range of identity
SET464=ClImgId      (1) Class image under identity
SET465=Id1to1       (1) Identity is one-to-one
SET466=InvId        (1) Inverse of identity is identity
SET467=Set1El1      (1) Sets with at most one member 1
SET468=Set1El2      (1) Sets with at most one member 2
SET469=Set1El3      (1) Sets with at most one member 3
SET470=Set1ElCor    (1) Corollary to sets with one member
SET471=SetNEl1      (1) Sets with more than one member 1
SET472=SetNEl2      (1) Sets with more than one member 2
SET473=RstdDomLem1  (1) Lemma 1 to restricted domain
SET474=RstdDomLem2  (1) Lemma 2 to restricted domain
SET475=RstdDom      (1) Restricted domain
SET476=IntescCl     (1) Intersection subclass
SET477=AxOfSubs1    (1) Axiom of subsets 1
SET478=AxOfSubs2    (1) Axiom of subsets 2
SET479=RplmtEqn1    (1) Replacement property 1
SET480=RplmtEqn2    (1) Replacement property 2
SET481=RplmtEqn3    (1) Replacement property 3
SET482=RplmtEqn4    (1) Replacement property 4
SET483=RplmtEqn5    (1) Replacement property 5
SET484=RplmtEqn6    (1) Replacement property 6
SET485=RplmtEqn7    (1) Replacement property 7
SET486=RplmtEqn8    (1) Replacement property 8
SET487=RplmtEqn9    (1) Replacement property 9
SET488=RplmtEqn10   (1) Replacement property 10
SET489=RplmtEqn11   (1) Replacement property 11
SET490=RplmtEqn12   (1) Replacement property 12
SET491=DiagnLem1    (1) Diagonalization lemma 1
SET492=DiagnLem2    (1) Diagonalization lemma 2
SET493=DiagnCor     (1) Diagonalization corollary
SET494=DiagnAltDef1 (1) Diagonalization alternate definition 1
SET495=DiagnAltDef2 (1) Diagonalization alternate definition 2
SET496=DiagnAltDef3 (1) Diagonalization alternate definition 3
SET497=RussellCl1   (1) Special case of the Russell class, without the regularity axiom
SET498=RussellCl2   (1) Special case of the Russell class, without the regularity axiom
SET499=RussellClNotSet  (1) The Russell class not a set
SET500=DiagnEqn1    (1) Diagonalization property 1
SET501=DiagnEqn2    (1) Diagonalization property 2
SET502=DiagnEqn3    (1) Diagonalization property 3
SET503=UnivClNotSet (1) The universal class not set
SET504=UnivClNotSetCor1 (1) Corollary 1 to universal class not set
SET505=UnivClNotSetCor2 (1) Corollary 2 to universal class not set
SET506=UnivClNotNullCl  (1) Universal class not null class
SET507=UnivClNotNullSubCl   (1) Universal class not subclass of null class
SET508=SgtnUOrdPrAxCor1 (1) Corollary 1 to singleton in unordered pair axiom
SET509=SgtnUOrdPrAxCor2 (1) Corollary 2 to singleton in unordered pair axiom
SET510=SgtnNullClCor    (1) Corollary to singleton is null class
SET511=OrdPrElCor1  (1) Corollary 1 to special members of ordered pairs
SET512=OrdPrElCor2  (1) Corollary 2 to special members of ordered pairs
SET513=OrdPrElCor3  (1) Corollary 3 to special members of ordered pairs
SET514=OrdPrClNotSet    (1) Class of ordered pairs is not a set
SET515=ClNotClEl    (1) No class belongs to itself
SET516=ClNotClElCor (1) Corollary to no class belongs to itself
SET517=XElXNotSgtn  (1) If member of X is X then X is not a singleton of a set
SET518=No2Cycle     (1) There are no cycles of length 2
SET519=No2CycleCor1 (1) Corollary 1 to no cycles of length 2
SET520=No2CycleCor2 (1) Corollary 2 to no cycles of length 2
SET521=OrdPrCmpts1  (1) Ordered pair determines components 1
SET522=OrdPrCmpts2  (1) Ordered pair determines components 2
SET523=ElCpmtNotSet (1) Element and complement can't both be sets
SET524=NotOrdPr1    (1) Equivalent condition 1 for x not to be an ordered pair
SET525=NotOrdPr2    (1) Equivalent condition 2 for x not to be an ordered pair
SET526=OrdPrCmptSet1    (1) Ordered pair components are sets 1
SET527=OrdPrCmptSet2    (1) Ordered pair components are sets 2
SET528=OrdPrCmptSetCor1 (1) Corollary 1 to ordered pair components are sets
SET529=OrdPrCmptSetCor2 (1) Corollary 2 to ordered pair components are sets
SET530=OrdPrCmptSetCor3 (1) Corollary 3 to ordered pair components are sets
SET531=AppnEqn1     (1) Application property 1
SET532=AppnEqn2     (1) Application property 2
SET533=RngClAppn1   (1) The range of Z is the class of applications of Z to Z's domain 1
SET534=RngClAppn2   (1) The range of Z is the class of applications of Z to Z's domain 2
SET535=AppnEqn3     (1) Application property 3
SET536=AppnEqn3Cor1 (1) Corollary 1 to application property 3
SET537=AppnEqn3Cor2 (1) Corollary 2 to application property 3
SET538=AppnEqn4     (1) Application property 4
SET539=AppnEqn5     (1) Application property 5
SET540=AppnEqn6     (1) Application property 6
SET541=AppnEqn7     (1) Application property 7
SET542=AppnEqn9Cor  (1) Corollary to application property 9
SET543=AppnEqn10Cor (1) Corollary to application property 10
SET544=AppnEqn11Cor (1) Corollary to application property 11
SET545=AppnEqn13    (1) Application special case 1
SET546=AppnEqn14    (1) Application special case 2
SET547=AppnEqn15    (1) Application special case 3
SET548=AppnEqn16    (1) Application property 16
SET549=AppnEqn17    (1) Application property 17
SET550=AppnEqn18    (1) Application property 18
SET551=AppnEqn19    (1) Application property 19
SET552=AppnEqn20    (1) Application property 20
SET553=CantorAltDef1    (1) Cantor class alternate definition 1
SET554=CantorAltDef2    (1) Cantor class alternate definition 2
SET555=CantorAltDef3    (1) Cantor class alternate definition 3
SET556=CantorEqn1   (1) Cantor class property 1
SET557=CantorThm    (1) Cantor's theorem
SET558=CmpblFuncAltDef1 (1) Compatible functions alternate definition 1
SET559=CmpblFuncAltDef2 (1) Compatible functions alternate definition 2
SET560=CmpblFuncAltDef3 (1) Compatible functions alternate definition 3
SET561=CmpblFuncEqn1    (1) Compatible function property 1
SET562=CmpblFuncEqn2    (1) Compatible function property 2
SET563=CmpblFuncEqn3    (1) Compatible function property 3
SET564=CmpblFuncEqn3Cor1    (1) Corollary 1 to compatible function property 3
SET565=CmpblFuncEqn3Cor2    (1) Corollary 2 to compatible function property 3
SET566=CmpblFuncEqn4    (1) Compatible function property 4
SET567=CmpblFunc1   (1) Compatible function special case
-------------------------------------------------------------------------------
Domain SYN = Syntactic (381 abstract problems, 350 problems)
-------------------------------------------------------------------------------
SYN001=Allways      (1) All signed combinations of some propositions.
SYN002=OddEven      (1) Odd and Even Problem
SYN003=Implies1     (1) Implications that form a contradiction
SYN004=Implies2     (1) Implications that form a contradiction
SYN005=Or1          (1) Disjunctions that form a contradiction
SYN006=Splits       (1) A problem to demonstrate controlling splits
SYN007=FPell71      (1) Pelletier Problem 71
SYN008=Relev1       (1) A problem to demonstrate the usefulness of relevancy testing
SYN009=Relev2       (1) A problem to demonstrate the usefulness of relevancy testing
SYN010=Letz         (1) Example for Proposition 5.2 in [Letz, et al., 1994]
SYN011=CRdcn        (1) A problem to demonstrate C-reduction
SYN012=ModelElim    (1) A problem to demonstrate Model Elimination
SYN013=Quant1       (1) A problem in quantification theory
SYN014=Quant2       (2) A problem in quantification theory
SYN015=Quant3       (2) A problem in quantification theory
SYN028=EW1          (1) EW1
SYN029=EW2          (1) EW2
SYN030=EW3          (1) EW3
SYN031=MQW          (1) MQW
SYN032=Ances        (1) Ances
SYN033=DM           (1) DM
SYN034=QW           (1) QW
SYN035=ROB1         (1) ROB1
SYN036=PAndrews     (4) Andrews Challenge Problem
SYN037=PAndrews2    (2) Andrews Challenge Problem Variant
SYN038=SFleisig4    (1) Syntactic formula
SYN039=VLifsch      (1) A challenge to resolution programs
SYN040=FPell01      (1) Pelletier Problem 1
SYN041=FPell03      (1) Pelletier Problem 3, 16
SYN044=FPell10      (1) Pelletier Problem 10
SYN045=FPell13      (1) Pelletier Problem 13
SYN046=FPell15      (1) Pelletier Problem 15
SYN047=FPell17      (1) Pelletier Problem 17
SYN048=FPell18      (1) Pelletier Problem 18
SYN049=FPell19      (1) Pelletier Problem 19
SYN050=FPell20      (1) Pelletier Problem 20
SYN051=FPell21      (1) Pelletier Problem 21
SYN052=FPell22      (1) Pelletier Problem 22
SYN053=FPell23      (1) Pelletier Problem 23
SYN054=FPell24      (1) Pelletier Problem 24
SYN055=FPell25      (1) Pelletier Problem 25
SYN056=FPell26      (1) Pelletier Problem 26
SYN057=FPell27      (1) Pelletier Problem 27
SYN058=FPell28      (1) Pelletier Problem 28
SYN059=FPell29      (1) Pelletier Problem 29
SYN060=FPell30      (1) Pelletier Problem 30
SYN061=FPell31      (1) Pelletier Problem 31
SYN062=FPell32      (1) Pelletier Problem 32
SYN063=FPell33      (2) Pelletier Problem 33
SYN064=FPell35      (1) Pelletier Problem 35
SYN065=FPell36      (1) Pelletier Problem 36
SYN066=FPell37      (1) Pelletier Problem 37
SYN067=FPell38      (3) Pelletier Problem 38
SYN068=FPell44      (1) Pelletier Problem 44
SYN069=FPell45      (1) Pelletier Problem 45
SYN070=FPell46      (1) Pelletier Problem 46
SYN071=FPell48      (1) Pelletier Problem 48
SYN072=FPell49      (1) Pelletier Problem 49
SYN073=FPell50      (1) Pelletier Problem 50
SYN074=FPell51      (1) Pelletier Problem 51
SYN075=FPell52      (1) Pelletier Problem 52
SYN076=FPell53      (1) Pelletier Problem 53
SYN077=FPell54      (1) Pelletier Problem 54
SYN078=FPell56      (1) Pelletier Problem 56
SYN079=FPell57      (1) Pelletier Problem 57
SYN080=FPell58      (1) Pelletier Problem 58
SYN081=FPell59      (1) Pelletier Problem 59
SYN082=FPell60      (1) Pelletier Problem 60
SYN083=FPell61      (1) Pelletier Problem 61
SYN084=FPell62      (2) Pelletier Problem 62
SYN085=DAPs1        (1) Plaisted problem s(1,10)
SYN086=DAPs2        (1) Plaisted problem s(2,3)
SYN087=DAPs3        (1) Plaisted problem s(3,3)
SYN088=DAPs4        (1) Plaisted problem s(4,10)
SYN089=DAPt2        (1) Plaisted problem t(2,2)
SYN090=DAPt3        (1) Plaisted problem t(3,8)
SYN091=DAPsyms2     (1) Plaisted problem sym(s(2,3))
SYN092=DAPsyms3     (1) Plaisted problem sym(s(3,3))
SYN093=DAPut2       (1) Plaisted problem u(t(2,2))
SYN094=DAPut3       (1) Plaisted problem u(t(3,5))
SYN095=DAPmt2       (1) Plaisted problem m(t(2,2))
SYN096=DAPmt3       (1) Plaisted problem m(t(3,8))
SYN097=DAPsymut2    (1) Plaisted problem sym(u(t(2,2)))
SYN098=DAPsymut3    (1) Plaisted problem sym(u(t(3,2)))
SYN099=DAPsymmt2    (1) Plaisted problem sym(m(t(2,3)))
SYN100=DAPsymmt3    (1) Plaisted problem sym(m(t(3,5)))
SYN101=DAPnt2       (1) Plaisted problem n(t(2,2),2)
SYN102=DAPnt3       (1) Plaisted problem n(t(3,7),7)
SYN103=RPT63_QU_1   (1) RPT63 synthetic problem 1 (quasi-uniform distribution)
SYN104=RPT63_QU_2   (1) RPT63 synthetic problem 2 (quasi-uniform distribution)
SYN105=RPT63_QU_3   (1) RPT63 synthetic problem 3 (quasi-uniform distribution)
SYN106=RPT63_QU_4   (1) RPT63 synthetic problem 4 (quasi-uniform distribution)
SYN107=RPT63_QU_5   (1) RPT63 synthetic problem 5 (quasi-uniform distribution)
SYN108=RPT63_QU_6   (1) RPT63 synthetic problem 6 (quasi-uniform distribution)
SYN109=RPT63_QU_7   (1) RPT63 synthetic problem 7 (quasi-uniform distribution)
SYN110=RPT63_QU_8   (1) RPT63 synthetic problem 8 (quasi-uniform distribution)
SYN111=RPT63_QU_9   (1) RPT63 synthetic problem 9 (quasi-uniform distribution)
SYN112=RPT63_QU_10  (1) RPT63 synthetic problem 10 (quasi-uniform distribution)
SYN113=RPT63_QU_11  (1) RPT63 synthetic problem 11 (quasi-uniform distribution)
SYN114=RPT63_QU_12  (1) RPT63 synthetic problem 12 (quasi-uniform distribution)
SYN115=RPT63_QU_13  (1) RPT63 synthetic problem 13 (quasi-uniform distribution)
SYN116=RPT63_QU_14  (1) RPT63 synthetic problem 14 (quasi-uniform distribution)
SYN117=RPT63_QU_15  (1) RPT63 synthetic problem 15 (quasi-uniform distribution)
SYN118=RPT63_QU_16  (1) RPT63 synthetic problem 16 (quasi-uniform distribution)
SYN119=RPT63_QU_17  (1) RPT63 synthetic problem 17 (quasi-uniform distribution)
SYN120=RPT63_QU_18  (1) RPT63 synthetic problem 18 (quasi-uniform distribution)
SYN121=RPT63_QU_19  (1) RPT63 synthetic problem 19 (quasi-uniform distribution)
SYN122=RPT63_QU_20  (1) RPT63 synthetic problem 20 (quasi-uniform distribution)
SYN123=RPT63_QU_21  (1) RPT63 synthetic problem 21 (quasi-uniform distribution)
SYN124=RPT63_QU_22  (1) RPT63 synthetic problem 22 (quasi-uniform distribution)
SYN125=RPT63_QU_23  (1) RPT63 synthetic problem 23 (quasi-uniform distribution)
SYN126=RPT63_QU_24  (1) RPT63 synthetic problem 24 (quasi-uniform distribution)
SYN127=RPT63_QU_25  (1) RPT63 synthetic problem 25 (quasi-uniform distribution)
SYN128=RPT63_QU_26  (1) RPT63 synthetic problem 26 (quasi-uniform distribution)
SYN129=RPT63_QU_27  (1) RPT63 synthetic problem 27 (quasi-uniform distribution)
SYN130=RPT63_QU_28  (1) RPT63 synthetic problem 28 (quasi-uniform distribution)
SYN131=RPT63_QU_29  (1) RPT63 synthetic problem 29 (quasi-uniform distribution)
SYN132=RPT63_QU_30  (1) RPT63 synthetic problem 30 (quasi-uniform distribution)
SYN133=RPT63_QU_31  (1) RPT63 synthetic problem 31 (quasi-uniform distribution)
SYN134=RPT63_QU_32  (1) RPT63 synthetic problem 32 (quasi-uniform distribution)
SYN135=RPT63_QU_33  (1) RPT63 synthetic problem 33 (quasi-uniform distribution)
SYN136=RPT63_QU_34  (1) RPT63 synthetic problem 34 (quasi-uniform distribution)
SYN137=RPT63_QU_35  (1) RPT63 synthetic problem 35 (quasi-uniform distribution)
SYN138=RPT63_QU_36  (1) RPT63 synthetic problem 36 (quasi-uniform distribution)
SYN139=RPT63_QU_37  (1) RPT63 synthetic problem 37 (quasi-uniform distribution)
SYN140=RPT63_QU_38  (1) RPT63 synthetic problem 38 (quasi-uniform distribution)
SYN141=RPT63_QU_39  (1) RPT63 synthetic problem 39 (quasi-uniform distribution)
SYN142=RPT63_QU_40  (1) RPT63 synthetic problem 40 (quasi-uniform distribution)
SYN143=RPT63_QU_41  (1) RPT63 synthetic problem 41 (quasi-uniform distribution)
SYN144=RPT63_QU_42  (1) RPT63 synthetic problem 42 (quasi-uniform distribution)
SYN145=RPT63_QU_43  (1) RPT63 synthetic problem 43 (quasi-uniform distribution)
SYN146=RPT63_QU_44  (1) RPT63 synthetic problem 44 (quasi-uniform distribution)
SYN147=RPT63_QU_45  (1) RPT63 synthetic problem 45 (quasi-uniform distribution)
SYN148=RPT63_QU_46  (1) RPT63 synthetic problem 46 (quasi-uniform distribution)
SYN149=RPT63_QU_47  (1) RPT63 synthetic problem 47 (quasi-uniform distribution)
SYN150=RPT63_QU_48  (1) RPT63 synthetic problem 48 (quasi-uniform distribution)
SYN151=RPT63_QU_49  (1) RPT63 synthetic problem 49 (quasi-uniform distribution)
SYN152=RPT63_QU_50  (1) RPT63 synthetic problem 50 (quasi-uniform distribution)
SYN153=RPT63_QU_51  (1) RPT63 synthetic problem 51 (quasi-uniform distribution)
SYN154=RPT63_QU_52  (1) RPT63 synthetic problem 52 (quasi-uniform distribution)
SYN155=RPT63_QU_53  (1) RPT63 synthetic problem 53 (quasi-uniform distribution)
SYN156=RPT63_QU_54  (1) RPT63 synthetic problem 54 (quasi-uniform distribution)
SYN157=RPT63_QU_55  (1) RPT63 synthetic problem 55 (quasi-uniform distribution)
SYN158=RPT63_QU_56  (1) RPT63 synthetic problem 56 (quasi-uniform distribution)
SYN159=RPT63_QU_57  (1) RPT63 synthetic problem 57 (quasi-uniform distribution)
SYN160=RPT63_QU_58  (1) RPT63 synthetic problem 58 (quasi-uniform distribution)
SYN161=RPT63_QU_59  (1) RPT63 synthetic problem 59 (quasi-uniform distribution)
SYN162=RPT63_QU_60  (1) RPT63 synthetic problem 60 (quasi-uniform distribution)
SYN163=RPT63_QU_61  (1) RPT63 synthetic problem 61 (quasi-uniform distribution)
SYN164=RPT63_QU_62  (1) RPT63 synthetic problem 62 (quasi-uniform distribution)
SYN165=RPT63_QU_63  (1) RPT63 synthetic problem 63 (quasi-uniform distribution)
SYN166=RPT63_QU_64  (1) RPT63 synthetic problem 64 (quasi-uniform distribution)
SYN167=RPT63_QU_65  (1) RPT63 synthetic problem 65 (quasi-uniform distribution)
SYN168=RPT63_QU_66  (1) RPT63 synthetic problem 66 (quasi-uniform distribution)
SYN169=RPT63_QU_67  (1) RPT63 synthetic problem 67 (quasi-uniform distribution)
SYN170=RPT63_QU_68  (1) RPT63 synthetic problem 68 (quasi-uniform distribution)
SYN171=RPT63_QU_69  (1) RPT63 synthetic problem 69 (quasi-uniform distribution)
SYN172=RPT63_QU_70  (1) RPT63 synthetic problem 70 (quasi-uniform distribution)
SYN173=RPT63_QU_71  (1) RPT63 synthetic problem 71 (quasi-uniform distribution)
SYN174=RPT63_QU_72  (1) RPT63 synthetic problem 72 (quasi-uniform distribution)
SYN175=RPT63_QU_73  (1) RPT63 synthetic problem 73 (quasi-uniform distribution)
SYN176=RPT63_QU_74  (1) RPT63 synthetic problem 74 (quasi-uniform distribution)
SYN177=RPT63_QU_75  (1) RPT63 synthetic problem 75 (quasi-uniform distribution)
SYN178=RPT63_QU_76  (1) RPT63 synthetic problem 76 (quasi-uniform distribution)
SYN179=RPT63_QU_77  (1) RPT63 synthetic problem 77 (quasi-uniform distribution)
SYN180=RPT63_QU_78  (1) RPT63 synthetic problem 78 (quasi-uniform distribution)
SYN181=RPT63_QU_79  (1) RPT63 synthetic problem 79 (quasi-uniform distribution)
SYN182=RPT63_QU_80  (1) RPT63 synthetic problem 80 (quasi-uniform distribution)
SYN183=RPT63_QU_81  (1) RPT63 synthetic problem 81 (quasi-uniform distribution)
SYN184=RPT63_QU_82  (1) RPT63 synthetic problem 82 (quasi-uniform distribution)
SYN185=RPT63_QU_83  (1) RPT63 synthetic problem 83 (quasi-uniform distribution)
SYN186=RPT63_QU_84  (1) RPT63 synthetic problem 84 (quasi-uniform distribution)
SYN187=RPT63_QU_85  (1) RPT63 synthetic problem 85 (quasi-uniform distribution)
SYN188=RPT63_QU_86  (1) RPT63 synthetic problem 86 (quasi-uniform distribution)
SYN189=RPT63_QU_87  (1) RPT63 synthetic problem 87 (quasi-uniform distribution)
SYN190=RPT63_QU_88  (1) RPT63 synthetic problem 88 (quasi-uniform distribution)
SYN191=RPT63_QU_89  (1) RPT63 synthetic problem 89 (quasi-uniform distribution)
SYN192=RPT63_QU_90  (1) RPT63 synthetic problem 90 (quasi-uniform distribution)
SYN193=RPT63_QU_91  (1) RPT63 synthetic problem 91 (quasi-uniform distribution)
SYN194=RPT63_QU_92  (1) RPT63 synthetic problem 92 (quasi-uniform distribution)
SYN195=RPT63_QU_93  (1) RPT63 synthetic problem 93 (quasi-uniform distribution)
SYN196=RPT63_QU_94  (1) RPT63 synthetic problem 94 (quasi-uniform distribution)
SYN197=RPT63_QU_95  (1) RPT63 synthetic problem 95 (quasi-uniform distribution)
SYN198=RPT63_QU_96  (1) RPT63 synthetic problem 96 (quasi-uniform distribution)
SYN199=RPT63_QU_97  (1) RPT63 synthetic problem 97 (quasi-uniform distribution)
SYN200=RPT63_QU_98  (1) RPT63 synthetic problem 98 (quasi-uniform distribution)
SYN201=RPT63_QU_99  (1) RPT63 synthetic problem 99 (quasi-uniform distribution)
SYN202=RPT63_QU_100 (1) RPT63 synthetic problem 100 (quasi-uniform distribution)
SYN203=RPT63_QU_101 (1) RPT63 synthetic problem 101 (quasi-uniform distribution)
SYN204=RPT63_QU_102 (1) RPT63 synthetic problem 102 (quasi-uniform distribution)
SYN205=RPT63_QU_103 (1) RPT63 synthetic problem 103 (quasi-uniform distribution)
SYN206=RPT63_QU_104 (1) RPT63 synthetic problem 104 (quasi-uniform distribution)
SYN207=RPT63_QU_105 (1) RPT63 synthetic problem 105 (quasi-uniform distribution)
SYN208=RPT63_QU_106 (1) RPT63 synthetic problem 106 (quasi-uniform distribution)
SYN209=RPT63_QU_107 (1) RPT63 synthetic problem 107 (quasi-uniform distribution)
SYN210=RPT63_QU_108 (1) RPT63 synthetic problem 108 (quasi-uniform distribution)
SYN211=RPT63_QU_109 (1) RPT63 synthetic problem 109 (quasi-uniform distribution)
SYN212=RPT63_QU_110 (1) RPT63 synthetic problem 110 (quasi-uniform distribution)
SYN213=RPT63_QU_111 (1) RPT63 synthetic problem 111 (quasi-uniform distribution)
SYN214=RPT63_QU_112 (1) RPT63 synthetic problem 112 (quasi-uniform distribution)
SYN215=RPT63_QU_113 (1) RPT63 synthetic problem 113 (quasi-uniform distribution)
SYN216=RPT63_SK_1   (1) RPT63 synthetic problem 1 (skewed distribution)
SYN217=RPT63_SK_2   (1) RPT63 synthetic problem 2 (skewed distribution)
SYN218=RPT63_SK_3   (1) RPT63 synthetic problem 3 (skewed distribution)
SYN219=RPT63_SK_4   (1) RPT63 synthetic problem 4 (skewed distribution)
SYN220=RPT63_SK_5   (1) RPT63 synthetic problem 5 (skewed distribution)
SYN221=RPT63_SK_6   (1) RPT63 synthetic problem 6 (skewed distribution)
SYN222=RPT63_SK_7   (1) RPT63 synthetic problem 7 (skewed distribution)
SYN223=RPT63_SK_8   (1) RPT63 synthetic problem 8 (skewed distribution)
SYN224=RPT63_SK_9   (1) RPT63 synthetic problem 9 (skewed distribution)
SYN225=RPT63_SK_10  (1) RPT63 synthetic problem 10 (skewed distribution)
SYN226=RPT63_SK_11  (1) RPT63 synthetic problem 11 (skewed distribution)
SYN227=RPT63_SK_12  (1) RPT63 synthetic problem 12 (skewed distribution)
SYN228=RPT63_SK_13  (1) RPT63 synthetic problem 13 (skewed distribution)
SYN229=RPT63_SK_14  (1) RPT63 synthetic problem 14 (skewed distribution)
SYN230=RPT63_SK_15  (1) RPT63 synthetic problem 15 (skewed distribution)
SYN231=RPT63_SK_16  (1) RPT63 synthetic problem 16 (skewed distribution)
SYN232=RPT63_SK_17  (1) RPT63 synthetic problem 17 (skewed distribution)
SYN233=RPT63_SK_18  (1) RPT63 synthetic problem 18 (skewed distribution)
SYN234=RPT63_SK_19  (1) RPT63 synthetic problem 19 (skewed distribution)
SYN235=RPT63_SK_20  (1) RPT63 synthetic problem 20 (skewed distribution)
SYN236=RPT63_SK_21  (1) RPT63 synthetic problem 21 (skewed distribution)
SYN237=RPT63_SK_22  (1) RPT63 synthetic problem 22 (skewed distribution)
SYN238=RPT63_SK_23  (1) RPT63 synthetic problem 23 (skewed distribution)
SYN239=RPT63_SK_24  (1) RPT63 synthetic problem 24 (skewed distribution)
SYN240=RPT63_SK_25  (1) RPT63 synthetic problem 25 (skewed distribution)
SYN241=RPT63_SK_26  (1) RPT63 synthetic problem 26 (skewed distribution)
SYN242=RPT63_SK_27  (1) RPT63 synthetic problem 27 (skewed distribution)
SYN243=RPT63_SK_28  (1) RPT63 synthetic problem 28 (skewed distribution)
SYN244=RPT63_SK_29  (1) RPT63 synthetic problem 29 (skewed distribution)
SYN245=RPT63_SK_30  (1) RPT63 synthetic problem 30 (skewed distribution)
SYN246=RPT63_SK_31  (1) RPT63 synthetic problem 31 (skewed distribution)
SYN247=RPT63_SK_32  (1) RPT63 synthetic problem 32 (skewed distribution)
SYN248=RPT63_SK_33  (1) RPT63 synthetic problem 33 (skewed distribution)
SYN249=RPT63_SK_34  (1) RPT63 synthetic problem 34 (skewed distribution)
SYN250=RPT63_SK_35  (1) RPT63 synthetic problem 35 (skewed distribution)
SYN251=RPT63_SK_36  (1) RPT63 synthetic problem 36 (skewed distribution)
SYN252=RPT63_SK_37  (1) RPT63 synthetic problem 37 (skewed distribution)
SYN253=RPT63_SK_38  (1) RPT63 synthetic problem 38 (skewed distribution)
SYN254=RPT63_SK_39  (1) RPT63 synthetic problem 39 (skewed distribution)
SYN255=RPT63_SK_40  (1) RPT63 synthetic problem 40 (skewed distribution)
SYN256=RPT63_SK_41  (1) RPT63 synthetic problem 41 (skewed distribution)
SYN257=RPT63_SK_42  (1) RPT63 synthetic problem 42 (skewed distribution)
SYN258=RPT63_SK_43  (1) RPT63 synthetic problem 43 (skewed distribution)
SYN259=RPT63_SK_44  (1) RPT63 synthetic problem 44 (skewed distribution)
SYN260=RPT63_SK_45  (1) RPT63 synthetic problem 45 (skewed distribution)
SYN261=RPT63_SK_46  (1) RPT63 synthetic problem 46 (skewed distribution)
SYN262=RPT63_SK_47  (1) RPT63 synthetic problem 47 (skewed distribution)
SYN263=RPT63_SK_48  (1) RPT63 synthetic problem 48 (skewed distribution)
SYN264=RPT63_SK_49  (1) RPT63 synthetic problem 49 (skewed distribution)
SYN265=RPT63_SK_50  (1) RPT63 synthetic problem 50 (skewed distribution)
SYN266=RPT63_SK_51  (1) RPT63 synthetic problem 51 (skewed distribution)
SYN267=RPT63_SK_52  (1) RPT63 synthetic problem 52 (skewed distribution)
SYN268=RPT63_SK_53  (1) RPT63 synthetic problem 53 (skewed distribution)
SYN269=RPT63_SK_54  (1) RPT63 synthetic problem 54 (skewed distribution)
SYN270=RPT63_SK_55  (1) RPT63 synthetic problem 55 (skewed distribution)
SYN271=RPT63_SK_56  (1) RPT63 synthetic problem 56 (skewed distribution)
SYN272=RPT63_SK_57  (1) RPT63 synthetic problem 57 (skewed distribution)
SYN273=RPT63_SK_58  (1) RPT63 synthetic problem 58 (skewed distribution)
SYN274=RPT63_SK_59  (1) RPT63 synthetic problem 59 (skewed distribution)
SYN275=RPT63_SK_60  (1) RPT63 synthetic problem 60 (skewed distribution)
SYN276=RPT63_SK_61  (1) RPT63 synthetic problem 61 (skewed distribution)
SYN277=RPT63_SK_62  (1) RPT63 synthetic problem 62 (skewed distribution)
SYN278=RPT63_SK_63  (1) RPT63 synthetic problem 63 (skewed distribution)
SYN279=RPT63_SK_64  (1) RPT63 synthetic problem 64 (skewed distribution)
SYN280=RPT63_SK_65  (1) RPT63 synthetic problem 65 (skewed distribution)
SYN281=RPT63_SK_66  (1) RPT63 synthetic problem 66 (skewed distribution)
SYN282=RPT63_SK_67  (1) RPT63 synthetic problem 67 (skewed distribution)
SYN283=RPT63_SK_68  (1) RPT63 synthetic problem 68 (skewed distribution)
SYN284=RPT63_SK_69  (1) RPT63 synthetic problem 69 (skewed distribution)
SYN285=RPT63_SK_70  (1) RPT63 synthetic problem 70 (skewed distribution)
SYN286=RPT63_SK_71  (1) RPT63 synthetic problem 71 (skewed distribution)
SYN287=RPT63_SK_72  (1) RPT63 synthetic problem 72 (skewed distribution)
SYN288=RPT63_SK_73  (1) RPT63 synthetic problem 73 (skewed distribution)
SYN289=RPT63_SK_74  (1) RPT63 synthetic problem 74 (skewed distribution)
SYN290=RPT63_SK_75  (1) RPT63 synthetic problem 75 (skewed distribution)
SYN291=RPT63_SK_76  (1) RPT63 synthetic problem 76 (skewed distribution)
SYN292=RPT63_SK_77  (1) RPT63 synthetic problem 77 (skewed distribution)
SYN293=RPT63_SK_78  (1) RPT63 synthetic problem 78 (skewed distribution)
SYN294=RPT63_SK_79  (1) RPT63 synthetic problem 79 (skewed distribution)
SYN295=RPT63_SK_80  (1) RPT63 synthetic problem 80 (skewed distribution)
SYN296=RPT63_SK_81  (1) RPT63 synthetic problem 81 (skewed distribution)
SYN297=RPT63_SK_82  (1) RPT63 synthetic problem 82 (skewed distribution)
SYN298=RPT63_SK_83  (1) RPT63 synthetic problem 83 (skewed distribution)
SYN299=RPT63_SK_84  (1) RPT63 synthetic problem 84 (skewed distribution)
SYN300=RPT63_SK_85  (1) RPT63 synthetic problem 85 (skewed distribution)
SYN301=RPT63_SK_86  (1) RPT63 synthetic problem 86 (skewed distribution)
SYN302=DAPa         (1) Plaisted problem a(3)
SYN303=Decide1      (1) Problem for testing satisfiability
SYN304=Decide2      (1) Problem for testing satisfiability
SYN305=Decide3      (1) Problem for testing satisfiability
SYN306=Decide4      (1) Problem for testing satisfiability
SYN307=Decide5      (1) Problem for testing satisfiability
SYN308=Decide6      (1) Problem for testing satisfiability
SYN309=Decide7      (1) Problem for testing satisfiability
SYN310=Decide8      (1) Problem for testing satisfiability
SYN311=Decide9      (1) Problem for testing satisfiability
SYN312=Decide10     (1) Problem for testing satisfiability
SYN313=Decide11     (1) Problem for testing satisfiability
SYN314=Decide12     (1) Problem for testing satisfiability
SYN315=Church46_2_1 (1) Church problem 46.2 (1)
SYN316=Church46_2_2 (1) Church problem 46.2 (2)
SYN317=Church46_2_3 (1) Church problem 46.2 (3)
SYN318=Church46_2_4 (1) Church problem 46.2 (4)
SYN319=Church46_2_5 (1) Church problem 46.2 (5)
SYN320=Church46_3_1 (1) Church problem 46.3 (1)
SYN321=Church46_3_2 (1) Church problem 46.3 (2)
SYN322=Church46_4_1 (1) Church problem 46.4 (1)
SYN323=Church46_4_2 (1) Church problem 46.4 (2)
SYN324=Church46_9_1 (1) Church problem 46.9 (1)
SYN325=Church46_9_2 (1) Church problem 46.9 (2)
SYN326=Church46_12_1    (1) Church problem 46.12 (1)
SYN327=Church46_12_2    (1) Church problem 46.12 (2)
SYN328=Church46_12_3    (1) Church problem 46.12 (3)
SYN329=Church46_14_1    (1) Church problem 46.14 (1)
SYN330=Church46_14_2    (1) Church problem 46.14 (2)
SYN331=Church46_14_3    (1) Church problem 46.14 (3)
SYN332=Church46_14_4    (1) Church problem 46.14 (4)
SYN333=Church46_14_5    (1) Church problem 46.14 (5)
SYN334=Church46_14_6    (1) Church problem 46.14 (6)
SYN335=Church46_14_7    (1) Church problem 46.14 (7)
SYN336=Church46_15_1    (1) Church problem 46.15 (1)
SYN337=Church46_15_2    (1) Church problem 46.15 (2)
SYN338=Church46_15_3    (1) Church problem 46.15 (3)
SYN339=Church46_15_4    (1) Church problem 46.15 (4)
SYN340=Church46_15_5    (1) Church problem 46.15 (5)
SYN341=Church46_15_6    (1) Church problem 46.15 (6)
SYN342=Church46_15_7    (1) Church problem 46.15 (7)
SYN343=Church46_16_2    (1) Church problem 46.16 (2)
SYN344=Church46_16_3    (1) Church problem 46.16 (3)
SYN345=Church46_16_4    (1) Church problem 46.16 (4)
SYN346=Church46_17_2    (1) Church problem 46.17 (2)
SYN347=Church46_17_3    (1) Church problem 46.17 (3)
SYN348=Church46_17_4    (1) Church problem 46.17 (4)
SYN349=Church46_17_5    (1) Church problem 46.17 (5)
SYN350=Church46_18_2    (1) Church problem 46.18 (2)
SYN351=Church46_18_3    (1) Church problem 46.18 (3)
SYN352=Church46_18_4    (1) Church problem 46.18 (4)
SYN353=Church46_18_5    (1) Church problem 46.18 (5)
SYN354=Church46_20_1    (1) Church problem 46.20 (1)
-------------------------------------------------------------------------------
Domain TOP = Topology (19 abstract problems, 24 problems)
-------------------------------------------------------------------------------
TOP001=BasisTplgLem1    (2) Topology generated by a basis forms a topological space, part 1
TOP002=BasisTplgLem2    (2) Topology generated by a basis forms a topological space, part 2
TOP003=BasisTplgLem3    (2) Topology generated by a basis forms a topological space, part 3
TOP004=BasisTplgLem4    (2) Topology generated by a basis forms a topological space, part 4
TOP005=BasisTplgLem5    (2) Topology generated by a basis forms a topological space, part 5
TOP006=BasisTplg    (1) Topology generated by a basis forms a topological space
TOP007=TplgEqn1     (1) Property 1 of topological spaces
TOP008=SubSpTplg    (1) The subspace topology gives rise to a topological space
TOP009=OpenTrans    (1) If Y is open in X, and A is open in Y, then A is open in X
TOP010=FinerSubSp   (1) A finer topology induces a finer subspace topology
TOP011=TopBasisAltDef   (1) An alternative definition of top_of_basis
TOP012=UnionIntscClsd   (1) Intersections and finite unions of closed sets are closed
TOP013=IntrSubSClsr (1) Properties of interior and closure
TOP014=OpenIntrClsdClsr (1) Properties of open & interior and closed & closure
TOP015=IntrBndy     (1) The interior and the boundary of a set are disjoint
TOP016=UnionIntrBndy    (1) The union of the interior and the boundary is the closure
TOP017=BndyEmpty    (1) If the boundary of A is empty, A is both open and closed
TOP018=LmtPtConnSet (1) Propoerty of limits points and connected sets
TOP019=ClsrConn     (1) The closure of a connected set is connected
