overall ------- 1445 formulas (1379 first-order, 66 propos.; 1445 class. valid) provers first order propositional JProver ft ileanSeP ileanTAP ileanCoP ileanCoP_pt LJT STRIP Prolog C solved 162 199 226 156 184 318 323 55 60 (%) (*) 11.2 13.8 15.6 10.8 12.7 22.0 22.4 83.3 90.9 proved 160 173 198 153 181 265 270 31 34 TPTP-set 94 99 112 87 113 188 193 5 5 ILTP-set 66 74 86 66 68 77 77 26 29 refuted 2 26 28 3 3 53 53 24 26 time out (>300s) 1267 1192 673 1212 1201 1064 1050 7 4 average time (**) 0.70 0.03 <0.01 1.96 0.01 1.50 0.44 <0.01 0.05 errors (***) 16 54 546 77 60 63 72 4 2 (**) of all 1445 formulas, if it is a first-order prover of the 66 propositional formulas, if it is a propositional prover (**) computed only for formulas that were proved by all first-order provers, if it is a first-order prover (7.4% of all formulas) pure-propos. provers, if it is a pure-propos. prover (47.0% of all propos. formulas) (***) "stack overflow", except for JProver: "Invalid_argument Jprover bug (Jtunify module)" (16) ft (C) : "segmentation violation" (104), "Memory allocation error" (3), "stack overflow" (439) 1. TPTP v 2.7.0 --------------- 1337 formulas (1319 first-order, 18 propos.) provers first order propositional JProver ft ileanSeP ileanTAP ileanCoP ileanCoP_pt LJT STRIP Prolog C solved 96 112 125 90 116 234 239 17 17 proved 94 99 112 87 113 188 193 5 5 0 - 1 s 78 93 109 73 107 146 155 5 5 1 - 10 s 9 5 1 8 2 16 12 0 0 10 - 100 s 7 1 2 4 2 17 9 0 0 100 - 200 s 0 0 0 2 0 1 12 0 0 200 - 300 s 0 0 0 0 2 8 5 0 0 pure equality 2 2 2 1 6 6 7 0 0 refuted 2 13 13 3 3 46 46 12 12 time out (>300s) 1237 1171 667 1173 1165 1041 1031 0 1 errors 4 54 545 74 56 62 67 1 0 #proved formulas sorted by domains: prover total AGT ALG COM GEO GRP HAL LCL MGT NLP PUZ SET SWC SWV SYN ---------------------------------------------------------------------------- JProver 94 0 1 0 0 0 0 1 9 7 0 14 0 1 61 ft Prolog 99 2 0 1 0 0 0 0 7 7 0 15 0 1 66 C 112 2 0 2 0 0 0 1 7 7 0 21 0 1 71 ileanSeP 87 5 0 0 1 0 0 0 0 3 0 19 0 1 58 ileanTAP 113 0 6 0 1 0 0 1 6 11 0 26 0 1 61 ileanCoP 188 14 5 1 6 0 0 1 21 3 2 72 0 1 62 ileanCoP_pt 193 14 6 1 7 0 0 1 24 3 2 73 0 1 61 LJT 5 0 0 0 0 0 0 0 0 0 0 0 0 0 5 STRIP 5 0 0 0 0 0 0 0 0 0 0 0 0 0 5 2. ILTP-Benchmark ----------------- 108 formulae (60 first-order, 48 propos.; 90 intuit. valid, 18 intuit. invalid) provers first order propositional JProver ft ileanSeP ileanTAP ileanCoP ileanCoP_pt LJT STRIP Prolog C solved 66 87 101 66 68 84 84 38 43 proved 66 74 86 66 68 77 77 26 29 refuted 0 13 15 0 0 7 7 12 14 time out (>300s) 30 21 6 39 36 23 19 7 3 average time (*) 0.40 0.06 0.00 0.37 0.02 0.03 0.01 <0.01 0.05 errors 12 0 1 3 4 1 5 3 2 Times ----- abbreviations: stack - stack overflow segmf - segmentation fault mem - memory allocation error jtbug - Invalid_argument Jprover bug (Jtunify module) (123.45) - refuted in 123.45 sec. 1. TPTP-set ----------- formula provers first order propositional JProver ft ileanSeP ileanTAP ileanCoP ileanCoP_pt LJT STRIP Prolog C AGT001+1 >300 <0.01 <0.01 0.33 stack 0.01 0.02 AGT001+2 >300 <0.01 <0.01 2.13 stack 0.02 0.02 AGT002+1 >300 >300 >300 0.63 stack 0.09 0.05 AGT002+2 >300 >300 >300 3.23 stack 0.13 0.1 AGT003+1 >300 >300 >300 >300 stack 0.24 0.09 AGT003+2 >300 >300 >300 >300 stack 0.2 0.03 AGT004+1 >300 >300 >300 >300 stack 0.11 0.02 AGT004+2 >300 >300 >300 >300 stack 0.19 0.02 AGT005+1 >300 >300 >300 >300 stack 7.72 1.57 AGT005+2 >300 >300 >300 >300 stack 0.2 0.03 AGT006+1 >300 >300 >300 >300 stack >300 >300 AGT006+2 >300 >300 >300 >300 stack >300 >300 AGT007+1 >300 >300 >300 >300 stack >300 >300 AGT007+2 >300 >300 >300 >300 stack >300 >300 AGT008+1 >300 >300 >300 >300 stack >300 >300 AGT008+2 >300 >300 >300 >300 stack >300 >300 AGT009+1 >300 >300 >300 >300 stack >300 >300 AGT009+2 >300 >300 >300 >300 stack >300 >300 AGT010+1 >300 >300 >300 >300 stack >300 >300 AGT010+2 >300 >300 >300 >300 stack >300 >300 AGT011+1 >300 >300 >300 >300 stack >300 >300 AGT011+2 >300 >300 >300 >300 stack >300 >300 AGT012+1 >300 >300 >300 >300 stack >300 >300 AGT012+2 >300 >300 >300 >300 stack >300 >300 AGT013+1 >300 >300 >300 >300 stack >300 >300 AGT013+2 >300 >300 >300 >300 stack >300 >300 AGT014+1 >300 >300 >300 >300 stack >300 >300 AGT014+2 >300 >300 >300 >300 stack >300 >300 AGT015+1 >300 >300 stack >300 >300 0.09 0.03 AGT015+2 >300 >300 >300 >300 >300 0.2 0.02 AGT016+1 >300 >300 >300 >300 stack >300 >300 AGT016+2 >300 >300 >300 >300 stack >300 >300 AGT017+1 >300 >300 stack >300 >300 0.1 0.02 AGT017+2 >300 >300 >300 108.72 >300 0.16 0.03 AGT018+1 >300 >300 >300 >300 stack >300 >300 AGT018+2 >300 >300 >300 >300 stack >300 >300 AGT019+1 >300 >300 >300 >300 stack >300 >300 AGT019+2 >300 >300 >300 >300 stack >300 >300 AGT020+1 >300 >300 >300 >300 stack >300 >300 AGT020+2 >300 >300 >300 >300 stack >300 >300 AGT021+1 >300 >300 >300 >300 stack >300 >300 AGT021+2 >300 >300 >300 >300 stack >300 >300 AGT022+1 >300 >300 >300 >300 stack >300 >300 AGT022+2 >300 >300 >300 >300 stack >300 >300 AGT023+1 >300 >300 >300 >300 stack >300 >300 AGT023+2 >300 >300 >300 >300 stack >300 >300 AGT024+1 >300 >300 >300 >300 stack >300 >300 AGT024+2 >300 >300 >300 >300 stack >300 >300 AGT025+1 >300 >300 >300 >300 stack >300 >300 AGT025+2 >300 >300 >300 >300 stack >300 >300 AGT026+1 >300 >300 >300 >300 stack >300 >300 AGT026+2 >300 >300 >300 >300 stack >300 >300 ALG014+1 >300 >300 stack stack >300 >300 >300 ALG015+1 >300 >300 >300 >300 >300 >300 >300 ALG016+1 >300 stack stack stack >300 >300 >300 ALG017+1 5.33 stack stack stack 0.01 >300 >300 ALG018+1 >300 >300 segmf >300 >300 >300 >300 ALG019+1 >300 >300 segmf >300 >300 >300 >300 ALG020+1 >300 >300 >300 >300 >300 >300 >300 ALG021+1 >300 >300 >300 >300 >300 stack stack ALG022+1 >300 >300 >300 >300 >300 stack stack ALG025+1 >300 >300 >300 >300 >300 >300 >300 ALG026+1 >300 >300 >300 >300 >300 stack stack ALG027+1 >300 >300 stack >300 >300 stack stack ALG028+1 >300 stack stack stack 0.01 0.01 0.05 ALG029+1 >300 >300 segmf >300 >300 >300 >300 ALG030+1 >300 >300 segmf >300 >300 >300 >300 ALG031+1 >300 >300 >300 >300 >300 >300 >300 ALG032+1 >300 >300 >300 >300 >300 stack stack ALG033+1 >300 >300 >300 >300 >300 stack stack ALG034+1 >300 >300 >300 (0.01) (0.06) stack stack ALG036+1 >300 stack stack stack >300 >300 >300 ALG037+1 >300 >300 >300 >300 >300 >300 >300 ALG038+1 >300 stack stack stack >300 >300 >300 ALG039+1 >300 stack stack stack 0.01 >300 273.13 ALG040+1 >300 >300 segmf >300 >300 >300 >300 ALG041+1 >300 >300 segmf >300 >300 >300 >300 ALG042+1 >300 >300 >300 >300 >300 >300 >300 ALG043+1 >300 >300 >300 >300 >300 stack stack ALG044+1 >300 >300 >300 >300 >300 stack stack ALG047+1 >300 stack stack stack stack stack stack ALG048+1 >300 >300 >300 >300 >300 >300 stack ALG049+1 >300 stack stack >300 >300 stack stack ALG050+1 >300 stack stack >300 >300 >300 stack ALG051+1 >300 stack stack >300 >300 stack stack ALG052+1 >300 >300 stack >300 >300 stack stack ALG053+1 >300 >300 stack >300 >300 stack stack ALG054+1 >300 stack stack >300 stack >300 >300 ALG055+1 >300 stack stack >300 stack stack stack ALG056+1 >300 >300 stack >300 >300 stack stack ALG057+1 >300 >300 stack >300 >300 stack stack ALG058+1 >300 stack stack >300 >300 stack stack ALG059+1 >300 stack stack >300 >300 stack stack ALG060+1 >300 >300 stack >300 >300 stack stack ALG061+1 >300 >300 stack >300 >300 >300 >300 ALG062+1 >300 stack stack >300 stack stack stack ALG063+1 >300 >300 >300 >300 >300 stack stack ALG064+1 >300 >300 >300 >300 >300 stack stack ALG065+1 >300 stack stack >300 >300 >300 >300 ALG066+1 >300 stack stack >300 stack stack stack ALG067+1 >300 stack stack >300 stack stack stack ALG068+1 >300 stack stack >300 >300 stack stack ALG069+1 >300 >300 segmf >300 >300 >300 >300 ALG070+1 >300 >300 segmf >300 >300 >300 >300 ALG071+1 >300 >300 segmf >300 >300 >300 >300 ALG072+1 >300 >300 segmf >300 >300 >300 >300 ALG073+1 >300 >300 segmf >300 >300 >300 >300 ALG074+1 >300 >300 segmf >300 >300 >300 >300 ALG075+1 >300 >300 >300 >300 >300 >300 >300 ALG076+1 >300 >300 >300 >300 >300 >300 >300 ALG077+1 >300 >300 >300 >300 >300 >300 >300 ALG078+1 >300 >300 >300 >300 >300 >300 >300 ALG079+1 >300 >300 >300 >300 >300 >300 >300 ALG080+1 >300 >300 >300 >300 >300 >300 >300 ALG081+1 >300 >300 >300 >300 >300 >300 >300 ALG082+1 >300 >300 >300 >300 >300 >300 >300 ALG083+1 >300 >300 >300 >300 >300 >300 >300 ALG084+1 >300 >300 >300 >300 >300 >300 >300 ALG085+1 >300 >300 >300 >300 >300 >300 >300 ALG086+1 >300 >300 >300 >300 >300 >300 >300 ALG087+1 >300 >300 >300 >300 >300 >300 >300 ALG088+1 >300 >300 >300 >300 >300 >300 >300 ALG089+1 >300 >300 >300 >300 >300 >300 >300 ALG090+1 >300 >300 >300 >300 >300 stack stack ALG091+1 >300 >300 >300 >300 >300 stack stack ALG092+1 >300 >300 >300 >300 >300 stack stack ALG093+1 >300 >300 >300 >300 stack stack stack ALG094+1 >300 >300 >300 >300 >300 stack stack ALG102+1 >300 stack stack >300 >300 stack stack ALG103+1 >300 stack stack >300 >300 stack stack ALG104+1 >300 stack stack >300 >300 stack stack ALG105+1 >300 >300 >300 >300 >300 >300 >300 ALG106+1 >300 stack stack >300 >300 stack stack ALG107+1 >300 >300 >300 >300 >300 >300 >300 ALG108+1 >300 stack stack >300 >300 stack stack ALG109+1 >300 stack stack >300 >300 stack stack ALG110+1 >300 stack stack >300 >300 >300 >300 ALG111+1 >300 stack stack >300 >300 >300 >300 ALG112+1 >300 >300 >300 >300 >300 >300 >300 ALG113+1 >300 >300 >300 >300 >300 >300 >300 ALG114+1 >300 stack stack >300 >300 >300 >300 ALG115+1 >300 >300 >300 >300 >300 stack stack ALG116+1 >300 >300 >300 >300 >300 >300 >300 ALG117+1 >300 stack stack >300 >300 >300 >300 ALG118+1 >300 >300 >300 >300 >300 stack stack ALG119+1 >300 stack stack >300 >300 stack stack ALG120+1 >300 stack stack >300 >300 stack stack ALG121+1 >300 stack stack >300 >300 stack stack ALG122+1 >300 stack stack >300 >300 stack stack ALG123+1 >300 stack stack >300 >300 stack stack ALG124+1 >300 stack stack >300 >300 >300 stack ALG125+1 >300 stack stack >300 >300 >300 >300 ALG126+1 >300 stack stack >300 >300 stack stack ALG127+1 >300 stack stack >300 >300 stack stack ALG128+1 >300 stack stack >300 >300 stack stack ALG129+1 >300 stack stack >300 >300 stack stack ALG165+1 >300 >300 >300 >300 >300 >300 >300 ALG166+1 >300 stack stack >300 >300 >300 stack ALG167+1 >300 stack stack >300 >300 >300 stack ALG168+1 >300 >300 >300 >300 >300 stack stack ALG169+1 >300 >300 >300 >300 >300 stack stack ALG170+1 >300 stack stack stack >300 >300 >300 ALG171+1 >300 stack stack stack >300 >300 >300 ALG172+1 >300 stack stack stack >300 >300 >300 ALG173+1 >300 stack stack stack >300 >300 >300 ALG174+1 >300 stack stack stack >300 >300 >300 ALG175+1 >300 >300 >300 >300 >300 >300 >300 ALG176+1 >300 >300 segmf >300 >300 >300 >300 ALG177+1 >300 >300 segmf >300 >300 >300 >300 ALG178+1 >300 >300 segmf >300 >300 >300 >300 ALG179+1 >300 >300 segmf >300 >300 >300 >300 ALG180+1 >300 >300 >300 >300 >300 >300 >300 ALG181+1 >300 >300 >300 >300 >300 >300 >300 ALG182+1 >300 >300 >300 >300 >300 >300 >300 ALG183+1 >300 >300 >300 >300 >300 >300 >300 ALG184+1 >300 >300 >300 >300 >300 >300 >300 ALG185+1 >300 >300 >300 >300 >300 >300 >300 ALG186+1 >300 >300 >300 >300 >300 stack stack ALG187+1 >300 >300 >300 >300 >300 stack stack ALG188+1 >300 >300 >300 >300 >300 stack stack ALG189+1 >300 >300 >300 >300 >300 stack stack ALG194+1 >300 >300 >300 >300 >300 >300 >300 ALG195+1 >300 stack stack >300 >300 stack stack ALG196+1 >300 >300 segmf >300 >300 stack stack ALG197+1 >300 >300 stack >300 >300 stack stack ALG198+1 >300 stack stack stack 0.01 0.04 0.09 ALG199+1 >300 stack stack >300 0.01 17.6 8.98 ALG200+1 >300 stack stack >300 0.01 0.03 0.08 ALG201+1 >300 >300 segmf >300 >300 0.69 0.45 ALG202+1 >300 >300 segmf >300 >300 >300 >300 ALG203+1 >300 >300 segmf >300 >300 >300 >300 ALG204+1 >300 >300 >300 >300 >300 >300 >300 ALG205+1 >300 >300 >300 >300 >300 >300 >300 ALG206+1 >300 >300 >300 >300 >300 >300 >300 ALG207+1 >300 >300 >300 >300 >300 stack stack ALG208+1 >300 >300 >300 >300 >300 stack stack ALG209+1 >300 >300 >300 >300 >300 stack stack COM003+1 >300 >300 0.49 >300 >300 >300 >300 COM003+2 >300 >300 >300 >300 >300 25.68 8.53 COM003+3 >300 2.76 0.02 >300 >300 >300 >300 GEO080+1 >300 >300 stack 0.88 0.01 0.05 0.02 GEO081+1 >300 >300 stack >300 >300 >300 180.99 GEO082+1 >300 >300 stack >300 >300 >300 >300 GEO083+1 >300 >300 stack >300 >300 >300 >300 GEO084+1 >300 >300 stack >300 >300 >300 >300 GEO085+1 >300 >300 segmf >300 >300 >300 >300 GEO086+1 >300 >300 stack >300 >300 >300 >300 GEO087+1 >300 >300 stack >300 >300 >300 >300 GEO088+1 >300 >300 stack >300 >300 >300 >300 GEO089+1 >300 >300 stack >300 >300 >300 >300 GEO090+1 >300 >300 stack >300 >300 >300 >300 GEO091+1 >300 >300 stack >300 >300 >300 >300 GEO092+1 >300 >300 stack >300 >300 >300 >300 GEO093+1 >300 >300 stack >300 >300 >300 >300 GEO094+1 >300 >300 stack >300 >300 >300 >300 GEO095+1 >300 >300 segmf >300 >300 >300 >300 GEO096+1 >300 >300 stack >300 >300 >300 >300 GEO097+1 >300 >300 stack >300 >300 >300 >300 GEO098+1 >300 >300 stack >300 >300 >300 >300 GEO099+1 >300 >300 stack >300 >300 >300 >300 GEO100+1 >300 >300 segmf >300 >300 >300 >300 GEO101+1 >300 >300 stack >300 >300 >300 >300 GEO102+1 >300 >300 stack >300 >300 >300 >300 GEO103+1 >300 >300 stack >300 >300 >300 >300 GEO104+1 >300 >300 stack >300 >300 >300 >300 GEO105+1 >300 >300 stack >300 >300 >300 >300 GEO106+1 >300 >300 stack >300 >300 >300 >300 GEO107+1 >300 >300 stack >300 >300 >300 >300 GEO108+1 >300 >300 stack >300 >300 >300 >300 GEO109+1 >300 >300 stack >300 >300 >300 >300 GEO110+1 >300 >300 stack >300 >300 >300 >300 GEO111+1 >300 >300 stack >300 >300 >300 >300 GEO112+1 >300 >300 stack >300 >300 5.58 2.6 GEO113+1 >300 >300 stack >300 >300 >300 >300 GEO114+1 >300 >300 stack >300 >300 >300 >300 GEO116+1 >300 >300 stack >300 >300 >300 >300 GEO117+1 >300 >300 segmf >300 >300 2.24 0.9 GEO118+1 >300 >300 segmf >300 >300 2.22 0.9 GEO119+1 >300 >300 segmf >300 >300 >300 >300 GEO120+1 >300 >300 segmf >300 >300 >300 >300 GEO121+1 >300 >300 segmf >300 >300 >300 >300 GEO122+1 >300 >300 segmf >300 >300 >300 >300 GEO123+1 >300 >300 segmf >300 >300 >300 >300 GEO124+1 >300 >300 segmf >300 >300 >300 >300 GEO125+1 >300 >300 segmf >300 >300 >300 >300 GEO126+1 >300 >300 segmf >300 >300 >300 >300 GEO127+1 >300 >300 segmf >300 >300 >300 >300 GEO128+1 >300 >300 segmf >300 >300 >300 >300 GEO129+1 >300 >300 segmf >300 >300 >300 >300 GEO130+1 >300 >300 segmf >300 >300 >300 >300 GEO131+1 >300 >300 segmf >300 >300 >300 >300 GEO132+1 >300 >300 segmf >300 >300 >300 >300 GEO133+1 >300 >300 segmf >300 >300 >300 >300 GEO134+1 >300 >300 segmf >300 >300 >300 >300 GEO135+1 >300 >300 segmf >300 >300 >300 >300 GEO136+1 >300 >300 segmf >300 >300 >300 >300 GEO137+1 >300 >300 segmf >300 >300 >300 >300 GEO138+1 >300 >300 segmf >300 >300 >300 >300 GEO139+1 >300 >300 segmf >300 >300 >300 >300 GEO140+1 >300 >300 segmf >300 >300 >300 >300 GEO141+1 >300 >300 segmf >300 >300 >300 >300 GEO142+1 >300 >300 segmf >300 >300 >300 >300 GEO143+1 >300 >300 segmf >300 >300 >300 >300 GEO144+1 >300 >300 segmf >300 >300 >300 >300 GEO145+1 >300 >300 segmf >300 >300 >300 >300 GEO146+1 >300 >300 segmf >300 >300 >300 >300 GEO147+1 >300 >300 segmf >300 >300 20.49 7.06 GEO148+1 >300 >300 segmf >300 >300 0.12 0.06 GEO149+1 >300 >300 segmf >300 >300 >300 >300 GEO150+1 >300 >300 segmf >300 >300 >300 >300 GEO151+1 >300 >300 segmf >300 >300 >300 >300 GEO152+1 >300 >300 segmf >300 >300 >300 >300 GRP194+1 >300 >300 segmf >300 >300 >300 >300 HAL001+1 >300 >300 stack >300 >300 >300 >300 HAL001+2 >300 >300 segmf >300 >300 >300 >300 HAL002+1 >300 >300 segmf >300 >300 >300 >300 HAL003+1 >300 >300 stack >300 >300 >300 >300 HAL003+2 >300 >300 stack >300 >300 >300 >300 HAL003+3 >300 >300 segmf >300 >300 >300 >300 HAL004+1 >300 >300 segmf >300 >300 >300 >300 HAL005+1 >300 >300 segmf >300 >300 >300 >300 HAL006+1 >300 >300 stack >300 >300 >300 >300 LCL181+1 >300 (<0.01) (<0.01) >300 >300 (0.02) (<0.01) (<0.01) (0.03) LCL230+1 jtbug (<0.01) (<0.01) >300 >300 (<0.01) (0.01) (<0.01) (0.02) LCL414+1 18.9 >300 4.5 >300 <0.01 <0.01 <0.01 MGT001+1 >300 >300 >300 >300 >300 >300 >300 MGT002+1 >300 >300 mem >300 >300 2.07 2.04 MGT003+1 >300 >300 mem >300 >300 >300 >300 MGT004+1 >300 >300 >300 >300 >300 >300 >300 MGT005+1 >300 stack stack >300 >300 >300 >300 MGT005+2 >300 >300 stack >300 >300 >300 >300 MGT006+1 >300 >300 >300 >300 >300 >300 >300 MGT007+1 >300 >300 >300 >300 >300 >300 >300 MGT008+1 >300 >300 >300 >300 >300 1.57 1.56 MGT009+1 >300 >300 >300 >300 >300 11.34 11.29 MGT010+1 >300 >300 >300 >300 >300 >300 >300 MGT011+1 >300 stack stack >300 >300 >300 >300 MGT012+1 >300 stack stack >300 >300 >300 >300 MGT013+1 >300 >300 stack >300 >300 >300 140.3 MGT014+1 >300 >300 stack >300 >300 >300 138.86 MGT015+1 >300 >300 >300 >300 >300 0.15 0.13 MGT016+1 >300 >300 >300 >300 >300 0.27 0.17 MGT017+1 >300 >300 >300 >300 >300 0.15 0.15 MGT018+1 >300 >300 >300 >300 >300 0.27 0.15 MGT020+1 >300 >300 segmf >300 >300 >300 >300 MGT021+1 >300 >300 segmf >300 >300 79.08 30.67 MGT022+1 0.37 <0.01 <0.01 >300 0.01 0.14 0.15 MGT022+2 0.36 <0.01 <0.01 >300 <0.01 0.14 0.15 MGT023+1 >300 >300 segmf >300 >300 >300 >300 MGT023+2 >300 >300 segmf >300 >300 >300 >300 MGT024+1 >300 >300 segmf >300 >300 >300 >300 MGT025+1 >300 >300 segmf >300 >300 >300 >300 MGT026+1 >300 >300 segmf >300 >300 >300 >300 MGT027+1 >300 >300 segmf >300 >300 >300 >300 MGT028+1 0.14 0.01 <0.01 >300 <0.01 0.26 0.1 MGT029+1 >300 >300 segmf >300 >300 >300 >300 MGT030+1 0.14 0.01 <0.01 >300 0.01 >300 >300 MGT032+2 0.12 <0.01 <0.01 >300 <0.01 0.01 0.02 MGT034+2 >300 >300 >300 >300 >300 >300 >300 MGT035+1 >300 >300 segmf >300 >300 >300 >300 MGT035+2 >300 >300 stack >300 >300 >300 >300 MGT036+1 0.41 >300 segmf >300 >300 0.04 0.03 MGT036+2 28.86 >300 segmf >300 >300 0.04 0.03 MGT036+3 0.03 <0.01 <0.01 >300 0.01 <0.01 <0.01 MGT037+1 >300 >300 segmf >300 >300 >300 >300 MGT039+1 >300 >300 segmf >300 >300 >300 >300 MGT039+2 >300 >300 segmf >300 >300 >300 >300 MGT041+2 0.05 <0.01 <0.01 >300 >300 0.01 0.01 MGT042+1 >300 >300 stack >300 >300 >300 >300 MGT043+1 >300 >300 segmf >300 >300 >300 >300 MGT044+1 >300 >300 segmf >300 >300 0.55 0.26 MGT045+1 >300 >300 stack >300 >300 0.02 0.01 MGT046+1 >300 >300 segmf >300 >300 >300 262.81 MGT047+1 >300 >300 segmf >300 >300 >300 >300 MGT048+1 >300 >300 segmf >300 >300 0.68 0.36 MGT049+1 >300 >300 segmf >300 >300 0.03 <0.01 MGT050+1 >300 >300 segmf >300 >300 >300 >300 MGT051+1 >300 >300 segmf >300 >300 >300 >300 MGT052+1 >300 >300 stack >300 >300 >300 >300 MGT053+1 >300 >300 stack >300 >300 >300 >300 MGT054+1 >300 >300 segmf >300 >300 >300 >300 MGT055+1 >300 >300 segmf >300 >300 >300 >300 MGT056+1 >300 >300 segmf >300 >300 >300 >300 MGT057+1 >300 >300 segmf >300 >300 >300 >300 MGT058+1 >300 >300 segmf >300 >300 >300 >300 MGT059+1 >300 >300 stack >300 >300 0.11 0.05 MGT060+1 >300 >300 stack >300 >300 >300 >300 MGT061+1 >300 >300 segmf >300 >300 >300 >300 MGT062+1 >300 >300 segmf >300 >300 >300 >300 MGT063+1 >300 >300 segmf >300 >300 >300 >300 MGT064+1 >300 >300 segmf >300 >300 >300 >300 MGT065+1 >300 >300 segmf >300 >300 >300 >300 NLP001+1 0.11 <0.01 <0.01 <0.01 <0.01 4.17 1.36 NLP004+1 >300 >300 stack >300 0.09 >300 >300 NLP007+1 >300 >300 stack >300 0.1 >300 >300 NLP009+1 >300 >300 stack >300 0.03 >300 >300 NLP011+1 >300 >300 stack >300 0.1 >300 >300 NLP079+1 3.1 2.51 0.02 >300 0.13 >300 >300 NLP080+1 2.96 0.01 0.01 >300 0.12 >300 >300 NLP081+1 2.68 0.09 0.01 >300 0.12 >300 >300 NLP094+1 2.63 0.01 <0.01 >300 0.09 >300 >300 NLP117+1 0.21 <0.01 <0.01 2.37 0.02 77.49 22.5 NLP122+1 0.19 <0.01 0.01 0.59 0.02 76.87 22.49 NLP141+1 >300 >300 stack >300 >300 >300 >300 NLP143+1 >300 >300 stack >300 >300 >300 >300 NLP145+1 >300 >300 stack >300 >300 >300 >300 NLP147+1 >300 >300 stack >300 >300 >300 >300 NLP149+1 >300 >300 stack >300 >300 >300 >300 NLP204+1 >300 >300 stack >300 >300 >300 >300 NLP208+1 >300 >300 stack >300 >300 >300 >300 NLP251+1 >300 >300 stack >300 >300 >300 >300 NLP252+1 >300 >300 stack >300 >300 >300 >300 NLP257+1 >300 >300 stack >300 >300 >300 >300 NLP258+1 >300 >300 stack >300 >300 >300 >300 PUZ001+1 >300 >300 stack >300 >300 >300 >300 PUZ005+1 >300 >300 stack >300 >300 >300 >300 PUZ031+1 >300 >300 stack >300 >300 0.52 0.14 PUZ047+1 >300 >300 stack >300 >300 0.01 0.01 SET002+3 >300 >300 stack 0.04 >300 0.02 0.01 SET002+4 >300 >300 stack >300 >300 292.82 164.14 SET008+3 >300 >300 stack >300 >300 0.34 0.22 SET009+3 >300 >300 stack >300 >300 >300 >300 SET010+3 >300 >300 stack >300 >300 >300 >300 SET011+3 >300 >300 stack >300 >300 >300 >300 SET012+4 >300 >300 stack >300 >300 >300 >300 SET013+4 >300 >300 stack >300 >300 >300 >300 SET014+3 >300 >300 stack >300 >300 0.15 0.09 SET014+4 >300 >300 stack >300 >300 >300 >300 SET015+4 >300 >300 stack >300 >300 >300 >300 SET016+1 >300 >300 >300 >300 >300 >300 >300 SET016+4 >300 >300 stack >300 >300 >300 >300 SET017+1 >300 >300 >300 >300 >300 >300 >300 SET018+1 >300 >300 >300 >300 >300 >300 >300 SET018+4 >300 >300 stack >300 >300 >300 >300 SET019+4 >300 >300 stack 0.87 3.95 0.01 0.01 SET020+1 >300 >300 stack >300 >300 >300 >300 SET024+1 >300 >300 >300 >300 >300 >300 >300 SET025+1 >300 >300 >300 >300 >300 >300 >300 SET027+1 >300 >300 >300 >300 >300 >300 >300 SET027+3 >300 >300 stack >300 >300 0.02 0.01 SET027+4 >300 >300 stack >300 >300 >300 >300 SET043+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SET044+1 0.07 0.01 <0.01 7.86 0.03 <0.01 0.01 SET045+1 0.02 <0.01 <0.01 0.02 <0.01 0.02 0.01 SET046+1 0.73 <0.01 <0.01 0.1 <0.01 <0.01 <0.01 SET047+1 >300 >300 0.05 >300 >300 >300 >300 SET054+1 >300 >300 >300 0.58 <0.01 0.05 0.04 SET055+1 >300 >300 >300 >300 0.03 17.03 9.72 SET056+1 >300 >300 >300 >300 >300 >300 >300 SET060+1 >300 >300 stack >300 >300 0.02 0.01 SET061+1 >300 >300 >300 15.43 >300 0.04 0.03 SET062+1 >300 >300 >300 >300 >300 0.04 0.03 SET062+3 27.13 <0.01 <0.01 0.58 <0.01 <0.01 0.01 SET062+4 >300 >300 stack >300 >300 <0.01 <0.01 SET063+1 >300 >300 >300 >300 >300 0.75 0.44 SET063+3 1.02 >300 0.27 0.03 209.97 0.02 0.01 SET063+4 >300 >300 stack >300 >300 291.53 164.93 SET064+1 >300 >300 >300 >300 >300 >300 >300 SET065+1 >300 >300 stack >300 >300 0.05 0.04 SET066+1 >300 >300 >300 >300 >300 >300 >300 SET067+1 >300 >300 >300 >300 >300 >300 >300 SET069+1 >300 >300 >300 >300 >300 >300 >300 SET071+1 >300 >300 >300 >300 >300 >300 >300 SET072+1 >300 >300 >300 >300 >300 >300 >300 SET073+1 >300 >300 >300 >300 >300 >300 >300 SET074+1 >300 >300 >300 >300 >300 >300 >300 SET076+1 >300 >300 >300 >300 >300 >300 >300 SET077+1 >300 >300 >300 >300 >300 >300 >300 SET079+1 >300 >300 >300 >300 >300 >300 >300 SET081+1 >300 >300 >300 >300 >300 >300 >300 SET082+1 >300 >300 >300 >300 >300 >300 >300 SET083+1 >300 >300 >300 >300 >300 >300 >300 SET084+1 >300 >300 >300 >300 >300 >300 >300 SET086+1 >300 >300 >300 >300 >300 >300 >300 SET090+1 >300 >300 >300 >300 >300 >300 >300 SET091+1 >300 >300 >300 >300 >300 >300 >300 SET093+1 >300 >300 >300 >300 >300 >300 >300 SET094+1 >300 >300 >300 >300 >300 >300 >300 SET095+1 >300 >300 >300 >300 >300 >300 >300 SET095+4 >300 >300 stack >300 >300 >300 >300 SET096+1 >300 >300 >300 >300 >300 >300 >300 SET097+1 >300 >300 >300 >300 >300 >300 >300 SET098+1 >300 >300 >300 >300 >300 >300 >300 SET099+1 >300 >300 >300 >300 >300 >300 >300 SET101+1 >300 >300 >300 >300 >300 >300 >300 SET102+1 >300 >300 >300 >300 >300 >300 >300 SET103+1 >300 >300 >300 >300 >300 >300 >300 SET104+1 >300 >300 >300 >300 >300 >300 >300 SET105+1 >300 >300 >300 >300 >300 >300 >300 SET108+1 >300 >300 >300 >300 >300 >300 >300 SET113+1 >300 >300 >300 >300 >300 >300 >300 SET117+1 >300 >300 >300 >300 >300 >300 >300 SET119+1 >300 >300 >300 >300 >300 >300 >300 SET120+1 >300 >300 >300 >300 >300 >300 >300 SET121+1 >300 >300 >300 >300 >300 >300 >300 SET122+1 >300 >300 >300 >300 >300 >300 >300 SET143+3 >300 >300 stack >300 >300 >300 >300 SET143+4 >300 >300 stack >300 >300 >300 >300 SET144+3 >300 >300 segmf >300 >300 >300 >300 SET146+3 >300 >300 stack >300 >300 7.62 7.73 SET148+3 >300 >300 stack 0.03 >300 <0.01 0.01 SET148+4 >300 >300 stack >300 >300 292.06 162.95 SET155+4 >300 >300 stack >300 >300 >300 >300 SET156+4 >300 >300 stack >300 >300 >300 >300 SET159+3 >300 >300 stack >300 >300 >300 >300 SET159+4 >300 >300 stack >300 >300 >300 >300 SET162+3 >300 >300 stack >300 >300 >300 >300 SET162+4 >300 >300 stack >300 >300 292.47 163.09 SET169+3 >300 >300 stack >300 >300 >300 >300 SET169+4 >300 >300 stack >300 >300 >300 >300 SET171+3 >300 >300 stack >300 >300 >300 >300 SET171+4 >300 >300 stack >300 >300 >300 >300 SET173+3 >300 >300 stack >300 >300 0.12 0.09 SET175+3 >300 >300 stack >300 >300 0.12 0.1 SET183+3 >300 >300 stack >300 >300 0.07 0.06 SET185+3 >300 >300 stack >300 >300 0.07 0.05 SET194+3 >300 12.39 0.02 >300 71.64 <0.01 0.02 SET196+3 >300 2.43 0.02 >300 24.9 0.01 0.02 SET199+3 >300 >300 stack >300 >300 0.04 176.15 SET199+4 >300 >300 stack >300 >300 >300 >300 SET200+3 >300 >300 stack >300 >300 20.95 0.48 SET201+3 >300 >300 stack >300 >300 >300 >300 SET347+4 >300 >300 stack >300 >300 290.7 162.39 SET351+4 >300 >300 stack >300 >300 >300 >300 SET352+4 >300 >300 stack >300 >300 >300 >300 SET355+4 >300 >300 stack >300 >300 1.34 0.76 SET358+4 >300 >300 stack >300 >300 >300 >300 SET366+4 >300 >300 stack >300 >300 0.06 0.04 SET372+4 >300 >300 stack >300 >300 >300 >300 SET573+3 0.34 <0.01 <0.01 >300 <0.01 0.01 0.01 SET574+3 0.07 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SET575+3 0.03 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SET576+3 91.5 0.01 <0.01 >300 4.72 85.27 87.5 SET577+3 >300 >300 stack >300 >300 1.17 0.78 SET578+3 >300 >300 stack >300 >300 1.14 0.74 SET579+3 >300 >300 0.25 >300 >300 174.08 114.91 SET580+3 >300 >300 stack >300 >300 >300 >300 SET581+3 >300 >300 stack >300 >300 0.01 <0.01 SET582+3 >300 >300 >300 >300 >300 >300 >300 SET583+3 9.27 <0.01 <0.01 <0.01 0.01 <0.01 0.01 SET584+3 >300 >300 stack >300 >300 20.48 0.44 SET585+3 >300 >300 stack >300 <0.01 <0.01 <0.01 SET586+3 >300 >300 stack >300 >300 >300 >300 SET587+3 >300 >300 stack >300 >300 >300 >300 SET588+3 >300 >300 stack >300 >300 >300 >300 SET589+3 >300 >300 49.87 >300 0.02 0.02 <0.01 SET590+3 22.6 <0.01 <0.01 >300 204.78 0.03 0.01 SET591+3 >300 >300 49.2 >300 >300 1.32 0.83 SET592+3 >300 >300 stack >300 >300 >300 >300 SET593+3 >300 >300 >300 >300 >300 >300 >300 SET594+3 >300 >300 >300 >300 >300 >300 >300 SET595+3 >300 >300 >300 >300 >300 >300 >300 SET595+4 >300 >300 stack >300 >300 >300 >300 SET596+3 >300 >300 stack >300 >300 >300 >300 SET597+3 >300 >300 stack >300 >300 >300 >300 SET598+3 >300 >300 stack >300 >300 >300 >300 SET599+3 >300 >300 stack >300 >300 >300 >300 SET600+3 >300 >300 stack >300 >300 >300 >300 SET601+3 >300 >300 stack >300 >300 >300 >300 SET602+3 >300 >300 stack 0.04 >300 <0.01 0.01 SET602+4 >300 >300 stack >300 >300 291.63 165.2 SET603+3 >300 >300 mem >300 0.02 >300 >300 SET603+4 >300 >300 stack >300 >300 292.71 163.38 SET604+3 >300 >300 stack 0.04 <0.01 <0.01 0.01 SET605+3 >300 >300 stack 1.83 <0.01 0.02 <0.01 SET606+3 >300 >300 >300 >300 >300 >300 >300 SET607+3 >300 >300 stack >300 >300 >300 >300 SET608+3 >300 >300 stack >300 >300 >300 >300 SET609+3 >300 >300 stack >300 >300 >300 >300 SET610+3 >300 >300 >300 >300 >300 >300 >300 SET611+3 >300 >300 >300 >300 >300 >300 >300 SET612+3 >300 >300 stack >300 >300 >300 >300 SET613+3 >300 >300 segmf >300 >300 >300 >300 SET614+3 >300 >300 segmf >300 >300 >300 >300 SET615+3 >300 >300 segmf >300 >300 >300 >300 SET616+3 >300 >300 stack >300 >300 >300 >300 SET617+3 >300 >300 stack >300 >300 >300 >300 SET618+3 >300 >300 stack >300 >300 >300 >300 SET619+3 >300 >300 stack >300 >300 >300 >300 SET620+3 >300 >300 >300 >300 >300 >300 >300 SET621+3 >300 >300 stack >300 >300 >300 >300 SET622+3 >300 >300 >300 >300 >300 >300 >300 SET623+3 >300 >300 stack >300 >300 >300 >300 SET624+3 >300 >300 stack >300 >300 >300 >300 SET625+3 >300 >300 stack >300 >300 <0.01 <0.01 SET626+3 >300 >300 stack >300 >300 0.03 0.03 SET627+3 35.08 0.13 0.01 >300 0.03 0.01 <0.01 SET628+3 >300 >300 stack >300 >300 >300 >300 SET629+3 >300 >300 stack >300 >300 2.71 2.91 SET630+3 >300 >300 stack >300 >300 15.09 >300 SET631+3 >300 >300 0.2 >300 >300 273.59 270.04 SET632+3 >300 >300 stack >300 >300 3.54 0.75 SET633+3 >300 >300 stack >300 >300 >300 >300 SET634+3 >300 >300 >300 >300 >300 >300 >300 SET635+3 >300 >300 stack >300 >300 >300 >300 SET636+3 >300 >300 stack >300 >300 >300 >300 SET637+3 >300 >300 stack >300 >300 >300 >300 SET638+3 >300 >300 >300 >300 >300 42.55 24.72 SET639+3 >300 >300 stack >300 >300 >300 >300 SET640+3 >300 >300 >300 >300 >300 >300 >300 SET641+3 >300 >300 >300 >300 >300 >300 >300 SET642+3 >300 >300 >300 >300 0.62 >300 24.08 SET643+3 >300 >300 >300 >300 >300 >300 204.39 SET644+3 >300 >300 >300 >300 >300 >300 >300 SET645+3 >300 >300 >300 >300 >300 >300 >300 SET646+3 >300 >300 >300 >300 >300 >300 >300 SET647+3 >300 >300 >300 >300 >300 >300 >300 SET648+3 >300 >300 >300 >300 >300 >300 >300 SET649+3 >300 >300 >300 >300 >300 >300 >300 SET650+3 >300 >300 >300 >300 >300 >300 >300 SET651+3 >300 >300 >300 >300 >300 >300 >300 SET652+3 >300 >300 >300 >300 >300 >300 >300 SET653+3 >300 >300 >300 >300 >300 >300 >300 SET654+3 >300 >300 >300 >300 >300 >300 >300 SET655+3 >300 >300 >300 >300 >300 >300 >300 SET656+3 >300 >300 >300 >300 >300 >300 >300 SET657+3 >300 >300 >300 >300 >300 >300 >300 SET658+3 >300 >300 >300 >300 >300 17.65 10.05 SET659+3 >300 >300 >300 >300 >300 >300 >300 SET660+3 >300 >300 >300 >300 >300 >300 >300 SET661+3 >300 >300 >300 >300 >300 >300 >300 SET662+3 >300 >300 >300 >300 >300 >300 >300 SET663+3 >300 >300 >300 >300 >300 >300 >300 SET664+3 >300 >300 >300 >300 >300 >300 >300 SET665+3 >300 >300 >300 >300 >300 >300 >300 SET666+3 >300 >300 >300 >300 >300 >300 >300 SET667+3 >300 >300 >300 >300 >300 >300 >300 SET668+3 >300 >300 >300 >300 >300 >300 >300 SET669+3 >300 >300 >300 >300 >300 >300 >300 SET670+3 >300 >300 >300 >300 >300 >300 >300 SET671+3 >300 >300 >300 >300 >300 >300 >300 SET672+3 >300 >300 >300 >300 >300 >300 >300 SET673+3 >300 >300 >300 >300 >300 >300 >300 SET674+3 >300 >300 >300 >300 >300 >300 >300 SET675+3 >300 >300 >300 >300 >300 >300 >300 SET676+3 >300 >300 >300 >300 >300 0.05 0.03 SET677+3 >300 >300 >300 >300 >300 75.35 229.46 SET678+3 >300 >300 >300 >300 >300 >300 >300 SET679+3 >300 >300 >300 >300 >300 >300 >300 SET680+3 >300 >300 >300 >300 >300 >300 >300 SET681+3 >300 >300 >300 >300 >300 >300 >300 SET682+3 >300 >300 >300 >300 >300 >300 >300 SET683+3 >300 >300 >300 >300 >300 >300 >300 SET684+3 >300 >300 >300 >300 >300 >300 >300 SET685+3 >300 >300 >300 >300 >300 >300 >300 SET686+3 >300 >300 >300 >300 >300 >300 >300 SET687+4 >300 >300 stack 0.69 0.01 0.03 0.02 SET688+4 >300 >300 stack >300 >300 >300 >300 SET689+4 >300 >300 stack >300 >300 >300 >300 SET690+4 >300 >300 stack >300 >300 >300 >300 SET691+4 >300 >300 stack >300 >300 >300 >300 SET692+4 >300 >300 stack >300 >300 >300 >300 SET693+4 >300 >300 stack >300 >300 >300 >300 SET694+4 >300 >300 stack >300 >300 >300 >300 SET695+4 >300 >300 stack >300 >300 >300 >300 SET696+4 >300 >300 stack >300 >300 >300 >300 SET697+4 >300 >300 stack >300 >300 >300 >300 SET698+4 >300 >300 stack >300 >300 >300 >300 SET699+4 >300 >300 stack >300 >300 >300 >300 SET700+4 >300 >300 stack >300 >300 >300 >300 SET701+4 >300 >300 stack >300 >300 >300 >300 SET702+4 >300 >300 stack >300 >300 >300 >300 SET703+4 >300 >300 stack >300 >300 >300 >300 SET704+4 >300 >300 stack >300 >300 1.11 0.62 SET705+4 >300 >300 stack >300 >300 0.46 0.24 SET706+4 >300 >300 stack >300 >300 >300 >300 SET707+4 >300 >300 stack >300 >300 >300 >300 SET708+4 >300 >300 stack >300 >300 >300 >300 SET709+4 >300 >300 stack >300 >300 >300 >300 SET710+4 >300 >300 stack >300 >300 >300 >300 SET711+4 >300 >300 stack >300 >300 >300 >300 SET712+4 >300 >300 stack >300 >300 >300 >300 SET713+4 >300 >300 stack >300 >300 >300 >300 SET714+4 >300 >300 stack >300 >300 >300 >300 SET715+4 >300 >300 stack >300 >300 >300 >300 SET716+4 >300 >300 stack >300 >300 >300 >300 SET717+4 >300 >300 stack >300 >300 >300 >300 SET718+4 >300 >300 stack >300 >300 >300 >300 SET719+4 >300 >300 stack >300 >300 >300 >300 SET720+4 >300 >300 stack >300 >300 >300 >300 SET721+4 >300 >300 stack >300 >300 >300 >300 SET722+4 >300 >300 stack >300 >300 >300 >300 SET723+4 >300 >300 stack >300 >300 >300 >300 SET724+4 >300 >300 stack >300 >300 >300 >300 SET725+4 >300 >300 stack >300 >300 >300 >300 SET726+4 >300 >300 stack >300 >300 >300 >300 SET727+4 >300 >300 stack >300 >300 >300 >300 SET728+4 >300 >300 stack >300 >300 >300 >300 SET729+4 >300 >300 stack >300 >300 >300 >300 SET730+4 >300 >300 >300 >300 >300 >300 >300 SET731+4 >300 >300 >300 >300 >300 >300 >300 SET732+4 >300 >300 >300 >300 >300 >300 >300 SET733+4 >300 >300 stack >300 >300 >300 >300 SET734+4 >300 >300 stack >300 >300 >300 >300 SET735+4 >300 >300 stack >300 >300 >300 >300 SET736+4 >300 >300 stack >300 >300 >300 >300 SET737+4 >300 >300 stack >300 >300 >300 >300 SET738+4 >300 >300 stack >300 >300 >300 >300 SET739+4 >300 >300 stack >300 >300 >300 >300 SET740+4 >300 >300 stack >300 >300 >300 >300 SET741+4 >300 >300 stack >300 >300 >300 >300 SET742+4 >300 >300 stack >300 >300 >300 >300 SET743+4 >300 >300 stack >300 >300 >300 >300 SET744+4 >300 >300 stack >300 >300 >300 >300 SET745+4 >300 >300 stack >300 >300 >300 >300 SET746+4 >300 >300 stack >300 >300 >300 >300 SET747+4 >300 >300 stack >300 >300 >300 >300 SET748+4 >300 >300 stack >300 >300 >300 >300 SET749+4 >300 >300 stack >300 >300 >300 >300 SET750+4 >300 >300 stack >300 >300 >300 >300 SET751+4 >300 >300 stack >300 >300 >300 >300 SET752+4 >300 >300 stack >300 >300 >300 >300 SET753+4 >300 >300 stack >300 >300 >300 >300 SET754+4 >300 >300 stack >300 >300 >300 >300 SET755+4 >300 >300 stack >300 >300 >300 >300 SET756+4 >300 >300 stack >300 >300 >300 >300 SET757+4 >300 >300 stack >300 >300 >300 >300 SET758+4 >300 >300 stack >300 >300 >300 >300 SET759+4 >300 >300 stack >300 >300 >300 >300 SET760+4 >300 >300 stack >300 >300 >300 >300 SET761+4 >300 >300 stack >300 >300 >300 >300 SET762+4 >300 >300 stack >300 >300 >300 >300 SET763+4 >300 >300 stack >300 >300 >300 >300 SET764+4 >300 >300 stack >300 >300 >300 >300 SET765+4 >300 >300 stack >300 >300 >300 >300 SET766+4 >300 >300 stack >300 >300 1.09 0.44 SET767+4 >300 >300 stack >300 >300 48.52 19.69 SET768+4 >300 >300 stack >300 >300 >300 >300 SET769+4 >300 >300 stack >300 >300 >300 >300 SET770+4 >300 >300 stack >300 >300 >300 >300 SET771+4 >300 >300 stack >300 >300 >300 >300 SET772+4 >300 >300 stack >300 >300 >300 >300 SET773+4 >300 >300 stack >300 >300 >300 >300 SET774+4 >300 >300 stack >300 >300 >300 >300 SET775+4 >300 >300 stack >300 >300 >300 >300 SET776+4 >300 >300 stack >300 >300 >300 >300 SET786+1 0.73 <0.01 <0.01 0.1 <0.01 <0.01 0.01 SWC001+1 >300 >300 >300 >300 >300 >300 >300 SWC002+1 >300 >300 >300 >300 >300 >300 >300 SWC003+1 >300 >300 >300 >300 >300 >300 >300 SWC004+1 >300 >300 >300 >300 >300 >300 >300 SWC005+1 >300 >300 >300 >300 >300 >300 >300 SWC006+1 >300 >300 stack >300 >300 >300 >300 SWC007+1 >300 >300 >300 >300 >300 >300 >300 SWC008+1 >300 >300 >300 >300 >300 >300 >300 SWC009+1 >300 >300 >300 >300 >300 >300 >300 SWC010+1 >300 >300 >300 >300 >300 >300 >300 SWC011+1 >300 >300 >300 >300 >300 >300 >300 SWC012+1 >300 >300 >300 >300 >300 >300 >300 SWC013+1 >300 >300 >300 >300 >300 >300 >300 SWC014+1 >300 >300 >300 >300 >300 >300 >300 SWC015+1 >300 >300 >300 >300 >300 >300 >300 SWC016+1 >300 >300 >300 >300 >300 >300 >300 SWC017+1 >300 >300 stack >300 >300 >300 >300 SWC018+1 >300 >300 >300 >300 >300 >300 >300 SWC019+1 >300 >300 >300 >300 >300 >300 >300 SWC020+1 >300 >300 >300 >300 >300 >300 >300 SWC021+1 >300 >300 >300 >300 >300 >300 >300 SWC022+1 >300 >300 >300 >300 >300 >300 >300 SWC023+1 >300 >300 >300 >300 >300 >300 >300 SWC024+1 >300 >300 >300 >300 >300 >300 >300 SWC025+1 >300 >300 >300 >300 >300 >300 >300 SWC026+1 >300 >300 >300 >300 >300 >300 >300 SWC027+1 >300 >300 >300 >300 >300 >300 >300 SWC028+1 >300 >300 >300 >300 >300 >300 >300 SWC029+1 >300 >300 >300 >300 >300 >300 >300 SWC030+1 >300 >300 >300 >300 >300 >300 >300 SWC031+1 >300 >300 >300 >300 >300 >300 >300 SWC032+1 >300 >300 >300 >300 >300 >300 >300 SWC033+1 >300 >300 >300 >300 >300 >300 >300 SWC034+1 >300 >300 >300 >300 >300 >300 >300 SWC035+1 >300 >300 >300 >300 >300 >300 >300 SWC036+1 >300 >300 >300 >300 >300 >300 >300 SWC037+1 >300 >300 >300 >300 >300 >300 >300 SWC038+1 >300 >300 >300 >300 >300 >300 >300 SWC039+1 >300 >300 >300 >300 >300 >300 >300 SWC040+1 >300 >300 >300 >300 >300 >300 >300 SWC041+1 >300 >300 >300 >300 >300 >300 >300 SWC042+1 >300 >300 >300 >300 >300 >300 >300 SWC043+1 >300 >300 >300 >300 >300 >300 >300 SWC044+1 >300 >300 >300 >300 >300 >300 >300 SWC045+1 >300 >300 >300 >300 >300 >300 >300 SWC046+1 >300 >300 >300 >300 >300 >300 >300 SWC047+1 >300 >300 >300 >300 >300 >300 >300 SWC048+1 >300 >300 >300 >300 >300 >300 >300 SWC049+1 >300 >300 >300 >300 >300 >300 >300 SWC050+1 >300 >300 >300 >300 >300 >300 >300 SWC051+1 >300 >300 >300 >300 >300 >300 >300 SWC052+1 >300 >300 stack >300 >300 >300 >300 SWC053+1 >300 >300 >300 >300 >300 >300 >300 SWC054+1 >300 >300 stack >300 >300 >300 >300 SWC055+1 >300 >300 >300 >300 >300 >300 >300 SWC056+1 >300 >300 >300 >300 >300 >300 >300 SWC057+1 >300 >300 stack >300 >300 >300 >300 SWC058+1 >300 >300 stack >300 >300 >300 >300 SWC059+1 >300 >300 >300 >300 >300 >300 >300 SWC060+1 >300 >300 stack >300 >300 >300 >300 SWC061+1 >300 >300 stack >300 >300 >300 >300 SWC062+1 >300 >300 >300 >300 >300 >300 >300 SWC063+1 >300 >300 stack >300 >300 >300 >300 SWC064+1 >300 >300 >300 >300 >300 >300 >300 SWC065+1 >300 >300 >300 >300 >300 >300 >300 SWC066+1 >300 >300 >300 >300 >300 >300 >300 SWC067+1 >300 >300 >300 >300 >300 >300 >300 SWC068+1 >300 >300 >300 >300 >300 >300 >300 SWC069+1 >300 >300 >300 >300 >300 >300 >300 SWC070+1 >300 >300 >300 >300 >300 >300 >300 SWC071+1 >300 >300 >300 >300 >300 >300 >300 SWC072+1 >300 >300 stack >300 >300 >300 >300 SWC073+1 >300 >300 >300 >300 >300 >300 >300 SWC074+1 >300 >300 >300 >300 >300 >300 >300 SWC075+1 >300 >300 stack >300 >300 >300 >300 SWC076+1 >300 >300 >300 >300 >300 >300 >300 SWC077+1 >300 >300 >300 >300 >300 >300 >300 SWC078+1 >300 >300 >300 >300 >300 >300 >300 SWC079+1 >300 >300 >300 >300 >300 >300 >300 SWC080+1 >300 >300 stack >300 >300 >300 >300 SWC081+1 >300 >300 >300 >300 >300 >300 >300 SWC082+1 >300 >300 >300 >300 >300 >300 >300 SWC083+1 >300 >300 stack >300 >300 >300 >300 SWC084+1 >300 >300 >300 >300 >300 >300 >300 SWC085+1 >300 >300 >300 >300 >300 >300 >300 SWC086+1 >300 >300 >300 >300 >300 >300 >300 SWC087+1 >300 >300 >300 >300 >300 >300 >300 SWC088+1 >300 >300 >300 >300 >300 >300 >300 SWC089+1 >300 >300 >300 >300 >300 >300 >300 SWC090+1 >300 >300 >300 >300 >300 >300 >300 SWC091+1 >300 >300 >300 >300 >300 >300 >300 SWC092+1 >300 >300 >300 >300 >300 >300 >300 SWC093+1 >300 >300 >300 >300 >300 >300 >300 SWC094+1 >300 >300 >300 >300 >300 >300 >300 SWC095+1 >300 >300 stack >300 >300 >300 >300 SWC096+1 >300 >300 stack >300 >300 >300 >300 SWC097+1 >300 >300 >300 >300 >300 >300 >300 SWC098+1 >300 >300 >300 >300 >300 >300 >300 SWC099+1 >300 >300 >300 >300 >300 >300 >300 SWC100+1 >300 >300 >300 >300 >300 >300 >300 SWC101+1 >300 >300 >300 >300 >300 >300 >300 SWC102+1 >300 >300 >300 >300 >300 >300 >300 SWC103+1 >300 >300 >300 >300 >300 >300 >300 SWC104+1 >300 >300 >300 >300 >300 >300 >300 SWC105+1 >300 >300 >300 >300 >300 >300 >300 SWC106+1 >300 >300 >300 >300 >300 >300 >300 SWC107+1 >300 >300 >300 >300 >300 >300 >300 SWC108+1 >300 >300 >300 >300 >300 >300 >300 SWC109+1 >300 >300 stack >300 >300 >300 >300 SWC110+1 >300 >300 >300 >300 >300 >300 >300 SWC111+1 >300 >300 >300 >300 >300 >300 >300 SWC112+1 >300 >300 >300 >300 >300 >300 >300 SWC113+1 >300 >300 stack >300 >300 >300 >300 SWC114+1 >300 >300 >300 >300 >300 >300 >300 SWC115+1 >300 >300 >300 >300 >300 >300 >300 SWC116+1 >300 >300 >300 >300 >300 >300 >300 SWC117+1 >300 >300 >300 >300 >300 >300 >300 SWC118+1 >300 >300 >300 >300 >300 >300 >300 SWC119+1 >300 >300 >300 >300 >300 >300 >300 SWC120+1 >300 >300 >300 >300 >300 >300 >300 SWC121+1 >300 >300 >300 >300 >300 >300 >300 SWC122+1 >300 >300 >300 >300 >300 >300 >300 SWC123+1 >300 >300 >300 >300 >300 >300 >300 SWC124+1 >300 >300 >300 >300 >300 >300 >300 SWC125+1 >300 >300 >300 >300 >300 >300 >300 SWC126+1 >300 >300 >300 >300 >300 >300 >300 SWC127+1 >300 >300 >300 >300 >300 >300 >300 SWC128+1 >300 >300 stack >300 >300 >300 >300 SWC129+1 >300 >300 >300 >300 >300 >300 >300 SWC130+1 >300 >300 >300 >300 >300 >300 >300 SWC131+1 >300 >300 >300 >300 >300 >300 >300 SWC132+1 >300 >300 >300 >300 >300 >300 >300 SWC133+1 >300 >300 >300 >300 >300 >300 >300 SWC134+1 >300 >300 >300 >300 >300 >300 >300 SWC135+1 >300 >300 >300 >300 >300 >300 >300 SWC136+1 >300 >300 >300 >300 >300 >300 >300 SWC137+1 >300 >300 >300 >300 >300 >300 >300 SWC138+1 >300 >300 >300 >300 >300 >300 >300 SWC139+1 >300 >300 >300 >300 >300 >300 >300 SWC140+1 >300 >300 >300 >300 >300 >300 >300 SWC141+1 >300 >300 >300 >300 >300 >300 >300 SWC142+1 >300 >300 >300 >300 >300 >300 >300 SWC143+1 >300 >300 >300 >300 >300 >300 >300 SWC144+1 >300 >300 >300 >300 >300 >300 >300 SWC145+1 >300 >300 >300 >300 >300 >300 >300 SWC146+1 >300 >300 >300 >300 >300 >300 >300 SWC147+1 >300 >300 >300 >300 >300 >300 >300 SWC148+1 >300 >300 >300 >300 >300 >300 >300 SWC149+1 >300 >300 >300 >300 >300 >300 >300 SWC150+1 >300 >300 >300 >300 >300 >300 >300 SWC151+1 >300 >300 >300 >300 >300 >300 >300 SWC152+1 >300 >300 stack >300 >300 >300 >300 SWC153+1 >300 >300 >300 >300 >300 >300 >300 SWC154+1 >300 >300 >300 >300 >300 >300 >300 SWC155+1 >300 >300 >300 >300 >300 >300 >300 SWC156+1 >300 >300 >300 >300 >300 >300 >300 SWC157+1 >300 >300 >300 >300 >300 >300 >300 SWC158+1 >300 >300 >300 >300 >300 >300 >300 SWC159+1 >300 >300 stack >300 >300 >300 >300 SWC160+1 >300 >300 >300 >300 >300 >300 >300 SWC161+1 >300 >300 stack >300 >300 >300 >300 SWC162+1 >300 >300 >300 >300 >300 >300 >300 SWC163+1 >300 >300 stack >300 >300 >300 >300 SWC164+1 >300 >300 stack >300 >300 >300 >300 SWC165+1 >300 >300 >300 >300 >300 >300 >300 SWC166+1 >300 >300 >300 >300 >300 >300 >300 SWC167+1 >300 >300 >300 >300 >300 >300 >300 SWC168+1 >300 >300 stack >300 >300 >300 >300 SWC169+1 >300 >300 stack >300 >300 >300 >300 SWC170+1 >300 >300 >300 >300 >300 >300 >300 SWC171+1 >300 >300 stack >300 >300 >300 >300 SWC172+1 >300 >300 stack >300 >300 >300 >300 SWC173+1 >300 >300 >300 >300 >300 >300 >300 SWC174+1 >300 >300 >300 >300 >300 >300 >300 SWC175+1 >300 >300 >300 >300 >300 >300 >300 SWC176+1 >300 >300 stack >300 >300 >300 >300 SWC177+1 >300 >300 stack >300 >300 >300 >300 SWC178+1 >300 >300 >300 >300 >300 >300 >300 SWC179+1 >300 >300 >300 >300 >300 >300 >300 SWC180+1 >300 >300 >300 >300 >300 >300 >300 SWC181+1 >300 >300 >300 >300 >300 >300 >300 SWC182+1 >300 >300 >300 >300 >300 >300 >300 SWC183+1 >300 >300 stack >300 >300 >300 >300 SWC184+1 >300 >300 stack >300 >300 >300 >300 SWC185+1 >300 >300 >300 >300 >300 >300 >300 SWC186+1 >300 >300 >300 >300 >300 >300 >300 SWC187+1 >300 >300 >300 >300 >300 >300 >300 SWC188+1 >300 >300 >300 >300 >300 >300 >300 SWC189+1 >300 >300 >300 >300 >300 >300 >300 SWC190+1 >300 >300 stack >300 >300 >300 >300 SWC191+1 >300 >300 >300 >300 >300 >300 >300 SWC192+1 >300 >300 >300 >300 >300 >300 >300 SWC193+1 >300 >300 >300 >300 >300 >300 >300 SWC194+1 >300 >300 >300 >300 >300 >300 >300 SWC195+1 >300 >300 >300 >300 >300 >300 >300 SWC196+1 >300 >300 >300 >300 >300 >300 >300 SWC197+1 >300 >300 >300 >300 >300 >300 >300 SWC198+1 >300 >300 >300 >300 >300 >300 >300 SWC199+1 >300 >300 >300 >300 >300 >300 >300 SWC200+1 >300 >300 >300 >300 >300 >300 >300 SWC201+1 >300 >300 >300 >300 >300 >300 >300 SWC202+1 >300 >300 >300 >300 >300 >300 >300 SWC203+1 >300 >300 >300 >300 >300 >300 >300 SWC204+1 >300 >300 >300 >300 >300 >300 >300 SWC205+1 >300 >300 >300 >300 >300 >300 >300 SWC206+1 >300 >300 >300 >300 >300 >300 >300 SWC207+1 >300 >300 >300 >300 >300 >300 >300 SWC208+1 >300 >300 >300 >300 >300 >300 >300 SWC209+1 >300 >300 >300 >300 >300 >300 >300 SWC210+1 >300 >300 >300 >300 >300 >300 >300 SWC211+1 >300 >300 >300 >300 >300 >300 >300 SWC212+1 >300 >300 >300 >300 >300 >300 >300 SWC213+1 >300 >300 >300 >300 >300 >300 >300 SWC214+1 >300 >300 >300 >300 >300 >300 >300 SWC215+1 >300 >300 >300 >300 >300 >300 >300 SWC216+1 >300 >300 >300 >300 >300 >300 >300 SWC217+1 >300 >300 >300 >300 >300 >300 >300 SWC218+1 >300 >300 >300 >300 >300 >300 >300 SWC219+1 >300 >300 >300 >300 >300 >300 >300 SWC220+1 >300 >300 >300 >300 >300 >300 >300 SWC221+1 >300 >300 stack >300 >300 >300 >300 SWC222+1 >300 >300 stack >300 >300 >300 >300 SWC223+1 >300 >300 >300 >300 >300 >300 >300 SWC224+1 >300 >300 >300 >300 >300 >300 >300 SWC225+1 >300 >300 stack >300 >300 >300 >300 SWC226+1 >300 >300 >300 >300 >300 >300 >300 SWC227+1 >300 >300 stack >300 >300 >300 >300 SWC228+1 >300 >300 >300 >300 >300 >300 >300 SWC229+1 >300 >300 >300 >300 >300 >300 >300 SWC230+1 >300 >300 >300 >300 >300 >300 >300 SWC231+1 >300 >300 stack >300 >300 >300 >300 SWC232+1 >300 >300 >300 >300 >300 >300 >300 SWC233+1 >300 >300 >300 >300 >300 >300 >300 SWC234+1 >300 >300 stack >300 >300 >300 >300 SWC235+1 >300 >300 >300 >300 >300 >300 >300 SWC236+1 >300 >300 >300 >300 >300 >300 >300 SWC237+1 >300 >300 stack >300 >300 >300 >300 SWC238+1 >300 >300 >300 >300 >300 >300 >300 SWC239+1 >300 >300 >300 >300 >300 >300 >300 SWC240+1 >300 >300 >300 >300 >300 >300 >300 SWC241+1 >300 >300 stack >300 >300 >300 >300 SWC242+1 >300 >300 stack >300 >300 >300 >300 SWC243+1 >300 >300 >300 >300 >300 >300 >300 SWC244+1 >300 >300 >300 >300 >300 >300 >300 SWC245+1 >300 >300 stack >300 >300 >300 >300 SWC246+1 >300 >300 stack >300 >300 >300 >300 SWC247+1 >300 >300 >300 >300 >300 >300 >300 SWC248+1 >300 >300 stack >300 >300 >300 >300 SWC249+1 >300 >300 >300 >300 >300 >300 >300 SWC250+1 >300 >300 stack >300 >300 >300 >300 SWC251+1 >300 >300 stack >300 >300 >300 >300 SWC252+1 >300 >300 >300 >300 >300 >300 >300 SWC253+1 >300 >300 >300 >300 >300 >300 >300 SWC254+1 >300 >300 >300 >300 >300 >300 >300 SWC255+1 >300 >300 >300 >300 >300 >300 >300 SWC256+1 >300 >300 >300 >300 >300 >300 >300 SWC257+1 >300 >300 stack >300 >300 >300 >300 SWC258+1 >300 >300 >300 >300 >300 >300 >300 SWC259+1 >300 >300 stack >300 >300 >300 >300 SWC260+1 >300 >300 >300 >300 >300 >300 >300 SWC261+1 >300 >300 stack >300 >300 >300 >300 SWC262+1 >300 >300 >300 >300 >300 >300 >300 SWC263+1 >300 >300 stack >300 >300 >300 >300 SWC264+1 >300 >300 stack >300 >300 >300 >300 SWC265+1 >300 >300 stack >300 >300 >300 >300 SWC266+1 >300 >300 stack >300 >300 >300 >300 SWC267+1 >300 >300 >300 >300 >300 >300 >300 SWC268+1 >300 >300 stack >300 >300 >300 >300 SWC269+1 >300 >300 >300 >300 >300 >300 >300 SWC270+1 >300 >300 stack >300 >300 >300 >300 SWC271+1 >300 >300 >300 >300 >300 >300 >300 SWC272+1 >300 >300 stack >300 >300 >300 >300 SWC273+1 >300 >300 stack >300 >300 >300 >300 SWC274+1 >300 >300 stack >300 >300 >300 >300 SWC275+1 >300 >300 stack >300 >300 >300 >300 SWC276+1 >300 >300 >300 >300 >300 >300 >300 SWC277+1 >300 >300 >300 >300 >300 >300 >300 SWC278+1 >300 >300 >300 >300 >300 >300 >300 SWC279+1 >300 >300 >300 >300 >300 >300 >300 SWC280+1 >300 >300 >300 >300 >300 >300 >300 SWC281+1 >300 >300 >300 >300 >300 >300 >300 SWC282+1 >300 >300 stack >300 >300 >300 >300 SWC283+1 >300 >300 >300 >300 >300 >300 >300 SWC284+1 >300 >300 stack >300 >300 >300 >300 SWC285+1 >300 >300 >300 >300 >300 >300 >300 SWC286+1 >300 >300 stack >300 >300 >300 >300 SWC287+1 >300 >300 stack >300 >300 >300 >300 SWC288+1 >300 >300 stack >300 >300 >300 >300 SWC289+1 >300 >300 >300 >300 >300 >300 >300 SWC290+1 >300 >300 stack >300 >300 >300 >300 SWC291+1 >300 >300 >300 >300 >300 >300 >300 SWC292+1 >300 >300 >300 >300 >300 >300 >300 SWC293+1 >300 >300 stack >300 >300 >300 >300 SWC294+1 >300 >300 stack >300 >300 >300 >300 SWC295+1 >300 >300 >300 >300 >300 >300 >300 SWC296+1 >300 >300 >300 >300 >300 >300 >300 SWC297+1 >300 >300 >300 >300 >300 >300 >300 SWC298+1 >300 >300 >300 >300 >300 >300 >300 SWC299+1 >300 >300 >300 >300 >300 >300 >300 SWC300+1 >300 >300 >300 >300 >300 >300 >300 SWC301+1 >300 >300 >300 >300 >300 >300 >300 SWC302+1 >300 >300 >300 >300 >300 >300 >300 SWC303+1 >300 >300 stack >300 >300 >300 >300 SWC304+1 >300 >300 >300 >300 >300 >300 >300 SWC305+1 >300 >300 >300 >300 >300 >300 >300 SWC306+1 >300 >300 >300 >300 >300 >300 >300 SWC307+1 >300 >300 >300 >300 >300 >300 >300 SWC308+1 >300 >300 >300 >300 >300 >300 >300 SWC309+1 >300 >300 >300 >300 >300 >300 >300 SWC310+1 >300 >300 stack >300 >300 >300 >300 SWC311+1 >300 >300 >300 >300 >300 >300 >300 SWC312+1 >300 >300 stack >300 >300 >300 >300 SWC313+1 >300 >300 >300 >300 >300 >300 >300 SWC314+1 >300 >300 stack >300 >300 >300 >300 SWC315+1 >300 >300 stack >300 >300 >300 >300 SWC316+1 >300 >300 >300 >300 >300 >300 >300 SWC317+1 >300 >300 >300 >300 >300 >300 >300 SWC318+1 >300 >300 >300 >300 >300 >300 >300 SWC319+1 >300 >300 >300 >300 >300 >300 >300 SWC320+1 >300 >300 stack >300 >300 >300 >300 SWC321+1 >300 >300 >300 >300 >300 >300 >300 SWC322+1 >300 >300 >300 >300 >300 >300 >300 SWC323+1 >300 >300 >300 >300 >300 >300 >300 SWC324+1 >300 >300 stack >300 >300 >300 >300 SWC325+1 >300 >300 >300 >300 >300 >300 >300 SWC326+1 >300 >300 >300 >300 >300 >300 >300 SWC327+1 >300 >300 >300 >300 >300 >300 >300 SWC328+1 >300 >300 >300 >300 >300 >300 >300 SWC329+1 >300 >300 >300 >300 >300 >300 >300 SWC330+1 >300 >300 stack >300 >300 >300 >300 SWC331+1 >300 >300 >300 >300 >300 >300 >300 SWC332+1 >300 >300 >300 >300 >300 >300 >300 SWC333+1 >300 >300 >300 >300 >300 >300 >300 SWC334+1 >300 >300 >300 >300 >300 >300 >300 SWC335+1 >300 >300 >300 >300 >300 >300 >300 SWC336+1 >300 >300 stack >300 >300 >300 >300 SWC337+1 >300 >300 >300 >300 >300 >300 >300 SWC338+1 >300 >300 >300 >300 >300 >300 >300 SWC339+1 >300 >300 >300 >300 >300 >300 >300 SWC340+1 >300 >300 >300 >300 >300 >300 >300 SWC341+1 >300 >300 >300 >300 >300 >300 >300 SWC342+1 >300 >300 >300 >300 >300 >300 >300 SWC343+1 >300 >300 >300 >300 >300 >300 >300 SWC344+1 >300 >300 >300 >300 >300 >300 >300 SWC345+1 >300 >300 >300 >300 >300 >300 >300 SWC346+1 >300 >300 stack >300 >300 >300 >300 SWC347+1 >300 >300 >300 >300 >300 >300 >300 SWC348+1 >300 >300 >300 >300 >300 >300 >300 SWC349+1 >300 >300 >300 >300 >300 >300 >300 SWC350+1 >300 >300 >300 >300 >300 >300 >300 SWC351+1 >300 >300 >300 >300 >300 >300 >300 SWC352+1 >300 >300 >300 >300 >300 >300 >300 SWC353+1 >300 >300 >300 >300 >300 >300 >300 SWC354+1 >300 >300 >300 >300 >300 >300 >300 SWC355+1 >300 >300 >300 >300 >300 >300 >300 SWC356+1 >300 >300 >300 >300 >300 >300 >300 SWC357+1 >300 >300 >300 >300 >300 >300 >300 SWC358+1 >300 >300 >300 >300 >300 >300 >300 SWC359+1 >300 >300 >300 >300 >300 >300 >300 SWC360+1 >300 >300 >300 >300 >300 >300 >300 SWC361+1 >300 >300 >300 >300 >300 >300 >300 SWC362+1 >300 >300 >300 >300 >300 >300 >300 SWC363+1 >300 >300 >300 >300 >300 >300 >300 SWC364+1 >300 >300 >300 >300 >300 >300 >300 SWC365+1 >300 >300 >300 >300 >300 >300 >300 SWC366+1 >300 >300 >300 >300 >300 >300 >300 SWC367+1 >300 >300 >300 >300 >300 >300 >300 SWC368+1 >300 >300 >300 >300 >300 >300 >300 SWC369+1 >300 >300 >300 >300 >300 >300 >300 SWC370+1 >300 >300 >300 >300 >300 >300 >300 SWC371+1 >300 >300 >300 >300 >300 >300 >300 SWC372+1 >300 >300 >300 >300 >300 >300 >300 SWC373+1 >300 >300 >300 >300 >300 >300 >300 SWC374+1 >300 >300 >300 >300 >300 >300 >300 SWC375+1 >300 >300 >300 >300 >300 >300 >300 SWC376+1 >300 >300 >300 >300 >300 >300 >300 SWC377+1 >300 >300 >300 >300 >300 >300 >300 SWC378+1 >300 >300 stack >300 >300 >300 >300 SWC379+1 >300 >300 >300 >300 >300 >300 >300 SWC380+1 >300 >300 >300 >300 >300 >300 >300 SWC381+1 >300 >300 >300 >300 >300 >300 >300 SWC382+1 >300 >300 >300 >300 >300 >300 >300 SWC383+1 >300 >300 >300 >300 >300 >300 >300 SWC384+1 >300 >300 >300 >300 >300 >300 >300 SWC385+1 >300 >300 >300 >300 >300 >300 >300 SWC386+1 >300 >300 >300 >300 >300 >300 >300 SWC387+1 >300 >300 >300 >300 >300 >300 >300 SWC388+1 >300 >300 >300 >300 >300 >300 >300 SWC389+1 >300 >300 stack >300 >300 >300 >300 SWC390+1 >300 >300 >300 >300 >300 >300 >300 SWC391+1 >300 >300 >300 >300 >300 >300 >300 SWC392+1 >300 >300 >300 >300 >300 >300 >300 SWC393+1 >300 >300 >300 >300 >300 >300 >300 SWC394+1 >300 >300 >300 >300 >300 >300 >300 SWC395+1 >300 >300 stack >300 >300 >300 >300 SWC396+1 >300 >300 >300 >300 >300 >300 >300 SWC397+1 >300 >300 >300 >300 >300 >300 >300 SWC398+1 >300 >300 >300 >300 >300 >300 >300 SWC399+1 >300 >300 stack >300 >300 >300 >300 SWC400+1 >300 >300 >300 >300 >300 >300 >300 SWC401+1 >300 >300 >300 >300 >300 >300 >300 SWC402+1 >300 >300 stack >300 >300 >300 >300 SWC403+1 >300 >300 >300 >300 >300 >300 >300 SWC404+1 >300 >300 >300 >300 >300 >300 >300 SWC405+1 >300 >300 >300 >300 >300 >300 >300 SWC406+1 >300 >300 >300 >300 >300 >300 >300 SWC407+1 >300 >300 >300 >300 >300 >300 >300 SWC408+1 >300 >300 >300 >300 >300 >300 >300 SWC409+1 >300 >300 >300 >300 >300 >300 >300 SWC410+1 >300 >300 >300 >300 >300 >300 >300 SWC411+1 >300 >300 >300 >300 >300 >300 >300 SWC412+1 >300 >300 stack >300 >300 >300 >300 SWC413+1 >300 >300 >300 >300 >300 >300 >300 SWC414+1 >300 >300 stack >300 >300 >300 >300 SWC415+1 >300 >300 >300 >300 >300 >300 >300 SWC416+1 >300 >300 >300 >300 >300 >300 >300 SWC417+1 >300 >300 >300 >300 >300 >300 >300 SWC418+1 >300 >300 >300 >300 >300 >300 >300 SWC419+1 >300 >300 stack >300 >300 >300 >300 SWC420+1 >300 >300 stack >300 >300 >300 >300 SWC421+1 >300 >300 >300 >300 >300 >300 >300 SWC422+1 >300 >300 >300 >300 >300 >300 >300 SWV011+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SWV014+1 >300 >300 stack >300 >300 >300 >300 SYN001+1 >300 (<0.01) (<0.01) >300 >300 (<0.01) (0.01) (<0.01) (0.02) SYN007+1.014 >300 (<0.01) (<0.01) >300 >300 stack stack stack >300 SYN036+1 >300 <0.01 <0.01 0.37 >300 >300 >300 SYN036+2 >300 >300 >300 >300 >300 >300 >300 SYN040+1 >300 (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.05) SYN041+1 0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 <0.01 0.02 SYN044+1 jtbug <0.01 <0.01 <0.01 <0.01 0.29 1.12 <0.01 0.02 SYN045+1 <0.01 <0.01 <0.01 <0.01 <0.01 >300 >300 <0.01 0.02 SYN046+1 >300 (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.02) SYN047+1 >300 (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.03) SYN048+1 >300 >300 >300 >300 >300 (<0.01) (0.02) SYN049+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN050+1 <0.01 <0.01 <0.01 0.21 <0.01 0.01 <0.01 SYN051+1 >300 >300 >300 >300 >300 >300 >300 SYN052+1 >300 <0.01 <0.01 <0.01 <0.01 0.03 0.01 SYN053+1 >300 >300 stack >300 >300 >300 >300 SYN054+1 >300 >300 stack >300 >300 >300 >300 SYN055+1 0.02 <0.01 <0.01 152.36 <0.01 0.01 <0.01 SYN056+1 >300 <0.01 <0.01 >300 0.02 >300 >300 SYN057+1 >300 <0.01 <0.01 >300 <0.01 0.01 0.01 SYN058+1 0.04 <0.01 <0.01 0.05 0.01 <0.01 0.01 SYN059+1 0.62 <0.01 <0.01 <0.01 <0.01 >300 >300 SYN060+1 >300 >300 >300 >300 >300 >300 >300 SYN061+1 <0.01 <0.01 <0.01 0.01 <0.01 0.01 <0.01 SYN062+1 0.13 <0.01 <0.01 >300 <0.01 <0.01 <0.01 SYN063+1 >300 >300 stack >300 >300 >300 >300 SYN064+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN065+1 0.01 <0.01 <0.01 >300 0.01 0.01 0.01 SYN066+1 >300 >300 stack >300 >300 >300 >300 SYN067+1 >300 >300 >300 >300 >300 >300 >300 SYN068+1 0.01 <0.01 <0.01 5.09 <0.01 0.01 <0.01 SYN069+1 0.12 0.01 <0.01 >300 0.05 0.01 <0.01 SYN070+1 >300 >300 >300 >300 >300 >300 >300 SYN071+1 >300 2.73 0.01 >300 >300 38.53 >300 SYN072+1 >300 >300 stack >300 >300 >300 >300 SYN073+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN074+1 >300 >300 stack >300 >300 >300 >300 SYN075+1 >300 >300 stack >300 >300 >300 >300 SYN076+1 >300 >300 stack >300 >300 >300 >300 SYN077+1 >300 >300 stack >300 >300 >300 >300 SYN078+1 0.15 >300 0.3 >300 >300 >300 >300 SYN079+1 0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN080+1 0.24 5.92 0.01 0.75 >300 0.01 0.01 SYN081+1 >300 >300 stack >300 >300 >300 >300 SYN082+1 0.01 <0.01 <0.01 <0.01 <0.01 0.05 0.03 SYN083+1 >300 >300 segmf >300 >300 <0.01 0.02 SYN084+1 >300 >300 stack >300 >300 >300 >300 SYN315+1 >300 >300 >300 >300 >300 >300 >300 SYN317+1 >300 >300 >300 >300 >300 >300 >300 SYN318+1 >300 >300 stack >300 >300 (<0.01) (0.01) SYN319+1 >300 >300 >300 >300 >300 (0.01) (0.01) SYN321+1 0.02 <0.01 <0.01 <0.01 <0.01 0.04 0.06 SYN323+1 <0.01 <0.01 <0.01 0.04 <0.01 <0.01 <0.01 SYN325+1 >300 >300 >300 >300 >300 (0.01) (<0.01) SYN326+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN327+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN328+1 >300 >300 >300 >300 >300 (<0.01) (0.02) SYN331+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN332+1 >300 >300 >300 >300 >300 >300 >300 SYN333+1 >300 >300 >300 >300 >300 (0.01) (<0.01) SYN334+1 >300 >300 >300 >300 >300 >300 >300 SYN336+1 >300 >300 stack >300 >300 (0.01) (<0.01) SYN338+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN339+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN340+1 >300 >300 >300 >300 >300 (0.01) (<0.01) SYN341+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN343+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN345+1 >300 >300 stack >300 >300 (0.01) (0.02) SYN346+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN347+1 >300 >300 stack >300 >300 >300 >300 SYN349+1 >300 >300 >300 >300 >300 >300 >300 SYN350+1 >300 >300 stack >300 >300 (<0.01) (0.01) SYN351+1 >300 >300 stack >300 >300 (0.02) (<0.01) SYN352+1 >300 >300 stack >300 >300 (0.01) (0.01) SYN353+1 >300 >300 stack >300 >300 (0.01) (0.03) SYN354+1 >300 >300 stack >300 >300 >300 >300 SYN355+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN356+1 >300 <0.01 <0.01 0.65 <0.01 <0.01 <0.01 SYN357+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 SYN358+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.02 <0.01 SYN359+1 0.01 <0.01 <0.01 >300 <0.01 0.01 0.02 SYN360+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN361+1 0.01 <0.01 <0.01 >300 <0.01 <0.01 <0.01 SYN362+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN363+1 <0.01 <0.01 <0.01 0.04 <0.01 <0.01 0.02 SYN364+1 0.38 >300 0.11 >300 >300 <0.01 0.01 SYN365+1 4.26 >300 stack 16.54 >300 0.01 0.01 SYN366+1 0.17 <0.01 <0.01 2.48 <0.01 0.01 0.01 SYN367+1 0.07 <0.01 0.01 0.01 <0.01 <0.01 <0.01 SYN368+1 >300 >300 >300 >300 >300 (0.01) (<0.01) SYN369+1 >300 >300 stack >300 >300 (0.01) (0.01) SYN370+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN371+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN372+1 >300 >300 stack >300 >300 (<0.01) (0.01) SYN373+1 >300 >300 >300 >300 >300 >300 >300 SYN374+1 >300 <0.01 <0.01 0.01 <0.01 >300 >300 SYN375+1 0.51 <0.01 <0.01 <0.01 <0.01 >300 >300 SYN376+1 >300 >300 stack >300 >300 >300 >300 SYN377+1 0.04 <0.01 <0.01 <0.01 <0.01 >300 >300 SYN378+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN379+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 SYN380+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN381+1 15.67 <0.01 <0.01 3.49 <0.01 0.01 0.01 SYN382+1 0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SYN383+1 >300 >300 >300 >300 >300 (<0.01) (<0.01) SYN384+1 >300 >300 stack >300 >300 (0.01) (<0.01) SYN385+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN386+1 0.14 0.07 <0.01 >300 <0.01 <0.01 0.02 SYN387+1 (<0.01) (<0.01) (<0.01) (<0.01) (<0.01) (<0.01) (0.01) (<0.01) (0.02) SYN388+1 >300 (<0.01) (<0.01) >300 >300 (<0.01) (<0.01) (<0.01) (0.02) SYN389+1 jtbug (<0.01) (<0.01) >300 >300 (<0.01) (0.01) (<0.01) (0.02) SYN390+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 <0.01 0.03 SYN391+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.02 SYN392+1 >300 (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.02) SYN393+1 jtbug (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.02) SYN394+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN395+1 0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN396+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN397+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SYN398+1 0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SYN399+1 0.11 <0.01 <0.01 0.01 <0.01 0.02 0.01 SYN400+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN401+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN402+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN403+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN404+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN405+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SYN406+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 SYN407+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN408+1 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 SYN409+1 0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 SYN410+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN411+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN412+1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 SYN413+1 0.02 <0.01 <0.01 0.02 <0.01 0.01 0.01 SYN415+1 >300 >300 0.08 >300 >300 >300 >300 SYN416+1 (<0.01) (<0.01) (<0.01) (<0.01) (<0.01) (0.01) (<0.01) (<0.01) (0.02) SYN417+1 >300 >300 stack >300 >300 >300 >300 SYN436+1 >300 >300 >300 stack >300 >300 >300 SYN439+1 >300 >300 >300 stack >300 >300 >300 SYN440+1 >300 >300 >300 stack >300 >300 >300 SYN442+1 >300 >300 >300 stack >300 >300 >300 SYN443+1 >300 >300 >300 stack >300 >300 >300 SYN444+1 >300 >300 >300 stack >300 >300 >300 SYN445+1 >300 >300 >300 stack >300 >300 >300 SYN447+1 >300 >300 >300 stack stack >300 >300 SYN448+1 >300 >300 >300 stack >300 >300 >300 SYN450+1 >300 >300 >300 stack >300 >300 >300 SYN451+1 >300 >300 >300 stack >300 >300 >300 SYN452+1 >300 >300 >300 stack >300 >300 >300 SYN454+1 >300 >300 >300 stack >300 >300 >300 SYN455+1 >300 >300 >300 stack >300 >300 >300 SYN457+1 >300 >300 >300 stack >300 >300 >300 SYN458+1 >300 >300 >300 stack >300 >300 >300 SYN459+1 >300 >300 >300 stack >300 >300 >300 SYN460+1 >300 >300 >300 stack >300 >300 >300 SYN461+1 >300 >300 >300 stack >300 >300 >300 SYN462+1 >300 >300 >300 stack >300 >300 >300 SYN465+1 >300 >300 >300 stack >300 >300 >300 SYN466+1 >300 >300 >300 stack >300 >300 >300 SYN467+1 >300 >300 >300 stack >300 >300 >300 SYN468+1 >300 >300 >300 stack >300 >300 >300 SYN469+1 >300 >300 >300 stack >300 >300 >300 SYN470+1 >300 >300 >300 stack >300 >300 >300 SYN471+1 >300 >300 >300 stack >300 >300 >300 SYN472+1 >300 >300 >300 stack >300 >300 >300 SYN473+1 >300 >300 >300 stack >300 >300 >300 SYN474+1 >300 >300 >300 stack >300 >300 >300 SYN475+1 >300 >300 >300 stack >300 >300 >300 SYN476+1 >300 >300 >300 stack >300 >300 >300 SYN477+1 >300 >300 >300 stack >300 >300 >300 SYN478+1 >300 >300 >300 stack >300 >300 >300 SYN479+1 >300 >300 >300 stack >300 >300 >300 SYN480+1 >300 >300 >300 stack >300 >300 >300 SYN481+1 >300 >300 >300 stack >300 >300 >300 SYN482+1 >300 >300 >300 stack >300 >300 >300 SYN483+1 >300 >300 >300 stack >300 >300 >300 SYN484+1 >300 >300 >300 stack >300 >300 >300 SYN485+1 >300 >300 >300 stack >300 >300 >300 SYN486+1 >300 >300 >300 stack >300 >300 >300 SYN487+1 >300 >300 >300 stack >300 >300 >300 SYN488+1 >300 >300 >300 stack >300 >300 >300 SYN489+1 >300 >300 >300 stack >300 >300 >300 SYN498+1 >300 >300 >300 stack >300 >300 >300 SYN499+1 >300 >300 >300 stack >300 >300 >300 SYN500+1 >300 >300 >300 stack >300 >300 >300 SYN501+1 >300 >300 >300 stack >300 >300 >300 SYN502+1 >300 >300 >300 stack >300 >300 >300 SYN503+1 >300 >300 >300 stack >300 >300 >300 SYN504+1 >300 >300 >300 stack >300 >300 >300 SYN505+1 >300 >300 >300 stack >300 >300 >300 SYN506+1 >300 >300 >300 stack >300 >300 >300 SYN507+1 >300 >300 >300 stack >300 >300 >300 SYN508+1 >300 >300 >300 stack >300 >300 >300 SYN509+1 >300 >300 >300 stack >300 >300 >300 SYN510+1 >300 >300 >300 stack >300 >300 >300 SYN511+1 >300 >300 >300 stack >300 >300 >300 SYN512+1 >300 >300 >300 stack >300 >300 >300 SYN548+1 >300 >300 stack >300 >300 >300 >300 SYN549+1 >300 0.16 <0.01 >300 >300 >300 >300 SYN550+1 >300 >300 0.01 >300 >300 >300 >300 SYN551+1 >300 >300 stack >300 >300 >300 >300 SYN551+2 >300 >300 segmf >300 >300 >300 >300 SYN551+3 >300 >300 stack >300 >300 >300 >300 SYN721+1 <0.01 <0.01 <0.01 15.26 <0.01 <0.01 <0.01 SYN722+1 >300 0.01 <0.01 0.02 >300 <0.01 0.01 SYN723+1 >300 >300 >300 >300 >300 stack stack SYN724+1 0.02 <0.01 <0.01 <0.01 <0.01 >300 >300 SYN726+1 >300 >300 stack >300 >300 >300 >300 SYN727+1 <0.01 <0.01 <0.01 0.04 <0.01 <0.01 <0.01 SYN728+1 0.17 >300 0.11 >300 >300 <0.01 <0.01 SYN729+1 4.26 >300 stack 16.54 >300 0.01 <0.01 SYN730+1 >300 >300 >300 >300 >300 (<0.01) (0.01) SYN731+1 >300 >300 >300 >300 >300 (0.01) (<0.01) SYN732+1 >300 >300 stack >300 >300 (<0.01) (<0.01) SYN733+1 0.01 <0.01 0.01 <0.01 <0.01 <0.01 0.01 2. ILTP-Benchmark ----------------- formula provers first order propositional JProver ft ileanSeP ileanTAP ileanCoP ileanCoP_pt LJT STRIP Prolog C intuit. valid ft1.1 0.05 1.11 <0.01 0.01 <0.01 0.02 0.01 ft1.2 0.13 >300 <0.01 0.28 0.01 0.06 0.02 ft1.3 0.41 >300 >300 90.1 0.01 0.18 0.09 ft1.4 0.04 <0.01 <0.01 <0.01 <0.01 0.01 0.01 ft1.5 0.14 >300 0.02 8.06 <0.01 0.07 0.02 ft1.6 0.36 >300 0.18 4.04 0.01 0.16 0.07 ft1.7 0.02 1.67 0.01 0.01 <0.01 0.01 <0.01 ft1.8 0.09 >300 stack 3.81 <0.01 0.01 <0.01 ft2.1 >300 121.43 0.02 >300 >300 <0.01 <0.01 ft2.2 >300 >300 0.03 >300 >300 <0.01 0.01 ft2.3 >300 >300 0.06 >300 >300 0.01 <0.01 ft2.4 >300 >300 0.7 >300 >300 <0.01 <0.01 ft4.1 >300 >300 0.13 >300 >300 0.02 0.01 ft4.2 >300 >300 0.15 >300 >300 0.02 <0.01 ft4.3 >300 >300 0.15 >300 >300 0.02 0.01 ft5.1 0.03 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 ft5.2 9.45 <0.01 <0.01 <0.01 0.03 0.03 0.04 ft5.3 >300 0.09 0.01 0.01 1.0 1.19 1.27 ft6.1 0.01 <0.01 <0.01 <0.01 <0.01 0.05 0.05 ft6.2 0.07 <0.01 <0.01 >300 0.01 <0.01 0.02 ft6.3 1.42 <0.01 <0.01 10.06 0.01 0.02 <0.01 ft6.4 0.07 <0.01 <0.01 <0.01 <0.01 0.62 0.01 ft6.5 0.05 <0.01 <0.01 <0.01 <0.01 >300 >300 ft6.6 0.01 <0.01 <0.01 0.02 <0.01 0.01 <0.01 ft6.7 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 ft6.8 0.02 <0.01 <0.01 0.01 <0.01 0.01 0.01 ft6.9 <0.01 <0.01 <0.01 7.65 <0.01 0.01 0.01 ft6.10 0.01 <0.01 <0.01 0.09 0.01 <0.01 <0.01 ft6.11 0.02 <0.01 <0.01 0.1 <0.01 0.01 <0.01 ft6.12 >300 <0.01 <0.01 3.03 1.44 <0.01 0.01 ft6.13 >300 <0.01 <0.01 1.44 0.06 <0.01 <0.01 ft6.14 0.12 0.01 <0.01 0.04 <0.01 0.07 0.03 ft6.15 0.75 <0.01 <0.01 >300 0.66 0.01 0.02 ft7a 0.01 <0.01 <0.01 <0.01 <0.01 0.02 0.02 ft7b 0.13 <0.01 <0.01 <0.01 <0.01 0.05 0.02 ft7c 6.44 0.28 0.04 0.05 0.13 0.14 0.08 ft7d >300 42.88 19.2 3.94 11.64 0.44 0.23 ft8.1 0.06 <0.01 <0.01 0.01 0.01 <0.01 0.01 ft8.2 0.01 <0.01 <0.01 0.22 <0.01 <0.01 0.01 sch_ax <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 0.03 sch_notnot <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 <0.01 0.03 sch_notnot2 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 <0.01 0.02 sch_implies <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 <0.01 0.02 sch_mult2 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 <0.01 0.02 sch_mult3 0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.02 sch_mult4 0.04 <0.01 <0.01 0.02 0.65 0.01 <0.01 <0.01 0.02 sch_jens_prop 0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 <0.01 0.02 sch_prop_n1 0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 <0.01 0.02 sch_prop_n2 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 0.02 sch_prop_n3 0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.02 sch_prop_n4 0.04 0.01 <0.01 0.02 0.01 0.02 <0.01 <0.01 0.02 sch_ax_all <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 sch_all_exst <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 sch_jens_fo 0.33 <0.01 <0.01 0.06 0.01 0.01 0.02 sch_subst <0.01 <0.01 <0.01 0.01 <0.01 0.01 <0.01 sch_fv2 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 0.01 sch_jens_fo_fv 0.24 <0.01 <0.01 0.07 <0.01 <0.01 0.02 sch_fun1 1.05 <0.01 <0.01 0.07 0.01 <0.01 <0.01 sch_fun2 0.04 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 sch_fo_n1 0.01 <0.01 <0.01 <0.01 <0.01 0.01 <0.01 sch_fo_n2 0.1 >300 <0.01 >300 0.01 0.02 <0.01 sch_fo_n3 3.55 >300 0.02 >300 <0.01 0.02 0.01 sch_fo_n4 98.7 >300 0.61 >300 0.03 <0.01 <0.01 sch_deadlock1 <0.01 <0.01 <0.01 <0.01 <0.01 <0.01 0.01 sch_deadlock2 0.01 2.05 <0.01 >300 0.45 <0.01 <0.01 sch_deadlock3 <0.01 <0.01 <0.01 0.01 0.01 0.01 0.01 sch_deadlock4 0.01 <0.01 <0.01 0.01 0.16 <0.01 0.01 sch_mult_no_rename <0.01 <0.01 <0.01 0.02 <0.01 0.01 <0.01 sch_mult_no_rename2 <0.01 0.01 <0.01 <0.01 0.06 0.01 <0.01 sch_mult_eigen_del 0.01 <0.01 <0.01 0.01 <0.01 <0.01 <0.01 sch_mult_rename 0.01 0.01 <0.01 0.02 <0.01 <0.01 <0.01 sch_agatha 2.47 <0.01 0.01 >300 >300 0.01 <0.01 debruijn_p2 jtbug <0.01 <0.01 0.1 >300 >300 >300 0.01 0.02 debruijn_p6 >300 0.01 <0.01 >300 >300 >300 >300 0.02 0.03 debruijn_p10 >300 0.05 <0.01 >300 >300 >300 >300 0.08 0.08 ph_p2 0.02 <0.01 0.01 <0.01 0.01 <0.01 0.01 <0.01 0.02 ph_p6 >300 18.24 0.46 stack stack 9.09 3.56 stack 12.07 ph_p10 >300 >300 >300 stack stack stack stack stack stack con_p2 0.02 <0.01 <0.01 <0.01 >300 0.01 0.02 <0.01 0.03 con_p6 jtbug <0.01 <0.01 >300 >300 >300 >300 <0.01 0.02 con_p10 jtbug <0.01 <0.01 >300 >300 >300 >300 <0.01 0.02 schwicht_p2 <0.01 <0.01 <0.01 0.01 <0.01 <0.01 <0.01 <0.01 0.02 schwicht_p6 >300 <0.01 <0.01 >300 >300 <0.01 <0.01 <0.01 0.02 schwicht_p10 >300 <0.01 <0.01 >300 >300 0.03 0.03 <0.01 0.02 kk_p2 0.35 <0.01 <0.01 <0.01 0.01 >300 >300 <0.01 0.02 kk_p6 >300 0.5 0.05 0.31 >300 >300 >300 <0.01 0.02 kk_p10 >300 >300 >300 289.53 >300 >300 >300 <0.01 0.75 equiv_p2 0.02 <0.01 <0.01 <0.01 <0.01 >300 >300 <0.01 0.02 equiv_p6 jtbug <0.01 <0.01 >300 >300 >300 stack >300 0.02 equiv_p10 >300 163.8 18.96 >300 >300 >300 stack >300 0.06 intuit. invalid debruijn_n2 jtbug (<0.01) (<0.01) >300 >300 >300 >300 (0.01) (0.03) debruijn_n6 jtbug (21.9) (2.83) >300 >300 >300 >300 >300 >300 debruijn_n10 jtbug >300 >300 >300 >300 >300 >300 >300 >300 ph_n2 >300 (<0.01) (<0.01) >300 >300 (0.01) (0.01) (<0.01) (0.02) ph_n6 >300 (0.2) (<0.01) >300 stack >300 >300 (2.57) (0.24) ph_n10 >300 >300 (0.03) stack stack >300 >300 stack stack con_n2 jtbug (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.02) con_n6 jtbug (0.06) (0.01) >300 >300 >300 >300 (0.06) (0.04) con_n10 jtbug >300 (83.89) >300 >300 >300 >300 >300 (141.17) schwicht_n2 >300 (<0.01) (<0.01) >300 >300 (0.01) (0.01) (<0.01) (0.02) schwicht_n6 >300 (<0.01) (<0.01) >300 >300 (0.02) (<0.01) (<0.01) (0.02) schwicht_n10 >300 (<0.01) (<0.01) >300 >300 (0.1) (0.05) (<0.01) (0.02) kk_n2 jtbug (<0.01) (<0.01) >300 >300 (<0.01) (<0.01) (<0.01) (0.02) kk_n6 >300 >300 >300 >300 >300 (0.07) (0.07) (4.88) (0.15) kk_n10 >300 >300 >300 >300 >300 (7.46) (7.4) >300 >300 equiv_n2 >300 (<0.01) (<0.01) >300 >300 >300 >300 (<0.01) (0.02) equiv_n6 jtbug (<0.01) (<0.01) >300 >300 >300 stack (2.9) (0.02) equiv_n10 >300 (<0.01) (<0.01) >300 >300 >300 stack >300 (0.06)