import adversary
import sys
prover = adversary.Prover(
"= (ham x) k", "= (ham y) (+ k 1)", "= ham (^ x y) p").hint_symmetric()
bounds = prover.find_bounds(int(sys.argv[1]), 5, 8)