\begin{figure}
    \centering
    \begin{subfigure}[]{0.9\textwidth}
        \begin{lstlisting}
    PREFIX ulo: <https://mathhub.info/ulo#>

    SELECT ?theorem ?proof ?size
    WHERE {
        ?theorem ulo:theorem ?i .
        ?proof ulo:justifies ?theorem .
        ?proof ulo:proof ?j .
        ?proof ulo:external-size ?size .
    }
    ORDER BY DESC(?size)
        \end{lstlisting}

        \caption{SPARQL query that returns each pair of \texttt{theorem}
          and one given \texttt{proof}, ordered by the size of \texttt{proof}.}\label{fig:q1short}
    \end{subfigure}
    \vspace{0.5cm}

    \begin{subfigure}[]{0.9\textwidth}
        \begin{lstlisting}
    PREFIX ulo: <https://mathhub.info/ulo#>
    PREFIX xsd: <http://www.w3.org/2001/XMLSchema#>

    SELECT ?theorem ?proof ?size (
        xsd:float(?size) + xsd:float(?checktime) as ?rating
    )
    WHERE {
        ?theorem ulo:theorem ?i .
        ?proof ulo:justifies ?theorem .
        ?proof ulo:proof ?j .
        ?proof ulo:external-size ?size .
        ?proof ulo:check-time ?checktime .
    }
    ORDER BY DESC(?rating)
        \end{lstlisting}

        \caption{SPARQL query that returns each pair of \texttt{theorem}
          and one given \texttt{proof} ordered by the sum of size and
          check time of the given proof. A naive rating such as this one
          will hardly yield helpful results, but it shows that given some
          kind of complexity scale, we can rate theorems and their proofs
          by such a scale.}\label{fig:q1long}
    \end{subfigure}

    \caption{SPARQL queries for serving the organizational aspect
      of~$\mathcal{Q}_1$.}\label{fig:q1full}
\end{figure}
