(benchmark mkdir_grd5_WD
:logic LRM

:extrasorts ((NAME 0))
:extrasorts ((DATA 0))
:extrasorts ((USER 0))
:extrasorts ((OBJECT 0))
:extrasorts ((GROUP 0))
:extrasorts ((PERMISSION 0))
:extrafuns ((xbg PERMISSION))
:extrafuns ((parent (Map OBJECT OBJECT)))
:extrafuns ((wbg PERMISSION))
:extrafuns ((WPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER))))
:extrafuns ((root OBJECT))
:extrafuns ((users (Set USER)))
:extrafuns ((fcontent (Map OBJECT (Map Int DATA))))
:extrafuns ((groups (Set GROUP)))
:extrafuns ((fbuffer (Map OBJECT (Map Int DATA))))
:extrafuns ((|obj_grp'| (Set ((ind Tuple 2) OBJECT GROUP))))
:extrafuns ((xbw PERMISSION))
:extrafuns ((|directories'| (Set OBJECT)))
:extrafuns ((grp GROUP))
:extrafuns ((su USER))
:extrafuns ((XPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER))))
:extrafuns ((obj OBJECT))
:extrafuns ((directories (Set OBJECT)))
:extrafuns ((rbg PERMISSION))
:extrafuns ((indr OBJECT))
:extrafuns ((rbw PERMISSION))
:extrafuns ((|obj_owner| (Map OBJECT USER)))
:extrafuns ((|user_grps| (Set ((ind Tuple 2) USER GROUP))))
:extrafuns ((objects (Set OBJECT)))
:extrafuns ((|obj_perms'| (Set ((ind Tuple 2) OBJECT PERMISSION))))
:extrafuns ((wbo PERMISSION))
:extrafuns ((|user_pgrp| (Map USER GROUP)))
:extrafuns ((|opened_files| (Set OBJECT)))
:extrafuns ((rname NAME))
:extrafuns ((admin GROUP))
:extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((rbo PERMISSION))
:extrafuns ((RPerm ((ind Tuple 2) ((ind Tuple 2) ((ind Tuple 2) (Set ((ind Tuple 2) OBJECT PERMISSION)) (Map OBJECT USER)) (Map OBJECT GROUP)) (Set ((ind Tuple 2) USER GROUP))) (Set ((ind Tuple 2) OBJECT USER))))
:extrafuns ((usr USER))
:extrafuns ((|obj_owner'| (Set ((ind Tuple 2) OBJECT USER))))
:extrafuns ((xbo PERMISSION))
:extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((files (Set OBJECT)))
:extrafuns ((wbw PERMISSION))
:extrafuns ((|obj_perms| (Set ((ind Tuple 2) OBJECT PERMISSION))))
:extrafuns ((|obj_grp| (Map OBJECT GROUP)))
:extrafuns ((relImage10 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set OBJECT) (Set OBJECT)))
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT))) (s (Set OBJECT)) (b OBJECT)) (= (in b (relImage10 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r)))))
:extrafuns ((relConverse12 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:assumption (forall ((f (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) b a) (relConverse12 f)) (in ((ind tuple 2) a b) f)))
:extrafuns ((pfun2Relation13 (Map OBJECT OBJECT) (Set ((ind Tuple 2) OBJECT OBJECT))))
:assumption (forall ((f (Map OBJECT OBJECT)) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) a b) (pfun2Relation13 f)) (and (in a (domain f)) (= b (apply f a)))))
:extrafuns ((pfunConverse11 ((x (Map OBJECT OBJECT))) (relConverse12 (pfun2Relation13 x))))
:extrafuns ((pfun2Relation27 (Map OBJECT USER) (Set ((ind Tuple 2) OBJECT USER))))
:assumption (forall ((f (Map OBJECT USER)) (a OBJECT) (b USER)) (= (in ((ind tuple 2) a b) (pfun2Relation27 f)) (and (in a (domain f)) (= b (apply f a)))))
:extrafuns ((relImage28 (Set ((ind Tuple 2) USER GROUP)) (Set USER) (Set GROUP)))
:assumption (forall ((r (Set ((ind Tuple 2) USER GROUP))) (s (Set USER)) (b GROUP)) (= (in b (relImage28 r s)) (exists ((a USER)) (and (in a s) (in ((ind tuple 2) a b) r)))))
:extrafuns ((joinRelations34 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:assumption (forall ((r1 (Set ((ind Tuple 2) OBJECT OBJECT))) (r2 (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (c OBJECT)) (= (in ((ind tuple 2) a c) (joinRelations34 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2)))))
:extrafuns ((pfun2Relation42 (Map USER GROUP) (Set ((ind Tuple 2) USER GROUP))))
:assumption (forall ((f (Map USER GROUP)) (a USER) (b GROUP)) (= (in ((ind tuple 2) a b) (pfun2Relation42 f)) (and (in a (domain f)) (= b (apply f a)))))

:notes "objects∈ℙ(OBJECT)"
:assumption true

:notes "obj∈OBJECT ∖ (files∪directories)"
:assumption (not (or (in obj files) (in obj directories)))

:notes "WPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)"
:assumption true

:notes "∀s·s⊆parent∼[s]⇒s=∅"
:assumption (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 parent) s)) (= s (as emptySet (Set OBJECT)))))

