module fs sig File {} sig Dir { contents: set File + Dir } one sig Root extends Dir {} fact { File + Dir in Root.*contents all d: Dir | not d in d.^contents } run { not lone File and not lone Dir } for 2 File, 2 Dir run { some File and some Dir } for 2 File, 3 Dir // Remove comments to get the unsat core. /* fact { all f: File | one contents.f all d: Dir | one contents.d } */