p cnf 11 8
-1 -2 -3 -4 5 0
-1 -2 -3 4 -5 0
6 0
7 0
8 0
9 0
10 0
11 0

c def real 1 b - e = 0
c def real 2 a - d = 0
c def real 3 c - f = 0
c def real 4 b * c - a = 0
c def real 5 e * f - d = 0
c def real 6 a >= 0
c def real 7 b >= 0
c def real 8 c >= 0
c def real 9 d >= 0
c def real 10 e >= 0
c def real 11 f >= 0