QF_UFNRA (Single Query Track)

Competition results for the QF_UFNRA logic in the Single Query Track.

Page generated on 2021-07-18 17:29:07 +0000

Benchmarks: 27
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	Yices2	cvc5	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	23	4981.133	4972.403	23	21	2	4	4	0
2019-Par4n	0	23	5785.319	5295.525	23	21	2	4	4	0
Yices2	0	23	11498.993	11500.374	23	21	2	4	4	0
2020-CVC4n	0	13	18213.144	18216.704	13	11	2	14	14	0
MathSAT5n	0	8	21803.585	21781.711	8	6	2	19	18	0
cvc5	0	3	28798.825	28802.004	3	1	2	24	24	0
cvc5 - fixedn	0	3	28800.086	28802.038	3	1	2	24	24	0
veriT+raSAT+Redlog	0	1	31196.858	31200.841	1	1	0	26	26	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	25	6813.049	4609.66	25	23	2	2	2	0
z3n	0	23	4981.333	4972.253	23	21	2	4	4	0
Yices2	0	23	11499.583	11500.194	23	21	2	4	4	0
2020-CVC4n	0	13	18215.864	18216.174	13	11	2	14	14	0
MathSAT5n	0	8	21805.635	21781.011	8	6	2	19	18	0
cvc5	0	3	28801.275	28801.274	3	1	2	24	24	0
cvc5 - fixedn	0	3	28801.346	28801.348	3	1	2	24	24	0
veriT+raSAT+Redlog	0	1	31200.008	31200.011	1	1	0	26	26	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-Par4n	0	23	5613.036	3409.296	23	23	0	1	3	2	0
z3n	0	21	3781.004	3771.924	21	21	0	3	3	4	0
Yices2	0	21	10291.706	10292.316	21	21	0	3	3	4	0
2020-CVC4n	0	11	17013.774	17014.085	11	11	0	13	3	14	0
MathSAT5n	0	6	20605.398	20580.773	6	6	0	18	3	18	0
veriT+raSAT+Redlog	0	1	27600.008	27600.011	1	1	0	23	3	26	0
cvc5	0	1	27600.021	27600.021	1	1	0	23	3	24	0
cvc5 - fixedn	0	1	27600.022	27600.021	1	1	0	23	3	24	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
MathSAT5n	0	2	0.237	0.237	2	0	2	0	25	18	0
z3n	0	2	0.329	0.329	2	0	2	0	25	4	0
2019-Par4n	0	2	0.013	0.364	2	0	2	0	25	2	0
cvc5	0	2	1.254	1.253	2	0	2	0	25	24	0
cvc5 - fixedn	0	2	1.325	1.327	2	0	2	0	25	24	0
2020-CVC4n	0	2	2.09	2.089	2	0	2	0	25	14	0
Yices2	0	2	7.877	7.878	2	0	2	0	25	4	0
veriT+raSAT+Redlog	0	0	2400.0	2400.0	0	0	0	2	25	26	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	23	277.333	268.253	23	21	2	4	4	0
2019-Par4n	0	18	440.449	330.655	18	16	2	9	9	0
Yices2	0	5	544.795	544.8	5	3	2	22	22	0
MathSAT5n	0	5	547.025	547.039	5	3	2	22	21	0
cvc5	0	3	577.275	577.274	3	1	2	24	24	0
cvc5 - fixedn	0	3	577.346	577.348	3	1	2	24	24	0
2020-CVC4n	0	3	578.109	578.108	3	1	2	24	24	0
veriT+raSAT+Redlog	0	1	624.008	624.011	1	1	0	26	26	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.