| formula |
| test1_quant_squaring3.qdimacs | |
| C5315.blif_0.10_0.20_0_0_inp_exact.qdimacs | |
| adder-12-unsat.qdimacs | |
| test4_quant_squaring4.qdimacs | |
| connect_7x6_4_R.qdimacs | |
| cube_c11_ser--opt-42_.qdimacs | |
| connect_9x8_3_R.qdimacs | |
| k6_4_3.qdimacs | |
| c4_Debug_s3_f2_e1_v3.qdimacs | |
| b04_C_2_20.qdimacs | |
| k_ph_p-18.qdimacs | |
| k12_3_3.qdimacs | |
| audio_ddksynth_voice.cpp.qdimacs | |
| s38584_3_238.qdimacs | |
| test2_quant2.qdimacs | |
| s1269_d10_s.qdimacs | |
| filesys_cdfs_namesup.c.qdimacs | |
| k_ph_p-17.qdimacs | |
| k_ph_p-16.qdimacs | |
| uclid-pipe2.qdimacs | |
| adder-16-unsat.qdimacs | |
| ev-pr-8x8-19-7-0-1-2-lg.qdimacs | |
| test4_quant4.qdimacs | |
| test2_quant_squaring2.qdimacs | |
| C6288.blif_0.10_0.20_0_1_out_exact.qdimacs | |
| ring_r6_ser--opt-17_.qdimacs | |
| b22_C_2_12.qdimacs | |
| C499.blif_0.10_0.20_0_1_out_exact.qdimacs | |
| filesys_fastfat_allocsup.c.qdimacs | |
| test1_quant2.qdimacs | |
| test3_quant_squaring4.qdimacs | |
| k12_2_2.qdimacs | |
| k12_2_3.qdimacs | |
| C6288.blif_0.10_0.20_0_1_inp_exact.qdimacs | |
| filesys_smbmrx_smbxchng.c.qdimacs | |
| b21_C_3_206.qdimacs | |
| C5315.blif_0.10_0.20_0_1_out_exact.qdimacs | |
| filesys_fastfat_easup.c.qdimacs | |
| C499.blif_0.10_0.20_0_0_out_exact.qdimacs | |
| s1269_d13_u.qdimacs | |
| C5315.blif_0.10_0.20_0_0_out_exact.qdimacs | |
| blocks_enc_2_b4_ser--opt-26_.qdimacs | |
| C6288.blif_0.10_1.00_0_0_inp_exact.qdimacs | |
| b14_C_3_105.qdimacs | |
| k_ph_p-12.qdimacs | |
| adder-12-sat.qdimacs | |
| b20_C_3_2.qdimacs | |
| k12_4_2.qdimacs | |
| C6288.blif_0.10_0.20_0_0_out_exact.qdimacs | |
| test1_quant_squaring2.qdimacs | |
| test1_quant3.qdimacs | |
| s1269_d15_u.qdimacs | |
Number of Unsolved Formulas (solved by no solver)
| FORMULA | SOLVER |
| adder-10-sat.qdimacs | runAqme.sh | |
| adder-14-unsat.qdimacs | squeezebf1.2-qube7.2.pl | |
| audio_ac97_wavepcistream3.cpp.qdimacs | run_rareqs | |
| biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009.qdimacs | run_rareqs | |
| c3_Debug_s3_f2_e2_v2.qdimacs | squeezebf1.2-qube7.2.pl | |
| c4_Debug_s3_f1_e1_v3.qdimacs | squeezebf1.2-qube7.2.pl | |
| C880.blif_0.10_0.20_0_0_inp_exact.qdimacs | ghostq.sh | |
| C880.blif_0.10_0.20_0_1_inp_exact.qdimacs | ghostq.sh | |
| cube_c7_ser---23_.qdimacs | run_rareqs | |
| emptyroom_e4_ser--opt-44_.qdimacs | run_rareqs | |
| ev-pr-6x6-5-5-0-1-2-s.qdimacs | runAqme.sh | |
| k14_3_3.qdimacs | squeezebf1.2-qube7.2.pl | |
| k_branch_n-14.qdimacs | hiqqer3 | |
| k_branch_n-20.qdimacs | hiqqer3 | |
| k_branch_n-21.qdimacs | hiqqer3 | |
| k_branch_p-21.qdimacs | hiqqer3 | |
| ring_r7_ser--opt-20_.qdimacs | squeezebf1.2-qube7.2.pl | |
| s3330_d10_u.qdimacs | squeezebf1.2-qube7.2.pl | |
| s3330_d11_u.qdimacs | squeezebf1.2-qube7.2.pl | |
| s3330_d13_u.qdimacs | squeezebf1.2-qube7.2.pl | |
| s3330_d14_u.qdimacs | squeezebf1.2-qube7.2.pl | |
| stmt31_276_328.qdimacs | pre_dual_ooq.py | |
| stmt41_286_385.qdimacs | pre_dual_ooq.py | |
Formulas only solved by one solver
| formula | solver | result |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | bdepqbf | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | depqbf | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | StruQS | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | runAqme.sh | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | pre_dual_ooq.py | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | dual_ooq | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | ooq | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | hiqqer3 | 20 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | squeezebf1.2-qube3.0 | 1 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | qube7.2 | 10 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | squeezebf1.2-qube7.2.pl | 99 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | ghostq-cegar.sh | 20 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | ghostq-bq-cegar.sh | 20 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | ghostq.sh | 20 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | run_rareqs | 20 |
| C880.blif_0.10_1.00_0_0_inp_exact.qdimacs | qcnf2z3 | 44 |
| formula | solver | result |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | bdepqbf | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | depqbf | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | runAqme.sh | 20 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | StruQS | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | dual_ooq | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | pre_dual_ooq.py | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | ooq | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | hiqqer3 | 152 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | qube7.2 | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | squeezebf1.2-qube3.0 | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | squeezebf1.2-qube7.2.pl | 10 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | ghostq-bq-cegar.sh | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | ghostq.sh | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | ghostq-cegar.sh | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | run_rareqs | 1 |
| ev-pr-6x6-7-5-0-1-2-s.qdimacs | qcnf2z3 | 1 |
| formula | solver | result |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | depqbf | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | bdepqbf | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | StruQS | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | runAqme.sh | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | ooq | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | dual_ooq | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | pre_dual_ooq.py | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | hiqqer3 | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | squeezebf1.2-qube3.0 | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | squeezebf1.2-qube7.2.pl | 10 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | qube7.2 | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | ghostq-bq-cegar.sh | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | ghostq-cegar.sh | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | ghostq.sh | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | qcnf2z3 | 20 |
| fpu-01Xh-error02-nonuniform-depth-23.qdimacs | run_rareqs | 20 |
| formula | solver | result |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | bdepqbf | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | depqbf | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | StruQS | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | runAqme.sh | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | pre_dual_ooq.py | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | ooq | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | dual_ooq | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | hiqqer3 | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | squeezebf1.2-qube7.2.pl | 10 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | squeezebf1.2-qube3.0 | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | qube7.2 | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | ghostq-cegar.sh | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | ghostq.sh | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | ghostq-bq-cegar.sh | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | qcnf2z3 | 20 |
| fpu-10Xe-correct02-nonuniform-depth-27.qdimacs | run_rareqs | 20 |
| formula | solver | result |
| ring_r7_ser---19_.qdimacs | bdepqbf | 1 |
| ring_r7_ser---19_.qdimacs | depqbf | 1 |
| ring_r7_ser---19_.qdimacs | runAqme.sh | 1 |
| ring_r7_ser---19_.qdimacs | StruQS | 1 |
| ring_r7_ser---19_.qdimacs | ooq | 1 |
| ring_r7_ser---19_.qdimacs | pre_dual_ooq.py | 1 |
| ring_r7_ser---19_.qdimacs | dual_ooq | 1 |
| ring_r7_ser---19_.qdimacs | hiqqer3 | 1 |
| ring_r7_ser---19_.qdimacs | qube7.2 | 1 |
| ring_r7_ser---19_.qdimacs | squeezebf1.2-qube3.0 | 1 |
| ring_r7_ser---19_.qdimacs | squeezebf1.2-qube7.2.pl | 10 |
| ring_r7_ser---19_.qdimacs | ghostq-bq-cegar.sh | 1 |
| ring_r7_ser---19_.qdimacs | ghostq.sh | 1 |
| ring_r7_ser---19_.qdimacs | ghostq-cegar.sh | 1 |
| ring_r7_ser---19_.qdimacs | run_rareqs | 20 |
| ring_r7_ser---19_.qdimacs | qcnf2z3 | 1 |
