To the CCS 2022-04 Experiments main page

Pure D-Term Proofs with Minimal Compacted Size

This experiment shows results on finding proofs with minimal compacted size for problems in the TPTCD2 corpus.

Explanation of the Table Columns

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 proving problem set to 2400s. Shown times are wall clock times in seconds.

Problem: The 196 problems of the TPTPCD2 corpus.
Rating: Problem rating according to latest value of the Rating field in TPTP 7.5.0.
#Ax: Number of axioms of the problem, not counting the condensed detachment meta-level axiom and the goal.
C: Minimal compacted size of proofs of the problem as determined by runs of CCS in configurations M1 and M2. If no proof could be found by these, the largest exhaustively searched compacted size is shown prefixed with ≥. Totals shows the number of problems for which a proof with minimal compacted size could be found.
#Prf: Number of proofs of the problem which have the minimal compacted size. If the search space for that size could not be completely explored by at least one of M1 or M2, the maximum number of different proof found be these configurations is shown prefixed with ≥. Totals shows the number of problems for which the number of proofs with minimal compacted size could be determined.
H/T: Range of height and tree size among the found proofs of minimal compacted size. Pairs height/tree size indicate that there is a proof with both of these parameter values.
T/H: Range of tree size and height among the found proofs of minimal compacted size. Similar to H/T but ordering preference is given to tree size instead of height.
M1+M2 1st: Best values of M1 1st and M2 1st.
M1 1st: Time to find the first proof for CSS in configuration M1. Totals shows the number of problems for which a proof could be found within the timeout.
M2 1st: Like M1 1st but for configuration M2.
M1+M2 all: Best values of M1 all and M2 all.
M1 all: Time to find all proofs with minimal compacted size for CSS in configuration M1. This time includes exhaustive search at the level of the minimal compacted size, that is, also after the last proof at the level has been found, search is continued until the level is fully searched. Totals shows the number of problems for which this exhaustive search terminated within the timeout.
M2 all: Like M1 all but for configuration M2.
M1+M2+M3+M4: Best values of M1 1st, M2 1st, M3 and M4. Totals shows the number of problems for which a proof could be found in any one of these configurations.
M3: Time to find a proof for CSS in configuration M3. (This configuration does not systematically find proofs with minimal compacted size.) Totals shows the number of problems for which a proof could be found within the timeout.
M4: Time to find a proof for CSS in configuration M4. (This configuration does not systematically find proofs with minimal compacted size.) Totals shows the number of problems for which a proof could be found within the timeout.

