To the TPTPCD/SGCD Experiments main page

Results on the TPTPCD2 Corpus – Proofs with Small Compacted Size

This table shows for the 196 problems of the TPTPCD2 corpus the proving time and compacted size of proofs by SGCD and CCS in different configurations. In particular, the table shows the effect of proof structure generation by SGCD with the PSP technique as a supplement to SGCD with other generation modes and to CCS configured to find proofs with ascertained minimal compacted size.

An empty cell indicates that the problem could not be proven by the respective 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. Field #Ax shows the number of proper axioms of the problem, not counting the condensed detachment meta-level axiom and the goal.
Minimal values of the compacted size within a table row are highlighted.
All values of the compacted size are determined after n-simplification. An asterisk * indicates that n-simplification had an effect on the proof (the effect may concern a reduction of the tree size or height, not necessarily of the compacted size).
A link on a problem name leads to the problem representation on the TPTP website, which shows the problem file and results by other provers. A link on a size value leads to a graphical representation of the proof.
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.

Configurations

Min-C: Best values of CCS prover in configurations to find proofs with ascertained minimal compacted size. Hence the compacted size values in this column are minimal values for the respective problem. The particular CCS configurations are: occs001, occs002.
PSP-1-5: Best values of SGCD in five configurations with PSP as proof structure generator. To determine the best value for a problem, the solutions are lexically ordered by (1.) compacted size, (2.) tree size, (3.), height, (4.) time to find the solution, (5.) order of the contributing configuration as listed below. The particular contributing SGCD configurations are opts6 (aka SGCD-9, PSP-1), opts33 (aka PSP-2) opts36 (aka PSP-3), opts34 (aka PSP-4), opts35 (aka PSP-5). The individual contributions of these configurations are shown in subsequent columns PSP-1 to PSP-5.
Non-PSP: Best values of SGCD in eight configurations with a generator on on tree size or height, i.e., other than PSP. To determine the best value for a problem, the solutions are ordered as for column PSP-1-5. The particular contributing SGCD configurations are opts17 (aka SGCD-1), opts21 (aka SGCD-4), opts3 (aka SGCD-7), opts2 (aka SGCD-8), opts20 (aka SGCD-2), opts13 (aka SGCD-3), opts14 (aka SGCD-12), opts12 (aka SGCD-13).
PSP-1: SGCD in configuration opts6 (aka SGCD-9, PSP-1), which has PSP as proof structure generator.
PSP-2: SGCD in configuration opts33 (aka PSP-2), which has PSP as proof structure generator.
PSP-3: SGCD in configuration opts36 (aka PSP-3), which has PSP as proof structure generator.
PSP-4: SGCD in configuration opts34 (aka PSP-4), which has PSP as proof structure generator.
PSP-5: SGCD in configuration opts35 (aka PSP-5), which has PSP as proof structure generator.

