<> <> (TestB N (inv1 N) (inv2 N))