Enlarging the class of tractable SAT problems is a relevant topic because of the repercussions in both practical applications and theoretical grounds. In this paper, it is proved that some non-clausal Horn- like formulas can be solved in linear time. In addition to its theoretical importance, this result has a special practical interest because Knowledge Based Systems could benefit of it due to the Horn-like structure of the formulas. In order to prove such linearity a correct refutational calculi is first provided and second, a linear algorithm is described.