YES

Problem:
 f(a()) -> g(h(a()))
 h(g(x)) -> g(h(f(x)))
 k(x,h(x),a()) -> h(x)
 k(f(x),y,x) -> f(x)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: top
  automaton:
   final states: {41,40,39,38,35,34,32,31,30,29,19,18,17,15,10,9,6}
   transitions:
    f0(40) -> 6*
    f0(35) -> 6*
    f0(30) -> 6*
    f0(15) -> 6*
    f0(10) -> 6*
    f0(32) -> 6*
    f0(17) -> 6*
    f0(39) -> 6*
    f0(34) -> 6*
    f0(29) -> 6*
    f0(19) -> 6*
    f0(9) -> 6*
    f0(41) -> 6*
    f0(31) -> 6*
    f0(6) -> 6*
    f0(38) -> 6*
    f0(18) -> 6*
    a0() -> 6*
    g0(40) -> 6*
    g0(35) -> 6*
    g0(30) -> 6*
    g0(15) -> 6*
    g0(10) -> 6*
    g0(32) -> 6*
    g0(17) -> 6*
    g0(39) -> 6*
    g0(34) -> 6*
    g0(29) -> 6*
    g0(19) -> 6*
    g0(9) -> 6*
    g0(41) -> 6*
    g0(31) -> 6*
    g0(6) -> 6*
    g0(38) -> 6*
    g0(18) -> 6*
    h0(40) -> 6*
    h0(35) -> 6*
    h0(30) -> 6*
    h0(15) -> 6*
    h0(10) -> 6*
    h0(32) -> 6*
    h0(17) -> 6*
    h0(39) -> 6*
    h0(34) -> 6*
    h0(29) -> 6*
    h0(19) -> 6*
    h0(9) -> 6*
    h0(41) -> 6*
    h0(31) -> 6*
    h0(6) -> 6*
    h0(38) -> 6*
    h0(18) -> 6*
    k0(15,10,19) -> 6*
    k0(29,38,6) -> 6*
    k0(18,38,15) -> 6*
    k0(38,18,17) -> 6*
    k0(32,31,10) -> 6*
    k0(31,29,39) -> 6*
    k0(41,31,29) -> 6*
    k0(30,9,10) -> 6*
    k0(35,29,38) -> 6*
    k0(39,9,29) -> 6*
    k0(19,40,41) -> 6*
    k0(31,15,6) -> 6*
    k0(17,18,41) -> 6*
    k0(39,6,10) -> 6*
    k0(9,35,32) -> 6*
    k0(34,39,32) -> 6*
    k0(9,9,34) -> 6*
    k0(17,30,6) -> 6*
    k0(38,39,31) -> 6*
    k0(32,17,32) -> 6*
    k0(32,6,18) -> 6*
    k0(6,39,9) -> 6*
    k0(31,39,39) -> 6*
    k0(35,19,30) -> 6*
    k0(30,41,38) -> 6*
    k0(10,15,30) -> 6*
    k0(9,17,29) -> 6*
    k0(19,19,19) -> 6*
    k0(9,6,15) -> 6*
    k0(39,10,35) -> 6*
    k0(34,10,15) -> 6*
    k0(18,32,32) -> 6*
    k0(18,6,34) -> 6*
    k0(10,34,39) -> 6*
    k0(30,38,19) -> 6*
    k0(40,40,9) -> 6*
    k0(34,18,10) -> 6*
    k0(29,40,18) -> 6*
    k0(39,38,38) -> 6*
    k0(9,10,40) -> 6*
    k0(38,18,9) -> 6*
    k0(17,40,6) -> 6*
    k0(6,40,15) -> 6*
    k0(31,29,31) -> 6*
    k0(30,31,30) -> 6*
    k0(15,40,34) -> 6*
    k0(19,31,39) -> 6*
    k0(39,35,19) -> 6*
    k0(9,18,35) -> 6*
    k0(17,9,39) -> 6*
    k0(35,17,17) -> 6*
    k0(40,41,15) -> 6*
    k0(29,30,10) -> 6*
    k0(19,17,6) -> 6*
    k0(38,30,29) -> 6*
    k0(18,15,35) -> 6*
    k0(38,19,15) -> 6*
    k0(15,41,40) -> 6*
    k0(19,10,17) -> 6*
    k0(30,6,38) -> 6*
    k0(19,41,39) -> 6*
    k0(34,32,35) -> 6*
    k0(6,34,32) -> 6*
    k0(31,38,32) -> 6*
    k0(30,29,17) -> 6*
    k0(35,38,31) -> 6*
    k0(10,34,31) -> 6*
    k0(34,40,30) -> 6*
    k0(18,40,19) -> 6*
    k0(32,18,30) -> 6*
    k0(31,9,15) -> 6*
    k0(15,31,32) -> 6*
    k0(40,35,32) -> 6*
    k0(40,9,34) -> 6*
    k0(9,29,41) -> 6*
    k0(19,31,31) -> 6*
    k0(17,35,29) -> 6*
    k0(31,17,10) -> 6*
    k0(41,15,30) -> 6*
    k0(6,9,40) -> 6*
    k0(35,17,9) -> 6*
    k0(30,39,17) -> 6*
    k0(30,15,39) -> 6*
    k0(40,17,29) -> 6*
    k0(40,6,15) -> 6*
    k0(34,15,38) -> 6*
    k0(17,32,10) -> 6*
    k0(38,41,35) -> 6*
    k0(41,34,39) -> 6*
    k0(6,17,35) -> 6*
    k0(15,10,10) -> 6*
    k0(10,32,18) -> 6*
    k0(40,10,40) -> 6*
    k0(9,34,17) -> 6*
    k0(15,6,40) -> 6*
    k0(10,17,34) -> 6*
    k0(40,18,35) -> 6*
    k0(35,29,29) -> 6*
    k0(35,18,15) -> 6*
    k0(30,29,9) -> 6*
    k0(19,29,18) -> 6*
    k0(19,40,32) -> 6*
    k0(18,31,17) -> 6*
    k0(17,18,32) -> 6*
    k0(31,31,35) -> 6*
    k0(10,18,40) -> 6*
    k0(32,6,9) -> 6*
    k0(6,35,30) -> 6*
    k0(31,39,30) -> 6*
    k0(30,41,29) -> 6*
    k0(30,30,15) -> 6*
    k0(15,39,19) -> 6*
    k0(30,15,31) -> 6*
    k0(34,10,6) -> 6*
    k0(19,19,10) -> 6*
    k0(9,6,6) -> 6*
    k0(39,30,34) -> 6*
    k0(19,15,40) -> 6*
    k0(29,17,30) -> 6*
    k0(18,41,17) -> 6*
    k0(18,17,39) -> 6*
    k0(30,38,10) -> 6*
    k0(31,32,41) -> 6*
    k0(41,34,31) -> 6*
    k0(15,32,30) -> 6*
    k0(30,34,40) -> 6*
    k0(39,38,29) -> 6*
    k0(9,10,31) -> 6*
    k0(34,38,9) -> 6*
    k0(9,34,9) -> 6*
    k0(29,10,41) -> 6*
    k0(6,10,38) -> 6*
    k0(39,35,10) -> 6*
    k0(40,29,41) -> 6*
    k0(35,40,35) -> 6*
    k0(9,38,34) -> 6*
    k0(39,31,40) -> 6*
    k0(18,31,9) -> 6*
    k0(32,35,18) -> 6*
    k0(17,29,38) -> 6*
    k0(9,35,15) -> 6*
    k0(29,15,17) -> 6*
    k0(34,39,15) -> 6*
    k0(38,19,6) -> 6*
    k0(18,35,34) -> 6*
    k0(32,17,15) -> 6*
    k0(41,32,18) -> 6*
    k0(40,34,17) -> 6*
    k0(15,30,17) -> 6*
    k0(41,17,34) -> 6*
    k0(35,41,41) -> 6*
    k0(30,6,29) -> 6*
    k0(39,10,18) -> 6*
    k0(9,39,40) -> 6*
    k0(19,41,30) -> 6*
    k0(18,32,15) -> 6*
    k0(18,17,31) -> 6*
    k0(17,19,30) -> 6*
    k0(6,19,39) -> 6*
    k0(10,19,38) -> 6*
    k0(18,40,10) -> 6*
    k0(19,34,41) -> 6*
    k0(31,9,6) -> 6*
    k0(41,18,40) -> 6*
    k0(15,40,17) -> 6*
    k0(9,29,32) -> 6*
    k0(9,18,18) -> 6*
    k0(6,9,31) -> 6*
    k0(40,6,6) -> 6*
    k0(30,35,38) -> 6*
    k0(10,9,30) -> 6*
    k0(29,15,9) -> 6*
    k0(34,15,29) -> 6*
    k0(18,15,18) -> 6*
    k0(17,17,17) -> 6*
    k0(32,39,35) -> 6*
    k0(31,41,34) -> 6*
    k0(40,10,31) -> 6*
    k0(35,32,39) -> 6*
    k0(15,6,31) -> 6*
    k0(30,32,19) -> 6*
    k0(40,34,9) -> 6*
    k0(15,30,9) -> 6*
    k0(35,6,41) -> 6*
    k0(29,34,18) -> 6*
    k0(39,32,38) -> 6*
    k0(29,19,34) -> 6*
    k0(19,6,30) -> 6*
    k0(6,34,15) -> 6*
    k0(31,38,15) -> 6*
    k0(6,19,31) -> 6*
    k0(35,18,6) -> 6*
    k0(15,34,34) -> 6*
    k0(40,38,34) -> 6*
    k0(39,29,19) -> 6*
    k0(38,31,18) -> 6*
    k0(32,40,41) -> 6*
    k0(17,38,31) -> 6*
    k0(6,38,40) -> 6*
    k0(15,31,15) -> 6*
    k0(40,35,15) -> 6*
    k0(10,38,39) -> 6*
    k0(30,18,41) -> 6*
    k0(9,40,38) -> 6*
    k0(18,9,35) -> 6*
    k0(15,39,10) -> 6*
    k0(30,30,6) -> 6*
    k0(40,39,40) -> 6*
    k0(15,35,40) -> 6*
    k0(34,41,19) -> 6*
    k0(19,39,9) -> 6*
    k0(39,15,41) -> 6*
    k0(38,17,40) -> 6*
    k0(17,17,9) -> 6*
    k0(32,19,19) -> 6*
    k0(31,32,32) -> 6*
    k0(6,17,18) -> 6*
    k0(31,6,34) -> 6*
    k0(41,19,38) -> 6*
    k0(35,32,31) -> 6*
    k0(9,30,30) -> 6*
    k0(29,10,32) -> 6*
    k0(34,34,30) -> 6*
    k0(18,34,19) -> 6*
    k0(6,10,29) -> 6*
    k0(40,29,32) -> 6*
    k0(40,18,18) -> 6*
    k0(30,40,6) -> 6*
    k0(19,40,15) -> 6*
    k0(29,38,35) -> 6*
    k0(32,31,39) -> 6*
    k0(17,29,29) -> 6*
    k0(17,18,15) -> 6*
    k0(41,9,30) -> 6*
    k0(30,9,39) -> 6*
    k0(9,35,6) -> 6*
    k0(34,9,38) -> 6*
    k0(32,17,6) -> 6*
    k0(38,35,35) -> 6*
    k0(31,15,35) -> 6*
    k0(35,41,32) -> 6*
    k0(35,30,18) -> 6*
    k0(39,10,9) -> 6*
    k0(34,32,17) -> 6*
    k0(35,15,34) -> 6*
    k0(29,39,41) -> 6*
    k0(39,41,31) -> 6*
    k0(34,6,19) -> 6*
    k0(39,6,39) -> 6*
    k0(18,32,6) -> 6*
    k0(32,10,17) -> 6*
    k0(32,41,39) -> 6*
    k0(6,39,38) -> 6*
    k0(10,19,29) -> 6*
    k0(19,34,32) -> 6*
    k0(31,40,19) -> 6*
    k0(41,38,39) -> 6*
    k0(40,40,38) -> 6*
    k0(9,38,17) -> 6*
    k0(34,18,39) -> 6*
    k0(29,18,19) -> 6*
    k0(38,18,38) -> 6*
    k0(32,31,31) -> 6*
    k0(17,40,35) -> 6*
    k0(6,29,30) -> 6*
    k0(30,35,29) -> 6*
    k0(39,39,18) -> 6*
    k0(19,9,40) -> 6*
    k0(38,15,19) -> 6*
    k0(30,32,10) -> 6*
    k0(35,6,32) -> 6*
    k0(40,30,30) -> 6*
    k0(29,30,39) -> 6*
    k0(39,32,29) -> 6*
    k0(19,17,35) -> 6*
    k0(34,32,9) -> 6*
    k0(17,41,41) -> 6*
    k0(6,34,6) -> 6*
    k0(10,30,35) -> 6*
    k0(39,29,10) -> 6*
    k0(35,34,35) -> 6*
    k0(15,19,41) -> 6*
    k0(9,32,34) -> 6*
    k0(32,40,32) -> 6*
    k0(32,29,18) -> 6*
    k0(31,31,17) -> 6*
    k0(40,35,6) -> 6*
    k0(15,31,6) -> 6*
    k0(30,18,32) -> 6*
    k0(10,38,30) -> 6*
    k0(9,40,29) -> 6*
    k0(9,29,15) -> 6*
    k0(29,9,17) -> 6*
    k0(34,18,31) -> 6*
    k0(29,40,39) -> 6*
    k0(18,29,34) -> 6*
    k0(35,35,41) -> 6*
    k0(10,31,41) -> 6*
    k0(34,41,10) -> 6*
    k0(39,15,32) -> 6*
    k0(19,35,30) -> 6*
    k0(38,41,9) -> 6*
    k0(38,6,17) -> 6*
    k0(32,19,10) -> 6*
    k0(32,15,40) -> 6*
    k0(31,17,39) -> 6*
    k0(41,19,29) -> 6*
    k0(31,41,17) -> 6*
    k0(15,41,6) -> 6*
    k0(35,17,38) -> 6*
    k0(18,34,10) -> 6*
    k0(29,30,31) -> 6*
    k0(18,30,40) -> 6*
    k0(17,32,39) -> 6*
    k0(17,6,41) -> 6*
    k0(40,38,17) -> 6*
    k0(10,10,19) -> 6*
    k0(15,10,39) -> 6*
    k0(19,10,38) -> 6*
    k0(17,18,6) -> 6*
    k0(31,31,9) -> 6*
    k0(30,29,38) -> 6*
    k0(34,9,29) -> 6*
    k0(18,9,18) -> 6*
    k0(31,35,34) -> 6*
    k0(6,31,34) -> 6*
    k0(29,39,32) -> 6*
    k0(34,6,10) -> 6*
    k0(32,41,30) -> 6*
    k0(31,32,15) -> 6*
    k0(6,39,29) -> 6*
    k0(41,30,35) -> 6*
    k0(31,17,31) -> 6*
    k0(40,32,34) -> 6*
    k0(30,19,30) -> 6*
    k0(34,10,35) -> 6*
    k0(19,19,39) -> 6*
    k0(9,6,35) -> 6*
    k0(29,10,15) -> 6*
    k0(38,10,34) -> 6*
    k0(32,34,41) -> 6*
    k0(17,32,31) -> 6*
    k0(31,40,10) -> 6*
    k0(41,38,30) -> 6*
    k0(6,32,40) -> 6*
    k0(40,29,15) -> 6*
    k0(35,40,9) -> 6*
    k0(40,40,29) -> 6*
    k0(29,18,10) -> 6*
    k0(34,38,38) -> 6*
    k0(9,34,38) -> 6*
    k0(38,18,29) -> 6*
    k0(41,31,41) -> 6*
    k0(10,40,34) -> 6*
    k0(15,29,40) -> 6*
    k0(19,9,31) -> 6*
    k0(34,35,19) -> 6*
    k0(9,31,19) -> 6*
    k0(39,35,39) -> 6*
    k0(38,15,10) -> 6*
    k0(39,9,41) -> 6*
    k0(18,31,38) -> 6*
    k0(31,15,18) -> 6*
    k0(30,17,17) -> 6*
    k0(35,41,15) -> 6*
    k0(38,19,35) -> 6*
    k0(17,41,32) -> 6*
    k0(17,30,18) -> 6*
    k0(32,6,30) -> 6*
    k0(17,15,34) -> 6*
    k0(41,10,19) -> 6*
    k0(15,19,32) -> 6*
    k0(10,41,40) -> 6*
    k0(19,34,15) -> 6*
    k0(29,32,35) -> 6*
    k0(9,17,41) -> 6*
    k0(19,19,31) -> 6*
    k0(9,29,6) -> 6*
    k0(30,38,31) -> 6*
    k0(19,38,40) -> 6*
    k0(29,40,30) -> 6*
    k0(38,29,35) -> 6*
    k0(31,9,35) -> 6*
    k0(10,31,32) -> 6*
    k0(35,35,32) -> 6*
    k0(35,9,34) -> 6*
    k0(39,35,31) -> 6*
    k0(32,39,9) -> 6*
    k0(30,17,9) -> 6*
    k0(40,6,35) -> 6*
    k0(35,17,29) -> 6*
    k0(35,6,15) -> 6*
    k0(19,17,18) -> 6*
    k0(9,39,6) -> 6*
    k0(29,15,38) -> 6*
    k0(18,19,17) -> 6*
    k0(38,30,41) -> 6*
    k0(17,6,32) -> 6*
    k0(31,34,19) -> 6*
    k0(6,30,19) -> 6*
    k0(10,10,10) -> 6*
    k0(35,10,40) -> 6*
    k0(40,34,38) -> 6*
    k0(10,6,40) -> 6*
    k0(15,30,38) -> 6*
    k0(19,10,29) -> 6*
    k0(32,40,15) -> 6*
    k0(17,34,35) -> 6*
    k0(41,40,34) -> 6*
    k0(35,18,35) -> 6*
    k0(30,29,29) -> 6*
    k0(40,31,19) -> 6*
    k0(30,18,15) -> 6*
    k0(38,35,17) -> 6*
    k0(18,9,9) -> 6*
    k0(39,18,34) -> 6*
    k0(38,9,19) -> 6*
    k0(18,40,31) -> 6*
    k0(39,15,15) -> 6*
    k0(17,35,41) -> 6*
    k0(31,32,6) -> 6*
    k0(41,41,40) -> 6*
    k0(10,39,19) -> 6*
    k0(29,10,6) -> 6*
    k0(40,17,41) -> 6*
    k0(9,41,18) -> 6*
    k0(34,30,34) -> 6*
    k0(19,39,38) -> 6*
    k0(39,19,40) -> 6*
    k0(18,19,9) -> 6*
    k0(32,34,32) -> 6*
    k0(17,17,38) -> 6*
    k0(40,29,6) -> 6*
    k0(10,32,30) -> 6*
    k0(9,34,29) -> 6*
    k0(29,38,9) -> 6*
    k0(34,38,29) -> 6*
    k0(18,38,18) -> 6*
    k0(6,38,6) -> 6*
    k0(41,31,32) -> 6*
    k0(15,18,17) -> 6*
    k0(9,31,10) -> 6*
    k0(35,29,41) -> 6*
    k0(30,40,35) -> 6*
    k0(34,35,10) -> 6*
    k0(39,9,32) -> 6*
    k0(34,31,40) -> 6*
    k0(19,29,30) -> 6*
    k0(18,31,29) -> 6*
    k0(38,35,9) -> 6*
    k0(32,9,40) -> 6*
    k0(40,39,6) -> 6*
    k0(29,39,15) -> 6*
    k0(38,39,34) -> 6*
    k0(32,17,35) -> 6*
    k0(41,10,10) -> 6*
    k0(35,34,17) -> 6*
    k0(41,6,40) -> 6*
    k0(10,30,17) -> 6*
    k0(15,39,31) -> 6*
    k0(19,34,6) -> 6*
    k0(30,41,41) -> 6*
    k0(34,10,18) -> 6*
    k0(9,17,32) -> 6*
    k0(9,6,18) -> 6*
    k0(39,38,41) -> 6*
    k0(38,40,40) -> 6*
    k0(17,40,9) -> 6*
    k0(6,40,18) -> 6*
    k0(31,29,34) -> 6*
    k0(15,18,9) -> 6*
    k0(10,40,17) -> 6*
    k0(32,35,30) -> 6*
    k0(41,39,19) -> 6*
    k0(40,41,18) -> 6*
    k0(35,6,6) -> 6*
    k0(29,15,29) -> 6*
    k0(39,17,19) -> 6*
    k0(38,19,18) -> 6*
    k0(38,30,32) -> 6*
    k0(17,41,15) -> 6*
    k0(6,30,10) -> 6*
    k0(31,34,10) -> 6*
    k0(31,30,40) -> 6*
    k0(41,32,30) -> 6*
    k0(30,32,39) -> 6*
    k0(40,34,29) -> 6*
    k0(10,6,31) -> 6*
    k0(15,30,29) -> 6*
    k0(35,34,9) -> 6*
    k0(15,19,15) -> 6*
    k0(10,30,9) -> 6*
    k0(35,10,31) -> 6*
    k0(30,6,41) -> 6*
    k0(39,10,30) -> 6*
    k0(34,32,38) -> 6*
    k0(32,10,38) -> 6*
    k0(40,31,10) -> 6*
    k0(30,18,6) -> 6*
    k0(10,34,34) -> 6*
    k0(35,38,34) -> 6*
    k0(39,29,39) -> 6*
    k0(34,29,19) -> 6*
    k0(38,9,10) -> 6*
    k0(31,9,18) -> 6*
    k0(10,31,15) -> 6*
    k0(35,35,15) -> 6*
    k0(39,15,6) -> 6*
    k0(19,31,34) -> 6*
    k0(9,18,30) -> 6*
    k0(17,35,32) -> 6*
    k0(41,30,17) -> 6*
    k0(17,9,34) -> 6*
    k0(10,39,10) -> 6*
    k0(40,17,32) -> 6*
    k0(35,39,40) -> 6*
    k0(40,6,18) -> 6*
    k0(10,35,40) -> 6*
    k0(19,39,29) -> 6*
    k0(29,41,19) -> 6*
    k0(34,15,41) -> 6*
    k0(39,39,39) -> 6*
    k0(38,41,38) -> 6*
    k0(18,15,30) -> 6*
    k0(32,19,39) -> 6*
    k0(17,17,29) -> 6*
    k0(17,6,15) -> 6*
    k0(30,32,31) -> 6*
    k0(15,41,35) -> 6*
    k0(19,32,40) -> 6*
    k0(29,34,30) -> 6*
    k0(18,34,39) -> 6*
    k0(38,38,19) -> 6*
    k0(17,10,40) -> 6*
    k0(41,40,17) -> 6*
    k0(35,18,18) -> 6*
    k0(35,29,32) -> 6*
    k0(39,29,31) -> 6*
    k0(38,31,30) -> 6*
    k0(32,9,31) -> 6*
    k0(17,18,35) -> 6*
    k0(31,31,38) -> 6*
    k0(29,9,38) -> 6*
    k0(41,6,31) -> 6*
    k0(41,30,9) -> 6*
    k0(30,41,32) -> 6*
    k0(30,30,18) -> 6*
    k0(34,10,9) -> 6*
    k0(29,32,17) -> 6*
    k0(9,6,9) -> 6*
    k0(30,15,34) -> 6*
    k0(34,41,31) -> 6*
    k0(29,6,19) -> 6*
    k0(34,6,39) -> 6*
    k0(38,6,38) -> 6*
    k0(32,34,15) -> 6*
    k0(32,19,31) -> 6*
    k0(6,17,30) -> 6*
    k0(41,34,34) -> 6*
    k0(39,38,32) -> 6*
    k0(38,29,17) -> 6*
    k0(18,34,31) -> 6*
    k0(32,38,40) -> 6*
    k0(41,31,15) -> 6*
    k0(6,10,41) -> 6*
    k0(40,18,30) -> 6*
    k0(35,40,38) -> 6*
    k0(29,18,39) -> 6*
    k0(39,9,15) -> 6*
    k0(17,29,41) -> 6*
    k0(41,39,10) -> 6*
    k0(41,35,40) -> 6*
    k0(39,17,10) -> 6*
    k0(34,39,18) -> 6*
    k0(9,35,18) -> 6*
    k0(38,15,39) -> 6*
    k0(38,39,17) -> 6*
    k0(32,17,18) -> 6*
    k0(31,19,17) -> 6*
    k0(6,15,17) -> 6*
    k0(15,19,6) -> 6*
    k0(30,6,32) -> 6*
    k0(35,30,30) -> 6*
    k0(34,32,29) -> 6*
    k0(19,30,19) -> 6*
    k0(29,32,9) -> 6*
    k0(9,17,15) -> 6*
    k0(18,32,18) -> 6*
    k0(17,34,17) -> 6*
    k0(18,17,34) -> 6*
    k0(32,10,29) -> 6*
    k0(34,29,10) -> 6*
    k0(30,34,35) -> 6*
    k0(10,19,41) -> 6*
    k0(38,29,9) -> 6*
    k0(31,9,9) -> 6*
    k0(31,40,31) -> 6*
    k0(35,35,6) -> 6*
    k0(10,31,6) -> 6*
    k0(39,31,35) -> 6*
    k0(29,18,31) -> 6*
    k0(18,18,40) -> 6*
    k0(40,6,9) -> 6*
    k0(30,35,41) -> 6*
    k0(29,41,10) -> 6*
    k0(34,15,32) -> 6*
    k0(39,39,30) -> 6*
    k0(38,41,29) -> 6*
    k0(38,30,15) -> 6*
    k0(17,6,6) -> 6*
    k0(38,15,31) -> 6*
    k0(32,39,38) -> 6*
    k0(6,15,9) -> 6*
    k0(31,19,9) -> 6*
    k0(10,41,6) -> 6*
    k0(30,17,38) -> 6*
    k0(39,32,41) -> 6*
    k0(9,39,35) -> 6*
    k0(38,38,10) -> 6*
    k0(38,34,40) -> 6*
    k0(17,10,31) -> 6*
    k0(17,34,9) -> 6*
    k0(31,38,18) -> 6*
    k0(6,34,18) -> 6*
    k0(6,19,34) -> 6*
    k0(10,10,39) -> 6*
    k0(35,38,17) -> 6*
    k0(19,38,6) -> 6*
    k0(32,29,30) -> 6*
    k0(17,38,34) -> 6*
    k0(31,31,29) -> 6*
    k0(40,35,18) -> 6*
    k0(15,31,18) -> 6*
    k0(9,40,41) -> 6*
    k0(29,9,29) -> 6*
    k0(17,35,15) -> 6*
    k0(40,17,15) -> 6*
    k0(29,6,10) -> 6*
    k0(32,34,6) -> 6*
    k0(38,6,29) -> 6*
    k0(17,39,40) -> 6*
    k0(41,19,41) -> 6*
    k0(35,32,34) -> 6*
    k0(15,17,40) -> 6*
    k0(29,10,35) -> 6*
    k0(9,19,19) -> 6*
    k0(18,19,38) -> 6*
    k0(41,31,6) -> 6*
    k0(6,10,32) -> 6*
    k0(30,40,9) -> 6*
    k0(35,40,29) -> 6*
    k0(35,29,15) -> 6*
    k0(39,9,6) -> 6*
    k0(19,40,18) -> 6*
    k0(29,38,38) -> 6*
    k0(17,29,32) -> 6*
    k0(17,18,18) -> 6*
    k0(6,38,35) -> 6*
    k0(10,29,40) -> 6*
    k0(9,31,39) -> 6*
    k0(29,35,19) -> 6*
    k0(34,35,39) -> 6*
    k0(34,9,41) -> 6*
    k0(38,35,38) -> 6*
    k0(18,9,30) -> 6*
    k0(41,41,6) -> 6*
    k0(30,41,15) -> 6*
    k0(19,30,10) -> 6*
    k0(9,17,6) -> 6*
    k0(40,39,35) -> 6*
    k0(15,35,35) -> 6*
    k0(39,41,34) -> 6*
    k0(38,32,19) -> 6*
    k0(6,39,41) -> 6*
    k0(41,10,39) -> 6*
    k0(10,19,32) -> 6*
    k0(39,38,15) -> 6*
    k0(9,10,17) -> 6*
    k0(9,41,39) -> 6*
    k0(40,40,41) -> 6*
    k0(38,18,41) -> 6*
    k0(18,38,39) -> 6*
    k0(32,31,34) -> 6*
    k0(17,40,38) -> 6*
    k0(6,18,19) -> 6*
    k0(30,35,32) -> 6*
    k0(30,9,34) -> 6*
    k0(15,18,38) -> 6*
    k0(34,35,31) -> 6*
    k0(9,31,31) -> 6*
    k0(38,30,6) -> 6*
    k0(32,39,29) -> 6*
    k0(31,15,30) -> 6*
    k0(35,6,35) -> 6*
    k0(30,17,29) -> 6*
    k0(40,19,19) -> 6*
    k0(30,6,15) -> 6*
    k0(15,15,19) -> 6*
    k0(39,32,32) -> 6*
    k0(39,6,34) -> 6*
    k0(32,32,40) -> 6*
    k0(17,30,30) -> 6*
    k0(6,30,39) -> 6*
    k0(31,34,39) -> 6*
    k0(30,10,40) -> 6*
    k0(35,34,38) -> 6*
    k0(10,30,38) -> 6*
    k0(38,40,6) -> 6*
    k0(41,29,40) -> 6*
    k0(30,18,35) -> 6*
    k0(35,31,19) -> 6*
    k0(40,31,39) -> 6*
    k0(9,40,32) -> 6*
    k0(9,29,18) -> 6*
    k0(34,18,34) -> 6*
    k0(38,9,39) -> 6*
    k0(17,35,6) -> 6*
    k0(6,9,17) -> 6*
    k0(40,17,6) -> 6*
    k0(6,40,39) -> 6*
    k0(39,15,35) -> 6*
    k0(34,15,15) -> 6*
    k0(41,19,32) -> 6*
    k0(15,41,9) -> 6*
    k0(40,10,17) -> 6*
    k0(15,6,17) -> 6*
    k0(9,19,10) -> 6*
    k0(35,17,41) -> 6*
    k0(40,41,39) -> 6*
    k0(29,30,34) -> 6*
    k0(9,15,40) -> 6*
    k0(19,17,30) -> 6*
    k0(34,19,40) -> 6*
    k0(18,19,29) -> 6*
    k0(31,34,31) -> 6*
    k0(6,30,31) -> 6*
    k0(35,29,6) -> 6*
    k0(29,38,29) -> 6*
    k0(39,40,19) -> 6*
    k0(19,10,41) -> 6*
    k0(17,38,17) -> 6*
    k0(10,18,17) -> 6*
    k0(30,29,41) -> 6*
    k0(40,31,31) -> 6*
    k0(29,35,10) -> 6*
    k0(34,9,32) -> 6*
    k0(29,31,40) -> 6*
    k0(38,35,29) -> 6*
    k0(35,39,6) -> 6*
    k0(19,15,17) -> 6*
    k0(38,32,10) -> 6*
    k0(32,30,19) -> 6*
    k0(31,32,18) -> 6*
    k0(6,39,32) -> 6*
    k0(41,30,38) -> 6*
    k0(31,17,34) -> 6*
    k0(30,34,17) -> 6*
    k0(10,39,31) -> 6*
    k0(29,10,18) -> 6*
    k0(9,41,30) -> 6*
    k0(18,30,35) -> 6*
    k0(17,32,34) -> 6*
    k0(6,10,15) -> 6*
    k0(40,40,32) -> 6*
    k0(40,29,18) -> 6*
    k0(39,31,17) -> 6*
    k0(15,10,34) -> 6*
    k0(9,34,41) -> 6*
    k0(34,38,41) -> 6*
    k0(38,18,32) -> 6*
    k0(18,38,30) -> 6*
    k0(17,29,15) -> 6*
    k0(17,40,29) -> 6*
    k0(6,18,10) -> 6*
    k0(31,18,40) -> 6*
    k0(10,18,9) -> 6*
    k0(15,18,29) -> 6*
    k0(18,31,41) -> 6*
    k0(40,19,10) -> 6*
    k0(35,41,18) -> 6*
    k0(30,6,6) -> 6*
    k0(15,15,10) -> 6*
    k0(40,15,40) -> 6*
    k0(19,15,9) -> 6*
    k0(39,17,39) -> 6*
    k0(34,17,19) -> 6*
    k0(39,41,17) -> 6*
    k0(15,19,35) -> 6*
    k0(10,30,29) -> 6*
    k0(30,34,9) -> 6*
    k0(10,19,15) -> 6*
    k0(30,10,31) -> 6*
    k0(35,34,29) -> 6*
    k0(19,34,18) -> 6*
    k0(34,10,30) -> 6*
    k0(29,32,38) -> 6*
    k0(19,19,34) -> 6*
    k0(9,6,30) -> 6*
    k0(18,10,19) -> 6*
    k0(32,38,6) -> 6*
    k0(41,18,17) -> 6*
    k0(6,32,35) -> 6*
    k0(35,31,10) -> 6*
    k0(30,38,34) -> 6*
    k0(29,29,19) -> 6*
    k0(39,31,9) -> 6*
    k0(34,29,39) -> 6*
    k0(38,29,38) -> 6*
    k0(6,40,30) -> 6*
    k0(30,35,15) -> 6*
    k0(34,15,6) -> 6*
    k0(15,29,35) -> 6*
    k0(39,35,34) -> 6*
    k0(41,39,31) -> 6*
    k0(35,17,32) -> 6*
    k0(30,39,40) -> 6*
    k0(40,41,30) -> 6*
    k0(35,6,18) -> 6*
    k0(9,39,9) -> 6*
    k0(39,32,15) -> 6*
    k0(29,15,41) -> 6*
    k0(39,17,31) -> 6*
    k0(34,39,39) -> 6*
    k0(38,19,30) -> 6*
    k0(17,6,35) -> 6*
    k0(6,15,38) -> 6*
    k0(31,19,38) -> 6*
    k0(15,30,41) -> 6*
    k0(10,41,35) -> 6*
    k0(39,40,10) -> 6*
    k0(40,34,41) -> 6*
    k0(19,10,32) -> 6*
    k0(32,40,18) -> 6*
    k0(17,34,38) -> 6*
    k0(41,18,9) -> 6*
    k0(30,18,18) -> 6*
    k0(30,29,32) -> 6*
    k0(9,40,15) -> 6*
    k0(34,29,31) -> 6*
    k0(19,38,35) -> 6*
    k0(18,40,34) -> 6*
    k0(17,31,19) -> 6*
    k0(15,35,17) -> 6*
    k0(31,9,30) -> 6*
    k0(15,9,19) -> 6*
    k0(39,15,18) -> 6*
    k0(38,17,17) -> 6*
    k0(32,30,10) -> 6*
    k0(41,30,29) -> 6*
    k0(41,19,15) -> 6*
    k0(29,10,9) -> 6*
    k0(40,6,30) -> 6*
    k0(29,6,39) -> 6*
    k0(19,39,41) -> 6*
    k0(29,41,31) -> 6*
    k0(18,41,40) -> 6*
    k0(6,10,6) -> 6*
    k0(17,17,41) -> 6*
    k0(34,38,32) -> 6*
    k0(9,34,32) -> 6*
    k0(17,29,6) -> 6*
    k0(38,38,31) -> 6*
    k0(6,38,9) -> 6*
    k0(31,38,39) -> 6*
    k0(35,18,30) -> 6*
    k0(30,40,38) -> 6*
    k0(39,9,35) -> 6*
    k0(34,9,15) -> 6*
    k0(19,18,19) -> 6*
    k0(18,31,32) -> 6*
    k0(40,39,9) -> 6*
    k0(15,35,9) -> 6*
    k0(34,17,10) -> 6*
    k0(29,39,18) -> 6*
    k0(9,9,40) -> 6*
    k0(38,17,9) -> 6*
    k0(17,39,6) -> 6*
    k0(6,39,15) -> 6*
    k0(10,19,6) -> 6*
    k0(41,41,35) -> 6*
    k0(30,30,30) -> 6*
    k0(15,39,34) -> 6*
    k0(19,30,39) -> 6*
    k0(29,32,29) -> 6*
    k0(39,34,19) -> 6*
    k0(9,17,35) -> 6*
    k0(18,10,10) -> 6*
    k0(18,6,40) -> 6*
    k0(40,40,15) -> 6*
    k0(29,29,10) -> 6*
    k0(38,29,29) -> 6*
    k0(38,18,15) -> 6*
    k0(30,35,6) -> 6*
    k0(15,40,40) -> 6*
    k0(19,9,17) -> 6*
    k0(34,31,35) -> 6*
    k0(19,40,39) -> 6*
    k0(35,6,9) -> 6*
    k0(39,32,6) -> 6*
    k0(29,15,32) -> 6*
    k0(34,39,30) -> 6*
    k0(9,35,30) -> 6*
    k0(18,39,19) -> 6*
    k0(17,41,18) -> 6*
    k0(32,17,30) -> 6*
    k0(31,19,29) -> 6*
    k0(6,15,29) -> 6*
    k0(15,19,18) -> 6*
    k0(40,34,32) -> 6*
    k0(15,30,32) -> 6*
    k0(34,32,41) -> 6*
    k0(19,30,31) -> 6*
    k0(18,32,30) -> 6*
    k0(17,34,29) -> 6*
    k0(32,10,41) -> 6*
    k0(30,38,17) -> 6*
    k0(9,10,38) -> 6*
    k0(17,31,10) -> 6*
    k0(38,40,35) -> 6*
    k0(35,35,18) -> 6*
    k0(15,9,10) -> 6*
    k0(10,31,18) -> 6*
    k0(40,9,40) -> 6*
    k0(32,15,17) -> 6*
    k0(41,19,6) -> 6*
    k0(35,17,15) -> 6*
    k0(40,17,35) -> 6*
    k0(19,39,32) -> 6*
    k0(18,30,17) -> 6*
    k0(38,41,41) -> 6*
    k0(17,17,32) -> 6*
    k0(17,6,18) -> 6*
    k0(6,41,19) -> 6*
    k0(31,30,35) -> 6*
    k0(10,17,40) -> 6*
    k0(15,41,38) -> 6*
    k0(30,32,34) -> 6*
    k0(9,19,39) -> 6*
    k0(19,10,15) -> 6*
    k0(31,38,30) -> 6*
    k0(6,34,30) -> 6*
    k0(15,38,19) -> 6*
    k0(30,40,29) -> 6*
    k0(30,29,15) -> 6*
    k0(34,9,6) -> 6*
    k0(19,18,10) -> 6*
    k0(39,29,34) -> 6*
    k0(18,40,17) -> 6*
    k0(31,31,41) -> 6*
    k0(40,35,30) -> 6*
    k0(15,31,30) -> 6*
    k0(9,9,31) -> 6*
    k0(29,35,39) -> 6*
    k0(29,9,41) -> 6*
    k0(32,15,9) -> 6*
    k0(6,9,38) -> 6*
    k0(35,39,35) -> 6*
    k0(10,35,35) -> 6*
    k0(39,34,10) -> 6*
    k0(39,30,40) -> 6*
    k0(34,41,34) -> 6*
    k0(18,6,31) -> 6*
    k0(18,30,9) -> 6*
    k0(38,32,39) -> 6*
    k0(32,34,18) -> 6*
    k0(38,6,41) -> 6*
    k0(6,32,17) -> 6*
    k0(32,19,34) -> 6*
    k0(6,6,19) -> 6*
    k0(31,10,19) -> 6*
    k0(15,6,38) -> 6*
    k0(34,38,15) -> 6*
    k0(40,10,38) -> 6*
    k0(9,34,15) -> 6*
    k0(19,32,35) -> 6*
    k0(9,19,31) -> 6*
    k0(38,18,6) -> 6*
    k0(18,34,34) -> 6*
    k0(41,31,18) -> 6*
    k0(15,29,17) -> 6*
    k0(35,40,41) -> 6*
    k0(39,9,18) -> 6*
    k0(9,38,40) -> 6*
    k0(19,40,30) -> 6*
    k0(18,31,15) -> 6*
    k0(17,18,30) -> 6*
    k0(6,18,39) -> 6*
    k0(10,18,38) -> 6*
    k0(29,35,31) -> 6*
    k0(18,39,10) -> 6*
    k0(18,35,40) -> 6*
    k0(41,17,40) -> 6*
    k0(40,19,39) -> 6*
    k0(30,6,35) -> 6*
    k0(15,15,39) -> 6*
    k0(35,19,19) -> 6*
    k0(10,15,19) -> 6*
    k0(15,39,17) -> 6*
    k0(9,17,18) -> 6*
    k0(34,32,32) -> 6*
    k0(34,6,34) -> 6*
    k0(19,15,38) -> 6*
    k0(38,32,31) -> 6*
    k0(32,10,32) -> 6*
    k0(6,32,9) -> 6*
    k0(30,34,38) -> 6*
    k0(9,10,29) -> 6*
    k0(32,38,35) -> 6*
    k0(31,40,34) -> 6*
    k0(30,31,19) -> 6*
    k0(15,29,9) -> 6*
    k0(40,9,31) -> 6*
    k0(35,31,39) -> 6*
    k0(39,31,38) -> 6*
    k0(29,18,34) -> 6*
    k0(41,35,35) -> 6*
    k0(6,18,31) -> 6*
    k0(35,17,6) -> 6*
    k0(29,15,15) -> 6*
    k0(34,15,35) -> 6*
    k0(38,41,32) -> 6*
    k0(38,30,18) -> 6*
    k0(17,6,9) -> 6*
    k0(38,15,34) -> 6*
    k0(6,41,10) -> 6*
    k0(32,39,41) -> 6*
    k0(31,41,40) -> 6*
    k0(10,41,9) -> 6*
    k0(35,10,17) -> 6*
    k0(40,34,15) -> 6*
    k0(15,41,29) -> 6*
    k0(10,6,17) -> 6*
    k0(15,30,15) -> 6*
    k0(19,10,6) -> 6*
    k0(30,17,41) -> 6*
    k0(40,19,31) -> 6*
    k0(35,41,39) -> 6*
    k0(15,15,31) -> 6*
    k0(9,39,38) -> 6*
    k0(29,19,40) -> 6*
    k0(30,29,6) -> 6*
    k0(15,38,10) -> 6*
    k0(40,38,40) -> 6*
    k0(15,34,40) -> 6*
    k0(19,38,9) -> 6*
    k0(34,40,19) -> 6*
    k0(32,18,19) -> 6*
    k0(31,31,32) -> 6*
    k0(41,18,38) -> 6*
    k0(35,31,31) -> 6*
    k0(29,9,32) -> 6*
    k0(9,29,30) -> 6*
    k0(17,35,18) -> 6*
    k0(41,15,19) -> 6*
    k0(6,9,29) -> 6*
    k0(30,39,6) -> 6*
    k0(40,17,18) -> 6*
    k0(39,19,17) -> 6*
    k0(19,39,15) -> 6*
    k0(38,6,32) -> 6*
    k0(17,17,15) -> 6*
    k0(32,30,39) -> 6*
    k0(31,10,10) -> 6*
    k0(6,6,10) -> 6*
    k0(31,6,40) -> 6*
    k0(40,10,29) -> 6*
    k0(9,34,6) -> 6*
    k0(15,6,29) -> 6*
    k0(38,34,35) -> 6*
    k0(18,19,41) -> 6*
    k0(6,10,35) -> 6*
    k0(35,40,32) -> 6*
    k0(35,29,18) -> 6*
    k0(10,10,34) -> 6*
    k0(39,9,9) -> 6*
    k0(34,31,17) -> 6*
    k0(18,31,6) -> 6*
    k0(29,38,41) -> 6*
    k0(39,40,31) -> 6*
    k0(32,9,17) -> 6*
    k0(32,40,39) -> 6*
    k0(6,38,38) -> 6*
    k0(10,18,29) -> 6*
    k0(38,35,41) -> 6*
    k0(6,35,19) -> 6*
    k0(41,6,17) -> 6*
    k0(31,39,19) -> 6*
    k0(41,41,9) -> 6*
    k0(35,19,10) -> 6*
    k0(30,41,18) -> 6*
    k0(10,15,10) -> 6*
    k0(15,35,38) -> 6*
    k0(35,15,40) -> 6*
    k0(40,39,38) -> 6*
    k0(34,17,39) -> 6*
    k0(19,15,29) -> 6*
    k0(29,17,19) -> 6*
    k0(39,19,9) -> 6*
    k0(34,41,17) -> 6*
    k0(18,41,6) -> 6*
    k0(38,17,38) -> 6*
    k0(32,30,31) -> 6*
    k0(17,39,35) -> 6*
    k0(31,32,30) -> 6*
    k0(10,19,35) -> 6*
    k0(15,32,19) -> 6*
    k0(30,34,29) -> 6*
    k0(39,38,18) -> 6*
    k0(29,10,30) -> 6*
    k0(18,10,39) -> 6*
    k0(30,31,10) -> 6*
    k0(40,29,30) -> 6*
    k0(34,31,9) -> 6*
    k0(29,29,39) -> 6*
    k0(39,31,29) -> 6*
    k0(17,40,41) -> 6*
    k0(29,15,6) -> 6*
    k0(15,18,41) -> 6*
    k0(10,29,35) -> 6*
    k0(9,31,34) -> 6*
    k0(34,35,34) -> 6*
    k0(32,39,32) -> 6*
    k0(31,30,17) -> 6*
    k0(40,34,6) -> 6*
    k0(15,30,6) -> 6*
    k0(30,17,32) -> 6*
    k0(35,41,30) -> 6*
    k0(30,6,18) -> 6*
    k0(34,32,15) -> 6*
    k0(9,39,29) -> 6*
    k0(19,41,19) -> 6*
    k0(34,17,31) -> 6*
    k0(29,39,39) -> 6*
    k0(32,10,15) -> 6*
    k0(17,19,19) -> 6*
    k0(41,10,34) -> 6*
    k0(10,30,41) -> 6*
    k0(34,40,10) -> 6*
    k0(35,34,41) -> 6*
    k0(9,32,40) -> 6*
    k0(19,34,30) -> 6*
    k0(38,40,9) -> 6*
    k0(32,18,10) -> 6*
    k0(41,18,29) -> 6*
    k0(31,40,17) -> 6*
    k0(15,40,6) -> 6*
    k0(29,29,31) -> 6*
    k0(18,29,40) -> 6*
    k0(17,31,39) -> 6*
    k0(41,15,10) -> 6*
    k0(10,35,17) -> 6*
    k0(15,9,39) -> 6*
    k0(10,9,19) -> 6*
    k0(34,15,18) -> 6*
    k0(19,9,38) -> 6*
    k0(38,41,15) -> 6*
    k0(17,17,6) -> 6*
    k0(31,30,9) -> 6*
    k0(41,19,35) -> 6*
    k0(31,6,31) -> 6*
    k0(35,6,30) -> 6*
    k0(19,32,17) -> 6*
    k0(19,6,19) -> 6*
    k0(18,19,32) -> 6*
    k0(17,10,17) -> 6*
    k0(32,32,35) -> 6*
    k0(17,41,39) -> 6*
    k0(6,30,34) -> 6*
    k0(31,34,34) -> 6*
    k0(29,38,32) -> 6*
    k0(32,40,30) -> 6*
    k0(31,31,15) -> 6*
    k0(6,38,29) -> 6*
    k0(41,29,35) -> 6*
    k0(40,31,34) -> 6*
    k0(30,18,30) -> 6*
    k0(34,9,35) -> 6*
    k0(19,18,39) -> 6*
    k0(29,9,15) -> 6*
    k0(38,35,32) -> 6*
    k0(38,9,34) -> 6*
    k0(17,31,31) -> 6*
    k0(31,39,10) -> 6*
    k0(6,35,10) -> 6*
    k0(31,35,40) -> 6*
    k0(6,31,40) -> 6*
    k0(10,35,9) -> 6*
    k0(40,39,29) -> 6*
    k0(15,35,29) -> 6*
    k0(35,39,9) -> 6*
    k0(29,17,10) -> 6*
    k0(39,15,30) -> 6*
    k0(38,17,29) -> 6*
    k0(38,6,15) -> 6*
    k0(32,15,38) -> 6*
    k0(15,32,10) -> 6*
    k0(41,30,41) -> 6*
    k0(40,32,40) -> 6*
    k0(10,39,34) -> 6*
    k0(9,30,19) -> 6*
    k0(19,32,9) -> 6*
    k0(39,34,39) -> 6*
    k0(34,34,19) -> 6*
    k0(18,30,38) -> 6*
    k0(38,10,40) -> 6*
    k0(6,10,18) -> 6*
    k0(35,40,15) -> 6*
    k0(38,18,35) -> 6*
    k0(17,40,32) -> 6*
    k0(17,29,18) -> 6*
    k0(41,35,17) -> 6*
    k0(41,9,19) -> 6*
    k0(15,18,32) -> 6*
    k0(10,40,40) -> 6*
    k0(29,31,35) -> 6*
    k0(19,18,31) -> 6*
    k0(30,6,9) -> 6*
    k0(34,32,6) -> 6*
    k0(19,41,10) -> 6*
    k0(29,39,30) -> 6*
    k0(32,10,6) -> 6*
    k0(17,19,10) -> 6*
    k0(17,15,40) -> 6*
    k0(10,19,18) -> 6*
    k0(35,34,32) -> 6*
    k0(10,30,32) -> 6*
    k0(29,32,41) -> 6*
    k0(39,34,31) -> 6*
    k0(32,38,9) -> 6*
    k0(6,32,38) -> 6*
    k0(9,38,6) -> 6*
    k0(18,18,17) -> 6*
    k0(38,29,41) -> 6*
    k0(41,35,9) -> 6*
    k0(6,29,19) -> 6*
    k0(30,35,18) -> 6*
    k0(10,9,10) -> 6*
    k0(15,29,38) -> 6*
    k0(35,9,40) -> 6*
    k0(19,9,29) -> 6*
    k0(32,39,15) -> 6*
    k0(41,39,34) -> 6*
    k0(40,30,19) -> 6*
    k0(30,17,15) -> 6*
    k0(35,17,35) -> 6*
    k0(39,32,18) -> 6*
    k0(19,6,10) -> 6*
    k0(39,17,34) -> 6*
    k0(38,34,17) -> 6*
    k0(18,39,31) -> 6*
    k0(17,41,30) -> 6*
    k0(31,19,41) -> 6*
    k0(6,15,41) -> 6*
    k0(15,19,30) -> 6*
    k0(10,41,38) -> 6*
    k0(19,10,35) -> 6*
    k0(31,31,6) -> 6*
    k0(17,34,41) -> 6*
    k0(41,40,40) -> 6*
    k0(10,38,19) -> 6*
    k0(29,9,6) -> 6*
    k0(9,40,18) -> 6*
    k0(19,38,38) -> 6*
    k0(39,18,40) -> 6*
    k0(34,29,34) -> 6*
    k0(18,18,9) -> 6*
    k0(35,35,30) -> 6*
    k0(10,31,30) -> 6*
    k0(19,35,19) -> 6*
    k0(38,6,6) -> 6*
    k0(32,15,29) -> 6*
    k0(31,41,6) -> 6*
    k0(41,30,32) -> 6*
    k0(41,19,18) -> 6*
    k0(15,17,17) -> 6*
    k0(30,39,35) -> 6*
    k0(34,34,10) -> 6*
    k0(9,30,10) -> 6*
    k0(34,30,40) -> 6*
    k0(29,41,34) -> 6*
    k0(18,30,29) -> 6*
    k0(38,34,9) -> 6*
    k0(18,19,15) -> 6*
    k0(38,10,31) -> 6*
    k0(6,10,9) -> 6*
    k0(17,6,30) -> 6*
    k0(31,10,39) -> 6*
    k0(6,6,39) -> 6*
    k0(6,41,31) -> 6*
    k0(40,38,6) -> 6*
    k0(10,6,38) -> 6*
    k0(29,38,15) -> 6*
    k0(35,10,38) -> 6*
    k0(38,38,34) -> 6*
    k0(41,9,10) -> 6*
    k0(10,29,17) -> 6*
    k0(30,40,41) -> 6*
    k0(15,38,31) -> 6*
    k0(34,9,18) -> 6*
    k0(38,35,15) -> 6*
    k0(38,39,40) -> 6*
    k0(17,39,9) -> 6*
    k0(32,41,19) -> 6*
    k0(6,39,18) -> 6*
    k0(41,41,38) -> 6*
    k0(35,19,39) -> 6*
    k0(10,15,39) -> 6*
    k0(30,19,19) -> 6*
    k0(15,17,9) -> 6*
    k0(10,39,17) -> 6*
    k0(29,32,32) -> 6*
    k0(39,19,38) -> 6*
    k0(29,6,34) -> 6*
    k0(18,41,35) -> 6*
    k0(32,34,30) -> 6*
    k0(6,32,29) -> 6*
    k0(41,38,19) -> 6*
    k0(40,40,18) -> 6*
    k0(38,29,32) -> 6*
    k0(38,18,18) -> 6*
    k0(17,40,15) -> 6*
    k0(6,29,10) -> 6*
    k0(31,29,40) -> 6*
    k0(41,31,30) -> 6*
    k0(15,29,29) -> 6*
    k0(15,18,15) -> 6*
    k0(10,29,9) -> 6*
    k0(35,9,31) -> 6*
    k0(30,31,39) -> 6*
    k0(39,9,30) -> 6*
    k0(34,31,38) -> 6*
    k0(32,9,38) -> 6*
    k0(40,30,10) -> 6*
    k0(30,17,6) -> 6*
    k0(29,15,35) -> 6*
    k0(32,32,17) -> 6*
    k0(32,6,19) -> 6*
    k0(6,15,32) -> 6*
    k0(31,19,32) -> 6*
    k0(30,10,17) -> 6*
    k0(35,34,15) -> 6*
    k0(10,41,29) -> 6*
    k0(41,6,38) -> 6*
    k0(10,30,15) -> 6*
    k0(35,19,31) -> 6*
    k0(30,41,39) -> 6*
    k0(10,15,31) -> 6*
    k0(9,17,30) -> 6*
    k0(19,30,34) -> 6*
    k0(17,34,32) -> 6*
    k0(41,29,17) -> 6*
    k0(10,38,10) -> 6*
    k0(35,38,40) -> 6*
    k0(10,34,40) -> 6*
    k0(19,38,29) -> 6*
    k0(29,40,19) -> 6*
    k0(39,38,39) -> 6*
    k0(9,10,41) -> 6*
    k0(38,40,38) -> 6*
    k0(32,18,39) -> 6*
    k0(30,31,31) -> 6*
    k0(15,40,35) -> 6*
    k0(19,35,10) -> 6*
    k0(19,31,40) -> 6*
    k0(17,9,40) -> 6*
    k0(41,15,39) -> 6*
    k0(41,39,17) -> 6*
    k0(35,17,18) -> 6*
    k0(34,19,17) -> 6*
    k0(9,15,17) -> 6*
    k0(18,19,6) -> 6*
    k0(38,30,30) -> 6*
    k0(32,32,9) -> 6*
    k0(17,17,35) -> 6*
    k0(31,30,38) -> 6*
    k0(35,10,29) -> 6*
    k0(15,41,41) -> 6*
    k0(10,6,29) -> 6*
    k0(19,10,18) -> 6*
    k0(41,29,9) -> 6*
    k0(30,40,32) -> 6*
    k0(30,29,18) -> 6*
    k0(34,9,9) -> 6*
    k0(29,31,17) -> 6*
    k0(38,35,6) -> 6*
    k0(34,40,31) -> 6*
    k0(32,18,31) -> 6*
    k0(32,41,10) -> 6*
    k0(17,35,30) -> 6*
    k0(41,41,29) -> 6*
    k0(41,30,15) -> 6*
    k0(6,35,39) -> 6*
    k0(30,19,10) -> 6*
    k0(41,15,31) -> 6*
    k0(6,9,41) -> 6*
    k0(10,35,38) -> 6*
    k0(30,15,40) -> 6*
    k0(40,17,30) -> 6*
    k0(35,39,38) -> 6*
    k0(29,17,39) -> 6*
    k0(39,19,29) -> 6*
    k0(34,19,9) -> 6*
    k0(29,41,17) -> 6*
    k0(9,15,9) -> 6*
    k0(41,38,10) -> 6*
    k0(41,34,40) -> 6*
    k0(10,32,19) -> 6*
    k0(15,32,39) -> 6*
    k0(34,38,18) -> 6*
    k0(40,10,41) -> 6*
    k0(9,34,18) -> 6*
    k0(15,6,41) -> 6*
    k0(19,32,38) -> 6*
    k0(9,19,34) -> 6*
    k0(38,38,17) -> 6*
    k0(31,18,17) -> 6*
    k0(17,10,38) -> 6*
    k0(15,18,6) -> 6*
    k0(35,29,30) -> 6*
    k0(19,29,19) -> 6*
    k0(29,31,9) -> 6*
    k0(34,31,29) -> 6*
    k0(18,31,18) -> 6*
    k0(32,9,29) -> 6*
    k0(40,15,17) -> 6*
    k0(10,18,41) -> 6*
    k0(29,35,34) -> 6*
    k0(32,6,10) -> 6*
    k0(6,35,31) -> 6*
    k0(35,34,6) -> 6*
    k0(41,6,29) -> 6*
    k0(10,30,6) -> 6*
    k0(31,39,31) -> 6*
    k0(30,41,30) -> 6*
    k0(29,32,15) -> 6*
    k0(39,30,35) -> 6*
    k0(19,15,41) -> 6*
    k0(29,17,31) -> 6*
    k0(38,32,34) -> 6*
    k0(18,17,40) -> 6*
    k0(17,19,39) -> 6*
    k0(32,10,35) -> 6*
    k0(15,32,31) -> 6*
    k0(29,40,10) -> 6*
    k0(30,34,41) -> 6*
    k0(39,38,30) -> 6*
    k0(9,10,32) -> 6*
    k0(38,40,29) -> 6*
    k0(38,29,15) -> 6*
    k0(32,38,38) -> 6*
    k0(31,18,9) -> 6*
    k0(10,40,6) -> 6*
    k0(9,38,35) -> 6*
    k0(39,31,41) -> 6*
    k0(17,9,31) -> 6*
    k0(32,35,19) -> 6*
    k0(6,18,34) -> 6*
    k0(41,35,38) -> 6*
    k0(10,9,39) -> 6*
    k0(40,15,9) -> 6*
    k0(29,15,18) -> 6*
    k0(18,35,35) -> 6*
    k0(31,19,15) -> 6*
    k0(6,15,15) -> 6*
    k0(31,30,29) -> 6*
    k0(41,32,19) -> 6*
    k0(40,34,18) -> 6*
    k0(15,41,32) -> 6*
    k0(15,30,18) -> 6*
    k0(40,19,34) -> 6*
    k0(30,6,30) -> 6*
    k0(15,15,34) -> 6*
    k0(19,10,9) -> 6*
    k0(19,6,39) -> 6*
    k0(39,10,19) -> 6*
    k0(9,39,41) -> 6*
    k0(19,41,31) -> 6*
    k0(17,34,15) -> 6*
    k0(17,19,31) -> 6*
    k0(6,19,40) -> 6*
    k0(17,38,40) -> 6*
    k0(41,18,41) -> 6*
    k0(35,31,34) -> 6*
    k0(29,9,35) -> 6*
    k0(9,18,19) -> 6*
    k0(18,18,38) -> 6*
    k0(41,30,6) -> 6*
    k0(6,9,32) -> 6*
    k0(35,39,29) -> 6*
    k0(10,35,29) -> 6*
    k0(30,39,9) -> 6*
    k0(19,39,18) -> 6*
    k0(34,15,30) -> 6*
    k0(38,6,35) -> 6*
    k0(18,15,19) -> 6*
    k0(17,17,18) -> 6*
    k0(31,41,35) -> 6*
    k0(10,32,10) -> 6*
    k0(40,10,32) -> 6*
    k0(35,32,40) -> 6*
    k0(15,6,32) -> 6*
    k0(34,34,39) -> 6*
    k0(9,30,39) -> 6*
    k0(19,32,29) -> 6*
    k0(29,34,19) -> 6*
    k0(38,34,38) -> 6*
    k0(17,10,29) -> 6*
    k0(41,40,6) -> 6*
    k0(30,40,15) -> 6*
    k0(40,38,35) -> 6*
    k0(15,34,35) -> 6*
    k0(19,29,10) -> 6*
    k0(39,40,34) -> 6*
    k0(38,31,19) -> 6*
    k0(41,9,39) -> 6*
    k0(6,38,41) -> 6*
    k0(10,18,32) -> 6*
    k0(9,9,17) -> 6*
    k0(9,40,39) -> 6*
    k0(29,32,6) -> 6*
    k0(40,39,41) -> 6*
    k0(15,35,41) -> 6*
    k0(19,15,32) -> 6*
    k0(39,41,40) -> 6*
    k0(18,6,17) -> 6*
    k0(18,41,9) -> 6*
    k0(38,17,41) -> 6*
    k0(32,30,34) -> 6*
    k0(17,39,38) -> 6*
    k0(6,17,19) -> 6*
    k0(30,34,32) -> 6*
    k0(15,17,38) -> 6*
    k0(9,30,31) -> 6*
    k0(38,29,6) -> 6*
    k0(34,34,31) -> 6*
    k0(32,38,29) -> 6*
    k0(6,10,30) -> 6*
    k0(40,18,19) -> 6*
    k0(39,31,32) -> 6*
    k0(32,35,10) -> 6*
    k0(32,31,40) -> 6*
    k0(17,29,30) -> 6*
    k0(41,35,29) -> 6*
    k0(6,29,39) -> 6*
    k0(10,29,38) -> 6*
    k0(30,9,40) -> 6*
    k0(38,39,6) -> 6*
    k0(6,15,6) -> 6*
    k0(41,32,10) -> 6*
    k0(31,19,6) -> 6*
    k0(40,30,39) -> 6*
    k0(30,17,35) -> 6*
    k0(35,30,19) -> 6*
    k0(39,10,10) -> 6*
    k0(34,32,18) -> 6*
    k0(9,39,32) -> 6*
    k0(34,17,34) -> 6*
    k0(39,6,40) -> 6*
    k0(17,34,6) -> 6*
    k0(32,10,18) -> 6*
    k0(6,39,39) -> 6*
    k0(10,19,30) -> 6*
    k0(9,10,15) -> 6*
    k0(18,10,34) -> 6*
    k0(41,18,32) -> 6*
    k0(40,9,17) -> 6*
    k0(15,40,9) -> 6*
    k0(9,18,10) -> 6*
    k0(40,40,39) -> 6*
    k0(34,18,40) -> 6*
    k0(29,29,34) -> 6*
    k0(18,18,29) -> 6*
    k0(6,29,31) -> 6*
    k0(30,35,30) -> 6*
    k0(19,35,39) -> 6*
    k0(39,39,19) -> 6*
    k0(18,15,10) -> 6*
    k0(19,9,41) -> 6*
    k0(38,41,18) -> 6*
    k0(10,17,17) -> 6*
    k0(15,41,15) -> 6*
    k0(29,34,10) -> 6*
    k0(40,30,31) -> 6*
    k0(29,30,40) -> 6*
    k0(39,32,30) -> 6*
    k0(38,34,29) -> 6*
    k0(18,19,35) -> 6*
    k0(32,32,38) -> 6*
    k0(35,38,6) -> 6*
    k0(30,10,38) -> 6*
    k0(9,32,35) -> 6*
    k0(38,31,10) -> 6*
    k0(32,29,19) -> 6*
    k0(31,31,18) -> 6*
    k0(6,38,32) -> 6*
    k0(41,29,38) -> 6*
    k0(10,38,31) -> 6*
    k0(29,9,18) -> 6*
    k0(9,40,30) -> 6*
    k0(18,29,35) -> 6*
    k0(17,31,34) -> 6*
    k0(6,9,15) -> 6*
    k0(40,39,32) -> 6*
    k0(15,35,32) -> 6*
    k0(15,9,34) -> 6*
    k0(39,30,17) -> 6*
    k0(19,35,31) -> 6*
    k0(38,6,18) -> 6*
    k0(38,17,32) -> 6*
    k0(17,39,29) -> 6*
    k0(6,17,10) -> 6*
    k0(32,15,41) -> 6*
    k0(31,17,40) -> 6*
    k0(41,19,30) -> 6*
    k0(40,10,15) -> 6*
    k0(15,17,29) -> 6*
    k0(15,6,15) -> 6*
    k0(10,17,9) -> 6*
    k0(30,19,39) -> 6*
    k0(34,19,38) -> 6*
    k0(9,15,38) -> 6*
    k0(18,30,41) -> 6*
    k0(17,32,40) -> 6*
    k0(35,40,18) -> 6*
    k0(40,18,10) -> 6*
    k0(15,10,40) -> 6*
    k0(39,40,17) -> 6*
    k0(10,18,15) -> 6*
    k0(30,9,31) -> 6*
    k0(15,18,35) -> 6*
    k0(10,29,29) -> 6*
    k0(34,9,30) -> 6*
    k0(29,31,38) -> 6*
    k0(19,18,34) -> 6*
    k0(18,35,17) -> 6*
    k0(18,9,19) -> 6*
    k0(41,17,17) -> 6*
    k0(31,35,35) -> 6*
    k0(6,31,35) -> 6*
    k0(35,30,10) -> 6*
    k0(39,30,9) -> 6*
    k0(19,15,15) -> 6*
    k0(39,6,31) -> 6*
    k0(32,10,9) -> 6*
    k0(32,6,39) -> 6*
    k0(32,41,31) -> 6*
    k0(6,39,30) -> 6*
    k0(30,34,15) -> 6*
    k0(9,10,6) -> 6*
    k0(40,32,35) -> 6*
    k0(30,19,31) -> 6*
    k0(39,34,34) -> 6*
    k0(19,19,40) -> 6*
    k0(41,38,31) -> 6*
    k0(6,32,41) -> 6*
    k0(30,38,40) -> 6*
    k0(40,40,30) -> 6*
    k0(9,38,9) -> 6*
    k0(39,31,15) -> 6*
    k0(34,38,39) -> 6*
    k0(38,18,30) -> 6*
    k0(31,18,38) -> 6*
    k0(10,40,35) -> 6*
    k0(39,39,10) -> 6*
    k0(15,29,41) -> 6*
    k0(19,9,32) -> 6*
    k0(39,35,40) -> 6*
    k0(18,35,9) -> 6*
    k0(32,39,18) -> 6*
    k0(31,15,19) -> 6*
    k0(41,17,9) -> 6*
    k0(30,17,18) -> 6*
    k0(29,19,17) -> 6*
    k0(40,15,38) -> 6*
    k0(9,39,15) -> 6*
    k0(18,39,34) -> 6*
    k0(17,30,19) -> 6*
    k0(32,32,29) -> 6*
    k0(15,34,17) -> 6*
    k0(30,10,29) -> 6*
    k0(10,41,41) -> 6*
    k0(32,29,10) -> 6*
    k0(41,29,29) -> 6*
    k0(41,18,15) -> 6*
    k0(29,9,9) -> 6*
    k0(19,38,41) -> 6*
    k0(29,40,31) -> 6*
    k0(18,40,40) -> 6*
    k0(6,9,6) -> 6*
    k0(38,6,9) -> 6*
    k0(32,15,32) -> 6*
    k0(31,6,17) -> 6*
    k0(31,41,9) -> 6*
    k0(15,6,6) -> 6*
    k0(40,10,6) -> 6*
    k0(35,17,30) -> 6*
    k0(30,39,38) -> 6*
    k0(34,19,29) -> 6*
    k0(9,15,29) -> 6*
    k0(19,17,19) -> 6*
    k0(29,19,9) -> 6*
    k0(18,30,32) -> 6*
    k0(18,19,18) -> 6*
    k0(6,41,34) -> 6*
    k0(15,34,9) -> 6*
    k0(15,10,31) -> 6*
    k0(10,32,39) -> 6*
    k0(40,38,9) -> 6*
    k0(29,38,18) -> 6*
    k0(35,10,41) -> 6*
    k0(10,6,41) -> 6*
    k0(19,10,30) -> 6*
    k0(17,38,6) -> 6*
    k0(6,38,15) -> 6*
    k0(10,18,6) -> 6*
    k0(41,40,35) -> 6*
    k0(30,29,30) -> 6*
    k0(15,38,34) -> 6*
    k0(19,29,39) -> 6*
    k0(29,31,29) -> 6*
    k0(38,35,18) -> 6*
    k0(18,9,10) -> 6*
    k0(35,15,17) -> 6*
    k0(40,39,15) -> 6*
    k0(15,35,15) -> 6*
    k0(19,15,6) -> 6*
    k0(38,17,15) -> 6*
    k0(30,34,6) -> 6*
    k0(41,41,41) -> 6*
    k0(15,39,40) -> 6*
    k0(9,41,19) -> 6*
    k0(39,19,41) -> 6*
    k0(34,30,35) -> 6*
    k0(19,39,39) -> 6*
    k0(18,41,38) -> 6*
    k0(6,32,32) -> 6*
    k0(31,10,34) -> 6*
    k0(6,6,34) -> 6*
    k0(10,32,31) -> 6*
    k0(39,31,6) -> 6*
    k0(34,38,30) -> 6*
    k0(9,34,30) -> 6*
    k0(18,38,19) -> 6*
    k0(17,40,18) -> 6*
    k0(31,18,29) -> 6*
    k0(15,29,32) -> 6*
    k0(15,18,18) -> 6*
    k0(19,29,31) -> 6*
    k0(34,31,41) -> 6*
    k0(18,31,30) -> 6*
    k0(32,35,39) -> 6*
    k0(31,15,10) -> 6*
    k0(32,9,41) -> 6*
    k0(40,15,29) -> 6*
    k0(35,15,9) -> 6*
    k0(39,41,6) -> 6*
    k0(9,9,38) -> 6*
    k0(17,30,10) -> 6*
    k0(38,39,35) -> 6*
    k0(41,32,39) -> 6*
    k0(31,19,35) -> 6*
    k0(6,15,35) -> 6*
    k0(35,34,18) -> 6*
    k0(10,41,32) -> 6*
    k0(41,6,41) -> 6*
    k0(10,30,18) -> 6*
    k0(10,15,34) -> 6*
    k0(9,32,17) -> 6*
    k0(35,19,34) -> 6*
    k0(39,10,39) -> 6*
    k0(34,10,19) -> 6*
    k0(9,6,19) -> 6*
    k0(18,6,38) -> 6*
    k0(41,18,6) -> 6*
    k0(19,38,32) -> 6*
    k0(18,29,17) -> 6*
    k0(38,40,41) -> 6*
    k0(6,40,19) -> 6*
    k0(31,29,35) -> 6*
    k0(30,31,34) -> 6*
    k0(15,40,38) -> 6*
    k0(9,18,39) -> 6*
    k0(19,9,15) -> 6*
    k0(32,35,31) -> 6*
    k0(30,39,29) -> 6*
    k0(40,41,19) -> 6*
    k0(19,17,10) -> 6*
    k0(29,15,30) -> 6*
    k0(18,15,39) -> 6*
    k0(38,19,19) -> 6*
    k0(18,39,17) -> 6*
    k0(31,30,41) -> 6*
    k0(41,32,31) -> 6*
    k0(35,10,32) -> 6*
    k0(30,32,40) -> 6*
    k0(40,34,30) -> 6*
    k0(10,6,32) -> 6*
    k0(15,30,30) -> 6*
    k0(9,32,9) -> 6*
    k0(29,34,39) -> 6*
    k0(10,34,35) -> 6*
    k0(35,38,35) -> 6*
    k0(39,29,40) -> 6*
    k0(34,40,34) -> 6*
    k0(18,29,9) -> 6*
    k0(38,31,39) -> 6*
    k0(32,18,34) -> 6*
    k0(31,35,17) -> 6*
    k0(6,31,17) -> 6*
    k0(15,35,6) -> 6*
    k0(31,9,19) -> 6*
    k0(40,9,38) -> 6*
    k0(19,31,35) -> 6*
    k0(9,18,31) -> 6*
    k0(38,17,6) -> 6*
    k0(32,15,15) -> 6*
    k0(41,41,32) -> 6*
    k0(41,30,18) -> 6*
    k0(41,15,34) -> 6*
    k0(40,32,17) -> 6*
    k0(9,41,10) -> 6*
    k0(35,39,41) -> 6*
    k0(40,6,19) -> 6*
    k0(10,35,41) -> 6*
    k0(19,39,30) -> 6*
    k0(39,19,32) -> 6*
    k0(34,41,40) -> 6*
    k0(38,10,17) -> 6*
    k0(18,41,29) -> 6*
    k0(18,30,15) -> 6*
    k0(38,41,39) -> 6*
    k0(18,15,31) -> 6*
    k0(32,19,40) -> 6*
    k0(17,17,30) -> 6*
    k0(6,17,39) -> 6*
    k0(6,41,17) -> 6*
    k0(10,17,38) -> 6*
    k0(18,38,10) -> 6*
    k0(19,32,41) -> 6*
    k0(29,34,31) -> 6*
    k0(18,34,40) -> 6*
    k0(17,10,41) -> 6*
    k0(35,18,19) -> 6*
    k0(15,38,17) -> 6*
    k0(40,18,39) -> 6*
    k0(34,31,32) -> 6*
    k0(38,31,31) -> 6*
    k0(32,9,32) -> 6*
    k0(6,31,9) -> 6*
    k0(31,35,9) -> 6*
    k0(9,9,29) -> 6*
    k0(17,15,17) -> 6*
    k0(41,6,32) -> 6*
    k0(31,39,34) -> 6*
    k0(6,35,34) -> 6*
    k0(35,30,39) -> 6*
    k0(30,30,19) -> 6*
    k0(40,32,9) -> 6*
    k0(34,10,10) -> 6*
    k0(29,32,18) -> 6*
    k0(9,6,10) -> 6*
    k0(29,17,34) -> 6*
    k0(34,6,40) -> 6*
    k0(39,30,38) -> 6*
    k0(18,6,29) -> 6*
    k0(6,32,15) -> 6*
    k0(41,34,35) -> 6*
    k0(6,17,31) -> 6*
    k0(15,32,34) -> 6*
    k0(9,10,35) -> 6*
    k0(38,40,32) -> 6*
    k0(38,29,18) -> 6*
    k0(6,40,10) -> 6*
    k0(32,38,41) -> 6*
    k0(31,40,40) -> 6*
    k0(35,9,17) -> 6*
    k0(15,40,29) -> 6*
    k0(15,29,15) -> 6*
    k0(10,40,9) -> 6*
    k0(40,18,31) -> 6*
    k0(35,40,39) -> 6*
    k0(19,9,6) -> 6*
    k0(29,18,40) -> 6*
    k0(9,38,38) -> 6*
    k0(40,41,10) -> 6*
    k0(41,35,41) -> 6*
    k0(34,39,19) -> 6*
    k0(9,35,19) -> 6*
    k0(38,19,10) -> 6*
    k0(38,15,40) -> 6*
    k0(18,35,38) -> 6*
    k0(32,17,19) -> 6*
    k0(17,15,9) -> 6*
    k0(31,30,32) -> 6*
    k0(31,19,18) -> 6*
    k0(6,15,18) -> 6*
    k0(41,17,38) -> 6*
    k0(10,41,15) -> 6*
    k0(35,30,31) -> 6*
    k0(34,32,30) -> 6*
    k0(19,41,34) -> 6*
    k0(18,32,19) -> 6*
    k0(17,34,18) -> 6*
    k0(17,19,34) -> 6*
    k0(32,10,30) -> 6*
    k0(30,38,6) -> 6*
    k0(19,38,15) -> 6*
    k0(39,18,17) -> 6*
    k0(32,29,39) -> 6*
    k0(31,9,10) -> 6*
    k0(40,9,29) -> 6*
    k0(18,18,41) -> 6*
    k0(32,15,6) -> 6*
    k0(6,9,35) -> 6*
    k0(35,39,32) -> 6*
    k0(40,6,10) -> 6*
    k0(10,35,32) -> 6*
    k0(10,9,34) -> 6*
    k0(34,30,17) -> 6*
    k0(18,30,6) -> 6*
    k0(39,39,31) -> 6*
    k0(38,41,30) -> 6*
    k0(32,39,39) -> 6*
    k0(31,41,38) -> 6*
    k0(15,6,35) -> 6*
    k0(35,10,15) -> 6*
    k0(10,17,29) -> 6*
    k0(10,6,15) -> 6*
    k0(40,10,35) -> 6*
    k0(19,32,32) -> 6*
    k0(29,19,38) -> 6*
    k0(19,6,34) -> 6*
    k0(38,34,41) -> 6*
    k0(17,10,32) -> 6*
    k0(31,38,19) -> 6*
    k0(41,40,9) -> 6*
    k0(6,34,19) -> 6*
    k0(35,18,10) -> 6*
    k0(30,40,18) -> 6*
    k0(40,38,38) -> 6*
    k0(10,10,40) -> 6*
    k0(15,34,38) -> 6*
    k0(39,18,9) -> 6*
    k0(34,40,17) -> 6*
    k0(18,40,6) -> 6*
    k0(17,38,35) -> 6*
    k0(32,29,31) -> 6*
    k0(31,31,30) -> 6*
    k0(40,35,19) -> 6*
    k0(10,18,35) -> 6*
    k0(15,31,19) -> 6*
    k0(29,9,30) -> 6*
    k0(18,9,39) -> 6*
    k0(41,41,15) -> 6*
    k0(30,30,10) -> 6*
    k0(34,6,31) -> 6*
    k0(39,30,29) -> 6*
    k0(19,15,35) -> 6*
    k0(39,19,15) -> 6*
    k0(34,30,9) -> 6*
    k0(38,6,30) -> 6*
    k0(6,32,6) -> 6*
    k0(17,39,41) -> 6*
    k0(31,6,38) -> 6*
    k0(35,32,35) -> 6*
    k0(15,17,41) -> 6*
    k0(34,34,34) -> 6*
    k0(9,30,34) -> 6*
    k0(32,38,32) -> 6*
    k0(31,29,17) -> 6*
    k0(15,29,6) -> 6*
    k0(35,40,30) -> 6*
    k0(34,31,15) -> 6*
    k0(9,38,29) -> 6*
    k0(19,40,19) -> 6*
    k0(29,38,39) -> 6*
    k0(32,9,15) -> 6*
    k0(17,18,19) -> 6*
    k0(41,35,32) -> 6*
    k0(41,9,34) -> 6*
    k0(34,39,10) -> 6*
    k0(9,35,10) -> 6*
    k0(10,29,41) -> 6*
    k0(9,31,40) -> 6*
    k0(34,35,40) -> 6*
    k0(18,35,29) -> 6*
    k0(38,39,9) -> 6*
    k0(32,17,10) -> 6*
    k0(41,6,15) -> 6*
    k0(31,39,17) -> 6*
    k0(31,15,39) -> 6*
    k0(41,17,29) -> 6*
    k0(15,39,6) -> 6*
    k0(35,15,38) -> 6*
    k0(18,32,10) -> 6*
    k0(39,41,35) -> 6*
    k0(17,30,39) -> 6*
    k0(41,10,40) -> 6*
    k0(10,34,17) -> 6*
    k0(9,10,18) -> 6*
    k0(38,40,15) -> 6*
    k0(41,18,35) -> 6*
    k0(31,29,9) -> 6*
    k0(19,31,17) -> 6*
    k0(18,18,32) -> 6*
    k0(17,9,17) -> 6*
    k0(32,31,35) -> 6*
    k0(17,40,39) -> 6*
    k0(6,29,34) -> 6*
    k0(32,39,30) -> 6*
    k0(31,41,29) -> 6*
    k0(31,30,15) -> 6*
    k0(10,6,6) -> 6*
    k0(31,15,31) -> 6*
    k0(35,10,6) -> 6*
    k0(15,41,18) -> 6*
    k0(40,30,34) -> 6*
    k0(30,17,30) -> 6*
    k0(19,41,17) -> 6*
    k0(19,17,39) -> 6*
    k0(29,19,29) -> 6*
    k0(38,34,32) -> 6*
    k0(31,38,10) -> 6*
    k0(6,34,10) -> 6*
    k0(32,32,41) -> 6*
    k0(17,30,31) -> 6*
    k0(6,30,40) -> 6*
    k0(31,34,40) -> 6*
    k0(40,38,29) -> 6*
    k0(10,10,31) -> 6*
    k0(15,34,29) -> 6*
    k0(35,38,9) -> 6*
    k0(10,34,9) -> 6*
    k0(30,10,41) -> 6*
    k0(9,32,38) -> 6*
    k0(40,35,10) -> 6*
    k0(15,31,10) -> 6*
    k0(41,29,41) -> 6*
    k0(10,38,34) -> 6*
    k0(40,31,40) -> 6*
    k0(19,31,9) -> 6*
    k0(9,29,19) -> 6*
    k0(18,29,38) -> 6*
    k0(38,9,40) -> 6*
    k0(6,9,18) -> 6*
    k0(30,15,17) -> 6*
    k0(35,39,15) -> 6*
    k0(10,35,15) -> 6*
    k0(39,19,6) -> 6*
    k0(19,35,34) -> 6*
    k0(38,17,35) -> 6*
    k0(17,39,32) -> 6*
    k0(41,34,17) -> 6*
    k0(31,6,29) -> 6*
    k0(15,6,18) -> 6*
    k0(40,10,18) -> 6*
    k0(15,17,32) -> 6*
    k0(10,39,40) -> 6*
    k0(19,32,15) -> 6*
    k0(29,30,35) -> 6*
    k0(9,15,41) -> 6*
    k0(19,17,31) -> 6*
    k0(34,19,41) -> 6*
    k0(18,19,30) -> 6*
    k0(17,10,15) -> 6*
    k0(34,31,6) -> 6*
    k0(19,40,10) -> 6*
    k0(29,38,30) -> 6*
    k0(32,9,6) -> 6*
    k0(17,18,10) -> 6*
    k0(10,29,32) -> 6*
    k0(10,18,18) -> 6*
    k0(29,31,41) -> 6*
    k0(38,35,30) -> 6*
    k0(41,6,6) -> 6*
    k0(6,31,38) -> 6*
    k0(31,35,38) -> 6*
    k0(35,15,29) -> 6*
    k0(30,15,9) -> 6*
    k0(19,15,18) -> 6*
    k0(34,41,6) -> 6*
    k0(18,17,17) -> 6*
    k0(32,41,34) -> 6*
    k0(41,10,31) -> 6*
    k0(31,32,19) -> 6*
    k0(41,34,9) -> 6*
    k0(30,34,18) -> 6*
    k0(9,10,9) -> 6*
    k0(40,32,38) -> 6*
    k0(30,19,34) -> 6*
    k0(34,10,39) -> 6*
    k0(9,6,39) -> 6*
    k0(29,10,19) -> 6*
    k0(9,41,31) -> 6*
    k0(32,38,15) -> 6*
    k0(38,10,38) -> 6*
    k0(17,32,35) -> 6*
    k0(41,38,34) -> 6*
    k0(40,29,19) -> 6*
    k0(39,31,18) -> 6*
    k0(18,38,31) -> 6*
    k0(17,40,30) -> 6*
    k0(41,35,15) -> 6*
    k0(31,18,41) -> 6*
    k0(15,18,30) -> 6*
    k0(10,40,38) -> 6*
    k0(19,9,35) -> 6*
    k0(31,30,6) -> 6*
    k0(41,39,40) -> 6*
    k0(35,41,19) -> 6*
    k0(40,15,41) -> 6*
    k0(9,39,18) -> 6*
    k0(39,17,40) -> 6*
    k0(18,17,9) -> 6*
    k0(38,19,39) -> 6*
    k0(32,32,32) -> 6*
    k0(6,19,17) -> 6*
    k0(32,6,34) -> 6*
    k0(17,15,38) -> 6*
    k0(35,34,30) -> 6*
    k0(10,30,30) -> 6*
    k0(30,10,32) -> 6*
    k0(9,32,29) -> 6*
    k0(19,34,19) -> 6*
    k0(41,29,32) -> 6*
    k0(41,18,18) -> 6*
    k0(31,40,6) -> 6*
    k0(9,29,10) -> 6*
    k0(30,38,35) -> 6*
    k0(34,29,40) -> 6*
    k0(29,40,34) -> 6*
    k0(38,9,31) -> 6*
    k0(18,29,29) -> 6*
    k0(18,18,15) -> 6*
    k0(6,9,9) -> 6*
    k0(31,9,39) -> 6*
    k0(10,35,6) -> 6*
    k0(6,40,31) -> 6*
    k0(35,9,38) -> 6*
    k0(39,35,35) -> 6*
    k0(32,15,35) -> 6*
    k0(40,10,9) -> 6*
    k0(35,32,17) -> 6*
    k0(15,6,9) -> 6*
    k0(40,6,39) -> 6*
    k0(19,32,6) -> 6*
    k0(30,39,41) -> 6*
    k0(40,41,31) -> 6*
    k0(35,6,19) -> 6*
    k0(34,19,32) -> 6*
    k0(29,41,40) -> 6*
    k0(9,15,32) -> 6*
    k0(38,34,15) -> 6*
    k0(38,19,31) -> 6*
    k0(17,10,6) -> 6*
    k0(6,19,9) -> 6*
    k0(38,38,40) -> 6*
    k0(32,40,19) -> 6*
    k0(17,38,9) -> 6*
    k0(6,38,18) -> 6*
    k0(41,40,38) -> 6*
    k0(30,18,19) -> 6*
    k0(10,38,17) -> 6*
    k0(35,18,39) -> 6*
    k0(29,31,32) -> 6*
    k0(39,18,38) -> 6*
    k0(18,40,35) -> 6*
    k0(31,35,29) -> 6*
    k0(6,31,29) -> 6*
    k0(15,35,18) -> 6*
    k0(40,39,18) -> 6*
    k0(39,15,19) -> 6*
    k0(38,17,18) -> 6*
    k0(17,39,15) -> 6*
    k0(31,32,10) -> 6*
    k0(41,30,30) -> 6*
    k0(30,30,39) -> 6*
    k0(40,32,29) -> 6*
    k0(35,32,9) -> 6*
    k0(15,17,15) -> 6*
    k0(29,10,10) -> 6*
    k0(29,6,40) -> 6*
    k0(34,30,38) -> 6*
    k0(38,10,29) -> 6*
    k0(18,41,41) -> 6*
    k0(40,29,10) -> 6*
    k0(10,32,34) -> 6*
    k0(32,31,17) -> 6*
    k0(41,35,6) -> 6*
    k0(31,18,32) -> 6*
    k0(30,9,17) -> 6*
    k0(10,40,29) -> 6*
    k0(10,29,15) -> 6*
    k0(35,18,31) -> 6*
    k0(30,40,39) -> 6*
    k0(19,29,34) -> 6*
    k0(35,41,10) -> 6*
    k0(40,15,32) -> 6*
    k0(39,6,17) -> 6*
    k0(9,35,39) -> 6*
    k0(29,39,19) -> 6*
    k0(39,41,9) -> 6*
    k0(9,9,41) -> 6*
    k0(38,39,38) -> 6*
    k0(17,15,29) -> 6*
    k0(32,41,17) -> 6*
    k0(32,17,39) -> 6*
    k0(19,34,10) -> 6*
    k0(30,30,31) -> 6*
    k0(15,39,35) -> 6*
    k0(19,30,40) -> 6*
    k0(29,32,30) -> 6*
    k0(18,32,39) -> 6*
    k0(18,6,41) -> 6*
    k0(41,38,17) -> 6*
    k0(34,18,17) -> 6*
    k0(18,18,6) -> 6*
    k0(38,29,30) -> 6*
    k0(32,31,9) -> 6*
    k0(31,29,38) -> 6*
    k0(35,9,29) -> 6*
    k0(15,40,41) -> 6*
    k0(19,9,18) -> 6*
    k0(32,35,34) -> 6*
    k0(30,39,32) -> 6*
    k0(35,6,10) -> 6*
    k0(29,30,17) -> 6*
    k0(34,39,31) -> 6*
    k0(9,35,31) -> 6*
    k0(38,34,6) -> 6*
    k0(32,32,15) -> 6*
    k0(17,41,19) -> 6*
    k0(32,17,31) -> 6*
    k0(41,32,34) -> 6*
    k0(31,19,30) -> 6*
    k0(6,15,30) -> 6*
    k0(15,19,19) -> 6*
    k0(35,10,35) -> 6*
    k0(10,6,35) -> 6*
    k0(30,10,15) -> 6*
    k0(39,10,34) -> 6*
    k0(32,40,10) -> 6*
    k0(18,32,31) -> 6*
    k0(17,34,30) -> 6*
    k0(41,40,29) -> 6*
    k0(41,29,15) -> 6*
    k0(6,34,39) -> 6*
    k0(30,18,10) -> 6*
    k0(35,38,38) -> 6*
    k0(10,34,38) -> 6*
    k0(34,18,9) -> 6*
    k0(29,40,17) -> 6*
    k0(39,18,29) -> 6*
    k0(40,35,39) -> 6*
    k0(15,31,39) -> 6*
    k0(35,35,19) -> 6*
    k0(10,31,19) -> 6*
    k0(40,9,41) -> 6*
    k0(39,15,10) -> 6*
    k0(9,18,34) -> 6*
    k0(19,31,38) -> 6*
    k0(32,15,18) -> 6*
    k0(17,9,38) -> 6*
    k0(31,17,17) -> 6*
    k0(15,17,6) -> 6*
    k0(39,19,35) -> 6*
    k0(29,6,31) -> 6*
    k0(34,30,29) -> 6*
    k0(34,19,15) -> 6*
    k0(29,30,9) -> 6*
    k0(9,15,15) -> 6*
    k0(18,41,32) -> 6*
    k0(18,30,18) -> 6*
    k0(18,15,34) -> 6*
    k0(17,32,17) -> 6*
    k0(17,6,19) -> 6*
    k0(15,10,17) -> 6*
    k0(30,32,35) -> 6*
    k0(10,17,41) -> 6*
    k0(15,41,39) -> 6*
    k0(29,34,34) -> 6*
    k0(9,19,40) -> 6*
    k0(10,29,6) -> 6*
    k0(31,38,31) -> 6*
    k0(6,34,31) -> 6*
    k0(30,40,30) -> 6*
    k0(29,31,15) -> 6*
    k0(39,29,35) -> 6*
    k0(38,31,34) -> 6*
    k0(32,9,35) -> 6*
    k0(17,18,39) -> 6*
    k0(29,39,10) -> 6*
    k0(40,35,31) -> 6*
    k0(15,31,31) -> 6*
    k0(9,9,32) -> 6*
    k0(29,35,40) -> 6*
    k0(38,39,29) -> 6*
    k0(31,17,9) -> 6*
    k0(41,6,35) -> 6*
    k0(10,39,6) -> 6*
    k0(30,15,38) -> 6*
    k0(19,19,17) -> 6*
    k0(39,30,41) -> 6*
    k0(34,41,35) -> 6*
    k0(18,6,32) -> 6*
    k0(38,32,40) -> 6*
    k0(32,34,19) -> 6*
    k0(17,32,9) -> 6*
    k0(6,32,18) -> 6*
    k0(6,17,34) -> 6*
    k0(41,34,38) -> 6*
    k0(18,34,35) -> 6*
    k0(31,29,29) -> 6*
    k0(41,31,19) -> 6*
    k0(31,18,15) -> 6*
    k0(15,40,32) -> 6*
    k0(15,29,18) -> 6*
    k0(39,35,17) -> 6*
    k0(19,9,9) -> 6*
    k0(40,18,34) -> 6*
    k0(39,9,19) -> 6*
    k0(9,38,41) -> 6*
    k0(19,40,31) -> 6*
    k0(17,18,31) -> 6*
    k0(6,18,40) -> 6*
    k0(40,15,15) -> 6*
    k0(17,41,10) -> 6*
    k0(18,35,41) -> 6*
    k0(32,32,6) -> 6*
    k0(30,10,6) -> 6*
    k0(15,19,10) -> 6*
    k0(41,17,41) -> 6*
    k0(10,41,18) -> 6*
    k0(40,19,40) -> 6*
    k0(35,30,34) -> 6*
    k0(15,15,40) -> 6*
    k0(9,17,19) -> 6*
    k0(19,19,9) -> 6*
    k0(18,17,38) -> 6*
    k0(41,29,6) -> 6*
    k0(35,38,29) -> 6*
    k0(10,34,29) -> 6*
    k0(30,38,9) -> 6*
    k0(19,38,18) -> 6*
    k0(9,10,30) -> 6*
    k0(35,35,10) -> 6*
    k0(10,31,10) -> 6*
    k0(31,40,35) -> 6*
    k0(40,9,32) -> 6*
    k0(35,31,40) -> 6*
    k0(9,29,39) -> 6*
    k0(19,31,29) -> 6*
    k0(39,35,9) -> 6*
    k0(17,9,29) -> 6*
    k0(41,39,6) -> 6*
    k0(30,39,15) -> 6*
    k0(34,19,6) -> 6*
    k0(9,15,6) -> 6*
    k0(39,39,34) -> 6*
    k0(38,30,19) -> 6*
    k0(17,6,10) -> 6*
    k0(31,41,41) -> 6*
    k0(35,10,18) -> 6*
    k0(10,17,32) -> 6*
    k0(15,41,30) -> 6*
    k0(10,6,18) -> 6*
    k0(9,39,39) -> 6*
    k0(29,19,41) -> 6*
    k0(17,10,35) -> 6*
    k0(6,19,38) -> 6*
    k0(40,38,41) -> 6*
    k0(15,34,41) -> 6*
    k0(29,31,6) -> 6*
    k0(39,40,40) -> 6*
    k0(18,40,9) -> 6*
    k0(32,29,34) -> 6*
    k0(17,38,38) -> 6*
    k0(9,29,31) -> 6*
    k0(17,35,19) -> 6*
    k0(41,41,18) -> 6*
    k0(6,9,30) -> 6*
    k0(30,15,29) -> 6*
    k0(40,17,19) -> 6*
    k0(39,30,32) -> 6*
    k0(39,19,18) -> 6*
    k0(29,41,6) -> 6*
    k0(18,41,15) -> 6*
    k0(32,34,10) -> 6*
    k0(32,30,40) -> 6*
    k0(31,32,39) -> 6*
    k0(41,34,29) -> 6*
    k0(31,6,41) -> 6*
    k0(40,10,30) -> 6*
    k0(35,32,38) -> 6*
    k0(15,6,30) -> 6*
    k0(29,10,39) -> 6*
    k0(38,38,6) -> 6*
    k0(41,31,10) -> 6*
    k0(31,18,6) -> 6*
    k0(40,29,39) -> 6*
    k0(35,29,19) -> 6*
    k0(9,38,32) -> 6*
    k0(39,9,10) -> 6*
    k0(34,31,18) -> 6*
    k0(32,9,18) -> 6*
    k0(6,38,39) -> 6*
    k0(40,15,6) -> 6*
    k0(10,18,30) -> 6*
    k0(9,9,15) -> 6*
    k0(18,35,32) -> 6*
    k0(18,9,34) -> 6*
    k0(41,17,32) -> 6*
    k0(41,6,18) -> 6*
    k0(30,41,19) -> 6*
    k0(15,39,9) -> 6*
    k0(9,17,10) -> 6*
    k0(35,15,41) -> 6*
    k0(40,39,39) -> 6*
    k0(34,17,40) -> 6*
    k0(39,41,38) -> 6*
    k0(19,15,30) -> 6*
    k0(18,6,15) -> 6*
    k0(18,17,29) -> 6*
    k0(31,32,31) -> 6*
    k0(30,34,30) -> 6*
    k0(19,34,39) -> 6*
    k0(39,38,19) -> 6*
    k0(38,40,18) -> 6*
    k0(18,10,40) -> 6*
    k0(15,40,15) -> 6*
    k0(40,29,31) -> 6*
    k0(29,29,40) -> 6*
    k0(39,31,30) -> 6*
    k0(18,18,35) -> 6*
    k0(32,31,38) -> 6*
    k0(30,9,38) -> 6*
    k0(9,31,35) -> 6*
    k0(38,30,10) -> 6*
    k0(34,35,35) -> 6*
    k0(31,30,18) -> 6*
    k0(31,41,32) -> 6*
    k0(35,10,9) -> 6*
    k0(30,32,17) -> 6*
    k0(10,6,9) -> 6*
    k0(31,15,34) -> 6*
    k0(35,6,39) -> 6*
    k0(35,41,31) -> 6*
    k0(30,6,19) -> 6*
    k0(29,19,32) -> 6*
    k0(9,39,30) -> 6*
    k0(39,6,38) -> 6*
    k0(17,30,34) -> 6*
    k0(6,19,29) -> 6*
    k0(15,34,32) -> 6*
    k0(40,38,32) -> 6*
    k0(39,29,17) -> 6*
    k0(9,32,41) -> 6*
    k0(19,34,31) -> 6*
    k0(17,38,29) -> 6*
    k0(41,18,30) -> 6*
    k0(30,18,39) -> 6*
    k0(40,9,15) -> 6*
    k0(34,18,38) -> 6*
    k0(17,35,10) -> 6*
    k0(18,29,41) -> 6*
    k0(17,31,40) -> 6*
    k0(10,35,18) -> 6*
    k0(40,17,10) -> 6*
    k0(35,39,18) -> 6*
    k0(15,9,40) -> 6*
    k0(34,15,19) -> 6*
    k0(39,39,17) -> 6*
    k0(39,15,39) -> 6*
    k0(32,19,17) -> 6*
    k0(31,6,32) -> 6*
    k0(35,32,29) -> 6*
    k0(15,17,35) -> 6*
    k0(30,32,9) -> 6*
    k0(10,17,15) -> 6*
    k0(19,32,18) -> 6*
    k0(18,34,17) -> 6*
    k0(29,30,38) -> 6*
    k0(19,17,34) -> 6*
    k0(17,10,18) -> 6*
    k0(6,30,35) -> 6*
    k0(35,29,10) -> 6*
    k0(31,34,35) -> 6*
    k0(39,29,9) -> 6*
    k0(32,9,9) -> 6*
    k0(32,40,31) -> 6*
    k0(6,38,30) -> 6*
    k0(30,18,31) -> 6*
    k0(9,9,6) -> 6*
    k0(40,31,35) -> 6*
    k0(19,18,40) -> 6*
    k0(41,6,9) -> 6*
    k0(31,35,41) -> 6*
    k0(6,31,41) -> 6*
    k0(30,41,10) -> 6*
    k0(35,15,32) -> 6*
    k0(40,39,30) -> 6*
    k0(15,35,30) -> 6*
    k0(39,41,29) -> 6*
    k0(34,6,17) -> 6*
    k0(39,30,15) -> 6*
    k0(34,41,9) -> 6*
    k0(39,15,31) -> 6*
    k0(18,6,6) -> 6*
    k0(38,17,30) -> 6*
    k0(32,19,9) -> 6*
    k0(31,17,38) -> 6*
    k0(40,32,41) -> 6*
    k0(10,39,35) -> 6*
    k0(39,38,10) -> 6*
    k0(9,41,34) -> 6*
    k0(39,34,40) -> 6*
    k0(18,10,31) -> 6*
    k0(18,34,9) -> 6*
    k0(38,10,41) -> 6*
    k0(32,38,18) -> 6*
    k0(17,32,38) -> 6*
    k0(6,10,19) -> 6*
    k0(9,38,15) -> 6*
    k0(15,10,38) -> 6*
    k0(29,18,17) -> 6*
    k0(18,38,34) -> 6*
    k0(32,31,29) -> 6*
    k0(17,29,19) -> 6*
    k0(41,35,18) -> 6*
    k0(30,9,29) -> 6*
    k0(10,40,41) -> 6*
    k0(18,35,15) -> 6*
    k0(38,15,17) -> 6*
    k0(41,17,15) -> 6*
    k0(30,6,10) -> 6*
    k0(39,6,29) -> 6*
    k0(29,39,31) -> 6*
    k0(18,39,40) -> 6*
    k0(17,15,41) -> 6*
    k0(10,19,19) -> 6*
    k0(30,10,35) -> 6*
    k0(15,19,39) -> 6*
    k0(9,32,32) -> 6*
    k0(19,19,38) -> 6*
    k0(9,6,34) -> 6*
    k0(34,10,34) -> 6*
    k0(31,40,9) -> 6*
    k0(40,9,6) -> 6*
    k0(30,38,38) -> 6*
    k0(29,18,9) -> 6*
    k0(34,18,29) -> 6*
    k0(18,29,32) -> 6*
    k0(18,18,18) -> 6*
    k0(6,40,34) -> 6*
    k0(35,35,39) -> 6*
    k0(15,9,31) -> 6*
    k0(10,31,39) -> 6*
    k0(30,35,19) -> 6*
    k0(35,9,41) -> 6*
    k0(34,15,10) -> 6*
    k0(39,35,38) -> 6*
    k0(19,9,30) -> 6*
    k0(38,15,9) -> 6*
    k0(31,41,15) -> 6*
    k0(10,17,6) -> 6*
    k0(41,39,35) -> 6*
    k0(40,41,34) -> 6*
    k0(34,19,35) -> 6*
    k0(29,30,29) -> 6*
    k0(39,32,19) -> 6*
    k0(9,15,35) -> 6*
    k0(29,19,15) -> 6*
    k0(38,34,18) -> 6*
    k0(17,10,9) -> 6*
    k0(38,19,34) -> 6*
    k0(17,6,39) -> 6*
    k0(17,41,31) -> 6*
    k0(6,41,40) -> 6*
    k0(10,10,17) -> 6*
    k0(15,34,15) -> 6*
    k0(40,38,15) -> 6*
    k0(15,19,31) -> 6*
    k0(10,41,39) -> 6*
    k0(41,40,41) -> 6*
    k0(15,38,40) -> 6*
    k0(9,40,19) -> 6*
    k0(19,38,39) -> 6*
    k0(39,18,41) -> 6*
    k0(34,29,35) -> 6*
    k0(18,40,38) -> 6*
    k0(6,31,32) -> 6*
    k0(31,35,32) -> 6*
    k0(31,9,34) -> 6*
    k0(35,35,31) -> 6*
    k0(10,31,31) -> 6*
    k0(39,30,6) -> 6*
    k0(17,39,18) -> 6*
    k0(32,15,30) -> 6*
    k0(31,17,29) -> 6*
    k0(41,19,19) -> 6*
    k0(31,6,15) -> 6*
    k0(15,17,18) -> 6*
    k0(40,32,32) -> 6*
    k0(40,6,34) -> 6*
    k0(34,30,41) -> 6*
    k0(29,41,35) -> 6*
    k0(18,30,30) -> 6*
    k0(38,10,32) -> 6*
    k0(32,34,39) -> 6*
    k0(17,32,29) -> 6*
    k0(6,10,10) -> 6*
    k0(31,10,40) -> 6*
    k0(6,6,40) -> 6*
    k0(15,10,29) -> 6*
    k0(39,40,6) -> 6*
    k0(17,29,10) -> 6*
    k0(38,38,35) -> 6*
    k0(41,31,39) -> 6*
    k0(31,18,35) -> 6*
    k0(10,29,18) -> 6*
    k0(10,40,32) -> 6*
    k0(34,35,17) -> 6*
    k0(9,31,17) -> 6*
    k0(35,18,34) -> 6*
    k0(34,9,19) -> 6*
    k0(39,9,39) -> 6*
    k0(18,35,6) -> 6*
    k0(41,17,6) -> 6*
    k0(40,15,35) -> 6*
    k0(35,15,15) -> 6*
    k0(38,39,41) -> 6*
    k0(17,15,32) -> 6*
    k0(6,39,19) -> 6*
    k0(41,10,17) -> 6*
    k0(10,19,10) -> 6*
    k0(41,41,39) -> 6*
    k0(35,19,40) -> 6*
    k0(30,30,34) -> 6*
    k0(10,15,40) -> 6*
    k0(15,39,38) -> 6*
    k0(9,41,17) -> 6*
    k0(9,17,39) -> 6*
    k0(19,19,29) -> 6*
    k0(32,34,31) -> 6*
    k0(6,32,30) -> 6*
    k0(30,38,29) -> 6*
    k0(40,40,19) -> 6*
    k0(18,38,17) -> 6*
    k0(38,18,19) -> 6*
    k0(30,35,10) -> 6*
    k0(31,29,41) -> 6*
    k0(41,31,31) -> 6*
    k0(15,29,30) -> 6*
    k0(35,9,32) -> 6*
    k0(30,31,40) -> 6*
    k0(39,35,29) -> 6*
    k0(34,35,9) -> 6*
    k0(9,31,9) -> 6*
    k0(39,32,10) -> 6*
    k0(29,19,6) -> 6*
    k0(9,35,34) -> 6*
    k0(34,39,34) -> 6*
    k0(38,30,39) -> 6*
    k0(32,32,18) -> 6*
    k0(31,34,17) -> 6*
    k0(6,30,17) -> 6*
    k0(32,17,34) -> 6*
    k0(15,34,6) -> 6*
    k0(30,10,18) -> 6*
    k0(10,41,30) -> 6*
    k0(9,32,15) -> 6*
    k0(9,17,31) -> 6*
    k0(19,30,35) -> 6*
    k0(18,32,34) -> 6*
    k0(41,40,32) -> 6*
    k0(41,29,18) -> 6*
    k0(40,31,17) -> 6*
    k0(9,40,10) -> 6*
    k0(35,38,41) -> 6*
    k0(10,34,41) -> 6*
    k0(39,18,32) -> 6*
    k0(34,40,40) -> 6*
    k0(19,38,30) -> 6*
    k0(18,40,29) -> 6*
    k0(18,29,15) -> 6*
    k0(38,9,17) -> 6*
    k0(38,40,39) -> 6*
    k0(32,18,40) -> 6*
    k0(6,40,17) -> 6*
    k0(19,31,41) -> 6*
    k0(17,35,39) -> 6*
    k0(17,9,41) -> 6*
    k0(41,19,10) -> 6*
    k0(31,6,6) -> 6*
    k0(41,15,40) -> 6*
    k0(40,17,39) -> 6*
    k0(35,17,19) -> 6*
    k0(40,41,17) -> 6*
    k0(34,30,32) -> 6*
    k0(34,19,18) -> 6*
    k0(9,15,18) -> 6*
    k0(38,30,31) -> 6*
    k0(31,10,31) -> 6*
    k0(6,6,31) -> 6*
    k0(31,34,9) -> 6*
    k0(6,30,9) -> 6*
    k0(35,10,30) -> 6*
    k0(30,32,38) -> 6*
    k0(10,6,30) -> 6*
    k0(19,10,19) -> 6*
    k0(31,38,34) -> 6*
    k0(6,34,34) -> 6*
    k0(35,29,39) -> 6*
    k0(30,29,19) -> 6*
    k0(40,31,9) -> 6*
    k0(34,9,10) -> 6*
    k0(29,31,18) -> 6*
    k0(39,29,38) -> 6*
    k0(31,35,15) -> 6*
    k0(6,31,15) -> 6*
    k0(35,15,6) -> 6*
    k0(40,35,34) -> 6*
    k0(15,31,34) -> 6*
    k0(9,9,35) -> 6*
    k0(38,39,32) -> 6*
    k0(6,39,10) -> 6*
    k0(17,35,31) -> 6*
    k0(31,39,40) -> 6*
    k0(41,41,30) -> 6*
    k0(6,35,40) -> 6*
    k0(40,32,15) -> 6*
    k0(15,39,29) -> 6*
    k0(10,39,9) -> 6*
    k0(30,15,41) -> 6*
    k0(40,17,31) -> 6*
    k0(35,39,39) -> 6*
    k0(29,17,40) -> 6*
    k0(39,19,30) -> 6*
    k0(34,41,38) -> 6*
    k0(18,6,35) -> 6*
    k0(38,10,15) -> 6*
    k0(32,19,38) -> 6*
    k0(41,34,41) -> 6*
    k0(40,40,10) -> 6*
    k0(15,32,40) -> 6*
    k0(34,38,19) -> 6*
    k0(9,34,19) -> 6*
    k0(38,18,10) -> 6*
    k0(18,34,38) -> 6*
    k0(31,29,32) -> 6*
    k0(31,18,18) -> 6*
    k0(10,40,15) -> 6*
    k0(35,29,31) -> 6*
    k0(19,40,34) -> 6*
    k0(34,31,30) -> 6*
    k0(18,31,19) -> 6*
    k0(32,9,30) -> 6*
    k0(17,18,34) -> 6*
    k0(40,15,18) -> 6*
    k0(39,17,17) -> 6*
    k0(29,35,35) -> 6*
    k0(17,15,15) -> 6*
    k0(30,10,9) -> 6*
    k0(41,6,30) -> 6*
    k0(30,41,31) -> 6*
    k0(30,6,39) -> 6*
    k0(9,32,6) -> 6*
    k0(19,41,40) -> 6*
    k0(34,6,38) -> 6*
    k0(38,32,35) -> 6*
    k0(18,17,41) -> 6*
    k0(17,19,40) -> 6*
    k0(10,34,32) -> 6*
    k0(35,38,32) -> 6*
    k0(34,29,17) -> 6*
    k0(39,38,31) -> 6*
    k0(18,29,6) -> 6*
    k0(38,40,30) -> 6*
    k0(32,38,39) -> 6*
    k0(31,40,38) -> 6*
    k0(40,9,35) -> 6*
    k0(35,9,15) -> 6*
    k0(19,31,32) -> 6*
    k0(29,18,38) -> 6*
    k0(17,9,32) -> 6*
    k0(41,39,9) -> 6*
    k0(35,17,10) -> 6*
    k0(30,39,18) -> 6*
    k0(10,9,40) -> 6*
    k0(34,39,17) -> 6*
    k0(34,15,39) -> 6*
    k0(29,15,19) -> 6*
    k0(39,17,9) -> 6*
    k0(18,39,6) -> 6*
    k0(38,15,38) -> 6*
    k0(31,30,30) -> 6*
    k0(30,32,29) -> 6*
    k0(40,34,19) -> 6*
    k0(10,17,35) -> 6*
    k0(15,30,19) -> 6*
    k0(19,10,10) -> 6*
    k0(19,6,40) -> 6*
    k0(41,40,15) -> 6*
    k0(30,29,10) -> 6*
    k0(6,19,41) -> 6*
    k0(39,29,29) -> 6*
    k0(39,18,15) -> 6*
    k0(34,29,9) -> 6*
    k0(6,31,6) -> 6*
    k0(17,38,41) -> 6*
    k0(31,35,6) -> 6*
    k0(35,31,35) -> 6*
    k0(9,29,34) -> 6*
    k0(40,32,6) -> 6*
    k0(30,15,32) -> 6*
    k0(35,39,30) -> 6*
    k0(10,35,30) -> 6*
    k0(29,6,17) -> 6*
    k0(34,30,15) -> 6*
    k0(19,39,19) -> 6*
    k0(29,41,9) -> 6*
    k0(34,41,29) -> 6*
    k0(38,10,6) -> 6*
    k0(18,41,18) -> 6*
    k0(34,15,31) -> 6*
    k0(32,19,29) -> 6*
    k0(17,17,19) -> 6*
    k0(6,41,6) -> 6*
    k0(41,34,32) -> 6*
    k0(9,34,10) -> 6*
    k0(35,32,41) -> 6*
    k0(34,38,10) -> 6*
    k0(34,34,40) -> 6*
    k0(9,30,40) -> 6*
    k0(19,32,30) -> 6*
    k0(18,34,29) -> 6*
    k0(38,38,9) -> 6*
    k0(17,10,30) -> 6*
    k0(31,38,17) -> 6*
    k0(6,10,39) -> 6*
    k0(15,38,6) -> 6*
    k0(10,10,38) -> 6*
    k0(18,31,10) -> 6*
    k0(39,40,35) -> 6*
    k0(17,29,39) -> 6*
    k0(41,9,40) -> 6*
    k0(9,9,18) -> 6*
    k0(38,39,15) -> 6*
    k0(17,15,6) -> 6*
    k0(41,17,35) -> 6*
    k0(19,30,17) -> 6*
    k0(34,6,29) -> 6*
    k0(39,41,41) -> 6*
    k0(18,17,32) -> 6*
    k0(18,6,18) -> 6*
    k0(17,39,39) -> 6*
    k0(32,30,35) -> 6*
    k0(31,32,34) -> 6*
    k0(10,19,39) -> 6*
    k0(29,10,34) -> 6*
    k0(32,38,30) -> 6*
    k0(31,29,15) -> 6*
    k0(31,40,29) -> 6*
    k0(35,9,6) -> 6*
    k0(15,40,18) -> 6*
    k0(40,29,34) -> 6*
    k0(19,40,17) -> 6*
    k0(29,18,29) -> 6*
    k0(32,31,41) -> 6*
    k0(17,29,31) -> 6*
    k0(41,35,30) -> 6*
    k0(6,29,40) -> 6*
    k0(10,9,31) -> 6*
    k0(30,35,39) -> 6*
    k0(29,15,10) -> 6*
    k0(30,9,41) -> 6*
    k0(34,35,38) -> 6*
    k0(9,31,38) -> 6*
    k0(38,15,29) -> 6*
    k0(15,30,10) -> 6*
    k0(40,34,10) -> 6*
    k0(40,30,40) -> 6*
    k0(35,41,34) -> 6*
    k0(29,19,35) -> 6*
    k0(19,6,31) -> 6*
    k0(34,32,19) -> 6*
    k0(19,30,9) -> 6*
    k0(39,32,39) -> 6*
    k0(39,6,41) -> 6*
    k0(32,10,19) -> 6*
    k0(6,19,32) -> 6*
    k0(41,10,38) -> 6*
    k0(10,34,15) -> 6*
    k0(35,38,15) -> 6*
    k0(39,18,6) -> 6*
    k0(10,19,31) -> 6*
    k0(19,34,34) -> 6*
    k0(17,38,32) -> 6*
    k0(40,9,18) -> 6*
    k0(10,38,40) -> 6*
    k0(19,31,15) -> 6*
    k0(34,18,41) -> 6*
    k0(29,29,35) -> 6*
    k0(18,18,30) -> 6*
    k0(17,9,15) -> 6*
    k0(30,35,31) -> 6*
    k0(34,30,6) -> 6*
    k0(19,39,10) -> 6*
    k0(19,35,40) -> 6*
    k0(38,41,19) -> 6*
    k0(17,17,10) -> 6*
    k0(41,19,39) -> 6*
    k0(31,6,35) -> 6*
    k0(10,17,18) -> 6*
    k0(35,32,32) -> 6*
    k0(9,19,17) -> 6*
    k0(35,6,34) -> 6*
    k0(29,30,41) -> 6*
    k0(39,32,31) -> 6*
    k0(38,34,30) -> 6*
    k0(31,34,38) -> 6*
    k0(6,30,38) -> 6*
    k0(10,10,29) -> 6*
    k0(34,40,6) -> 6*
    k0(32,40,34) -> 6*
    k0(31,31,19) -> 6*
    k0(41,9,31) -> 6*
    k0(29,35,17) -> 6*
    k0(9,9,9) -> 6*
    k0(40,31,38) -> 6*
    k0(30,18,34) -> 6*
    k0(29,9,19) -> 6*
    k0(9,40,31) -> 6*
    k0(34,9,39) -> 6*
    k0(38,9,38) -> 6*
    k0(17,31,35) -> 6*
    k0(35,15,35) -> 6*
    k0(30,15,15) -> 6*
    k0(39,41,32) -> 6*
    k0(39,30,18) -> 6*
    k0(38,32,17) -> 6*
    k0(18,6,9) -> 6*
    k0(39,15,34) -> 6*
    k0(38,6,19) -> 6*
    k0(32,41,40) -> 6*
    k0(17,39,30) -> 6*
    k0(41,34,15) -> 6*
    k0(31,17,41) -> 6*
    k0(41,19,31) -> 6*
    k0(30,19,40) -> 6*
    k0(15,17,30) -> 6*
    k0(10,39,38) -> 6*
    k0(9,19,9) -> 6*
    k0(17,32,41) -> 6*
    k0(31,29,6) -> 6*
    k0(41,38,40) -> 6*
    k0(35,40,19) -> 6*
    k0(15,10,41) -> 6*
    k0(9,38,18) -> 6*
    k0(38,18,39) -> 6*
    k0(32,31,32) -> 6*
    k0(6,18,17) -> 6*
    k0(10,29,30) -> 6*
    k0(30,9,32) -> 6*
    k0(34,35,29) -> 6*
    k0(9,31,29) -> 6*
    k0(29,35,9) -> 6*
    k0(18,35,18) -> 6*
    k0(41,17,18) -> 6*
    k0(31,39,6) -> 6*
    k0(40,19,17) -> 6*
    k0(15,15,17) -> 6*
    k0(34,32,10) -> 6*
    k0(39,6,32) -> 6*
    k0(29,39,34) -> 6*
    k0(38,32,9) -> 6*
    k0(18,17,15) -> 6*
    k0(32,10,10) -> 6*
    k0(32,6,40) -> 6*
    k0(6,39,31) -> 6*
    k0(41,10,29) -> 6*
    k0(10,34,6) -> 6*
    k0(39,34,35) -> 6*
    k0(19,19,41) -> 6*
    k0(40,9,9) -> 6*
    k0(35,31,17) -> 6*
    k0(30,38,41) -> 6*
    k0(40,40,31) -> 6*
    k0(19,31,6) -> 6*
    k0(34,18,32) -> 6*
    k0(29,40,40) -> 6*
    k0(17,9,6) -> 6*
    k0(38,18,31) -> 6*
    k0(6,18,9) -> 6*
    k0(39,35,41) -> 6*
    k0(38,41,10) -> 6*
    k0(32,39,19) -> 6*
    k0(31,41,18) -> 6*
    k0(41,39,38) -> 6*
    k0(15,15,9) -> 6*
    k0(35,17,39) -> 6*
    k0(30,17,19) -> 6*
    k0(40,19,9) -> 6*
    k0(35,41,17) -> 6*
    k0(29,19,18) -> 6*
    k0(19,41,6) -> 6*
    k0(29,30,32) -> 6*
    k0(39,17,38) -> 6*
    k0(18,39,35) -> 6*
    k0(32,32,30) -> 6*
    k0(17,41,34) -> 6*
    k0(31,34,29) -> 6*
    k0(6,30,29) -> 6*
    k0(6,19,15) -> 6*
    k0(40,38,18) -> 6*
    k0(15,34,18) -> 6*
    k0(30,10,30) -> 6*
    k0(15,19,34) -> 6*
    k0(19,10,39) -> 6*
    k0(17,38,15) -> 6*
    k0(31,31,10) -> 6*
    k0(41,29,30) -> 6*
    k0(30,29,39) -> 6*
    k0(40,31,29) -> 6*
    k0(35,31,9) -> 6*
    k0(29,9,10) -> 6*
    k0(34,29,38) -> 6*
    k0(18,40,41) -> 6*
    k0(38,9,29) -> 6*
    k0(30,15,6) -> 6*
    k0(10,31,34) -> 6*
    k0(35,35,34) -> 6*
    k0(38,6,10) -> 6*
    k0(32,30,17) -> 6*
    k0(41,34,6) -> 6*
    k0(31,17,32) -> 6*
    k0(31,6,18) -> 6*
    k0(10,39,29) -> 6*
    k0(35,32,15) -> 6*
    k0(35,17,31) -> 6*
    k0(30,39,39) -> 6*
    k0(34,19,30) -> 6*
    k0(29,41,38) -> 6*
    k0(9,15,30) -> 6*
    k0(38,10,35) -> 6*
    k0(18,19,19) -> 6*
    k0(17,32,32) -> 6*
    k0(17,6,34) -> 6*
    k0(6,41,35) -> 6*
    k0(35,40,10) -> 6*
    k0(15,10,32) -> 6*
    k0(10,32,40) -> 6*
    k0(9,34,39) -> 6*
    k0(29,38,19) -> 6*
    k0(39,40,9) -> 6*
    k0(38,38,38) -> 6*
    k0(32,40,17) -> 6*
    k0(30,29,31) -> 6*
    k0(15,38,35) -> 6*
    k0(19,29,40) -> 6*
    k0(29,31,30) -> 6*
    k0(18,31,39) -> 6*
    k0(38,35,19) -> 6*
    k0(35,15,18) -> 6*
    k0(34,17,17) -> 6*
    k0(39,41,15) -> 6*
    k0(18,17,6) -> 6*
    k0(32,6,31) -> 6*
    k0(17,15,35) -> 6*
    k0(32,30,9) -> 6*
    k0(15,39,41) -> 6*
    k0(19,19,32) -> 6*
    k0(29,6,38) -> 6*
    k0(18,10,17) -> 6*
    k0(18,41,39) -> 6*
    k0(32,34,34) -> 6*
    k0(30,38,32) -> 6*
    k0(29,29,17) -> 6*
    k0(34,38,31) -> 6*
    k0(9,34,31) -> 6*
    k0(17,40,19) -> 6*
    k0(32,31,15) -> 6*
    k0(41,31,34) -> 6*
    k0(31,18,30) -> 6*
    k0(35,9,35) -> 6*
    k0(30,9,15) -> 6*
    k0(15,18,19) -> 6*
    k0(39,35,32) -> 6*
    k0(39,9,34) -> 6*
    k0(18,31,31) -> 6*
    k0(32,39,10) -> 6*
    k0(32,35,40) -> 6*
    k0(41,39,29) -> 6*
    k0(30,17,10) -> 6*
    k0(40,15,30) -> 6*
    k0(29,15,39) -> 6*
    k0(39,17,29) -> 6*
    k0(39,6,15) -> 6*
    k0(34,17,9) -> 6*
    k0(29,39,17) -> 6*
    k0(6,19,6) -> 6*
    k0(41,32,40) -> 6*
    k0(15,30,39) -> 6*
    k0(35,34,19) -> 6*
    k0(10,30,19) -> 6*
    k0(40,34,39) -> 6*
    k0(9,32,18) -> 6*
    k0(39,10,40) -> 6*
    k0(19,30,38) -> 6*
    k0(9,17,34) -> 6*
    k0(34,29,29) -> 6*
    k0(34,18,15) -> 6*
    k0(29,29,9) -> 6*
    k0(39,18,35) -> 6*
    k0(18,40,32) -> 6*
    k0(18,29,18) -> 6*
    k0(17,31,17) -> 6*
    k0(15,9,17) -> 6*
    k0(30,31,35) -> 6*
    k0(15,40,39) -> 6*
    k0(9,18,40) -> 6*
    k0(31,6,9) -> 6*
    k0(35,32,6) -> 6*
    k0(30,39,30) -> 6*
    k0(29,30,15) -> 6*
    k0(29,41,29) -> 6*
    k0(18,19,10) -> 6*
    k0(29,15,31) -> 6*
    k0(38,30,34) -> 6*
    k0(18,15,40) -> 6*
    k0(17,17,39) -> 6*
    k0(17,41,17) -> 6*
    k0(30,32,41) -> 6*
    k0(40,34,31) -> 6*
    k0(15,30,31) -> 6*
    k0(29,38,10) -> 6*
    k0(29,34,40) -> 6*
    k0(38,38,29) -> 6*
    k0(10,38,6) -> 6*
    k0(19,18,17) -> 6*
    k0(39,29,41) -> 6*
    k0(34,40,35) -> 6*
    k0(38,35,10) -> 6*
    k0(38,31,40) -> 6*
    k0(17,31,9) -> 6*
    k0(31,35,18) -> 6*
    k0(6,31,18) -> 6*
    k0(17,35,34) -> 6*
    k0(41,30,19) -> 6*
    k0(31,17,15) -> 6*
    k0(40,32,18) -> 6*
    k0(15,39,32) -> 6*
    k0(40,17,34) -> 6*
    k0(39,34,17) -> 6*
    k0(19,39,31) -> 6*
    k0(34,41,41) -> 6*
    k0(29,6,29) -> 6*
    k0(38,10,18) -> 6*
    k0(18,41,30) -> 6*
    k0(17,32,15) -> 6*
    k0(32,19,41) -> 6*
    k0(17,17,31) -> 6*
    k0(6,17,40) -> 6*
    k0(15,10,15) -> 6*
    k0(9,19,38) -> 6*
    k0(18,34,41) -> 6*
    k0(32,31,6) -> 6*
    k0(17,40,10) -> 6*
    k0(30,9,6) -> 6*
    k0(15,18,10) -> 6*
    k0(10,40,18) -> 6*
    k0(35,29,34) -> 6*
    k0(40,18,40) -> 6*
    k0(19,18,9) -> 6*
    k0(39,6,6) -> 6*
    k0(29,35,38) -> 6*
    k0(9,9,30) -> 6*
    k0(17,15,18) -> 6*
    k0(32,41,6) -> 6*
    k0(10,30,10) -> 6*
    k0(31,39,35) -> 6*
    k0(6,35,35) -> 6*
    k0(35,34,10) -> 6*
    k0(35,30,40) -> 6*
    k0(30,41,34) -> 6*
    k0(19,30,29) -> 6*
    k0(29,32,19) -> 6*
    k0(39,34,9) -> 6*
    k0(19,19,15) -> 6*
    k0(39,10,31) -> 6*
    k0(34,32,39) -> 6*
    k0(34,6,41) -> 6*
    k0(38,32,38) -> 6*
    k0(18,6,30) -> 6*
    k0(32,10,39) -> 6*
    k0(41,38,6) -> 6*
    k0(30,38,15) -> 6*
    k0(34,18,6) -> 6*
    k0(15,32,35) -> 6*
    k0(39,38,34) -> 6*
    k0(38,29,19) -> 6*
    k0(31,40,41) -> 6*
    k0(35,9,18) -> 6*
    k0(15,40,30) -> 6*
    k0(39,35,15) -> 6*
    k0(29,18,41) -> 6*
    k0(9,38,39) -> 6*
    k0(17,9,35) -> 6*
    k0(6,18,38) -> 6*
    k0(29,30,6) -> 6*
    k0(39,39,40) -> 6*
    k0(18,39,9) -> 6*
    k0(38,15,41) -> 6*
    k0(31,19,19) -> 6*
    k0(6,15,19) -> 6*
    k0(30,32,32) -> 6*
    k0(15,15,38) -> 6*
    k0(40,19,38) -> 6*
    k0(30,6,34) -> 6*
    k0(34,32,31) -> 6*
    k0(19,41,35) -> 6*
    k0(17,34,19) -> 6*
    k0(41,40,18) -> 6*
    k0(39,18,18) -> 6*
    k0(29,40,6) -> 6*
    k0(39,29,32) -> 6*
    k0(18,40,15) -> 6*
    k0(32,29,40) -> 6*
    k0(31,31,39) -> 6*
    k0(40,9,30) -> 6*
    k0(35,31,38) -> 6*
    k0(29,9,39) -> 6*
    k0(31,17,6) -> 6*
    k0(41,30,10) -> 6*
    k0(30,15,35) -> 6*
    k0(34,41,32) -> 6*
    k0(34,30,18) -> 6*
    k0(34,15,34) -> 6*
    k0(38,10,9) -> 6*
    k0(38,6,39) -> 6*
    k0(17,32,6) -> 6*
    k0(38,41,31) -> 6*
    k0(32,19,32) -> 6*
    k0(6,6,17) -> 6*
    k0(6,41,9) -> 6*
    k0(31,10,17) -> 6*
    k0(15,10,6) -> 6*
    k0(31,41,39) -> 6*
    k0(10,17,30) -> 6*
    k0(9,19,29) -> 6*
    k0(18,34,32) -> 6*
    k0(15,38,9) -> 6*
    k0(30,40,19) -> 6*
    k0(40,38,39) -> 6*
    k0(10,10,41) -> 6*
    k0(39,40,38) -> 6*
    k0(31,31,31) -> 6*
    k0(29,35,29) -> 6*
    k0(38,39,18) -> 6*
    k0(18,9,40) -> 6*
    k0(35,19,17) -> 6*
    k0(10,15,17) -> 6*
    k0(15,39,15) -> 6*
    k0(19,19,6) -> 6*
    k0(29,32,10) -> 6*
    k0(34,6,32) -> 6*
    k0(39,30,30) -> 6*
    k0(18,17,35) -> 6*
    k0(38,32,29) -> 6*
    k0(32,30,38) -> 6*
    k0(34,34,35) -> 6*
    k0(9,30,35) -> 6*
    k0(38,29,10) -> 6*
    k0(31,40,32) -> 6*
    k0(31,29,18) -> 6*
    k0(35,9,9) -> 6*
    k0(30,31,17) -> 6*
    k0(6,10,34) -> 6*
    k0(39,35,6) -> 6*
    k0(35,40,31) -> 6*
    k0(29,18,32) -> 6*
    k0(9,38,30) -> 6*
    k0(17,29,34) -> 6*
    k0(6,18,29) -> 6*
    k0(9,31,41) -> 6*
    k0(34,35,41) -> 6*
    k0(38,15,32) -> 6*
    k0(18,35,30) -> 6*
    k0(31,19,10) -> 6*
    k0(6,15,10) -> 6*
    k0(31,15,40) -> 6*
    k0(41,17,30) -> 6*
    k0(10,15,9) -> 6*
    k0(30,17,39) -> 6*
    k0(40,19,29) -> 6*
    k0(15,15,29) -> 6*
    k0(35,19,9) -> 6*
    k0(30,41,17) -> 6*
    k0(34,17,38) -> 6*
    k0(17,34,10) -> 6*
    k0(17,30,40) -> 6*
    k0(6,19,35) -> 6*
    k0(35,38,18) -> 6*
    k0(41,10,41) -> 6*
    k0(10,34,18) -> 6*
    k0(10,19,34) -> 6*
    k0(9,10,19) -> 6*
    k0(39,38,17) -> 6*
    k0(18,10,38) -> 6*
    k0(32,18,17) -> 6*
    k0(35,31,29) -> 6*
    k0(30,31,9) -> 6*
    k0(19,31,18) -> 6*
    k0(29,29,38) -> 6*
    k0(17,9,18) -> 6*
    k0(41,15,17) -> 6*
    k0(6,29,35) -> 6*
    k0(30,35,34) -> 6*
    k0(32,39,31) -> 6*
    k0(31,41,30) -> 6*
    k0(15,41,19) -> 6*
    k0(30,32,15) -> 6*
    k0(40,30,35) -> 6*
    k0(30,17,31) -> 6*
    k0(19,17,40) -> 6*
    k0(29,19,30) -> 6*
    k0(39,32,34) -> 6*
    k0(18,19,39) -> 6*
    k0(6,30,41) -> 6*
    k0(30,40,10) -> 6*
    k0(31,34,41) -> 6*
    k0(40,38,30) -> 6*
    k0(10,10,32) -> 6*
    k0(15,34,30) -> 6*
    k0(34,40,9) -> 6*
    k0(39,40,29) -> 6*
    k0(39,29,15) -> 6*
    k0(32,18,9) -> 6*
    k0(40,31,41) -> 6*
    k0(10,38,35) -> 6*
    k0(9,40,34) -> 6*
    k0(38,35,39) -> 6*
    k0(18,9,31) -> 6*
    k0(38,9,41) -> 6*
    k0(6,35,17) -> 6*
    k0(17,31,38) -> 6*
    k0(6,9,19) -> 6*
    k0(41,15,9) -> 6*
    k0(30,15,18) -> 6*
    k0(15,9,38) -> 6*
    k0(29,17,17) -> 6*
    k0(34,41,15) -> 6*
    k0(19,35,35) -> 6*
    k0(32,30,29) -> 6*
    k0(32,19,15) -> 6*
    k0(41,34,18) -> 6*
    k0(15,32,17) -> 6*
    k0(41,19,34) -> 6*
    k0(31,6,30) -> 6*
    k0(15,6,19) -> 6*
    k0(40,10,19) -> 6*
    k0(10,39,41) -> 6*
    k0(9,41,40) -> 6*
    k0(18,34,15) -> 6*
    k0(18,19,31) -> 6*
    k0(29,38,31) -> 6*
    k0(18,38,40) -> 6*
    k0(30,9,35) -> 6*
    k0(15,18,39) -> 6*
    k0(10,18,19) -> 6*
    k0(34,35,32) -> 6*
    k0(9,31,32) -> 6*
    k0(34,9,34) -> 6*
    k0(19,18,38) -> 6*
    k0(38,35,31) -> 6*
    k0(31,39,9) -> 6*
    k0(6,35,9) -> 6*
    k0(35,15,30) -> 6*
    k0(39,6,35) -> 6*
    k0(34,17,29) -> 6*
    k0(34,6,15) -> 6*
    k0(19,15,19) -> 6*
    k0(29,17,9) -> 6*
    k0(18,17,18) -> 6*
    k0(17,19,17) -> 6*
    k0(32,41,35) -> 6*
    k0(41,10,32) -> 6*
    k0(6,39,34) -> 6*
    k0(10,30,39) -> 6*
    k0(30,34,19) -> 6*
    k0(15,32,9) -> 6*
    k0(35,34,39) -> 6*
    k0(9,10,10) -> 6*
    k0(34,10,40) -> 6*
    k0(39,34,38) -> 6*
    k0(9,6,40) -> 6*
    k0(18,10,29) -> 6*
    k0(31,40,15) -> 6*
    k0(41,38,35) -> 6*
    k0(40,40,34) -> 6*
    k0(29,29,29) -> 6*
    k0(39,31,19) -> 6*
    k0(29,18,15) -> 6*
    k0(34,18,35) -> 6*
    k0(17,9,9) -> 6*
    k0(38,18,34) -> 6*
    k0(17,40,31) -> 6*
    k0(6,40,40) -> 6*
    k0(10,9,17) -> 6*
    k0(15,18,31) -> 6*
    k0(10,40,39) -> 6*
    k0(38,15,15) -> 6*
    k0(30,32,6) -> 6*
    k0(15,41,10) -> 6*
    k0(41,39,41) -> 6*
    k0(40,41,40) -> 6*
    k0(9,39,19) -> 6*
    k0(19,41,9) -> 6*
    k0(19,6,17) -> 6*
    k0(39,17,41) -> 6*
    k0(18,39,38) -> 6*
    k0(38,19,40) -> 6*
    k0(17,19,9) -> 6*
    k0(6,19,18) -> 6*
    k0(31,34,32) -> 6*
    k0(6,30,32) -> 6*
    k0(35,34,31) -> 6*
    k0(10,30,31) -> 6*
    k0(39,29,6) -> 6*
    k0(9,32,30) -> 6*
    k0(17,38,18) -> 6*
    k0(41,18,19) -> 6*
    k0(40,31,32) -> 6*
    k0(34,29,41) -> 6*
    k0(29,40,35) -> 6*
    k0(38,9,32) -> 6*
    k0(18,29,30) -> 6*
    k0(17,31,29) -> 6*
    k0(6,9,10) -> 6*
    k0(31,9,40) -> 6*
    k0(15,9,29) -> 6*
    k0(39,39,6) -> 6*
    k0(32,19,6) -> 6*
    k0(41,30,39) -> 6*
    k0(31,17,35) -> 6*
    k0(40,10,10) -> 6*
    k0(35,32,18) -> 6*
    k0(10,39,32) -> 6*
    k0(15,6,10) -> 6*
    k0(40,6,40) -> 6*
    k0(9,30,17) -> 6*
    k0(35,17,34) -> 6*
    k0(34,34,17) -> 6*
    k0(18,34,6) -> 6*
    k0(29,41,41) -> 6*
    k0(6,41,38) -> 6*
    k0(15,10,35) -> 6*
    k0(10,10,15) -> 6*
    k0(19,10,34) -> 6*
    k0(38,38,41) -> 6*
    k0(6,38,19) -> 6*
    k0(41,9,17) -> 6*
    k0(10,18,10) -> 6*
    k0(41,40,39) -> 6*
    k0(30,29,34) -> 6*
    k0(15,38,38) -> 6*
    k0(35,18,40) -> 6*
    k0(19,18,29) -> 6*
    k0(9,40,17) -> 6*
    k0(31,35,30) -> 6*
    k0(6,31,30) -> 6*
    k0(15,35,19) -> 6*
    k0(40,39,19) -> 6*
    k0(39,41,18) -> 6*
    k0(34,6,6) -> 6*
    k0(19,15,10) -> 6*
    k0(38,17,19) -> 6*
    k0(41,30,31) -> 6*
    k0(30,34,10) -> 6*
    k0(30,30,40) -> 6*
    k0(40,32,30) -> 6*
    k0(9,6,31) -> 6*
    k0(34,34,9) -> 6*
    k0(9,30,9) -> 6*
    k0(34,10,31) -> 6*
    k0(29,32,39) -> 6*
    k0(39,34,29) -> 6*
    k0(19,19,35) -> 6*
    k0(29,6,41) -> 6*
    k0(38,10,30) -> 6*
    k0(6,6,38) -> 6*
    k0(31,10,38) -> 6*
    k0(10,32,35) -> 6*
    k0(39,31,10) -> 6*
    k0(29,18,6) -> 6*
    k0(9,34,34) -> 6*
    k0(34,38,34) -> 6*
    k0(38,29,39) -> 6*
    k0(32,31,18) -> 6*
    k0(6,29,17) -> 6*
    k0(30,9,18) -> 6*
    k0(10,40,30) -> 6*
    k0(34,35,15) -> 6*
    k0(9,31,15) -> 6*
    k0(19,29,35) -> 6*
    k0(38,15,6) -> 6*
    k0(18,31,34) -> 6*
    k0(41,39,32) -> 6*
    k0(40,30,17) -> 6*
    k0(9,39,10) -> 6*
    k0(39,17,32) -> 6*
    k0(34,39,40) -> 6*
    k0(39,6,18) -> 6*
    k0(9,35,40) -> 6*
    k0(18,39,29) -> 6*
    k0(38,39,39) -> 6*
    k0(17,15,30) -> 6*
    k0(32,17,40) -> 6*
    k0(31,19,39) -> 6*
    k0(41,10,15) -> 6*
    k0(6,15,39) -> 6*
    k0(6,39,17) -> 6*
    k0(35,19,38) -> 6*
    k0(10,15,38) -> 6*
    k0(19,30,41) -> 6*
    k0(29,32,31) -> 6*
    k0(18,32,40) -> 6*
    k0(17,34,39) -> 6*
    k0(41,18,10) -> 6*
    k0(40,40,17) -> 6*
    k0(34,29,32) -> 6*
    k0(34,18,18) -> 6*
    k0(38,29,31) -> 6*
    k0(6,29,9) -> 6*
    k0(31,9,31) -> 6*
    k0(35,9,30) -> 6*
    k0(30,31,38) -> 6*
    k0(19,35,17) -> 6*
    k0(19,9,19) -> 6*
    k0(32,35,35) -> 6*
    k0(40,30,9) -> 6*
    k0(40,6,31) -> 6*
    k0(29,41,32) -> 6*
    k0(29,30,18) -> 6*
    k0(29,15,34) -> 6*
    k0(6,30,15) -> 6*
    k0(31,34,15) -> 6*
    k0(6,41,29) -> 6*
    k0(10,10,6) -> 6*
    k0(41,32,35) -> 6*
    k0(31,19,31) -> 6*
    k0(6,15,31) -> 6*
    k0(15,30,34) -> 6*
    k0(40,34,34) -> 6*
    k0(38,38,32) -> 6*
    k0(17,34,31) -> 6*
    k0(6,38,10) -> 6*
    k0(31,38,40) -> 6*
    k0(41,40,30) -> 6*
    k0(6,34,40) -> 6*
    k0(10,38,9) -> 6*
    k0(40,31,15) -> 6*
    k0(15,38,29) -> 6*
    k0(35,38,39) -> 6*
    k0(39,18,30) -> 6*
    k0(34,40,38) -> 6*
    k0(38,9,15) -> 6*
    k0(32,18,38) -> 6*
    k0(40,39,10) -> 6*
    k0(15,35,10) -> 6*
    k0(40,35,40) -> 6*
    k0(15,31,40) -> 6*
    k0(19,35,9) -> 6*
    k0(38,17,10) -> 6*
    k0(32,15,19) -> 6*
    k0(31,17,18) -> 6*
    k0(30,19,17) -> 6*
    k0(41,15,38) -> 6*
    k0(10,39,15) -> 6*
    k0(29,6,32) -> 6*
    k0(34,30,30) -> 6*
    k0(19,39,34) -> 6*
    k0(18,30,19) -> 6*
    k0(17,32,18) -> 6*
    k0(17,17,34) -> 6*
    k0(31,10,29) -> 6*
    k0(6,6,29) -> 6*
    k0(15,10,18) -> 6*
    k0(29,34,35) -> 6*
    k0(9,19,41) -> 6*
    k0(30,9,9) -> 6*
    k0(34,35,6) -> 6*
    k0(9,31,6) -> 6*
    k0(30,40,31) -> 6*
    k0(19,40,40) -> 6*
    k0(38,31,35) -> 6*
    k0(17,18,40) -> 6*
    k0(39,6,9) -> 6*
    k0(29,35,41) -> 6*
    k0(38,39,30) -> 6*
    k0(32,6,17) -> 6*
    k0(32,41,9) -> 6*
    k0(41,10,6) -> 6*
    k0(6,35,38) -> 6*
    k0(31,39,38) -> 6*
    k0(35,19,29) -> 6*
    k0(10,15,29) -> 6*
    k0(30,19,9) -> 6*
    k0(9,41,6) -> 6*
    k0(19,30,32) -> 6*
    k0(19,19,18) -> 6*
    k0(29,17,38) -> 6*
    k0(38,32,41) -> 6*
    k0(6,32,19) -> 6*
    k0(41,38,9) -> 6*
    k0(30,38,18) -> 6*
    k0(15,32,38) -> 6*
    k0(9,10,39) -> 6*
    k0(34,38,17) -> 6*
    k0(18,38,6) -> 6*
    k0(31,29,30) -> 6*
    k0(15,29,19) -> 6*
    k0(30,31,29) -> 6*
    k0(39,35,18) -> 6*
    k0(19,9,10) -> 6*
    k0(41,39,15) -> 6*
    k0(6,18,41) -> 6*
    k0(39,17,15) -> 6*
    k0(31,34,6) -> 6*
    k0(6,30,6) -> 6*
    k0(10,41,19) -> 6*
    k0(40,19,41) -> 6*
    k0(35,30,35) -> 6*
    k0(15,15,41) -> 6*
    k0(34,32,34) -> 6*
    k0(19,41,38) -> 6*
    k0(32,10,34) -> 6*
    k0(17,19,38) -> 6*
    k0(40,31,6) -> 6*
    k0(35,38,30) -> 6*
    k0(10,34,30) -> 6*
    k0(34,40,29) -> 6*
    k0(34,29,15) -> 6*
    k0(19,38,19) -> 6*
    k0(29,40,9) -> 6*
    k0(38,9,6) -> 6*
    k0(18,40,18) -> 6*
    k0(32,18,29) -> 6*
    k0(6,40,6) -> 6*
    k0(35,31,41) -> 6*
    k0(9,29,40) -> 6*
    k0(19,31,30) -> 6*
    k0(32,15,10) -> 6*
    k0(17,9,30) -> 6*
    k0(41,15,29) -> 6*
    k0(6,9,39) -> 6*
    k0(40,41,6) -> 6*
    k0(10,9,38) -> 6*
    k0(29,41,15) -> 6*
    k0(39,39,35) -> 6*
    k0(18,30,10) -> 6*
    k0(38,41,34) -> 6*
    k0(32,19,35) -> 6*
    k0(10,32,17) -> 6*
    k0(15,10,9) -> 6*
    k0(10,6,19) -> 6*
    k0(40,10,39) -> 6*
    k0(15,6,39) -> 6*
    k0(35,10,19) -> 6*
    k0(15,41,31) -> 6*
    k0(9,19,32) -> 6*
    k0(19,6,38) -> 6*
    k0(38,38,15) -> 6*
    k0(19,29,17) -> 6*
    k0(39,40,41) -> 6*
    k0(32,29,35) -> 6*
    k0(17,38,39) -> 6*
    k0(31,31,34) -> 6*
    k0(10,18,39) -> 6*
    k0(29,35,32) -> 6*
    k0(29,9,34) -> 6*
    k0(31,39,29) -> 6*
    k0(41,41,19) -> 6*
    k0(6,35,29) -> 6*
    k0(15,39,18) -> 6*
    k0(30,15,30) -> 6*
    k0(34,6,35) -> 6*
    k0(19,15,39) -> 6*
    k0(29,17,29) -> 6*
    k0(39,19,19) -> 6*
    k0(29,6,15) -> 6*
    k0(19,39,17) -> 6*
    k0(38,32,32) -> 6*
    k0(38,6,34) -> 6*
    k0(6,32,10) -> 6*
    k0(32,30,41) -> 6*
    k0(31,32,40) -> 6*
    k0(41,34,30) -> 6*
    k0(15,32,29) -> 6*
    k0(10,32,9) -> 6*
    k0(30,34,39) -> 6*
    k0(29,10,40) -> 6*
    k0(34,34,38) -> 6*
    k0(9,30,38) -> 6*
    k0(15,29,10) -> 6*
    k0(40,29,40) -> 6*
    k0(35,40,34) -> 6*
    k0(34,31,19) -> 6*
    k0(19,29,9) -> 6*
    k0(39,31,39) -> 6*
    k0(29,18,35) -> 6*
    k0(32,35,17) -> 6*
    k0(32,9,19) -> 6*
    k0(6,18,32) -> 6*
    k0(41,9,38) -> 6*
    k0(10,18,31) -> 6*
    k0(39,17,6) -> 6*
    k0(38,15,35) -> 6*
    k0(41,32,17) -> 6*
    k0(10,41,10) -> 6*
    k0(41,6,19) -> 6*
    k0(15,15,32) -> 6*
    k0(40,19,32) -> 6*
    k0(35,41,40) -> 6*
    k0(39,10,17) -> 6*
    k0(19,41,29) -> 6*
    k0(19,30,15) -> 6*
    k0(34,17,41) -> 6*
    k0(39,41,39) -> 6*
    k0(19,15,31) -> 6*
    k0(18,17,30) -> 6*
    k0(17,19,29) -> 6*
    k0(34,29,6) -> 6*
    k0(19,38,10) -> 6*
    k0(30,34,31) -> 6*
    k0(19,34,40) -> 6*
    k0(38,40,19) -> 6*
    k0(18,10,41) -> 6*
    k0(41,18,39) -> 6*
    k0(35,31,32) -> 6*
    k0(9,18,17) -> 6*
    k0(39,31,31) -> 6*
    k0(29,29,41) -> 6*
    k0(32,35,9) -> 6*
    k0(6,29,38) -> 6*
    k0(10,9,29) -> 6*
    k0(34,39,6) -> 6*
    k0(18,15,17) -> 6*
    k0(32,39,34) -> 6*
    k0(31,30,19) -> 6*
    k0(41,32,9) -> 6*
    k0(35,10,10) -> 6*
    k0(30,32,18) -> 6*
    k0(10,6,10) -> 6*
    k0(35,6,40) -> 6*
    k0(40,30,38) -> 6*
    k0(30,17,34) -> 6*
    k0(29,34,17) -> 6*
    k0(9,39,31) -> 6*
    k0(19,6,29) -> 6*
    k0(17,30,35) -> 6*
    k0(6,19,30) -> 6*
    k0(10,10,35) -> 6*
    k0(39,40,32) -> 6*
    k0(39,29,18) -> 6*
    k0(38,31,17) -> 6*
    k0(32,40,40) -> 6*
    k0(17,38,30) -> 6*
    k0(41,18,31) -> 6*
    k0(10,38,38) -> 6*
    k0(30,18,40) -> 6*
    k0(9,18,9) -> 6*
    k0(17,31,41) -> 6*
    k0(41,41,10) -> 6*
    k0(10,35,19) -> 6*
    k0(15,35,39) -> 6*
    k0(35,39,19) -> 6*
    k0(39,19,10) -> 6*
    k0(34,41,18) -> 6*
    k0(29,6,6) -> 6*
    k0(15,9,41) -> 6*
    k0(19,35,38) -> 6*
    k0(39,15,40) -> 6*
    k0(38,17,39) -> 6*
    k0(38,41,17) -> 6*
    k0(18,15,9) -> 6*
    k0(32,30,32) -> 6*
    k0(32,19,18) -> 6*
    k0(6,17,17) -> 6*
    k0(35,32,30) -> 6*
    k0(9,30,29) -> 6*
    k0(19,32,19) -> 6*
    k0(29,34,9) -> 6*
    k0(9,19,15) -> 6*
    k0(29,10,31) -> 6*
    k0(34,34,29) -> 6*
    k0(18,34,18) -> 6*
    k0(18,19,34) -> 6*
    k0(17,10,19) -> 6*
    k0(31,38,6) -> 6*
    k0(40,18,17) -> 6*
    k0(34,31,10) -> 6*
    k0(29,38,34) -> 6*
    k0(38,31,9) -> 6*
    k0(32,9,10) -> 6*
    k0(6,38,31) -> 6*
    k0(41,9,29) -> 6*
    k0(29,35,15) -> 6*
    k0(19,18,41) -> 6*
    k0(38,35,34) -> 6*
    k0(41,6,10) -> 6*
    k0(35,30,17) -> 6*
    k0(15,35,31) -> 6*
    k0(19,30,6) -> 6*
    k0(40,39,31) -> 6*
    k0(34,17,32) -> 6*
    k0(29,39,40) -> 6*
    k0(39,41,30) -> 6*
    k0(34,6,18) -> 6*
    k0(38,32,15) -> 6*
    k0(38,17,31) -> 6*
    k0(32,41,38) -> 6*
    k0(6,17,9) -> 6*
    k0(41,10,35) -> 6*
    k0(30,19,38) -> 6*
    k0(9,41,35) -> 6*
    k0(38,40,10) -> 6*
    k0(39,34,41) -> 6*
    k0(18,10,32) -> 6*
    k0(32,38,19) -> 6*
    k0(31,40,18) -> 6*
    k0(41,38,38) -> 6*
    k0(40,18,9) -> 6*
    k0(35,40,17) -> 6*
    k0(19,40,6) -> 6*
    k0(29,29,32) -> 6*
    k0(29,18,18) -> 6*
    k0(18,38,35) -> 6*
    k0(32,31,30) -> 6*
    k0(17,40,34) -> 6*
    k0(6,29,29) -> 6*
    k0(6,18,15) -> 6*
    k0(41,35,19) -> 6*
    k0(30,9,30) -> 6*
    k0(15,18,34) -> 6*
    k0(19,9,39) -> 6*
    k0(38,15,18) -> 6*
    k0(31,30,10) -> 6*
    k0(35,30,9) -> 6*
    k0(15,15,15) -> 6*
    k0(35,6,31) -> 6*
    k0(40,30,29) -> 6*
    k0(40,19,15) -> 6*
    k0(39,6,30) -> 6*
    k0(18,39,41) -> 6*
    k0(17,41,40) -> 6*
    k0(32,6,38) -> 6*
    k0(35,34,34) -> 6*
    k0(15,19,40) -> 6*
    k0(10,30,34) -> 6*
    k0(32,29,17) -> 6*
    k0(35,31,15) -> 6*
    k0(10,38,29) -> 6*
    k0(30,38,39) -> 6*
    k0(34,18,30) -> 6*
    k0(29,40,38) -> 6*
    k0(18,18,19) -> 6*
    k0(38,9,35) -> 6*
    k0(17,31,32) -> 6*
    k0(6,40,35) -> 6*
    k0(35,39,10) -> 6*
    k0(10,35,10) -> 6*
    k0(35,35,40) -> 6*
    k0(15,9,32) -> 6*
    k0(10,31,40) -> 6*
    k0(19,35,29) -> 6*
    k0(39,39,9) -> 6*
    k0(32,15,39) -> 6*
    k0(32,39,17) -> 6*
    k0(19,32,10) -> 6*
    k0(9,19,6) -> 6*
    k0(40,41,35) -> 6*
    k0(29,30,30) -> 6*
    k0(18,30,39) -> 6*
    k0(38,34,19) -> 6*
    k0(17,10,10) -> 6*
    k0(17,6,40) -> 6*
    k0(6,41,41) -> 6*
    k0(10,10,18) -> 6*
    k0(39,40,15) -> 6*
    k0(32,29,9) -> 6*
    k0(29,35,6) -> 6*
    k0(15,38,41) -> 6*
    k0(19,18,32) -> 6*
    k0(18,9,17) -> 6*
    k0(18,40,39) -> 6*
    k0(34,6,9) -> 6*
    k0(38,32,6) -> 6*
    k0(32,41,29) -> 6*
    k0(32,30,15) -> 6*
    k0(17,39,19) -> 6*
    k0(32,15,31) -> 6*
    k0(41,30,34) -> 6*
    k0(31,17,30) -> 6*
    k0(30,19,29) -> 6*
    k0(15,17,19) -> 6*
    k0(39,34,32) -> 6*
    k0(18,30,31) -> 6*
    k0(32,38,10) -> 6*
    k0(32,34,40) -> 6*
    k0(17,32,30) -> 6*
    k0(41,38,29) -> 6*
    k0(6,32,39) -> 6*
    k0(31,10,41) -> 6*
    k0(6,6,41) -> 6*
    k0(15,10,30) -> 6*
    k0(10,32,38) -> 6*
    k0(29,38,17) -> 6*
    k0(41,35,10) -> 6*
    k0(6,18,6) -> 6*
    k0(41,31,40) -> 6*
    k0(10,29,19) -> 6*
    k0(15,29,39) -> 6*
    k0(34,35,18) -> 6*
    k0(9,31,18) -> 6*
    k0(19,29,38) -> 6*
    k0(39,9,40) -> 6*
    k0(31,15,17) -> 6*
    k0(40,19,6) -> 6*
    k0(15,15,6) -> 6*
    k0(34,17,15) -> 6*
    k0(39,17,35) -> 6*
    k0(18,39,32) -> 6*
    k0(17,30,17) -> 6*
    k0(32,6,29) -> 6*
    k0(41,10,18) -> 6*
    k0(35,19,41) -> 6*
    k0(30,30,35) -> 6*
    k0(10,15,41) -> 6*
    k0(15,39,39) -> 6*
    k0(29,32,34) -> 6*
    k0(9,17,40) -> 6*
    k0(19,19,30) -> 6*
    k0(18,10,15) -> 6*
    k0(6,32,31) -> 6*
    k0(35,31,6) -> 6*
    k0(30,38,30) -> 6*
    k0(29,40,29) -> 6*
    k0(29,29,15) -> 6*
    k0(18,18,10) -> 6*
    k0(38,29,34) -> 6*
    k0(17,40,17) -> 6*
    k0(15,29,31) -> 6*
    k0(30,31,41) -> 6*
    k0(39,35,30) -> 6*
    k0(32,35,38) -> 6*
    k0(31,15,9) -> 6*
    k0(35,41,6) -> 6*
    k0(19,17,17) -> 6*
    k0(34,39,35) -> 6*
    k0(9,35,35) -> 6*
    k0(38,34,10) -> 6*
    k0(38,30,40) -> 6*
    k0(17,30,9) -> 6*
    k0(17,6,31) -> 6*
    k0(32,32,19) -> 6*
    k0(31,34,18) -> 6*
    k0(6,41,32) -> 6*
    k0(6,30,18) -> 6*
    k0(31,19,34) -> 6*
    k0(6,15,34) -> 6*
    k0(10,10,9) -> 6*
    k0(41,32,38) -> 6*
    k0(35,10,39) -> 6*
    k0(10,6,39) -> 6*
    k0(30,10,19) -> 6*
    k0(10,41,31) -> 6*
    k0(39,10,38) -> 6*
    k0(18,32,35) -> 6*
    k0(17,34,34) -> 6*
    k0(41,29,19) -> 6*
    k0(40,31,18) -> 6*
    k0(15,38,32) -> 6*
    k0(34,40,41) -> 6*
    k0(19,38,31) -> 6*
    k0(18,40,30) -> 6*
    k0(38,9,18) -> 6*
    k0(17,31,15) -> 6*
    k0(32,18,41) -> 6*
    k0(15,9,15) -> 6*
    k0(9,18,38) -> 6*
    k0(32,30,6) -> 6*
    k0(17,39,10) -> 6*
    k0(17,35,40) -> 6*
    k0(15,17,10) -> 6*
    k0(41,15,41) -> 6*
    k0(10,39,18) -> 6*
    k0(40,17,40) -> 6*
    k0(29,6,35) -> 6*
    k0(34,19,19) -> 6*
    k0(9,15,19) -> 6*
    k0(19,17,9) -> 6*
    k0(39,19,39) -> 6*
    k0(18,15,38) -> 6*
    k0(31,10,32) -> 6*
    k0(6,6,32) -> 6*
    k0(10,32,29) -> 6*
    k0(29,34,38) -> 6*
    k0(32,40,6) -> 6*
    k0(31,38,35) -> 6*
    k0(6,34,35) -> 6*
    k0(10,29,10) -> 6*
    k0(30,40,34) -> 6*
    k0(35,29,40) -> 6*
    k0(19,18,15) -> 6*
    k0(39,9,31) -> 6*
    k0(34,31,39) -> 6*
    k0(19,29,29) -> 6*
    k0(29,31,19) -> 6*
    k0(38,31,38) -> 6*
    k0(32,9,39) -> 6*
    k0(40,35,35) -> 6*
    k0(15,31,35) -> 6*
    k0(34,17,6) -> 6*
    k0(41,10,9) -> 6*
    k0(6,35,41) -> 6*
    k0(31,39,41) -> 6*
    k0(41,6,39) -> 6*
    k0(41,41,31) -> 6*
    k0(30,41,40) -> 6*
    k0(10,15,32) -> 6*
    k0(15,39,30) -> 6*
    k0(35,19,32) -> 6*
    k0(34,10,17) -> 6*
    k0(39,34,15) -> 6*
    k0(9,6,17) -> 6*
    k0(9,41,9) -> 6*
    k0(29,17,41) -> 6*
    k0(18,10,6) -> 6*
    k0(39,19,31) -> 6*
    k0(34,41,39) -> 6*
    k0(6,17,38) -> 6*
    k0(29,29,6) -> 6*
    k0(15,32,41) -> 6*
    k0(39,38,40) -> 6*
    k0(18,38,9) -> 6*
    k0(31,18,19) -> 6*
    k0(30,31,32) -> 6*
    k0(40,18,38) -> 6*
    k0(19,40,35) -> 6*
    k0(34,31,31) -> 6*
    k0(32,35,29) -> 6*
    k0(41,39,18) -> 6*
    k0(40,15,19) -> 6*
    k0(29,39,6) -> 6*
    k0(39,17,18) -> 6*
    k0(38,19,17) -> 6*
    k0(18,39,15) -> 6*
    k0(32,32,10) -> 6*
    k0(41,32,29) -> 6*
    k0(31,30,39) -> 6*
    k0(30,10,10) -> 6*
    k0(30,6,40) -> 6*
    k0(35,30,38) -> 6*
    k0(39,10,29) -> 6*
    k0(19,41,41) -> 6*
    k0(17,19,41) -> 6*
    k0(41,29,10) -> 6*
    k0(34,40,32) -> 6*
    k0(34,29,18) -> 6*
    k0(9,10,34) -> 6*
    k0(38,9,9) -> 6*
    k0(38,40,31) -> 6*
    k0(17,31,6) -> 6*
    k0(32,18,32) -> 6*
    k0(31,9,17) -> 6*
    k0(6,40,9) -> 6*
    k0(31,40,39) -> 6*
    k0(15,9,6) -> 6*
    k0(9,18,29) -> 6*
    k0(41,15,32) -> 6*
    k0(40,6,17) -> 6*
    k0(10,35,39) -> 6*
    k0(30,39,19) -> 6*
    k0(40,41,9) -> 6*
    k0(29,41,18) -> 6*
    k0(9,15,10) -> 6*
    k0(10,9,41) -> 6*
    k0(34,19,10) -> 6*
    k0(34,15,40) -> 6*
    k0(39,39,38) -> 6*
    k0(18,15,29) -> 6*
    k0(38,19,9) -> 6*
    k0(17,41,6) -> 6*
    k0(6,41,15) -> 6*
    k0(31,30,31) -> 6*
    k0(30,32,30) -> 6*
    k0(15,41,34) -> 6*
    k0(19,32,39) -> 6*
    k0(29,34,29) -> 6*
    k0(9,19,35) -> 6*
    k0(38,38,18) -> 6*
    k0(19,6,41) -> 6*
    k0(17,10,39) -> 6*
    k0(35,18,17) -> 6*
    k0(15,38,15) -> 6*
    k0(29,31,10) -> 6*
    k0(19,18,6) -> 6*
    k0(39,29,30) -> 6*
    k0(38,31,29) -> 6*
    k0(32,29,38) -> 6*
    k0(9,29,35) -> 6*
    k0(31,39,32) -> 6*
    k0(6,35,32) -> 6*
    k0(6,9,34) -> 6*
    k0(30,30,17) -> 6*
    k0(39,34,6) -> 6*
    k0(35,39,31) -> 6*
    k0(10,35,31) -> 6*
    k0(29,6,18) -> 6*
    k0(29,17,32) -> 6*
    k0(34,41,30) -> 6*
    k0(18,41,19) -> 6*
    k0(32,19,30) -> 6*
    k0(31,10,15) -> 6*
    k0(6,17,29) -> 6*
    k0(6,6,15) -> 6*
    k0(15,32,32) -> 6*
    k0(40,10,34) -> 6*
    k0(15,6,34) -> 6*
    k0(9,30,41) -> 6*
    k0(34,34,41) -> 6*
    k0(19,32,31) -> 6*
    k0(18,34,30) -> 6*
    k0(31,18,10) -> 6*
    k0(6,10,40) -> 6*
    k0(40,18,29) -> 6*
    k0(30,40,17) -> 6*
    k0(35,18,9) -> 6*
    k0(17,29,40) -> 6*
    k0(41,35,39) -> 6*
    k0(6,18,35) -> 6*
    k0(40,15,10) -> 6*
    k0(41,9,41) -> 6*
    k0(10,18,34) -> 6*
    k0(9,35,17) -> 6*
    k0(9,9,19) -> 6*
    k0(32,17,17) -> 6*
    k0(18,9,38) -> 6*
    k0(30,30,9) -> 6*
    k0(10,15,15) -> 6*
    k0(40,19,35) -> 6*
    k0(30,6,31) -> 6*
    k0(35,30,29) -> 6*
    k0(15,15,35) -> 6*
    k0(35,19,15) -> 6*
    k0(19,41,32) -> 6*
    k0(19,30,18) -> 6*
    k0(34,6,30) -> 6*
    k0(19,15,34) -> 6*
    k0(18,32,17) -> 6*
    k0(18,6,19) -> 6*
    k0(17,19,32) -> 6*
    k0(31,32,35) -> 6*
    k0(10,19,40) -> 6*
    k0(30,34,34) -> 6*
    k0(32,38,31) -> 6*
    k0(31,40,30) -> 6*
    k0(15,40,19) -> 6*
    k0(30,31,15) -> 6*
    k0(40,29,35) -> 6*
    k0(39,31,34) -> 6*
    k0(29,18,30) -> 6*
    k0(18,18,39) -> 6*
    k0(41,35,31) -> 6*
    k0(6,29,41) -> 6*
    k0(30,39,10) -> 6*
    k0(30,35,40) -> 6*
    k0(10,9,32) -> 6*
    k0(9,35,9) -> 6*
    k0(39,39,29) -> 6*
    k0(34,39,9) -> 6*
    k0(38,15,30) -> 6*
    k0(32,17,9) -> 6*
    k0(31,15,38) -> 6*
    k0(35,41,35) -> 6*
    k0(40,30,41) -> 6*
    k0(39,32,40) -> 6*
    k0(19,6,32) -> 6*
    k0(9,39,34) -> 6*
    k0(18,32,9) -> 6*
    k0(38,34,39) -> 6*
    k0(17,30,38) -> 6*
    k0(6,34,17) -> 6*
    k0(34,40,15) -> 6*
    k0(19,34,35) -> 6*
    k0(32,29,29) -> 6*
    k0(32,18,15) -> 6*
    k0(41,18,34) -> 6*
    k0(40,35,17) -> 6*
    k0(15,31,17) -> 6*
    k0(10,38,41) -> 6*
    k0(40,9,19) -> 6*
    k0(9,40,40) -> 6*
    k0(18,18,31) -> 6*
    k0(41,15,15) -> 6*
    k0(29,6,9) -> 6*
    k0(18,41,10) -> 6*
    k0(19,35,41) -> 6*
    k0(6,6,6) -> 6*
    k0(31,10,6) -> 6*
    k0(41,19,40) -> 6*
    k0(15,41,17) -> 6*
    k0(15,17,39) -> 6*
    k0(10,17,19) -> 6*
    k0(34,34,32) -> 6*
    k0(9,30,32) -> 6*
    k0(9,19,18) -> 6*
    k0(19,17,38) -> 6*
    k0(38,34,31) -> 6*
    k0(6,34,9) -> 6*
    k0(6,10,31) -> 6*
    k0(31,38,9) -> 6*
    k0(10,10,30) -> 6*
    k0(17,18,17) -> 6*
    k0(32,40,35) -> 6*
    k0(41,9,32) -> 6*
    k0(6,38,34) -> 6*
    k0(40,35,9) -> 6*
    k0(15,31,9) -> 6*
    k0(10,29,39) -> 6*
    k0(29,35,18) -> 6*
    k0(9,9,10) -> 6*
    k0(34,9,40) -> 6*
    k0(18,9,29) -> 6*
    k0(31,39,15) -> 6*
    k0(6,35,15) -> 6*
    k0(35,19,6) -> 6*
    k0(10,15,6) -> 6*
    k0(40,39,34) -> 6*
    k0(15,35,34) -> 6*
    k0(34,17,35) -> 6*
    k0(39,30,19) -> 6*
    k0(29,17,15) -> 6*
    k0(38,32,18) -> 6*
    k0(18,6,10) -> 6*
    k0(38,17,34) -> 6*
    k0(32,41,41) -> 6*
    k0(17,39,31) -> 6*
    k0(6,39,40) -> 6*
    k0(15,32,15) -> 6*
    k0(30,19,41) -> 6*
    k0(15,17,31) -> 6*
    k0(10,39,39) -> 6*
    k0(9,41,38) -> 6*
    k0(18,10,35) -> 6*
    k0(41,38,41) -> 6*
    k0(15,40,10) -> 6*
    k0(30,31,6) -> 6*
    k0(40,40,40) -> 6*
    k0(9,38,19) -> 6*
    k0(19,40,9) -> 6*
    k0(38,18,40) -> 6*
    k0(18,38,38) -> 6*
    k0(17,18,9) -> 6*
    k0(6,29,32) -> 6*
    k0(6,18,18) -> 6*
    k0(10,29,31) -> 6*
    k0(34,35,30) -> 6*
    k0(9,31,30) -> 6*
    k0(18,35,19) -> 6*
    k0(41,17,19) -> 6*
    k0(31,15,29) -> 6*
    k0(30,41,6) -> 6*
    k0(40,30,32) -> 6*
    k0(40,19,18) -> 6*
    k0(15,15,18) -> 6*
    k0(19,41,15) -> 6*
    k0(29,39,35) -> 6*
    k0(32,32,39) -> 6*
    k0(17,30,29) -> 6*
    k0(17,19,15) -> 6*
    k0(32,6,41) -> 6*
    k0(41,10,30) -> 6*
    k0(30,10,39) -> 6*
    k0(39,38,6) -> 6*
    k0(34,10,38) -> 6*
    k0(9,6,38) -> 6*
    k0(32,18,6) -> 6*
    k0(41,29,39) -> 6*
    k0(40,9,10) -> 6*
    k0(35,31,18) -> 6*
    k0(10,38,32) -> 6*
    k0(9,29,17) -> 6*
    k0(29,40,41) -> 6*
    k0(41,15,6) -> 6*
    k0(6,40,38) -> 6*
    k0(10,9,15) -> 6*
    k0(15,9,35) -> 6*
    k0(19,35,32) -> 6*
    k0(19,9,34) -> 6*
    k0(31,41,19) -> 6*
    k0(41,39,39) -> 6*
    k0(10,17,10) -> 6*
    k0(35,17,40) -> 6*
    k0(40,41,38) -> 6*
    k0(9,15,39) -> 6*
    k0(19,17,29) -> 6*
    k0(29,19,19) -> 6*
    k0(19,6,15) -> 6*
    k0(9,39,17) -> 6*
    k0(34,19,39) -> 6*
    k0(38,19,38) -> 6*
    k0(17,41,35) -> 6*
    k0(32,32,31) -> 6*
    k0(31,34,30) -> 6*
    k0(6,30,30) -> 6*
    k0(40,38,19) -> 6*
    k0(15,34,19) -> 6*
    k0(39,40,18) -> 6*
    k0(19,10,40) -> 6*
    k0(41,29,31) -> 6*
    k0(30,29,40) -> 6*
    k0(40,31,30) -> 6*
    k0(9,29,9) -> 6*
    k0(34,9,31) -> 6*
    k0(29,31,39) -> 6*
    k0(19,18,35) -> 6*
    k0(38,9,30) -> 6*
    k0(6,35,6) -> 6*
    k0(31,9,38) -> 6*
    k0(35,35,35) -> 6*
    k0(10,31,35) -> 6*
    k0(39,30,10) -> 6*
    k0(29,17,6) -> 6*
    k0(32,41,32) -> 6*
    k0(32,30,18) -> 6*
    k0(32,15,34) -> 6*
    k0(31,32,17) -> 6*
    k0(15,32,6) -> 6*
    k0(31,6,19) -> 6*
    k0(10,39,30) -> 6*
    k0(30,19,32) -> 6*
    k0(9,41,29) -> 6*
    k0(40,6,38) -> 6*
    k0(29,10,17) -> 6*
    k0(34,34,15) -> 6*
    k0(9,30,15) -> 6*
    k0(29,41,39) -> 6*
    k0(34,19,31) -> 6*
    k0(9,15,31) -> 6*
    k0(18,30,34) -> 6*
    k0(41,38,32) -> 6*
    k0(40,29,17) -> 6*
    k0(10,32,41) -> 6*
    k0(9,38,10) -> 6*
    k0(34,38,40) -> 6*
    k0(9,34,40) -> 6*
    k0(18,38,29) -> 6*
    k0(38,38,39) -> 6*
    k0(41,9,15) -> 6*
    k0(6,38,17) -> 6*
    k0(31,18,39) -> 6*
    k0(35,18,38) -> 6*
    k0(18,35,10) -> 6*
    k0(19,29,41) -> 6*
    k0(29,31,31) -> 6*
    k0(18,31,40) -> 6*
    k0(41,17,10) -> 6*
    k0(40,39,17) -> 6*
    k0(35,15,19) -> 6*
    k0(40,15,39) -> 6*
    k0(34,17,18) -> 6*
    k0(17,19,6) -> 6*
    k0(32,6,32) -> 6*
    k0(31,32,9) -> 6*
    k0(19,34,17) -> 6*
    k0(30,30,38) -> 6*
    k0(34,10,29) -> 6*
    k0(9,6,29) -> 6*
    k0(18,10,18) -> 6*
    k0(32,34,35) -> 6*
    k0(6,32,34) -> 6*
    k0(40,29,9) -> 6*
    k0(29,40,32) -> 6*
    k0(29,29,18) -> 6*
    k0(6,40,29) -> 6*
    k0(6,29,15) -> 6*
    k0(10,9,6) -> 6*
    k0(41,31,35) -> 6*
    k0(31,18,31) -> 6*
    k0(15,29,34) -> 6*
    k0(31,41,10) -> 6*
    k0(32,35,41) -> 6*
    k0(41,39,30) -> 6*
    k0(40,41,29) -> 6*
    k0(35,6,17) -> 6*
    k0(40,30,15) -> 6*
    k0(35,41,9) -> 6*
    k0(19,6,6) -> 6*
    k0(40,15,31) -> 6*
    k0(29,19,10) -> 6*
    k0(29,15,40) -> 6*
    k0(39,17,30) -> 6*
    k0(34,39,38) -> 6*
    k0(9,35,38) -> 6*
    k0(38,19,29) -> 6*
    k0(32,17,38) -> 6*
    k0(40,38,10) -> 6*
    k0(41,32,41) -> 6*
    k0(15,34,10) -> 6*
    k0(15,30,40) -> 6*
    k0(10,41,34) -> 6*
    k0(40,34,40) -> 6*
    k0(19,10,31) -> 6*
    k0(9,32,19) -> 6*
    k0(19,34,9) -> 6*
    k0(39,10,41) -> 6*
    k0(18,32,38) -> 6*
    k0(10,38,15) -> 6*
    k0(30,18,17) -> 6*
    k0(34,29,30) -> 6*
    k0(19,38,34) -> 6*
    k0(18,29,19) -> 6*
    k0(17,31,18) -> 6*
    k0(31,9,29) -> 6*
    k0(15,9,18) -> 6*
    k0(39,15,17) -> 6*
    k0(19,35,15) -> 6*
    k0(9,18,41) -> 6*
    k0(31,6,10) -> 6*
    k0(40,6,29) -> 6*
    k0(34,34,6) -> 6*
    k0(9,30,6) -> 6*
    k0(30,39,31) -> 6*
    k0(19,39,40) -> 6*
    k0(29,41,30) -> 6*
    k0(38,30,35) -> 6*
    k0(18,15,41) -> 6*
    k0(17,17,40) -> 6*
    k0(6,6,35) -> 6*
    k0(31,10,35) -> 6*
    k0(10,32,32) -> 6*
    k0(35,10,34) -> 6*
    k0(10,6,34) -> 6*
    k0(29,34,41) -> 6*
    k0(38,38,30) -> 6*
    k0(32,40,9) -> 6*
    k0(41,9,6) -> 6*
    k0(31,38,38) -> 6*
    k0(6,34,38) -> 6*
    k0(30,18,9) -> 6*
    k0(35,18,29) -> 6*
    k0(9,40,6) -> 6*
    k0(19,29,32) -> 6*
    k0(19,18,18) -> 6*
    k0(38,31,41) -> 6*
    k0(31,35,19) -> 6*
    k0(6,31,19) -> 6*
    k0(35,15,10) -> 6*
    k0(40,35,38) -> 6*
    k0(15,31,38) -> 6*
    k0(9,9,39) -> 6*
    k0(39,15,9) -> 6*
    k0(32,41,15) -> 6*
    k0(17,35,35) -> 6*
    k0(41,41,34) -> 6*
    k0(40,32,19) -> 6*
    k0(35,19,35) -> 6*
    k0(30,30,29) -> 6*
    k0(10,15,35) -> 6*
    k0(30,19,15) -> 6*
    k0(39,34,18) -> 6*
    k0(18,10,9) -> 6*
    k0(39,19,34) -> 6*
    k0(29,6,30) -> 6*
    k0(18,41,31) -> 6*
    k0(18,6,39) -> 6*
    k0(38,10,19) -> 6*
    k0(41,38,15) -> 6*
    k0(6,17,41) -> 6*
    k0(6,29,6) -> 6*
    k0(10,40,19) -> 6*
    k0(40,18,41) -> 6*
    k0(35,29,35) -> 6*
    k0(34,31,34) -> 6*
    k0(19,40,38) -> 6*
    k0(32,35,32) -> 6*
    k0(32,9,34) -> 6*
    k0(17,18,38) -> 6*
    k0(40,30,6) -> 6*
    k0(34,39,29) -> 6*
    k0(9,35,29) -> 6*
    k0(29,39,9) -> 6*
    k0(18,39,18) -> 6*
    k0(32,17,29) -> 6*
    k0(32,6,15) -> 6*
    k0(17,15,19) -> 6*
    k0(41,32,32) -> 6*
    k0(6,39,6) -> 6*
    k0(41,6,34) -> 6*
    k0(15,19,17) -> 6*
    k0(35,30,41) -> 6*
    k0(9,32,10) -> 6*
    k0(30,41,35) -> 6*
    k0(19,30,30) -> 6*
    k0(39,10,32) -> 6*
    k0(34,32,40) -> 6*
    k0(18,32,29) -> 6*
    k0(32,10,40) -> 6*
    k0(40,40,6) -> 6*
    k0(29,40,15) -> 6*
    k0(18,29,10) -> 6*
    k0(39,38,35) -> 6*
    k0(38,40,34) -> 6*
    k0(32,18,35) -> 6*
    k0(35,35,17) -> 6*
    k0(15,9,9) -> 6*
    k0(10,31,17) -> 6*
    k0(15,40,31) -> 6*
    k0(40,9,39) -> 6*
    k0(19,35,6) -> 6*
    k0(35,9,19) -> 6*
    k0(9,18,32) -> 6*
    k0(41,15,35) -> 6*
    k0(39,39,41) -> 6*
    k0(38,41,40) -> 6*
    k0(18,15,32) -> 6*
    k0(17,6,17) -> 6*
    k0(17,41,9) -> 6*
    k0(6,41,18) -> 6*
    k0(31,30,34) -> 6*
    k0(10,41,17) -> 6*
    k0(10,17,39) -> 6*
    k0(15,19,9) -> 6*
    k0(29,34,32) -> 6*
    k0(31,38,29) -> 6*
    k0(41,40,19) -> 6*
    k0(6,34,29) -> 6*
    k0(15,38,18) -> 6*
    k0(39,18,19) -> 6*
    k0(19,38,17) -> 6*
    k0(38,31,32) -> 6*
    k0(31,35,10) -> 6*
    k0(6,31,10) -> 6*
    k0(32,29,41) -> 6*
    k0(31,31,40) -> 6*
    k0(40,35,29) -> 6*
    k0(10,31,9) -> 6*
    k0(15,31,29) -> 6*
    k0(35,35,9) -> 6*
    k0(29,9,40) -> 6*
    k0(9,29,38) -> 6*
    k0(40,32,10) -> 6*
    k0(30,19,6) -> 6*
    k0(35,39,34) -> 6*
    k0(10,35,34) -> 6*
    k0(39,30,39) -> 6*
    k0(29,17,35) -> 6*
    k0(34,30,19) -> 6*
    k0(38,10,10) -> 6*
    k0(38,6,40) -> 6*
    k0(32,34,17) -> 6*
    k0(6,6,18) -> 6*
    k0(31,10,18) -> 6*
    k0(6,17,32) -> 6*
    k0(10,32,15) -> 6*
    k0(10,17,31) -> 6*
    k0(19,32,34) -> 6*
    k0(9,19,30) -> 6*
    k0(17,10,34) -> 6*
    k0(41,31,17) -> 6*
    k0(10,40,10) -> 6*
    k0(40,18,32) -> 6*
    k0(35,40,40) -> 6*
    k0(39,9,17) -> 6*
    k0(19,40,29) -> 6*
    k0(19,29,15) -> 6*
    k0(39,40,39) -> 6*
    k0(17,18,29) -> 6*
    k0(29,35,30) -> 6*
    k0(18,35,39) -> 6*
    k0(38,39,19) -> 6*
    k0(17,15,10) -> 6*
    k0(18,9,41) -> 6*
    k0(32,6,6) -> 6*
    k0(41,41,17) -> 6*
    k0(41,17,39) -> 6*
    k0(35,30,32) -> 6*
    k0(35,19,18) -> 6*
    k0(10,15,18) -> 6*
    k0(9,17,17) -> 6*
    k0(39,30,31) -> 6*
    k0(38,32,30) -> 6*
    k0(32,10,31) -> 6*
    k0(17,19,35) -> 6*
    k0(32,34,9) -> 6*
    k0(31,32,38) -> 6*
    k0(34,38,6) -> 6*
    k0(29,10,38) -> 6*
    k0(32,38,34) -> 6*
    k0(31,29,19) -> 6*
    k0(41,31,9) -> 6*
    k0(35,9,10) -> 6*
    k0(30,31,18) -> 6*
    k0(40,29,38) -> 6*
    k0(9,38,31) -> 6*
    k0(32,35,15) -> 6*
    k0(17,29,35) -> 6*
    k0(41,35,34) -> 6*
    k0(6,18,30) -> 6*
    k0(10,9,35) -> 6*
    k0(39,39,32) -> 6*
    k0(38,30,17) -> 6*
    k0(18,35,31) -> 6*
    k0(32,39,40) -> 6*
    k0(41,32,15) -> 6*
    k0(41,17,31) -> 6*
    k0(31,15,41) -> 6*
    k0(30,17,40) -> 6*
    k0(40,19,30) -> 6*
    k0(35,41,38) -> 6*
    k0(15,15,30) -> 6*
    k0(9,17,9) -> 6*
    k0(29,19,39) -> 6*
    k0(19,6,35) -> 6*
    k0(39,10,15) -> 6*
    k0(17,30,41) -> 6*
    k0(41,40,10) -> 6*
    k0(15,34,39) -> 6*
    k0(35,38,19) -> 6*
    k0(10,34,19) -> 6*
    k0(39,18,10) -> 6*
    k0(34,40,18) -> 6*
    k0(19,34,38) -> 6*
    k0(38,40,17) -> 6*
    k0(32,29,32) -> 6*
    k0(32,18,18) -> 6*
    k0(35,31,30) -> 6*
    k0(29,9,31) -> 6*
    k0(9,29,29) -> 6*
    k0(19,31,19) -> 6*
    k0(9,18,15) -> 6*
    k0(17,35,17) -> 6*
    k0(18,18,34) -> 6*
    k0(17,9,19) -> 6*
    k0(41,15,18) -> 6*
    k0(40,17,17) -> 6*
    k0(34,30,10) -> 6*
    k0(30,35,35) -> 6*
    k0(38,6,31) -> 6*
    k0(38,30,9) -> 6*
    k0(18,15,15) -> 6*
    k0(31,10,9) -> 6*
    k0(6,6,9) -> 6*
    k0(31,41,31) -> 6*
    k0(31,6,39) -> 6*
    k0(10,32,6) -> 6*
    k0(29,34,15) -> 6*
    k0(35,6,38) -> 6*
    k0(19,17,41) -> 6*
    k0(29,19,31) -> 6*
    k0(39,32,35) -> 6*
    k0(18,19,40) -> 6*
    k0(38,34,34) -> 6*
    k0(35,29,17) -> 6*
    k0(40,38,31) -> 6*
    k0(19,29,6) -> 6*
    k0(15,34,31) -> 6*
    k0(29,38,40) -> 6*
    k0(39,40,30) -> 6*
    k0(38,31,15) -> 6*
    k0(32,40,38) -> 6*
    k0(41,9,35) -> 6*
    k0(30,18,38) -> 6*
    k0(9,40,35) -> 6*
    k0(38,39,10) -> 6*
    k0(38,35,40) -> 6*
    k0(18,9,32) -> 6*
    k0(17,35,9) -> 6*
    k0(6,35,18) -> 6*
    k0(31,39,18) -> 6*
    k0(40,17,9) -> 6*
    k0(30,15,19) -> 6*
    k0(35,39,17) -> 6*
    k0(35,15,39) -> 6*
    k0(29,17,18) -> 6*
    k0(19,39,6) -> 6*
    k0(39,15,38) -> 6*
    k0(32,30,30) -> 6*
    k0(17,39,34) -> 6*
    k0(41,34,19) -> 6*
    k0(31,32,29) -> 6*
    k0(6,17,15) -> 6*
    k0(15,32,18) -> 6*
    k0(15,17,34) -> 6*
    k0(29,10,29) -> 6*
    k0(9,41,41) -> 6*
    k0(31,29,10) -> 6*
    k0(40,29,29) -> 6*
    k0(40,18,15) -> 6*
    k0(35,29,9) -> 6*
    k0(18,38,41) -> 6*
    k0(32,35,6) -> 6*
    k0(17,40,40) -> 6*
    k0(15,18,40) -> 6*
    k0(10,29,34) -> 6*
    k0(41,32,6) -> 6*
    k0(31,15,32) -> 6*
    k0(35,41,29) -> 6*
    k0(30,6,17) -> 6*
    k0(35,30,15) -> 6*
    k0(30,41,9) -> 6*
    k0(35,15,31) -> 6*
    k0(39,10,6) -> 6*
    k0(19,41,18) -> 6*
    k0(34,17,30) -> 6*
    k0(29,39,38) -> 6*
    k0(18,17,19) -> 6*
    k0(17,30,32) -> 6*
    k0(17,19,18) -> 6*
    k0(35,38,10) -> 6*
    k0(10,34,10) -> 6*
    k0(6,39,35) -> 6*
    k0(35,34,40) -> 6*
    k0(10,30,40) -> 6*
    k0(9,32,39) -> 6*
    k0(19,34,29) -> 6*
    k0(39,38,9) -> 6*
    k0(9,6,41) -> 6*
    k0(34,10,41) -> 6*
    k0(18,10,30) -> 6*
    k0(32,38,17) -> 6*
    k0(40,40,35) -> 6*
    k0(19,31,10) -> 6*
    k0(9,18,6) -> 6*
    k0(29,29,30) -> 6*
    k0(18,29,39) -> 6*
    k0(17,9,10) -> 6*
    k0(6,40,41) -> 6*
    k0(10,9,18) -> 6*
    k0(34,15,17) -> 6*
    k0(39,39,15) -> 6*
    k0(18,15,6) -> 6*
    k0(40,41,41) -> 6*
    k0(35,6,29) -> 6*
    k0(29,34,6) -> 6*
    k0(19,17,32) -> 6*
    k0(19,6,18) -> 6*
    k0(38,19,41) -> 6*
    k0(18,39,39) -> 6*
    k0(32,32,34) -> 6*
    k0(17,41,38) -> 6*
    k0(6,19,19) -> 6*
    k0(30,10,34) -> 6*
    k0(15,19,38) -> 6*
    k0(9,32,31) -> 6*
    k0(38,31,6) -> 6*
    k0(32,40,29) -> 6*
    k0(32,29,15) -> 6*
    k0(17,38,19) -> 6*
    k0(41,29,34) -> 6*
    k0(30,18,29) -> 6*
    k0(18,29,31) -> 6*
    k0(17,31,30) -> 6*
    k0(31,35,39) -> 6*
    k0(6,31,39) -> 6*
    k0(31,9,41) -> 6*
    k0(30,15,10) -> 6*
    k0(35,35,38) -> 6*
    k0(15,9,30) -> 6*
    k0(10,31,38) -> 6*
    k0(34,15,9) -> 6*
    k0(39,15,29) -> 6*
    k0(38,41,6) -> 6*
    k0(41,34,10) -> 6*
    k0(6,17,6) -> 6*
    k0(41,30,40) -> 6*
    k0(40,32,39) -> 6*
    k0(30,19,35) -> 6*
    k0(35,32,19) -> 6*
    k0(9,41,32) -> 6*
    k0(40,6,41) -> 6*
    k0(9,30,18) -> 6*
    k0(34,34,18) -> 6*
    k0(9,15,34) -> 6*
    k0(34,19,34) -> 6*
    k0(38,10,39) -> 6*
    k0(6,10,17) -> 6*
    k0(17,6,38) -> 6*
    k0(6,41,39) -> 6*
    k0(40,18,6) -> 6*
    k0(18,38,32) -> 6*
    k0(17,29,17) -> 6*
    k0(41,9,18) -> 6*
    k0(35,18,41) -> 6*
    k0(30,29,35) -> 6*
    k0(15,38,39) -> 6*
    k0(29,31,34) -> 6*
    k0(19,18,30) -> 6*
    k0(18,9,15) -> 6*
    k0(31,35,31) -> 6*
    k0(6,31,31) -> 6*
    k0(35,30,6) -> 6*
    k0(39,41,19) -> 6*
    k0(29,39,29) -> 6*
    k0(18,17,10) -> 6*
    k0(17,39,17) -> 6*
    k0(32,6,35) -> 6*
    k0(17,15,39) -> 6*
    k0(10,19,17) -> 6*
    k0(30,30,41) -> 6*
    k0(40,32,31) -> 6*
    k0(29,32,40) -> 6*
    k0(9,6,32) -> 6*
    k0(34,10,32) -> 6*
    k0(39,34,30) -> 6*
    k0(32,34,38) -> 6*
    k0(35,40,6) -> 6*
    k0(9,34,35) -> 6*
    k0(34,38,35) -> 6*
    k0(38,29,40) -> 6*
    k0(32,31,19) -> 6*
    k0(17,29,9) -> 6*
    k0(6,40,32) -> 6*
    k0(6,29,18) -> 6*
    k0(30,35,17) -> 6*
    k0(10,9,9) -> 6*
    k0(41,31,38) -> 6*
    k0(31,18,34) -> 6*
    k0(10,40,31) -> 6*
    k0(30,9,19) -> 6*
    k0(35,9,39) -> 6*
    k0(39,9,38) -> 6*
    k0(18,31,35) -> 6*
    k0(31,15,15) -> 6*
    k0(40,41,32) -> 6*
    k0(40,30,18) -> 6*
    k0(39,32,17) -> 6*
    k0(19,6,9) -> 6*
    k0(40,15,34) -> 6*
    k0(9,35,41) -> 6*
    k0(34,39,41) -> 6*
    k0(39,6,19) -> 6*
    k0(38,19,32) -> 6*
    k0(18,39,30) -> 6*
    k0(17,41,29) -> 6*
    k0(17,30,15) -> 6*
    k0(32,17,41) -> 6*
    k0(17,15,31) -> 6*
    k0(6,19,10) -> 6*
    k0(31,19,40) -> 6*
    k0(6,15,40) -> 6*
    k0(10,19,9) -> 6*
    k0(15,19,29) -> 6*
    k0(9,17,38) -> 6*
    k0(18,32,41) -> 6*
    k0(32,29,6) -> 6*
    k0(17,38,10) -> 6*
    k0(17,34,40) -> 6*
    k0(10,38,18) -> 6*
    k0(39,18,39) -> 6*
    k0(34,18,19) -> 6*
    k0(31,9,32) -> 6*
    k0(35,35,29) -> 6*
    k0(10,31,29) -> 6*
    k0(30,35,9) -> 6*
    k0(19,35,18) -> 6*
    k0(32,39,6) -> 6*
    k0(41,19,17) -> 6*
    k0(35,32,10) -> 6*
    k0(40,6,32) -> 6*
    k0(30,39,34) -> 6*
    k0(34,30,39) -> 6*
    k0(29,30,19) -> 6*
    k0(39,32,9) -> 6*
    k0(19,17,15) -> 6*
    k0(38,30,38) -> 6*
    k0(17,6,29) -> 6*
    k0(6,41,30) -> 6*
    k0(40,34,35) -> 6*
    k0(15,30,35) -> 6*
    k0(41,9,9) -> 6*
    k0(6,34,41) -> 6*
    k0(31,38,41) -> 6*
    k0(41,40,31) -> 6*
    k0(30,40,40) -> 6*
    k0(35,18,32) -> 6*
    k0(15,38,30) -> 6*
    k0(34,9,17) -> 6*
    k0(9,40,9) -> 6*
    k0(18,9,6) -> 6*
    k0(39,18,31) -> 6*
    k0(34,40,39) -> 6*
    k0(40,35,41) -> 6*
    k0(15,31,41) -> 6*
    k0(39,41,10) -> 6*
    k0(32,41,18) -> 6*
    k0(17,35,38) -> 6*
    k0(41,19,9) -> 6*
    k0(31,17,19) -> 6*
    k0(30,30,32) -> 6*
    k0(30,19,18) -> 6*
    k0(40,17,38) -> 6*
    k0(9,41,15) -> 6*
    k0(34,30,31) -> 6*
    k0(19,39,35) -> 6*
    k0(18,41,34) -> 6*
    k0(32,34,29) -> 6*
    k0(17,32,19) -> 6*
    k0(41,38,18) -> 6*
    k0(6,6,30) -> 6*
    k0(31,10,30) -> 6*
    f1(40) -> 6,9*,7
    f1(35) -> 6,9*,7
    f1(30) -> 7,6,9*
    f1(20) -> 7*
    f1(15) -> 6,9*
    f1(10) -> 7,6,9*
    f1(37) -> 7*
    f1(32) -> 6,7,9*
    f1(22) -> 7*
    f1(17) -> 6,9*
    f1(12) -> 7*
    f1(39) -> 6,9*
    f1(34) -> 6,9*,7
    f1(29) -> 6,9*
    f1(24) -> 7*
    f1(19) -> 6,9*,7
    f1(14) -> 7*
    f1(9) -> 6,9*
    f1(41) -> 6,9*,7
    f1(31) -> 6,9*
    f1(6) -> 9*,6,7
    f1(38) -> 6,9*
    f1(33) -> 7*
    f1(18) -> 6,9*,7
    f1(8) -> 7*
    h1(40) -> 6*
    h1(35) -> 10*,8,6
    h1(30) -> 8,6,10*
    h1(15) -> 8,10*,6
    h1(10) -> 6*
    h1(32) -> 6*
    h1(17) -> 8,10*,6
    h1(7) -> 8*
    h1(39) -> 8,10*,6
    h1(34) -> 6*
    h1(29) -> 8,10*,6
    h1(19) -> 6*
    h1(9) -> 10*,8,6
    h1(41) -> 6*
    h1(31) -> 6,10*,8
    h1(16) -> 8*
    h1(6) -> 6*
    h1(38) -> 10*,8,6
    h1(28) -> 8*
    h1(18) -> 6*
    g1(40) -> 6*
    g1(35) -> 6*
    g1(30) -> 6*
    g1(20) -> 6*
    g1(10) -> 6*
    g1(32) -> 6*
    g1(34) -> 6*
    g1(19) -> 6*
    g1(41) -> 6*
    g1(33) -> 6*
    g1(18) -> 6*
    g1(8) -> 6*
    a1() -> 9*,6,7
    g2(40) -> 6,10*
    g2(35) -> 6,10*
    g2(30) -> 6,10*
    g2(20) -> 6*
    g2(15) -> 6,10*
    g2(10) -> 6,10*
    g2(32) -> 6,10*
    g2(17) -> 6,10*
    g2(12) -> 9*
    g2(39) -> 6,10*
    g2(34) -> 6,30*
    g2(29) -> 6,10*
    g2(24) -> 10*
    g2(19) -> 9,30*,6
    g2(14) -> 6*
    g2(9) -> 6,10*
    g2(41) -> 6,10*
    g2(31) -> 6,10*
    g2(6) -> 6,10*
    g2(38) -> 6,10*
    g2(33) -> 6,10*
    g2(18) -> 10*,6
    h2(35) -> 10,6,8,18*,14
    h2(15) -> 10,18*,6,8,14
    h2(17) -> 10,19*,6,8,12
    h2(39) -> 10,6,8,32*,24,14
    h2(29) -> 10,6,8,19*,12
    h2(31) -> 10,14,8,6,32*,24
    h2(16) -> 20*,8,14
    h2(11) -> 12*
    h2(38) -> 10,6,8,18*,14
    h2(28) -> 33*,8,24
    h2(23) -> 24*
    h2(13) -> 14*
    f2(40) -> 9,7,6,15*
    f2(35) -> 9,7,6,15*
    f2(30) -> 9,7,6,15*
    f2(20) -> 7,16*
    f2(15) -> 9,6,15*
    f2(10) -> 9,7,15*,6,13
    f2(37) -> 16*,7,13
    f2(32) -> 9,7,6,15*
    f2(22) -> 7,15*
    f2(17) -> 9,6,15*
    f2(12) -> 28*,7,23
    f2(39) -> 9,6,15*
    f2(34) -> 9,7,6,31*
    f2(29) -> 9,6,15*
    f2(24) -> 16*,7,13
    f2(19) -> 15,9,31*,7,6
    f2(14) -> 16*,7,13
    f2(9) -> 9,15*,6,13
    f2(41) -> 9,7,6,15*
    f2(31) -> 9,6,15*
    f2(6) -> 9,15*,7,6,13
    f2(38) -> 9,6,15*
    f2(33) -> 7,16*
    f2(18) -> 9,7,6,15*
    f2(8) -> 16*,7,13
    a2() -> 9,17*,7,6,11
    g3(40) -> 10,6,18*
    g3(37) -> 18*
    g3(22) -> 15*
    g3(34) -> 15,30,35*,6
    g3(41) -> 10,6,18*
    h3(39) -> 10,32,40*,14,24,8,6,37
    h3(29) -> 10,19,34*,12,8,6,22
    h3(36) -> 37*
    h3(21) -> 22*
    h3(38) -> 10,18,41*,14,8,6,37
    a3() -> 9,17,29*,11,6,7,21
    f3(22) -> 15,38*,7,36
    f3(34) -> 31,9,39*,6,7,36
  problem:
   
  Qed