To the TPTPCD/SGCD Experiments main page

Results on the TPTPCD2 Corpus – Overview and Times

This table shows for the 196 problems of the TPTPCD2 corpus the proving time of SGCD in different configurations and selected other provers.

An empty cell indicates that the problem could not be solved by the respective prover or configuration.
The problems are from TPTP 8.0.0. Ratings refer to the latest value of the problem's Rating field in TPTP 8.0.0.
Unless specially indicated, all reported results were obtained on a HPC system with Intel(R) Xeon(R) Platinum 9242 CPU @ 2.30GHz CPUs and 3.7 GB of memory per CPU, and time limit per prover run for a problem set to 2400s. Shown times are wall clock times in seconds.

SGCD Configurations and Other Provers

SGCD-1: SGCD in single Configuration.
SGCD-1+2+3: SGCD, union of: Configuration-1, Configuration-2, Configuration-3, Configuration-7.
Prover9: Prover9 with default settings. Invoked via CD Tools. Reported times exclude the pre- and postrocessing by CD Tools. Problems LCL020-1 and LCL021-1 failed due to exhaustion of memory on the HPC system such that results for these two problems were supplemented from runs on a notebook with 16 GB RAM.
E 2.6: E 2.6 with options --auto-schedule and --cpu-limit=600. The time limit was 600s. (A time limit of 2400s with the corresponding --cpu-limit option did not lead to more proven problems, just increased time values for finding proofs.)
SGCD-G1+G2: SGCD, union of: Configuration-1, Configuration-2. These are purely goal-driven configurations.
TABX: Union of SETHEO 3.3, S-SETHEO, lazyCoP 0.1 and SATCop 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
CMProver: CMProver, union of various configurations, according to http://cs.christophwernhard.com/pie/cmprover/evaluation_201803/tptp_neq.html.

