1\setlength{\tabcolsep}{3.5pt}\begin{tabular}{@{}rrrrrrll@{}}2\toprule3$n$ & variables & clauses & CaDiCaL (s) & proof lines & drat-trim (s) & CNF SHA-256 & proof SHA-256\\4\midrule526 & 1,779 & 3,589 & 20.8 & 1,528,402 & 18.1 & \texttt{8b2b39c3769f94b2} & \texttt{3d1a3b3652f8e732}\\630 & 2,171 & 4,381 & 20.5 & 1,440,157 & 16.4 & \texttt{c526d49854f86414} & \texttt{e2656fd1b6e21c20}\\740 & 3,151 & 6,361 & 23.2 & 1,438,038 & 19.0 & \texttt{108bc245d1983d35} & \texttt{5f3a371fc8fb20c3}\\850 & 4,131 & 8,341 & 27.3 & 1,367,546 & 28.9 & \texttt{925b74a12023475f} & \texttt{cf91a7b47240bf41}\\960 & 5,111 & 10,321 & 31.6 & 1,437,601 & 40.4 & \texttt{7f5d6d4cc0c34a73} & \texttt{a2ff4fe669cd7e2b}\\1070 & 6,091 & 12,301 & 49.1 & 1,751,245 & 42.4 & \texttt{41cbe28199c05b53} & \texttt{01aebd7b76c4e379}\\1180 & 7,071 & 14,281 & 45.4 & 1,780,669 & 50.9 & \texttt{6ef97ab92c165054} & \texttt{a52be3cb21ad3a59}\\1290 & 8,051 & 16,261 & 115.2 & 2,796,452 & 103.0 & \texttt{217a9f570f340a2d} & \texttt{1ac406abdd73beee}\\13100 & 9,031 & 18,241 & 107.7 & 3,132,080 & 95.0 & \texttt{9716f6fe9658d889} & \texttt{defbfdb12994c8dc}\\14110 & 10,011 & 20,221 & 110.1 & 3,281,673 & 104.9 & \texttt{90cc4aceefceca54} & \texttt{85b0a09a20712e6e}\\15120 & 10,991 & 22,201 & 143.6 & 3,669,833 & 153.9 & \texttt{0a5576422e6c22f1} & \texttt{4ef95714eacd70ae}\\16130 & 11,971 & 24,181 & 179.1 & 4,107,598 & 151.3 & \texttt{705fda01008e9e47} & \texttt{3259fd182fabf86c}\\17140 & 12,951 & 26,161 & 231.9 & 4,137,876 & 177.3 & \texttt{8d53e0c5734cb054} & \texttt{5058e939dc808016}\\18150 & 13,931 & 28,141 & 204.5 & 4,545,857 & 168.6 & \texttt{c44db207409a5796} & \texttt{4d9c5a910260bbe2}\\19154 & 14,323 & 28,933 & 226.5 & 4,662,907 & 197.2 & \texttt{fa15c4c63db1c686} & \texttt{41ea487bdc464bf0}\\20\bottomrule21\end{tabular}22% totals: solve 12972.145 s, check 11700.677 s, proof lines 34650279623