sat
((l0 (- 1))
 (l1 0)
 (l2 (- 5))
 (l3 (- 1)))
((u0 0)
 (u1 4)
 (u2 (- 4))
 (u3 7))
((x0r0 0)
 (x1r0 0)
 (x2r0 0)
 (x3r0 0))
((x0r1 (- 4))
 (x1r1 0)
 (x2r1 (- 4))
 (x3r1 8))
((x0r2 (/ (- 10) 3))
 (x1r2 (/ 1 3))
 (x2r2 (- 4))
 (x3r2 7))
((x0r3 (- 1))
 (x1r3 5)
 (x2r3 (- 11))
 (x3r3 7))
((x0r4 (- 1))
 (x1r4 4)
 (x2r4 (- 9))
 (x3r4 6))
((x0r5 3)
 (x1r5 4)
 (x2r5 (- 5))
 (x3r5 (- 2)))
((x0r6 (/ 7 3))
 (x1r6 (/ 11 3))
 (x2r6 (- 5))
 (x3r6 (- 1)))
((x0r7 0)
 (x1r7 (- 1))
 (x2r7 2)
 (x3r7 (- 1)))
((x0r8 0)
 (x1r8 0)
 (x2r8 0)
 (x3r8 0))
((x0 (- 1))
 (x1 2)
 (x2 (- 5))
 (x3 4))