Input: Which ACL2 contributor is not on the University of Texas at Austin faculty ?
Output: Matt Kaufmann