:notes "opened_files⊆files"
:assumption (subset |opened_files| files)

:notes "admin∈GROUP"
:assumption true

:notes "user_pgrp∈users → groups"
:assumption true

:notes "tcl∈objrel → objrel"
:assumption true

:notes "objects=files∪directories"
:assumption (= objects (union files directories))

:notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M⇒f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N"
:assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M)) true))

:notes "obj_owner∈files∪directories → users"
:assumption true

:notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈XPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ xbo∈p)∨(g(o)∈m[{u}]∧o ↦ xbg∈p)∨o ↦ xbw∈p∨u=su)"
:assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (XPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation27 s)) (in ((ind tuple 2) o xbo) p)) (and (in (apply g o) (relImage28 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o xbg) p)) (in ((ind tuple 2) o xbw) p) (= u su)))))

:notes "root∈objects"
:assumption (in root objects)

:notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M∧(∀A·A⊆f∼[A]⇒A=∅)∧(∀B·B⊆g∼[B]⇒B=∅)∧f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N⇒(∀C·C⊆(f∪g∪{u ↦ x})∼[C]⇒C=∅)"
:assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M) (forall ((A (Set OBJECT))) (implies (subset A (relImage10 (pfunConverse11 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage10 (pfunConverse11 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage10 (relConverse12 (union (pfun2Relation13 f) (pfun2Relation13 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT)))))))

:notes "∀x·((tcl(parent))∼[{x}]∪{x}) ⩤ parent∈(objects ∖ ((tcl(parent))∼[{x}]∪{x})) ∖ {root} → objects ∖ ((tcl(parent))∼[{x}]∪{x})"
:assumption (forall ((x OBJECT)) true)

:notes "tcl(parent)∩(OBJECT ◁ id)=∅"
:assumption (forall ((var31 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var31 (tcl (pfun2Relation13 parent))) (= ((ind project 2 1) var31) ((ind project 2 2) var31))) (in var31 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT))))))

:notes "∀f,c,g,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧t∈M∧f∈M ∖ {t} → M∧(∀s·s⊆f∼[s]⇒s=∅)∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c∧g∈N ∖ {u} → N⇒(∀w·w⊆g∼[w]⇒w=∅)"
:assumption (forall ((f (Map OBJECT OBJECT))(c (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (in t M) false (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation13 g) (joinRelations34 (joinRelations34 (pfunConverse11 c) (pfun2Relation13 f)) (pfun2Relation13 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage10 (pfunConverse11 g) w)) (= w (as emptySet (Set OBJECT)))))))

:notes "objfn⊆objrel"
:assumption true

:notes "parent∈objects ∖ {root} → objects"
:assumption true

:notes "root∈OBJECT"
:assumption true

:notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations34 r (tcl r))  (tcl r))))

:notes "tcl(∅)=∅"
:assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT))))

