To the TPTPCD/SGCD Experiments main page

Results on the TPTPCD2 Corpus – Purely Goal-Driven Proving

This table shows for the 196 problems of the TPTPCD2 corpus the proving time of SGCD in two purely goal-driven configurations and those other goal-driven provers based on clausal tableaux, the connection method or model elimination for which roughly comparable performance data were available. For SGCD also proof dimensions are show, written as

Compacted Size / Tree Size / Height.

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.
Proof sizes are shown after n-simplification. An asterisk (*) indicates that n-simplification took effect.

SGCD Configurations and Other Provers

SGCD-G1: SGCD in single Configuration.
SGCD-G2: SGCD in single Configuration.
SGCD-G1+G2: SGCD, union of: Configuration-1, Configuration-2.
CM+TABX: Union of CMProver and TABX.
CMProver: CMProver, union of various configurations, according to http://cs.christophwernhard.com/pie/cmprover/evaluation_201803/tptp_neq.html.
TABX: Union of S-SETHEO, SETHEO 3.3, SATCoP 0.1, lazyCoP 0.1.
S-SETHEO: S-SETHEO according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
SETHEO 3.3: SETHEO 3.3 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
SATCoP 0.1: SATCoP 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.
lazyCoP 0.1: lazyCoP 0.1 according to the ProblemAndSolutionStatistics document of TPTP 8.0.0.

