L1 m0 conv K: u3 = -u2 for s0 = 0..164 : ALL HOLD  (1.1s)
L1 m0 conv O: u4 = u3 for s0 = 0..1316 : ALL HOLD  (14.4s)
L2 m0 conv K: u4 = u2 for s0 = 0..1316 : ALL HOLD  (24.6s)
L2 m1 conv K: u4 = u2 for s0 = 0..1316 : ALL HOLD  (34.8s)
control L1 K u3 = +u2 (must fail): [0, 1, 2, 3]
control L2 O u4 = u2 (must fail): [0, 1, 2, 3]
control wrong modulus t^4-2t^2+1/3, u3 = -u2 (must be False): False
