// 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'b11111100101111100000111111011011", c "32'b11010011001000011101111100000100"), (c "32'b11001111110111111110111011011111", c "32'b00101001100111000011000011010111", c "32'b00001111000000110000010001101100"))
      , ((c "32'b01111110000000110111101101000011", c "32'b11110110011011010000100000111011"), (c "32'b01110100011100001000001101111110", c "32'b10000111100101100111001100001000", c "32'b00000100001011101000000001110001"))
      , ((c "32'b11001110010010000010101001110000", c "32'b01100110101101111100011101101000"), (c "32'b00110100111111111111000111011000", c "32'b01100111100100000110001100001000", c "32'b11011100010111100100110110000000"))
      , ((c "32'b11101100000111101101101000000100", c "32'b01000110010110100011001010101001"), (c "32'b00110010011110010000110010101101", c "32'b10100101110001001010011101011011", c "32'b10100100010110101011010010100100"))
      , ((c "32'b01100001111110001001010001100111", c "32'b00000000110110001111101100000110"), (c "32'b01100010110100011000111101101101", c "32'b01100001000111111001100101100001", c "32'b00111100001111000111011101101010"))
      , ((c "32'b00110000111000101101100010001100", c "32'b00010000111010100011000111001101"), (c "32'b01000001110011010000101001011001", c "32'b00011111111110001010011010111111", c "32'b01000001000100100011010000011100"))
      , ((c "32'b01001011111100011011001111111101", c "32'b00100001001001001101110010001011"), (c "32'b01101101000101101001000010001000", c "32'b00101010110011001101011101110010", c "32'b11011111011111100010011001011111"))
      , ((c "32'b10010110100010000101011001010110", c "32'b01100000101010001100010111001010"), (c "32'b11110111001100010001110000100000", c "32'b00110101110111111001000010001100", c "32'b10011010011101000100110111011100"))
      , ((c "32'b11000010101110101100100001010110", c "32'b11100101101010010011011001111100"), (c "32'b10101000011000111111111011010010", c "32'b11011101000100011001000111011010", c "32'b11100111100000010010110110101000"))
      , ((c "32'b10001011000100001011010011110010", c "32'b11110000000100001101010100001111"), (c "32'b01111011001000011000101000000001", c "32'b10011010111111111101111111100011", c "32'b00111011101001111111010000101110"))
      ];