The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.

@article{KourtisP16,
  title = {Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting},
  author = {Georgios Kourtis and Ian Pratt-Hartmann},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 4},
  year = {2017},
  doi = {10.23638/lmcs-13(4:4)2017}
}