(benchmark close_inv3_INV :logic LRM :extrasorts ((NAME 0)) :extrasorts ((DATA 0)) :extrasorts ((OBJECT 0)) :extrafuns ((parent (Map OBJECT OBJECT))) :extrafuns ((root OBJECT)) :extrafuns ((f OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((fcontent (Map OBJECT (Map Int DATA)))) :extrafuns ((fbuffer (Map OBJECT (Map Int DATA)))) :extrafuns ((|opened_files'| (Set OBJECT))) :extrafuns ((|fbuffer'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA)))))) :extrafuns ((directories (Set OBJECT))) :extrafuns ((files (Set OBJECT))) :extrafuns ((objects (Set OBJECT))) :extrafuns ((rname NAME)) :extrafuns ((|opened_files| (Set OBJECT))) :extrafuns ((relImage2 (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 (relImage2 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse4 (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) (relConverse4 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation5 (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) (pfun2Relation5 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse3 ((x (Map OBJECT OBJECT))) (relConverse4 (pfun2Relation5 x)))) :extrafuns ((joinRelations16 (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) (joinRelations16 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "objects∈ℙ(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 ((var1 OBJECT)) (implies (in var1 (domain t)) (not (= var1 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var6 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var6 (tcl (pfun2Relation5 t))) (= ((ind project 2 1) var6) ((ind project 2 2) var6))) (in var6 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∅∈CONTENT" :assumption (forall ((var7 Int) (var8 DATA) (var9 DATA)) (implies (and (in ((ind tuple 2) var7 var8) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var7 var9) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var8 var9) (>= var7 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 (relImage2 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage2 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))) (= (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert x (as emptySet (Set OBJECT)))) (as emptySet (Set OBJECT))))) :notes "objrel=OBJECT ↔ OBJECT" :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 "∀s·s⊆parent∼[s]⇒s=∅" :assumption (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 parent) s)) (= s (as emptySet (Set OBJECT))))) :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 (joinRelations16 (joinRelations16 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) )) true)) :notes "opened_files⊆files" :assumption (subset |opened_files| files) :notes "tcl∈objrel → objrel" :assumption true :notes "directories⊆objects" :assumption (subset directories objects) :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 "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 "files⊆objects" :assumption (subset files objects) :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 (relImage2 (pfunConverse3 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage2 (pfunConverse3 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage2 (relConverse4 (union (pfun2Relation5 f) (pfun2Relation5 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT))))))) :notes "CONTENT=ℕ ⇸ DATA" :assumption true :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 ((var26 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var26 (tcl (pfun2Relation5 parent))) (= ((ind project 2 1) var26) ((ind project 2 2) var26))) (in var26 (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 (relImage2 (pfunConverse3 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation5 g) (joinRelations16 (joinRelations16 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage2 (pfunConverse3 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 "∀T·root∈T∧parent∼[T]⊆T⇒objects⊆T" :assumption (forall ((T (Set OBJECT))) (implies (and (in root T) (subset (relImage2 (pfunConverse3 parent) T) T)) (subset objects T))) :notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations16 r (tcl r)) (tcl r)))) :notes "∀x,s·s⊆((tcl(parent))∼[{x}] ◁ parent)∼[s]⇒s=∅" :assumption (forall ((x OBJECT)(s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 (restrict parent (relImage2 (relConverse4 (tcl (pfun2Relation5 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 (joinRelations16 r (tcl r)) )))) :notes "tcl(∅)=∅" :assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) :notes "rname∈NAME" :assumption true :notes "objects ∖ {root}⊆(tcl(parent))∼[{root}]" :assumption (subset (setminus objects (insert root (as emptySet (Set OBJECT)))) (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert root (as emptySet (Set OBJECT))))) :notes "files∩directories=∅" :assumption (= (inter files directories) (as emptySet (Set OBJECT))) :notes "root∈directories" :assumption (in root directories) :notes "⊤" :assumption true :notes "objects⊆{root}∪(tcl(parent))∼[{root}]" :assumption (subset objects (union (insert root (as emptySet (Set OBJECT))) (relImage2 (relConverse4 (tcl (pfun2Relation5 parent))) (insert root (as emptySet (Set OBJECT)))))) :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 (joinRelations16 r t) t)) (subset (tcl r) t))) :notes "ran(parent)⊆directories" :assumption (subset (range parent) directories) :notes "{f} ⩤ fbuffer∈opened_files ∖ {f} → CONTENT" :formula (not false) )