AUFDTLIA (Single Query Track)

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

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

Benchmarks: 147
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	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	147	23097.124	23393.936	147	93	54	0	0	0
cvc5 - fixedn	0	119	15599.044	43112.692	119	65	54	28	28	0
cvc5	0	115	13307.656	45492.624	115	61	54	32	32	0
2018-CVC4n	0	99	23006.889	23266.247	99	45	54	48	0	0
Vampire	0	54	111664.335	111686.761	54	0	54	93	93	0
Vampire - fixedn	0	54	111768.114	111678.868	54	0	54	93	93	0
2020-Vampiren	0	54	112428.072	111919.995	54	0	54	93	93	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-CVC4n	0	147	23097.124	23393.936	147	93	54	0	0	0
cvc5 - fixedn	0	119	42970.236	43111.282	119	65	54	28	28	0
cvc5	0	115	45371.699	45490.894	115	61	54	32	32	0
2018-CVC4n	0	99	23006.889	23266.247	99	45	54	48	0	0
Vampire - fixedn	0	54	111768.114	111678.868	54	0	54	93	93	0
Vampire	0	54	111785.045	111686.671	54	0	54	93	93	0
2020-Vampiren	0	54	112428.072	111919.995	54	0	54	93	93	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-CVC4n	0	93	23091.177	23388.004	93	93	0	0	54	0	0
cvc5 - fixedn	0	65	42967.577	43108.65	65	65	0	28	54	28	0
cvc5	0	61	45369.033	45488.258	61	61	0	32	54	32	0
2018-CVC4n	0	45	23001.24	23260.614	45	45	0	48	54	0	0
2020-Vampiren	0	0	111600.0	111600.0	0	0	0	93	54	93	0
Vampire	0	0	111600.0	111600.0	0	0	0	93	54	93	0
Vampire - fixedn	0	0	111600.0	111600.0	0	0	0	93	54	93	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5 - fixedn	0	54	2.659	2.632	54	0	54	0	93	28	0
cvc5	0	54	2.666	2.636	54	0	54	0	93	32	0
2018-CVC4n	0	54	5.649	5.633	54	0	54	0	93	0	0
2020-CVC4n	0	54	5.947	5.931	54	0	54	0	93	0	0
Vampire - fixedn	0	54	168.114	78.868	54	0	54	0	93	93	0
Vampire	0	54	185.045	86.671	54	0	54	0	93	93	0
2020-Vampiren	0	54	828.072	319.995	54	0	54	0	93	93	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5 - fixedn	0	99	1170.597	1170.945	99	45	54	48	48	0
2018-CVC4n	0	99	1171.289	1171.174	99	45	54	48	48	0
cvc5	0	99	1171.059	1171.454	99	45	54	48	48	0
2020-CVC4n	0	99	1172.863	1174.385	99	45	54	48	48	0
Vampire - fixedn	0	54	2400.114	2310.868	54	0	54	93	93	0
Vampire	0	53	2381.805	2313.733	53	0	53	94	94	0
2020-Vampiren	0	50	2525.232	2418.806	50	0	50	97	97	0

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