\begin{figure}
    \centering
    \small
    \begin{subfigure}[]{0.9\textwidth}
        \begin{flushleft}
            \texttt{check-time} \texttt{defines} \texttt{definition}
            \texttt{derived} \texttt{experimental}
            \texttt{external-size} \texttt{function}
            \texttt{important} \texttt{inductive-on}
            \texttt{instance-of} \texttt{justifies} \texttt{name}
            \texttt{para} \texttt{paratype} \texttt{predicate}
            \texttt{primitive} \texttt{section} \texttt{sourceref}
            \texttt{specified-in} \texttt{specifies}
            \texttt{statement} \texttt{theory} \texttt{type}
            \texttt{unimportant} \texttt{universe} \texttt{uses}
        \end{flushleft}
        \caption{ULO predicates used in the Isabelle exports.}\label{fig:used}
    \end{subfigure}
    \vspace{0.5cm}

    \begin{subfigure}[]{.9\textwidth}
        \begin{flushleft}
            \texttt{action-times} \texttt{aligned-with}
            \texttt{alternative-for} \texttt{antonym}
            \texttt{automatically-proved} \texttt{axiom}
            \texttt{constructs} \texttt{contains}
            \texttt{counter-example-for} \texttt{crossrefs}
            \texttt{declaration} \texttt{deprecated} \texttt{docref}
            \texttt{example} \texttt{example-for} \texttt{file}
            \texttt{folder} \texttt{formalizes} \texttt{generated-by}
            \texttt{hypernym} \texttt{hyponym}
            \texttt{implementation-uses}
            \texttt{implementation-uses-implementation-of}
            \texttt{implementation-uses-interface-of} \texttt{inspired-by}
            \texttt{inter-statement} \texttt{interface-uses}
            \texttt{interface-uses-implementation-of}
            \texttt{interface-uses-interface-of} \texttt{internal-size}
            \texttt{last-checked-at} \texttt{library}
            \texttt{library-group} \texttt{logical}
            \texttt{mutual-block} \texttt{nyms}
            \texttt{organizational} \texttt{phrase} \texttt{physical}
            \texttt{proof} \texttt{proposition} \texttt{revision}
            \texttt{rule} \texttt{same-as} \texttt{see-also}
            \texttt{similar-to} \texttt{size-properties}
            \texttt{superseded-by} \texttt{theorem} \texttt{typedec}
            \texttt{uses-implementation} \texttt{uses-interface}
        \end{flushleft}
        \caption{ULO predicates \emph{not} used in the Isabelle exports.}\label{fig:used}
    \end{subfigure}
    \vspace{0.5cm}

    \begin{subfigure}[]{.9\textwidth}
        \begin{flushleft}
            \texttt{axiom} \texttt{definition}
            \texttt{derived} \texttt{example} \texttt{file}
            \texttt{folder} \texttt{internal-size}
            \texttt{library} \texttt{library-group}
            \texttt{predicate} \texttt{primitive}
            \texttt{proposition} \texttt{revision}
            \texttt{statement} \texttt{theory} \texttt{type}
            \texttt{uses}
        \end{flushleft}
        \caption{ULO predicates used in the Coq exports.}\label{fig:used}
    \end{subfigure}
    \vspace{0.5cm}

    \begin{subfigure}[]{.9\textwidth}
        \begin{flushleft}
            \texttt{action-times} \texttt{aligned-with}
            \texttt{alternative-for} \texttt{antonym}
            \texttt{automatically-proved} \texttt{check-time}
            \texttt{constructs} \texttt{contains}
            \texttt{counter-example-for} \texttt{crossrefs}
            \texttt{declaration} \texttt{defines}
            \texttt{deprecated} \texttt{docref}
            \texttt{example-for} \texttt{experimental}
            \texttt{external-size} \texttt{formalizes}
            \texttt{function} \texttt{generated-by}
            \texttt{hypernym} \texttt{hyponym}
            \texttt{implementation-uses}
            \texttt{implementation-uses-implementation-of}
            \texttt{implementation-uses-interface-of}
            \texttt{important} \texttt{inductive-on}
            \texttt{inspired-by} \texttt{instance-of}
            \texttt{inter-statement} \texttt{interface-uses}
            \texttt{interface-uses-implementation-of}
            \texttt{interface-uses-interface-of}
            \texttt{justifies} \texttt{last-checked-at}
            \texttt{logical} \texttt{mutual-block}
            \texttt{name} \texttt{nyms}
            \texttt{organizational} \texttt{para}
            \texttt{paratype} \texttt{phrase}
            \texttt{physical} \texttt{proof} \texttt{rule}
            \texttt{same-as} \texttt{section}
            \texttt{see-also} \texttt{similar-to}
            \texttt{size-properties} \texttt{sourceref}
            \texttt{specified-in} \texttt{specifies}
            \texttt{superseded-by} \texttt{theorem}
            \texttt{typedec} \texttt{unimportant}
            \texttt{universe} \texttt{uses-implementation}
            \texttt{uses-interface}
        \end{flushleft}
        \caption{ULO predicates \emph{not} used in the Coq exports.}\label{fig:used}
    \end{subfigure}
    \vspace{0.5cm}

    \caption{ULO predicates in their usage}\label{fig:used}
\end{figure}