SomeFunnyRel(R1,R2,x,y) = (forall x y z . (R1(x,y) & R1(y,z) -> R1(x,z))) & (forall p q . R2(p,q) -> R1(p,q)) & (forall Q . ((forall a b c . (Q(a,b) & Q(b,c) -> Q(a,c))) & (forall m n . R2(m,n) -> Q(m,n)) -> (forall l g . R1(l,g) -> Q(l,g))))