(benchmark thm1_WD :logic LRM :extrasorts ((OBJECT 0)) :extrafuns ((root OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((joinRelations13 (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) (joinRelations13 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 "tcl∈objrel → objrel" :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 (joinRelations13 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 (joinRelations13 r (tcl r)) (tcl r)))) :notes "∀r·r∈objrel⇒r∈dom(tcl)∧tcl∈ℙ(OBJECT × OBJECT) ⇸ ℙ(OBJECT × OBJECT)∧r∈dom(tcl)∧tcl∈ℙ(OBJECT × OBJECT) ⇸ ℙ(OBJECT × OBJECT)" :formula (not (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (and true true true true)))) )