// 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'b10010110100101100010010100001000", c "32'b11110011110111000110111110011000"), (c "32'b10001010011100101001010010100000", c "32'b10100010101110011011010101110000", c "32'b11101110000101000111010011000000"))
      , ((c "32'b10110100010100111000001110010110", c "32'b10001111001100111000110110011100"), (c "32'b01000011100001110001000100110010", c "32'b00100101000111111111010111111010", c "32'b11100011001111111100110101101000"))
      , ((c "32'b11100000000101111111011010011111", c "32'b11100111010100010000110010110111"), (c "32'b11000111011010010000001101010110", c "32'b11111000110001101110100111101000", c "32'b11010001111111111011111110101001"))
      , ((c "32'b10011000010001111111110101101000", c "32'b00011110011001110001101100111001"), (c "32'b10110110101011110001100010100001", c "32'b01111001111000001110001000101111", c "32'b10100100100110010110010000101000"))
      , ((c "32'b10111001101000101110101100011001", c "32'b01101110111011011100011001110100"), (c "32'b00101000100100001011000110001101", c "32'b01001010101101010010010010100101", c "32'b10000011110011001101110101010100"))
      , ((c "32'b01001111010101110110011001000111", c "32'b00000000010110000010001001101110"), (c "32'b01001111101011111000100010110101", c "32'b01001110111111110100001111011001", c "32'b11011011100010110110000010000010"))
      , ((c "32'b00100100111111110010110011011000", c "32'b01000110011011101011011101100111"), (c "32'b01101011011011011110010000111111", c "32'b11011110100100000111010101110001", c "32'b10100000100010010111001011101000"))
      , ((c "32'b00001000001101100011110100010100", c "32'b11011100111111100100001001010011"), (c "32'b11100101001101000111111101100111", c "32'b00101011001101111111101011000001", c "32'b01101111001011001111010101111100"))
      , ((c "32'b11101110111110101100100101110101", c "32'b01000101101110011100111011001101"), (c "32'b00110100101101001001100001000010", c "32'b10101001010000001111101010101000", c "32'b01001011011111000111100010110001"))
      , ((c "32'b00101110111000110100110110000001", c "32'b11011010101111010000100110010100"), (c "32'b00001001101000000101011100010101", c "32'b01010100001001100100001111101101", c "32'b00101011010111110101011110010100"))
      ];