TPTP-set -------- 1337 formulas 1319 first-order 18 propositional 228 Theorems 53 Non-Theorems 1056 Unknown Rating 0.0 0.01-0.25 0.26-0.50 0.51-0.75 0.76-0.99 1.0 Sum Theorem 74 21 28 97 0 8 228 Non-Theorem 2 0 5 45 1 0 53 Unknown 0 0 0 0 0 1056 1056 Propositional 5 2 5 5 1 0 18 First-Order 71 19 28 137 0 1064 1319 Sum 76 21 33 142 1 1064 1337 Domain AGT ALG COM GEO GRP HAL LCL MGT NLP PUZ SET SWC SWV SYN Theorem 14 7 3 7 0 0 1 25 11 2 75 0 1 74 Non-Theorem 0 1 0 0 0 0 2 0 0 0 0 0 0 50 Unknown 38 137 0 65 1 9 0 42 11 2 244 422 1 92 int. 0.0 0 0 0 0 0 0 1 5 3 0 14 0 1 52 >0.0 52 145 3 72 1 9 2 62 19 4 305 422 1 164 class. 0.0 43 6 1 0 0 0 3 29 7 3 40 30 1 123 >0.0 9 139 2 72 1 9 0 38 15 1 279 392 1 93 formula Status Rating AGT001+1 Theorem 0.50 AGT001+2 Theorem 0.50 AGT002+1 Theorem 0.75 AGT002+2 Theorem 0.75 AGT003+1 Theorem 0.75 AGT003+2 Theorem 0.75 AGT004+1 Theorem 0.75 AGT004+2 Theorem 0.75 AGT005+1 Theorem 0.75 AGT005+2 Theorem 0.75 AGT006+1 Unknown 1.00 AGT006+2 Unknown 1.00 AGT007+1 Unknown 1.00 AGT007+2 Unknown 1.00 AGT008+1 Unknown 1.00 AGT008+2 Unknown 1.00 AGT009+1 Unknown 1.00 AGT009+2 Unknown 1.00 AGT010+1 Unknown 1.00 AGT010+2 Unknown 1.00 AGT011+1 Unknown 1.00 AGT011+2 Unknown 1.00 AGT012+1 Unknown 1.00 AGT012+2 Unknown 1.00 AGT013+1 Unknown 1.00 AGT013+2 Unknown 1.00 AGT014+1 Unknown 1.00 AGT014+2 Unknown 1.00 AGT015+1 Theorem 0.75 AGT015+2 Theorem 0.75 AGT016+1 Unknown 1.00 AGT016+2 Unknown 1.00 AGT017+1 Theorem 0.75 AGT017+2 Theorem 0.75 AGT018+1 Unknown 1.00 AGT018+2 Unknown 1.00 AGT019+1 Unknown 1.00 AGT019+2 Unknown 1.00 AGT020+1 Unknown 1.00 AGT020+2 Unknown 1.00 AGT021+1 Unknown 1.00 AGT021+2 Unknown 1.00 AGT022+1 Unknown 1.00 AGT022+2 Unknown 1.00 AGT023+1 Unknown 1.00 AGT023+2 Unknown 1.00 AGT024+1 Unknown 1.00 AGT024+2 Unknown 1.00 AGT025+1 Unknown 1.00 AGT025+2 Unknown 1.00 AGT026+1 Unknown 1.00 AGT026+2 Unknown 1.00 ALG014+1 Unknown 1.00 ALG015+1 Unknown 1.00 ALG016+1 Unknown 1.00 ALG017+1 Theorem 0.50 ALG018+1 Unknown 1.00 ALG019+1 Unknown 1.00 ALG020+1 Unknown 1.00 ALG021+1 Unknown 1.00 ALG022+1 Unknown 1.00 ALG025+1 Unknown 1.00 ALG026+1 Unknown 1.00 ALG027+1 Unknown 1.00 ALG028+1 Theorem 0.50 ALG029+1 Unknown 1.00 ALG030+1 Unknown 1.00 ALG031+1 Unknown 1.00 ALG032+1 Unknown 1.00 ALG033+1 Unknown 1.00 ALG034+1 Non-Theorem 0.75 ALG036+1 Unknown 1.00 ALG037+1 Unknown 1.00 ALG038+1 Unknown 1.00 ALG039+1 Theorem 0.50 ALG040+1 Unknown 1.00 ALG041+1 Unknown 1.00 ALG042+1 Unknown 1.00 ALG043+1 Unknown 1.00 ALG044+1 Unknown 1.00 ALG047+1 Unknown 1.00 ALG048+1 Unknown 1.00 ALG049+1 Unknown 1.00 ALG050+1 Unknown 1.00 ALG051+1 Unknown 1.00 ALG052+1 Unknown 1.00 ALG053+1 Unknown 1.00 ALG054+1 Unknown 1.00 ALG055+1 Unknown 1.00 ALG056+1 Unknown 1.00 ALG057+1 Unknown 1.00 ALG058+1 Unknown 1.00 ALG059+1 Unknown 1.00 ALG060+1 Unknown 1.00 ALG061+1 Unknown 1.00 ALG062+1 Unknown 1.00 ALG063+1 Unknown 1.00 ALG064+1 Unknown 1.00 ALG065+1 Unknown 1.00 ALG066+1 Unknown 1.00 ALG067+1 Unknown 1.00 ALG068+1 Unknown 1.00 ALG069+1 Unknown 1.00 ALG070+1 Unknown 1.00 ALG071+1 Unknown 1.00 ALG072+1 Unknown 1.00 ALG073+1 Unknown 1.00 ALG074+1 Unknown 1.00 ALG075+1 Unknown 1.00 ALG076+1 Unknown 1.00 ALG077+1 Unknown 1.00 ALG078+1 Unknown 1.00 ALG079+1 Unknown 1.00 ALG080+1 Unknown 1.00 ALG081+1 Unknown 1.00 ALG082+1 Unknown 1.00 ALG083+1 Unknown 1.00 ALG084+1 Unknown 1.00 ALG085+1 Unknown 1.00 ALG086+1 Unknown 1.00 ALG087+1 Unknown 1.00 ALG088+1 Unknown 1.00 ALG089+1 Unknown 1.00 ALG090+1 Unknown 1.00 ALG091+1 Unknown 1.00 ALG092+1 Unknown 1.00 ALG093+1 Unknown 1.00 ALG094+1 Unknown 1.00 ALG102+1 Unknown 1.00 ALG103+1 Unknown 1.00 ALG104+1 Unknown 1.00 ALG105+1 Unknown 1.00 ALG106+1 Unknown 1.00 ALG107+1 Unknown 1.00 ALG108+1 Unknown 1.00 ALG109+1 Unknown 1.00 ALG110+1 Unknown 1.00 ALG111+1 Unknown 1.00 ALG112+1 Unknown 1.00 ALG113+1 Unknown 1.00 ALG114+1 Unknown 1.00 ALG115+1 Unknown 1.00 ALG116+1 Unknown 1.00 ALG117+1 Unknown 1.00 ALG118+1 Unknown 1.00 ALG119+1 Unknown 1.00 ALG120+1 Unknown 1.00 ALG121+1 Unknown 1.00 ALG122+1 Unknown 1.00 ALG123+1 Unknown 1.00 ALG124+1 Unknown 1.00 ALG125+1 Unknown 1.00 ALG126+1 Unknown 1.00 ALG127+1 Unknown 1.00 ALG128+1 Unknown 1.00 ALG129+1 Unknown 1.00 ALG165+1 Unknown 1.00 ALG166+1 Unknown 1.00 ALG167+1 Unknown 1.00 ALG168+1 Unknown 1.00 ALG169+1 Unknown 1.00 ALG170+1 Unknown 1.00 ALG171+1 Theorem 1.00 ALG172+1 Unknown 1.00 ALG173+1 Unknown 1.00 ALG174+1 Unknown 1.00 ALG175+1 Unknown 1.00 ALG176+1 Unknown 1.00 ALG177+1 Unknown 1.00 ALG178+1 Unknown 1.00 ALG179+1 Unknown 1.00 ALG180+1 Unknown 1.00 ALG181+1 Unknown 1.00 ALG182+1 Unknown 1.00 ALG183+1 Unknown 1.00 ALG184+1 Unknown 1.00 ALG185+1 Unknown 1.00 ALG186+1 Unknown 1.00 ALG187+1 Unknown 1.00 ALG188+1 Unknown 1.00 ALG189+1 Unknown 1.00 ALG194+1 Unknown 1.00 ALG195+1 Unknown 1.00 ALG196+1 Unknown 1.00 ALG197+1 Unknown 1.00 ALG198+1 Theorem 0.50 ALG199+1 Theorem 0.50 ALG200+1 Theorem 0.50 ALG201+1 Theorem 0.75 ALG202+1 Unknown 1.00 ALG203+1 Unknown 1.00 ALG204+1 Unknown 1.00 ALG205+1 Unknown 1.00 ALG206+1 Unknown 1.00 ALG207+1 Unknown 1.00 ALG208+1 Unknown 1.00 ALG209+1 Unknown 1.00 COM003+1 Theorem 0.75 COM003+2 Theorem 0.75 COM003+3 Theorem 0.75 GEO080+1 Theorem 0.50 GEO081+1 Theorem 0.75 GEO082+1 Unknown 1.00 GEO083+1 Unknown 1.00 GEO084+1 Theorem 1.00 GEO085+1 Theorem 1.00 GEO086+1 Unknown 1.00 GEO087+1 Unknown 1.00 GEO088+1 Unknown 1.00 GEO089+1 Unknown 1.00 GEO090+1 Unknown 1.00 GEO091+1 Unknown 1.00 GEO092+1 Unknown 1.00 GEO093+1 Unknown 1.00 GEO094+1 Unknown 1.00 GEO095+1 Unknown 1.00 GEO096+1 Unknown 1.00 GEO097+1 Unknown 1.00 GEO098+1 Unknown 1.00 GEO099+1 Unknown 1.00 GEO100+1 Unknown 1.00 GEO101+1 Unknown 1.00 GEO102+1 Unknown 1.00 GEO103+1 Unknown 1.00 GEO104+1 Unknown 1.00 GEO105+1 Unknown 1.00 GEO106+1 Unknown 1.00 GEO107+1 Unknown 1.00 GEO108+1 Unknown 1.00 GEO109+1 Unknown 1.00 GEO110+1 Unknown 1.00 GEO111+1 Unknown 1.00 GEO112+1 Theorem 0.75 GEO113+1 Unknown 1.00 GEO114+1 Unknown 1.00 GEO116+1 Unknown 1.00 GEO117+1 Theorem 0.75 GEO118+1 Theorem 0.75 GEO119+1 Unknown 1.00 GEO120+1 Unknown 1.00 GEO121+1 Unknown 1.00 GEO122+1 Unknown 1.00 GEO123+1 Unknown 1.00 GEO124+1 Unknown 1.00 GEO125+1 Unknown 1.00 GEO126+1 Unknown 1.00 GEO127+1 Unknown 1.00 GEO128+1 Unknown 1.00 GEO129+1 Unknown 1.00 GEO130+1 Unknown 1.00 GEO131+1 Unknown 1.00 GEO132+1 Unknown 1.00 GEO133+1 Unknown 1.00 GEO134+1 Unknown 1.00 GEO135+1 Unknown 1.00 GEO136+1 Unknown 1.00 GEO137+1 Unknown 1.00 GEO138+1 Unknown 1.00 GEO139+1 Unknown 1.00 GEO140+1 Unknown 1.00 GEO141+1 Unknown 1.00 GEO142+1 Unknown 1.00 GEO143+1 Unknown 1.00 GEO144+1 Unknown 1.00 GEO145+1 Unknown 1.00 GEO146+1 Unknown 1.00 GEO147+1 Theorem 0.75 GEO148+1 Theorem 0.75 GEO149+1 Unknown 1.00 GEO150+1 Unknown 1.00 GEO151+1 Unknown 1.00 GEO152+1 Unknown 1.00 GRP194+1 Unknown 1.00 HAL001+1 Unknown 1.00 HAL001+2 Unknown 1.00 HAL002+1 Unknown 1.00 HAL003+1 Unknown 1.00 HAL003+2 Unknown 1.00 HAL003+3 Theorem 1.00 HAL004+1 Unknown 1.00 HAL005+1 Unknown 1.00 HAL006+1 Unknown 1.00 LCL181+1 Non-Theorem 0.40 LCL230+1 Non-Theorem 0.40 LCL414+1 Theorem 0.00 MGT001+1 Unknown 1.00 MGT002+1 Theorem 0.75 MGT003+1 Unknown 1.00 MGT004+1 Unknown 1.00 MGT005+1 Unknown 1.00 MGT005+2 Unknown 1.00 MGT006+1 Unknown 1.00 MGT007+1 Unknown 1.00 MGT008+1 Theorem 0.75 MGT009+1 Theorem 0.75 MGT010+1 Unknown 1.00 MGT011+1 Unknown 1.00 MGT012+1 Unknown 1.00 MGT013+1 Theorem 0.75 MGT014+1 Theorem 0.75 MGT015+1 Theorem 0.75 MGT016+1 Theorem 0.75 MGT017+1 Theorem 0.75 MGT018+1 Theorem 0.75 MGT020+1 Unknown 1.00 MGT021+1 Theorem 0.75 MGT022+1 Theorem 0.00 MGT022+2 Theorem 0.00 MGT023+1 Unknown 1.00 MGT023+2 Unknown 1.00 MGT024+1 Unknown 1.00 MGT025+1 Unknown 1.00 MGT026+1 Unknown 1.00 MGT027+1 Unknown 1.00 MGT028+1 Theorem 0.00 MGT029+1 Unknown 1.00 MGT030+1 Theorem 0.25 MGT032+2 Theorem 0.00 MGT034+2 Unknown 1.00 MGT035+1 Unknown 1.00 MGT035+2 Unknown 1.00 MGT036+1 Theorem 0.50 MGT036+2 Theorem 0.50 MGT036+3 Theorem 0.00 MGT037+1 Unknown 1.00 MGT039+1 Unknown 1.00 MGT039+2 Unknown 1.00 MGT041+2 Theorem 0.25 MGT042+1 Unknown 1.00 MGT043+1 Unknown 1.00 MGT044+1 Theorem 0.75 MGT045+1 Theorem 0.75 MGT046+1 Theorem 0.75 MGT047+1 Unknown 1.00 MGT048+1 Theorem 0.75 MGT049+1 Theorem 0.75 MGT050+1 Unknown 1.00 MGT051+1 Unknown 1.00 MGT052+1 Unknown 1.00 MGT053+1 Unknown 1.00 MGT054+1 Unknown 1.00 MGT055+1 Unknown 1.00 MGT056+1 Unknown 1.00 MGT057+1 Unknown 1.00 MGT058+1 Unknown 1.00 MGT059+1 Theorem 0.75 MGT060+1 Unknown 1.00 MGT061+1 Unknown 1.00 MGT062+1 Unknown 1.00 MGT063+1 Unknown 1.00 MGT064+1 Unknown 1.00 MGT065+1 Unknown 1.00 NLP001+1 Theorem 0.00 NLP004+1 Theorem 0.75 NLP007+1 Theorem 0.75 NLP009+1 Theorem 0.75 NLP011+1 Theorem 0.75 NLP079+1 Theorem 0.25 NLP080+1 Theorem 0.25 NLP081+1 Theorem 0.25 NLP094+1 Theorem 0.25 NLP117+1 Theorem 0.00 NLP122+1 Theorem 0.00 NLP141+1 Unknown 1.00 NLP143+1 Unknown 1.00 NLP145+1 Unknown 1.00 NLP147+1 Unknown 1.00 NLP149+1 Unknown 1.00 NLP204+1 Unknown 1.00 NLP208+1 Unknown 1.00 NLP251+1 Unknown 1.00 NLP252+1 Unknown 1.00 NLP257+1 Unknown 1.00 NLP258+1 Unknown 1.00 PUZ001+1 Unknown 1.00 PUZ005+1 Unknown 1.00 PUZ031+1 Theorem 0.75 PUZ047+1 Theorem 0.75 SET002+3 Theorem 0.75 SET002+4 Theorem 0.75 SET008+3 Theorem 0.75 SET009+3 Unknown 1.00 SET010+3 Unknown 1.00 SET011+3 Unknown 1.00 SET012+4 Unknown 1.00 SET013+4 Unknown 1.00 SET014+3 Theorem 0.75 SET014+4 Unknown 1.00 SET015+4 Unknown 1.00 SET016+1 Unknown 1.00 SET016+4 Unknown 1.00 SET017+1 Unknown 1.00 SET018+1 Unknown 1.00 SET018+4 Unknown 1.00 SET019+4 Theorem 0.50 SET020+1 Unknown 1.00 SET024+1 Unknown 1.00 SET025+1 Unknown 1.00 SET027+1 Unknown 1.00 SET027+3 Theorem 0.75 SET027+4 Unknown 1.00 SET043+1 Theorem 0.00 SET044+1 Theorem 0.00 SET045+1 Theorem 0.00 SET046+1 Theorem 0.00 SET047+1 Theorem 0.75 SET054+1 Theorem 0.50 SET055+1 Theorem 0.50 SET056+1 Unknown 1.00 SET060+1 Theorem 0.75 SET061+1 Theorem 0.75 SET062+1 Theorem 0.75 SET062+3 Theorem 0.00 SET062+4 Theorem 0.75 SET063+1 Theorem 0.75 SET063+3 Theorem 0.00 SET063+4 Theorem 0.75 SET064+1 Unknown 1.00 SET065+1 Theorem 0.75 SET066+1 Unknown 1.00 SET067+1 Unknown 1.00 SET069+1 Unknown 1.00 SET071+1 Unknown 1.00 SET072+1 Unknown 1.00 SET073+1 Unknown 1.00 SET074+1 Unknown 1.00 SET076+1 Unknown 1.00 SET077+1 Unknown 1.00 SET079+1 Unknown 1.00 SET081+1 Unknown 1.00 SET082+1 Unknown 1.00 SET083+1 Unknown 1.00 SET084+1 Unknown 1.00 SET086+1 Unknown 1.00 SET090+1 Unknown 1.00 SET091+1 Unknown 1.00 SET093+1 Unknown 1.00 SET094+1 Unknown 1.00 SET095+1 Unknown 1.00 SET095+4 Unknown 1.00 SET096+1 Unknown 1.00 SET097+1 Unknown 1.00 SET098+1 Unknown 1.00 SET099+1 Unknown 1.00 SET101+1 Unknown 1.00 SET102+1 Unknown 1.00 SET103+1 Unknown 1.00 SET104+1 Unknown 1.00 SET105+1 Unknown 1.00 SET108+1 Unknown 1.00 SET113+1 Unknown 1.00 SET117+1 Unknown 1.00 SET119+1 Unknown 1.00 SET120+1 Unknown 1.00 SET121+1 Unknown 1.00 SET122+1 Unknown 1.00 SET143+3 Unknown 1.00 SET143+4 Unknown 1.00 SET144+3 Unknown 1.00 SET146+3 Theorem 0.75 SET148+3 Theorem 0.75 SET148+4 Theorem 0.75 SET155+4 Unknown 1.00 SET156+4 Unknown 1.00 SET159+3 Unknown 1.00 SET159+4 Unknown 1.00 SET162+3 Unknown 1.00 SET162+4 Theorem 0.75 SET169+3 Unknown 1.00 SET169+4 Unknown 1.00 SET171+3 Unknown 1.00 SET171+4 Unknown 1.00 SET173+3 Theorem 0.75 SET175+3 Theorem 0.75 SET183+3 Theorem 0.75 SET185+3 Theorem 0.75 SET194+3 Theorem 0.25 SET196+3 Theorem 0.25 SET199+3 Theorem 0.75 SET199+4 Unknown 1.00 SET200+3 Theorem 0.75 SET201+3 Unknown 1.00 SET347+4 Theorem 0.75 SET351+4 Unknown 1.00 SET352+4 Unknown 1.00 SET355+4 Theorem 0.75 SET358+4 Unknown 1.00 SET366+4 Theorem 0.75 SET372+4 Unknown 1.00 SET573+3 Theorem 0.00 SET574+3 Theorem 0.00 SET575+3 Theorem 0.00 SET576+3 Theorem 0.00 SET577+3 Theorem 0.75 SET578+3 Theorem 0.75 SET579+3 Theorem 0.50 SET580+3 Unknown 1.00 SET581+3 Theorem 0.75 SET582+3 Unknown 1.00 SET583+3 Theorem 0.00 SET584+3 Theorem 0.75 SET585+3 Theorem 0.50 SET586+3 Unknown 1.00 SET587+3 Unknown 1.00 SET588+3 Unknown 1.00 SET589+3 Theorem 0.25 SET590+3 Theorem 0.00 SET591+3 Theorem 0.50 SET592+3 Unknown 1.00 SET593+3 Unknown 1.00 SET594+3 Theorem 1.00 SET595+3 Unknown 1.00 SET595+4 Unknown 1.00 SET596+3 Unknown 1.00 SET597+3 Unknown 1.00 SET598+3 Unknown 1.00 SET599+3 Unknown 1.00 SET600+3 Unknown 1.00 SET601+3 Unknown 1.00 SET602+3 Theorem 0.75 SET602+4 Theorem 0.75 SET603+3 Theorem 0.75 SET603+4 Theorem 0.75 SET604+3 Theorem 0.50 SET605+3 Theorem 0.50 SET606+3 Unknown 1.00 SET607+3 Unknown 1.00 SET608+3 Unknown 1.00 SET609+3 Unknown 1.00 SET610+3 Unknown 1.00 SET611+3 Unknown 1.00 SET612+3 Unknown 1.00 SET613+3 Unknown 1.00 SET614+3 Unknown 1.00 SET615+3 Unknown 1.00 SET616+3 Unknown 1.00 SET617+3 Unknown 1.00 SET618+3 Unknown 1.00 SET619+3 Unknown 1.00 SET620+3 Unknown 1.00 SET621+3 Unknown 1.00 SET622+3 Unknown 1.00 SET623+3 Unknown 1.00 SET624+3 Unknown 1.00 SET625+3 Theorem 0.75 SET626+3 Theorem 0.75 SET627+3 Theorem 0.00 SET628+3 Unknown 1.00 SET629+3 Theorem 0.75 SET630+3 Unknown 1.00 SET631+3 Theorem 0.50 SET632+3 Theorem 0.75 SET633+3 Unknown 1.00 SET634+3 Unknown 1.00 SET635+3 Unknown 1.00 SET636+3 Unknown 1.00 SET637+3 Unknown 1.00 SET638+3 Theorem 0.75 SET639+3 Unknown 1.00 SET640+3 Unknown 1.00 SET641+3 Unknown 1.00 SET642+3 Theorem 0.50 SET643+3 Theorem 0.75 SET644+3 Unknown 1.00 SET645+3 Unknown 1.00 SET646+3 Unknown 1.00 SET647+3 Unknown 1.00 SET648+3 Unknown 1.00 SET649+3 Unknown 1.00 SET650+3 Unknown 1.00 SET651+3 Unknown 1.00 SET652+3 Unknown 1.00 SET653+3 Theorem 1.00 SET654+3 Theorem 1.00 SET655+3 Unknown 1.00 SET656+3 Unknown 1.00 SET657+3 Unknown 1.00 SET658+3 Theorem 0.75 SET659+3 Unknown 1.00 SET660+3 Unknown 1.00 SET661+3 Unknown 1.00 SET662+3 Unknown 1.00 SET663+3 Unknown 1.00 SET664+3 Unknown 1.00 SET665+3 Unknown 1.00 SET666+3 Unknown 1.00 SET667+3 Unknown 1.00 SET668+3 Unknown 1.00 SET669+3 Unknown 1.00 SET670+3 Unknown 1.00 SET671+3 Unknown 1.00 SET672+3 Unknown 1.00 SET673+3 Unknown 1.00 SET674+3 Unknown 1.00 SET675+3 Unknown 1.00 SET676+3 Theorem 0.75 SET677+3 Theorem 0.75 SET678+3 Unknown 1.00 SET679+3 Unknown 1.00 SET680+3 Unknown 1.00 SET681+3 Unknown 1.00 SET682+3 Unknown 1.00 SET683+3 Unknown 1.00 SET684+3 Unknown 1.00 SET685+3 Unknown 1.00 SET686+3 Unknown 1.00 SET687+4 Theorem 0.50 SET688+4 Unknown 1.00 SET689+4 Unknown 1.00 SET690+4 Unknown 1.00 SET691+4 Unknown 1.00 SET692+4 Unknown 1.00 SET693+4 Unknown 1.00 SET694+4 Unknown 1.00 SET695+4 Unknown 1.00 SET696+4 Unknown 1.00 SET697+4 Unknown 1.00 SET698+4 Unknown 1.00 SET699+4 Unknown 1.00 SET700+4 Unknown 1.00 SET701+4 Unknown 1.00 SET702+4 Unknown 1.00 SET703+4 Unknown 1.00 SET704+4 Theorem 0.75 SET705+4 Theorem 0.75 SET706+4 Unknown 1.00 SET707+4 Unknown 1.00 SET708+4 Unknown 1.00 SET709+4 Unknown 1.00 SET710+4 Unknown 1.00 SET711+4 Unknown 1.00 SET712+4 Unknown 1.00 SET713+4 Unknown 1.00 SET714+4 Unknown 1.00 SET715+4 Unknown 1.00 SET716+4 Unknown 1.00 SET717+4 Unknown 1.00 SET718+4 Unknown 1.00 SET719+4 Unknown 1.00 SET720+4 Unknown 1.00 SET721+4 Unknown 1.00 SET722+4 Unknown 1.00 SET723+4 Unknown 1.00 SET724+4 Unknown 1.00 SET725+4 Unknown 1.00 SET726+4 Unknown 1.00 SET727+4 Unknown 1.00 SET728+4 Unknown 1.00 SET729+4 Unknown 1.00 SET730+4 Unknown 1.00 SET731+4 Unknown 1.00 SET732+4 Unknown 1.00 SET733+4 Unknown 1.00 SET734+4 Unknown 1.00 SET735+4 Unknown 1.00 SET736+4 Unknown 1.00 SET737+4 Unknown 1.00 SET738+4 Unknown 1.00 SET739+4 Unknown 1.00 SET740+4 Unknown 1.00 SET741+4 Unknown 1.00 SET742+4 Unknown 1.00 SET743+4 Unknown 1.00 SET744+4 Unknown 1.00 SET745+4 Unknown 1.00 SET746+4 Unknown 1.00 SET747+4 Unknown 1.00 SET748+4 Unknown 1.00 SET749+4 Unknown 1.00 SET750+4 Unknown 1.00 SET751+4 Unknown 1.00 SET752+4 Unknown 1.00 SET753+4 Unknown 1.00 SET754+4 Unknown 1.00 SET755+4 Unknown 1.00 SET756+4 Unknown 1.00 SET757+4 Unknown 1.00 SET758+4 Unknown 1.00 SET759+4 Unknown 1.00 SET760+4 Unknown 1.00 SET761+4 Unknown 1.00 SET762+4 Unknown 1.00 SET763+4 Unknown 1.00 SET764+4 Unknown 1.00 SET765+4 Unknown 1.00 SET766+4 Theorem 0.75 SET767+4 Theorem 0.75 SET768+4 Unknown 1.00 SET769+4 Unknown 1.00 SET770+4 Unknown 1.00 SET771+4 Unknown 1.00 SET772+4 Unknown 1.00 SET773+4 Unknown 1.00 SET774+4 Unknown 1.00 SET775+4 Unknown 1.00 SET776+4 Theorem 1.00 SET786+1 Theorem 0.00 SWC001+1 Unknown 1.00 SWC002+1 Unknown 1.00 SWC003+1 Unknown 1.00 SWC004+1 Unknown 1.00 SWC005+1 Unknown 1.00 SWC006+1 Unknown 1.00 SWC007+1 Unknown 1.00 SWC008+1 Unknown 1.00 SWC009+1 Unknown 1.00 SWC010+1 Unknown 1.00 SWC011+1 Unknown 1.00 SWC012+1 Unknown 1.00 SWC013+1 Unknown 1.00 SWC014+1 Unknown 1.00 SWC015+1 Unknown 1.00 SWC016+1 Unknown 1.00 SWC017+1 Unknown 1.00 SWC018+1 Unknown 1.00 SWC019+1 Unknown 1.00 SWC020+1 Unknown 1.00 SWC021+1 Unknown 1.00 SWC022+1 Unknown 1.00 SWC023+1 Unknown 1.00 SWC024+1 Unknown 1.00 SWC025+1 Unknown 1.00 SWC026+1 Unknown 1.00 SWC027+1 Unknown 1.00 SWC028+1 Unknown 1.00 SWC029+1 Unknown 1.00 SWC030+1 Unknown 1.00 SWC031+1 Unknown 1.00 SWC032+1 Unknown 1.00 SWC033+1 Unknown 1.00 SWC034+1 Unknown 1.00 SWC035+1 Unknown 1.00 SWC036+1 Unknown 1.00 SWC037+1 Unknown 1.00 SWC038+1 Unknown 1.00 SWC039+1 Unknown 1.00 SWC040+1 Unknown 1.00 SWC041+1 Unknown 1.00 SWC042+1 Unknown 1.00 SWC043+1 Unknown 1.00 SWC044+1 Unknown 1.00 SWC045+1 Unknown 1.00 SWC046+1 Unknown 1.00 SWC047+1 Unknown 1.00 SWC048+1 Unknown 1.00 SWC049+1 Unknown 1.00 SWC050+1 Unknown 1.00 SWC051+1 Unknown 1.00 SWC052+1 Unknown 1.00 SWC053+1 Unknown 1.00 SWC054+1 Unknown 1.00 SWC055+1 Unknown 1.00 SWC056+1 Unknown 1.00 SWC057+1 Unknown 1.00 SWC058+1 Unknown 1.00 SWC059+1 Unknown 1.00 SWC060+1 Unknown 1.00 SWC061+1 Unknown 1.00 SWC062+1 Unknown 1.00 SWC063+1 Unknown 1.00 SWC064+1 Unknown 1.00 SWC065+1 Unknown 1.00 SWC066+1 Unknown 1.00 SWC067+1 Unknown 1.00 SWC068+1 Unknown 1.00 SWC069+1 Unknown 1.00 SWC070+1 Unknown 1.00 SWC071+1 Unknown 1.00 SWC072+1 Unknown 1.00 SWC073+1 Unknown 1.00 SWC074+1 Unknown 1.00 SWC075+1 Unknown 1.00 SWC076+1 Unknown 1.00 SWC077+1 Unknown 1.00 SWC078+1 Unknown 1.00 SWC079+1 Unknown 1.00 SWC080+1 Unknown 1.00 SWC081+1 Unknown 1.00 SWC082+1 Unknown 1.00 SWC083+1 Unknown 1.00 SWC084+1 Unknown 1.00 SWC085+1 Unknown 1.00 SWC086+1 Unknown 1.00 SWC087+1 Unknown 1.00 SWC088+1 Unknown 1.00 SWC089+1 Unknown 1.00 SWC090+1 Unknown 1.00 SWC091+1 Unknown 1.00 SWC092+1 Unknown 1.00 SWC093+1 Unknown 1.00 SWC094+1 Unknown 1.00 SWC095+1 Unknown 1.00 SWC096+1 Unknown 1.00 SWC097+1 Unknown 1.00 SWC098+1 Unknown 1.00 SWC099+1 Unknown 1.00 SWC100+1 Unknown 1.00 SWC101+1 Unknown 1.00 SWC102+1 Unknown 1.00 SWC103+1 Unknown 1.00 SWC104+1 Unknown 1.00 SWC105+1 Unknown 1.00 SWC106+1 Unknown 1.00 SWC107+1 Unknown 1.00 SWC108+1 Unknown 1.00 SWC109+1 Unknown 1.00 SWC110+1 Unknown 1.00 SWC111+1 Unknown 1.00 SWC112+1 Unknown 1.00 SWC113+1 Unknown 1.00 SWC114+1 Unknown 1.00 SWC115+1 Unknown 1.00 SWC116+1 Unknown 1.00 SWC117+1 Unknown 1.00 SWC118+1 Unknown 1.00 SWC119+1 Unknown 1.00 SWC120+1 Unknown 1.00 SWC121+1 Unknown 1.00 SWC122+1 Unknown 1.00 SWC123+1 Unknown 1.00 SWC124+1 Unknown 1.00 SWC125+1 Unknown 1.00 SWC126+1 Unknown 1.00 SWC127+1 Unknown 1.00 SWC128+1 Unknown 1.00 SWC129+1 Unknown 1.00 SWC130+1 Unknown 1.00 SWC131+1 Unknown 1.00 SWC132+1 Unknown 1.00 SWC133+1 Unknown 1.00 SWC134+1 Unknown 1.00 SWC135+1 Unknown 1.00 SWC136+1 Unknown 1.00 SWC137+1 Unknown 1.00 SWC138+1 Unknown 1.00 SWC139+1 Unknown 1.00 SWC140+1 Unknown 1.00 SWC141+1 Unknown 1.00 SWC142+1 Unknown 1.00 SWC143+1 Unknown 1.00 SWC144+1 Unknown 1.00 SWC145+1 Unknown 1.00 SWC146+1 Unknown 1.00 SWC147+1 Unknown 1.00 SWC148+1 Unknown 1.00 SWC149+1 Unknown 1.00 SWC150+1 Unknown 1.00 SWC151+1 Unknown 1.00 SWC152+1 Unknown 1.00 SWC153+1 Unknown 1.00 SWC154+1 Unknown 1.00 SWC155+1 Unknown 1.00 SWC156+1 Unknown 1.00 SWC157+1 Unknown 1.00 SWC158+1 Unknown 1.00 SWC159+1 Unknown 1.00 SWC160+1 Unknown 1.00 SWC161+1 Unknown 1.00 SWC162+1 Unknown 1.00 SWC163+1 Unknown 1.00 SWC164+1 Unknown 1.00 SWC165+1 Unknown 1.00 SWC166+1 Unknown 1.00 SWC167+1 Unknown 1.00 SWC168+1 Unknown 1.00 SWC169+1 Unknown 1.00 SWC170+1 Unknown 1.00 SWC171+1 Unknown 1.00 SWC172+1 Unknown 1.00 SWC173+1 Unknown 1.00 SWC174+1 Unknown 1.00 SWC175+1 Unknown 1.00 SWC176+1 Unknown 1.00 SWC177+1 Unknown 1.00 SWC178+1 Unknown 1.00 SWC179+1 Unknown 1.00 SWC180+1 Unknown 1.00 SWC181+1 Unknown 1.00 SWC182+1 Unknown 1.00 SWC183+1 Unknown 1.00 SWC184+1 Unknown 1.00 SWC185+1 Unknown 1.00 SWC186+1 Unknown 1.00 SWC187+1 Unknown 1.00 SWC188+1 Unknown 1.00 SWC189+1 Unknown 1.00 SWC190+1 Unknown 1.00 SWC191+1 Unknown 1.00 SWC192+1 Unknown 1.00 SWC193+1 Unknown 1.00 SWC194+1 Unknown 1.00 SWC195+1 Unknown 1.00 SWC196+1 Unknown 1.00 SWC197+1 Unknown 1.00 SWC198+1 Unknown 1.00 SWC199+1 Unknown 1.00 SWC200+1 Unknown 1.00 SWC201+1 Unknown 1.00 SWC202+1 Unknown 1.00 SWC203+1 Unknown 1.00 SWC204+1 Unknown 1.00 SWC205+1 Unknown 1.00 SWC206+1 Unknown 1.00 SWC207+1 Unknown 1.00 SWC208+1 Unknown 1.00 SWC209+1 Unknown 1.00 SWC210+1 Unknown 1.00 SWC211+1 Unknown 1.00 SWC212+1 Unknown 1.00 SWC213+1 Unknown 1.00 SWC214+1 Unknown 1.00 SWC215+1 Unknown 1.00 SWC216+1 Unknown 1.00 SWC217+1 Unknown 1.00 SWC218+1 Unknown 1.00 SWC219+1 Unknown 1.00 SWC220+1 Unknown 1.00 SWC221+1 Unknown 1.00 SWC222+1 Unknown 1.00 SWC223+1 Unknown 1.00 SWC224+1 Unknown 1.00 SWC225+1 Unknown 1.00 SWC226+1 Unknown 1.00 SWC227+1 Unknown 1.00 SWC228+1 Unknown 1.00 SWC229+1 Unknown 1.00 SWC230+1 Unknown 1.00 SWC231+1 Unknown 1.00 SWC232+1 Unknown 1.00 SWC233+1 Unknown 1.00 SWC234+1 Unknown 1.00 SWC235+1 Unknown 1.00 SWC236+1 Unknown 1.00 SWC237+1 Unknown 1.00 SWC238+1 Unknown 1.00 SWC239+1 Unknown 1.00 SWC240+1 Unknown 1.00 SWC241+1 Unknown 1.00 SWC242+1 Unknown 1.00 SWC243+1 Unknown 1.00 SWC244+1 Unknown 1.00 SWC245+1 Unknown 1.00 SWC246+1 Unknown 1.00 SWC247+1 Unknown 1.00 SWC248+1 Unknown 1.00 SWC249+1 Unknown 1.00 SWC250+1 Unknown 1.00 SWC251+1 Unknown 1.00 SWC252+1 Unknown 1.00 SWC253+1 Unknown 1.00 SWC254+1 Unknown 1.00 SWC255+1 Unknown 1.00 SWC256+1 Unknown 1.00 SWC257+1 Unknown 1.00 SWC258+1 Unknown 1.00 SWC259+1 Unknown 1.00 SWC260+1 Unknown 1.00 SWC261+1 Unknown 1.00 SWC262+1 Unknown 1.00 SWC263+1 Unknown 1.00 SWC264+1 Unknown 1.00 SWC265+1 Unknown 1.00 SWC266+1 Unknown 1.00 SWC267+1 Unknown 1.00 SWC268+1 Unknown 1.00 SWC269+1 Unknown 1.00 SWC270+1 Unknown 1.00 SWC271+1 Unknown 1.00 SWC272+1 Unknown 1.00 SWC273+1 Unknown 1.00 SWC274+1 Unknown 1.00 SWC275+1 Unknown 1.00 SWC276+1 Unknown 1.00 SWC277+1 Unknown 1.00 SWC278+1 Unknown 1.00 SWC279+1 Unknown 1.00 SWC280+1 Unknown 1.00 SWC281+1 Unknown 1.00 SWC282+1 Unknown 1.00 SWC283+1 Unknown 1.00 SWC284+1 Unknown 1.00 SWC285+1 Unknown 1.00 SWC286+1 Unknown 1.00 SWC287+1 Unknown 1.00 SWC288+1 Unknown 1.00 SWC289+1 Unknown 1.00 SWC290+1 Unknown 1.00 SWC291+1 Unknown 1.00 SWC292+1 Unknown 1.00 SWC293+1 Unknown 1.00 SWC294+1 Unknown 1.00 SWC295+1 Unknown 1.00 SWC296+1 Unknown 1.00 SWC297+1 Unknown 1.00 SWC298+1 Unknown 1.00 SWC299+1 Unknown 1.00 SWC300+1 Unknown 1.00 SWC301+1 Unknown 1.00 SWC302+1 Unknown 1.00 SWC303+1 Unknown 1.00 SWC304+1 Unknown 1.00 SWC305+1 Unknown 1.00 SWC306+1 Unknown 1.00 SWC307+1 Unknown 1.00 SWC308+1 Unknown 1.00 SWC309+1 Unknown 1.00 SWC310+1 Unknown 1.00 SWC311+1 Unknown 1.00 SWC312+1 Unknown 1.00 SWC313+1 Unknown 1.00 SWC314+1 Unknown 1.00 SWC315+1 Unknown 1.00 SWC316+1 Unknown 1.00 SWC317+1 Unknown 1.00 SWC318+1 Unknown 1.00 SWC319+1 Unknown 1.00 SWC320+1 Unknown 1.00 SWC321+1 Unknown 1.00 SWC322+1 Unknown 1.00 SWC323+1 Unknown 1.00 SWC324+1 Unknown 1.00 SWC325+1 Unknown 1.00 SWC326+1 Unknown 1.00 SWC327+1 Unknown 1.00 SWC328+1 Unknown 1.00 SWC329+1 Unknown 1.00 SWC330+1 Unknown 1.00 SWC331+1 Unknown 1.00 SWC332+1 Unknown 1.00 SWC333+1 Unknown 1.00 SWC334+1 Unknown 1.00 SWC335+1 Unknown 1.00 SWC336+1 Unknown 1.00 SWC337+1 Unknown 1.00 SWC338+1 Unknown 1.00 SWC339+1 Unknown 1.00 SWC340+1 Unknown 1.00 SWC341+1 Unknown 1.00 SWC342+1 Unknown 1.00 SWC343+1 Unknown 1.00 SWC344+1 Unknown 1.00 SWC345+1 Unknown 1.00 SWC346+1 Unknown 1.00 SWC347+1 Unknown 1.00 SWC348+1 Unknown 1.00 SWC349+1 Unknown 1.00 SWC350+1 Unknown 1.00 SWC351+1 Unknown 1.00 SWC352+1 Unknown 1.00 SWC353+1 Unknown 1.00 SWC354+1 Unknown 1.00 SWC355+1 Unknown 1.00 SWC356+1 Unknown 1.00 SWC357+1 Unknown 1.00 SWC358+1 Unknown 1.00 SWC359+1 Unknown 1.00 SWC360+1 Unknown 1.00 SWC361+1 Unknown 1.00 SWC362+1 Unknown 1.00 SWC363+1 Unknown 1.00 SWC364+1 Unknown 1.00 SWC365+1 Unknown 1.00 SWC366+1 Unknown 1.00 SWC367+1 Unknown 1.00 SWC368+1 Unknown 1.00 SWC369+1 Unknown 1.00 SWC370+1 Unknown 1.00 SWC371+1 Unknown 1.00 SWC372+1 Unknown 1.00 SWC373+1 Unknown 1.00 SWC374+1 Unknown 1.00 SWC375+1 Unknown 1.00 SWC376+1 Unknown 1.00 SWC377+1 Unknown 1.00 SWC378+1 Unknown 1.00 SWC379+1 Unknown 1.00 SWC380+1 Unknown 1.00 SWC381+1 Unknown 1.00 SWC382+1 Unknown 1.00 SWC383+1 Unknown 1.00 SWC384+1 Unknown 1.00 SWC385+1 Unknown 1.00 SWC386+1 Unknown 1.00 SWC387+1 Unknown 1.00 SWC388+1 Unknown 1.00 SWC389+1 Unknown 1.00 SWC390+1 Unknown 1.00 SWC391+1 Unknown 1.00 SWC392+1 Unknown 1.00 SWC393+1 Unknown 1.00 SWC394+1 Unknown 1.00 SWC395+1 Unknown 1.00 SWC396+1 Unknown 1.00 SWC397+1 Unknown 1.00 SWC398+1 Unknown 1.00 SWC399+1 Unknown 1.00 SWC400+1 Unknown 1.00 SWC401+1 Unknown 1.00 SWC402+1 Unknown 1.00 SWC403+1 Unknown 1.00 SWC404+1 Unknown 1.00 SWC405+1 Unknown 1.00 SWC406+1 Unknown 1.00 SWC407+1 Unknown 1.00 SWC408+1 Unknown 1.00 SWC409+1 Unknown 1.00 SWC410+1 Unknown 1.00 SWC411+1 Unknown 1.00 SWC412+1 Unknown 1.00 SWC413+1 Unknown 1.00 SWC414+1 Unknown 1.00 SWC415+1 Unknown 1.00 SWC416+1 Unknown 1.00 SWC417+1 Unknown 1.00 SWC418+1 Unknown 1.00 SWC419+1 Unknown 1.00 SWC420+1 Unknown 1.00 SWC421+1 Unknown 1.00 SWC422+1 Unknown 1.00 SWV011+1 Theorem 0.00 SWV014+1 Unknown 1.00 SYN001+1 Non-Theorem 0.40 SYN007+1.014 Non-Theorem 0.80 SYN036+1 Theorem 0.75 SYN036+2 Unknown 1.00 SYN040+1 Non-Theorem 0.60 SYN041+1 Theorem 0.00 SYN044+1 Theorem 0.20 SYN045+1 Theorem 0.20 SYN046+1 Non-Theorem 0.60 SYN047+1 Non-Theorem 0.60 SYN048+1 Non-Theorem 0.75 SYN049+1 Non-Theorem 0.75 SYN050+1 Theorem 0.00 SYN051+1 Unknown 1.00 SYN052+1 Theorem 0.25 SYN053+1 Unknown 1.00 SYN054+1 Unknown 1.00 SYN055+1 Theorem 0.00 SYN056+1 Theorem 0.50 SYN057+1 Theorem 0.25 SYN058+1 Theorem 0.00 SYN059+1 Theorem 0.25 SYN060+1 Unknown 1.00 SYN061+1 Theorem 0.00 SYN062+1 Theorem 0.00 SYN063+1 Unknown 1.00 SYN064+1 Non-Theorem 0.75 SYN065+1 Theorem 0.00 SYN066+1 Unknown 1.00 SYN067+1 Unknown 1.00 SYN068+1 Theorem 0.00 SYN069+1 Theorem 0.00 SYN070+1 Unknown 1.00 SYN071+1 Theorem 0.75 SYN072+1 Unknown 1.00 SYN073+1 Non-Theorem 0.75 SYN074+1 Unknown 1.00 SYN075+1 Unknown 1.00 SYN076+1 Unknown 1.00 SYN077+1 Unknown 1.00 SYN078+1 Theorem 0.50 SYN079+1 Theorem 0.00 SYN080+1 Theorem 0.25 SYN081+1 Unknown 1.00 SYN082+1 Theorem 0.00 SYN083+1 Theorem 0.75 SYN084+1 Unknown 1.00 SYN315+1 Unknown 1.00 SYN317+1 Unknown 1.00 SYN318+1 Non-Theorem 0.75 SYN319+1 Non-Theorem 0.75 SYN321+1 Theorem 0.00 SYN323+1 Theorem 0.00 SYN325+1 Non-Theorem 0.75 SYN326+1 Non-Theorem 0.75 SYN327+1 Non-Theorem 0.75 SYN328+1 Non-Theorem 0.75 SYN331+1 Non-Theorem 0.75 SYN332+1 Unknown 1.00 SYN333+1 Non-Theorem 0.75 SYN334+1 Unknown 1.00 SYN336+1 Non-Theorem 0.75 SYN338+1 Non-Theorem 0.75 SYN339+1 Non-Theorem 0.75 SYN340+1 Non-Theorem 0.75 SYN341+1 Non-Theorem 0.75 SYN343+1 Non-Theorem 0.75 SYN345+1 Non-Theorem 0.75 SYN346+1 Theorem 0.00 SYN347+1 Unknown 1.00 SYN349+1 Unknown 1.00 SYN350+1 Non-Theorem 0.75 SYN351+1 Non-Theorem 0.75 SYN352+1 Non-Theorem 0.75 SYN353+1 Non-Theorem 0.75 SYN354+1 Unknown 1.00 SYN355+1 Non-Theorem 0.75 SYN356+1 Theorem 0.25 SYN357+1 Theorem 0.00 SYN358+1 Theorem 0.00 SYN359+1 Theorem 0.00 SYN360+1 Theorem 0.00 SYN361+1 Theorem 0.00 SYN362+1 Theorem 0.00 SYN363+1 Theorem 0.00 SYN364+1 Theorem 0.25 SYN365+1 Theorem 0.50 SYN366+1 Theorem 0.00 SYN367+1 Theorem 0.00 SYN368+1 Non-Theorem 0.75 SYN369+1 Non-Theorem 0.75 SYN370+1 Non-Theorem 0.75 SYN371+1 Theorem 0.00 SYN372+1 Non-Theorem 0.75 SYN373+1 Unknown 1.00 SYN374+1 Theorem 0.50 SYN375+1 Theorem 0.25 SYN376+1 Unknown 1.00 SYN377+1 Theorem 0.25 SYN378+1 Non-Theorem 0.75 SYN379+1 Theorem 0.00 SYN380+1 Non-Theorem 0.75 SYN381+1 Theorem 0.00 SYN382+1 Theorem 0.00 SYN383+1 Non-Theorem 0.75 SYN384+1 Non-Theorem 0.75 SYN385+1 Non-Theorem 0.75 SYN386+1 Theorem 0.00 SYN387+1 Non-Theorem 0.00 SYN388+1 Non-Theorem 0.40 SYN389+1 Non-Theorem 0.40 SYN390+1 Theorem 0.00 SYN391+1 Theorem 0.00 SYN392+1 Non-Theorem 0.60 SYN393+1 Non-Theorem 0.60 SYN394+1 Theorem 0.00 SYN395+1 Theorem 0.00 SYN396+1 Non-Theorem 0.75 SYN397+1 Theorem 0.00 SYN398+1 Theorem 0.00 SYN399+1 Theorem 0.00 SYN400+1 Theorem 0.00 SYN401+1 Theorem 0.00 SYN402+1 Theorem 0.00 SYN403+1 Theorem 0.00 SYN404+1 Theorem 0.00 SYN405+1 Theorem 0.00 SYN406+1 Theorem 0.00 SYN407+1 Non-Theorem 0.75 SYN408+1 Theorem 0.00 SYN409+1 Theorem 0.00 SYN410+1 Theorem 0.00 SYN411+1 Non-Theorem 0.75 SYN412+1 Theorem 0.00 SYN413+1 Theorem 0.00 SYN415+1 Theorem 0.75 SYN416+1 Non-Theorem 0.00 SYN417+1 Unknown 1.00 SYN436+1 Unknown 1.00 SYN439+1 Unknown 1.00 SYN440+1 Unknown 1.00 SYN442+1 Unknown 1.00 SYN443+1 Unknown 1.00 SYN444+1 Unknown 1.00 SYN445+1 Unknown 1.00 SYN447+1 Unknown 1.00 SYN448+1 Unknown 1.00 SYN450+1 Unknown 1.00 SYN451+1 Unknown 1.00 SYN452+1 Unknown 1.00 SYN454+1 Unknown 1.00 SYN455+1 Unknown 1.00 SYN457+1 Unknown 1.00 SYN458+1 Unknown 1.00 SYN459+1 Unknown 1.00 SYN460+1 Unknown 1.00 SYN461+1 Unknown 1.00 SYN462+1 Unknown 1.00 SYN465+1 Unknown 1.00 SYN466+1 Unknown 1.00 SYN467+1 Unknown 1.00 SYN468+1 Unknown 1.00 SYN469+1 Unknown 1.00 SYN470+1 Unknown 1.00 SYN471+1 Unknown 1.00 SYN472+1 Unknown 1.00 SYN473+1 Unknown 1.00 SYN474+1 Unknown 1.00 SYN475+1 Unknown 1.00 SYN476+1 Unknown 1.00 SYN477+1 Unknown 1.00 SYN478+1 Unknown 1.00 SYN479+1 Unknown 1.00 SYN480+1 Unknown 1.00 SYN481+1 Unknown 1.00 SYN482+1 Unknown 1.00 SYN483+1 Unknown 1.00 SYN484+1 Unknown 1.00 SYN485+1 Unknown 1.00 SYN486+1 Unknown 1.00 SYN487+1 Unknown 1.00 SYN488+1 Unknown 1.00 SYN489+1 Unknown 1.00 SYN498+1 Unknown 1.00 SYN499+1 Unknown 1.00 SYN500+1 Unknown 1.00 SYN501+1 Unknown 1.00 SYN502+1 Unknown 1.00 SYN503+1 Unknown 1.00 SYN504+1 Unknown 1.00 SYN505+1 Unknown 1.00 SYN506+1 Unknown 1.00 SYN507+1 Unknown 1.00 SYN508+1 Unknown 1.00 SYN509+1 Unknown 1.00 SYN510+1 Unknown 1.00 SYN511+1 Unknown 1.00 SYN512+1 Unknown 1.00 SYN548+1 Unknown 1.00 SYN549+1 Theorem 0.75 SYN550+1 Theorem 0.75 SYN551+1 Unknown 1.00 SYN551+2 Unknown 1.00 SYN551+3 Unknown 1.00 SYN721+1 Theorem 0.00 SYN722+1 Theorem 0.50 SYN723+1 Unknown 1.00 SYN724+1 Theorem 0.25 SYN726+1 Unknown 1.00 SYN727+1 Theorem 0.00 SYN728+1 Theorem 0.25 SYN729+1 Theorem 0.50 SYN730+1 Non-Theorem 0.75 SYN731+1 Non-Theorem 0.75 SYN732+1 Non-Theorem 0.75 SYN733+1 Theorem 0.00