-------------------------------------------------------------------------------
Generators (85 generators)
-------------------------------------------------------------------------------
GRP123=321COILS         (8) (3,2,1) conjugate orthogonality
GRP123=321COILS-1           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-2           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-3           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-4           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-6           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-7           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-8           Sizes: X,(X>=1)    TPTP size: 3
GRP123=321COILS-9           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS         (8) (3,1,2) conjugate orthogonality
GRP124=312COILS-1           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-2           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-3           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-4           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-6           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-7           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-8           Sizes: X,(X>=1)    TPTP size: 3
GRP124=312COILS-9           Sizes: X,(X>=1)    TPTP size: 4
GRP125=Schroeder        (4) (a.b).(b.a) = a
GRP125=Schroeder-1          Sizes: X,(X>=1)    TPTP size: 3
GRP125=Schroeder-2          Sizes: X,(X>=1)    TPTP size: 3
GRP125=Schroeder-3          Sizes: X,(X>=1)    TPTP size: 3
GRP125=Schroeder-4          Sizes: X,(X>=1)    TPTP size: 3
GRP126=SteinLaw3        (4) (a.b).(b.a) = b
GRP126=SteinLaw3-1          Sizes: X,(X>=3)    TPTP size: 3
GRP126=SteinLaw3-2          Sizes: X,(X>=3)    TPTP size: 3
GRP126=SteinLaw3-3          Sizes: X,(X>=3)    TPTP size: 3
GRP126=SteinLaw3-4          Sizes: X,(X>=3)    TPTP size: 3
GRP127=QG5              (4) ((b.a).b).b) = a
GRP127=QG5-1                Sizes: X,(X>=1)    TPTP size: 3
GRP127=QG5-2                Sizes: X,(X>=1)    TPTP size: 3
GRP127=QG5-3                Sizes: X,(X>=1)    TPTP size: 3
GRP127=QG5-4                Sizes: X,(X>=1)    TPTP size: 3
GRP128=SchroederLaw1    (4) (a.b).b = a.(a.b)
GRP128=SchroederLaw1-1      Sizes: X,(X>=1)    TPTP size: 3
GRP128=SchroederLaw1-2      Sizes: X,(X>=1)    TPTP size: 3
GRP128=SchroederLaw1-3      Sizes: X,(X>=1)    TPTP size: 3
GRP128=SchroederLaw1-4      Sizes: X,(X>=1)    TPTP size: 3
GRP129=QG7              (4) a.(b.a) = (b.a).b
GRP129=QG7-1                Sizes: X,(X>=1)    TPTP size: 2
GRP129=QG7-2                Sizes: X,(X>=1)    TPTP size: 2
GRP129=QG7-3                Sizes: X,(X>=1)    TPTP size: 2
GRP129=QG7-4                Sizes: X,(X>=1)    TPTP size: 2
GRP130=QG8              (4) (a.(a.b)).b = a
GRP130=QG8-1                Sizes: X,(X>=1)    TPTP size: 2
GRP130=QG8-2                Sizes: X,(X>=1)    TPTP size: 2
GRP130=QG8-3                Sizes: X,(X>=1)    TPTP size: 2
GRP130=QG8-4                Sizes: X,(X>=1)    TPTP size: 2
GRP131=321COILSNoIdem   (2) (3,2,1) conjugate orthogonality, no idempotence
GRP131=321COILSNoIdem-1     Sizes: X,(X>=1)    TPTP size: 2
GRP131=321COILSNoIdem-2     Sizes: X,(X>=1)    TPTP size: 2
GRP132=312COILSNoIdem   (2) (3,1,2) conjugate orthogonality, no idempotence
GRP132=312COILSNoIdem-1     Sizes: X,(X>=1)    TPTP size: 2
GRP132=312COILSNoIdem-2     Sizes: X,(X>=1)    TPTP size: 2
GRP133=SchroederNoIdem  (2) (a.b).(b.a) = a, no idempotence
GRP133=SchroederNoIdem-1    Sizes: X,(X>=1)    TPTP size: 2
GRP133=SchroederNoIdem-2    Sizes: X,(X>=1)    TPTP size: 2
GRP134=SteinLaw3NoIdem  (2) (a.b).(b.a) = b, no idempotence
GRP134=SteinLaw3NoIdem-1    Sizes: X,(X>=1)    TPTP size: 2
GRP134=SteinLaw3NoIdem-2    Sizes: X,(X>=1)    TPTP size: 2
GRP135=QG5NoIdem        (2) ((b.a).b).b) = a, no idempotence
GRP135=QG5NoIdem-1          Sizes: X,(X>=1)    TPTP size: 2
GRP135=QG5NoIdem-2          Sizes: X,(X>=1)    TPTP size: 2
MSC007=Pigeon           (2) Cook pigeon-hole problem
MSC007=Pigeon-1             Sizes: X,(X>=2)    TPTP size: 5
MSC007=Pigeon-2             Sizes: X,(X>=2)    TPTP size: 2
MSC008=LatSq            (1) The (in)constructability of Graeco-Latin Squares
MSC008=LatSq-1              Sizes: X,(X>=2,X mod 4 =:= 2)      TPTP size: 2
NUM283=Factorial        (1) Calculation of factorial
NUM283=Factorial-1          Sizes: X,(X>=1)    TPTP size: 5
NUM284=Fibonacci        (1) Calculation of fibonacci numbers
NUM284=Fibonacci-1          Sizes: X,(X>=1)    TPTP size: 10
PUZ015=Checkers1        (1) Checkerboard and Dominoes : Opposing corners removed
PUZ015=Checkers1-2          Sizes: X,(X>=2)    TPTP size: 3
PUZ016=Checkers2        (1) Checkerboard and Dominoes : Row 1, columns 2 and 3 removed
PUZ016=Checkers2-2          Sizes: X,(X>=3)    TPTP size: 3
PUZ034=NQueens          (1) N queens problem
PUZ034=NQueens-1            Sizes: X,(X>=2)    TPTP size: 3
SYN001=Allways          (1) All signed combinations of some propositions.
SYN001=Allways-1            Sizes: X,(X>=1)    TPTP size: 5
SYN002=OddEven          (1) Odd and Even Problem
SYN002=OddEven-1            Sizes: X:Y,(X>=1,Y>X,(X+Y) mod 2 =:= 1)    TPTP size: 7:8
SYN003=Implies1         (1) Implications that form a contradiction
SYN003=Implies1-1           Sizes: X,(X>=2)    TPTP size: 6
SYN004=Implies2         (1) Implications that form a contradiction
SYN004=Implies2-1           Sizes: X,(X>=2)    TPTP size: 7
SYN005=Or1              (1) Disjunctions that form a contradiction
SYN005=Or1-1                Sizes: X,(X>=1)    TPTP size: 10
SYN010=Letz             (1) Example for Proposition 5.2 in [Letz, et al., 1994]
SYN010=Letz-1               Sizes: X:Y,(X>=1,Y>=1)     TPTP size: 5:5
SYN085=DAPs1            (1) Plaisted problem s(1,SIZE)
SYN085=DAPs1-1              Sizes: X,(X>=0)    TPTP size: 10
SYN086=DAPs2            (1) Plaisted problem s(2,SIZE)
SYN086=DAPs2-1              Sizes: X,(X>=1)    TPTP size: 3
SYN087=DAPs3            (1) Plaisted problem s(3,SIZE)
SYN087=DAPs3-1              Sizes: X,(X>=1)    TPTP size: 3
SYN088=DAPs4            (1) Plaisted problem s(4,SIZE)
SYN088=DAPs4-1              Sizes: X,(X>=1)    TPTP size: 10
SYN089=DAPt2            (1) Plaisted problem t(2,SIZE)
SYN089=DAPt2-1              Sizes: X,(X>=1)    TPTP size: 2
SYN090=DAPt3            (1) Plaisted problem t(3,SIZE)
SYN090=DAPt3-1              Sizes: X,(X>=1)    TPTP size: 8
SYN091=DAPsyms2         (1) Plaisted problem sym(s(2,SIZE))
SYN091=DAPsyms2-1           Sizes: X,(X>=1)    TPTP size: 3
SYN092=DAPsyms3         (1) Plaisted problem sym(s(3,SIZE))
SYN092=DAPsyms3-1           Sizes: X,(X>=1)    TPTP size: 3
SYN093=DAPut2           (1) Plaisted problem u(t(2,SIZE))
SYN093=DAPut2-1             Sizes: X,(X>=1)    TPTP size: 2
SYN094=DAPut3           (1) Plaisted problem u(t(3,SIZE))
SYN094=DAPut3-1             Sizes: X,(X>=1)    TPTP size: 5
SYN095=DAPmt2           (1) Plaisted problem m(t(2,SIZE))
SYN095=DAPmt2-1             Sizes: X,(X>=1)    TPTP size: 2
SYN096=DAPmt3           (1) Plaisted problem m(t(3,SIZE))
SYN096=DAPmt3-1             Sizes: X,(X>=1)    TPTP size: 8
SYN097=DAPsymut2        (1) Plaisted problem sym(u(t(2,SIZE)))
SYN097=DAPsymut2-1          Sizes: X,(X>=1)    TPTP size: 2
SYN098=DAPsymut3        (1) Plaisted problem sym(u(t(3,SIZE)))
SYN098=DAPsymut3-1          Sizes: X,(X>=1)    TPTP size: 2
SYN099=DAPsymmt2        (1) Plaisted problem sym(m(t(2,SIZE)))
SYN099=DAPsymmt2-1          Sizes: X,(X>=1)    TPTP size: 3
SYN100=DAPsymmt3        (1) Plaisted problem sym(m(t(3,SIZE)))
SYN100=DAPsymmt3-1          Sizes: X,(X>=1)    TPTP size: 5
SYN101=DAPnt2           (1) Plaisted problem n(t(2,SIZE1),SIZE2)
SYN101=DAPnt2-1             Sizes: X:Y,(X>=1,Y>=1)     TPTP size: 2:2
SYN102=DAPnt3           (1) Plaisted problem n(t(3,SIZE1),SIZE2)
SYN102=DAPnt3-1             Sizes: X:Y,(X>=1,Y>=1)     TPTP size: 7:7
SYN302=DAPa             (1) Plaisted problem a(SIZE)
SYN302=DAPa-1               Sizes: X,(X>=1)    TPTP size: 3
SYN313=Decide11         (1) Problem for testing satisfiability
SYN313=Decide11-1           Sizes: X:Y,(X>=1,Y>=1)     TPTP size: 1:2
SYN314=Decide12         (1) Problem for testing satisfiability
SYN314=Decide12-1           Sizes: X:Y,(X>=0,Y>=0)     TPTP size: 2:1
