  We establish various complexity results for the entailment problem between
formulas in Separation Logic with user-defined predicates denoting recursive
data structures. The considered fragments are characterized by syntactic
conditions on the inductive rules that define the semantics of the predicates.
We focus on so-called P-rules, which are similar to (but simpler than) the PCE
rules introduced by Iosif et al. in 2013. In particular, for a specific
fragment where predicates are defined by so-called loc-deterministic inductive
rules, we devise a sound and complete cyclic proof procedure running in
polynomial time. Several complexity lower bounds are provided, showing that any
relaxing of the provided conditions makes the problem intractable.
