p cnf 0 0
1 0

c def real 1 x * y > 1
c def real 1 x * y < 0