------------------------------------------------------------------------------- Generators 87 generators (49 abstract, 86 CNF, 1 FOF, 0 TFF, 0 THF) ------------------------------------------------------------------------------- GRP123 ( -8 +0 _0 ^0) (3,2,1) conjugate orthogonality GRP123-1 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP123-2 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP123-3 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP123-4 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP123-6 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP123-7 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP123-8 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP123-9 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP124 ( -8 +0 _0 ^0) (3,1,2) conjugate orthogonality GRP124-1 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-2 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-3 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-4 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-6 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-7 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-8 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP124-9 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP125 ( -4 +0 _0 ^0) (a.b).(b.a) = a GRP125-1 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP125-2 Sizes: X,(X>=1) TPTP sizes: 5,4 GRP125-3 Sizes: X,(X>=1) TPTP sizes: 5,4 GRP125-4 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP126 ( -4 +0 _0 ^0) (a.b).(b.a) = b GRP126-1 Sizes: X,(X>=3) TPTP sizes: 4,5 GRP126-2 Sizes: X,(X>=3) TPTP sizes: 4,5 GRP126-3 Sizes: X,(X>=3) TPTP sizes: 4,5 GRP126-4 Sizes: X,(X>=3) TPTP sizes: 4,5 GRP127 ( -4 +0 _0 ^0) ((b.a).b).b) = a GRP127-1 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP127-2 Sizes: X,(X>=1) TPTP sizes: 6,5 GRP127-3 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP127-4 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP128 ( -4 +0 _0 ^0) (a.b).b = a.(a.b) GRP128-1 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP128-2 Sizes: X,(X>=1) TPTP sizes: 6,4 GRP128-3 Sizes: X,(X>=1) TPTP sizes: 5,4 GRP128-4 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP129 ( -4 +0 _0 ^0) a.(b.a) = (b.a).b GRP129-1 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP129-2 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP129-3 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP129-4 Sizes: X,(X>=1) TPTP sizes: 4,5 GRP130 ( -4 +0 _0 ^0) (a.(a.b)).b = a GRP130-1 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP130-2 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP130-3 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP130-4 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP131 ( -2 +0 _0 ^0) (3,2,1) conjugate orthogonality, no idempotence GRP131-1 Sizes: X,(X>=1) TPTP sizes: 2,5 GRP131-2 Sizes: X,(X>=1) TPTP sizes: 2,5 GRP132 ( -2 +0 _0 ^0) (3,1,2) conjugate orthogonality, no idempotence GRP132-1 Sizes: X,(X>=1) TPTP sizes: 2,5 GRP132-2 Sizes: X,(X>=1) TPTP sizes: 2,5 GRP133 ( -2 +0 _0 ^0) (a.b).(b.a) = a, no idempotence GRP133-1 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP133-2 Sizes: X,(X>=1) TPTP sizes: 3,4 GRP134 ( -2 +0 _0 ^0) (a.b).(b.a) = b, no idempotence GRP134-1 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP134-2 Sizes: X,(X>=1) TPTP sizes: 3,5 GRP135 ( -2 +0 _0 ^0) ((b.a).b).b) = a, no idempotence GRP135-1 Sizes: X,(X>=1) TPTP sizes: 2,5 GRP135-2 Sizes: X,(X>=1) TPTP sizes: 2,5 MSC007 ( -2 +0 _0 ^0) Cook pigeon-hole problem MSC007-1 Sizes: X,(X>=2) TPTP sizes: 8 MSC007-2 Sizes: X,(X>=2) TPTP sizes: 5 MSC008 ( -1 +0 _0 ^0) The (in)constructability of Graeco-Latin Squares MSC008-1 Sizes: X,(X>=2,X mod 4 =:= 2) TPTP sizes: 2,10 NUM283 ( -1 +0 _0 ^0) Calculation of factorial NUM283-1 Sizes: X,(X>=1) TPTP sizes: 5 NUM284 ( -1 +0 _0 ^0) Calculation of fibonacci numbers NUM284-1 Sizes: X,(X>=1) TPTP sizes: 14 PUZ015 ( -1 +0 _0 ^0) Checkerboard and Dominoes : Opposing corners removed PUZ015-2 Sizes: X,(X>=2) TPTP sizes: 6 PUZ016 ( -1 +0 _0 ^0) Checkerboard and Dominoes : Row 1, columns 2 and 3 removed PUZ016-2 Sizes: X,(X>=3) TPTP sizes: 5,4 PUZ034 ( -1 +0 _0 ^0) N queens problem PUZ034-1 Sizes: X,(X>=2) TPTP sizes: 4,3 PUZ036 ( -1 +0 _0 ^0) TopSpin PUZ036-1 Sizes: X,(X>=1,20>=X) TPTP sizes: 5 SYN001 ( -1 +0 _0 ^0) All signed combinations of some propositions. SYN001-1 Sizes: X,(X>=1) TPTP sizes: 5 SYN002 ( -1 +0 _0 ^0) Odd and Even Problem SYN002-1 Sizes: X:Y,(X>=1,Y>X,(X+Y) mod 2 =:= 1) TPTP sizes: 7:8 SYN003 ( -1 +0 _0 ^0) Implications that form a contradiction SYN003-1 Sizes: X,(X>=2) TPTP sizes: 6 SYN004 ( -1 +0 _0 ^0) Implications that form a contradiction SYN004-1 Sizes: X,(X>=2) TPTP sizes: 7 SYN005 ( -1 +0 _0 ^0) Disjunctions that form a contradiction SYN005-1 Sizes: X,(X>=1) TPTP sizes: 10 SYN007 ( -0 +1 _0 ^0) Pelletier Problem 71 SYN007+1 Sizes: X,(X>=1) TPTP sizes: 14 SYN010 ( -1 +0 _0 ^0) Example for Proposition 5.2 in [LMG94] SYN010-1 Sizes: X:Y,(X>=1,Y>=1) TPTP sizes: 5:5 SYN085 ( -1 +0 _0 ^0) Plaisted problem s(1,SIZE) SYN085-1 Sizes: X,(X>=0) TPTP sizes: 10 SYN086 ( -1 +0 _0 ^0) Plaisted problem s(2,SIZE) SYN086-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN087 ( -1 +0 _0 ^0) Plaisted problem s(3,SIZE) SYN087-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN088 ( -1 +0 _0 ^0) Plaisted problem s(4,SIZE) SYN088-1 Sizes: X,(X>=1) TPTP sizes: 10 SYN089 ( -1 +0 _0 ^0) Plaisted problem t(2,SIZE) SYN089-1 Sizes: X,(X>=1) TPTP sizes: 2 SYN090 ( -1 +0 _0 ^0) Plaisted problem t(3,SIZE) SYN090-1 Sizes: X,(X>=1) TPTP sizes: 8 SYN091 ( -1 +0 _0 ^0) Plaisted problem sym(s(2,SIZE)) SYN091-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN092 ( -1 +0 _0 ^0) Plaisted problem sym(s(3,SIZE)) SYN092-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN093 ( -1 +0 _0 ^0) Plaisted problem u(t(2,SIZE)) SYN093-1 Sizes: X,(X>=1) TPTP sizes: 2 SYN094 ( -1 +0 _0 ^0) Plaisted problem u(t(3,SIZE)) SYN094-1 Sizes: X,(X>=1) TPTP sizes: 5 SYN095 ( -1 +0 _0 ^0) Plaisted problem m(t(2,SIZE)) SYN095-1 Sizes: X,(X>=1) TPTP sizes: 2 SYN096 ( -1 +0 _0 ^0) Plaisted problem m(t(3,SIZE)) SYN096-1 Sizes: X,(X>=1) TPTP sizes: 8 SYN097 ( -1 +0 _0 ^0) Plaisted problem sym(u(t(2,SIZE))) SYN097-1 Sizes: X,(X>=1) TPTP sizes: 2 SYN098 ( -1 +0 _0 ^0) Plaisted problem sym(u(t(3,SIZE))) SYN098-1 Sizes: X,(X>=1) TPTP sizes: 2 SYN099 ( -1 +0 _0 ^0) Plaisted problem sym(m(t(2,SIZE))) SYN099-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN100 ( -1 +0 _0 ^0) Plaisted problem sym(m(t(3,SIZE))) SYN100-1 Sizes: X,(X>=1) TPTP sizes: 5 SYN101 ( -1 +0 _0 ^0) Plaisted problem n(t(2,SIZE1),SIZE2) SYN101-1 Sizes: X:Y,(X>=1,Y>=1) TPTP sizes: 2:2 SYN102 ( -1 +0 _0 ^0) Plaisted problem n(t(3,SIZE1),SIZE2) SYN102-1 Sizes: X:Y,(X>=1,Y>=1) TPTP sizes: 7:7 SYN302 ( -1 +0 _0 ^0) Plaisted problem a(SIZE) SYN302-1 Sizes: X,(X>=1) TPTP sizes: 3 SYN313 ( -1 +0 _0 ^0) Problem for testing satisfiability SYN313-1 Sizes: X:Y,(X>=1,Y>=1) TPTP sizes: 1:2 SYN314 ( -1 +0 _0 ^0) Problem for testing satisfiability SYN314-1 Sizes: X:Y,(X>=0,Y>=0) TPTP sizes: 2:1