Automating Free Logic in HOL, with an Experimental Application in Category Theory Academic Article