  The Triguarded Fragment (TGF) is among the most expressive decidable
fragments of first-order logic, subsuming both its two-variable and guarded
fragments without equality. We show that the TGF has the finite model property
(providing a tight doubly exponential bound on the model size) and hence finite
satisfiability coincides with satisfiability known to be N2ExpTime-complete.
Using similar constructions, we also establish 2ExpTime-completeness for finite
satisfiability of the constant-free (tri)guarded fragment with transitive
guards.
