Recently introduced Transformational Semantics (TS) formalizes, restraints and makes rigorous the transformational approach epitomized by QR and Transformational Grammars: deriving a meaning (in the form of a logical formula or a logical form) by a series of transformations from a suitably abstract (tecto-) form of a sentence. Unlike QR, each transformation in TS is rigorously and precisely defined, typed, and deterministic. The restraints of TS and the sparsity of the choice points (in the order of applying the deterministic transformation steps) help derive negative predictions and control over-generation. The rigorous nature of TS makes it easier to carry analyses mechanically, by a computer. We report on such a mechanical, fully automatic application of TS to a tree bank of FraCAS text entailment problems (generalized quantifier section). Set-theoretic logical formulas derived by TS as meanings for input sentences are submitted to an automatic first-order theorem prover to decide entailment. A characteristic feature of our approach is the exhaustive enumeration of quantifier and other such ambiguities. Overall TS proved just as capable as natural logic in inferences involving a variety of generalized quantifiers. Still open is the problem of mechanically dealing with bare plurals.