Original classical TFL constraint search
Premises: P -> (Q or R); P. Conclusion: Q.
Countervaluation target: both premises T, conclusion F.
Forced: P=T, Q=F; then Q or R must be T.
Rejected trial: R=F makes Q or R=F and the first premise F.
Successful trial: R=T.
Full check: P=T,Q=F,R=T; first premise T, second premise T, conclusion F.
Modified argument: add not Q, conclude R.
Target R=F, not Q=T forces Q=F; P=T forces Q or R=T. Contradiction: Q or R=F. These values are forced, so no countervaluation remains.

Genuine branching example: premise (P or Q) and not(P and Q), conclusion R.
Target R=F; P or Q=T and P and Q=F.
P=T branch forces Q=F, success. P=F branch forces Q=T, success.
Full rows with R=F: TT premise F; TF premise T; FT premise T; FF premise F.