+v1@E,v2,v1:F,(v3) || (!v2);E,v3,v1:F,(!v3) || (v2)/v2@E,v1,v2:F,(!v1 && !v3);E,v3,v2:F,(v1 && v3)
v1@E,v2,v1:F,(v3) || (!v2)/v2@F,(v1 && !v3)
+v1@E,v3,v1:F,(!v3) || (v2)/v2@E,v3,v2:F,(v1 && v3)
