fixed interpreter and tested
Fixed interpreter
fixed negative input value for k
Output of counterexample with original instead of internal name
Adjusted log levels