UFDTLIA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-CVC4n	0	197	198426.842	204478.296	197	0	197	80	80	0
2020-CVC4n	0	196	149250.562	151570.056	196	0	196	81	81	0
cvc5 - fixedn	0	144	121329.334	200876.532	144	0	144	133	133	0
Vampire	0	133	177211.056	174125.167	133	0	133	144	144	0
cvc5	0	132	106225.89	210884.717	132	0	132	145	145	0
Vampire - fixedn	0	132	177731.369	175150.429	132	0	132	145	145	0
2020-Vampiren	0	124	187027.453	184588.75	124	0	124	153	152	0
iProver	0	28	301812.068	299570.679	28	0	28	249	249	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-CVC4n	0	197	202450.312	204473.486	197	0	197	80	80	0
2020-CVC4n	0	196	150473.582	151566.546	196	0	196	81	81	0
cvc5 - fixedn	0	144	199916.39	200869.262	144	0	144	133	133	0
Vampire	0	133	180811.176	174122.227	133	0	133	144	144	0
Vampire - fixedn	0	133	178001.879	174334.323	133	0	133	144	144	0
cvc5	0	132	210013.467	210877.387	132	0	132	145	145	0
2020-Vampiren	0	126	193159.193	182562.845	126	0	126	151	149	0
iProver	0	29	304847.548	299441.569	29	0	29	248	248	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-CVC4n	0	0	0.0	0.0	0	0	0	0	277	80	0
2020-Vampiren	0	0	0.0	0.0	0	0	0	0	277	149	0
2020-CVC4n	0	0	0.0	0.0	0	0	0	0	277	81	0
cvc5	0	0	0.0	0.0	0	0	0	0	277	145	0
iProver	0	0	0.0	0.0	0	0	0	0	277	248	0
Vampire	0	0	0.0	0.0	0	0	0	0	277	144	0
Vampire - fixedn	0	0	0.0	0.0	0	0	0	0	277	144	0
cvc5 - fixedn	0	0	0.0	0.0	0	0	0	0	277	133	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-CVC4n	0	197	118450.312	120473.486	197	0	197	10	70	80	0
2020-CVC4n	0	196	66473.582	67566.546	196	0	196	11	70	81	0
cvc5 - fixedn	0	144	115916.39	116869.262	144	0	144	63	70	133	0
Vampire	0	133	96811.176	90122.227	133	0	133	74	70	144	0
Vampire - fixedn	0	133	94001.879	90334.323	133	0	133	74	70	144	0
cvc5	0	132	126013.467	126877.387	132	0	132	75	70	145	0
2020-Vampiren	0	126	109159.193	98562.845	126	0	126	81	70	149	0
iProver	0	29	220847.548	215441.569	29	0	29	178	70	248	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Vampire	0	120	4009.312	3897.045	120	0	120	157	157	0
Vampire - fixedn	0	119	3987.432	3899.277	119	0	119	158	158	0
2020-Vampiren	0	112	6855.153	5564.071	112	0	112	165	164	0
2020-CVC4n	0	27	6037.918	6037.921	27	0	27	250	250	0
2019-CVC4n	0	26	6053.864	6053.854	26	0	26	251	251	0
cvc5 - fixedn	0	24	6097.84	6092.441	24	0	24	253	253	0
cvc5	0	24	6092.457	6092.449	24	0	24	253	253	0
iProver	0	18	6630.48	6327.106	18	0	18	259	259	0

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