## Chart: Cumulative Solving + Checking Time ### Overview The image is a line chart comparing the cumulative solving and checking time for three different solver-checker combinations: Duper, cvc5+Lean-SMT, and veriT+Sledgehammer. The x-axis represents the number of benchmarks, and the y-axis represents the time in seconds on a logarithmic scale. ### Components/Axes * **Title:** Cumulative solving + checking time * **X-axis:** Number of benchmarks, ranging from 0 to 2500 in increments of 500. * **Y-axis:** Time (s), on a logarithmic scale from 10^-2 to 10⁴. The axis markers are 10^-2, 10^-1, 10⁰, 10¹, 10², 10³, and 10⁴. * **Legend:** Located in the bottom-right corner. * **Blue:** Duper * **Orange:** cvc5+Lean-SMT * **Green:** veriT+Sledgehammer ### Detailed Analysis * **Duper (Blue):** The line starts at approximately 10^-1 seconds at 0 benchmarks. It increases rapidly until around 500 benchmarks, reaching approximately 10² seconds. From 500 to 1000 benchmarks, the increase slows down. After 1000 benchmarks, the line continues to increase, reaching approximately 10⁴ seconds. * **cvc5+Lean-SMT (Orange):** The line starts at approximately 10^-2 seconds at 0 benchmarks. It increases rapidly until around 250 benchmarks, reaching approximately 10¹ seconds. From 250 to 2500 benchmarks, the increase is gradual, reaching approximately 10³ seconds. * **veriT+Sledgehammer (Green):** The line starts at approximately 10^-2 seconds at 0 benchmarks. It increases rapidly until around 2000 benchmarks, reaching approximately 10² seconds. From 2000 to 2500 benchmarks, the increase is rapid, reaching approximately 10³ seconds. ### Key Observations * Duper has the fastest initial solving time but increases rapidly, becoming the slowest for a large number of benchmarks. * cvc5+Lean-SMT has a slower initial solving time but increases more gradually, making it faster than Duper for a large number of benchmarks. * veriT+Sledgehammer has the slowest initial solving time but remains relatively slow until around 2000 benchmarks, after which it increases rapidly. ### Interpretation The chart compares the performance of three different solver-checker combinations in terms of cumulative solving and checking time. The logarithmic scale on the y-axis indicates that the differences in time are significant. The data suggests that the choice of solver-checker combination depends on the number of benchmarks being processed. For a small number of benchmarks, Duper may be the fastest option. However, for a large number of benchmarks, cvc5+Lean-SMT is likely to be more efficient. veriT+Sledgehammer is the least efficient for a smaller number of benchmarks, but its performance degrades significantly after 2000 benchmarks.

\n ## Chart: Cumulative Solving + Checking Time ### Overview The image presents a line chart illustrating the cumulative solving and checking time for three different solver/checker combinations across a varying number of benchmarks. The y-axis represents time in seconds on a logarithmic scale, while the x-axis represents the number of benchmarks. The chart aims to compare the performance of these solvers as the number of benchmarks increases. ### Components/Axes * **Title:** "Cumulative solving + checking time" (centered at the top) * **X-axis Label:** "Number of benchmarks" (bottom-center) * **Y-axis Label:** "Time (s)" (left-center) - Logarithmic scale. * **Legend:** Located in the bottom-right corner. * "Duper" (Blue line) * "cvc5+Lean-SMT" (Orange line) * "veriT+Sledgehammer" (Green line) * **Gridlines:** Dashed horizontal and vertical lines providing a visual reference. * **Y-axis Scale:** Logarithmic, with markers at 10^-2, 10^-1, 10⁰, 10¹, 10², 10³, 10⁴. ### Detailed Analysis The chart displays three distinct curves, each representing a solver/checker combination. * **Duper (Blue Line):** The blue line starts at approximately 0.1 seconds at 0 benchmarks and rapidly increases, reaching approximately 10⁴ seconds (10,000 seconds) at 2500 benchmarks. The curve initially shows a steep slope, which gradually flattens as the number of benchmarks increases. * At 100 benchmarks: ~10¹ seconds (10 seconds) * At 500 benchmarks: ~10² seconds (100 seconds) * At 1000 benchmarks: ~300 seconds * At 1500 benchmarks: ~600 seconds * At 2000 benchmarks: ~1500 seconds * At 2500 benchmarks: ~10,000 seconds * **cvc5+Lean-SMT (Orange Line):** The orange line starts at approximately 0.01 seconds at 0 benchmarks and increases more gradually than the blue line. It reaches approximately 500 seconds at 2500 benchmarks. The slope is consistently less steep than the blue line. * At 100 benchmarks: ~0.5 seconds * At 500 benchmarks: ~20 seconds * At 1000 benchmarks: ~70 seconds * At 1500 benchmarks: ~150 seconds * At 2000 benchmarks: ~250 seconds * At 2500 benchmarks: ~500 seconds * **veriT+Sledgehammer (Green Line):** The green line starts at approximately 0.001 seconds at 0 benchmarks and exhibits the slowest growth among the three. It reaches approximately 100 seconds at 2500 benchmarks. The slope is consistently the least steep. * At 100 benchmarks: ~0.1 seconds * At 500 benchmarks: ~1 seconds * At 1000 benchmarks: ~5 seconds * At 1500 benchmarks: ~15 seconds * At 2000 benchmarks: ~30 seconds * At 2500 benchmarks: ~100 seconds ### Key Observations * Duper consistently exhibits the highest cumulative solving and checking time across all benchmark counts. * cvc5+Lean-SMT performs better than Duper, with significantly lower cumulative times. * veriT+Sledgehammer demonstrates the best performance, with the lowest cumulative times throughout the entire range of benchmarks. * The logarithmic scale emphasizes the differences in performance, particularly at higher benchmark counts. * All three lines show diminishing returns, meaning the increase in time slows down as the number of benchmarks increases. ### Interpretation The chart demonstrates a clear performance hierarchy among the three solver/checker combinations. veriT+Sledgehammer is the most efficient, followed by cvc5+Lean-SMT, and then Duper. This suggests that veriT+Sledgehammer scales better with an increasing number of benchmarks. The logarithmic scale highlights the substantial difference in performance, especially as the problem size (number of benchmarks) grows. The diminishing returns observed in all three curves indicate that the complexity of solving each additional benchmark increases, but veriT+Sledgehammer handles this complexity more effectively. This data is valuable for selecting the appropriate solver/checker for a given task, considering the expected number of benchmarks and the acceptable solving time. The chart suggests that for a large number of benchmarks, veriT+Sledgehammer would be the preferred choice.

