Rule
vars
vars(rule, l) = l is the list of vars used in rule
if
if(rule, l) = l is the list of premises in rule
then
then(rule, s) = s is the conclusion of rule