(benchmark axm5_WD :logic LRM :extrasorts ((GROUP 0)) :extrasorts ((PERMISSION 0)) :extrasorts ((USER 0)) :extrasorts ((OBJECT 0)) :extrafuns ((xbg PERMISSION)) :extrafuns ((admin GROUP)) :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 ((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 ((xbw PERMISSION)) :extrafuns ((xbo PERMISSION)) :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 ((rbg PERMISSION)) :extrafuns ((wbw PERMISSION)) :extrafuns ((rbw PERMISSION)) :extrafuns ((wbo PERMISSION)) :extrafuns ((relImage11 (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 (relImage11 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse13 (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) (relConverse13 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation14 (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) (pfun2Relation14 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse12 ((x (Map OBJECT OBJECT))) (relConverse13 (pfun2Relation14 x)))) :extrafuns ((joinRelations31 (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) (joinRelations31 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :extrafuns ((pfun2Relation72 (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) (pfun2Relation72 f)) (and (in a (domain f)) (= b (apply f a))))) :notes "PERMISSION={rbo,wbo,xbo,rbg,wbg,xbg,rbw,wbw,xbw}" :assumption (forall ((var0 PERMISSION)) (= true (or (= var0 rbo) (= var0 wbo) (= var0 xbo) (= var0 rbg) (= var0 wbg) (= var0 xbg) (= var0 rbw) (= var0 wbw) (= var0 xbw)))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "WPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅" :assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var10 OBJECT)) (implies (in var10 (domain t)) (not (= var10 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage11 (pfunConverse12 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var15 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var15 (tcl (pfun2Relation14 t))) (= ((ind project 2 1) var15) ((ind project 2 2) var15))) (in var15 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "objrel=OBJECT ↔ OBJECT" :assumption true :notes "objfn⊆objrel" :assumption true :notes "XPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :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 (joinRelations31 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 "∀r·r∈objrel⇒tcl(r)=r∪(r;tcl(r))" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (= (tcl r) (union r (joinRelations31 r (tcl r)) )))) :notes "tcl∈objrel → objrel" :assumption true :notes "RPerm∈(OBJECT ↔ PERMISSION) × (OBJECT ⇸ USER) × (OBJECT ⇸ GROUP) × (USER ↔ GROUP) → (OBJECT ↔ USER)" :assumption true :notes "⊤" :assumption true :notes "∀r·r∈objrel⇒r⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset r (tcl r)))) :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 (joinRelations31 r t) t)) (subset (tcl r) t))) :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)⇒p ↦ s ↦ g ↦ m∈dom(WPerm)∧WPerm∈ℙ(OBJECT × PERMISSION) × ℙ(OBJECT × USER) × ℙ(OBJECT × GROUP) × ℙ(USER × GROUP) ⇸ ℙ(OBJECT × USER)∧((o ↦ u∈s∧o ↦ wbo∈p)∨(o∈dom(g)∧g∈OBJECT ⇸ GROUP))" :formula (not (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))) (and true true (or (and (in ((ind tuple 2) o u) (pfun2Relation72 s)) (in ((ind tuple 2) o wbo) p)) (and (in o (domain g)) true)))))) )