Greater Than Sudoku

I've found this on http://www.killersudokuonline.com:

It can be solved easily with Z3. I've took the same piece of code I used for usual Sudoku ( https://github.com/DennisYurichev/SAT_SMT_article/blob/master/SMT/sudoku2.py, PDF file: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf ) and added this:

...

"""
Subsquares:

------------------------------
|          |
1,1     | 1,2      | 1,3
|          |
------------------------------
|          |
2,1     | 2,2      | 2,3
|          |
------------------------------
|          |
3,1     | 3,2      | 3,3
|          |
------------------------------
"""

# from http://www.killersudokuonline.com/puzzles/2017/puzzle-GD4hzi164344.pdf

# subsquare 1,1:

# subsquare 1,3:

# subsquare 2,1:

# subsquare 3,2:

# subsquare 3,3:

...


The puzzle marked as "Outrageous" (for humans?), however it took ~30s on my old Intel Xeon E3-1220 3.10GHz to solve it:

7 3 4 6 9 2 5 1 8
2 1 5 8 3 7 9 4 6
6 8 9 5 1 4 7 2 3
1 7 3 2 8 9 6 5 4
5 4 6 1 7 3 2 8 9
9 2 8 4 5 6 1 3 7
8 6 7 3 2 1 4 9 5
4 5 2 9 6 8 3 7 1
3 9 1 7 4 5 8 6 2