:notes "user_grps∈users ↔ groups"
:assumption true

:notes "users⊆USER"
:assumption true

:notes "rname∈NAME"
:assumption true

:notes "files∩directories=∅"
:assumption (= (inter files directories) (as emptySet (Set OBJECT)))

:notes "⊤"
:assumption true

:notes "usr ↦ grp∈user_pgrp"
:assumption (in ((ind tuple 2) usr grp) (pfun2Relation42 |user_pgrp|))

:notes "∀r·r∈objrel⇒r⊆tcl(r)"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset r (tcl r))))

:notes "PERMISSION={rbo,wbo,xbo,rbg,wbg,xbg,rbw,wbw,xbw}"
:assumption (forall ((var45 PERMISSION)) (= true (or (= var45 rbo) (= var45 wbo) (= var45 xbo) (= var45 rbg) (= var45 wbg) (= var45 xbg) (= var45 rbw) (= var45 wbw) (= var45 xbw))))

:notes "obj_perms∈OBJECT ↔ PERMISSION"
:assumption true

:notes "objfn=OBJECT ∖ {root} ⇸ OBJECT"
:assumption true

:notes "fcontent∈files → CONTENT"
:assumption true

:notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅"
:assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var48 OBJECT)) (implies (in var48 (domain t)) (not (= var48 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var49 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var49 (tcl (pfun2Relation13 t))) (= ((ind project 2 1) var49) ((ind project 2 2) var49))) (in var49 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT))))))))

:notes "∅∈CONTENT"
:assumption (forall ((var50 Int) (var51 DATA) (var52 DATA)) (implies (and (in ((ind tuple 2) var50 var51) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var50 var52) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var51 var52) (>= var50 0))))

:notes "∀r,r2·r∈objrel∧r2∈objrel∧r2⊆r∧(∀s·s⊆r[s]⇒s=∅)⇒(∀t·t⊆r2[t]⇒t=∅)"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(r2 (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true true (subset r2 r) (forall ((s (Set OBJECT))) (implies (subset s (relImage10 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage10 r2 t)) (= t (as emptySet (Set OBJECT)))))))

:notes "∀x·x∉ran(parent)⇒(tcl(parent))∼[{x}]=∅"
:assumption (forall ((x OBJECT)) (implies (not (in x (range parent))) (= (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert x (as emptySet (Set OBJECT)))) (as emptySet (Set OBJECT)))))

:notes "objrel=OBJECT ↔ OBJECT"
:assumption true

:notes "obj_grp∈files∪directories → groups"
:assumption true

:notes "fbuffer∈opened_files → CONTENT"
:assumption true

:notes "∀x·(tcl(parent))∼[{x}] ◁ parent∈(tcl(parent))∼[{x}] → (tcl(parent))∼[{x}]∪{x}"
:assumption (forall ((x OBJECT)) true)

:notes "∀f,g,c,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c⇒g∈N ∖ {u} → N"
:assumption (forall ((f (Map OBJECT OBJECT))(g (Set ((ind Tuple 2) OBJECT OBJECT)))(c (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (= u (apply c t)) (= g (joinRelations34 (joinRelations34 (pfunConverse11 c) (pfun2Relation13 f)) (pfun2Relation13 c)) )) true))

:notes "directories⊆objects"
:assumption (subset directories objects)

:notes "∀x·(tcl(parent))∼[{x}] ◁ parent∈((tcl(parent))∼[{x}]∪{x}) ∖ {x} → (tcl(parent))∼[{x}]∪{x}"
:assumption (forall ((x OBJECT)) true)

:notes "usr∈users"
:assumption (in usr users)

:notes "indr∈directories"
:assumption (in indr directories)

:notes "files⊆objects"
:assumption (subset files objects)

:notes "CONTENT=ℕ ⇸ DATA"
:assumption true

:notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈RPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ rbo∈p)∨(g(o)∈m[{u}]∧o ↦ rbg∈p)∨o ↦ rbw∈p∨u=su)"
:assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (RPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation27 s)) (in ((ind tuple 2) o rbo) p)) (and (in (apply g o) (relImage28 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o rbg) p)) (in ((ind tuple 2) o rbw) p) (= u su)))))

