Found 958 TPTP 7.5.0 Problems both lash-d and satallax-3.4d can do with 10s timeout (listed below) with mode213b. mode213b is a modification of mode213 that turns off ENABLE_PATTERN_CLAUSES (since this has no effect in Lash). Lash spends a total of 104.297 seconds proving them all and Satallax spends a total of 186.262 seconds. Perhaps surprisingly, Satallax proves most of the 958 slightly faster, presumably due to the time needed to make the shared representation. Specifically 704 problems are proven faster by Satallax and 14 problems take the same time. The other 240 are proven faster by Lash. Restricting to the 240 proven faster by Lash we have: Lash total time: 78.919 Satallax total time: 167.56 So, that's most of the time for both of them and Lash is over 2 times faster on them. With the other 718 problems: Lash total time: 25.378 Satallax total time: 18.702 So these are "quick" ones where Lash is only marginally slower. === The two with the most significant improvement: Satallax time(ms) Lash time(ms) PUZ090^5 : 1300 12 LCL859^1 : 3396 29 PUZ090^5 is strange. Lash does it with 13 search steps while Satallax does it without search, but takes longer. I'll have to look closer to figure out what's happening. LCL859^1 is the opposite. Lash takes 498 search steps and Satallax takes 23381. I'd expect them to take the same number of steps (at least roughly) since the only significant difference should be the shared term representation. === 9 Problems where Lash is at least 10 times faster Satallax time(ms) Lash time(ms) Lash/Satallax Percent SYN393^4.002 : 1061 66 6% SEV019^5 : 821 51 6% SEU568^2 : 321 16 4% SEU492^1 : 1689 76 4% PUZ090^5 : 1300 12 0% PUZ081^1 : 330 31 9% LCL861^1 : 9383 308 3% LCL859^1 : 3396 29 0% LCL705^1 : 701 36 5% === 240 Problems where Lash is faster Satallax time(ms) Lash time(ms) Lash/Satallax Percent SYO576^7 : 322 179 55% SYO574^7 : 27 20 74% SYO572^7 : 21 20 95% SYO568^7 : 45 42 93% SYO545^1 : 27 22 81% SYO544^1 : 414 346 83% SYO505^1 : 6400 4234 66% SYO500^1.008 : 24 18 75% SYO500^1.007 : 19 17 89% SYO500^1.006 : 21 18 85% SYO497^6 : 26 24 92% SYO474^6 : 25 22 88% SYO471^6 : 34 25 73% SYO470^6 : 115 39 33% SYO469^6 : 356 184 51% SYO469^5 : 516 400 77% SYO468^6 : 21 20 95% SYO464^5 : 28 20 71% SYO463^6 : 60 38 63% SYO463^5 : 47 37 78% SYO462^6 : 25 20 80% SYO462^5 : 24 21 87% SYO462^4 : 18 17 94% SYO460^6 : 29 19 65% SYO459^6 : 411 226 54% SYO459^4 : 217 129 59% SYO458^3 : 18 15 83% SYO454^6 : 23 22 95% SYO451^6 : 79 45 56% SYO451^5 : 70 40 57% SYO450^6 : 24 21 87% SYO450^5 : 29 26 89% SYO449^1 : 323 148 45% SYO448^1 : 38 32 84% SYO447^1 : 699 297 42% SYO446^1 : 116 72 62% SYO444^1 : 1169 627 53% SYO443^1 : 186 63 33% SYO441^1 : 408 89 21% SYO440^1 : 168 137 81% SYO437^1 : 457 255 55% SYO436^1 : 162 26 16% SYO435^1 : 2354 1568 66% SYO434^1 : 76 46 60% SYO433^1 : 69 43 62% SYO432^1 : 69 54 78% SYO423^1 : 21 20 95% SYO417^1 : 27 26 96% SYO415^1 : 24 22 91% SYO382^5 : 110 36 32% SYO234^5 : 20 14 70% SYO220^5 : 12 11 91% SYO197^5 : 15 12 80% SYO175^5 : 95 70 73% SYO154^5 : 20 19 95% SYO114^5 : 32 15 46% SYO113^5 : 141 34 24% SYO111^5 : 16 14 87% SYO102^5 : 21 16 76% SYO084^5 : 57 45 78% SYO068^4.001 : 41 30 73% SYO064^4.001 : 35 18 51% SYO060^4 : 29 26 89% SYO058^4 : 17 14 82% SYN978^4 : 50 47 94% SYN397^7 : 1443 741 51% SYN393^4.002 : 1061 66 6% SYN391^4 : 26 24 92% SYN390^4 : 24 17 70% SYN365^5 : 1083 537 49% SYN056^5 : 78 20 25% SYN045^4 : 2434 341 14% SYN044^4 : 628 200 31% SYN041^4 : 3701 1780 48% SEV434^1 : 17 16 94% SEV405^5 : 14 13 92% SEV391^5 : 58 46 79% SEV233^5 : 163 22 13% SEV218^5 : 554 82 14% SEV135^5 : 14 13 92% SEV108^5 : 398 221 55% SEV104^5 : 30 23 76% SEV097^5 : 47 39 82% SEV096^5 : 58 38 65% SEV091^5 : 70 63 90% SEV081^5 : 29 17 58% SEV053^5 : 172 105 61% SEV034^5 : 5815 4535 77% SEV019^5 : 821 51 6% SEV017^5 : 23 20 86% SEU937^5 : 22 15 68% SEU935^5 : 669 360 53% SEU934^5 : 14 12 85% SEU901^5 : 1527 862 56% SEU895^5 : 16 15 93% SEU857^5 : 18 16 88% SEU850^5 : 15 13 86% SEU834^5 : 16 13 81% SEU827^1 : 17 13 76% SEU817^2 : 57 43 75% SEU813^2 : 3454 2131 61% SEU786^2 : 133 65 48% SEU758^2 : 3363 1964 58% SEU747^2 : 203 115 56% SEU746^2 : 182 50 27% SEU739^2 : 1377 749 54% SEU738^2 : 310 238 76% SEU723^2 : 6252 2849 45% SEU722^2 : 2285 918 40% SEU721^2 : 543 338 62% SEU720^2 : 196 115 58% SEU719^2 : 71 41 57% SEU718^2 : 50 31 62% SEU715^2 : 1911 1065 55% SEU697^1 : 47 33 70% SEU694^1 : 43 36 83% SEU693^1 : 44 30 68% SEU661^1 : 35 28 80% SEU644^2 : 125 64 51% SEU641^2 : 376 225 59% SEU641^1 : 5567 2902 52% SEU636^1 : 280 116 41% SEU622^2 : 123 40 32% SEU615^2 : 646 434 67% SEU614^2 : 372 162 43% SEU606^2 : 32 28 87% SEU605^2 : 45 34 75% SEU599^2 : 6354 3318 52% SEU596^2 : 424 258 60% SEU594^2 : 5945 2713 45% SEU586^2 : 254 151 59% SEU575^1 : 27 23 85% SEU574^2 : 96 58 60% SEU574^1 : 118 65 55% SEU568^2 : 321 16 4% SEU567^2 : 68 43 63% SEU566^2 : 23 21 91% SEU554^1 : 27 23 85% SEU552^1 : 28 21 75% SEU551^3 : 14 12 85% SEU532^2 : 19 17 89% SEU531^2 : 1293 766 59% SEU527^2 : 58 53 91% SEU527^1 : 172 76 44% SEU523^2 : 1802 953 52% SEU522^2 : 140 89 63% SEU521^2 : 198 127 64% SEU516^2 : 104 62 59% SEU515^2 : 155 58 37% SEU512^2 : 2462 1189 48% SEU509^2 : 23 21 91% SEU506^2 : 24 21 87% SEU501^2 : 13 12 92% SEU498^1 : 33 22 66% SEU497^1 : 90 88 97% SEU493^1 : 166 49 29% SEU492^1 : 1689 76 4% SEU490^1 : 21 20 95% SEU465^1 : 76 14 18% SEU455^1 : 20 17 85% SET716^4 : 25 21 84% SET680^3 : 20 19 95% SET647^3 : 20 18 90% SET623^5 : 14 13 92% SET623^3 : 24 16 66% SET611^3 : 17 13 76% SET589^5 : 16 12 75% SET583^7 : 1632 1484 90% SET575^7 : 3606 1935 53% SET027^7 : 5834 3085 52% SET011^5 : 62 16 25% SET002^7 : 1840 1052 57% SCT171^2 : 309 58 18% SCT171^1 : 48 40 83% PUZ092^5 : 488 100 20% PUZ090^5 : 1300 12 0% PUZ085^1 : 51 41 80% PUZ081^1 : 330 31 9% PLA032^7 : 1006 605 60% NUM793^1 : 53 40 75% NUM792^1 : 70 48 68% NUM781^1 : 13 12 92% NUM771^1 : 16 15 93% NUM770^1 : 3953 1992 50% NUM769^1 : 51 40 78% NUM748^1 : 22 15 68% NUM747^1 : 1920 1207 62% NUM746^1 : 119 29 24% NUM743^1 : 120 33 27% NUM742^1 : 94 35 37% NUM739^1 : 616 172 27% NUM738^1 : 212 124 58% NUM728^1 : 5628 3929 69% NUM703^1 : 25 24 96% NUM698^1 : 294 231 78% NUM667^1 : 34 20 58% NUM666^1 : 57 30 52% NUM665^1 : 123 53 43% NUM664^1 : 24 20 83% NUM663^1 : 35 29 82% NUM654^1 : 14 11 78% NUM635^4 : 5961 665 11% LCL873^1 : 838 493 58% LCL868^1 : 350 212 60% LCL862^1 : 4719 1412 29% LCL861^1 : 9383 308 3% LCL859^1 : 3396 29 0% LCL725^1 : 190 175 92% LCL724^1 : 31 26 83% LCL707^1 : 36 26 72% LCL706^1 : 526 306 58% LCL705^1 : 701 36 5% LCL702^1 : 28 26 92% LCL700^1 : 18 17 94% LCL604^1 : 54 53 98% LCL597^1 : 28 22 78% LCL590^1 : 17 14 82% LCL589^1 : 18 14 77% LCL586^1 : 16 12 75% LCL460^7 : 3589 1982 55% KRS276^7 : 23 17 73% KRS275^7 : 5973 3346 56% ITP128^1 : 65 33 50% ITP094^1 : 3466 1366 39% ITP056^1 : 40 26 65% ITP055^1 : 56 33 58% ITP049^1 : 164 31 18% ITP041^1 : 49 37 75% ITP039^1 : 46 38 82% ITP010^5 : 2075 848 40% CSR149^1 : 490 142 28% CSR148^1 : 622 246 39% CSR141^1 : 1194 755 63% CSR135^2 : 111 15 13% CSR135^1 : 96 14 14% CSR128^1 : 32 19 59% ALG260^2 : 4585 3352 73% ALG250^3 : 34 33 97% ALG248^3 : 266 84 31% AGT028^2 : 93 59 63% === 958 TPTP 7.5.0 Problems both lash-d and satallax-3.4d can do with 10s timeout AGT028^2 ALG248^3 ALG250^3 ALG260^2 CSR119^1 CSR120^1 CSR121^1 CSR122^1 CSR124^1 CSR125^1 CSR126^1 CSR127^1 CSR128^1 CSR135^1 CSR135^2 CSR141^1 CSR148^1 CSR149^1 CSR151^1 CSR152^1 ITP001^1 ITP001^2 ITP001^5 ITP010^1 ITP010^2 ITP010^5 ITP019^1 ITP019^2 ITP039^1 ITP041^1 ITP049^1 ITP055^1 ITP056^1 ITP094^1 ITP128^1 KRS275^7 KRS276^7 LCL460^7 LCL579^1 LCL579^2 LCL580^1 LCL581^1 LCL583^1 LCL584^1 LCL585^1 LCL586^1 LCL587^1 LCL588^1 LCL589^1 LCL590^1 LCL591^1 LCL592^1 LCL597^1 LCL604^1 LCL606^1 LCL607^1 LCL608^1 LCL609^1 LCL611^1 LCL612^1 LCL613^1 LCL614^1 LCL620^1 LCL624^1 LCL699^1 LCL700^1 LCL701^1 LCL702^1 LCL703^1 LCL704^1 LCL705^1 LCL706^1 LCL707^1 LCL719^1 LCL720^1 LCL721^1 LCL722^1 LCL723^1 LCL724^1 LCL725^1 LCL859^1 LCL861^1 LCL862^1 LCL867^1 LCL868^1 LCL870^1 LCL871^1 LCL873^1 MSC025^2 NLP264^7 NUM415^1 NUM416^1 NUM417^1 NUM635^1 NUM635^2 NUM635^4 NUM639^1 NUM641^1 NUM652^1 NUM653^1 NUM654^1 NUM655^1 NUM656^1 NUM657^1 NUM658^1 NUM659^1 NUM660^1 NUM663^1 NUM664^1 NUM665^1 NUM666^1 NUM667^1 NUM671^1 NUM674^1 NUM694^1 NUM697^1 NUM698^1 NUM699^1 NUM700^1 NUM701^1 NUM702^1 NUM703^1 NUM706^1 NUM708^1 NUM726^1 NUM728^1 NUM730^1 NUM736^1 NUM738^1 NUM739^1 NUM740^1 NUM742^1 NUM743^1 NUM746^1 NUM747^1 NUM748^1 NUM769^1 NUM770^1 NUM771^1 NUM781^1 NUM781^2 NUM781^3 NUM782^1 NUM783^1 NUM784^1 NUM785^1 NUM786^1 NUM787^1 NUM788^1 NUM789^1 NUM790^1 NUM791^1 NUM792^1 NUM793^1 PLA032^7 PUZ081^1 PUZ081^3 PUZ082^1 PUZ083^1 PUZ084^1 PUZ085^1 PUZ088^5 PUZ090^5 PUZ092^5 PUZ093^5 PUZ100^5 PUZ102^5 PUZ137^1 PUZ146^1 SCT171^1 SCT171^2 SET002^7 SET008^5 SET009^5 SET010^5 SET011^5 SET014^4 SET014^5 SET017^1 SET027^5 SET027^7 SET043^5 SET044^5 SET046^5 SET062^5 SET062^6 SET063^5 SET066^1 SET067^1 SET076^1 SET086^1 SET096^1 SET143^3 SET143^5 SET144^5 SET159^5 SET162^5 SET169^5 SET171^3 SET171^5 SET173^5 SET175^5 SET183^5 SET185^5 SET194^5 SET196^5 SET199^5 SET200^5 SET201^5 SET575^7 SET580^3 SET580^5 SET582^5 SET583^7 SET584^5 SET585^5 SET586^5 SET587^5 SET588^5 SET589^5 SET590^5 SET591^5 SET592^5 SET593^5 SET594^5 SET595^5 SET596^5 SET599^5 SET600^5 SET601^3 SET601^5 SET603^5 SET604^5 SET605^5 SET606^3 SET606^5 SET607^3 SET607^5 SET608^5 SET609^3 SET609^5 SET610^5 SET611^3 SET611^5 SET612^3 SET612^5 SET613^5 SET614^3 SET614^5 SET615^3 SET615^5 SET616^5 SET617^5 SET618^5 SET619^5 SET620^5 SET621^5 SET622^5 SET623^3 SET623^5 SET624^3 SET624^5 SET625^5 SET626^5 SET627^5 SET628^5 SET629^5 SET630^3 SET630^5 SET631^5 SET632^5 SET633^5 SET634^5 SET635^5 SET636^5 SET638^5 SET640^3 SET646^3 SET647^3 SET648^3 SET649^3 SET651^3 SET657^3 SET669^3 SET670^3 SET671^3 SET672^3 SET673^3 SET680^3 SET683^3 SET684^3 SET716^4 SET764^4 SEU453^1 SEU454^1 SEU455^1 SEU456^1 SEU457^1 SEU458^1 SEU459^1 SEU460^1 SEU465^1 SEU467^1 SEU472^1 SEU474^1 SEU490^1 SEU492^1 SEU493^1 SEU494^1 SEU495^1 SEU497^1 SEU498^1 SEU501^2 SEU502^2 SEU503^2 SEU505^2 SEU506^2 SEU507^1 SEU509^1 SEU509^2 SEU511^2 SEU512^2 SEU513^2 SEU515^2 SEU516^2 SEU518^2 SEU521^2 SEU522^2 SEU523^2 SEU526^2 SEU527^1 SEU527^2 SEU528^2 SEU530^2 SEU531^2 SEU532^2 SEU535^2 SEU536^2 SEU537^2 SEU538^2 SEU539^2 SEU541^2 SEU547^1 SEU547^2 SEU548^2 SEU549^2 SEU551^1 SEU551^2 SEU551^3 SEU552^1 SEU552^2 SEU553^1 SEU553^2 SEU554^1 SEU555^1 SEU559^2 SEU561^2 SEU562^2 SEU563^2 SEU564^2 SEU565^2 SEU566^2 SEU567^2 SEU568^2 SEU569^2 SEU574^1 SEU574^2 SEU575^1 SEU575^2 SEU578^2 SEU586^2 SEU594^2 SEU596^2 SEU599^2 SEU605^2 SEU606^2 SEU614^2 SEU615^2 SEU622^2 SEU636^1 SEU636^2 SEU641^1 SEU641^2 SEU644^2 SEU650^2 SEU661^1 SEU661^2 SEU662^2 SEU663^2 SEU693^1 SEU693^2 SEU694^1 SEU694^2 SEU697^1 SEU697^2 SEU715^2 SEU718^2 SEU719^2 SEU720^2 SEU721^2 SEU722^2 SEU723^2 SEU724^2 SEU738^2 SEU739^2 SEU746^2 SEU747^2 SEU758^2 SEU786^2 SEU808^2 SEU809^2 SEU810^2 SEU812^2 SEU813^2 SEU814^2 SEU817^2 SEU821^2 SEU826^1 SEU827^1 SEU828^1 SEU829^1 SEU831^5 SEU832^5 SEU833^5 SEU834^5 SEU836^5 SEU839^5 SEU841^5 SEU842^5 SEU843^5 SEU845^5 SEU846^5 SEU847^5 SEU848^5 SEU849^5 SEU850^5 SEU851^5 SEU852^5 SEU853^5 SEU854^5 SEU855^5 SEU856^5 SEU857^5 SEU858^5 SEU883^5 SEU884^5 SEU885^5 SEU886^5 SEU887^5 SEU888^5 SEU889^5 SEU890^5 SEU891^5 SEU893^5 SEU895^5 SEU896^5 SEU899^5 SEU901^5 SEU908^5 SEU919^5 SEU920^5 SEU923^5 SEU925^5 SEU926^5 SEU928^5 SEU934^5 SEU935^5 SEU936^5 SEU937^5 SEU941^5 SEU967^5 SEV012^5 SEV013^5 SEV014^5 SEV015^5 SEV017^5 SEV019^5 SEV034^5 SEV043^5 SEV045^5 SEV047^5 SEV048^5 SEV049^5 SEV051^5 SEV053^5 SEV056^5 SEV060^5 SEV061^5 SEV065^5 SEV067^5 SEV079^5 SEV081^5 SEV088^5 SEV091^5 SEV096^5 SEV097^5 SEV104^5 SEV108^5 SEV121^5 SEV122^5 SEV131^5 SEV134^5 SEV135^5 SEV159^5 SEV160^5 SEV161^5 SEV187^5 SEV188^5 SEV218^5 SEV225^5 SEV227^5 SEV229^5 SEV231^5 SEV232^5 SEV233^5 SEV235^5 SEV241^5 SEV258^5 SEV272^5 SEV282^5 SEV285^5 SEV286^5 SEV288^5 SEV290^5 SEV383^5 SEV387^5 SEV388^5 SEV389^5 SEV390^5 SEV391^5 SEV392^5 SEV393^5 SEV394^5 SEV396^5 SEV397^5 SEV405^5 SEV406^5 SEV408^5 SEV409^5 SEV411^5 SEV412^5 SEV413^5 SEV416^5 SEV417^5 SEV427^1 SEV433^1 SEV434^1 SWV429^1 SWV429^2 SWV435^3 SWW469^1 SYN000^1 SYN041^4 SYN044^4 SYN045^4 SYN049^5 SYN051^5 SYN055^5 SYN056^5 SYN057^5 SYN058^5 SYN059^5 SYN064^5 SYN355^5 SYN356^5 SYN357^5 SYN357^7 SYN358^5 SYN360^5 SYN361^5 SYN365^5 SYN374^5 SYN375^5 SYN377^5 SYN381^5 SYN382^5 SYN390^4 SYN391^4 SYN393^4.002 SYN397^7 SYN731^5 SYN732^5 SYN915^4 SYN978^4 SYN983^1 SYN984^1 SYN987^2 SYN988^2 SYN989^1 SYN989^3 SYN992^1 SYN998^1 SYN999^1 SYO001^1 SYO002^1 SYO003^1 SYO004^1 SYO005^1 SYO006^1 SYO007^1 SYO008^1 SYO009^1 SYO010^1 SYO011^1 SYO012^1 SYO013^1 SYO015^1 SYO016^1 SYO017^1 SYO018^1 SYO019^1 SYO020^1 SYO021^1 SYO022^1 SYO023^1 SYO024^1 SYO025^1 SYO026^1 SYO027^1 SYO028^1 SYO035^1 SYO039^1 SYO039^2 SYO040^1 SYO040^2 SYO041^1 SYO041^2 SYO042^1 SYO042^2 SYO043^1 SYO044^1 SYO045^1 SYO046^1 SYO047^1 SYO048^1 SYO049^1 SYO058^4 SYO059^4 SYO060^4 SYO061^4 SYO064^4.001 SYO066^4.001 SYO068^4.001 SYO076^5 SYO077^5 SYO078^5 SYO079^5 SYO080^5 SYO081^5 SYO082^5 SYO083^5 SYO084^5 SYO085^5 SYO086^5 SYO087^5 SYO088^5 SYO089^5 SYO090^5 SYO091^5 SYO092^5 SYO093^5 SYO094^5 SYO095^5 SYO096^5 SYO098^5 SYO099^5 SYO101^5 SYO102^5 SYO104^5 SYO107^5 SYO108^5 SYO109^5 SYO111^5 SYO112^5 SYO113^5 SYO114^5 SYO118^5 SYO119^5 SYO120^5 SYO123^5 SYO124^5 SYO125^5 SYO128^5 SYO129^5 SYO131^5 SYO132^5 SYO133^5 SYO134^5 SYO135^5 SYO136^5 SYO139^5 SYO140^5 SYO141^5 SYO142^5 SYO143^5 SYO145^5 SYO146^5 SYO147^5 SYO148^5 SYO149^5 SYO154^5 SYO159^5 SYO160^5 SYO161^5 SYO171^5 SYO175^5 SYO183^5 SYO183^6 SYO184^5 SYO185^5 SYO186^5 SYO187^5 SYO188^5 SYO189^5 SYO190^5 SYO191^5 SYO192^5 SYO193^5 SYO195^5 SYO196^5 SYO197^5 SYO198^5 SYO199^5 SYO200^5 SYO202^5 SYO203^5 SYO204^5 SYO205^5 SYO206^5 SYO207^5 SYO212^5 SYO214^5 SYO215^5 SYO216^5 SYO217^5 SYO220^5 SYO226^5 SYO229^5 SYO230^5 SYO231^5 SYO232^5 SYO233^5 SYO234^5 SYO235^5 SYO236^5 SYO237^5 SYO238^5 SYO250^5 SYO252^5 SYO253^5 SYO256^5 SYO258^5 SYO259^5 SYO260^5 SYO265^5 SYO267^5 SYO271^5 SYO274^5 SYO277^5 SYO281^5 SYO282^5 SYO285^5 SYO286^5 SYO289^5 SYO290^5 SYO291^5 SYO292^5 SYO293^5 SYO296^5 SYO299^5 SYO304^5 SYO305^5 SYO307^5 SYO308^5 SYO344^5 SYO345^5 SYO346^5 SYO347^5 SYO348^5 SYO349^5 SYO350^5 SYO351^5 SYO352^5 SYO353^5 SYO354^5 SYO355^5 SYO356^5 SYO358^5 SYO359^5 SYO361^5 SYO365^5 SYO366^5 SYO367^5 SYO368^5 SYO369^5 SYO370^5 SYO371^5 SYO372^5 SYO373^5 SYO375^5 SYO376^5 SYO377^5 SYO380^5 SYO381^5 SYO382^5 SYO389^5 SYO390^5 SYO393^1 SYO394^1 SYO395^1 SYO396^1 SYO397^1 SYO398^1 SYO399^1 SYO400^1 SYO401^1 SYO402^1 SYO403^1 SYO404^1 SYO405^1 SYO406^1 SYO407^1 SYO408^1 SYO409^1 SYO410^1 SYO411^1 SYO412^1 SYO413^1 SYO414^1 SYO415^1 SYO416^1 SYO417^1 SYO418^1 SYO419^1 SYO420^1 SYO421^1 SYO422^1 SYO423^1 SYO424^1 SYO425^1 SYO426^1 SYO427^1 SYO428^1 SYO429^1 SYO431^1 SYO432^1 SYO433^1 SYO434^1 SYO435^1 SYO436^1 SYO437^1 SYO440^1 SYO441^1 SYO443^1 SYO444^1 SYO446^1 SYO447^1 SYO448^1 SYO449^1 SYO450^3 SYO450^4 SYO450^5 SYO450^6 SYO451^5 SYO451^6 SYO454^6 SYO455^2 SYO455^3 SYO455^4 SYO455^5 SYO455^6 SYO456^4 SYO456^6 SYO457^3 SYO457^4 SYO457^5 SYO457^6 SYO458^2 SYO458^3 SYO458^4 SYO458^5 SYO458^6 SYO459^4 SYO459^6 SYO460^1 SYO460^2 SYO460^3 SYO460^4 SYO460^5 SYO460^6 SYO462^2 SYO462^3 SYO462^4 SYO462^5 SYO462^6 SYO463^5 SYO463^6 SYO464^4 SYO464^5 SYO464^6 SYO468^6 SYO469^5 SYO469^6 SYO470^6 SYO471^6 SYO474^6 SYO475^6 SYO476^6 SYO478^6 SYO480^6 SYO481^6 SYO482^6 SYO483^6 SYO485^6 SYO487^6 SYO488^6 SYO495^6 SYO497^6 SYO499^1 SYO500^1.002 SYO500^1.003 SYO500^1.004 SYO500^1.005 SYO500^1.006 SYO500^1.007 SYO500^1.008 SYO500^1 SYO501^1 SYO502^1 SYO503^1 SYO504^1 SYO505^1 SYO507^1 SYO512^1 SYO515^1 SYO520^1 SYO526^1 SYO530^1 SYO534^1 SYO536^1 SYO537^1 SYO538^1 SYO539^1 SYO540^1 SYO544^1 SYO545^1 SYO546^1 SYO547^1 SYO549^1 SYO554^1 SYO555^1 SYO556^1 SYO566^7 SYO568^7 SYO570^7 SYO572^7 SYO574^7 SYO576^7