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

InstanceResultTime
query04_query03_1133UNSAT4.53
query30_eequery_1133SAT4.56
random-qcir-1000-50-134UNSAT4.57
query51_query48_1133UNSAT4.58
random-qcir-1000-50-267UNSAT4.59
random-qcir-1000-50-743UNSAT4.6
k0206272.s.oeSAT4.62
query50_query49_1133UNSAT4.62
random-qcir-1000-50-898UNSAT4.62
random-qcir-1000-50-98UNSAT4.62
random-qcir-1000-50-983UNSAT4.62
ntrivil_query54_1133SAT4.63
random-qcir-1000-50-68UNSAT4.63
random-qcir-1000-50-255UNSAT4.64
random-qcir-1000-50-441UNSAT4.64
random-qcir-1000-50-393UNSAT4.64
random-qcir-1000-50-361UNSAT4.64
random-qcir-1000-50-428UNSAT4.64
random-qcir-1000-50-930UNSAT4.64
JP-sat-02-08-3SAT4.64
random-qcir-1000-50-970UNSAT4.64
6s318r_c0to15.unsatUNSAT4.65
pg-hkb-2UNSAT4.65
bs128n.unsatUNSAT4.65
query71_query15_1133UNSAT4.66
random-qcir-1000-50-275UNSAT4.67
random-qcir-1000-50-658UNSAT4.67
random-qcir-1000-50-295UNSAT4.68
query21_reachqu_1133SAT4.68
random-qcir-1000-50-456UNSAT4.68
random-qcir-1000-50-846UNSAT4.69
random-qcir-1000-50-754UNSAT4.69
random-qcir-1000-50-940UNSAT4.69
SR-unsat-02-01-06-1UNSAT4.7
random-qcir-1000-50-793UNSAT4.7
ci.e#1.a#3.E#40.A#60.c#200.w#6.s#6.aspSAT4.7
random-qcir-1000-50-473UNSAT4.72
random-qcir-1000-50-857UNSAT4.73
random-qcir-1000-50-545UNSAT4.73
query64_query31_1133UNSAT4.8
stay22n.unsatUNSAT4.81
ci.e#1.a#3.E#40.A#60.c#432.w#2.s#8.aspUNSAT4.85
CM-sat-02-01-07-3SAT4.98
ci.e#1.a#3.E#40.A#60.c#424.w#2.s#1.aspUNSAT5.02
driver_a9y.unsatUNSAT5.1
query08_query26_1344SAT5.12
query44_query57_1133UNSAT5.15
pg-hkb-3UNSAT5.23
jctc6-passSAT5.4
k0201058.c.oeSAT5.46
CM-sat-03-01-06-4SAT5.47
SR-sat-02-01-07-2SAT5.73
k_ph_n-21SAT5.77
SR-sat-02-01-06-2SAT5.84
ci.e#1.a#3.E#40.A#60.c#208.w#6.s#8.aspSAT5.9
klieber2017q-112-28-t1UNSAT5.92
klieber2017q-078-19-t1UNSAT5.95
ci.e#1.a#3.E#40.A#60.c#264.w#4.s#2.aspSAT6
driver_d9n.unsatUNSAT6.32
ev-pr-4x4-11-3-0-0-1-lgSAT6.38
CM-sat-03-01-07-3SAT6.43
ev-pr-4x4-13-3-0-0-1-lgSAT6.72
JP-sat-02-07-3SAT6.73
sortnetsort9.v.stepl.005FAIL6.84
klieber2017q-082-20-eqFAIL6.84
ltl2dpa_C26_comp2_REAL.unsatFAIL6.85
klieber2017q-104-26-t1FAIL6.86
k0026150.s.oeFAIL6.86
rankfunc33_signed_32FAIL6.87
klieber2017q-108-27-t1FAIL6.87
klieber2017q-116-29-eqFAIL6.87
genbuf5b4n.satFAIL6.87
klieber2017q-100-25-t1FAIL6.87
ltl2dpa_C26_comp3_REAL.satFAIL6.88
ken.oop^2.C-d4FAIL6.88
klieber2017q-078-19-eqFAIL6.88
klieber2017q-108-27-eqFAIL6.88
chess_solving_mate_in_2_2005_POLTAVA-OPEN_01FAIL6.89
rankfunc17_unsigned_16FAIL6.89
genbuf10b4y.unsatFAIL6.89
query49_query58_1344FAIL6.9
query64_query55_1344FAIL6.9
klieber2017q-104-26-eqFAIL6.9
query33_query71_1344FAIL6.9
k0300663.s.oeFAIL6.9
k0225418.v.oeFAIL6.9
klieber2017q-074-18-t1FAIL6.9
small-swap1-fixpoint-3FAIL6.9
genbuf5b4n.unsatFAIL6.9
gb_s2_r2_comp3_REAL.unsatFAIL6.91
incrementer-enc07-uniform-depth-25FAIL6.91
mult_bool_matrix_2_3_30.unsatFAIL6.91
k0026150.h.oeFAIL6.91
klieber2017q-084-21-t1FAIL6.91
jctc2-passFAIL6.92
mult_bool_matrix_4_5_5.unsatFAIL6.92
incrementer-enc08-uniform-depth-33FAIL6.92
k0206272.connected.oeFAIL6.92
audio_ddksynth_csynth2.cppFAIL6.93
k0206272.h.oeFAIL6.93
query03_query57_1344FAIL6.93
k_ph_p-12FAIL6.93
k0225418.connected.oeFAIL6.93
k0026150.connected.oeFAIL6.93
klieber2017q-076-19-eqFAIL6.93
stay24n.satFAIL6.93
k0302060.c.oeFAIL6.94
klieber2017q-096-24-t1FAIL6.94
test2_quant_squaring3FAIL6.94
jctc9-passFAIL6.94
klieber2017q-074-18-eqFAIL6.94
sdlx-fixpoint-3FAIL6.94
small-swap2-fixpoint-4FAIL6.94
chess_solving_mate_in_2_1983_FIN-CH-4_01FAIL6.94
sortnetsort10.v.stepl.005FAIL6.94
klieber2017q-080-20-t1FAIL6.94
amba2f9n.unsatFAIL6.94
klieber2017q-086-21-eqFAIL6.94
klieber2017q-092-23-t1FAIL6.94
genbuf9b4n.unsatFAIL6.94
jctc10-failFAIL6.95
k0206272.v.oeFAIL6.95
klieber2017q-100-25-eqFAIL6.95
k0225744.connected.oeFAIL6.95
load_full_3_comp3_REAL.satFAIL6.95
amba2f9n.satFAIL6.95
klieber2017q-092-23-eqFAIL6.95
klieber2017q-086-21-t1FAIL6.96
gb_s2_r2_comp3_REAL.satFAIL6.96
k0300663.v.oeFAIL6.96
ltl2dpa_C26_comp3_REAL.unsatFAIL6.96
mult_bool_matrix_4_5_5.satFAIL6.96
p20-1.pddl_planlen=24FAIL6.96
query44_query58_1344FAIL6.96
k0225744.h.oeFAIL6.96
load_3c_comp_comp7_REAL.unsatFAIL6.96
test1_quant_squaring3FAIL6.96
klieber2017q-112-28-eqFAIL6.96
query48_query42_1344FAIL6.96
k0026150.v.oeFAIL6.96
chess_solving_mate_in_3_2016_BEL-CH-23A_02FAIL6.97
klieber2017q-096-24-eqFAIL6.97
jctc4-failFAIL6.97
jctc5-failFAIL6.97
ev-pr-8x8-7-7-0-1-2-lgFAIL6.98
chess_solving_mate_in_2_1996_FIN-CH-17_03FAIL6.98
beemldelec4b1_c0to15.satFAIL6.98
k0225744.v.oeFAIL6.98
bs128n.satFAIL6.98
k0300663.connected.oeFAIL6.98
k0225418.h.oeFAIL6.98
nreachq_query02_1344FAIL6.98
chess_composing_6_template_04FAIL6.99
mult_bool_matrix_2_3_30.satFAIL6.99
oski3ub1i_c0to63.satFAIL6.99
sortnetsort9.v.stepl.007FAIL6.99
cycle_sched_6_2_1.satFAIL6.99
chess_solving_mate_in_3_2009_POLTAVA-OPEN_03FAIL6.99
chess_solving_mate_in_3_2009_FIN-CH-30_04FAIL6.99
klieber2017q-116-29-t1FAIL6.99
load_full_3_comp3_REAL.unsatFAIL6.99
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL7
ken.flash^08.C-d4FAIL7
jctc1-passFAIL7
chess_solving_mate_in_5_1996_UKR-CH-10_15FAIL7
chess_solving_mate_in_2_2011_ISC-7B_01FAIL7
chess_solving_mate_in_2_2012_GER-CH-36-19_03FAIL7
chess_composing_6_template_06FAIL7.01
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL7.01
incrementer-enc02-uniform-depth-58FAIL7.01
query08_query64_1344FAIL7.02
query42_query57_1344FAIL7.02
k0225418.c.oeFAIL7.02
input_pnpi8042_moudep.cFAIL7.02
oski3ub1i_c0to63.unsatFAIL7.02
jctc13-failFAIL7.03
filesys_smbmrx_cvsndrcv.cFAIL7.03
chess_solving_mate_in_3_1999_WCSC-23_05FAIL7.03
rankfunc13_unsigned_64FAIL7.03
chess_solving_mate_in_4_1984_GBR-CH-5_04FAIL7.03
chess_composing_8_template_43FAIL7.04
query64_query58_1344FAIL7.04
k_ph_p-19FAIL7.05
chess_solving_mate_in_4_1999_GER-CH-23-6_14FAIL7.06
nreachq_reachqu_2233FAIL7.06
k0225744.s.oeFAIL7.06
chess_solving_mate_in_5_1984_FIN-CH-5_09FAIL7.07
ev-pr-4x4-15-3-0-0-1-sFAIL7.07
k0225682.c.oeFAIL7.07
chess_composing_8_template_02FAIL7.07
chess_composing_6_template_01FAIL7.07
mv16y.satFAIL7.08
chess_composing_8_template_13FAIL7.08
beemldelec4b1_c0to15.unsatFAIL7.08
jctc8-passFAIL7.08
chess_composing_8_template_42FAIL7.08
jctc14-unrolled-failFAIL7.09
jctc7-passFAIL7.09
query42_query64_1344FAIL7.09
network_irda_miniport_nscirda_comm.cFAIL7.09
jctc16-vals-0,2-passFAIL7.1
jctc15-unrolled-failFAIL7.1
chess_solving_mate_in_6_2013_WCCC-OPEN-56_10FAIL7.11
klieber2017q-080-20-eqFAIL7.12
6s318r_c0to31.satFAIL7.12
chess_solving_mate_in_4_2009_SEROCK-OPEN_09FAIL7.12
chess_solving_mate_in_6_2016_RUS-CH_15FAIL7.13
k0226271.c.oeFAIL7.13
test2_quant_squaring2FAIL7.13
chess_solving_mate_in_5_2012_NED-CH-18A_11FAIL7.14
test3_quant_squaring2FAIL7.14
k0225418.s.oeFAIL7.14
cycle_sched_6_2_1.unsatFAIL7.18
chess_composing_8_template_38FAIL7.21
chess_solving_mate_in_6_2011_SRB-CH_15FAIL7.33
jctc3-vals-0,2-passFAIL7.37
p20-5.pddl_planlen=32FAIL7.39
jctc11-passFAIL7.63
jctc18-vals-0,2-passFAIL7.86
query09_trivial_1344FAIL7.96
k0300663.h.oeFAIL7.97
pg-hkb-4UNSAT8.11
nreachq_reachqu_2133FAIL8.19
chess_solving_mate_in_6_1998_OST-CH-1_15FAIL8.2
jctc17-vals-0,2-passFAIL8.23
DW-sat-06-20-1SAT8.52
CM-sat-04-01-06-3SAT8.59
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL8.95
JP-unsat-02-06-3UNSAT9.19
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL9.3
k_branch_p-10UNSAT9.68
JP-sat-02-07-4SAT9.84
SR-unsat-02-01-05-2UNSAT10.08
DW-sat-08-22-1SAT10.39
DW-sat-08-23-1SAT10.46
p20-20.pddl_planlen=23FAIL10.82
CM-sat-04-01-06-4SAT11.27
DWs-sat-10-23-1SAT13.85
CM-sat-04-01-07-3SAT14.53
DWs-unsat-07-16-1UNSAT14.74
DWs-sat-10-25-1SAT14.8
pg-hkb-5UNSAT15.35
DWs-sat-12-28-1SAT20.6
DWs-unsat-08-17-1UNSAT20.7
DWs-unsat-08-18-1UNSAT23.33
DW-sat-08-24-1SAT24.05
query49_query64_1133UNSAT26.14
ci.e#1.a#3.E#40.A#60.c#288.w#4.s#8.aspSAT33.75
k_branch_p-11UNSAT35.14
DWs-sat-15-35-1SAT39.77
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspUNSAT42.45
SR-sat-02-01-06-3SAT42.73
ci.e#1.a#3.E#40.A#60.c#296.w#6.s#7.aspSAT47.97
DWs-unsat-09-19-1UNSAT52.02
pg-hkb-6UNSAT58.44
ci.e#1.a#3.E#40.A#60.c#320.w#4.s#8.aspSAT63.85
CM-sat-07-01-07-3SAT67.61
cnt14SAT70.59
DW-sat-09-26-1SAT82.7
CM-sat-07-01-06-4SAT87.66
ci.e#1.a#3.E#40.A#60.c#304.w#6.s#8.aspSAT95.76
DW-unsat-09-22-1UNSAT118.69
ci.e#1.a#3.E#40.A#60.c#312.w#2.s#3.aspSAT119.32
ci.e#1.a#3.E#40.A#60.c#304.w#4.s#7.aspSAT133.23
SR-sat-03-01-07-2SAT139.88
SR-sat-03-01-08-2SAT144.83
k_branch_n-10SAT153.18
ci.e#1.a#3.E#40.A#60.c#280.w#6.s#7.aspSAT158.02
DWs-sat-10-24-1SAT158.51
ci.e#1.a#3.E#40.A#60.c#296.w#4.s#7.aspSAT171.31
DWs-unsat-11-23-1UNSAT176.01
JP-unsat-03-08-3UNSAT178.69
JP-unsat-03-07-4UNSAT211.07
CM-sat-07-01-06-3SAT213.87
sortnetsort9.AE.stepl.012UNSAT251.73
DW-unsat-10-25-1UNSAT261.98
CM-unsat-07-01-06-2UNSAT287.34
pg-hkb-7UNSAT298.92
DWs-unsat-11-24-1UNSAT313.47
k_branch_p-16UNSAT347.76
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspUNSAT357.55
ev-pr-6x6-9-5-0-1-2-lgUNSAT390.59
DWs-unsat-12-25-1UNSAT392.45
ci.e#1.a#3.E#40.A#60.c#312.w#4.s#3.aspSAT542.28
DW-unsat-11-26-1UNSAT668.78
DW-unsat-11-27-1UNSAT807.24
SR-unsat-03-01-06-2UNSAT888.41
pipesnotankage18_8FAIL900
pg-hkb-20FAIL900
pg-hkb-15FAIL900
pg-hkb-14FAIL900
ci.e#1.a#3.E#40.A#60.c#368.w#6.s#7.aspFAIL900
ci.e#1.a#3.E#40.A#60.c#400.w#6.s#4.aspFAIL900
chess_solving_mate_in_7_2005_GER-CH-29-12_15FAIL900
pg-hkb-16FAIL900
pg-hkb-21FAIL900.01
cnt16rFAIL900.01
ev-pr-6x6-11-5-0-1-2-lgFAIL900.01
pg-hkb-22FAIL900.02
pg-hkb-17FAIL900.02
k_branch_n-12FAIL900.02
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#3.aspFAIL900.02
JP-unsat-03-09-4FAIL900.02
pg-hkb-12FAIL900.02
chess_solving_mate_in_7_2009_POL-CH-33_15FAIL900.02
ci.e#1.a#3.E#40.A#60.c#360.w#2.s#8.aspFAIL900.03
ci.e#1.a#3.E#40.A#60.c#368.w#2.s#7.aspFAIL900.03
pg-hkb-23FAIL900.03
ev-pr-6x6-17-5-0-1-2-lgFAIL900.04
chess_solving_mate_in_7_2016_BEL-CH-23A_03FAIL900.05
JP-sat-03-09-4FAIL900.05
pg-hkb-26FAIL900.05
chess_solving_mate_in_7_2011_SVK-CH-19_15FAIL900.05
pg-hkb-8FAIL900.06
JP-unsat-03-08-5FAIL900.06
pg-hkb-13FAIL900.07
pg-hkb-24FAIL900.07
pg-hkb-11FAIL900.07
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#6.aspFAIL900.07
pg-hkb-10FAIL900.08
qshifter_7FAIL900.08
pg-hkb-25FAIL900.08
chess_solving_mate_in_9_2003_RUS-CH_15FAIL900.08
ci.e#1.a#3.E#40.A#60.c#400.w#4.s#5.aspFAIL900.08
ci.e#1.a#3.E#40.A#60.c#376.w#4.s#6.aspFAIL900.08
ci.e#1.a#3.E#40.A#60.c#376.w#6.s#7.aspFAIL900.08
pipesnotankage14_10FAIL900.08
JP-sat-03-08-4FAIL900.09
pg-hkb-18FAIL900.09
pg-hkb-19FAIL900.09
DWs-unsat-13-28-1FAIL900.09
pg-hkb-9FAIL900.11
chess_solving_mate_in_8_2011_BEL-CH-19A_03FAIL900.12