Problem	Rating	SGCD-G1	SGCD-G2	SGCD-G1+G2	CM+TABX	CMProver	TABX	S-SETHEO	SETHEO 3.3	SATCoP 0.1	lazyCoP 0.1
Totals of 196:		81	65	89	92	89	76	66	65	59	42
LCL006-1	0.00	0.03	0.00	0.00	•	0.02	•	•	•	•	•
LCL007-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL008-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL009-1	0.00	0.01	0.01	0.01	•	0.03	•	•	•	•
LCL010-1	0.00	0.00	0.00	0.00	•	0.02	•	•	•	•	•
LCL011-1	0.00	0.06	0.14	0.06	•	0.07	•	•	•	•
LCL012-1	0.00
LCL013-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL014-1	0.00	3.76		3.76	•	3.19
LCL015-1	0.00
LCL016-1	0.00
LCL017-1	0.00
LCL018-1	0.00
LCL019-1	0.00
LCL021-1	0.00
LCL022-1	0.00	0.04	0.00	0.00	•	0.01	•	•	•	•
LCL023-1	0.00	0.01	0.00	0.00	•	0.01	•	•	•	•
LCL024-1	0.00	3.11		3.11	•	6.44
LCL025-1	0.00	0.02		0.02	•	0.05	•	•	•	•	•
LCL026-1	0.00
LCL027-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL029-1	0.00	1.04	28.20	1.04	•	1.69	•	•	•
LCL030-1	0.00		37.28	37.28	•	61.64
LCL032-1	0.00
LCL033-1	0.00	0.00	5.67	0.00	•	0.02	•	•	•	•	•
LCL034-1	0.00
LCL035-1	0.00	0.00	0.00	0.00	•	0.02	•	•	•	•	•
LCL036-1	0.00
LCL038-1	0.00
LCL040-1	0.00	3.95		3.95	•	2.67	•	•	•
LCL041-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL042-1	0.00	12.67	15.61	12.67	•	0.67	•	•	•
LCL043-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL044-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL045-1	0.00	0.01	0.00	0.00	•	0.02	•	•	•	•	•
LCL046-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL047-1	0.00		86.70	86.70
LCL048-1	0.00
LCL049-1	0.00
LCL050-1	0.00
LCL051-1	0.00
LCL052-1	0.00
LCL053-1	0.00
LCL054-1	0.00
LCL055-1	0.00
LCL056-1	0.00
LCL057-1	0.00
LCL058-1	0.00
LCL059-1	0.00		50.13	50.13	•	82.09
LCL060-1	0.00
LCL064-1	0.00	0.02		0.02	•	0.05	•	•	•	•	•
LCL064-2	0.00	0.01	216.76	0.01	•	0.03	•	•	•	•	•
LCL065-1	0.00	0.54		0.54	•	0.15	•	•	•
LCL066-1	0.00	0.02		0.02	•	0.04	•	•	•	•	•
LCL067-1	0.00				•	13.59	•		•
LCL068-1	0.00
LCL069-1	0.00	0.04	66.66	0.04	•	0.07	•	•	•
LCL070-1	0.00		1,345.86	1,345.86	•	5.80	•		•
LCL071-1	0.00				•	83.00
LCL072-1	0.00	0.05	0.01	0.01	•	0.01	•	•	•
LCL075-1	0.00	356.92		356.92	•	122.90
LCL076-1	0.00	0.32		0.32	•	0.44	•	•	•
LCL076-2	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL077-1	0.00	0.08		0.08	•	0.10	•	•	•
LCL079-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL080-1	0.00	29.98		29.98	•	3.75	•	•	•
LCL080-2	0.00	704.27		704.27	•	4.72	•	•	•
LCL081-1	0.00	0.01	0.00	0.00	•	0.02	•	•	•	•	•
LCL082-1	0.00	0.00	5.62	0.00	•	0.02	•	•	•	•	•
LCL083-1	0.00	1.68		1.68
LCL083-2	0.00	0.32		0.32	•	0.05	•			•
LCL084-2	0.00
LCL084-3	0.00
LCL085-1	0.00
LCL086-1	0.00	1,523.50		1,523.50	•		•			•
LCL087-1	0.00	0.06		0.06	•	0.13	•			•
LCL088-1	0.00	129.47		129.47	•	213.39	•			•
LCL089-1	0.00
LCL090-1	0.00	76.27		76.27	•	125.66	•			•
LCL091-1	0.00	1.99		1.99	•	3.46	•			•
LCL093-1	0.00
LCL094-1	0.00
LCL095-1	0.00	674.43		674.43	•		•			•
LCL096-1	0.00	0.00	0.00	0.00	•	0.02	•	•	•	•	•
LCL097-1	0.00	0.01	0.00	0.00	•	0.02	•	•	•	•	•
LCL098-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL100-1	0.00
LCL101-1	0.00	1.04	0.67	0.67	•	0.07	•	•	•
LCL102-1	0.00	0.03	0.03	0.03	•	0.01	•	•	•	•	•
LCL103-1	0.00		73.71	73.71	•	42.26
LCL104-1	0.00	0.69	0.19	0.19	•	0.04	•	•	•	•
LCL106-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL107-1	0.00	0.01	0.00	0.00	•	0.02	•	•	•	•
LCL108-1	0.00	0.43	0.06	0.06	•	0.12	•	•	•	•
LCL110-1	0.00	0.35	0.02	0.02	•	0.06	•	•	•
LCL111-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL112-1	0.00	1.83		1.83	•	0.92	•	•	•
LCL113-1	0.00				•	523.74
LCL114-1	0.00
LCL115-1	0.00				•	338.82
LCL116-1	0.00
LCL117-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL118-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL120-1	0.00	0.00	0.22	0.00	•	0.02	•	•	•	•	•
LCL121-1	0.00
LCL122-1	0.00
LCL123-1	0.00		0.03	0.03	•	0.01	•	•	•
LCL126-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL127-1	0.00
LCL128-1	0.00				•	418.15
LCL129-1	0.00
LCL130-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL131-1	0.00				•	120.36
LCL166-1	0.00
LCL256-1	0.00
LCL257-1	0.00	0.01	0.00	0.00	•	0.01	•	•	•	•
LCL355-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL356-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL357-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL358-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL360-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL361-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL362-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL363-1	0.00	0.00	0.43	0.00	•	0.03	•	•		•	•
LCL364-1	0.00	24.24	0.16	0.16	•	4.06
LCL366-1	0.00	910.90	52.96	52.96	•	73.27
LCL367-1	0.00		99.56	99.56
LCL370-1	0.00
LCL371-1	0.00
LCL373-1	0.00
LCL378-1	0.00
LCL380-1	0.00
LCL381-1	0.00
LCL382-1	0.00
LCL384-1	0.00		14.33	14.33	•	357.07
LCL385-1	0.00
LCL386-1	0.00
LCL387-1	0.00
LCL390-1	0.00
LCL391-1	0.00
LCL396-1	0.00
LCL397-1	0.00	0.10	0.43	0.10	•	0.27	•	•		•
LCL398-1	0.00	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL399-1	0.00	891.46		891.46	•		•	•
LCL400-1	0.00
LCL401-1	0.00
LCL402-1	0.00
LCL403-1	0.00
LCL404-1	0.00
LCL405-1	0.00
LCL416-1	0.00	59.21		59.21	•	96.97	•			•
LCL020-1	0.25
LCL031-1	0.25
LCL037-1	0.25
LCL062-1	0.25
LCL074-1	0.25
LCL092-1	0.25	32.05		32.05	•	51.16
LCL099-1	0.25
LCL105-1	0.25
LCL119-1	0.25
LCL125-1	0.25
LCL167-1	0.25
LCL359-1	0.25	0.00	0.00	0.00	•	0.01	•	•	•	•	•
LCL365-1	0.25	105.42	0.25	0.25	•	12.40
LCL368-1	0.25
LCL369-1	0.25
LCL372-1	0.25
LCL375-1	0.25
LCL376-1	0.25
LCL379-1	0.25
LCL383-1	0.25
LCL388-1	0.25
LCL389-1	0.25
LCL392-1	0.25
LCL393-1	0.25
LCL394-1	0.25
LCL028-1	0.50
LCL061-1	0.50
LCL124-1	0.50
LCL374-1	0.50
LCL377-1	0.50
LCL395-1	0.50
LCL428-1	0.50
LCL875-1	0.50
LCL063-1	0.75
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-G1	SGCD-G2	SGCD-G1+G2	CM+TABX	CMProver	TABX	S-SETHEO	SETHEO 3.3	SATCoP 0.1	lazyCoP 0.1
Totals of 196:		81	65	89	92	89	76	66	65	59	42