subsumes_term/2 incorrect

[UWN]

(using Playground)

?- subsumes_term(X, f(X)).
{ERROR: No handle found for thrown exception error(existence_error(procedure,'user:subsumes_term'/2),'user:subsumes_term'/2)}
% unexpected

aborted
?- use_module(library(terms_check),[subsumes_term/2]).
Note: module terms_check already in executable, just made visible
yes % should not be necessary 
?- subsumes_term(f(X,Y), f(Z,Z)).

yes
?- subsumes_term(f(Z,Z), f(X,Y)).

no
?- subsumes_term(g(X), g(f(X))).

yes, unexpected.
?- subsumes_term(X, f(X)).

yes, unexpected.

Note that the definition of subsumes_term/2 has two conditions a and b. Cor.2 since 2012-02-15, reported as #32 2016-10-26.

[UWN]

Also note that the documentation incorrectly states that Ciao checks for an instance. However,

?- subsumes_term(f(X,X),f(Y,X)).

yes, unexpected. % this is not even an instance
?- subsumes_term(f(Y,X),f(X,X)).

yes % ok, this is an instance

[UWN]

Currently, the following twelve implementations implement this correctly: B, ECLiPSe, GNU, Ichiban, SICStus, SWI, Scryer, Tau, Trealla, X, XSB, YAP.

[UWN]

Also note that the documentation neither agrees with Cor.2 nor does it agree with the current implementation, as it incorrectly reads:

subsumes_term(Term1,Term2) [ISO]
Term2 is an instance of Term1. % this is not ISO!

But here is what Ciao does:

?- subsumes_term(f(X,X,Y),f(Y,X,X)).

yes, unexpected.

This is neither an instance (as falsely documented) nor is it what ISO defines.

[UWN]

A shorter example:

?- subsumes_term(f(X,X),f(_,X)).

yes, unexpected