tptp « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	ARI086=1.p	1431	log plain
d---------	Axioms	156	log plain
-rw-r--r--	BOO003-4.p	1345	log plain
-rw-r--r--	BOO027-1.p	2017	log plain
-rw-r--r--	DAT001=1.p	2035	log plain
-rw-r--r--	KRS018+1.p	2097	log plain
-rw-r--r--	KRS063+1.p	4624	log plain
-rw-r--r--	MGT019+2.p	3807	log plain
-rw-r--r--	MGT031-1.p	3272	log plain
-rw-r--r--	MGT041-2.p	2134	log plain
-rw-r--r--	NLP114-1.p	4802	log plain
-rw-r--r--	PUZ131_1.p	3238	log plain
-rw-r--r--	SYN000+1.p	2619	log plain
-rw-r--r--	SYN000+2.p	3439	log plain
-rw-r--r--	SYN000-1.p	2107	log plain
-rw-r--r--	SYN000-2.p	3041	log plain
-rw-r--r--	SYN000=2.p	6595	log plain
-rw-r--r--	SYN000_1.p	3807	log plain
-rw-r--r--	SYN000_2.p	3762	log plain
-rw-r--r--	SYN075+1.p	1806	log plain
-rw-r--r--	SYN075-1.p	2222	log plain
-rw-r--r--	tff0-arith.p	901	log plain
-rw-r--r--	tff0.p	1484	log plain
-rw-r--r--	tptp_parser.p	355	log plain
-rw-r--r--	tptp_parser10.p	271	log plain
-rw-r--r--	tptp_parser2.p	310	log plain
-rw-r--r--	tptp_parser3.p	324	log plain
-rw-r--r--	tptp_parser4.p	324	log plain
-rw-r--r--	tptp_parser5.p	352	log plain
-rw-r--r--	tptp_parser6.p	366	log plain
-rw-r--r--	tptp_parser7.p	352	log plain
-rw-r--r--	tptp_parser8.p	283	log plain
-rw-r--r--	tptp_parser9.p	341	log plain