Yes, the cut is confusing.
+ does use a cut, but the cut is executed within the definition of + and will prune away the second clause of +. It does not affect the clauses calling + :
+(P) :- P,!,fail.
+(_). % <--- pruned away by cut
For your example member(A, [1,2,3]), + (A = 2), A = 3, this happens: 1) the first call to + will be +(1=2) and the cut is not executed, 1=3 fails, 2) we backtrack to member, then for +(2=2), the call 2=2 succeeds and the cut is called, meaning that +(2=2) fails and 3) we backtrack to member and then get the final candidate A=3 from member for which all calls succeed.
Note, If in foo you use the dif/2 predicate instead of + you will get more natural behaviour. E.g., with foo(A,B) :- dif(A,B), A=1, B=2. you will get the solution you expected.
Indeed, in contrast to + or \=, dif is declarative and not binding sensitive (i.e., dif(X,a), X=b is equivalent to X=b, dif(X,a)).
Yes, the cut is confusing. + does use a cut, but the cut is executed within the definition of + and will prune away the second clause of +. It does not affect the clauses calling + : +(P) :- P,!,fail. +(_). % <--- pruned away by cut
For your example member(A, [1,2,3]), + (A = 2), A = 3, this happens: 1) the first call to + will be +(1=2) and the cut is not executed, 1=3 fails, 2) we backtrack to member, then for +(2=2), the call 2=2 succeeds and the cut is called, meaning that +(2=2) fails and 3) we backtrack to member and then get the final candidate A=3 from member for which all calls succeed.
Note, If in foo you use the dif/2 predicate instead of + you will get more natural behaviour. E.g., with foo(A,B) :- dif(A,B), A=1, B=2. you will get the solution you expected. Indeed, in contrast to + or \=, dif is declarative and not binding sensitive (i.e., dif(X,a), X=b is equivalent to X=b, dif(X,a)).