added definition range_vars and lemmas vars_of_subst_conv_Union, vars_of_subst_subset, range_vars_comp_subset, and unify_gives_minimal_range
#!/usr/bin/python3 -Es
import re
import sys
import matplotlib.pyplot as plt
from matplotlib.backends.backend_pdf import PdfPages
output = PdfPages('chart.pdf')
re_entry = re.compile(R'^(.*\S+)\s+(\d+)\s*\**\s*$')
labels = []
values = []
for line in sys.stdin.readlines():
match = re_entry.match(line)
labels.append(match.group(1))
values.append(match.group(2))
plt.pie(values, labels = labels)
output.savefig()
output.close()