Problem	Rating	#Ax	Min-C		PSP-1-5		Non-PSP		PSP-1		PSP-2		PSP-3		PSP-4		PSP-5
Totals of 196:			86		153		176		139		129		98		93		80
LCL006-1	0.00	2	0.07	5	0.06	6	0.07	5	0.06	6	1.48	6			0.16	6	1.00	6
LCL007-1	0.00	2	0.06	1	0.00	1	0.00	1	0.01	1	0.00	1	0.00	1	0.00	1	0.00	1
LCL008-1	0.00	1	0.06	5	0.01	5	0.00	5	0.00	5	0.01	5	0.00	5	0.00	5	0.01	5
LCL009-1	0.00	1	0.07	7	0.08	7	0.04	8	0.08	7	1.77	7	0.06	8	0.35	7	1.53	7
LCL010-1	0.00	1	0.05	5	0.00	5	0.01	5	0.00	5	0.01	5	0.00	5	0.00	5	0.01	5
LCL011-1	0.00	1	0.08	7	0.23	7	0.09	8	0.03	7	1.25	7	0.01	8	0.23	7	1.10	7
LCL012-1	0.00	1			404.42	13	27.59	18	9.91	16	43.73	16			404.42	13
LCL013-1	0.00	1	0.05	2	0.00	2	0.00	2	0.00	2	0.00	2			0.00	2	0.00	2
LCL014-1	0.00	1	12.66	10	1.62	11	16.45	11	1.62	11	17.82	11			121.68	11
LCL015-1	0.00	1			14.34	15	44.91	24			74.23	15			14.34	15
LCL016-1	0.00	1			1,036.13	16	85.76	31	44.84	23	116.97	18			1,036.13	16
LCL017-1	0.00	1			585.65	23	93.51	50			585.65	23
LCL018-1	0.00	1			1,582.38	15	43.45	22			35.94	15			8.96	17	1,582.38	15
LCL019-1	0.00	1					752.79	32
LCL021-1	0.00	1					212.14	56
LCL022-1	0.00	1	0.45	8	8.73	8	0.12	10	0.19	8	8.73	8	0.06	8	8.39	8	125.24	8
LCL023-1	0.00	1	0.09	7	1.74	7	0.04	8	0.05	7	1.74	7	0.20	9	0.32	7	1.51	7
LCL024-1	0.00	1	65.61	10	3.20	13	2.09	10	3.20	13					350.50	13
LCL025-1	0.00	3	0.09	6	0.01	6	0.03	7	0.02	6	0.06	6	0.01	6	0.02	6	0.05	6
LCL026-1	0.00	3			36.31	19	13.59	18	12.01	20			36.31	19
LCL027-1	0.00	3	0.05	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3
LCL029-1	0.00	4	1.08	7	0.03	8	0.25	8	0.77	8	6.03	8	0.03	8	21.12	8	345.80	8
LCL030-1	0.00	4	44.95	8	2.21	9	6.84	10	2.21	9	7.76	9	5.11	20	852.77	9
LCL032-1	0.00	1			13.83	20	515.46	29	13.83	20			46.76	29
LCL033-1	0.00	1	0.06	*6	0.00	6	0.00	6	0.01	6	0.01	6	0.00	6	0.00	6	0.01	6
LCL034-1	0.00	1			10.46	19	0.91	*16	10.46	19			45.35	29
LCL035-1	0.00	1	0.07	*5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5
LCL036-1	0.00	1	652.42	*11	0.03	11	0.06	*11	0.06	11	0.07	11	0.03	11	0.03	11	0.07	11
LCL038-1	0.00	1			3.55	22	488.31	41							3.55	22	251.38	22
LCL040-1	0.00	5	12.48	8	0.68	8	1.13	9	0.68	8	1.99	8	0.06	9	2.47	8	17.41	8
LCL041-1	0.00	5	0.06	3	0.02	4	0.00	3	0.02	4	0.10	4	0.03	4	0.06	4	0.08	4
LCL042-1	0.00	5	447.10	8	39.45	9	12.01	8					39.45	9
LCL043-1	0.00	5	0.05	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2
LCL044-1	0.00	5	0.06	3	0.01	3	0.00	3	0.01	3	0.01	3	0.01	3	0.01	3	0.01	3
LCL045-1	0.00	5	0.11	5	0.82	6	0.06	5	0.82	6	5.45	6	1.61	7	63.90	6	187.82	6
LCL046-1	0.00	3	0.05	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2
LCL047-1	0.00	3			1,553.33	12	28.47	15	1.96	13	19.05	13			1,553.33	12
LCL048-1	0.00	3			16.35	12	30.65	16	2.46	14	16.35	12			1,563.34	12
LCL049-1	0.00	3			24.01	14	227.98	19	3.15	15	24.01	14
LCL050-1	0.00	3			29.87	15	177.81	21	4.71	16	29.87	15
LCL051-1	0.00	3			23.79	14	320.31	18	4.80	16	23.79	14
LCL052-1	0.00	3			40.30	16	37.92	17	8.64	19	40.30	16
LCL053-1	0.00	3			47.50	17	48.99	18	9.09	19	47.50	17
LCL054-1	0.00	3			54.79	29	398.23	33	54.79	29
LCL055-1	0.00	3			24.26	14	32.90	15	6.21	17	24.26	14
LCL056-1	0.00	3			30.20	15	31.01	16	7.04	18	30.20	15
LCL057-1	0.00	3			10.60	20	52.96	20	10.60	20	124.63	23
LCL058-1	0.00	3			57.23	33	317.15	31	57.23	33
LCL059-1	0.00	3			40.09	16	16.44	14	6.01	17	40.09	16
LCL060-1	0.00	3			754.50	25	376.47	40	45.80	30	386.00	35	754.50	25
LCL064-1	0.00	3	0.09	6	0.01	6	0.03	7	0.02	6	0.06	6	0.01	6	0.02	6	0.05	6
LCL064-2	0.00	2	0.07	6	0.01	6	0.02	7	0.01	6	0.04	6	0.01	6	0.02	6	0.03	6
LCL065-1	0.00	3	0.25	7	0.02	7	0.01	7	0.05	7	0.26	7	0.02	7	0.09	7	0.20	7
LCL066-1	0.00	3	0.31	7	0.02	7	0.01	7	0.05	7	0.26	7	0.02	7	0.09	7	0.20	7
LCL067-1	0.00	3	770.58	10	3.55	14	4.70	13	3.55	14	6.83	14	69.05	19
LCL068-1	0.00	3			1,464.79	13	4.45	15	25.52	26	7.75	15	1.69	14	1,464.79	13
LCL069-1	0.00	3	1.65	8	0.14	8	0.01	8	0.10	8	0.48	8	0.04	8	0.14	8	0.32	8
LCL070-1	0.00	3	216.78	10	12.31	16	4.64	11	5.35	16	12.31	16	81.99	16
LCL071-1	0.00	3			1,604.22	18	5.03	13					1,604.22	18
LCL072-1	0.00	3	0.26	7	0.28	10	0.00	7	0.54	10	1.67	10	0.28	10	1.23	10	3.83	10
LCL075-1	0.00	1	0.16	8	0.02	8	0.05	8	0.05	8	0.23	8	0.02	8	0.04	8	0.15	8
LCL076-1	0.00	3	0.17	7	0.02	7	0.01	7	0.05	7	0.26	7	0.02	7	0.09	7	0.21	7
LCL076-2	0.00	4	0.05	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1
LCL077-1	0.00	3	0.08	6	0.01	6	0.01	6	0.02	6	0.06	6	0.01	6	0.03	6	0.05	6
LCL079-1	0.00	5	0.05	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3
LCL080-1	0.00	3	297.18	9	4.61	12	1.86	9	4.61	12	17.09	14	0.55	17
LCL080-2	0.00	4			4.53	12	1.96	9	4.53	12	16.40	14	0.54	17
LCL081-1	0.00	1	0.05	*6	0.00	6	0.01	6	0.01	6	0.01	6	0.00	6	0.00	6	0.01	6
LCL082-1	0.00	1	0.06	*6	0.00	6	0.00	6	0.01	6	0.01	6	0.00	6	0.00	6	0.01	6
LCL083-1	0.00	1	391.94	*11	0.08	11	0.09	11	0.12	11	0.63	11			0.08	11	0.30	11
LCL083-2	0.00	2	5.07	*8	0.02	8	0.01	8	0.03	8	0.04	8			0.02	8	0.03	8
LCL084-2	0.00	2			3.92	22	387.89	40							3.92	22	365.21	22
LCL084-3	0.00	3			4.13	22	299.16	34							4.13	22	452.67	22
LCL085-1	0.00	1			1.23	20	6.99	23			7.31	20			1.23	20	52.39	20
LCL086-1	0.00	1	19.39	*10	0.59	11	0.09	*10	0.59	11	17.03	14	0.17	14	0.99	11	1,348.10	14
LCL087-1	0.00	1	0.49	*8	0.01	8	0.01	8	0.03	8	0.07	8	0.01	8	0.03	8	0.06	8
LCL088-1	0.00	1			0.11	13	0.10	*12	2.62	13	12.70	13	0.11	13	11.34	13	218.89	13
LCL089-1	0.00	1	259.01	*10	0.43	10	11.16	11	0.43	10	4.08	11	0.32	15	0.97	11	5.14	11
LCL090-1	0.00	1			0.07	14	97.06	14	4.36	14	18.88	14	0.07	14	147.05	14	2,061.47	14
LCL091-1	0.00	1	73.47	*11	0.04	12	13.81	*11	1.96	12	9.35	12	0.04	12	7.28	12	82.14	12
LCL093-1	0.00	1			8.98	17	372.85	21	8.98	17	29.45	17	3.45	25
LCL094-1	0.00	1			0.17	14	0.13	16	3.64	14	17.42	14	0.17	14	61.04	14	1,321.63	14
LCL095-1	0.00	1			5.99	15	160.95	17	5.99	15	25.73	15	0.56	22	494.06	15
LCL096-1	0.00	3	0.06	4	0.30	6	0.00	4	0.30	6			3.10	6	23.06	6	37.31	6
LCL097-1	0.00	2	0.06	4	0.00	4	0.01	4	0.00	4	0.01	4	0.00	4	0.00	4	0.01	4
LCL098-1	0.00	1	0.05	4	0.00	4	0.00	4	0.00	4	0.00	4	0.00	4	0.00	4	0.00	4
LCL100-1	0.00	2					28.17	22
LCL101-1	0.00	2	0.10	7	0.01	8	0.03	9	0.01	8	0.02	8	0.01	8	0.01	8	0.02	8
LCL102-1	0.00	3	0.56	7	0.47	7	0.28	7	0.47	7	6.06	7	0.35	7	77.32	7	610.99	7
LCL103-1	0.00	2	1,082.13	10			170.56	13
LCL104-1	0.00	2	0.07	6	0.02	6	0.00	7	0.02	6	0.08	6	0.02	6	0.03	6	0.07	6
LCL106-1	0.00	2	0.06	4	0.00	4	0.00	4	0.00	4	0.00	4			0.00	4	0.00	4
LCL107-1	0.00	1	0.06	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5
LCL108-1	0.00	1	0.07	7	0.20	8	0.49	8	0.11	8	0.76	8	0.33	8	0.20	8	0.73	8
LCL110-1	0.00	4	0.70	7	73.86	8	0.64	7	1.00	8	6.44	9	3.65	23	73.86	8	850.12	8
LCL111-1	0.00	4	0.06	5	0.02	6	0.00	5	0.09	6	0.77	6	0.02	6	0.38	6	0.75	6
LCL112-1	0.00	4	6.40	8	833.70	9	2.66	8	2.39	10	7.83	10	3.31	22	833.70	9
LCL113-1	0.00	4			2.01	18	81.26	14	5.55	19	14.77	19	2.01	18
LCL114-1	0.00	4					1,402.52	17
LCL115-1	0.00	4			3.54	12	0.06	11	3.54	12	10.87	12	2.99	21
LCL116-1	0.00	4					2,257.80	24
LCL117-1	0.00	1	0.05	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3
LCL118-1	0.00	1	0.06	7	0.02	7	0.01	7	0.02	7	0.82	7			0.05	7	0.47	7
LCL120-1	0.00	1	0.06	6	0.00	6	0.00	6	0.01	6	0.03	6	0.00	6	0.01	6	0.03	6
LCL121-1	0.00	1	591.56	12	22.82	12	151.09	18	18.31	17			22.82	12
LCL122-1	0.00	1					601.64	18
LCL123-1	0.00	1	0.82	10	1.20	10	34.03	11	1.20	10	13.85	10	3.49	10	136.35	10	323.08	10
LCL126-1	0.00	2	0.05	4	0.00	4	0.00	4	0.00	4	0.01	4	0.00	4	0.01	4	0.01	4
LCL127-1	0.00	1			15.07	16	853.97	23	15.07	16
LCL128-1	0.00	1			224.33	16	146.46	22	17.90	17			224.33	16
LCL129-1	0.00	1	484.58	11	1.49	11	78.54	16	1.49	11			25.63	12	1,353.36	12
LCL130-1	0.00	1	0.07	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5	0.00	5
LCL131-1	0.00	1	710.53	11	962.86	11	4.60	13	2.96	11	25.24	12	7.54	11	962.86	11
LCL166-1	0.00	1			77.08	16	19.71	24			81.37	17					77.08	16
LCL256-1	0.00	3					52.90	20
LCL257-1	0.00	1	0.09	7	1.74	7	0.05	8	0.06	7	1.74	7	0.09	7	0.41	7	1.55	7
LCL355-1	0.00	3	0.05	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1
LCL356-1	0.00	3	0.05	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2
LCL357-1	0.00	3	0.05	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2	0.00	2
LCL358-1	0.00	3	0.06	4	0.00	4	0.01	4	0.01	4	0.01	4	0.00	4	0.00	4	0.01	4
LCL360-1	0.00	3	0.05	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1	0.00	1
LCL361-1	0.00	3	0.06	4	0.01	4	0.00	4	0.01	4	0.01	4	0.01	4	0.01	4	0.01	4
LCL362-1	0.00	3	0.06	4	0.01	4	0.00	4	0.01	4	0.01	4	325.67	13	0.01	4	0.01	4
LCL363-1	0.00	3	0.08	6	0.13	7	0.02	6	0.13	7	24.67	14	1.60	16	0.90	7	3.72	7
LCL364-1	0.00	3	35.66	9	16.04	11	2.43	10	3.27	13	16.04	11	0.41	12
LCL366-1	0.00	3			20.19	13	1.85	12	3.26	15	20.19	13
LCL367-1	0.00	3			1,559.65	12	4.96	13	1.99	13	20.84	13			1,559.65	12
LCL370-1	0.00	3			218.99	31	103.05	27	68.42	35	218.99	31
LCL371-1	0.00	3			218.17	31	112.13	27	68.38	35	218.17	31
LCL373-1	0.00	3			257.04	33	365.55	37	66.54	35	257.04	33
LCL378-1	0.00	3			25.47	14	27.95	14	4.51	16	25.47	14
LCL380-1	0.00	3			40.07	16	52.73	17	9.51	19	40.07	16	14.15	20
LCL381-1	0.00	3			11.89	17	1.52	18	11.89	17	46.10	17
LCL382-1	0.00	3			299.65	34	465.47	29			299.65	34
LCL384-1	0.00	3	1,785.69	10	30.51	15	19.73	14	6.25	15	30.51	15	5.29	15
LCL385-1	0.00	3					87.69	30
LCL386-1	0.00	3			156.89	26	111.69	27	34.47	26	156.89	26
LCL387-1	0.00	3			411.18	20	0.41	24	45.91	26	156.38	26	411.18	20
LCL390-1	0.00	3			45.39	30	175.77	28	45.39	30
LCL391-1	0.00	3					181.93	39
LCL396-1	0.00	3			45.68	17	85.17	21	17.75	22	45.68	17	168.81	23
LCL397-1	0.00	3	0.28	7	0.08	7	0.06	7	0.08	7	2.93	7			0.35	7	3.16	7
LCL398-1	0.00	3	0.06	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3
LCL399-1	0.00	3			14.66	20	4.27	12					14.66	20
LCL400-1	0.00	3			47.44	17	78.56	32	10.66	20	47.44	17
LCL401-1	0.00	3			22.55	24	95.10	29	22.55	24	136.63	24
LCL402-1	0.00	3			122.31	23	74.37	31	22.36	24	122.31	23	383.51	24
LCL403-1	0.00	3			55.76	33	275.30	39	55.76	33
LCL404-1	0.00	3					258.73	36
LCL405-1	0.00	3					90.06	26
LCL416-1	0.00	1	97.15	10	1.30	10	3.65	10			1.30	10			0.84	18	3.19	14
LCL020-1	0.25	1
LCL031-1	0.25	4					46.61	20
LCL037-1	0.25	1
LCL062-1	0.25	3					212.79	48
LCL074-1	0.25	1					1,040.88	*50
LCL092-1	0.25	1	45.30	*12	142.34	14	52.85	17	6.03	15	24.88	15	1.93	24	142.34	14	2,052.49	14
LCL099-1	0.25	2					246.55	20
LCL105-1	0.25	3
LCL119-1	0.25	1
LCL125-1	0.25	2
LCL167-1	0.25	1					192.46	58
LCL359-1	0.25	3	0.06	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3	0.00	3
LCL365-1	0.25	3	347.44	10	6.51	12	4.68	11	6.51	12	18.37	12	373.23	13
LCL368-1	0.25	3			11.03	16	1.22	21	11.03	16	39.71	16	26.19	17
LCL369-1	0.25	3			39.74	16	796.98	22	10.96	16	39.74	16	26.92	17
LCL372-1	0.25	3			68.10	31	0.48	24	68.10	31	233.80	32
LCL375-1	0.25	3					11.04	36
LCL376-1	0.25	3			91.30	34	118.54	30	91.30	34
LCL379-1	0.25	3			13.25	21	48.05	19	13.25	21	95.48	21
LCL383-1	0.25	3			385.29	35	2.76	29			385.29	35
LCL388-1	0.25	3					1,811.69	38
LCL389-1	0.25	3					3.93	37
LCL392-1	0.25	3			61.49	30	0.63	28	61.49	30
LCL393-1	0.25	3			65.96	31	3.94	35	65.96	31
LCL394-1	0.25	3			79.19	32	124.24	41	79.19	32
LCL028-1	0.50	3					107.89	28
LCL061-1	0.50	3					6.79	36
LCL124-1	0.50	1
LCL374-1	0.50	3			83.83	33	3.70	32	83.83	33
LCL377-1	0.50	3			205.71	19	12.04	37	81.70	33	429.31	36	205.71	19
LCL395-1	0.50	3					28.16	40
LCL428-1	0.50	4
LCL875-1	0.50	4
LCL063-1	0.75	3
LCL109-1	0.75	4
LCL417-1	0.75	1
LCL422-1	0.75	4
LCL876+1	0.93	4
LCL073-1	1.00	1
LCL418-1	1.00	1
LCL419-1	1.00	4
LCL420-1	1.00	4
LCL421-1	1.00	4
LCL425-1	1.00	3
LCL426-1	1.00	3
Problem	Rating	#Ax	Min-C		PSP-1-5		Non-PSP		PSP-1		PSP-2		PSP-3		PSP-4		PSP-5
Totals of 196:			86		153		176		139		129		98		93		80