Instances solved by qfun0.1
QBFEVAL'17 - Prenex non-CNF Track

InstanceResultTime
halfadder_match2.satSAT0.06
halfadder_match2.unsatUNSAT0.06
mvs16y.unsatUNSAT0.08
mutex-4-sSAT0.1
C499.blif_0.10_1.00_0_0_out_exactUNSAT0.16
stmt16_950_951SAT0.19
klieber2017q-076-19-t1UNSAT0.22
stmt41_738_749SAT0.26
ltl2dba_C2-6_comp3_REAL.unsatUNSAT0.27
klieber2017q-074-18-t1UNSAT0.3
klieber2017q-086-21-t1UNSAT0.31
klieber2017q-082-20-t1UNSAT0.33
klieber2017q-092-23-t1UNSAT0.36
klieber2017q-084-21-eqSAT0.39
klieber2017q-078-19-t1UNSAT0.39
szymanski-5-sUNSAT0.41
klieber2017q-080-20-t1UNSAT0.41
klieber2017q-086-21-eqSAT0.42
klieber2017q-088-22-t1UNSAT0.42
klieber2017q-100-25-t1UNSAT0.43
driver_d9y.unsatUNSAT0.45
klieber2017q-074-18-eqSAT0.46
mutex-32-sSAT0.46
klieber2017q-078-19-eqSAT0.48
klieber2017q-108-27-t1UNSAT0.5
klieber2017q-082-20-eqSAT0.5
klieber2017q-080-20-eqSAT0.5
klieber2017q-076-19-eqSAT0.51
klieber2017q-084-21-t1UNSAT0.51
klieber2017q-104-26-t1UNSAT0.54
klieber2017q-116-29-t1UNSAT0.55
klieber2017q-092-23-eqSAT0.58
klieber2017q-088-22-eqSAT0.59
stay24n.unsatUNSAT0.61
klieber2017q-096-24-eqSAT0.61
klieber2017q-096-24-t1UNSAT0.62
klieber2017q-112-28-t1UNSAT0.64
ltl2dpa_C26_comp2_REAL.unsatUNSAT0.64
klieber2017q-112-28-eqSAT0.75
consistency_0_2FAIL0.81
possibility10_0_2FAIL0.81
klieber2017q-100-25-eqSAT0.81
assertion12_0_2FAIL0.82
klieber2017q-104-26-eqSAT0.87
klieber2017q-108-27-eqSAT0.88
mutex-64-sSAT0.91
BLOCKS4iii.6UNSAT1.03
CHAIN20v.21SAT1.1
assertion12_0_1UNSAT1.14
possibility6_0_3FAIL1.16
consistency_0_3FAIL1.16
possibility7_0_3FAIL1.17
assertion7_0_3FAIL1.18
possibility3_0_3FAIL1.18
possibility1_0_3FAIL1.18
assertion9_0_3FAIL1.18
incrementer-enc07-uniform-depth-25UNSAT1.19
assertion6_0_3FAIL1.19
assertion2_0_3FAIL1.19
C499.blif_0.10_0.20_0_1_out_exactUNSAT1.36
szymanski-6-sUNSAT1.38
CHAIN22v.23SAT1.44
incrementer-enc08-uniform-depth-33SAT1.47
C499.blif_0.10_0.20_0_0_out_exactUNSAT1.5
consistency_0_4FAIL1.57
assertion7_0_4FAIL1.59
possibility5_0_4FAIL1.59
assertion1_0_4FAIL1.6
CHAIN23v.24SAT1.66
SR-unsat-03-01-07-1UNSAT2.03
consistency_0_5FAIL2.05
assertion2_0_5FAIL2.07
possibility4_0_5FAIL2.08
C880.blif_0.10_1.00_0_0_inp_exactUNSAT2.44
consistency_0_6FAIL2.62
assertion3_0_6FAIL2.63
assertion10_0_6FAIL2.64
possibility7_0_6FAIL2.64
possibility3_0_6FAIL2.65
assertion2_0_6FAIL2.65
klieber2017q-116-29-eqSAT2.85
incrementer-enc02-uniform-depth-58UNSAT3.18
possibility4_0_7FAIL3.26
possibility11_0_7FAIL3.26
assertion11_0_7FAIL3.27
assertion9_0_7FAIL3.27
consistency_0_7FAIL3.27
possibility6_0_7FAIL3.28
possibility10_0_7FAIL3.3
possibility8_0_7FAIL3.37
JP-unsat-02-07-2UNSAT3.78
consistency_0_8FAIL3.99
possibility1_0_8FAIL3.99
assertion2_0_8FAIL4.03
assertion1_0_9FAIL4.87
consistency_0_9FAIL4.88
assertion5_0_9FAIL4.91
possibility5_0_9FAIL4.92
assertion10_0_9FAIL4.95
load_3c_comp_comp7_REAL.unsatUNSAT5.21
assertion1_0_10FAIL5.89
consistency_0_10FAIL5.92
possibility6_0_10FAIL5.93
assertion4_0_10FAIL5.97
sortnetsort9.AE.stepl.012UNSAT6.19
szymanski-8-sUNSAT6.91
driver_a9n.unsatUNSAT7.01
b20_PR_7_20SAT7.09
cube_c7_ser--opt-24_SAT7.89
oski3ub5i_c0to255.unsatUNSAT7.89
beemldelec4b1_c0to127.unsatUNSAT8.11
b21_C_3_206SAT8.64
filesys_smbmrx_cvsndrcv.cUNSAT10.05
amba2f9n.unsatUNSAT15.21
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.aspSAT20.57
JP-unsat-02-06-3UNSAT20.7
sortnetsort9.v.stepl.007SAT26.97
b22_PR_8_20SAT28.58
k_ph_p-12UNSAT31.59
uclid-pipe3aSAT37.26
stmt28_68_81SAT39.52
stmt17_63_82SAT45.21
stmt17_70_90SAT48.81
stmt19_64_99SAT50.58
DW-sat-08-23-1SAT50.75
SR-unsat-04-01-08-1UNSAT54.19
DW-sat-08-24-1SAT57.07
stay24n.satSAT64.92
fpu-10Xe-correct01-nonuniform-depth-24UNSAT72.62
p20-1.pddl_planlen=24UNSAT80.37
stmt17_86_98SAT88.31
fpu-10Xh-correct04-nonuniform-depth-27UNSAT93.23
DWs-sat-10-24-1SAT94.19
k_ph_n-21SAT97.07
c2_BMC_p1_k2048SAT106.98
emptyroom_e4_ser--opt-44_SAT109.72
ev-pr-8x8-7-7-0-1-2-lgUNSAT109.8
load_full_4_comp3_REAL.unsatUNSAT111.07
DW-sat-08-22-1SAT136.32
CM-sat-07-01-07-3SAT137.68
mvs16y.satSAT146.82
CM-sat-07-01-06-3SAT161.58
p20-20.pddl_planlen=23SAT189.02
genbuf9b4n.unsatUNSAT189.67
DW-unsat-08-21-1UNSAT204.14
b20_C_3_2SAT205.56
driver_d9y.satSAT206.82
vonNeumann-ripple-carry-12-cUNSAT247.06
DW-unsat-09-22-1UNSAT255.53
genbuf10b4n.unsatUNSAT292.61
DWs-sat-10-25-1SAT313.86
dungeon_i15-m7-u4-v0.pddl_planlen=81UNSAT318.3
DWs-sat-10-23-1SAT323.67
k5_2_3SAT360.12
ken.flash^08.C-d4UNSAT377.82
pipesnotankage14_10UNSAT478.93
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.aspSAT531.18
DW-unsat-09-23-1UNSAT558.27
CM-sat-07-01-06-4SAT763.52
cycle_sched_4_7_1.unsatUNSAT796.48
szymanski-14-sUNSAT836.39
SR-sat-03-01-07-3FAIL882.05
c3_Debug_s3_f2_e2_v2FAIL882.61
pipesnotankage18_8FAIL885.12
CM-sat-17-01-06-4FAIL885.22
SR-sat-04-01-08-2FAIL891.83
CM-sat-17-01-07-3FAIL892.59
SR-unsat-04-01-07-2FAIL893.05
CM-sat-17-01-06-3FAIL893.83
CM-unsat-18-01-05-3FAIL894.31
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL894.75
CM-unsat-17-01-05-3FAIL895.01
c4_Debug_s5_f2_e2_v1FAIL895.04
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL895.41
c2_Debug_s3_f1_e1_v2FAIL895.83
ev-pr-6x6-17-5-0-1-2-sFAIL895.84
c1_Debug_s5_f1_e1_v2FAIL896.43
ev-pr-6x6-13-5-0-1-2-sFAIL896.91
DWs-unsat-11-23-1UNSAT898.65
mult_bool_matrix_17_17_17.unsatFAIL900
oski3ub5i_c0to255.satFAIL900
CM-unsat-07-01-05-3FAIL900
beemldelec4b1_c0to127.satFAIL900
mult_bool_matrix_17_17_17.satFAIL900
genbuf9b4n.satFAIL900
ltl2dba_C2-6_comp3_REAL.satFAIL900
mult_bool_matrix_10_9_11.satFAIL900
genbuf10b4n.satFAIL900
mult_bool_matrix_10_9_11.unsatFAIL900
ltl2dpa_C26_comp2_REAL.satFAIL900
CM-unsat-08-01-05-3FAIL900
driver_a9n.satFAIL900
cycle_sched_6_7_1.unsatFAIL900
cycle_sched_6_7_1.satFAIL900
CM-unsat-07-01-06-2FAIL900
JP-sat-03-09-5FAIL900
load_3c_comp_comp7_REAL.satFAIL900
DW-sat-19-44-1FAIL900
DW-sat-19-45-1FAIL900
DW-sat-19-46-1FAIL900
SR-sat-03-01-08-2FAIL900
CM-unsat-17-01-06-2FAIL900
JP-unsat-03-07-4FAIL900
DWs-unsat-11-24-1FAIL900
DWs-unsat-12-25-1FAIL900
connect_9x8_6_RFAIL900
DW-unsat-19-42-1FAIL900
load_full_4_comp3_REAL.satFAIL900
DW-unsat-19-43-1FAIL900
DW-unsat-20-44-1FAIL900
JP-sat-03-08-5FAIL900
JP-sat-03-09-4FAIL900
cycle_sched_4_7_1.satFAIL900
amba4b9y.unsatFAIL900
c5_BMC_p2_k64FAIL900
k_branch_p-10FAIL900
k_branch_n-10FAIL900
adder-12-unsatFAIL900
ev-pr-8x8-15-7-0-1-2-lgFAIL900
szymanski-16-sFAIL900
test3_quant_squaring2FAIL900
test3_quant_squaring4FAIL900
Adder2-16-sFAIL900
s3330_d9_sFAIL900
test1_quant_squaring3FAIL900
C5315.blif_0.10_0.20_0_0_out_exactFAIL900
k_branch_p-11FAIL900
k_ph_p-19FAIL900
c5_BMC_p2_k128FAIL900
ring_r6_ser--opt-17_FAIL900
ev-pr-6x6-17-5-0-1-2-lgFAIL900
c4_Debug_s3_f2_e2_v2FAIL900
sortnetsort9.v.stepl.005FAIL900
sortnetsort10.v.stepl.005FAIL900
ken.oop^2.C-d4FAIL900
s3330_d12_uFAIL900
s1269_d15_uFAIL900
cnt16rFAIL900
cnt14FAIL900
ev-pr-4x4-11-3-0-0-1-lgFAIL900
ev-pr-4x4-13-3-0-0-1-sFAIL900
ev-pr-4x4-17-3-0-0-1-sFAIL900
ev-pr-8x8-13-7-0-1-2-lgFAIL900
qshifter_7FAIL900
k_branch_n-12FAIL900
k_branch_p-16FAIL900
C6288.blif_0.10_0.20_0_0_out_exactFAIL900
ev-pr-6x6-11-5-0-1-2-sFAIL900
ev-pr-4x4-15-3-0-0-1-sFAIL900
adder-10-satFAIL900
connect_8x7_6_RFAIL900
ev-pr-6x6-11-5-0-1-2-lgFAIL900
adder-14-satFAIL900
ev-pr-4x4-13-3-0-0-1-lgFAIL900
C6288.blif_0.10_1.00_0_0_out_exactFAIL900
uclid-pipe2FAIL900
C6288.blif_0.10_0.20_0_1_out_exactFAIL900
ev-pr-8x8-19-7-0-1-2-lgFAIL900
C880.blif_0.10_0.20_0_1_inp_exactFAIL900
ev-pr-6x6-9-5-0-1-2-lgFAIL900
test2_quant_squaring3FAIL900
C6288.blif_0.10_0.20_0_0_inp_exactFAIL900
ev-pr-4x4-7-3-0-0-1-sFAIL900
ev-pr-6x6-9-5-0-1-2-sFAIL900
test2_quant_squaring2FAIL900
ev-pr-6x6-19-5-0-1-2-lgFAIL900
qshifter_8FAIL900
amba4b9y.satFAIL900
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.aspFAIL900
possibility8_0_1FAIL900
possibility5_0_1FAIL900
possibility10_0_1FAIL900
consistency_0_1FAIL900
s15850_PR_8_50FAIL900
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.aspFAIL900
amba2f9n.satFAIL900
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#408.w#4.s#3.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#392.w#6.s#4.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#376.w#2.s#4.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#344.w#4.s#5.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#336.w#4.s#5.aspFAIL900
query44_query26_1344nFAIL900
query42_query06_1344nFAIL900
p20-5.pddl_planlen=32FAIL900
rankfunc14_signed_64FAIL900
rankfunc5_unsigned_64FAIL900
rankfunc33_signed_32FAIL900
rankfunc17_unsigned_16FAIL900
rankfunc13_unsigned_64FAIL900
s1269_d12_uFAIL900
s1269_d13_uFAIL900
k14_2_3FAIL900
k8_2_3FAIL900
k12_4_2FAIL900
stmt41_160_235FAIL900
Umbrella_tbm_05.tex.module.000039FAIL900
Core1108_tbm_02.tex.moduleQ3.2S.000015FAIL900
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL900
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL900
audio_ddksynth_csynth2.cppFAIL900
network_irda_miniport_nscirda_comm.cFAIL900
input_pnpi8042_moudep.cFAIL900
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL900
small-swap2-fixpoint-4FAIL900
small-synabs-fixpoint-9FAIL900
small-swap1-fixpoint-3FAIL900
sdlx-fixpoint-3FAIL900
cache-coherence-2-fixpoint-6FAIL900
f600-50FAIL900