Quelle  nri24_7.nr   Sprache: unbekannt

NI24_7 := rec(
  group_name := "24/7",
  group_generators := [ (1,2,3,4), (2,4), (5,6,7) ],
  elements := rec(
      1 := (),
      2 := (5,6,7),
      3 := (5,7,6),
      4 := (2,4),
      5 := (2,4)(5,6,7),
      6 := (2,4)(5,7,6),
      7 := (1,2)(3,4),
      8 := (1,2)(3,4)(5,6,7),
      9 := (1,2)(3,4)(5,7,6),
      10 := (1,2,3,4),
      11 := (1,2,3,4)(5,6,7),
      12 := (1,2,3,4)(5,7,6),
      13 := (1,3),
      14 := (1,3)(5,6,7),
      15 := (1,3)(5,7,6),
      16 := (1,3)(2,4),
      17 := (1,3)(2,4)(5,6,7),
      18 := (1,3)(2,4)(5,7,6),
      19 := (1,4,3,2),
      20 := (1,4,3,2)(5,6,7),
      21 := (1,4,3,2)(5,7,6),
      22 := (1,4)(2,3),
      23 := (1,4)(2,3)(5,6,7),
      24 := (1,4)(2,3)(5,7,6) ),
  group_endomorphisms := rec(
      1 := [ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 ],
      2 := [ 1, 1, 1, 1, 1, 1, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 4, 4, 4, 4, 4, 4 ],
      3 := [ 1, 1, 1, 1, 1, 1, 7, 7, 7, 7, 7, 7, 1, 1, 1, 1, 1, 1, 7, 7, 7, 7, 7, 7 ],
      4 := [ 1, 1, 1, 1, 1, 1, 13, 13, 13, 13, 13, 13, 1, 1, 1, 1, 1, 1, 13, 13, 13, 
          13, 13, 13 ],
      5 := [ 1, 1, 1, 1, 1, 1, 16, 16, 16, 16, 16, 16, 1, 1, 1, 1, 1, 1, 16, 16, 16, 
          16, 16, 16 ],
      6 := [ 1, 1, 1, 1, 1, 1, 22, 22, 22, 22, 22, 22, 1, 1, 1, 1, 1, 1, 22, 22, 22, 
          22, 22, 22 ],
      7 := [ 1, 1, 1, 4, 4, 4, 1, 1, 1, 4, 4, 4, 4, 4, 4, 1, 1, 1, 4, 4, 4, 1, 1, 1 ],
      8 := [ 1, 1, 1, 4, 4, 4, 4, 4, 4, 1, 1, 1, 4, 4, 4, 1, 1, 1, 1, 1, 1, 4, 4, 4 ],
      9 := [ 1, 1, 1, 4, 4, 4, 7, 7, 7, 10, 10, 10, 13, 13, 13, 16, 16, 16, 19, 19, 
          19, 22, 22, 22 ],
      10 := [ 1, 1, 1, 4, 4, 4, 13, 13, 13, 16, 16, 16, 4, 4, 4, 1, 1, 1, 16, 16, 16, 
          13, 13, 13 ],
      11 := [ 1, 1, 1, 4, 4, 4, 16, 16, 16, 13, 13, 13, 4, 4, 4, 1, 1, 1, 13, 13, 13, 
          16, 16, 16 ],
      12 := [ 1, 1, 1, 4, 4, 4, 22, 22, 22, 19, 19, 19, 13, 13, 13, 16, 16, 16, 10, 
          10, 10, 7, 7, 7 ],
      13 := [ 1, 1, 1, 7, 7, 7, 1, 1, 1, 7, 7, 7, 7, 7, 7, 1, 1, 1, 7, 7, 7, 1, 1, 1 ],
      14 := [ 1, 1, 1, 7, 7, 7, 4, 4, 4, 19, 19, 19, 22, 22, 22, 16, 16, 16, 10, 10, 
          10, 13, 13, 13 ],
      15 := [ 1, 1, 1, 7, 7, 7, 7, 7, 7, 1, 1, 1, 7, 7, 7, 1, 1, 1, 1, 1, 1, 7, 7, 7 ],
      16 := [ 1, 1, 1, 7, 7, 7, 13, 13, 13, 10, 10, 10, 22, 22, 22, 16, 16, 16, 19, 
          19, 19, 4, 4, 4 ],
      17 := [ 1, 1, 1, 7, 7, 7, 16, 16, 16, 22, 22, 22, 7, 7, 7, 1, 1, 1, 22, 22, 22, 
          16, 16, 16 ],
      18 := [ 1, 1, 1, 7, 7, 7, 22, 22, 22, 16, 16, 16, 7, 7, 7, 1, 1, 1, 16, 16, 16, 
          22, 22, 22 ],
      19 := [ 1, 1, 1, 13, 13, 13, 1, 1, 1, 13, 13, 13, 13, 13, 13, 1, 1, 1, 13, 13, 
          13, 1, 1, 1 ],
      20 := [ 1, 1, 1, 13, 13, 13, 4, 4, 4, 16, 16, 16, 13, 13, 13, 1, 1, 1, 16, 16, 
          16, 4, 4, 4 ],
      21 := [ 1, 1, 1, 13, 13, 13, 7, 7, 7, 19, 19, 19, 4, 4, 4, 16, 16, 16, 10, 10, 
          10, 22, 22, 22 ],
      22 := [ 1, 1, 1, 13, 13, 13, 13, 13, 13, 1, 1, 1, 13, 13, 13, 1, 1, 1, 1, 1, 1, 
          13, 13, 13 ],
      23 := [ 1, 1, 1, 13, 13, 13, 16, 16, 16, 4, 4, 4, 13, 13, 13, 1, 1, 1, 4, 4, 4, 
          16, 16, 16 ],
      24 := [ 1, 1, 1, 13, 13, 13, 22, 22, 22, 10, 10, 10, 4, 4, 4, 16, 16, 16, 19, 
          19, 19, 7, 7, 7 ],
      25 := [ 1, 1, 1, 16, 16, 16, 1, 1, 1, 16, 16, 16, 16, 16, 16, 1, 1, 1, 16, 16, 
          16, 1, 1, 1 ],
      26 := [ 1, 1, 1, 16, 16, 16, 4, 4, 4, 13, 13, 13, 16, 16, 16, 1, 1, 1, 13, 13, 
          13, 4, 4, 4 ],
      27 := [ 1, 1, 1, 16, 16, 16, 7, 7, 7, 22, 22, 22, 16, 16, 16, 1, 1, 1, 22, 22, 
          22, 7, 7, 7 ],
      28 := [ 1, 1, 1, 16, 16, 16, 13, 13, 13, 4, 4, 4, 16, 16, 16, 1, 1, 1, 4, 4, 4, 
          13, 13, 13 ],
      29 := [ 1, 1, 1, 16, 16, 16, 16, 16, 16, 1, 1, 1, 16, 16, 16, 1, 1, 1, 1, 1, 1, 
          16, 16, 16 ],
      30 := [ 1, 1, 1, 16, 16, 16, 22, 22, 22, 7, 7, 7, 16, 16, 16, 1, 1, 1, 7, 7, 7, 
          22, 22, 22 ],
      31 := [ 1, 1, 1, 22, 22, 22, 1, 1, 1, 22, 22, 22, 22, 22, 22, 1, 1, 1, 22, 22, 
          22, 1, 1, 1 ],
      32 := [ 1, 1, 1, 22, 22, 22, 4, 4, 4, 10, 10, 10, 7, 7, 7, 16, 16, 16, 19, 19, 
          19, 13, 13, 13 ],
      33 := [ 1, 1, 1, 22, 22, 22, 7, 7, 7, 16, 16, 16, 22, 22, 22, 1, 1, 1, 16, 16, 
          16, 7, 7, 7 ],
      34 := [ 1, 1, 1, 22, 22, 22, 13, 13, 13, 19, 19, 19, 7, 7, 7, 16, 16, 16, 10, 
          10, 10, 4, 4, 4 ],
      35 := [ 1, 1, 1, 22, 22, 22, 16, 16, 16, 7, 7, 7, 22, 22, 22, 1, 1, 1, 7, 7, 7, 
          16, 16, 16 ],
      36 := [ 1, 1, 1, 22, 22, 22, 22, 22, 22, 1, 1, 1, 22, 22, 22, 1, 1, 1, 1, 1, 1, 
          22, 22, 22 ],
      37 := [ 1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3, 1, 2, 3 ],
      38 := [ 1, 2, 3, 1, 2, 3, 4, 5, 6, 4, 5, 6, 1, 2, 3, 1, 2, 3, 4, 5, 6, 4, 5, 6 ],
      39 := [ 1, 2, 3, 1, 2, 3, 7, 8, 9, 7, 8, 9, 1, 2, 3, 1, 2, 3, 7, 8, 9, 7, 8, 9 ],
      40 := [ 1, 2, 3, 1, 2, 3, 13, 14, 15, 13, 14, 15, 1, 2, 3, 1, 2, 3, 13, 14, 15, 
          13, 14, 15 ],
      41 := [ 1, 2, 3, 1, 2, 3, 16, 17, 18, 16, 17, 18, 1, 2, 3, 1, 2, 3, 16, 17, 18, 
          16, 17, 18 ],
      42 := [ 1, 2, 3, 1, 2, 3, 22, 23, 24, 22, 23, 24, 1, 2, 3, 1, 2, 3, 22, 23, 24, 
          22, 23, 24 ],
      43 := [ 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3 ],
      44 := [ 1, 2, 3, 4, 5, 6, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 1, 2, 3, 4, 5, 6 ],
      45 := [ 1, 2, 3, 4, 5, 6, 13, 14, 15, 16, 17, 18, 4, 5, 6, 1, 2, 3, 16, 17, 18, 
          13, 14, 15 ],
      46 := [ 1, 2, 3, 4, 5, 6, 16, 17, 18, 13, 14, 15, 4, 5, 6, 1, 2, 3, 13, 14, 15, 
          16, 17, 18 ],
      47 := [ 1, 2, 3, 4, 5, 6, 22, 23, 24, 19, 20, 21, 13, 14, 15, 16, 17, 18, 10, 
          11, 12, 7, 8, 9 ],
      48 := [ 1, 2, 3, 7, 8, 9, 1, 2, 3, 7, 8, 9, 7, 8, 9, 1, 2, 3, 7, 8, 9, 1, 2, 3 ],
      49 := [ 1, 2, 3, 7, 8, 9, 4, 5, 6, 19, 20, 21, 22, 23, 24, 16, 17, 18, 10, 11, 
          12, 13, 14, 15 ],
      50 := [ 1, 2, 3, 7, 8, 9, 7, 8, 9, 1, 2, 3, 7, 8, 9, 1, 2, 3, 1, 2, 3, 7, 8, 9 ],
      51 := [ 1, 2, 3, 7, 8, 9, 13, 14, 15, 10, 11, 12, 22, 23, 24, 16, 17, 18, 19, 
          20, 21, 4, 5, 6 ],
      52 := [ 1, 2, 3, 7, 8, 9, 16, 17, 18, 22, 23, 24, 7, 8, 9, 1, 2, 3, 22, 23, 24, 
          16, 17, 18 ],
      53 := [ 1, 2, 3, 7, 8, 9, 22, 23, 24, 16, 17, 18, 7, 8, 9, 1, 2, 3, 16, 17, 18, 
          22, 23, 24 ],
      54 := [ 1, 2, 3, 13, 14, 15, 1, 2, 3, 13, 14, 15, 13, 14, 15, 1, 2, 3, 13, 14, 
          15, 1, 2, 3 ],
      55 := [ 1, 2, 3, 13, 14, 15, 4, 5, 6, 16, 17, 18, 13, 14, 15, 1, 2, 3, 16, 17, 
          18, 4, 5, 6 ],
      56 := [ 1, 2, 3, 13, 14, 15, 7, 8, 9, 19, 20, 21, 4, 5, 6, 16, 17, 18, 10, 11, 
          12, 22, 23, 24 ],
      57 := [ 1, 2, 3, 13, 14, 15, 13, 14, 15, 1, 2, 3, 13, 14, 15, 1, 2, 3, 1, 2, 3, 
          13, 14, 15 ],
      58 := [ 1, 2, 3, 13, 14, 15, 16, 17, 18, 4, 5, 6, 13, 14, 15, 1, 2, 3, 4, 5, 6, 
          16, 17, 18 ],
      59 := [ 1, 2, 3, 13, 14, 15, 22, 23, 24, 10, 11, 12, 4, 5, 6, 16, 17, 18, 19, 
          20, 21, 7, 8, 9 ],
      60 := [ 1, 2, 3, 16, 17, 18, 1, 2, 3, 16, 17, 18, 16, 17, 18, 1, 2, 3, 16, 17, 
          18, 1, 2, 3 ],
      61 := [ 1, 2, 3, 16, 17, 18, 4, 5, 6, 13, 14, 15, 16, 17, 18, 1, 2, 3, 13, 14, 
          15, 4, 5, 6 ],
      62 := [ 1, 2, 3, 16, 17, 18, 7, 8, 9, 22, 23, 24, 16, 17, 18, 1, 2, 3, 22, 23, 
          24, 7, 8, 9 ],
      63 := [ 1, 2, 3, 16, 17, 18, 13, 14, 15, 4, 5, 6, 16, 17, 18, 1, 2, 3, 4, 5, 6, 
          13, 14, 15 ],
      64 := [ 1, 2, 3, 16, 17, 18, 16, 17, 18, 1, 2, 3, 16, 17, 18, 1, 2, 3, 1, 2, 3, 
          16, 17, 18 ],
      65 := [ 1, 2, 3, 16, 17, 18, 22, 23, 24, 7, 8, 9, 16, 17, 18, 1, 2, 3, 7, 8, 9, 
          22, 23, 24 ],
      66 := [ 1, 2, 3, 22, 23, 24, 1, 2, 3, 22, 23, 24, 22, 23, 24, 1, 2, 3, 22, 23, 
          24, 1, 2, 3 ],
      67 := [ 1, 2, 3, 22, 23, 24, 4, 5, 6, 10, 11, 12, 7, 8, 9, 16, 17, 18, 19, 20, 
          21, 13, 14, 15 ],
      68 := [ 1, 2, 3, 22, 23, 24, 7, 8, 9, 16, 17, 18, 22, 23, 24, 1, 2, 3, 16, 17, 
          18, 7, 8, 9 ],
      69 := [ 1, 2, 3, 22, 23, 24, 13, 14, 15, 19, 20, 21, 7, 8, 9, 16, 17, 18, 10, 
          11, 12, 4, 5, 6 ],
      70 := [ 1, 2, 3, 22, 23, 24, 16, 17, 18, 7, 8, 9, 22, 23, 24, 1, 2, 3, 7, 8, 9, 
          16, 17, 18 ],
      71 := [ 1, 2, 3, 22, 23, 24, 22, 23, 24, 1, 2, 3, 22, 23, 24, 1, 2, 3, 1, 2, 3, 
          22, 23, 24 ],
      72 := [ 1, 3, 2, 1, 3, 2, 1, 3, 2, 1, 3, 2, 1, 3, 2, 1, 3, 2, 1, 3, 2, 1, 3, 2 ],
      73 := [ 1, 3, 2, 1, 3, 2, 4, 6, 5, 4, 6, 5, 1, 3, 2, 1, 3, 2, 4, 6, 5, 4, 6, 5 ],
      74 := [ 1, 3, 2, 1, 3, 2, 7, 9, 8, 7, 9, 8, 1, 3, 2, 1, 3, 2, 7, 9, 8, 7, 9, 8 ],
      75 := [ 1, 3, 2, 1, 3, 2, 13, 15, 14, 13, 15, 14, 1, 3, 2, 1, 3, 2, 13, 15, 14, 
          13, 15, 14 ],
      76 := [ 1, 3, 2, 1, 3, 2, 16, 18, 17, 16, 18, 17, 1, 3, 2, 1, 3, 2, 16, 18, 17, 
          16, 18, 17 ],
      77 := [ 1, 3, 2, 1, 3, 2, 22, 24, 23, 22, 24, 23, 1, 3, 2, 1, 3, 2, 22, 24, 23, 
          22, 24, 23 ],
      78 := [ 1, 3, 2, 4, 6, 5, 1, 3, 2, 4, 6, 5, 4, 6, 5, 1, 3, 2, 4, 6, 5, 1, 3, 2 ],
      79 := [ 1, 3, 2, 4, 6, 5, 4, 6, 5, 1, 3, 2, 4, 6, 5, 1, 3, 2, 1, 3, 2, 4, 6, 5 ],
      80 := [ 1, 3, 2, 4, 6, 5, 7, 9, 8, 10, 12, 11, 13, 15, 14, 16, 18, 17, 19, 21, 
          20, 22, 24, 23 ],
      81 := [ 1, 3, 2, 4, 6, 5, 13, 15, 14, 16, 18, 17, 4, 6, 5, 1, 3, 2, 16, 18, 17, 
          13, 15, 14 ],
      82 := [ 1, 3, 2, 4, 6, 5, 16, 18, 17, 13, 15, 14, 4, 6, 5, 1, 3, 2, 13, 15, 14, 
          16, 18, 17 ],
      83 := [ 1, 3, 2, 4, 6, 5, 22, 24, 23, 19, 21, 20, 13, 15, 14, 16, 18, 17, 10, 
          12, 11, 7, 9, 8 ],
      84 := [ 1, 3, 2, 7, 9, 8, 1, 3, 2, 7, 9, 8, 7, 9, 8, 1, 3, 2, 7, 9, 8, 1, 3, 2 ],
      85 := [ 1, 3, 2, 7, 9, 8, 4, 6, 5, 19, 21, 20, 22, 24, 23, 16, 18, 17, 10, 12, 
          11, 13, 15, 14 ],
      86 := [ 1, 3, 2, 7, 9, 8, 7, 9, 8, 1, 3, 2, 7, 9, 8, 1, 3, 2, 1, 3, 2, 7, 9, 8 ],
      87 := [ 1, 3, 2, 7, 9, 8, 13, 15, 14, 10, 12, 11, 22, 24, 23, 16, 18, 17, 19, 
          21, 20, 4, 6, 5 ],
      88 := [ 1, 3, 2, 7, 9, 8, 16, 18, 17, 22, 24, 23, 7, 9, 8, 1, 3, 2, 22, 24, 23, 
          16, 18, 17 ],
      89 := [ 1, 3, 2, 7, 9, 8, 22, 24, 23, 16, 18, 17, 7, 9, 8, 1, 3, 2, 16, 18, 17, 
          22, 24, 23 ],
      90 := [ 1, 3, 2, 13, 15, 14, 1, 3, 2, 13, 15, 14, 13, 15, 14, 1, 3, 2, 13, 15, 
          14, 1, 3, 2 ],
      91 := [ 1, 3, 2, 13, 15, 14, 4, 6, 5, 16, 18, 17, 13, 15, 14, 1, 3, 2, 16, 18, 
          17, 4, 6, 5 ],
      92 := [ 1, 3, 2, 13, 15, 14, 7, 9, 8, 19, 21, 20, 4, 6, 5, 16, 18, 17, 10, 12, 
          11, 22, 24, 23 ],
      93 := [ 1, 3, 2, 13, 15, 14, 13, 15, 14, 1, 3, 2, 13, 15, 14, 1, 3, 2, 1, 3, 2, 
          13, 15, 14 ],
      94 := [ 1, 3, 2, 13, 15, 14, 16, 18, 17, 4, 6, 5, 13, 15, 14, 1, 3, 2, 4, 6, 5, 
          16, 18, 17 ],
      95 := [ 1, 3, 2, 13, 15, 14, 22, 24, 23, 10, 12, 11, 4, 6, 5, 16, 18, 17, 19, 
          21, 20, 7, 9, 8 ],
      96 := [ 1, 3, 2, 16, 18, 17, 1, 3, 2, 16, 18, 17, 16, 18, 17, 1, 3, 2, 16, 18, 
          17, 1, 3, 2 ],
      97 := [ 1, 3, 2, 16, 18, 17, 4, 6, 5, 13, 15, 14, 16, 18, 17, 1, 3, 2, 13, 15, 
          14, 4, 6, 5 ],
      98 := [ 1, 3, 2, 16, 18, 17, 7, 9, 8, 22, 24, 23, 16, 18, 17, 1, 3, 2, 22, 24, 
          23, 7, 9, 8 ],
      99 := [ 1, 3, 2, 16, 18, 17, 13, 15, 14, 4, 6, 5, 16, 18, 17, 1, 3, 2, 4, 6, 5, 
          13, 15, 14 ],
      100 := [ 1, 3, 2, 16, 18, 17, 16, 18, 17, 1, 3, 2, 16, 18, 17, 1, 3, 2, 1, 3, 2, 
          16, 18, 17 ],
      101 := [ 1, 3, 2, 16, 18, 17, 22, 24, 23, 7, 9, 8, 16, 18, 17, 1, 3, 2, 7, 9, 8, 
          22, 24, 23 ],
      102 := [ 1, 3, 2, 22, 24, 23, 1, 3, 2, 22, 24, 23, 22, 24, 23, 1, 3, 2, 22, 24, 
          23, 1, 3, 2 ],
      103 := [ 1, 3, 2, 22, 24, 23, 4, 6, 5, 10, 12, 11, 7, 9, 8, 16, 18, 17, 19, 21, 
          20, 13, 15, 14 ],
      104 := [ 1, 3, 2, 22, 24, 23, 7, 9, 8, 16, 18, 17, 22, 24, 23, 1, 3, 2, 16, 18, 
          17, 7, 9, 8 ],
      105 := [ 1, 3, 2, 22, 24, 23, 13, 15, 14, 19, 21, 20, 7, 9, 8, 16, 18, 17, 10, 
          12, 11, 4, 6, 5 ],
      106 := [ 1, 3, 2, 22, 24, 23, 16, 18, 17, 7, 9, 8, 22, 24, 23, 1, 3, 2, 7, 9, 8, 
          16, 18, 17 ],
      107 := [ 1, 3, 2, 22, 24, 23, 22, 24, 23, 1, 3, 2, 22, 24, 23, 1, 3, 2, 1, 3, 2, 
          22, 24, 23 ],
      108 := [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 
          21, 22, 23, 24 ] ),
  classes := rec(
      1 := rec(
          phi := [ 1, 37, 72, 2, 38, 73, 3, 39, 74, 9, 108, 80, 4, 40, 75, 5, 41, 76, 
              12, 47, 83, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 80, 83, 85, 87, 108 ] ),
      2 := rec(
          phi := [ 1, 37, 72, 2, 38, 73, 3, 39, 74, 9, 108, 80, 4, 40, 75, 5, 41, 76, 
              21, 56, 92, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 80, 83, 85, 87, 108 ] ),
      3 := rec(
          phi := [ 1, 37, 72, 2, 38, 73, 3, 39, 74, 9, 108, 80, 4, 40, 75, 5, 41, 76, 
              21, 56, 92, 27, 62, 98 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 56, 59, 67, 69, 80, 83, 85, 87, 92, 
              95, 103, 105, 108 ] ),
      4 := rec(
          phi := [ 1, 37, 72, 2, 38, 73, 3, 39, 74, 9, 108, 80, 26, 61, 97, 5, 41, 76, 
              12, 47, 83, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 56, 59, 67, 69, 80, 83, 85, 87, 92, 
              95, 103, 105, 108 ] ),
      5 := rec(
          phi := [ 1, 37, 72, 7, 43, 78, 3, 39, 74, 9, 108, 80, 11, 46, 82, 5, 41, 76, 
              12, 47, 83, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 56, 59, 67, 69, 80, 83, 85, 87, 92, 
              95, 103, 105, 108 ] ),
      6 := rec(
          phi := [ 1, 37, 72, 7, 43, 78, 3, 39, 74, 9, 108, 80, 19, 54, 90, 5, 41, 76, 
              12, 47, 83, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 80, 83, 85, 87, 108 ] ),
      7 := rec(
          phi := [ 1, 37, 72, 7, 43, 78, 3, 39, 74, 9, 108, 80, 19, 54, 90, 5, 41, 76, 
              21, 56, 92, 6, 42, 77 ],
          autos_yielding_iso_nrs := [ 47, 49, 51, 80, 83, 85, 87, 108 ] ) ) );