Family	Overall				Time	Hardness
Family	N	#	S	U	Time	EA	ME	MH
Abduction	1	0	0	0	-
Adder	4	0	0	0	-
amba	4	2	1	1	400.14		2
Blocks	1	1		1	0.42		1
BMC	3	1	1		106.98		1
bomb	3	2	1	1	269.39			2
BoundedSynthesisPetriGames	42	23	10	13	2816.69	5	17	1
C499	3	3		3	2.91		3
C5315	1	0	0	0	-
C6288	4	1	1		196.18			1
C880	2	1		1	2.44		1
Chain	3	3	3		0.34		3
circuits	4	1	1		360.12			1
CombinationalEquivalence	30	30	15	15	17.41		30
conformant_planning	3	2	2		117.61		1	1
Connect4	2	0	0	0	-
Counter	2	1	1		87.64		1
cycle-sched	4	1		1	796.48			1
Debug	5	0	0	0	-
driver	4	3	1	2	2.33	1	2
dungeon	3	1		1	1.56		1
evader-pursuer-4x4-logarithmic	2	2	2		5.37		2
evader-pursuer-4x4-standard	4	0	0	0	-
evader-pursuer-6x6-logarithmic	4	1		1	166.35		1
evader-pursuer-6x6-standard	4	0	0	0	-
evader-pursuer-8x8-logarithmic	4	1		1	19.05		1
fpu	2	2		2	14.25	2
genbuf	4	2		2	482.28		2
HardwareFixpoint	5	0	0	0	-
hwmcc	4	2		2	2.14	2
hyperLTL	2	2	1	1	0	2
incrementer-encoder	3	3	1	2	0.88		3
irqlkeapclte	5	5	5		180.62		5
ISCAS89	1	1	1		18.46		1
ITC99	4	4	4		225.46		2	2
jmc_quant_squaring	5	1		1	266.44		1
k_branch_n	2	2	2		114.54			2
k_branch_p	3	3		3	11.72		2	1
k_ph_n	1	1	1		0.24		1
k_ph_p	2	1		1	31.59			1
LinearBitvectorRankingFunction	5	1		1	0.66		1
ltl2aig-comp	4	2		2	116.28		1	1
LTL2DBA	2	1		1	0.27	1
LTL2DPA	2	1		1	0.64		1
Model_instances	20	14	10	4	811.94		11	3
mqm	2	2	1	1	469.94		1	1
mult-matrix	4	0	0	0	-
MutexP	3	3	3		0.12		3
Planning-CTE	2	1		1	478.93			1
QBF-Hardness	2	1	1		6.33		1
QLTL_safety	50	28	20	8	2142.86	1	24	3
Qshifter	2	0	0	0	-
RankingFunctions	5	0	0	0	-
Reduction-finding	2	0	0	0	-
s1269	3	0	0	0	-
s3330	2	0	0	0	-
Sorting_networks	4	2	1	1	33.16		1	1
SzymanskiP	5	5		5	41.53		5
terminator	1	1		1	3.37		1
tipdiam	2	1		1	340.32		1
toy	4	4	2	2	0.51	2	2
uclid	2	2	2		68.96		2
VonNeumann	1	1		1	13.63	1
wmiforward	2	2	2		0.04		2

QBF Solver Evaluation Portal