Problem	Rating	#Ax	Min C	#Prf	H/T	T/H	M1+M2 1st	M1 1st	M2 1st	M1+M2 all	M1 all	M2 all	M1+M2+M3+M4	M3	M4
Totals of 196:			86	79			86	85	83	79	79	79	94	86	85
LCL006-1	0.00	2	5	1	4/7	7/4	0.07	0.10	0.07	0.08	0.12	0.08	0.07	0.07	0.08
LCL007-1	0.00	2	1	1	1/1	1/1	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL008-1	0.00	1	5	4	5/5–5/9	5/5–9/5	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL009-1	0.00	1	7	2	6/17–7/16	16/7–17/6	0.07	0.08	0.07	0.20	0.20	0.20	0.07	0.07	0.07
LCL010-1	0.00	1	5	2	5/8–5/11	8/5–11/5	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL011-1	0.00	1	7	6	6/25–7/34	16/7–34/7	0.06	0.08	0.06	0.18	0.18	0.18	0.06	0.08	0.11
LCL012-1	0.00	1	≥10
LCL013-1	0.00	1	2	1	2/2	2/2	0.05	0.05	0.06	0.07	0.07	0.07	0.05	0.06	0.06
LCL014-1	0.00	1	10	1	7/15	15/7	12.66	12.66	161.37	162.97	168.18	162.97	12.66	65.04	753.70
LCL015-1	0.00	1	≥10
LCL016-1	0.00	1	≥10
LCL017-1	0.00	1	≥11
LCL018-1	0.00	1	≥10
LCL019-1	0.00	1	≥10
LCL021-1	0.00	1	≥10
LCL022-1	0.00	1	8	91	5/14–8/49	13/8–49/8	0.21	0.38	0.21	2.26	2.27	2.26	0.09	0.19	0.09
LCL023-1	0.00	1	7	4	6/15–7/18	15/6–21/6	0.07	0.07	0.09	0.20	0.20	0.20	0.07	0.07	0.09
LCL024-1	0.00	1	10	5	8/15–10/16	15/8–26/9	11.46	11.46	65.61	152.83	152.83	156.74	6.36	6.36
LCL025-1	0.00	3	6	1	6/9	9/6	0.09	0.14	0.09	0.17	0.17	0.17	0.08	0.10	0.08
LCL026-1	0.00	3	≥9
LCL027-1	0.00	3	3	1	3/3	3/3	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.05	0.05
LCL029-1	0.00	4	7	1	6/14	14/6	1.08	6.88	1.08	8.11	8.16	8.11	0.59	5.35	0.59
LCL030-1	0.00	4	8	6	5/18–6/18	15/6–18/6	30.51	44.94	30.51	200.86	205.08	200.86	30.51	42.51	92.95
LCL032-1	0.00	1	≥11
LCL033-1	0.00	1	6	30	6/7–6/19	7/6–19/6	0.06	0.06	0.06	0.08	0.08	0.08	0.06	0.06	0.06
LCL034-1	0.00	1	≥11
LCL035-1	0.00	1	5	40	5/6–5/23	6/5–23/5	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.05
LCL036-1	0.00	1	11	36	11/59–11/131	59/11–131/11	652.42	652.42	654.11	1,242.57	1,244.89	1,242.57	0.22	7.45	0.22
LCL038-1	0.00	1	≥11
LCL040-1	0.00	5	8	12	5/9–8/19	9/5–19/8	6.27	12.48	6.27	86.19	88.70	86.19	0.23	2.32	0.23
LCL041-1	0.00	5	3	1	2/3	3/2	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL042-1	0.00	5	8	30	4/8–8/12	8/4–16/7	113.06	447.10	113.06	2,021.91	2,021.91	2,044.27	113.06	697.41	297.18
LCL043-1	0.00	5	2	1	2/2	2/2	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.05	0.05
LCL044-1	0.00	5	3	1	3/3	3/3	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL045-1	0.00	5	5	2	4/5	5/4	0.11	0.11	0.17	0.22	0.22	0.22	0.11	0.12	0.12
LCL046-1	0.00	3	2	1	2/2	2/2	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.05	0.05
LCL047-1	0.00	3	≥9
LCL048-1	0.00	3	≥9
LCL049-1	0.00	3	≥9
LCL050-1	0.00	3	≥9
LCL051-1	0.00	3	≥9
LCL052-1	0.00	3	≥9
LCL053-1	0.00	3	≥9
LCL054-1	0.00	3	≥9
LCL055-1	0.00	3	≥9
LCL056-1	0.00	3	≥9
LCL057-1	0.00	3	≥9
LCL058-1	0.00	3	≥9
LCL059-1	0.00	3	≥9
LCL060-1	0.00	3	≥9
LCL064-1	0.00	3	6	1	6/9	9/6	0.09	0.14	0.09	0.17	0.17	0.17	0.08	0.10	0.08
LCL064-2	0.00	2	6	1	6/9	9/6	0.07	0.09	0.07	0.11	0.11	0.11	0.06	0.07	0.06
LCL065-1	0.00	3	7	4	7/9–7/16	9/7–16/7	0.24	0.24	1.11	1.24	1.24	1.24	0.14	0.14	0.62
LCL066-1	0.00	3	7	1	7/7	7/7	0.31	0.31	1.33	1.50	1.50	1.51	0.10	0.16	0.10
LCL067-1	0.00	3	10	≥2	6/20–14/63	20/6–63/14	770.58	770.58					770.58		809.30
LCL068-1	0.00	3	≥10
LCL069-1	0.00	3	8	31	5/8–8/30	8/5–30/8	1.65	1.65	3.73	5.13	5.14	5.13	0.13	0.34	0.13
LCL070-1	0.00	3	10	≥9	6/18–7/30	18/6–30/7	216.78	216.78	1,745.41				216.78
LCL071-1	0.00	3	≥10
LCL072-1	0.00	3	7	2	4/8	8/4	0.26	0.26	0.26	0.36	0.37	0.36	0.26	1.87	10.40
LCL075-1	0.00	1	8	1	8/20	20/8	0.16	0.16	0.39	0.47	0.52	0.47	0.12	0.12	0.14
LCL076-1	0.00	3	7	8	7/9–7/17	9/7–17/7	0.16	0.16	0.94	1.18	1.18	1.18	0.10	0.10	0.11
LCL076-2	0.00	4	1	1	1/1	1/1	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL077-1	0.00	3	6	4	6/8–6/14	8/6–14/6	0.07	0.07	0.12	0.14	0.14	0.14	0.07	0.07	0.07
LCL079-1	0.00	5	3	1	3/3	3/3	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL080-1	0.00	3	9	≥61	5/12–11/43	10/8–43/11	297.18	297.18	547.04				61.30	499.87	61.30
LCL080-2	0.00	4	≥8										171.74	264.33	171.74
LCL081-1	0.00	1	6	24	6/10–6/31	10/6–31/6	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL082-1	0.00	1	6	24	6/7–6/19	7/6–19/6	0.06	0.06	0.06	0.07	0.07	0.08	0.06	0.06	0.06
LCL083-1	0.00	1	11	352	11/15–11/61	15/11–61/11	391.94	391.94	900.50	1,225.78	1,270.31	1,225.78	0.46	5.81	0.46
LCL083-2	0.00	2	8	54	8/9–8/25	9/8–25/8	5.07	5.07	7.95	14.61	14.76	14.61	0.09	0.42	0.09
LCL084-2	0.00	2	≥9
LCL084-3	0.00	3	≥9
LCL085-1	0.00	1	≥11
LCL086-1	0.00	1	10	5,600	8/22–9/199	22/8–199/9	19.39	82.72	19.39	97.92	100.59	97.92	0.26	0.99	0.26
LCL087-1	0.00	1	8	384	8/12–8/75	12/8–75/8	0.49	0.49	0.70	1.19	1.19	1.19	0.07	0.10	0.07
LCL088-1	0.00	1	≥10										3.78	35.23	3.78
LCL089-1	0.00	1	10	432	8/20–10/77	20/8–85/9	258.99	306.69	258.99	534.73	534.73	551.66	1.25	3.70	1.25
LCL090-1	0.00	1	≥12										20.89		20.89
LCL091-1	0.00	1	11	4,400	10/16–11/135	16/10–135/11	73.47	191.71	73.47	253.54	253.54	258.54	1.04	14.84	1.04
LCL093-1	0.00	1	≥11
LCL094-1	0.00	1	≥10										44.61		44.61
LCL095-1	0.00	1	≥11										1,268.47		1,268.47
LCL096-1	0.00	3	4	1	3/4	4/3	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL097-1	0.00	2	4	1	4/6	6/4	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL098-1	0.00	1	4	1	4/6	6/4	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL100-1	0.00	2	≥9
LCL101-1	0.00	2	7	6	6/11–6/17	11/6–17/6	0.07	0.08	0.07	0.16	0.16	0.16	0.07	0.07
LCL102-1	0.00	3	7	33	4/7–7/11	7/4–13/6	0.50	0.50	1.04	3.06	3.06	3.06	0.22	0.27	0.22
LCL103-1	0.00	2	10	≥33	7/36–10/30	15/9–37/9	176.20	1,151.56	176.20				25.88	164.48	25.88
LCL104-1	0.00	2	6	3	5/15–6/19	15/5–19/6	0.06	0.07	0.06	0.09	0.09	0.09	0.06	0.07	0.06
LCL106-1	0.00	2	4	1	4/4	4/4	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL107-1	0.00	1	5	1	5/9	9/5	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL108-1	0.00	1	7	1	6/20	20/6	0.07	0.08	0.07	0.10	0.10	0.10	0.07	0.08	0.07
LCL110-1	0.00	4	7	16	5/8–7/15	8/5–15/7	0.69	0.69	3.32	4.69	4.69	4.70	0.40	0.40	10.63
LCL111-1	0.00	4	5	2	3/5–4/5	5/3–5/4	0.06	0.06	0.07	0.09	0.09	0.09	0.06	0.06	0.16
LCL112-1	0.00	4	8	16	6/9–8/16	9/6–16/8	6.39	6.39	95.89	95.47	95.47	97.30	1.88	1.88	1,663.24
LCL113-1	0.00	4	≥8
LCL114-1	0.00	4	≥8
LCL115-1	0.00	4	≥9
LCL116-1	0.00	4	≥8
LCL117-1	0.00	1	3	1	3/4	4/3	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL118-1	0.00	1	7	5	5/10–7/13	8/7–13/7	0.06	0.06	0.07	0.09	0.09	0.09	0.06	0.06	0.06
LCL120-1	0.00	1	6	1	6/7	7/6	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL121-1	0.00	1	12	4	11/91–12/92	77/12–111/11	591.52	1,461.70	591.52	2,039.13	2,084.20	2,039.13	530.03	530.03
LCL122-1	0.00	1	≥12										64.61		64.61
LCL123-1	0.00	1	10	27	7/42–10/88	40/8–88/10	0.63	0.81	0.63	8.71	8.73	8.71	0.07	1.09	0.07
LCL126-1	0.00	2	4	6	3/6–4/9	4/4–9/4	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL127-1	0.00	1	≥11
LCL128-1	0.00	1	≥11										7.38		7.38
LCL129-1	0.00	1	11	≥3	11/42–13/57	42/11–62/12	484.58	484.58					0.53	450.33	0.53
LCL130-1	0.00	1	5	2	5/8–5/11	8/5–11/5	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL131-1	0.00	1	11	21	9/72–11/72	44/10–85/10	164.11	164.11	225.87	1,681.37	1,681.37	1,718.51	1.04	20.47	1.04
LCL166-1	0.00	1	≥10
LCL256-1	0.00	3	≥9
LCL257-1	0.00	1	7	12	5/11–7/22	11/5–22/7	0.06	0.06	0.07	0.14	0.14	0.14	0.06	0.06	0.06
LCL355-1	0.00	3	1	1	1/1	1/1	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL356-1	0.00	3	2	1	2/3	3/2	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL357-1	0.00	3	2	1	2/2	2/2	0.05	0.05	0.06	0.07	0.07	0.07	0.05	0.06	0.06
LCL358-1	0.00	3	4	5	3/6–4/8	5/4–8/4	0.05	0.06	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL360-1	0.00	3	1	1	1/1	1/1	0.05	0.05	0.05	0.07	0.07	0.07	0.05	0.06	0.06
LCL361-1	0.00	3	4	2	3/4–4/4	4/3–4/4	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL362-1	0.00	3	4	1	4/4	4/4	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL363-1	0.00	3	6	4	5/6–6/7	6/5–7/6	0.08	0.08	0.11	0.17	0.17	0.17	0.08	0.08	0.16
LCL364-1	0.00	3	9	3	6/17–8/14	14/8–17/6	35.66	35.66	80.54	269.73	269.73	277.18	7.38	7.38
LCL366-1	0.00	3	≥9										964.94	964.94
LCL367-1	0.00	3	≥9
LCL370-1	0.00	3	≥9
LCL371-1	0.00	3	≥9
LCL373-1	0.00	3	≥9
LCL378-1	0.00	3	≥9
LCL380-1	0.00	3	≥9
LCL381-1	0.00	3	≥9
LCL382-1	0.00	3	≥9
LCL384-1	0.00	3	10	≥1	7/26	26/7	1,785.69		1,785.69				1,785.69
LCL385-1	0.00	3	≥9
LCL386-1	0.00	3	≥9
LCL387-1	0.00	3	≥9
LCL390-1	0.00	3	≥9
LCL391-1	0.00	3	≥9
LCL396-1	0.00	3	≥9
LCL397-1	0.00	3	7	4	6/9–7/8	8/7–9/6	0.28	0.28	0.71	1.22	1.22	1.25	0.21	0.21	0.44
LCL398-1	0.00	3	3	1	3/3	3/3	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL399-1	0.00	3	≥9
LCL400-1	0.00	3	≥9
LCL401-1	0.00	3	≥9
LCL402-1	0.00	3	≥9
LCL403-1	0.00	3	≥9
LCL404-1	0.00	3	≥9
LCL405-1	0.00	3	≥9
LCL416-1	0.00	1	10	6	7/22–10/24	17/8–31/8	95.95	95.95	186.74	288.58	300.01	288.58	10.87	10.87
LCL020-1	0.25	1	≥10
LCL031-1	0.25	4	≥8
LCL037-1	0.25	1	≥11
LCL062-1	0.25	3	≥9
LCL074-1	0.25	1	≥11
LCL092-1	0.25	1	12	17,280	11/25–12/303	25/11–303/12	45.29	425.61	45.29	452.67	452.67	467.41	1.12	32.59	1.12
LCL099-1	0.25	2	≥9
LCL105-1	0.25	3	≥9
LCL119-1	0.25	1	≥10
LCL125-1	0.25	2	≥9
LCL167-1	0.25	1	≥10
LCL359-1	0.25	3	3	1	3/5	5/3	0.06	0.06	0.06	0.07	0.07	0.07	0.06	0.06	0.06
LCL365-1	0.25	3	10	≥3	7/18–9/15	15/9–18/7	347.44	347.44					38.28	38.28
LCL368-1	0.25	3	≥9
LCL369-1	0.25	3	≥9
LCL372-1	0.25	3	≥9
LCL375-1	0.25	3	≥9
LCL376-1	0.25	3	≥9
LCL379-1	0.25	3	≥9
LCL383-1	0.25	3	≥9
LCL388-1	0.25	3	≥9
LCL389-1	0.25	3	≥9
LCL392-1	0.25	3	≥9
LCL393-1	0.25	3	≥9
LCL394-1	0.25	3	≥9
LCL028-1	0.50	3	≥9
LCL061-1	0.50	3	≥9
LCL124-1	0.50	1	≥11
LCL374-1	0.50	3	≥9
LCL377-1	0.50	3	≥9
LCL395-1	0.50	3	≥9
LCL428-1	0.50	4	≥8
LCL875-1	0.50	4	≥8
LCL063-1	0.75	3	≥9
LCL109-1	0.75	4	≥8
LCL417-1	0.75	1	≥10
LCL422-1	0.75	4	≥8
LCL876+1	0.93	4	≥8
LCL073-1	1.00	1	≥11
LCL418-1	1.00	1	≥11
LCL419-1	1.00	4	≥8
LCL420-1	1.00	4	≥8
LCL421-1	1.00	4	≥8
LCL425-1	1.00	3	≥8
LCL426-1	1.00	3	≥8
Problem	Rating	#Ax	Min C	#Prf	H/T	T/H	M1+M2 1st	M1 1st	M2 1st	M1+M2 all	M1 all	M2 all	M1+M2+M3+M4	M3	M4
Totals of 196:			86	79			86	85	83	79	79	79	94	86	85