An ILP-based proof that 1-tough 4-regular graphs of at most 17 nodes are Hamiltonian