## Line Graph: Cumulative solving + checking time ### Overview The graph compares the cumulative solving and checking time (in seconds) across three solver+checker combinations as the number of benchmarks increases from 0 to 2500. The y-axis uses a logarithmic scale (10^-2 to 10^4 seconds), while the x-axis is linear. ### Components/Axes - **X-axis**: Number of benchmarks (0–2500, linear scale) - **Y-axis**: Time (s) (10^-2 to 10^4, logarithmic scale) - **Legend**: Located in the bottom-right corner, with three entries: - **Blue line**: Duper - **Orange line**: cvc5+Lean-SMT - **Green line**: veriT+Sledgehammer ### Detailed Analysis 1. **Duper (Blue line)**: - Starts at ~0.1 seconds for 0 benchmarks. - Rises sharply to ~1000 seconds at 1000 benchmarks. - Plateaus slightly above 1000 benchmarks, reaching ~3000 seconds at 2500 benchmarks. - **Key trend**: Exponential growth on the logarithmic scale, indicating rapid time increases with benchmarks. 2. **cvc5+Lean-SMT (Orange line)**: - Begins at ~0.01 seconds for 0 benchmarks. - Gradually increases to ~200 seconds at 1000 benchmarks. - Continues rising steadily to ~350 seconds at 2500 benchmarks. - **Key trend**: Linear growth on the logarithmic scale, suggesting sub-exponential time complexity. 3. **veriT+Sledgehammer (Green line)**: - Starts at ~0.001 seconds for 0 benchmarks. - Remains flat until ~2000 benchmarks, then surges to ~1000 seconds at 2000 benchmarks. - Accelerates further to ~2000 seconds at 2500 benchmarks. - **Key trend**: Sudden nonlinear increase after 2000 benchmarks, contrasting with earlier stability. ### Key Observations - **Duper** exhibits the steepest growth, with time increasing ~100x between 1000 and 2500 benchmarks. - **cvc5+Lean-SMT** maintains the slowest growth rate across all benchmarks. - **veriT+Sledgehammer** shows a stark performance drop after 2000 benchmarks, with time increasing ~10x between 2000 and 2500 benchmarks. - All lines intersect near 0 benchmarks, but diverge significantly as benchmarks increase. ### Interpretation The data suggests: 1. **Scalability differences**: Duper’s exponential time growth makes it unsuitable for large benchmark sets, while cvc5+Lean-SMT scales more efficiently. 2. **veriT+Sledgehammer’s anomaly**: Its stable performance until 2000 benchmarks followed by a sharp decline implies potential algorithmic limitations or optimization thresholds. 3. **Logarithmic scale implications**: The y-axis compression highlights Duper’s disproportionate time costs at higher benchmarks, which might be overlooked on a linear scale. The graph underscores trade-offs between solver+checker combinations, with cvc5+Lean-SMT appearing most efficient for large-scale applications. The veriT+Sledgehammer combination warrants further investigation into its post-2000 performance degradation.