{ grid: satisfiable }
conj (
@ c -<>c,
@ c <>T,
@ c [][] down x @ c <> x,
@ c [] down x [] down x1 @ x [] down x2 @ x [] down x3
disj (
@ x1 x2,
@ x1 x3,
@ x2 x3
),
@ c [] down x [][] down x1
@ x [][] down x2
@ x [][] down x3
@ x [][] down x4
disj (
@ x1 x2,
@ x1 x3,
@ x1 x4,
@ x2 x3,
@ x2 x4,
@ x3 x4
)
)