> Hopefully everything is right. Fingers crossed. So it seems! As far as I can see, it reduces to 2437 steps towards L1 using --transform -z, but I only used the five theorems from w4.mm (which are ax1, id, luk1, luk2, th0), not the inferences — but you could still use their greatest subproofs of theorems as well. I attached my translation of your entire w4.mm to this mail (with inferences commented out).
$ ./pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq --parse data/w4-dProofs-GG.txt -f -n -s -d -o data/tmp.txt --transform data/tmp.txt -f -n -t CCNpCCNqrCspCCqsCqp,CpCqp,Cpp,CCNppp,CCpqCCqrCpr -p -2 -d > There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 > (index 0). > There are 59 steps towards CpCqp / C0C1.0 (index 13). > There are 465 steps towards Cpp / C0.0 (index 21). > There are 1703 steps towards CCNppp / CCN0.0.0 (index 22). > There are 9513 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23). Using -z in the end resulted in: > There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 > (index 0). > There are 59 steps towards CpCqp / C0C1.0 (index 13). > There are 465 steps towards Cpp / C0.0 (index 21). > There are 1703 steps towards CCNppp / CCN0.0.0 (index 22). > There are 2437 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23). Spoiler: My incoming w4:L1 will still be multiple times smaller (currently 827, unphased by compressing with your proofs of theorems :-), and even w4:id went down to 361 steps. ________________________________ Von: [email protected] <[email protected]> im Auftrag von Gino Giotto <[email protected]> Gesendet: Mittwoch, 8. Januar 2025 22:40 An: Metamath Betreff: [Metamath] Re: Upcoming contributions to proof minimization challenges I might have something. I created a Metamath database for Walsh's fourth axiom https://github.com/GinoGiotto/w4.mm and my proof for luk1 seems shorter than the current one. Preliminary information: - All theorems are complete and verified with metamath.exe. - I saved all proofs in the normal format because the compressed one shows a lower step count (yes, this makes the database very big). - The command "SHOW TRACE_BACK luk1 /COUNT /ESSENTIAL" says that "The proof would have 9513 steps if fully expanded back to axiom references." which is lower than the 11989 step count in the table. So, if the metamath.exe count is correct and if I have not made rookie mistakes then I have a shortening of luk1 in w4. I am not 100% confident that everything is fine until I translate it into condensed detachment and verify it with pmGenerator. This email is just to claim my (potential) result before the new proofs arrive. I'm probably going to do the translation tomorrow or the day after tomorrow, and I will also attempt to shorten the proof further with the automatic compression algorithm. Hopefully everything is right. Fingers crossed. Il giorno lunedì 6 gennaio 2025 alle 12:44:29 UTC+1 [email protected] ha scritto: In probably at most a few weeks, I will post some weighty proof minimizations. I don't know if anyone else is currently working on those, but in this case I would suggest to hurry up. :-) * In Metamath's pmproofs.txt challenge<https://us.metamath.org/mmsolitaire/pmproofs.txt>, I am reducing at least 38 proofs by at least 1420 steps total. * In my minimal 1-base challenge<https://github.com/xamidi/pmGenerator/discussions/2>, I am reducing at least 22 proofs by at least 99312 steps total. I am throwing a lot of computing power at a new proof compression<https://github.com/xamidi/pmGenerator/discussions/3> algorithm that I will release as part of pmGenerator<https://github.com/xamidi/pmGenerator> along with these contributions. Afterwards, it will be extremely difficult to make further non-tiny contributions (unless I missed something significant). — Samiro Discher -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]<mailto:[email protected]>. To view this discussion visit https://groups.google.com/d/msgid/metamath/a327629a-f1e2-4437-a6d9-50ae7095235an%40googlegroups.com<https://groups.google.com/d/msgid/metamath/a327629a-f1e2-4437-a6d9-50ae7095235an%40googlegroups.com?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/9f356e3381754fe49886a382748f5da8%40rwth-aachen.de.
% a1d %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = CpCrq, for 1 premise of schema Cpq %, % a1dd %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = CpCqCsr, for 1 premise of schema CpCqr %, % a1ddd %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = CpCqCrCts, for 1 premise of schema CpCqCrs %, % a1i %DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = Cqp, for 1 premise of schema p %, % ax1 DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111 , % id DDDDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDDD1111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111D1111DDD111DDDD111DDDD111DDDD1111111111 , % luk1 DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDDD1111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111D1111DDD111DDDD111DDDD111DDDD1111111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111 , % luk2 DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111 , % mpd %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#2>DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = Cpr, for 2 premises of schemas Cpq,CpCqr %, % syl %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#2><#1> % = Cpr, for 2 premises of schemas Cpq,Cqr %, % syld %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#2>DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = CpCqs, for 2 premises of schemas CpCqr,CpCrs %, % syldd %DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD111111111DDD11DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#2>DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDD11DDDD111DDDD111D111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111DDDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111111DD1111DDDD11DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD1111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDD1111DDDD111DDDD111111DDD111DDDD111DDDD111DDDD1111111DD1111DDDD11DDDD111DDDD111DDDD1111111DD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD1111111DDDD111DD111DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DD11DDD11DDDD111DDDD111DDDD111111DDD11DDDD111DDDD111DDDD111111DDDD1111DDD1111DDD1111DDDD111DDDD111111DDD111DDD11DDDD11DDDD111DDDD111DDDD111111DDD111DDDD11111111<#1> % = CpCqCrt, for 2 premises of schemas CpCqCrs,CpCqCst %, % th0 D11 %, % th0i %DD11<#1> % = CCqsCqp, for 1 premise of schema CNpCCNqrCsp
