@xamidi/mmsolitaire (repository)

Branch of metamath/mmsolitaire/pmproofs of the Metamath Solitaire project.

Contributions

1. [2be2349] found 17 shorter proofs (proposal)
2. [21911f8] found 5 shorter proofs (proposal)
3. [f9a40e7] found 40 shorter proofs (proposal)
4. [9bb17b0] found 38 shorter proofs (proposal)

Summary

	Formula	Improvement(s)	Reduced by
*2.32	CAApqrApAqr	91↦83	8
*2.62	CApqCCpqq	89↦77	12
*2.73	CCpqCAApqrAqr	165↦153	12
*2.82	CAApqrCAApNrsAApqs	91↦89	2
*3.3 Exp	CCKpqrCpCqr	59↦55	4
*3.31 Imp	CCpCqrCKpqr	103↦83	20
*3.33 Syll	CKCpqCqrCpr	95↦73	22
*3.34 Syll	CKCpqCrpCrq	105↦73	32
*3.43 Comp	CKCpqCprCpKqr	137↦109	28
*3.44	CKCpqCrqCAprq	203↦161	42
*3.47	CKCpqCrsCKprKqs	203↦199	4
*3.48	CKCpqCrsCAprAqs	241↦167	74
*4.11	EEpqENpNq	363↦359	4
*4.12	EEpNqEqNp	363↦359	4
*4.14	ECKpqrCKpNrNq	321↦263	58
*4.15	ECKpqNrCKqrNp	277↦205	72
*4.22	CKEpqEqrEpr	273↦271	2
*4.32	EKKpqrKpKqr	355↦313	42
*4.33	EAApqrApAqr	207↦199	8
*4.36	CEpqEKprKqr	271↦219	52
*4.37	CEpqEAprAqr	307↦255	52
*4.38	CKEpqErsEKprKqs	585↦527	58
*4.39	CKEpqErsEAprAqs	609↦463	146
*4.4	EKpAqrAKpqKpr	355↦345	10
*4.41	EApKqrKApqApr	271↦241	30
*4.42	EpAKpqKpNq	165↦157	8
*4.52	EKpNqNANpq	219↦207	12
*4.53	ENKpNqANpq	169↦157	12
*4.72	ECpqEqApq	195↦193	2
*4.76	EKCpqCprCpKqr	271↦241	30
*4.77	EKCpqCrqCAprq	375↦265	110
*4.78	EACpqCprCpAqr	319↦191	128
*4.79	EACpqCrqCKprq	383↦259	124
*4.82	EKCpqCpNqNp	175↦157	18
*4.83	EKCpqCNpqq	245↦197	48
*4.85	CEpqECrpCrq	123↦119	4
*4.86	CEpqEEprEqr	617↦473	144
*4.87	KKECKpqrCpCqrECpCqrCqCprECqCprCKqpr	523↦439	84
*5.1	CKpqEpq	107↦87	20
*5.15	AEpqEpNq	267↦161	106
*5.16	NKEpqEpNq	333↦331	2
*5.17	EKApqNKpqEpNq	329↦285	44
*5.18	EEpqNEpNq	503↦491	12
*5.19	NEpNp	123↦105	18
*5.21	CKNpNqEpq	115↦111	4
*5.22	ENEpqAKpNqKqNp	363↦333	30
*5.23	EEpqAKpqKNpNq	513↦501	12
*5.24	ENAKpqKNpNqAKpNqKqNp	585↦545	40
*5.3	ECKpqrCKpqKpr	127↦125	2
*5.31	CKpCqrCqKrp	119↦105	14
*5.32	ECpEqrEKpqKpr	625↦621	4
*5.33	EKpCqrKpCKpqr	389↦311	78
*5.35	CKCpqCprCpEqr	159↦129	30
*5.36	EKpEpqKqEpq	381↦257	124
*5.53	ECAApqrsKKCpsCqsCrs	673↦551	122
*5.54	AEKpqpEKpqq	239↦149	90
*5.55	AEApqpEApqq	167↦165	2
*5.6	ECKpNqrCpAqr	203↦163	40
*5.61	EKApqNqKpNq	259↦231	28
*5.62	EAKpqNqApNq	167↦157	10
*5.7	EEApqArqAqEpr	673↦605	68
*5.74	ECpEqrECpqCpr	337↦333	4
*5.75	CKCpNqErAqpEKrNqp	387↦331	56
meredith	CCCCCpqCNrNsrtCCtpCsp	145↦141	4
biass	EEEpqrEpEqr	2127↦1579	548
Σ	(65 theorems)	20333↦17299	3034