(benchmark writefile_grd3_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 ((xbw 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 ((directories (Set OBJECT))) :extrafuns ((rbw PERMISSION)) :extrafuns ((|obj_owner| (Map OBJECT USER))) :extrafuns ((|user_grps| (Set ((ind Tuple 2) USER GROUP)))) :extrafuns ((objects (Set OBJECT))) :extrafuns ((wbo PERMISSION)) :extrafuns ((rname NAME)) :extrafuns ((|user_pgrp| (Map USER GROUP))) :extrafuns ((|opened_files| (Set OBJECT))) :extrafuns ((admin GROUP)) :extrafuns ((f 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 ((usr USER)) :extrafuns ((|fcontent'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((xbo PERMISSION)) :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))))) :notes "objects∈ℙ(OBJECT)" :assumption true :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 "∀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 ((var44 PERMISSION)) (= true (or (= var44 rbo) (= var44 wbo) (= var44 xbo) (= var44 rbg) (= var44 wbg) (= var44 xbg) (= var44 rbw) (= var44 wbw) (= var44 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 ((var47 OBJECT)) (implies (in var47 (domain t)) (not (= var47 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage10 (pfunConverse11 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var48 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var48 (tcl (pfun2Relation13 t))) (= ((ind project 2 1) var48) ((ind project 2 2) var48))) (in var48 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∅∈CONTENT" :assumption (forall ((var49 Int) (var50 DATA) (var51 DATA)) (implies (and (in ((ind tuple 2) var49 var50) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var49 var51) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var50 var51) (>= var49 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 "f∈opened_files" :assumption (in f |opened_files|) :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 "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 "∀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)) )