Problem	Rating	SGCD-1	SGCD-1+2+3+7	Prover9	E 2.6	SGCD-G1+G2	TABX	CMProver
Totals of 196:		165	176	168	185	89	76	89
LCL006-1	0.00	0.07	0.00	0.77	0.05	0.00	•	0.02
LCL007-1	0.00	0.00	0.00	0.09	0.01	0.00	•	0.01
LCL008-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL009-1	0.00	0.07	0.00	0.04	0.05	0.01	•	0.03
LCL010-1	0.00	0.01	0.00	0.05	0.02	0.00	•	0.02
LCL011-1	0.00	0.42	0.03	0.96	0.05	0.06	•	0.07
LCL012-1	0.00	25.51	25.51	4.57	0.26
LCL013-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL014-1	0.00	6.10	6.10	2.98	0.04	3.76		3.19
LCL015-1	0.00	44.91	44.91	4.44	0.02
LCL016-1	0.00	66.87	66.87	3.67	0.32
LCL017-1	0.00	93.51	93.51	12.05	0.07
LCL018-1	0.00	43.45	43.45	5.04	0.02
LCL019-1	0.00	99.58	99.58	7.26	0.28
LCL021-1	0.00	157.43	157.43	42.52	0.45
LCL022-1	0.00	0.30	0.00	0.03	0.04	0.00	•	0.01
LCL023-1	0.00	0.07	0.01	0.06	0.05	0.00	•	0.01
LCL024-1	0.00	2.09	1.57	2.73	0.22	3.11		6.44
LCL025-1	0.00	0.04	0.03	0.43	0.02	0.02	•	0.05
LCL026-1	0.00	13.59	0.76	0.97	0.40
LCL027-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL029-1	0.00	0.51	0.25	0.06	0.02	1.04	•	1.69
LCL030-1	0.00	6.88	2.68	7.21	12.81	37.28		61.64
LCL032-1	0.00		291.85	99.16	40.56
LCL033-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.02
LCL034-1	0.00	5.47	0.95	0.11	0.04
LCL035-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.02
LCL036-1	0.00	1.20	0.08	0.05	0.05
LCL038-1	0.00	78.86	78.86	41.16	18.58
LCL040-1	0.00	1.13	0.15	3.73	79.90	3.95	•	2.67
LCL041-1	0.00	0.00	0.00	0.03	0.03	0.00	•	0.01
LCL042-1	0.00	12.08	0.13	2.63	25.55	12.67	•	0.67
LCL043-1	0.00	0.00	0.00	0.05	0.01	0.00	•	0.01
LCL044-1	0.00	0.00	0.00	0.05	0.03	0.00	•	0.01
LCL045-1	0.00	0.08	0.00	0.67	2.74	0.00	•	0.02
LCL046-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL047-1	0.00	28.47	0.35	0.07	0.82	86.70
LCL048-1	0.00	30.65	16.19	0.07	0.92
LCL049-1	0.00	60.65	28.32	0.23	0.82
LCL050-1	0.00	73.72	44.22	0.33	0.77
LCL051-1	0.00	69.76	39.95	0.38	1.72
LCL052-1	0.00	51.64	37.92	0.39	0.89
LCL053-1	0.00	70.91	48.99	0.43	0.99
LCL054-1	0.00	92.32	5.02	396.45	2.02
LCL055-1	0.00	66.53	32.90	0.38	0.86
LCL056-1	0.00	67.24	31.01	0.37	0.97
LCL057-1	0.00	72.50	52.96	0.40	0.93
LCL058-1	0.00	104.94	104.94	29.12	0.88
LCL059-1	0.00	16.44	0.76	0.60	0.67	50.13		82.09
LCL060-1	0.00	136.25	136.25	34.93	0.89
LCL064-1	0.00	0.04	0.03	3.08	0.20	0.02	•	0.05
LCL064-2	0.00	0.02	0.01	0.08	0.02	0.01	•	0.03
LCL065-1	0.00	0.58	0.01	0.05	0.25	0.54	•	0.15
LCL066-1	0.00	0.04	0.01	0.04	0.02	0.02	•	0.04
LCL067-1	0.00	4.83	0.30	1.40	21.38		•	13.59
LCL068-1	0.00	5.18	2.50	2.78	0.23
LCL069-1	0.00	0.09	0.02	0.09	0.09	0.04	•	0.07
LCL070-1	0.00	5.28	4.36	0.91	5.07	1,345.86	•	5.80
LCL071-1	0.00	5.03	5.03	3.31	1.80			83.00
LCL072-1	0.00	0.14	0.00	0.12	0.69	0.01	•	0.01
LCL075-1	0.00	1.94	0.11	0.10	0.04	356.92		122.90
LCL076-1	0.00	0.56	0.01	0.03	0.02	0.32	•	0.44
LCL076-2	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL077-1	0.00	0.13	0.01	0.03	0.02	0.08	•	0.10
LCL079-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL080-1	0.00	1.86	0.07	0.34	16.85	29.98	•	3.75
LCL080-2	0.00	1.96	0.08	0.34	4.54	704.27	•	4.72
LCL081-1	0.00	0.02	0.00	0.03	0.02	0.00	•	0.02
LCL082-1	0.00	0.00	0.00	0.03	0.02	0.00	•	0.02
LCL083-1	0.00	0.28	0.09	0.13	0.03	1.68
LCL083-2	0.00	0.01	0.01	0.10	0.04	0.32	•	0.05
LCL084-2	0.00	73.95	73.95	38.92	54.13
LCL084-3	0.00	94.05	94.05	38.80	53.42
LCL085-1	0.00	6.100	6.100	9.62	7.59
LCL086-1	0.00	11.03	0.06	0.03	0.02	1,523.50	•
LCL087-1	0.00	0.13	0.01	0.03	0.01	0.06	•	0.13
LCL088-1	0.00	5.43	0.04	0.07	0.02	129.47	•	213.39
LCL089-1	0.00	11.35	0.09	0.08	0.02
LCL090-1	0.00	11.64	11.64	0.19	0.03	76.27	•	125.66
LCL091-1	0.00	2.42	2.42	0.08	0.03	1.99	•	3.46
LCL093-1	0.00	72.63	72.63	53.27	0.13
LCL094-1	0.00	14.75	0.13	0.07	0.05
LCL095-1	0.00	48.65	48.65	0.47	0.05	674.43	•
LCL096-1	0.00	0.00	0.00	2.17	0.11	0.00	•	0.02
LCL097-1	0.00	0.01	0.00	0.06	0.13	0.00	•	0.02
LCL098-1	0.00	0.00	0.00	0.05	0.85	0.00	•	0.01
LCL100-1	0.00		32.68	198.63	23.25
LCL101-1	0.00	0.03	0.01	0.03	0.02	0.67	•	0.07
LCL102-1	0.00	1.94	0.01	0.28	0.04	0.03	•	0.01
LCL103-1	0.00	32.76	0.48	2.46	3.65	73.71		42.26
LCL104-1	0.00	0.36	0.01	0.03	0.01	0.19	•	0.04
LCL106-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL107-1	0.00	0.01	0.00	0.03	0.32	0.00	•	0.02
LCL108-1	0.00	0.50	0.00	0.05	0.02	0.06	•	0.12
LCL110-1	0.00	0.90	0.01	0.03	0.03	0.02	•	0.06
LCL111-1	0.00	0.01	0.00	0.09	0.33	0.00	•	0.01
LCL112-1	0.00	1.58	0.02	0.04	0.04	1.83	•	0.92
LCL113-1	0.00	59.23	39.90	11.79	0.84			523.74
LCL114-1	0.00	246.74	246.74	11.66	8.08
LCL115-1	0.00	22.79	0.06	0.10	0.03			338.82
LCL116-1	0.00	255.44	255.44	11.62	27.55
LCL117-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL118-1	0.00	0.01	0.00	0.08	0.02	0.00	•	0.01
LCL120-1	0.00	0.00	0.00	0.42	0.01	0.00	•	0.02
LCL121-1	0.00	53.53	48.98	2.28	0.16
LCL122-1	0.00		70.21	77.04	0.72
LCL123-1	0.00	7.74	0.07	3.62	46.22	0.03	•	0.01
LCL126-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL127-1	0.00	52.42	52.42	21.30	7.28
LCL128-1	0.00	47.08	47.08	3.07	0.61			418.15
LCL129-1	0.00	20.46	20.46	33.78	28.44
LCL130-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL131-1	0.00	4.63	0.46	2.10	0.10			120.36
LCL166-1	0.00	89.43	89.43	18.86	0.09
LCL256-1	0.00	58.02	52.90	0.39	0.85
LCL257-1	0.00	0.09	0.00	0.03	0.02	0.00	•	0.01
LCL355-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL356-1	0.00	0.00	0.00	0.03	0.02	0.00	•	0.01
LCL357-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL358-1	0.00	0.01	0.00	0.42	0.02	0.00	•	0.01
LCL360-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL361-1	0.00	0.00	0.00	0.05	0.01	0.00	•	0.01
LCL362-1	0.00	0.00	0.00	0.04	0.01	0.00	•	0.01
LCL363-1	0.00	0.02	0.02	0.04	0.01	0.00	•	0.03
LCL364-1	0.00	2.43	0.04	0.07	0.62	0.16		4.06
LCL366-1	0.00	7.16	0.87	0.21	0.66	52.96		73.27
LCL367-1	0.00	12.11	0.38	0.07	0.63	99.56
LCL370-1	0.00	72.56	72.56	35.32	0.71
LCL371-1	0.00	95.39	95.39	35.92	0.72
LCL373-1	0.00	112.93	112.93	35.76	0.82
LCL378-1	0.00	54.27	27.95	0.37	0.92
LCL380-1	0.00	75.25	52.73	0.38	0.98
LCL381-1	0.00	82.77	1.52	0.42	0.80
LCL382-1	0.00	75.23	3.30	28.88	0.84
LCL384-1	0.00	20.00	0.16	0.34	0.83	14.33		357.07
LCL385-1	0.00	98.50	98.50	28.89	0.84
LCL386-1	0.00	72.21	72.21	1.71	0.86
LCL387-1	0.00	98.94	6.91	1.71	0.95
LCL390-1	0.00	79.60	79.60	36.05	0.77
LCL391-1	0.00	181.93	42.65	132.18	2.32
LCL396-1	0.00	64.63	64.63	0.41	0.94
LCL397-1	0.00	0.29	0.06	0.03	0.01	0.10	•	0.27
LCL398-1	0.00	0.00	0.00	0.03	0.01	0.00	•	0.01
LCL399-1	0.00	7.08	4.27	0.16	0.29	891.46	•
LCL400-1	0.00	100.58	100.58	0.83	1.01
LCL401-1	0.00	95.10	95.10	0.83	1.07
LCL402-1	0.00	74.37	74.37	0.38	0.100
LCL403-1	0.00	100.31	100.31	29.64	63.53
LCL404-1	0.00	95.49	95.49	29.09	63.36
LCL405-1	0.00	81.17	81.17	0.41	0.86
LCL416-1	0.00	3.65	2.04	2.31	0.02	59.21	•	96.97
LCL020-1	0.25			131.47	0.34
LCL031-1	0.25	155.91	155.91	516.18	18.74
LCL037-1	0.25			183.21	114.71
LCL062-1	0.25		212.79		3.81
LCL074-1	0.25		1,040.88		69.27
LCL092-1	0.25	51.01	51.01	0.21	0.04	32.05		51.16
LCL099-1	0.25		246.55		1.75
LCL105-1	0.25			56.06	19.58
LCL119-1	0.25			119.39	0.19
LCL125-1	0.25			30.36	147.78
LCL167-1	0.25	192.46	192.46	80.09	0.29
LCL359-1	0.25	0.01	0.00	0.34	11.01	0.00	•	0.01
LCL365-1	0.25	4.77	0.27		1.43	0.25		12.40
LCL368-1	0.25	81.09	1.22	1.66	1.75
LCL369-1	0.25	80.23	1.64	1.66	3.61
LCL372-1	0.25	93.88	6.95		1.53
LCL375-1	0.25		37.81		2.36
LCL376-1	0.25	118.54	65.37		2.30
LCL379-1	0.25	75.86	48.05	0.39	0.87
LCL383-1	0.25	103.69	15.30		1.97
LCL388-1	0.25	140.84	38.38	29.96	0.91
LCL389-1	0.25	145.57	25.30	28.99	2.17
LCL392-1	0.25	79.94	9.93	989.65	1.19
LCL393-1	0.25		28.36	2,391.86	1.63
LCL394-1	0.25		124.24		3.10
LCL028-1	0.50	153.56	153.56	1,963.92	36.32
LCL061-1	0.50		30.56		1.28
LCL124-1	0.50				46.66
LCL374-1	0.50	117.85	22.66		7.29
LCL377-1	0.50	115.96	34.93		3.06
LCL395-1	0.50		56.44		2.14
LCL428-1	0.50				0.03
LCL875-1	0.50				0.02
LCL063-1	0.75				162.66
LCL109-1	0.75
LCL417-1	0.75
LCL422-1	0.75
LCL876+1	0.93
LCL073-1	1.00
LCL418-1	1.00
LCL419-1	1.00
LCL420-1	1.00
LCL421-1	1.00
LCL425-1	1.00
LCL426-1	1.00
Problem	Rating	SGCD-1	SGCD-1+2+3+7	Prover9	E 2.6	SGCD-G1+G2	TABX	CMProver
Totals of 196:		165	176	168	185	89	76	89