The program FORKLIFT is an inclusion checker for Büchi automata. It takes two automata as input, let us call the first A and the second B. Upon termination, FORKLIFT exit code is: "0" if L(A) is a subset of L(B), it is "1" if L(A) is NOT a subset of L(B), otherwise it is "127" when the inclusion has not been computed. The input format of the automata is described here: http://languageinclusion.org/doku.php?id=tools#the_ba_format