Е. Качко and Д. Телевный, “A study of the applicability of the SMT/SAT-based theorem proves for Keccak hash functions cryptanalysis”, RT, vol. 2, no. 189, pp. 75–80, Jun. 2017.