// Automatically generated by SBV. Do not edit!
let ForteTest =
   let c s = val [_, r] = str_split s "'" in map (\s. s == "1") (explode (string_tl r))
   in [ ((c "32'b00000110110101111001111111011000", c "32'b10010110100101100010010100001000"), (c "32'b10011101011011011100010011100000", c "32'b01110000010000010111101011010000", c "32'b10011001011001110011011011000000"))
      , ((c "32'b11110011110111000110111110011000", c "32'b11110111011010101101101101101011"), (c "32'b11101011010001110100101100000011", c "32'b11111100011100011001010000101101", c "32'b01011101100010011010110010001000"))
      , ((c "32'b10110100010100111000001110010110", c "32'b10001111001100111000110110011100"), (c "32'b01000011100001110001000100110010", c "32'b00100101000111111111010111111010", c "32'b11100011001111111100110101101000"))
      , ((c "32'b11011110100100001101101101111111", c "32'b11100000000101111111011010011111"), (c "32'b10111110101010001101001000011110", c "32'b11111110011110001110010011100000", c "32'b01000111010011010101110111100001"))
      , ((c "32'b11100111010100010000110010110111", c "32'b01011110100011101111110101101101"), (c "32'b01000101111000000000101000100100", c "32'b10001000110000100000111101001010", c "32'b11010110100101010100010011101011"))
      , ((c "32'b10011000010001111111110101101000", c "32'b00011110011001110001101100111001"), (c "32'b10110110101011110001100010100001", c "32'b01111001111000001110001000101111", c "32'b10100100100110010110010000101000"))
      , ((c "32'b00111100101110100101011100110111", c "32'b10111001101000101110101100011001"), (c "32'b11110110010111010100001001010000", c "32'b10000011000101110110110000011110", c "32'b11101100000100000000000101011111"))
      , ((c "32'b01101110111011011100011001110100", c "32'b00110011101001010000110101101001"), (c "32'b10100010100100101101001111011101", c "32'b00111011010010001011100100001011", c "32'b10010111010111100100100110010100"))
      , ((c "32'b01001111010101110110011001000111", c "32'b00000000010110000010001001101110"), (c "32'b01001111101011111000100010110101", c "32'b01001110111111110100001111011001", c "32'b11011011100010110110000010000010"))
      , ((c "32'b10100010010000001011111001010000", c "32'b00100100111111110010110011011000"), (c "32'b11000111001111111110101100101000", c "32'b01111101010000011001000101111000", c "32'b11011001000001100101001110000000"))
      ];