p cnf 1 1
1 0

c def real 1 a / b < 3
c def real 1 a > 0
c def real 1 b > 0
c def real 1 a < 5
c def real 1 b < 5