QBF Solver Evaluation Portal
Home
QBFLIB
QBFGALLERY'23
QBFEVALs
2022
2020
2019
2018
2017
2016
2010
2008
2007
2006
2005
2004
QBF GALLERIES
QBF Gallery 2014
QBF Gallery 2013
DOWNLOADS
Download the QBFEVAL'22 dataset
Download the QBFEVAL'20 dataset
Download the QBFEVAL'19 dataset and raw results
Download the QBFEVAL'18 dataset and raw results
Download the QBFEVAL'17 dataset and raw results
Download the QBFEVAL'16 dataset
Download the QBFEVAL'10 dataset
Download the QBFEVAL'08 dataset
Download the non-prenex non-cnf track dataset
Download the QBFEVAL'07 dataset
Download the QBFEVAL'06 dataset
Download the QDIMACS to QPRO converter
Download the QDIMACS to QBF1.0 converter
qbflib.org
Instances solved by
rareqs-nn
QBFEVAL'16 - Prenex non-CNF Track.
Instance
Result
Time
incrementer-enc05-uniform-depth-2
UNSAT
0.05
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-001
UNSAT
0.05
stmt44_107_108
SAT
0.06
flipflop-3-c
UNSAT
0.06
toilet_g_04_01.2
SAT
0.06
z4ml.blif_0.10_0.20_0_1_out_exact
SAT
0.07
counter5_2
SAT
0.07
mutex-2-s
SAT
0.07
counter4_3
SAT
0.07
rewriting_k_10
UNSAT
0.07
counter4_2
SAT
0.07
z4ml.blif_0.10_1.00_0_1_out_exact
SAT
0.07
counter4_4
SAT
0.08
counter7_2
SAT
0.08
rewriting_k_21
UNSAT
0.08
z4ml.blif_0.10_0.20_0_1_inp_exact
SAT
0.08
qshifter_3
SAT
0.08
counter6_2
SAT
0.08
ring5_2
SAT
0.08
z4ml.blif_0.10_1.00_0_0_inp_exact
UNSAT
0.08
toilet_g_08_01.2
SAT
0.08
ring6_2
SAT
0.08
ring4_2
SAT
0.08
toilet_a_04_01.4
UNSAT
0.08
rewriting_k_17
UNSAT
0.08
rewriting_k_19
UNSAT
0.08
ring4_3
SAT
0.09
counter8_2
SAT
0.09
counter5_4
SAT
0.09
counter4_5
SAT
0.09
toilet_c_06_01.4
UNSAT
0.1
semaphore_2
SAT
0.1
counter4_6
SAT
0.1
s27_d4_u
UNSAT
0.1
toilet_a_04_01.6
UNSAT
0.1
stmt17_18_19
SAT
0.1
counter4_7
SAT
0.11
ring4_4
SAT
0.11
ring5_4
SAT
0.11
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf00.01X-QBF.BB1-01X.BB2-01X.BB3-01X.with-IOC.unfold-003
UNSAT
0.11
counter6_4
SAT
0.11
ring4_5
SAT
0.12
mutex-4-s
SAT
0.12
counter4_8
SAT
0.12
eijk.S382.S-d4
SAT
0.12
counter7_4
SAT
0.12
k_ph_p-3
UNSAT
0.12
s27_d5_u
UNSAT
0.12
counter4_9
SAT
0.13
ring6_4
SAT
0.13
semaphore3_2
SAT
0.13
ring4_6
SAT
0.14
semaphore_3
SAT
0.14
counter5_8
SAT
0.14
counter4_10
SAT
0.14
counter8_4
SAT
0.14
counter4_11
SAT
0.15
ring4_7
SAT
0.15
counter4_12
SAT
0.15
semaphore4_2
SAT
0.16
ring4_8
SAT
0.16
counter4_14
SAT
0.17
counter4_13
SAT
0.17
counter6_8
SAT
0.17
counter4_15
SAT
0.18
rewriting_k_100
UNSAT
0.18
ring5_8
SAT
0.18
semaphore_4
SAT
0.18
semaphore3_3
SAT
0.19
counter4_16
SAT
0.19
toilet_a_06_01.6
UNSAT
0.2
C5315.blif_0.10_1.00_0_0_out_exact
UNSAT
0.2
Adder2-2-c
UNSAT
0.2
semaphore5_2
SAT
0.2
dmeSmall_2
SAT
0.21
counter7_8
SAT
0.21
ring6_8
SAT
0.21
s641_d2_s
SAT
0.21
semaphore_5
SAT
0.22
toilet_g_15_01.2
SAT
0.22
semaphore6_2
SAT
0.22
s713_d2_s
SAT
0.22
counter_e_2
SAT
0.22
stmt27_296_297
SAT
0.23
Core1108_tbm_21.tex.module.000091
UNSAT
0.23
semaphore4_3
SAT
0.24
k_lin_p-2
UNSAT
0.24
tree-exa10-10
SAT
0.25
C5315.blif_0.10_1.00_0_0_inp_exact
UNSAT
0.25
semaphore3_4
SAT
0.25
Core1108_tbm_21.tex.module.000017
UNSAT
0.26
s510_d3_s
SAT
0.26
counter8_8
SAT
0.26
Umbrella_tbm_24.tex.module.000103
UNSAT
0.27
counter5_16
SAT
0.28
dme1_2
SAT
0.29
Core1108_tbm_03.tex.module.000092
UNSAT
0.29
Core1108_tbm_21.tex.module.000023
UNSAT
0.29
Core1108_tbm_03.tex.module.000090
UNSAT
0.29
Core1108_tbm_21.tex.module.000026
UNSAT
0.29
Core1108_tbm_21.tex.module.000030
UNSAT
0.29
Umbrella_tbm_24.tex.module.000066
UNSAT
0.29
semaphore5_3
SAT
0.3
Core1108_tbm_03.tex.module.000065
UNSAT
0.3
Core1108_tbm_03.tex.module.000056
UNSAT
0.3
Core1108_tbm_03.tex.module.000057
UNSAT
0.3
k_path_p-2
UNSAT
0.3
Core1108_tbm_03.tex.module.000058
UNSAT
0.3
Core1108_tbm_21.tex.module.000014
UNSAT
0.3
Core1108_tbm_03.tex.module.000064
UNSAT
0.3
Core1108_tbm_21.tex.module.000008
UNSAT
0.31
Core1108_tbm_03.tex.module.000037
UNSAT
0.31
Umbrella_tbm_29.tex.module.000078
UNSAT
0.31
Core1108_tbm_03.tex.module.000048
UNSAT
0.31
ring5_16
SAT
0.31
Core1108_tbm_21.tex.module.000010
UNSAT
0.31
s1196_d2_s
SAT
0.31
counter6_16
SAT
0.31
Core1108_tbm_03.tex.module.000039
UNSAT
0.31
Core1108_tbm_21.tex.module.000009
UNSAT
0.31
Core1108_tbm_03.tex.module.000023
UNSAT
0.32
Core1108_tbm_03.tex.module.000034
UNSAT
0.32
b12_PR_9_2
SAT
0.32
Core1108_tbm_03.tex.module.000031
UNSAT
0.32
Core1108_tbm_03.tex.module.000003
UNSAT
0.32
Core1108_tbm_03.tex.module.000021
UNSAT
0.32
Core1108_tbm_03.tex.module.000019
UNSAT
0.32
semaphore4_4
SAT
0.33
Core1108_tbm_21.tex.module.000027
UNSAT
0.34
vis.4-arbit^2.E-f2
SAT
0.34
semaphore6_3
SAT
0.36
Umbrella_tbm_29.tex.module.000010
UNSAT
0.37
k3_1_1
SAT
0.37
Umbrella_tbm_29.tex.module.000009
UNSAT
0.37
ring6_16
SAT
0.38
dmeSmall_4
SAT
0.39
counter7_16
SAT
0.4
semaphore5_4
SAT
0.41
Umbrella_tbm_05.tex.module.000065
UNSAT
0.42
dme1_3
SAT
0.42
Core1108_tbm_09.tex.module.000028
UNSAT
0.43
irst.dme6.B-d2
SAT
0.44
Core1108_tbm_03.tex.module.000038
UNSAT
0.44
Umbrella_tbm_21.tex.module.000149
UNSAT
0.44
term1.blif_0.10_1.00_0_0_out_exact
UNSAT
0.44
Umbrella_tbm_21.tex.module.000129
UNSAT
0.45
Umbrella_tbm_21.tex.module.000134
UNSAT
0.45
Umbrella_tbm_21.tex.module.000139
UNSAT
0.45
Umbrella_tbm_21.tex.module.000079
UNSAT
0.46
s386_d3_s
SAT
0.46
Umbrella_tbm_05.tex.module.000043
UNSAT
0.47
Umbrella_tbm_05.tex.module.000088
UNSAT
0.47
Umbrella_tbm_21.tex.module.000069
UNSAT
0.47
Core1108_tbm_09.tex.module.000033
UNSAT
0.47
Umbrella_tbm_21.tex.module.000056
UNSAT
0.48
counter5_32
SAT
0.48
Umbrella_tbm_21.tex.module.000049
UNSAT
0.48
Umbrella_tbm_21.tex.module.000044
UNSAT
0.48
semaphore6_4
SAT
0.49
Umbrella_tbm_26.tex.module.000061
UNSAT
0.49
counter8_16
SAT
0.49
Umbrella_tbm_26.tex.module.000041
UNSAT
0.5
BLOCKS3ii.4.3
UNSAT
0.5
counter5_33
SAT
0.5
Core1108_tbm_09.tex.module.000008
UNSAT
0.51
k_lin_p-4
UNSAT
0.51
Umbrella_tbm_21.tex.module.000029
UNSAT
0.51
Umbrella_tbm_21.tex.module.000024
UNSAT
0.52
Umbrella_tbm_05.tex.module.000079
UNSAT
0.52
Core1108_tbm_09.tex.module.000010
UNSAT
0.52
Core1108_tbm_09.tex.module.000009
UNSAT
0.52
Umbrella_tbm_26.tex.module.000021
UNSAT
0.53
Umbrella_tbm_26.tex.module.000004
UNSAT
0.53
toilet_g_20_01.2
SAT
0.54
Umbrella_tbm_05.tex.module.000064
UNSAT
0.54
s499_d7_s
SAT
0.55
dme1_4
SAT
0.57
Umbrella_tbm_05.tex.module.000053
UNSAT
0.57
s641_d4_s
SAT
0.57
Umbrella_tbm_25.tex.module.000121
UNSAT
0.59
ring5_32
SAT
0.59
toilet_c_08_01.11
UNSAT
0.59
ring5_33
SAT
0.6
s820_d3_s
SAT
0.6
stmt16_950_951
SAT
0.6
Umbrella_tbm_25.tex.module.000087
UNSAT
0.61
Umbrella_tbm_25.tex.module.000106
UNSAT
0.61
Umbrella_tbm_25.tex.module.000084
UNSAT
0.61
toilet_c_08_05.4
SAT
0.61
Umbrella_tbm_05.tex.module.000030
UNSAT
0.62
flipflop-5-c
UNSAT
0.62
Umbrella_tbm_05.tex.module.000025
UNSAT
0.63
counter6_32
SAT
0.64
Umbrella_tbm_25.tex.module.000099
UNSAT
0.65
Umbrella_tbm_05.tex.module.000015
UNSAT
0.66
Umbrella_tbm_05.tex.module.000011
UNSAT
0.67
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.68
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.68
mutex-32-s
SAT
0.69
W3-Umbrella_tbm_21.tex.moduleQ3.6S.000001
UNSAT
0.7
Umbrella_tbm_25.tex.module.000041
UNSAT
0.7
dme1_5
SAT
0.71
s713_d4_s
SAT
0.71
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.71
toilet_a_08_05.2
UNSAT
0.71
Umbrella_tbm_25.tex.module.000031
UNSAT
0.72
Umbrella_tbm_25.tex.module.000003
UNSAT
0.72
ring6_32
SAT
0.74
s3330_d2_s
SAT
0.74
par8-1-c-50
UNSAT
0.76
dmeSmall_8
SAT
0.77
possibility9_0_2
FAIL
0.78
possibility10_0_2
FAIL
0.78
assertion5_0_2
FAIL
0.78
possibility6_0_2
FAIL
0.78
W4-Umbrella_tbm_21.tex.moduleQ3.6S.000001
UNSAT
0.78
possibility2_0_2
FAIL
0.79
assertion10_0_2
FAIL
0.79
possibility5_0_2
FAIL
0.79
assertion3_0_2
FAIL
0.79
possibility1_0_2
FAIL
0.79
assertion11_0_2
FAIL
0.79
possibility4_0_2
FAIL
0.79
assertion9_0_2
FAIL
0.79
assertion6_0_2
FAIL
0.79
possibility7_0_2
FAIL
0.79
assertion2_0_2
FAIL
0.79
possibility3_0_2
FAIL
0.79
possibility12_0_2
FAIL
0.79
assertion1_0_2
FAIL
0.79
assertion8_0_2
FAIL
0.79
possibility11_0_2
FAIL
0.79
consistency_0_2
FAIL
0.79
assertion4_0_2
FAIL
0.8
assertion7_0_2
FAIL
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000027
UNSAT
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000014
UNSAT
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000002
UNSAT
0.8
possibility8_0_2
FAIL
0.8
assertion12_0_2
FAIL
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000007
UNSAT
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000019
UNSAT
0.8
Core1108_tbm_21.tex.moduleQ3.2S.000024
UNSAT
0.81
Core1108_tbm_21.tex.moduleQ3.2S.000011
UNSAT
0.81
counter7_32
SAT
0.81
Core1108_tbm_21.tex.moduleQ3.2S.000015
UNSAT
0.81
dme1_6
SAT
0.86
dmeSmall_9
SAT
0.87
Core1108_tbm_28.tex.moduleQ2.2S.000003
UNSAT
0.88
query01_ntrivil_1344
UNSAT
0.89
Core1108_tbm_03.tex.moduleQ3.2S.000002
UNSAT
0.9
Core1108_tbm_03.tex.moduleQ3.2S.000018
UNSAT
0.91
Core1108_tbm_03.tex.moduleQ3.2S.000009
UNSAT
0.91
Core1108_tbm_03.tex.moduleQ3.2S.000048
UNSAT
0.91
Core1108_tbm_03.tex.moduleQ3.2S.000003
UNSAT
0.91
Core1108_tbm_03.tex.moduleQ3.2S.000011
UNSAT
0.91
query48_query15_1344
UNSAT
0.92
s386_d4_s
SAT
0.96
C499.blif_0.10_1.00_0_1_inp_exact
SAT
0.98
dme1_7
SAT
1.02
counter8_32
SAT
1.02
stmt41_738_749
SAT
1.09
possibility4_0_3
FAIL
1.11
assertion8_0_3
FAIL
1.11
possibility3_0_3
FAIL
1.12
possibility6_0_3
FAIL
1.12
possibility2_0_3
FAIL
1.12
lut4_XOR_fOR
UNSAT
1.12
possibility11_0_3
FAIL
1.12
possibility10_0_3
FAIL
1.12
possibility1_0_3
FAIL
1.12
consistency_0_3
FAIL
1.12
W4-Umbrella_tbm_26.tex.moduleQ3.7S.000003
UNSAT
1.12
assertion4_0_3
FAIL
1.12
assertion11_0_3
FAIL
1.12
assertion2_0_3
FAIL
1.12
assertion10_0_3
FAIL
1.12
assertion12_0_3
FAIL
1.12
assertion5_0_3
FAIL
1.13
assertion9_0_3
FAIL
1.13
assertion3_0_3
FAIL
1.13
possibility12_0_3
FAIL
1.13
assertion6_0_3
FAIL
1.13
possibility9_0_3
FAIL
1.13
assertion7_0_3
FAIL
1.14
dme1_8
SAT
1.16
ring_r4_ser--opt-11_
UNSAT
1.19
arbiter-07-comp-error01-qbf-hardness-depth-4
UNSAT
1.19
W5-Umbrella_tbm_26.tex.moduleQ3.7S.000003
UNSAT
1.21
nusmv.tcas-t^1.B-d2
SAT
1.21
toilet_c_10_01.12
UNSAT
1.25
assertion1_0_3
FAIL
1.28
counter6_64
SAT
1.34
counter6_65
SAT
1.35
mutex-64-s
SAT
1.39
k_d4_n-1
SAT
1.4
Core1108_tbm_02.tex.moduleQ3.2S.000015
UNSAT
1.44
possibility5_0_3
FAIL
1.45
W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001
UNSAT
1.48
possibility2_0_4
FAIL
1.49
consistency_0_4
FAIL
1.49
s1269_d3_s
SAT
1.49
assertion11_0_4
FAIL
1.49
possibility7_0_4
FAIL
1.49
possibility4_0_4
FAIL
1.49
possibility11_0_4
FAIL
1.5
assertion6_0_4
FAIL
1.5
possibility3_0_4
FAIL
1.5
assertion10_0_4
FAIL
1.5
assertion9_0_4
FAIL
1.5
assertion12_0_4
FAIL
1.5
possibility9_0_4
FAIL
1.5
assertion8_0_4
FAIL
1.5
possibility8_0_3
FAIL
1.5
assertion1_0_4
FAIL
1.5
assertion4_0_4
FAIL
1.51
possibility5_0_4
FAIL
1.51
possibility6_0_4
FAIL
1.51
W4-Umbrella_tbm_25.tex.moduleQ3.7S.000003
UNSAT
1.51
assertion5_0_4
FAIL
1.51
possibility1_0_4
FAIL
1.51
possibility10_0_4
FAIL
1.51
assertion2_0_4
FAIL
1.51
assertion7_0_4
FAIL
1.52
assertion3_0_4
FAIL
1.52
Core1108_tbm_02.tex.moduleQ3.2S.000095
UNSAT
1.53
Core1108_tbm_02.tex.moduleQ3.2S.000077
UNSAT
1.53
Core1108_tbm_02.tex.moduleQ3.2S.000056
UNSAT
1.53
possibility12_0_4
FAIL
1.53
possibility8_0_4
FAIL
1.53
ring6_64
SAT
1.54
Core1108_tbm_02.tex.moduleQ3.2S.000026
UNSAT
1.54
Core1108_tbm_02.tex.moduleQ3.2S.000099
UNSAT
1.54
Core1108_tbm_02.tex.moduleQ3.2S.000108
UNSAT
1.54
Core1108_tbm_02.tex.moduleQ3.2S.000098
UNSAT
1.56
Core1108_tbm_02.tex.moduleQ3.2S.000007
UNSAT
1.57
flipflop-6-c
UNSAT
1.57
ring6_65
SAT
1.57
W4-Umbrella_tbm_05.tex.moduleQ3.8S.000001
UNSAT
1.65
k_ph_p-5
UNSAT
1.7
counter7_64
SAT
1.7
Umbrella_tbm_24.tex.moduleQ2.1S.000136
UNSAT
1.74
Umbrella_tbm_24.tex.moduleQ2.1S.000188
UNSAT
1.75
Umbrella_tbm_24.tex.moduleQ2.1S.000022
UNSAT
1.75
W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003
UNSAT
1.77
Umbrella_tbm_29.tex.moduleQ2.2S.000001
UNSAT
1.87
C432.blif_0.10_1.00_0_1_out_exact
SAT
1.89
possibility1_0_5
FAIL
1.93
assertion11_0_5
FAIL
1.93
consistency_0_5
FAIL
1.93
possibility4_0_5
FAIL
1.93
assertion6_0_5
FAIL
1.94
possibility2_0_5
FAIL
1.94
assertion1_0_5
FAIL
1.94
assertion5_0_5
FAIL
1.94
assertion7_0_5
FAIL
1.94
possibility11_0_5
FAIL
1.94
possibility9_0_5
FAIL
1.94
possibility7_0_5
FAIL
1.94
possibility10_0_5
FAIL
1.94
assertion8_0_5
FAIL
1.95
assertion3_0_5
FAIL
1.95
assertion12_0_5
FAIL
1.95
assertion10_0_5
FAIL
1.95
assertion4_0_5
FAIL
1.95
assertion9_0_5
FAIL
1.95
possibility3_0_5
FAIL
1.95
possibility6_0_5
FAIL
1.95
assertion2_0_5
FAIL
1.95
possibility12_0_5
FAIL
1.96
possibility5_0_5
FAIL
1.97
Umbrella_tbm_23.tex.moduleQ1.2S.000001
UNSAT
1.97
possibility8_0_5
FAIL
1.98
k_lin_p-9
UNSAT
2.06
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004
SAT
2.13
possibility7_0_3
FAIL
2.16
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004
SAT
2.22
counter8_64
SAT
2.42
possibility10_0_6
FAIL
2.45
consistency_0_6
FAIL
2.46
possibility2_0_6
FAIL
2.46
assertion11_0_6
FAIL
2.46
assertion10_0_6
FAIL
2.46
assertion12_0_6
FAIL
2.47
assertion6_0_6
FAIL
2.47
possibility6_0_6
FAIL
2.47
assertion9_0_6
FAIL
2.47
possibility1_0_6
FAIL
2.47
possibility11_0_6
FAIL
2.47
possibility4_0_6
FAIL
2.47
assertion5_0_6
FAIL
2.48
Umbrella_tbm_14.tex.moduleQ2.1S.000792
UNSAT
2.48
assertion4_0_6
FAIL
2.48
Umbrella_tbm_26.tex.moduleQ3.2S.000041
UNSAT
2.48
assertion1_0_6
FAIL
2.48
assertion2_0_6
FAIL
2.48
Umbrella_tbm_14.tex.moduleQ2.2S.000002
UNSAT
2.48
Umbrella_tbm_14.tex.moduleQ2.1S.000812
UNSAT
2.49
Umbrella_tbm_14.tex.moduleQ2.2S.000001
UNSAT
2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000720
UNSAT
2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000757
UNSAT
2.49
possibility5_0_6
FAIL
2.49
Umbrella_tbm_14.tex.moduleQ2.1S.000808
UNSAT
2.49
possibility12_0_6
FAIL
2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000787
UNSAT
2.5
assertion7_0_6
FAIL
2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000773
UNSAT
2.5
assertion3_0_6
FAIL
2.5
Umbrella_tbm_14.tex.moduleQ2.2S.000003
UNSAT
2.5
Umbrella_tbm_14.tex.moduleQ2.1S.000749
UNSAT
2.51
Umbrella_tbm_26.tex.moduleQ3.2S.000037
UNSAT
2.51
possibility9_0_6
FAIL
2.51
assertion8_0_6
FAIL
2.51
Umbrella_tbm_26.tex.moduleQ3.2S.000009
UNSAT
2.52
Umbrella_tbm_26.tex.moduleQ3.2S.000020
UNSAT
2.52
Umbrella_tbm_26.tex.moduleQ3.2S.000014
UNSAT
2.52
possibility8_0_6
FAIL
2.54
s499_d15_s
SAT
2.56
possibility7_0_6
FAIL
2.76
BLOCKS4iii.6
UNSAT
2.82
k_ph_n-6
SAT
2.82
possibility7_0_7
FAIL
3.04
consistency_0_7
FAIL
3.04
possibility9_0_7
FAIL
3.05
BLOCKS3iii.5
SAT
3.05
assertion11_0_7
FAIL
3.05
possibility2_0_7
FAIL
3.05
possibility5_0_7
FAIL
3.06
assertion5_0_7
FAIL
3.06
possibility3_0_7
FAIL
3.06
assertion10_0_7
FAIL
3.06
possibility10_0_7
FAIL
3.07
possibility1_0_7
FAIL
3.07
assertion3_0_7
FAIL
3.07
possibility11_0_7
FAIL
3.07
assertion12_0_7
FAIL
3.07
assertion7_0_7
FAIL
3.07
assertion1_0_7
FAIL
3.07
stmt27_16_97
UNSAT
3.07
assertion9_0_7
FAIL
3.07
possibility6_0_7
FAIL
3.08
possibility4_0_7
FAIL
3.08
assertion6_0_7
FAIL
3.08
assertion2_0_7
FAIL
3.08
assertion8_0_7
FAIL
3.09
assertion4_0_7
FAIL
3.1
possibility3_0_6
FAIL
3.12
possibility12_0_7
FAIL
3.12
possibility8_0_7
FAIL
3.16
Core1108_tbm_09.tex.moduleQ3.9S.000001
UNSAT
3.42
Core1108_tbm_09.tex.moduleQ3.10S.000001
UNSAT
3.42
Core1108_tbm_09.tex.moduleQ3.2S.000011
UNSAT
3.44
possibility1_0_8
FAIL
3.71
ken.flash^10.C-f3
UNSAT
3.71
assertion11_0_8
FAIL
3.72
assertion12_0_8
FAIL
3.72
possibility6_0_8
FAIL
3.73
assertion1_0_8
FAIL
3.73
consistency_0_8
FAIL
3.73
possibility4_0_8
FAIL
3.73
possibility3_0_8
FAIL
3.73
assertion7_0_8
FAIL
3.74
possibility7_0_8
FAIL
3.74
assertion9_0_8
FAIL
3.74
possibility11_0_8
FAIL
3.75
possibility5_0_8
FAIL
3.75
assertion3_0_8
FAIL
3.76
assertion6_0_8
FAIL
3.76
assertion2_0_8
FAIL
3.77
assertion10_0_8
FAIL
3.77
assertion4_0_8
FAIL
3.78
assertion5_0_8
FAIL
3.78
possibility12_0_8
FAIL
3.81
possibility9_0_8
FAIL
3.82
assertion8_0_8
FAIL
3.82
counter7_129
SAT
3.85
possibility8_0_8
FAIL
3.87
k_lin_p-10
UNSAT
3.95
Core1108_tbm_09.tex.moduleQ3.2S.000005
UNSAT
3.97
C880.blif_0.10_1.00_0_0_out_exact
UNSAT
3.98
toilet_a_10_05.3
UNSAT
4.07
possibility10_0_8
FAIL
4.07
driverlog03_7
SAT
4.14
Core1108_tbm_09.tex.moduleQ3.2S.000007
UNSAT
4.15
s298_d12_s
SAT
4.16
Core1108_tbm_09.tex.moduleQ3.2S.000003
UNSAT
4.16
counter7_128
SAT
4.19
nusmv.tcas^3.B-f2
SAT
4.2
possibility2_0_8
FAIL
4.28
Core1108_tbm_09.tex.moduleQ3.2S.000010
UNSAT
4.31
s298_d14_s
SAT
4.44
assertion11_0_9
FAIL
4.51
possibility4_0_9
FAIL
4.56
possibility2_0_9
FAIL
4.56
possibility10_0_9
FAIL
4.56
assertion12_0_9
FAIL
4.56
assertion1_0_9
FAIL
4.57
possibility11_0_9
FAIL
4.57
possibility9_0_9
FAIL
4.57
consistency_0_9
FAIL
4.58
assertion3_0_9
FAIL
4.58
assertion7_0_9
FAIL
4.58
possibility6_0_9
FAIL
4.59
assertion10_0_9
FAIL
4.59
s499_d17_s
SAT
4.6
assertion2_0_9
FAIL
4.6
possibility7_0_9
FAIL
4.6
assertion4_0_9
FAIL
4.61
assertion6_0_9
FAIL
4.62
assertion9_0_9
FAIL
4.62
assertion8_0_9
FAIL
4.63
counter8_128
SAT
4.63
assertion5_0_9
FAIL
4.64
possibility5_0_9
FAIL
4.66
possibility12_0_9
FAIL
4.66
possibility8_0_9
FAIL
4.66
possibility1_0_9
FAIL
4.76
connect_6x5_5_D
UNSAT
4.88
Umbrella_tbm_25.tex.moduleQ3.2S.000052
UNSAT
4.88
Umbrella_tbm_25.tex.moduleQ3.2S.000063
UNSAT
4.89
Umbrella_tbm_25.tex.moduleQ3.2S.000120
UNSAT
4.91
CHAIN14v.15
SAT
4.98
possibility3_0_9
FAIL
5.05
assertion10_0_10
FAIL
5.43
assertion11_0_10
FAIL
5.44
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-003
UNSAT
5.44
possibility1_0_10
FAIL
5.45
assertion6_0_10
FAIL
5.46
assertion12_0_10
FAIL
5.47
possibility5_0_10
FAIL
5.47
possibility3_0_10
FAIL
5.47
assertion9_0_10
FAIL
5.47
possibility7_0_10
FAIL
5.48
possibility11_0_10
FAIL
5.48
possibility4_0_10
FAIL
5.49
consistency_0_10
FAIL
5.5
possibility10_0_10
FAIL
5.5
possibility6_0_10
FAIL
5.51
assertion3_0_10
FAIL
5.51
possibility2_0_10
FAIL
5.51
assertion2_0_10
FAIL
5.52
assertion8_0_10
FAIL
5.53
assertion1_0_10
FAIL
5.54
possibility9_0_10
FAIL
5.54
assertion5_0_10
FAIL
5.55
assertion7_0_10
FAIL
5.56
s1269_d8_s
SAT
5.57
assertion4_0_10
FAIL
5.58
possibility12_0_10
FAIL
5.6
possibility8_0_10
FAIL
5.67
c4_BMC_p1_k32
SAT
5.8
s386_d8_u
UNSAT
5.93
lut4_AND_fXOR
UNSAT
6.01
BLOCKS3ii.5.3
SAT
6.26
Umbrella_tbm_25.tex.moduleQ3.2S.000075
UNSAT
6.38
arbiter-06-comp-error02-qbf-hardness-depth-5
UNSAT
7.1
par8-4-50
UNSAT
7.41
BLOCKS3i.5.3
UNSAT
7.56
term1.blif_0.10_1.00_0_1_out_exact
SAT
7.73
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-005
UNSAT
7.78
fpu-10Xh-error01-uniform-depth-5
UNSAT
8.03
vonNeumann-ripple-carry-5-c
UNSAT
8.33
CHAIN16v.17
SAT
8.35
term1.blif_0.10_0.20_0_0_out_exact
UNSAT
8.54
tlc03-uniform-depth-21
UNSAT
9.34
fpu-10Xe-correct01-nonuniform-depth-6
UNSAT
9.67
assertion11_0_1
UNSAT
10.22
s386_d10_u
UNSAT
10.23
assertion12_0_1
UNSAT
10.33
s510_d11_s
SAT
10.47
connect_7x6_4_W
UNSAT
10.64
emptyroom_e3_ser--opt-20_
SAT
13.3
szymanski-5-s
UNSAT
13.57
connect_8x7_7_W
UNSAT
13.74
term1.blif_0.10_0.20_0_1_inp_exact
SAT
13.84
counter8_256
SAT
14.47
counter8_257
SAT
15.22
s386_d12_u
UNSAT
15.63
ring_r3_ser--opt-8_
SAT
17.09
assertion5_0_1
UNSAT
18.25
vonNeumann-ripple-carry-6-c
UNSAT
19.38
lognBWLARGEA1
UNSAT
19.9
k_branch_n-2
SAT
20.6
CHAIN20v.21
SAT
20.89
k_lin_p-19
UNSAT
24.63
vonNeumann-ripple-carry-7-c
UNSAT
26.06
flipflop-10-c
UNSAT
27.79
filesys_smbmrx_cvsndrcv.c
UNSAT
30.25
CHAIN22v.23
SAT
30.93
s820_d8_s
SAT
33.82
C432.blif_0.10_0.20_0_1_inp_exact
SAT
35.21
C499.blif_0.10_1.00_0_0_out_exact
UNSAT
35.42
CHAIN23v.24
SAT
37.64
tlc01-uniform-depth-73
UNSAT
41.86
k_dum_n-1
SAT
42.16
flipflop-11-c
UNSAT
47.1
stmt19_90_266
UNSAT
56.42
lut4_2_f2
UNSAT
56.43
lognBWLARGEB1
UNSAT
57.36
p10-10.pddl_planlen=6
UNSAT
57.71
k_ph_n-9
SAT
59.07
c4_BMC_p2_k128
UNSAT
87.6
tlc03-uniform-depth-52
UNSAT
89.05
k_lin_n-3
SAT
92.28
lut4_2_fXOR
SAT
101.94
s713_d6_s
SAT
102.82
C432.blif_0.10_1.00_0_0_out_exact
UNSAT
130.24
vonNeumann-ripple-carry-11-c
UNSAT
130.79
s820_d11_u
UNSAT
133.31
stmt21_79_304
UNSAT
144.62
szymanski-6-s
UNSAT
151.14
s820_d12_u
UNSAT
165.89
s499_d22_u
UNSAT
167.87
vonNeumann-ripple-carry-12-c
UNSAT
178.24
ev-pr-6x6-9-5-0-1-2-s
FAIL
193.02
s510_d24_s
SAT
198.3
ev-pr-6x6-11-5-0-1-2-s
FAIL
202.23
query51_query50_1344
UNSAT
206.46
s3330_d3_s
SAT
206.57
ev-pr-6x6-13-5-0-1-2-s
FAIL
211.72
par16-1-50
UNSAT
219.39
ev-pr-6x6-17-5-0-1-2-s
FAIL
231.42
s499_d24_u
UNSAT
246.17
s820_d15_u
UNSAT
274.38
s3330_d4_s
SAT
277.18
C432.blif_0.10_0.20_0_0_out_exact
UNSAT
289.15
C880.blif_0.10_0.20_0_1_out_exact
UNSAT
317.82
texas.PI_main^05.E-f3
SAT
339.49
s641_d6_s
SAT
407.75
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf03.01X-QBF.BB1-Zi.BB2-Zi.BB3-01X.with-IOC.unfold-005
UNSAT
429.84
p10-10.pddl_planlen=10
SAT
445.13
s510_d31_s
SAT
483.5
c3_Debug_s3_f2_e2_v2
FAIL
580.51
pipesnotankage18_8
FAIL
585.31
p20-20.pddl_planlen=23
FAIL
588.71
c2_BMC_p1_k2048
FAIL
593.11
pipesnotankage14_10
FAIL
593.41
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
593.71
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
594.51
c4_Debug_s5_f2_e2_v1
FAIL
594.81
c2_Debug_s3_f1_e1_v2
FAIL
595.71
c1_Debug_s5_f1_e1_v2
FAIL
596.01
fpu-10Xh-correct04-nonuniform-depth-27
FAIL
596.22
c4_Debug_s3_f2_e2_v2
FAIL
596.22
fpu-10Xe-correct01-uniform-depth-22
FAIL
596.61
fpu-10Xe-correct01-nonuniform-depth-24
FAIL
596.71
qshifter_8
FAIL
598.42
p20-5.pddl_planlen=32
FAIL
598.71
c5_BMC_p2_k128
FAIL
598.71
connect_9x8_6_R
FAIL
598.91
b20_C_3_2
FAIL
598.91
ring_r6_ser--opt-17_
FAIL
598.91
szymanski-16-s
FAIL
599.01
c5_BMC_p2_k64
FAIL
599.12
ev-pr-8x8-15-7-0-1-2-lg
FAIL
599.21
network_irda_miniport_nscirda_comm.c
FAIL
599.21
szymanski-14-s
FAIL
599.21
ev-pr-4x4-17-3-0-0-1-s
FAIL
599.21
connect_8x7_6_R
FAIL
599.31
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
599.31
ev-pr-4x4-13-3-0-0-1-s
FAIL
599.31
ev-pr-4x4-15-3-0-0-1-s
FAIL
599.31
input_pnpi8042_moudep.c
FAIL
599.31
s3330_d12_u
FAIL
599.31
ev-pr-8x8-19-7-0-1-2-lg
FAIL
599.31
qshifter_7
FAIL
599.32
dungeon_i10-m10-u10-v0.pddl_planlen=187
FAIL
599.42
s3330_d9_s
FAIL
599.42
k14_2_3
FAIL
599.42
query42_query06_1344n
FAIL
599.42
ev-pr-8x8-13-7-0-1-2-lg
FAIL
599.42
k12_4_2
FAIL
599.43
s1269_d15_u
FAIL
599.52
stmt17_86_98
FAIL
599.52
audio_ddksynth_csynth2.cpp
FAIL
599.52
ev-pr-4x4-7-3-0-0-1-s
FAIL
599.52
s1269_d12_u
FAIL
599.52
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
599.52
ev-pr-6x6-11-5-0-1-2-lg
FAIL
599.52
ev-pr-6x6-17-5-0-1-2-lg
FAIL
599.52
emptyroom_e4_ser--opt-44_
FAIL
599.52
s510_d36_s
FAIL
599.52
s15850_PR_8_50
FAIL
599.52
b22_PR_8_20
FAIL
599.52
b21_C_3_206
FAIL
599.52
ev-pr-6x6-19-5-0-1-2-lg
FAIL
599.52
Adder2-16-s
FAIL
599.53
incrementer-enc02-uniform-depth-58
FAIL
599.53
ev-pr-8x8-7-7-0-1-2-lg
FAIL
599.53
s1269_d13_u
FAIL
599.53
k_ph_n-16
FAIL
599.61
szymanski-8-s
FAIL
599.61
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
599.61
ev-pr-4x4-11-3-0-0-1-lg
FAIL
599.61
s1196_d5_u
FAIL
599.61
cube_c7_ser--opt-24_
FAIL
599.61
f600-50
FAIL
599.61
texas.PI_main^08.E-f3
FAIL
599.61
k_d4_n-20
FAIL
599.61
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
599.61
gttt_2_1_00102030_4x4_torus_b
FAIL
599.61
stmt52_244_394
FAIL
599.61
test2_quant_squaring2
FAIL
599.61
ev-pr-4x4-13-3-0-0-1-lg
FAIL
599.61
k_branch_p-10
FAIL
599.61
k_branch_p-11
FAIL
599.61
k_ph_p-19
FAIL
599.61
k_lin_n-17
FAIL
599.61
s298_d22_u
FAIL
599.61
s09234_PR_8_2
FAIL
599.61
k_branch_p-16
FAIL
599.61
arbiter-10-comp-error01-qbf-hardness-depth-10
FAIL
599.61
b20_PR_7_20
FAIL
599.61
query44_query26_1344n
FAIL
599.61
dungeon_i10-m5-u10-v0.pddl_planlen=23
FAIL
599.61
possibility8_0_1
FAIL
599.61
rankfunc17_unsigned_16
FAIL
599.61
incrementer-enc07-uniform-depth-25
FAIL
599.61
ken.flash^08.C-d4
FAIL
599.61
stmt28_68_81
FAIL
599.61
possibility2_0_1
FAIL
599.61
assertion3_0_1
FAIL
599.61
ev-pr-6x6-9-5-0-1-2-lg
FAIL
599.61
test2_quant_squaring3
FAIL
599.61
stmt17_70_90
FAIL
599.61
s298_d19_u
FAIL
599.61
stmt17_63_82
FAIL
599.61
stmt19_64_99
FAIL
599.61
cnt14
FAIL
599.61
possibility3_0_1
FAIL
599.61
cache-coherence-2-fixpoint-6
FAIL
599.62
k_ph_n-21
FAIL
599.62
adder-12-unsat
FAIL
599.62
adder-10-sat
FAIL
599.62
adder-14-sat
FAIL
599.62
sortnetsort9.AE.stepl.012
FAIL
599.62
k_ph_p-12
FAIL
599.62
s298_d25_u
FAIL
599.62
tlc04-nonuniform-depth-56
FAIL
599.62
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
599.63
incrementer-enc08-uniform-depth-33
FAIL
599.63
rankfunc5_unsigned_64
FAIL
599.71
k_t4p_p-4
FAIL
599.71
tree-exa2-20
FAIL
599.71
possibility9_0_1
FAIL
599.71
uclid-pipe3a
FAIL
599.71
Umbrella_tbm_24.tex.module.000131
FAIL
599.71
rankfunc14_signed_64
FAIL
599.71
impl10
FAIL
599.71
rankfunc33_signed_32
FAIL
599.71
C499.blif_0.10_0.20_0_1_out_exact
FAIL
599.71
k8_2_3
FAIL
599.71
possibility4_0_1
FAIL
599.71
ii32b1-00
FAIL
599.71
stmt41_160_235
FAIL
599.71
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
599.71
tree-exa2-25
FAIL
599.71
possibility12_0_1
FAIL
599.71
impl08
FAIL
599.71
impl16
FAIL
599.71
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
599.71
lut4_3_fAND
FAIL
599.71
rankfunc13_unsigned_64
FAIL
599.71
possibility5_0_1
FAIL
599.71
k_path_p-16
FAIL
599.71
tree-exa2-45
FAIL
599.71
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
599.71
possibility7_0_1
FAIL
599.71
possibility11_0_1
FAIL
599.71
k_d4_p-20
FAIL
599.71
C5315.blif_0.10_0.20_0_1_inp_exact
FAIL
599.71
k_t4p_n-2
FAIL
599.71
k_d4_n-14
FAIL
599.71
k_d4_n-15
FAIL
599.71
k_d4_p-17
FAIL
599.71
k_d4_p-13
FAIL
599.71
k_d4_p-11
FAIL
599.71
k_dum_n-18
FAIL
599.71
assertion10_0_1
FAIL
599.71
k_path_p-14
FAIL
599.71
k_path_p-10
FAIL
599.71
k_dum_n-17
FAIL
599.71
k_dum_p-2
FAIL
599.71
k_ph_n-11
FAIL
599.71
k_ph_p-10
FAIL
599.71
k_poly_n-18
FAIL
599.71
k_dum_n-12
FAIL
599.71
k_poly_p-4
FAIL
599.71
k_poly_p-19
FAIL
599.71
toilet_c_10_01.17
FAIL
599.71
k_branch_n-10
FAIL
599.71
k_poly_p-7
FAIL
599.71
k_poly_n-17
FAIL
599.71
k_poly_n-7
FAIL
599.71
k_poly_n-2
FAIL
599.71
k_branch_n-3
FAIL
599.71
k_branch_p-5
FAIL
599.71
k_dum_p-3
FAIL
599.71
k_dum_p-6
FAIL
599.71
k_path_n-9
FAIL
599.71
k_grz_p-13
FAIL
599.71
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
599.71
k_path_n-5
FAIL
599.71
tlc03-nonuniform-depth-17
FAIL
599.71
k_lin_n-6
FAIL
599.71
k_lin_n-5
FAIL
599.71
incrementer-enc03-nonuniform-depth-24
FAIL
599.71
small-swap2-fixpoint-4
FAIL
599.71
small-synabs-fixpoint-9
FAIL
599.71
small-swap1-fixpoint-3
FAIL
599.71
gttt_1_1_001020_3x3_w
FAIL
599.71
gttt_2_1_000111_3x3_torus_b
FAIL
599.71
k_path_n-13
FAIL
599.71
k_path_p-5
FAIL
599.71
assertion1_0_1
FAIL
599.71
gttt_1_1_000111_3x3_torus_w
FAIL
599.71
k_grz_n-5
FAIL
599.71
k_grz_n-10
FAIL
599.71
k_grz_p-18
FAIL
599.71
k_grz_p-10
FAIL
599.71
k_grz_p-11
FAIL
599.71
p20-1.pddl_planlen=24
FAIL
599.71
lights3_035_0_051
FAIL
599.71
lights3_035_0_027
FAIL
599.71
sdlx-fixpoint-3
FAIL
599.71
Umbrella_tbm_05.tex.module.000039
FAIL
599.71
possibility1_0_1
FAIL
599.71
ken.oop^2.C-d4
FAIL
599.71
k_t4p_p-12
FAIL
599.71
test3_quant_squaring4
FAIL
599.71
test3_quant_squaring2
FAIL
599.71
k_t4p_p-15
FAIL
599.71
assertion7_0_1
FAIL
599.71
s713_d8_u
FAIL
599.71
s641_d8_u
FAIL
599.71
k_poly_p-16
FAIL
599.71
assertion6_0_1
FAIL
599.71
k_dum_p-12
FAIL
599.71
assertion8_0_1
FAIL
599.71
ev-pr-4x4-7-3-0-0-1-lg
FAIL
599.71
test1_quant_squaring3
FAIL
599.71
s713_d7_u
FAIL
599.71
consistency_0_1
FAIL
599.71
k_t4p_p-16
FAIL
599.71
sortnetsort9.v.stepl.007
FAIL
599.71
ev-pr-4x4-9-3-0-0-1-lg
FAIL
599.71
k_lin_n-8
FAIL
599.71
assertion9_0_1
FAIL
599.71
sortnetsort8.v.stepl.009
FAIL
599.71
s1196_d3_u
FAIL
599.71
sortnetsort10.v.stepl.005
FAIL
599.71
k_path_n-12
FAIL
599.71
k_dum_p-16
FAIL
599.71
s641_d7_u
FAIL
599.71
k_poly_p-8
FAIL
599.71
k_path_n-16
FAIL
599.71
k_grz_n-21
FAIL
599.71
k_t4p_p-18
FAIL
599.71
cnt10
FAIL
599.71
assertion4_0_1
FAIL
599.71
k_t4p_n-13
FAIL
599.71
k_t4p_n-5
FAIL
599.71
cnt16r
FAIL
599.71
k_t4p_n-15
FAIL
599.71
k_grz_n-20
FAIL
599.71
C499.blif_0.10_0.20_0_0_out_exact
FAIL
599.71
k_branch_n-8
FAIL
599.71
k_t4p_n-14
FAIL
599.71
k_poly_n-21
FAIL
599.71
assertion2_0_1
FAIL
599.71
k5_2_3
FAIL
599.72
gttt_2_2_001020_4x4_w
FAIL
599.72
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
599.72
k_d4_n-2
FAIL
599.81
k_d4_p-8
FAIL
599.81
k_dum_n-5
FAIL
599.81
tree-exa2-35
FAIL
599.81
impl20
FAIL
599.81
uclid-pipe2
FAIL
599.81
sortnetsort9.v.stepl.005
FAIL
599.81
k_grz_n-2
FAIL
599.81
cnt05
FAIL
599.81
s01238_PR_8_2
FAIL
599.81
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
599.81
impl12
FAIL
599.81
k_grz_p-17
FAIL
599.81
k_branch_n-12
FAIL
600
possibility10_0_1
FAIL
600
k_branch_p-6
FAIL
600
possibility6_0_1
FAIL
600
Contact
|
Organization
|
Links
|
Citing QBFLIB