# An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
## 5 Experimental Results
### DRUP Analysis
\begin{table}
\begin{tabular}{c c c c c c c c c c c c c} \hline \hline  & & & & & & & & & & & & & \\ \hline no shuffle & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & 0.02 & \(1.83\times 10^{-2}\) & 0.00 & 0.00 & \(6.47\times 10^{-2}\) \\ shuffle1 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(7.09\times 10^{-1}\) & 0.30 & 0.06 & \(1.00\times 10^{0}\) \\ shuffle2 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & 0.01 & \(7.23\times 10^{-1}\) & 0.20 & 0.04 & \(9.85\times 10^{-1}\) \\ shuffle3 & 11 & 119 & 597 & 0.06 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.20 & 0.04 & \(7.86\times 10^{-1}\) & 0.10 & 0.03 & \(7.56\times 10^{-1}\) \\ \hline no shuffle & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(1.58\times 10^{-9}\) \\ shuffle12 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.02 & \(1.00\times 10^{0}\) \\ shuffle2 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.02 & \(9.25\times 10^{-1}\) \\ shuffle3 & 12 & 142 & 778 & 0.05 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.04 & \(6.00\times 10^{-2}\) \\ \hline no shuffle & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ shuffle1 & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ shuffle2 & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ shuffle3 & 13 & 167 & 993 & 0.04 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ \hline \hline \end{tabular}
\end{table} 
Table 4: DRUP analysis results of PHP instances with full extension for MiniSAT. \begin{table}
\begin{tabular}{c c c c c c c c c c c c c} \hline \hline  & & & & & & & & & & & & & & \\ \hline no shuffle & 11 & 200 & 921 & 0.39 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.80 & 0.77 & \(1.03\times 10^{-85}\) & 0.50 & 0.51 & \(1.09\times 10^{-34}\) \\ shuffle1 & 11 & 200 & 921 & 0.39 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.10 & 0.32 & \(6.73\times 10^{-1}\) & 0.70 & 0.81 & \(7.01\times 10^{-34}\) \\ shuffle2 & 11 & 200 & 921 & 0.39 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.50 & 0.74 & \(6.44\times 10^{-46}\) & 0.70 & 0.76 & \(1.42\times 10^{-21}\) \\ shuffle3 & 11 & 200 & 921 & 0.39 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.50 & 0.77 & \(6.73\times 10^{-53}\) & 0.60 & 0.61 & \(6.31\times 10^{-2}\) \\ \hline no shuffle & 12 & 242 & 1178 & 0.37 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.80 & 0.59 & \(7.40\times 10^{-67}\) & 0.70 & 0.80 & \(5.12\times 10^{-57}\) \\ shuffle1 & 12 & 242 & 1178 & 0.37 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.60 & 0.82 & \(2.28\times 10^{-24}\) & 0.50 & 0.55 & \(1.79\times 10^{-2}\) \\ shuffle2 & 12 & 242 & 1178 & 0.37 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.30 & 0.31 & \(3.07\times 10^{-1}\) & 0.00 & 0.00 & \(1.00\times 10^{0}\) \\ shuffle3 & 12 & 242 & 1178 & 0.37 & 0.00 & 0.00 & \(1.00\times 10^{0}\) & 0.00 & 0.68 & \(1.67\times 10^{-18}\) & 0.60 & 0.82 & \(1.03\times 10^{-32}\) \\ \hline no shuffle & 13 & 288 & 1477 & 0.36 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ shuffle3 & 13 & 288 & 1477 & 0.36 & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data & no-data \\ \hline \hline \end{tabular}
\end{table} 
Table 5: DRUP analysis results of PHP instances with full extension for Glucose.