The answer is either ``the TRS is in 
CBN
 or
``the TRS is not in 
CBN
; in the latter case an 
``
-free-term''
i.e. a term with no 
-needed redex is shown.
The Call-by-need  command checks membership to 
CBN
 
but with the signature extended with a fresh constant symbol .
Indeed a TRS may be in 
CBN
 with the signature consiting of 
all the symbols appearing in its rules but not in 
CBN
 with 
the same signature extended by just one fresh symbol. The preservation of 
membership thru ``signature extension''
has been investigated in [5].
Note that the membership to 
CBN
 problem 
having a double exponential time complexity,
may run for a very long time for big TRS.
Use the Stop  button to stop the computation.