AI 中文总结
该研究针对电路图示等价性问题，引入含三种变体的新基准系列，提供TPTP与SMT-LIB格式的一阶编码及自动生成脚本，并在先进自动定理证明器和SMT求解器上完成评估。
AI 中文摘要
我们针对电路的图示等价性问题引入了新的基准系列，考虑了从基础到具有挑战性的三种问题变体，并为每种变体生成了基准。我们提供了TPTP和SMT-LIB格式的一阶编码，以及自动生成基准实例的脚本，并在最先进的自动定理证明器和SMT求解器上对这些基准进行了评估。
英文摘要
We introduce a new family of benchmarks for the problem of diagrammatic equivalence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances, and evaluate these benchmarks on state-of-the-art automated theorem provers and SMT solvers.
