(benchmark thm2_WD :logic LRM :extrasorts ((OBJECT 0)) :extrafuns ((root OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((joinRelations2 (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) (joinRelations2 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :extrafuns ((relImage19 (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 (relImage19 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse21 (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) (relConverse21 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation22 (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) (pfun2Relation22 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse20 ((x (Map OBJECT OBJECT))) (relConverse21 (pfun2Relation22 x)))) :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 (joinRelations2 r (tcl r)) )))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "tcl∈objrel → objrel" :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 "objrel=OBJECT ↔ OBJECT" :assumption true :notes "objfn⊆objrel" :assumption true :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 (joinRelations2 r t) t)) (subset (tcl r) t))) :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 (joinRelations2 r (tcl r)) (tcl r)))) :notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒t∈dom(tcl)∧tcl∈ℙ(OBJECT × OBJECT) ⇸ ℙ(OBJECT × OBJECT)" :formula (not (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var18 OBJECT)) (implies (in var18 (domain t)) (not (= var18 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage19 (pfunConverse20 t) s)) (= s (as emptySet (Set OBJECT)))))) (and true true)))) )