Instances solved by GhostQ_PG___cegar_qcir_2018
QBFEVAL'18 - Prenex non-CNF Track

InstanceResultTime
query71_query15_1133UNSAT0
query30_eequery_1133SAT0
pg-hkb-2UNSAT0
query04_query03_1133UNSAT0
query51_query48_1133UNSAT0.09
query50_query49_1133UNSAT0.09
pg-hkb-3UNSAT0.11
query64_query31_1133UNSAT0.14
driver_d9n.unsatUNSAT0.18
ntrivil_query54_1133SAT0.18
pg-hkb-4UNSAT0.2
SR-unsat-02-01-06-1UNSAT0.22
query21_reachqu_1133SAT0.26
k0206272.s.oeSAT0.37
query09_trivial_1344SAT0.64
bs128n.unsatUNSAT0.76
k0201058.c.oeSAT0.83
stay22n.unsatUNSAT0.83
k0206272.h.oeSAT0.88
ltl2dpa_C26_comp2_REAL.unsatUNSAT0.96
6s318r_c0to15.unsatUNSAT1.15
ltl2dpa_C26_comp3_REAL.unsatUNSAT1.28
CM-sat-02-01-07-3SAT1.32
query44_query57_1133UNSAT1.59
random-qcir-1000-50-930UNSAT1.61
pg-hkb-5UNSAT1.62
nreachq_query02_1344UNSAT1.75
random-qcir-1000-50-983UNSAT2.24
random-qcir-1000-50-793UNSAT2.29
random-qcir-1000-50-393UNSAT2.3
query08_query26_1344SAT2.48
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.aspSAT2.51
random-qcir-1000-50-940UNSAT3.13
query03_query57_1344SAT3.13
driver_a9y.unsatUNSAT3.49
incrementer-enc08-uniform-depth-33SAT3.6
random-qcir-1000-50-267UNSAT4
k0206272.v.oeSAT4.02
random-qcir-1000-50-743UNSAT4.07
random-qcir-1000-50-441UNSAT4.08
random-qcir-1000-50-857UNSAT4.39
query49_query64_1133UNSAT4.74
random-qcir-1000-50-295UNSAT4.8
random-qcir-1000-50-98UNSAT4.98
random-qcir-1000-50-545UNSAT5.18
random-qcir-1000-50-134UNSAT5.41
k0226271.c.oeSAT5.48
pg-hkb-13FAIL5.52
random-qcir-1000-50-361UNSAT5.61
random-qcir-1000-50-275UNSAT5.65
random-qcir-1000-50-68UNSAT5.78
random-qcir-1000-50-970UNSAT5.99
k0026150.h.oeSAT6.06
jctc13-failUNSAT6.36
jctc6-passSAT6.37
random-qcir-1000-50-456UNSAT6.42
JP-sat-02-07-3SAT6.52
klieber2017q-104-26-t1UNSAT6.58
random-qcir-1000-50-846UNSAT6.61
random-qcir-1000-50-754UNSAT6.71
random-qcir-1000-50-658UNSAT6.98
k0225744.s.oeSAT7.28
pg-hkb-14FAIL7.3
klieber2017q-076-19-eqSAT7.37
klieber2017q-078-19-eqSAT7.43
random-qcir-1000-50-898UNSAT7.62
random-qcir-1000-50-428UNSAT7.87
pg-hkb-6UNSAT8.17
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.aspSAT8.68
random-qcir-1000-50-255UNSAT8.75
klieber2017q-108-27-t1UNSAT8.9
incrementer-enc07-uniform-depth-25UNSAT9.41
pg-hkb-15FAIL9.53
beemldelec4b1_c0to15.unsatUNSAT9.61
JP-sat-02-07-4SAT9.68
CM-sat-03-01-07-3SAT10
random-qcir-1000-50-473UNSAT10.12
klieber2017q-074-18-t1UNSAT10.25
klieber2017q-074-18-eqSAT11.51
query08_query64_1344SAT12.3
pg-hkb-16FAIL12.34
SR-sat-02-01-06-2SAT12.59
klieber2017q-086-21-eqSAT12.7
SR-sat-02-01-07-2SAT14.03
JP-sat-02-08-3SAT14.59
JP-unsat-02-06-3UNSAT14.86
pg-hkb-17FAIL15.59
jctc16-vals-0,2-passSAT16.15
DW-sat-06-20-1SAT16.76
klieber2017q-082-20-eqSAT18.59
klieber2017q-112-28-t1UNSAT18.82
pg-hkb-18FAIL19.59
klieber2017q-100-25-t1UNSAT20.79
jctc1-passSAT20.79
klieber2017q-080-20-t1UNSAT22.78
k0225418.v.oeSAT23.44
DWs-unsat-07-16-1UNSAT24.33
pg-hkb-19FAIL24.35
CM-sat-03-01-06-4SAT24.61
klieber2017q-092-23-t1UNSAT24.77
klieber2017q-100-25-eqSAT25.81
CM-sat-04-01-06-3SAT26.8
jctc4-failUNSAT27.29
k0225418.connected.oeSAT28.21
SR-unsat-02-01-05-2UNSAT29.13
pg-hkb-20FAIL30.02
load_full_3_comp3_REAL.unsatUNSAT30.98
genbuf5b4n.unsatUNSAT31.91
klieber2017q-096-24-t1UNSAT33.5
pg-hkb-21FAIL36.03
pg-hkb-7UNSAT36.1
DWs-unsat-08-17-1UNSAT38.26
klieber2017q-078-19-t1UNSAT42.86
load_3c_comp_comp7_REAL.unsatUNSAT43.8
pg-hkb-22FAIL44.12
amba2f9n.unsatUNSAT45.72
CM-sat-04-01-07-3SAT48.62
chess_solving_mate_in_2_1983_FIN-CH-4_01SAT53.68
jctc2-passSAT53.91
klieber2017q-104-26-eqSAT55.88
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.aspSAT56.04
klieber2017q-092-23-eqSAT56.99
pg-hkb-23FAIL57.31
DWs-unsat-08-18-1UNSAT60.78
pg-hkb-24FAIL63.04
klieber2017q-086-21-t1UNSAT63.97
klieber2017q-096-24-eqSAT65.52
DW-sat-08-24-1SAT70.52
pg-hkb-25FAIL72.74
klieber2017q-116-29-eqSAT79.01
pg-hkb-26FAIL86.47
DW-sat-08-22-1SAT88.15
DWs-unsat-09-19-1UNSAT93.11
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01SAT94.69
query33_query71_1344UNSAT99.77
DWs-sat-10-25-1SAT100.75
chess_solving_mate_in_2_2011_ISC-7B_01SAT109.07
CM-sat-04-01-06-4SAT111.39
DW-sat-09-26-1SAT111.85
chess_solving_mate_in_2_1996_FIN-CH-17_03SAT113.91
jctc8-passSAT129.83
DW-sat-08-23-1SAT145.45
CM-sat-07-01-06-3SAT160.7
pg-hkb-8UNSAT170.3
klieber2017q-084-21-t1UNSAT171.47
DW-unsat-09-22-1UNSAT175.49
query64_query58_1344UNSAT227.38
DWs-sat-10-24-1SAT242.81
incrementer-enc02-uniform-depth-58UNSAT243.71
klieber2017q-080-20-eqSAT245.51
oski3ub1i_c0to63.unsatUNSAT245.65
klieber2017q-112-28-eqSAT252.73
chess_solving_mate_in_2_2012_GER-CH-36-19_03SAT260.08
query48_query42_1344SAT297.11
genbuf9b4n.unsatUNSAT321.74
genbuf10b4y.unsatUNSAT336.89
jctc9-passSAT380.15
ev-pr-4x4-11-3-0-0-1-lgSAT386.43
gb_s2_r2_comp3_REAL.unsatUNSAT512.38
DW-unsat-10-25-1UNSAT529.34
SR-sat-02-01-06-3SAT545.15
DWs-unsat-11-23-1UNSAT576.48
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.aspSAT585.63
klieber2017q-116-29-t1UNSAT618.74
ev-pr-4x4-13-3-0-0-1-lgSAT628.61
CM-sat-07-01-06-4SAT630.49
query64_query55_1344UNSAT645.18
DWs-sat-10-23-1SAT664.36
pg-hkb-9UNSAT724.07
ev-pr-6x6-9-5-0-1-2-lgUNSAT791.92
DWs-unsat-11-24-1UNSAT895.07
chess_solving_mate_in_3_2009_FIN-CH-30_04FAIL900
query42_query57_1344FAIL900
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspFAIL900
test3_quant_squaring2FAIL900
jctc14-unrolled-failFAIL900
k0302060.c.oeFAIL900
chess_solving_mate_in_4_2009_SEROCK-OPEN_09FAIL900
chess_solving_mate_in_9_2003_RUS-CH_15FAIL900
small-swap1-fixpoint-3FAIL900
chess_solving_mate_in_7_2016_BEL-CH-23A_03FAIL900
ken.flash^08.C-d4FAIL900.01
cnt14FAIL900.01
chess_solving_mate_in_3_1999_WCSC-23_05FAIL900.01
chess_composing_6_template_01FAIL900.01
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.aspFAIL900.01
chess_composing_6_template_04FAIL900.01
query49_query58_1344FAIL900.01
ev-pr-8x8-7-7-0-1-2-lgFAIL900.01
sortnetsort9.v.stepl.005FAIL900.01
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.aspFAIL900.01
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.aspFAIL900.01
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.aspFAIL900.01
pg-hkb-10FAIL900.01
k0225418.c.oeFAIL900.01
rankfunc33_signed_32FAIL900.01
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL900.01
pg-hkb-12FAIL900.01
input_pnpi8042_moudep.cFAIL900.01
k0206272.connected.oeFAIL900.01
pipesnotankage18_8FAIL900.01
cycle_sched_6_2_1.satFAIL900.02
cycle_sched_6_2_1.unsatFAIL900.02
p20-20.pddl_planlen=23FAIL900.02
ev-pr-6x6-17-5-0-1-2-lgFAIL900.02
rankfunc17_unsigned_16FAIL900.02
load_full_3_comp3_REAL.satFAIL900.02
k0225418.h.oeFAIL900.02
k0026150.v.oeFAIL900.02
k0300663.h.oeFAIL900.02
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.aspFAIL900.02
k0300663.connected.oeFAIL900.02
ev-pr-6x6-11-5-0-1-2-lgFAIL900.02
chess_composing_8_template_42FAIL900.02
CM-unsat-07-01-06-2FAIL900.02
chess_solving_mate_in_3_2016_BEL-CH-23A_02FAIL900.02
JP-unsat-03-07-4FAIL900.02
jctc7-passFAIL900.02
jctc17-vals-0,2-passFAIL900.02
DW-unsat-11-26-1FAIL900.02
chess_composing_8_template_02FAIL900.02
JP-sat-03-08-4FAIL900.02
jctc11-passFAIL900.02
JP-unsat-03-08-5FAIL900.02
amba2f9n.satFAIL900.02
chess_composing_8_template_43FAIL900.03
small-swap2-fixpoint-4FAIL900.03
mult_bool_matrix_2_3_30.satFAIL900.03
SR-sat-03-01-08-2FAIL900.03
mult_bool_matrix_4_5_5.satFAIL900.03
jctc5-failFAIL900.03
chess_solving_mate_in_6_2011_SRB-CH_15FAIL900.03
rankfunc13_unsigned_64FAIL900.03
k0225744.connected.oeFAIL900.03
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.aspFAIL900.03
network_irda_miniport_nscirda_comm.cFAIL900.03
DWs-unsat-12-25-1FAIL900.03
test1_quant_squaring3FAIL900.03
genbuf5b4n.satFAIL900.03
DWs-unsat-13-28-1FAIL900.03
jctc15-unrolled-failFAIL900.03
oski3ub1i_c0to63.satFAIL900.03
k_branch_p-10FAIL900.03
pipesnotankage14_10FAIL900.03
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL900.04
chess_solving_mate_in_7_2011_SVK-CH-19_15FAIL900.04
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.aspFAIL900.04
p20-5.pddl_planlen=32FAIL900.04
sdlx-fixpoint-3FAIL900.04
pg-hkb-11FAIL900.04
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL900.04
filesys_smbmrx_cvsndrcv.cFAIL900.04
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspFAIL900.04
DWs-sat-15-35-1FAIL900.04
k0225682.c.oeFAIL900.04
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.aspFAIL900.04
mult_bool_matrix_2_3_30.unsatFAIL900.04
k_ph_n-21FAIL900.04
jctc18-vals-0,2-passFAIL900.04
JP-unsat-03-09-4FAIL900.04
query42_query64_1344FAIL900.04
chess_solving_mate_in_4_1999_GER-CH-23-6_14FAIL900.04
test2_quant_squaring2FAIL900.04
chess_composing_6_template_06FAIL900.04
k0300663.v.oeFAIL900.05
chess_composing_8_template_38FAIL900.05
k_branch_p-11FAIL900.05
k_ph_p-19FAIL900.05
cnt16rFAIL900.05
chess_composing_8_template_13FAIL900.05
k0300663.s.oeFAIL900.05
chess_solving_mate_in_6_2016_RUS-CH_15FAIL900.05
chess_solving_mate_in_5_1984_FIN-CH-5_09FAIL900.05
k0225744.h.oeFAIL900.05
ev-pr-4x4-15-3-0-0-1-sFAIL900.05
JP-sat-03-09-4FAIL900.05
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.aspFAIL900.05
mv16y.satFAIL900.05
DWs-sat-12-28-1FAIL900.05
stay24n.satFAIL900.05
beemldelec4b1_c0to15.satFAIL900.05
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.aspFAIL900.05
DW-unsat-11-27-1FAIL900.05
JP-unsat-03-08-3FAIL900.05
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL900.05
SR-sat-03-01-07-2FAIL900.05
jctc3-vals-0,2-passFAIL900.05
6s318r_c0to31.satFAIL900.05
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.aspFAIL900.05
sortnetsort9.AE.stepl.012FAIL900.06
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.aspFAIL900.06
CM-sat-07-01-07-3FAIL900.06
sortnetsort10.v.stepl.005FAIL900.06
nreachq_reachqu_2233FAIL900.06
audio_ddksynth_csynth2.cppFAIL900.06
k0026150.s.oeFAIL900.06
chess_solving_mate_in_7_2009_POL-CH-33_15FAIL900.06
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10FAIL900.06
k_ph_p-12FAIL900.07
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.aspFAIL900.07
klieber2017q-108-27-eqFAIL900.07
test2_quant_squaring3FAIL900.07
SR-unsat-03-01-06-2FAIL900.07
bs128n.satFAIL900.07
mult_bool_matrix_4_5_5.unsatFAIL900.07
k0225744.v.oeFAIL900.07
jctc10-failFAIL900.07
nreachq_reachqu_2133FAIL900.07
chess_solving_mate_in_6_1998_OST-CH-1_15FAIL900.07
chess_solving_mate_in_5_2012_NED-CH-18A_11FAIL900.07
chess_solving_mate_in_7_2005_GER-CH-29-12_15FAIL900.07
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.aspFAIL900.07
ken.oop^2.C-d4FAIL900.08
k_branch_n-12FAIL900.08
sortnetsort9.v.stepl.007FAIL900.08
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.aspFAIL900.08
k0026150.connected.oeFAIL900.08
k_branch_n-10FAIL900.08
chess_solving_mate_in_5_1996_UKR-CH-10_15FAIL900.08
k0225418.s.oeFAIL900.08
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.aspFAIL900.08
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.aspFAIL900.08
p20-1.pddl_planlen=24FAIL900.09
k_branch_p-16FAIL900.09
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.aspFAIL900.09
gb_s2_r2_comp3_REAL.satFAIL900.09
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.aspFAIL900.09
ltl2dpa_C26_comp3_REAL.satFAIL900.09
chess_solving_mate_in_4_1984_GBR-CH-5_04FAIL900.09
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03FAIL900.1
chess_solving_mate_in_8_2011_BEL-CH-19A_03FAIL900.1
qshifter_7FAIL900.11
query44_query58_1344FAIL900.11