:notes "XPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)"
:assumption true

:notes "∀T·root∈T∧parent∼[T]⊆T⇒objects⊆T"
:assumption (forall ((T (Set OBJECT))) (implies (and (in root T) (subset (relImage10 (pfunConverse11 parent) T) T)) (subset objects T)))

:notes "grp∈groups"
:assumption (in grp groups)

:notes "∀x,s·s⊆((tcl(parent))∼[{x}] ◁ parent)∼[s]⇒s=∅"
:assumption (forall ((x OBJECT)(s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 (restrict parent (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert x (as emptySet (Set OBJECT)))))) s)) (= s (as emptySet (Set OBJECT)))))

:notes "∀r·r∈objrel⇒tcl(r)=r∪(r;tcl(r))"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (= (tcl r) (union r (joinRelations34 r (tcl r)) ))))

:notes "∀o,u,p,s,g,m·o∈OBJECT∧u∈USER∧p∈OBJECT ↔ PERMISSION∧s∈OBJECT ⇸ USER∧g∈OBJECT ⇸ GROUP∧m∈USER ↔ GROUP∧o∈dom(g)⇒(o ↦ u∈WPerm(p ↦ s ↦ g ↦ m)⇔(o ↦ u∈s∧o ↦ wbo∈p)∨(g(o)∈m[{u}]∧o ↦ wbg∈p)∨o ↦ wbw∈p∨u=su)"
:assumption (forall ((o OBJECT)(u USER)(p (Set ((ind Tuple 2) OBJECT PERMISSION)))(s (Map OBJECT USER))(g (Map OBJECT GROUP))(m (Set ((ind Tuple 2) USER GROUP)))) (implies (and true true true true true true (in o (domain g))) (= (in ((ind tuple 2) o u) (WPerm ((ind tuple 2) ((ind tuple 2) ((ind tuple 2) p s) g) m))) (or (and (in ((ind tuple 2) o u) (pfun2Relation27 s)) (in ((ind tuple 2) o wbo) p)) (and (in (apply g o) (relImage28 m (insert u (as emptySet (Set USER))))) (in ((ind tuple 2) o wbg) p)) (in ((ind tuple 2) o wbw) p) (= u su)))))

:notes "objects ∖ {root}⊆(tcl(parent))∼[{root}]"
:assumption (subset (setminus objects (insert root (as emptySet (Set OBJECT)))) (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert root (as emptySet (Set OBJECT)))))

:notes "obj_perms∈files∪directories ↔ PERMISSION"
:assumption true

:notes "root∈directories"
:assumption (in root directories)

:notes "RPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)"
:assumption true

:notes "su∈USER"
:assumption true

:notes "objects⊆{root}∪(tcl(parent))∼[{root}]"
:assumption (subset objects (union (insert root (as emptySet (Set OBJECT))) (relImage10 (relConverse12 (tcl (pfun2Relation13 parent))) (insert root (as emptySet (Set OBJECT))))))

:notes "groups⊆GROUP"
:assumption true

:notes "∀u·u∈users⇒user_pgrp(u)∈user_grps[{u}]"
:assumption (forall ((u USER)) (implies (in u users) (in (apply |user_pgrp| u) (relImage28 |user_grps| (insert u (as emptySet (Set USER)))))))

:notes "∀r,t·r∈objrel∧r⊆t∧r;t⊆t⇒tcl(r)⊆t"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(t (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true (subset r t) (subset (joinRelations34 r t)  t)) (subset (tcl r) t)))

:notes "ran(parent)⊆directories"
:assumption (subset (range parent) directories)

:notes "obj_perms ↦ obj_owner ↦ obj_grp ↦ user_grps∈dom(WPerm)∧WPerm∈ℙ(OBJECT × PERMISSION) × ℙ(OBJECT × USER) × ℙ(OBJECT × GROUP) × ℙ(USER × GROUP) ⇸ ℙ(OBJECT × USER)"
:formula (not (and true true))

)