Bounds for the computational complexity of major justification logics were found in papers by Buss, N. Krupski, Kuznets, and Milnikel: logics J, J4, JT, LP and JD, were established to be Σp2 -complete. A corresponding lower bound is also known for JD4, the system that includes the consistency axiom and positive introspection. However, no upper bound has been established so far for this logic. Here, the missing upper bound for the complexity of JD4 is established through an alternating algorithm. It is shown that using Fitting models of only two worlds is adequate to describe JD4; this helps to produce an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.