UFDTNIRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	819	27724.472	27731.569	819	0	819	102	23	0
cvc5 - fixedn	0	819	37812.314	37819.442	819	0	819	102	30	0
cvc5	0	818	38081.421	38088.8	818	0	818	103	31	0
2020-Vampiren	0	782	281340.577	193033.456	782	0	782	139	130	0
Vampire	0	694	395215.819	307549.817	694	0	694	227	227	0
Vampire - fixedn	0	682	384440.753	299164.369	682	0	682	239	221	0
iProver	0	483	556595.868	533674.199	483	0	483	438	438	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Vampiren	0	827	325568.727	161708.293	827	0	827	94	83	0
2020-CVC4n	0	819	27730.762	27730.529	819	0	819	102	23	0
cvc5 - fixedn	0	819	37817.844	37817.972	819	0	819	102	30	0
cvc5	0	818	38087.561	38087.33	818	0	818	103	31	0
Vampire	0	712	424084.159	297028.923	712	0	712	209	209	0
Vampire - fixedn	0	700	406829.703	288757.939	700	0	700	221	203	0
iProver	0	497	582439.918	527653.977	497	0	497	424	424	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2020-Vampiren	0	0	0.0	0.0	0	0	0	0	921	83	0
2020-CVC4n	0	0	0.0	0.0	0	0	0	0	921	23	0
cvc5	0	0	0.0	0.0	0	0	0	0	921	31	0
iProver	0	0	0.0	0.0	0	0	0	0	921	424	0
Vampire	0	0	0.0	0.0	0	0	0	0	921	209	0
Vampire - fixedn	0	0	0.0	0.0	0	0	0	0	921	203	0
cvc5 - fixedn	0	0	0.0	0.0	0	0	0	0	921	30	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2020-Vampiren	0	827	293424.307	132051.887	827	0	827	69	25	83	0
2020-CVC4n	0	819	24129.115	24128.888	819	0	819	77	25	23	0
cvc5 - fixedn	0	819	34191.103	34191.234	819	0	819	77	25	30	0
cvc5	0	818	34444.499	34444.271	818	0	818	78	25	31	0
Vampire	0	712	390483.999	267035.293	712	0	712	184	25	209	0
Vampire - fixedn	0	700	376829.703	258757.939	700	0	700	196	25	203	0
iProver	0	497	552439.918	497653.977	497	0	497	399	25	424	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	819	682.762	682.529	819	0	819	102	23	0
cvc5 - fixedn	0	815	1077.673	1077.431	815	0	815	106	37	0
cvc5	0	814	1091.356	1091.062	814	0	814	107	37	0
Vampire	0	428	12952.912	12353.08	428	0	428	493	493	0
Vampire - fixedn	0	421	12834.308	12309.652	421	0	421	500	494	0
iProver	0	410	15974.192	13412.368	410	0	410	511	511	0
2020-Vampiren	0	381	14875.019	13833.938	381	0	381	540	533	0

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