%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : SYO581+1 : TPTP v7.5.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 01:53:25 EDT 2022 % Result : CounterSatisfiable 0.47s 0.68s % Output : Model 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.11 % Problem : SYO581+1 : TPTP v7.5.0. Released v5.5.0. % 0.12/0.12 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 0.12/0.33 % Computer : n011.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Sun Mar 13 22:23:41 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.12/0.34 % 0.12/0.34 % 0.12/0.34 Defaulting to tptp format. % 0.12/0.34 Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.12/0.37 % 0.12/0.39 % 0.12/0.39 % 0.18/0.45 Proving ... % 0.18/0.45 % 0.47/0.68 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.47/0.68 % 0.47/0.68 START OF MODEL (DIG): % 0.47/0.70 b48_buttercup10007(_0) % 0.47/0.70 b48_buttercup10013(sK450) % 0.47/0.70 b48_buttercup10013(sK18) % 0.47/0.70 b48_buttercup10013(sK20) % 0.47/0.70 b48_buttercup10013(sK212) % 0.47/0.70 b48_buttercup10013(sK384) % 0.47/0.70 b48_buttercup10013(sK360) % 0.47/0.70 b48_buttercup10013(sK19) % 0.47/0.70 b48_buttercup10013(sK449) % 0.47/0.70 b48_buttercup10019(sK360) % 0.47/0.70 b48_buttercup10021(sK450) % 0.47/0.70 b48_buttercup10022(sK449) % 0.47/0.70 b48_buttercup10024(sK426) % 0.47/0.70 b48_buttercup10024(sK430) % 0.47/0.70 b48_buttercup10024(sK16) % 0.47/0.70 b48_buttercup10024(sK260) % 0.47/0.70 b48_buttercup10024(sK21) % 0.47/0.70 b48_buttercup10024(sK116) % 0.47/0.70 b48_buttercup10024(sK229) % 0.47/0.70 b48_buttercup10024(sK432) % 0.47/0.70 b48_buttercup10024(sK261) % 0.47/0.70 b48_buttercup10024(sK453) % 0.47/0.70 b48_buttercup10024(sK246) % 0.47/0.70 b48_buttercup10029(sK229) % 0.47/0.70 b48_buttercup10029(sK453) % 0.47/0.70 b48_buttercup10031(sK432) % 0.47/0.70 b48_buttercup10031(sK246) % 0.47/0.70 b48_buttercup10034(sK430) % 0.47/0.70 b48_buttercup10034(sK261) % 0.47/0.70 b48_buttercup10035(sK247) % 0.47/0.70 b48_buttercup10035(sK431) % 0.47/0.70 b48_buttercup10043(sK303) % 0.47/0.70 b48_buttercup10043(sK156) % 0.47/0.70 b48_buttercup10045(sK300) % 0.47/0.70 b48_buttercup10045(sK158) % 0.47/0.70 b48_buttercup10046(sK487) % 0.47/0.70 b48_buttercup10046(sK160) % 0.47/0.70 b48_buttercup10046(sK161) % 0.47/0.70 b48_buttercup10046(sK302) % 0.47/0.70 b48_buttercup10046(sK489) % 0.47/0.70 b48_buttercup10046(sK282) % 0.47/0.70 b48_buttercup10050(sK489) % 0.47/0.70 b48_buttercup10050(sK282) % 0.47/0.70 b48_buttercup10052(sK487) % 0.47/0.70 b48_buttercup10052(sK160) % 0.47/0.70 b48_buttercup10054(sK354) % 0.47/0.70 b48_buttercup10054(sK494) % 0.47/0.70 b48_buttercup10054(sK62) % 0.47/0.70 b48_buttercup10054(sK66) % 0.47/0.70 b48_buttercup10054(sK195) % 0.47/0.70 b48_buttercup10054(sK176) % 0.47/0.70 b48_buttercup10054(sK328) % 0.47/0.70 b48_buttercup10054(sK332) % 0.47/0.70 b48_buttercup10054(sK352) % 0.47/0.70 b48_buttercup10054(sK245) % 0.47/0.70 b48_buttercup10054(sK485) % 0.47/0.70 b48_buttercup10054(sK278) % 0.47/0.70 b48_buttercup10054(sK329) % 0.47/0.70 b48_buttercup10054(sK65) % 0.47/0.70 b48_buttercup10054(sK194) % 0.47/0.70 b48_buttercup10058(sK494) % 0.47/0.70 b48_buttercup10058(sK195) % 0.47/0.70 b48_buttercup10065(sK354) % 0.47/0.70 b48_buttercup10065(sK245) % 0.47/0.70 b48_buttercup10068(sK352) % 0.47/0.70 b48_buttercup10070(sK328) % 0.47/0.70 b48_buttercup10072(sK176) % 0.47/0.70 b48_buttercup10072(sK329) % 0.47/0.70 b48_buttercup10075(sK332) % 0.47/0.70 b48_buttercup10076(sK172) % 0.47/0.70 b48_buttercup10076(sK333) % 0.47/0.70 b48_buttercup10082(sK391) % 0.47/0.70 b48_buttercup10082(sK157) % 0.47/0.70 b48_buttercup10085(sK191) % 0.47/0.70 b48_buttercup10085(sK421) % 0.47/0.70 b48_buttercup10086(sK404) % 0.47/0.70 b48_buttercup10086(sK241) % 0.47/0.70 b48_buttercup10092(sK397) % 0.47/0.70 b48_buttercup10092(sK222) % 0.47/0.70 b48_buttercup10098(sK27) % 0.47/0.70 b48_buttercup10098(sK47) % 0.47/0.70 b48_buttercup10098(sK102) % 0.47/0.70 b48_buttercup10098(sK403) % 0.47/0.70 b48_buttercup10098(sK42) % 0.47/0.70 b48_buttercup10098(sK60) % 0.47/0.70 b48_buttercup10098(sK54) % 0.47/0.70 b48_buttercup10098(sK455) % 0.47/0.70 b48_buttercup10098(sK37) % 0.47/0.70 b48_buttercup10098(sK456) % 0.47/0.70 b48_buttercup10098(sK31) % 0.47/0.70 b48_buttercup10098(sK262) % 0.47/0.70 b48_buttercup10098(sK482) % 0.47/0.70 b48_buttercup10098(sK96) % 0.47/0.70 b48_buttercup10098(sK186) % 0.47/0.70 b48_buttercup10098(sK483) % 0.47/0.70 b48_buttercup10098(sK97) % 0.47/0.70 b48_buttercup10098(sK458) % 0.47/0.70 b48_buttercup10098(sK272) % 0.47/0.70 b48_buttercup10098(sK106) % 0.47/0.70 b48_buttercup10098(sK38) % 0.47/0.70 b48_buttercup10098(sK98) % 0.47/0.70 b48_buttercup10098(sK459) % 0.47/0.70 b48_buttercup10098(sK205) % 0.47/0.70 b48_buttercup10098(sK58) % 0.47/0.70 b48_buttercup10098(sK52) % 0.47/0.70 b48_buttercup10098(sK460) % 0.47/0.70 b48_buttercup10102(sK455) % 0.47/0.70 b48_buttercup10104(sK456) % 0.47/0.70 b48_buttercup10107(sK458) % 0.47/0.70 b48_buttercup10107(sK272) % 0.47/0.70 b48_buttercup10108(sK459) % 0.47/0.70 b48_buttercup10109(sK96) % 0.47/0.70 b48_buttercup10109(sK458) % 0.47/0.70 b48_buttercup10109(sK482) % 0.47/0.70 b48_buttercup10109(sK97) % 0.47/0.70 b48_buttercup10109(sK272) % 0.47/0.70 b48_buttercup10109(sK455) % 0.47/0.70 b48_buttercup10109(sK459) % 0.47/0.70 b48_buttercup10109(sK483) % 0.47/0.70 b48_buttercup10109(sK460) % 0.47/0.70 b48_buttercup10109(sK205) % 0.47/0.70 b48_buttercup10109(sK27) % 0.47/0.70 b48_buttercup10109(sK98) % 0.47/0.70 b48_buttercup10109(sK456) % 0.47/0.70 b48_buttercup10109(sK31) % 0.47/0.70 b48_buttercup10109(sK37) % 0.47/0.70 b48_buttercup10109(sK186) % 0.47/0.70 b48_buttercup10110(sK483) % 0.47/0.70 b48_buttercup10111(sK482) % 0.47/0.70 b48_buttercup10115(sK275) % 0.47/0.70 b48_buttercup10115(sK478) % 0.47/0.70 b48_buttercup10115(sK135) % 0.47/0.70 b48_buttercup10115(sK480) % 0.47/0.70 b48_buttercup10115(sK412) % 0.47/0.70 b48_buttercup10119(sK478) % 0.47/0.70 b48_buttercup10120(sK412) % 0.47/0.70 b48_buttercup10121(sK413) % 0.47/0.70 b48_buttercup10121(sK234) % 0.47/0.70 b48_buttercup10130(sK119) % 0.47/0.70 b48_buttercup10130(sK434) % 0.47/0.70 b48_buttercup10130(sK435) % 0.47/0.70 b48_buttercup10130(sK120) % 0.47/0.70 b48_buttercup10130(sK249) % 0.47/0.70 b48_buttercup10130(sK436) % 0.47/0.70 b48_buttercup10133(sK436) % 0.47/0.70 b48_buttercup10134(sK434) % 0.47/0.70 b48_buttercup10143(sK448) % 0.47/0.70 b48_buttercup10143(sK230) % 0.47/0.70 b48_buttercup10150(sK93) % 0.47/0.70 b48_buttercup10150(sK382) % 0.47/0.70 b48_buttercup10150(sK386) % 0.47/0.70 b48_buttercup10150(sK2) % 0.47/0.70 b48_buttercup10150(sK94) % 0.47/0.70 b48_buttercup10150(sK208) % 0.47/0.70 b48_buttercup10150(sK383) % 0.47/0.70 b48_buttercup10150(sK3) % 0.47/0.70 b48_buttercup10150(sK381) % 0.47/0.70 b48_buttercup10150(sK92) % 0.47/0.70 b48_buttercup10150(sK321) % 0.47/0.70 b48_buttercup10150(sK385) % 0.47/0.70 b48_buttercup10154(sK383) % 0.47/0.70 b48_buttercup10156(sK382) % 0.47/0.70 b48_buttercup10158(sK386) % 0.47/0.70 b48_buttercup10159(sK385) % 0.47/0.70 b48_buttercup10160(sK321) % 0.47/0.70 b48_buttercup10161(sK123) % 0.47/0.70 b48_buttercup10161(sK296) % 0.47/0.70 b48_buttercup10161(sK124) % 0.47/0.70 b48_buttercup10161(sK125) % 0.47/0.70 b48_buttercup10161(sK293) % 0.47/0.70 b48_buttercup10161(sK297) % 0.47/0.70 b48_buttercup10161(sK154) % 0.47/0.70 b48_buttercup10161(sK298) % 0.47/0.70 b48_buttercup10166(sK297) % 0.47/0.70 b48_buttercup10167(sK298) % 0.47/0.70 b48_buttercup10169(sK293) % 0.47/0.70 b48_buttercup10170(sK326) % 0.47/0.70 b48_buttercup10170(sK324) % 0.47/0.70 b48_buttercup10170(sK173) % 0.47/0.70 b48_buttercup10170(sK122) % 0.47/0.70 b48_buttercup10170(sK126) % 0.47/0.70 b48_buttercup10170(sK325) % 0.47/0.70 b48_buttercup10173(sK325) % 0.47/0.70 b48_buttercup10174(sK326) % 0.47/0.70 b48_buttercup10176(sK327) % 0.47/0.70 b48_buttercup10176(sK290) % 0.47/0.70 b48_buttercup10179(sK322) % 0.47/0.70 b48_buttercup10180(sK506) % 0.47/0.70 b48_buttercup10180(sK270) % 0.47/0.70 b48_buttercup10182(sK379) % 0.47/0.70 b48_buttercup10186(sK474) % 0.47/0.70 b48_buttercup10186(sK25) % 0.47/0.70 b48_buttercup10186(sK287) % 0.47/0.70 b48_buttercup10186(sK498) % 0.47/0.70 b48_buttercup10186(sK502) % 0.47/0.70 b48_buttercup10186(sK26) % 0.47/0.70 b48_buttercup10186(sK500) % 0.47/0.70 b48_buttercup10186(sK133) % 0.47/0.70 b48_buttercup10191(sK502) % 0.47/0.70 b48_buttercup10193(sK500) % 0.47/0.70 b48_buttercup10195(sK498) % 0.47/0.70 b48_buttercup10196(sK497) % 0.47/0.70 b48_buttercup10197(sK496) % 0.47/0.70 b48_buttercup10198(sK461) % 0.47/0.70 b48_buttercup10199(sK159) % 0.47/0.70 b48_buttercup10199(sK504) % 0.47/0.70 b48_buttercup10201(sK266) % 0.47/0.70 b48_buttercup10201(sK77) % 0.47/0.70 b48_buttercup10201(sK350) % 0.47/0.70 b48_buttercup10201(sK410) % 0.47/0.70 b48_buttercup10201(sK216) % 0.47/0.70 b48_buttercup10201(sK72) % 0.47/0.70 b48_buttercup10201(sK285) % 0.47/0.70 b48_buttercup10201(sK127) % 0.47/0.70 b48_buttercup10201(sK128) % 0.47/0.70 b48_buttercup10201(sK465) % 0.47/0.70 b48_buttercup10201(sK24) % 0.47/0.70 b48_buttercup10201(sK492) % 0.47/0.70 b48_buttercup10201(sK281) % 0.47/0.70 b48_buttercup10201(sK493) % 0.47/0.70 b48_buttercup10201(sK307) % 0.47/0.70 b48_buttercup10201(sK163) % 0.47/0.70 b48_buttercup10201(sK206) % 0.47/0.70 b48_buttercup10208(sK350) % 0.47/0.70 b48_buttercup10208(sK266) % 0.47/0.70 b48_buttercup10210(sK285) % 0.47/0.70 b48_buttercup10210(sK493) % 0.47/0.70 b48_buttercup10214(sK410) % 0.47/0.70 b48_buttercup10214(sK216) % 0.47/0.70 b48_buttercup10217(sK492) % 0.47/0.70 b48_buttercup10217(sK281) % 0.47/0.70 b48_buttercup10220(sK465) % 0.47/0.70 b48_buttercup10220(sK206) % 0.47/0.70 b48_buttercup10222(sK143) % 0.47/0.70 b48_buttercup10222(sK466) % 0.47/0.70 b48_buttercup10222(sK5) % 0.47/0.70 b48_buttercup10222(sK470) % 0.47/0.70 b48_buttercup10222(sK471) % 0.47/0.70 b48_buttercup10222(sK129) % 0.47/0.70 b48_buttercup10222(sK145) % 0.47/0.70 b48_buttercup10222(sK269) % 0.47/0.70 b48_buttercup10222(sK4) % 0.47/0.70 b48_buttercup10222(sK501) % 0.47/0.70 b48_buttercup10227(sK501) % 0.47/0.70 b48_buttercup10228(sK471) % 0.47/0.70 b48_buttercup10229(sK470) % 0.47/0.70 b48_buttercup10231(sK184) % 0.47/0.70 b48_buttercup10231(sK177) % 0.47/0.70 b48_buttercup10231(sK257) % 0.47/0.70 b48_buttercup10231(sK441) % 0.47/0.70 b48_buttercup10240(sK239) % 0.47/0.70 b48_buttercup10240(sK423) % 0.47/0.70 b48_buttercup10247(sK418) % 0.47/0.70 b48_buttercup10248(sK415) % 0.47/0.70 b48_buttercup10248(sK225) % 0.47/0.70 b48_buttercup10253(sK227) % 0.47/0.70 b48_buttercup10253(sK451) % 0.47/0.70 b48_buttercup10260(sK299) % 0.47/0.70 b48_buttercup10261(sK377) % 0.47/0.70 b48_buttercup10266(sK375) % 0.47/0.70 b48_buttercup10266(sK495) % 0.47/0.70 b48_buttercup10266(sK376) % 0.47/0.70 b48_buttercup10267(sK375) % 0.47/0.70 b48_buttercup10268(sK495) % 0.47/0.70 b48_buttercup10269(sK370) % 0.47/0.70 b48_buttercup10269(sK196) % 0.47/0.70 b48_buttercup10271(sK407) % 0.47/0.70 b48_buttercup10271(sK347) % 0.47/0.70 b48_buttercup10272(sK368) % 0.47/0.70 b48_buttercup10273(sK347) % 0.47/0.70 b48_buttercup10274(sK342) % 0.47/0.70 b48_buttercup10274(sK343) % 0.47/0.70 b48_buttercup10274(sK344) % 0.47/0.70 b48_buttercup10274(sK340) % 0.47/0.70 b48_buttercup10274(sK345) % 0.47/0.70 b48_buttercup10275(sK345) % 0.47/0.70 b48_buttercup10276(sK342) % 0.47/0.70 b48_buttercup10277(sK343) % 0.47/0.70 b48_buttercup10278(sK340) % 0.47/0.70 b48_buttercup10279(sK113) % 0.47/0.70 b48_buttercup10279(sK323) % 0.47/0.70 b48_buttercup10279(sK150) % 0.47/0.70 b48_buttercup10283(sK151) % 0.47/0.70 b48_buttercup10283(sK292) % 0.47/0.70 b48_buttercup10289(sK295) % 0.47/0.70 b48_buttercup10289(sK188) % 0.47/0.70 b48_buttercup10289(sK91) % 0.47/0.70 b48_buttercup10289(sK150) % 0.47/0.70 b48_buttercup10290(sK476) % 0.47/0.70 b48_buttercup10290(sK153) % 0.47/0.70 b48_buttercup10291(sK475) % 0.47/0.70 b48_buttercup10291(sK276) % 0.47/0.70 b48_buttercup10291(sK273) % 0.47/0.70 b48_buttercup10291(sK477) % 0.47/0.70 b48_buttercup10291(sK274) % 0.47/0.70 b48_buttercup10291(sK389) % 0.47/0.70 b48_buttercup10294(sK475) % 0.47/0.70 b48_buttercup10294(sK273) % 0.47/0.70 b48_buttercup10299(sK276) % 0.47/0.70 b48_buttercup10299(sK389) % 0.47/0.70 b48_buttercup10300(sK1) % 0.47/0.70 b48_buttercup10300(sK510) % 0.47/0.70 b48_buttercup10300(sK371) % 0.47/0.70 b48_buttercup10300(sK121) % 0.47/0.70 b48_buttercup10300(sK508) % 0.47/0.70 b48_buttercup10300(sK512) % 0.47/0.70 b48_buttercup10300(sK481) % 0.47/0.70 b48_buttercup10300(sK0) % 0.47/0.70 b48_buttercup10300(sK202) % 0.47/0.70 b48_buttercup10300(sK373) % 0.47/0.70 b48_buttercup10305(sK512) % 0.47/0.70 b48_buttercup10305(sK373) % 0.47/0.70 b48_buttercup10307(sK371) % 0.47/0.70 b48_buttercup10308(sK508) % 0.47/0.70 b48_buttercup10309(sK221) % 0.47/0.70 b48_buttercup10309(sK457) % 0.47/0.70 b48_buttercup10313(sK398) % 0.47/0.70 b48_buttercup10313(sK283) % 0.47/0.70 b48_buttercup10313(sK402) % 0.47/0.70 b48_buttercup10313(sK114) % 0.47/0.70 b48_buttercup10313(sK416) % 0.47/0.70 b48_buttercup10318(sK402) % 0.47/0.70 b48_buttercup10320(sK416) % 0.47/0.70 b48_buttercup10322(sK237) % 0.47/0.70 b48_buttercup10322(sK417) % 0.47/0.70 b48_buttercup10326(sK414) % 0.47/0.70 b48_buttercup10326(sK235) % 0.47/0.70 b48_buttercup10332(sK304) % 0.47/0.70 b48_buttercup10332(sK250) % 0.47/0.70 b48_buttercup10334(sK438) % 0.47/0.70 b48_buttercup10334(sK468) % 0.47/0.70 b48_buttercup10334(sK472) % 0.47/0.70 b48_buttercup10334(sK473) % 0.47/0.70 b48_buttercup10334(sK505) % 0.47/0.70 b48_buttercup10343(sK473) % 0.47/0.70 b48_buttercup10344(sK472) % 0.47/0.70 b48_buttercup10348(sK468) % 0.47/0.70 b48_buttercup10352(sK505) % 0.47/0.70 b48_buttercup10353(sK289) % 0.47/0.70 b48_buttercup10353(sK429) % 0.47/0.70 b48_buttercup10358(sK316) % 0.47/0.70 b48_buttercup10359(sK168) % 0.47/0.70 b48_buttercup10359(sK437) % 0.47/0.70 b48_buttercup10361(sK288) % 0.47/0.70 b48_buttercup10361(sK314) % 0.47/0.70 b48_buttercup10362(sK315) % 0.47/0.70 b48_buttercup10365(sK317) % 0.47/0.70 b48_buttercup10367(sK338) % 0.47/0.70 b48_buttercup10367(sK183) % 0.47/0.70 b48_buttercup10367(sK319) % 0.47/0.70 b48_buttercup10367(sK164) % 0.47/0.70 b48_buttercup10367(sK336) % 0.47/0.70 b48_buttercup10367(sK181) % 0.47/0.70 b48_buttercup10367(sK185) % 0.47/0.70 b48_buttercup10367(sK341) % 0.47/0.70 b48_buttercup10370(sK185) % 0.47/0.70 b48_buttercup10370(sK341) % 0.47/0.70 b48_buttercup10374(sK338) % 0.47/0.70 b48_buttercup10374(sK181) % 0.47/0.70 b48_buttercup10377(sK183) % 0.47/0.70 b48_buttercup10377(sK336) % 0.47/0.70 b48_buttercup10378(sK193) % 0.47/0.70 b48_buttercup10378(sK349) % 0.47/0.70 b48_buttercup10381(sK223) % 0.47/0.70 b48_buttercup10381(sK355) % 0.47/0.70 b48_buttercup10383(sK192) % 0.47/0.70 b48_buttercup10383(sK353) % 0.47/0.70 b48_buttercup10386(sK356) % 0.47/0.70 b48_buttercup10386(sK190) % 0.47/0.70 b48_buttercup10394(sK388) % 0.47/0.70 b48_buttercup10394(sK213) % 0.47/0.70 b48_buttercup10398(sK387) % 0.47/0.70 b48_buttercup10402(sK243) % 0.47/0.70 b48_buttercup10402(sK240) % 0.47/0.70 b48_buttercup10402(sK428) % 0.47/0.70 b48_buttercup10402(sK424) % 0.47/0.70 b48_buttercup10402(sK242) % 0.47/0.70 b48_buttercup10402(sK405) % 0.47/0.70 b48_buttercup10405(sK243) % 0.47/0.70 b48_buttercup10405(sK424) % 0.47/0.70 b48_buttercup10410(sK240) % 0.47/0.70 b48_buttercup10410(sK405) % 0.47/0.70 b48_buttercup10411(sK406) % 0.47/0.70 b48_buttercup10411(sK226) % 0.47/0.70 b48_buttercup10417(sK147) % 0.47/0.70 b48_buttercup10417(sK199) % 0.47/0.70 b48_buttercup10417(sK462) % 0.47/0.70 b48_buttercup10417(sK447) % 0.47/0.70 b48_buttercup10417(sK363) % 0.47/0.70 b48_buttercup10417(sK491) % 0.47/0.70 b48_buttercup10417(sK149) % 0.47/0.70 b48_buttercup10417(sK67) % 0.47/0.70 b48_buttercup10417(sK320) % 0.47/0.70 b48_buttercup10417(sK420) % 0.47/0.70 b48_buttercup10417(sK68) % 0.47/0.70 b48_buttercup10417(sK198) % 0.47/0.70 b48_buttercup10417(sK361) % 0.47/0.70 b48_buttercup10420(sK469) % 0.47/0.70 b48_buttercup10421(sK320) % 0.47/0.70 b48_buttercup10421(sK198) % 0.47/0.70 b48_buttercup10422(sK467) % 0.47/0.70 b48_buttercup10427(sK256) % 0.47/0.70 b48_buttercup10427(sK464) % 0.47/0.70 b48_buttercup10433(sK445) % 0.47/0.70 b48_buttercup10434(sK446) % 0.47/0.70 b48_buttercup10434(sK259) % 0.47/0.70 b48_buttercup10440(sK110) % 0.47/0.70 b48_buttercup10440(sK311) % 0.47/0.70 b48_buttercup10440(sK308) % 0.47/0.70 b48_buttercup10440(sK108) % 0.47/0.70 b48_buttercup10440(sK309) % 0.47/0.70 b48_buttercup10441(sK308) % 0.47/0.70 b48_buttercup10442(sK311) % 0.47/0.70 b48_buttercup10443(sK310) % 0.47/0.70 b48_buttercup10443(sK166) % 0.47/0.70 b48_buttercup10446(sK367) % 0.47/0.70 b48_buttercup10446(sK10) % 0.47/0.70 b48_buttercup10446(sK479) % 0.47/0.70 b48_buttercup10446(sK6) % 0.47/0.70 b48_buttercup10446(sK200) % 0.47/0.70 b48_buttercup10446(sK454) % 0.47/0.70 b48_buttercup10446(sK11) % 0.47/0.70 b48_buttercup10446(sK286) % 0.47/0.70 b48_buttercup10446(sK201) % 0.47/0.70 b48_buttercup10446(sK84) % 0.47/0.70 b48_buttercup10446(sK7) % 0.47/0.70 b48_buttercup10446(sK313) % 0.47/0.70 b48_buttercup10446(sK228) % 0.47/0.70 b48_buttercup10446(sK499) % 0.47/0.70 b48_buttercup10446(sK79) % 0.47/0.70 b48_buttercup10446(sK364) % 0.47/0.70 b48_buttercup10446(sK8) % 0.47/0.70 b48_buttercup10446(sK365) % 0.47/0.70 b48_buttercup10446(sK366) % 0.47/0.70 b48_buttercup10446(sK248) % 0.47/0.70 b48_buttercup10446(sK9) % 0.47/0.70 b48_buttercup10450(sK433) % 0.47/0.70 b48_buttercup10451(sK499) % 0.47/0.70 b48_buttercup10451(sK286) % 0.47/0.70 b48_buttercup10454(sK479) % 0.47/0.70 b48_buttercup10456(sK454) % 0.47/0.70 b48_buttercup10458(sK12) % 0.47/0.70 b48_buttercup10458(sK10) % 0.47/0.70 b48_buttercup10458(sK83) % 0.47/0.70 b48_buttercup10458(sK503) % 0.47/0.70 b48_buttercup10458(sK248) % 0.47/0.70 b48_buttercup10460(sK200) % 0.47/0.70 b48_buttercup10460(sK364) % 0.47/0.70 b48_buttercup10465(sK367) % 0.47/0.70 b48_buttercup10466(sK366) % 0.47/0.70 b48_buttercup10467(sK365) % 0.47/0.70 b48_buttercup10469(sK179) % 0.47/0.70 b48_buttercup10469(sK359) % 0.47/0.70 b48_buttercup10471(sK335) % 0.47/0.70 b48_buttercup10471(sK180) % 0.47/0.70 b48_buttercup10474(sK334) % 0.47/0.70 b48_buttercup10474(sK374) % 0.47/0.70 b48_buttercup10474(sK100) % 0.47/0.70 b48_buttercup10474(sK331) % 0.47/0.70 b48_buttercup10474(sK351) % 0.47/0.70 b48_buttercup10474(sK411) % 0.47/0.70 b48_buttercup10474(sK22) % 0.47/0.70 b48_buttercup10474(sK236) % 0.47/0.70 b48_buttercup10474(sK23) % 0.47/0.70 b48_buttercup10474(sK189) % 0.47/0.70 b48_buttercup10474(sK178) % 0.47/0.70 b48_buttercup10474(sK509) % 0.47/0.70 b48_buttercup10474(sK99) % 0.47/0.70 b48_buttercup10478(sK331) % 0.47/0.70 b48_buttercup10479(sK236) % 0.47/0.70 b48_buttercup10479(sK509) % 0.47/0.70 b48_buttercup10483(sK351) % 0.47/0.70 b48_buttercup10487(sK411) % 0.47/0.70 b48_buttercup10489(sK374) % 0.47/0.70 b48_buttercup10490(sK215) % 0.47/0.70 b48_buttercup10490(sK393) % 0.47/0.70 b48_buttercup10493(sK392) % 0.47/0.70 b48_buttercup10493(sK214) % 0.47/0.70 b48_buttercup10496(sK390) % 0.47/0.70 b48_buttercup10496(sK219) % 0.47/0.70 b48_buttercup10502(sK175) % 0.47/0.70 b48_buttercup10502(sK294) % 0.47/0.70 b48_buttercup10507(sK330) % 0.47/0.70 b48_buttercup10507(sK197) % 0.47/0.70 b48_buttercup10512(sK358) % 0.47/0.70 b48_buttercup10512(sK362) % 0.47/0.70 b48_buttercup10512(sK357) % 0.47/0.70 b48_buttercup10513(sK357) % 0.47/0.70 b48_buttercup10514(sK362) % 0.47/0.70 b48_buttercup10515(sK462) % 0.47/0.70 b48_buttercup10515(sK363) % 0.47/0.70 b48_buttercup10515(sK491) % 0.47/0.70 b48_buttercup10515(sK420) % 0.47/0.70 b48_buttercup10515(sK361) % 0.47/0.70 b48_buttercup10518(sK462) % 0.47/0.70 b48_buttercup10519(sK363) % 0.47/0.70 b48_buttercup10520(sK491) % 0.47/0.70 b48_buttercup10521(sK420) % 0.47/0.70 b48_buttercup10522(sK490) % 0.47/0.70 b48_buttercup10526(sK280) % 0.47/0.70 b48_buttercup10526(sK425) % 0.47/0.70 b48_buttercup10530(sK306) % 0.47/0.70 b48_buttercup10531(sK305) % 0.47/0.70 b48_buttercup10531(sK162) % 0.47/0.70 b48_buttercup10538(sK155) % 0.47/0.70 b48_buttercup10538(sK301) % 0.47/0.70 b48_buttercup10541(sK439) % 0.47/0.70 b48_buttercup10541(sK252) % 0.47/0.70 b48_buttercup10542(sK442) % 0.47/0.70 b48_buttercup10542(sK255) % 0.47/0.70 b48_buttercup10542(sK443) % 0.47/0.70 b48_buttercup10542(sK440) % 0.47/0.70 b48_buttercup10542(sK253) % 0.47/0.70 b48_buttercup10542(sK254) % 0.47/0.70 b48_buttercup10545(sK442) % 0.47/0.70 b48_buttercup10545(sK254) % 0.47/0.70 b48_buttercup10548(sK255) % 0.47/0.70 b48_buttercup10548(sK443) % 0.47/0.70 b48_buttercup10549(sK444) % 0.47/0.70 b48_buttercup10549(sK265) % 0.47/0.70 b48_buttercup10552(sK263) % 0.47/0.70 b48_buttercup10552(sK463) % 0.47/0.70 b48_buttercup10552(sK264) % 0.47/0.70 b48_buttercup10552(sK399) % 0.47/0.70 b48_buttercup10552(sK401) % 0.47/0.70 b48_buttercup10561(sK401) % 0.47/0.70 b48_buttercup10562(sK263) % 0.47/0.70 b48_buttercup10562(sK399) % 0.47/0.70 b48_buttercup10563(sK422) % 0.47/0.70 b48_buttercup10563(sK419) % 0.47/0.70 b48_buttercup10563(sK507) % 0.47/0.70 b48_buttercup10563(sK400) % 0.47/0.70 b48_buttercup10563(sK117) % 0.47/0.70 b48_buttercup10563(sK136) % 0.47/0.70 b48_buttercup10563(sK217) % 0.47/0.70 b48_buttercup10563(sK118) % 0.47/0.70 b48_buttercup10570(sK422) % 0.47/0.70 b48_buttercup10572(sK507) % 0.47/0.70 b48_buttercup10574(sK419) % 0.47/0.70 b48_buttercup10575(sK244) % 0.47/0.70 b48_buttercup10575(sK380) % 0.47/0.70 b48_buttercup10579(sK427) % 0.47/0.70 b48_buttercup10579(sK238) % 0.47/0.70 b48_buttercup10582(sK187) % 0.47/0.70 b48_buttercup10582(sK348) % 0.47/0.70 b48_buttercup10589(sK378) % 0.47/0.70 b48_buttercup10589(sK203) % 0.47/0.70 b48_buttercup10589(sK339) % 0.47/0.70 b48_buttercup10589(sK204) % 0.47/0.70 b48_buttercup10589(sK396) % 0.47/0.70 b48_buttercup10589(sK218) % 0.47/0.70 b48_buttercup10596(sK378) % 0.47/0.70 b48_buttercup10596(sK203) % 0.47/0.70 b48_buttercup10604(sK396) % 0.47/0.70 b48_buttercup10604(sK218) % 0.53/0.70 b48_buttercup10605(sK271) % 0.53/0.70 b48_buttercup10605(sK395) % 0.53/0.70 b48_buttercup10606(sK394) % 0.53/0.70 b48_buttercup10609(sK211) % 0.53/0.70 b48_buttercup10609(sK408) % 0.53/0.70 b48_buttercup10612(sK369) % 0.53/0.70 b48_buttercup10616(sK207) % 0.53/0.70 b48_buttercup10616(sK372) % 0.53/0.70 b48_buttercup10624(sK337) % 0.53/0.70 b48_buttercup10624(sK182) % 0.53/0.70 b48_buttercup10629(sK346) % 0.53/0.70 b48_buttercup10629(sK167) % 0.53/0.70 b48_buttercup10632(sK318) % 0.53/0.70 b48_buttercup10632(sK486) % 0.53/0.70 b48_buttercup10632(sK171) % 0.53/0.70 b48_buttercup10632(sK279) % 0.53/0.70 b48_buttercup10632(sK312) % 0.53/0.70 b48_buttercup10632(sK165) % 0.53/0.70 b48_buttercup10632(sK452) % 0.53/0.70 b48_buttercup10632(sK209) % 0.53/0.70 b48_buttercup10636(sK452) % 0.53/0.70 b48_buttercup10636(sK209) % 0.53/0.70 b48_buttercup10638(sK318) % 0.53/0.70 b48_buttercup10638(sK171) % 0.53/0.70 b48_buttercup10640(sK486) % 0.53/0.70 b48_buttercup10640(sK279) % 0.53/0.70 b48_buttercup10642(sK484) % 0.53/0.70 b48_buttercup10642(sK277) % 0.53/0.70 b48_buttercup10646(sK488) % 0.53/0.70 k04_buttercup10000(sK231) % 0.53/0.70 k04_buttercup10004(sK232) % 0.53/0.70 k04_buttercup10012(sK463) % 0.53/0.70 k04_buttercup10012(sK177) % 0.53/0.70 k04_buttercup10012(sK320) % 0.53/0.70 k04_buttercup10012(sK464) % 0.53/0.70 k04_buttercup10012(sK178) % 0.53/0.70 k04_buttercup10012(sK321) % 0.53/0.70 k04_buttercup10012(sK465) % 0.53/0.70 k04_buttercup10012(sK179) % 0.53/0.70 k04_buttercup10012(sK322) % 0.53/0.70 k04_buttercup10012(sK180) % 0.53/0.70 k04_buttercup10012(sK467) % 0.53/0.70 k04_buttercup10012(sK181) % 0.53/0.70 k04_buttercup10012(sK324) % 0.53/0.70 k04_buttercup10012(sK72) % 0.53/0.70 k04_buttercup10012(sK468) % 0.53/0.70 k04_buttercup10012(sK182) % 0.53/0.70 k04_buttercup10012(sK325) % 0.53/0.70 k04_buttercup10012(sK183) % 0.53/0.70 k04_buttercup10012(sK326) % 0.53/0.70 k04_buttercup10012(sK470) % 0.53/0.70 k04_buttercup10012(sK184) % 0.53/0.70 k04_buttercup10012(sK327) % 0.53/0.70 k04_buttercup10012(sK471) % 0.53/0.70 k04_buttercup10012(sK185) % 0.53/0.70 k04_buttercup10012(sK328) % 0.53/0.70 k04_buttercup10012(sK472) % 0.53/0.70 k04_buttercup10012(sK186) % 0.53/0.70 k04_buttercup10012(sK329) % 0.53/0.70 k04_buttercup10012(sK473) % 0.53/0.70 k04_buttercup10012(sK187) % 0.53/0.70 k04_buttercup10012(sK330) % 0.53/0.70 k04_buttercup10012(sK474) % 0.53/0.70 k04_buttercup10012(sK188) % 0.53/0.70 k04_buttercup10012(sK331) % 0.53/0.70 k04_buttercup10012(sK77) % 0.53/0.70 k04_buttercup10012(sK475) % 0.53/0.70 k04_buttercup10012(sK189) % 0.53/0.70 k04_buttercup10012(sK332) % 0.53/0.70 k04_buttercup10012(sK190) % 0.53/0.70 k04_buttercup10012(sK333) % 0.53/0.70 k04_buttercup10012(sK477) % 0.53/0.70 k04_buttercup10012(sK191) % 0.53/0.70 k04_buttercup10012(sK334) % 0.53/0.70 k04_buttercup10012(sK478) % 0.53/0.70 k04_buttercup10012(sK192) % 0.53/0.70 k04_buttercup10012(sK335) % 0.53/0.70 k04_buttercup10012(sK479) % 0.53/0.70 k04_buttercup10012(sK193) % 0.53/0.70 k04_buttercup10012(sK336) % 0.53/0.70 k04_buttercup10012(sK79) % 0.53/0.70 k04_buttercup10012(sK480) % 0.53/0.70 k04_buttercup10012(sK194) % 0.53/0.70 k04_buttercup10012(sK337) % 0.53/0.70 k04_buttercup10012(sK481) % 0.53/0.70 k04_buttercup10012(sK195) % 0.53/0.70 k04_buttercup10012(sK338) % 0.53/0.70 k04_buttercup10012(sK482) % 0.53/0.70 k04_buttercup10012(sK196) % 0.53/0.70 k04_buttercup10012(sK339) % 0.53/0.70 k04_buttercup10012(sK80) % 0.53/0.70 k04_buttercup10012(sK483) % 0.53/0.70 k04_buttercup10012(sK197) % 0.53/0.70 k04_buttercup10012(sK81) % 0.53/0.70 k04_buttercup10012(sK484) % 0.53/0.70 k04_buttercup10012(sK198) % 0.53/0.70 k04_buttercup10012(sK341) % 0.53/0.70 k04_buttercup10012(sK82) % 0.53/0.70 k04_buttercup10012(sK485) % 0.53/0.70 k04_buttercup10012(sK199) % 0.53/0.70 k04_buttercup10012(sK486) % 0.53/0.70 k04_buttercup10012(sK200) % 0.53/0.70 k04_buttercup10012(sK84) % 0.53/0.70 k04_buttercup10012(sK487) % 0.53/0.70 k04_buttercup10012(sK201) % 0.53/0.70 k04_buttercup10012(sK202) % 0.53/0.70 k04_buttercup10012(sK489) % 0.53/0.70 k04_buttercup10012(sK203) % 0.53/0.70 k04_buttercup10012(sK346) % 0.53/0.70 k04_buttercup10012(sK204) % 0.53/0.70 k04_buttercup10012(sK491) % 0.53/0.70 k04_buttercup10012(sK205) % 0.53/0.70 k04_buttercup10012(sK348) % 0.53/0.70 k04_buttercup10012(sK492) % 0.53/0.70 k04_buttercup10012(sK206) % 0.53/0.70 k04_buttercup10012(sK349) % 0.53/0.70 k04_buttercup10012(sK493) % 0.53/0.70 k04_buttercup10012(sK207) % 0.53/0.70 k04_buttercup10012(sK350) % 0.53/0.70 k04_buttercup10012(sK494) % 0.53/0.70 k04_buttercup10012(sK208) % 0.53/0.70 k04_buttercup10012(sK351) % 0.53/0.70 k04_buttercup10012(sK91) % 0.53/0.70 k04_buttercup10012(sK209) % 0.53/0.70 k04_buttercup10012(sK352) % 0.53/0.70 k04_buttercup10012(sK210) % 0.53/0.70 k04_buttercup10012(sK353) % 0.53/0.70 k04_buttercup10012(sK211) % 0.53/0.70 k04_buttercup10012(sK354) % 0.53/0.70 k04_buttercup10012(sK498) % 0.53/0.70 k04_buttercup10012(sK212) % 0.53/0.70 k04_buttercup10012(sK355) % 0.53/0.70 k04_buttercup10012(sK499) % 0.53/0.70 k04_buttercup10012(sK213) % 0.53/0.70 k04_buttercup10012(sK356) % 0.53/0.70 k04_buttercup10012(sK92) % 0.53/0.70 k04_buttercup10012(sK500) % 0.53/0.70 k04_buttercup10012(sK214) % 0.53/0.70 k04_buttercup10012(sK93) % 0.53/0.70 k04_buttercup10012(sK501) % 0.53/0.70 k04_buttercup10012(sK215) % 0.53/0.70 k04_buttercup10012(sK94) % 0.53/0.70 k04_buttercup10012(sK502) % 0.53/0.70 k04_buttercup10012(sK216) % 0.53/0.70 k04_buttercup10012(sK359) % 0.53/0.70 k04_buttercup10012(sK217) % 0.53/0.70 k04_buttercup10012(sK360) % 0.53/0.70 k04_buttercup10012(sK504) % 0.53/0.70 k04_buttercup10012(sK218) % 0.53/0.70 k04_buttercup10012(sK361) % 0.53/0.70 k04_buttercup10012(sK96) % 0.53/0.70 k04_buttercup10012(sK505) % 0.53/0.70 k04_buttercup10012(sK219) % 0.53/0.70 k04_buttercup10012(sK97) % 0.53/0.70 k04_buttercup10012(sK506) % 0.53/0.70 k04_buttercup10012(sK363) % 0.53/0.70 k04_buttercup10012(sK98) % 0.53/0.70 k04_buttercup10012(sK507) % 0.53/0.70 k04_buttercup10012(sK221) % 0.53/0.70 k04_buttercup10012(sK364) % 0.53/0.70 k04_buttercup10012(sK99) % 0.53/0.70 k04_buttercup10012(sK508) % 0.53/0.70 k04_buttercup10012(sK222) % 0.53/0.70 k04_buttercup10012(sK365) % 0.53/0.70 k04_buttercup10012(sK100) % 0.53/0.70 k04_buttercup10012(sK509) % 0.53/0.70 k04_buttercup10012(sK223) % 0.53/0.70 k04_buttercup10012(sK366) % 0.53/0.70 k04_buttercup10012(sK101) % 0.53/0.70 k04_buttercup10012(sK510) % 0.53/0.70 k04_buttercup10012(sK224) % 0.53/0.70 k04_buttercup10012(sK367) % 0.53/0.70 k04_buttercup10012(sK225) % 0.53/0.70 k04_buttercup10012(sK0) % 0.53/0.70 k04_buttercup10012(sK512) % 0.53/0.70 k04_buttercup10012(sK226) % 0.53/0.70 k04_buttercup10012(sK1) % 0.53/0.70 k04_buttercup10012(sK2) % 0.53/0.70 k04_buttercup10012(sK370) % 0.53/0.70 k04_buttercup10012(sK228) % 0.53/0.70 k04_buttercup10012(sK3) % 0.53/0.70 k04_buttercup10012(sK371) % 0.53/0.70 k04_buttercup10012(sK106) % 0.53/0.70 k04_buttercup10012(sK229) % 0.53/0.70 k04_buttercup10012(sK4) % 0.53/0.70 k04_buttercup10012(sK372) % 0.53/0.70 k04_buttercup10012(sK230) % 0.53/0.70 k04_buttercup10012(sK5) % 0.53/0.70 k04_buttercup10012(sK373) % 0.53/0.70 k04_buttercup10012(sK374) % 0.53/0.70 k04_buttercup10012(sK6) % 0.53/0.70 k04_buttercup10012(sK108) % 0.53/0.70 k04_buttercup10012(sK233) % 0.53/0.70 k04_buttercup10012(sK109) % 0.53/0.70 k04_buttercup10012(sK234) % 0.53/0.70 k04_buttercup10012(sK7) % 0.53/0.70 k04_buttercup10012(sK235) % 0.53/0.70 k04_buttercup10012(sK378) % 0.53/0.70 k04_buttercup10012(sK111) % 0.53/0.70 k04_buttercup10012(sK236) % 0.53/0.70 k04_buttercup10012(sK8) % 0.53/0.70 k04_buttercup10012(sK237) % 0.53/0.70 k04_buttercup10012(sK380) % 0.53/0.70 k04_buttercup10012(sK238) % 0.53/0.70 k04_buttercup10012(sK9) % 0.53/0.70 k04_buttercup10012(sK381) % 0.53/0.70 k04_buttercup10012(sK112) % 0.53/0.70 k04_buttercup10012(sK239) % 0.53/0.70 k04_buttercup10012(sK10) % 0.53/0.70 k04_buttercup10012(sK382) % 0.53/0.70 k04_buttercup10012(sK240) % 0.53/0.70 k04_buttercup10012(sK383) % 0.53/0.70 k04_buttercup10012(sK114) % 0.53/0.70 k04_buttercup10012(sK241) % 0.53/0.70 k04_buttercup10012(sK11) % 0.53/0.70 k04_buttercup10012(sK384) % 0.53/0.70 k04_buttercup10012(sK115) % 0.53/0.70 k04_buttercup10012(sK242) % 0.53/0.70 k04_buttercup10012(sK385) % 0.53/0.70 k04_buttercup10012(sK243) % 0.53/0.70 k04_buttercup10012(sK386) % 0.53/0.70 k04_buttercup10012(sK244) % 0.53/0.70 k04_buttercup10012(sK387) % 0.53/0.70 k04_buttercup10012(sK245) % 0.53/0.70 k04_buttercup10012(sK388) % 0.53/0.70 k04_buttercup10012(sK246) % 0.53/0.70 k04_buttercup10012(sK16) % 0.53/0.70 k04_buttercup10012(sK389) % 0.53/0.70 k04_buttercup10012(sK247) % 0.53/0.70 k04_buttercup10012(sK390) % 0.53/0.70 k04_buttercup10012(sK248) % 0.53/0.70 k04_buttercup10012(sK391) % 0.53/0.70 k04_buttercup10012(sK117) % 0.53/0.70 k04_buttercup10012(sK249) % 0.53/0.70 k04_buttercup10012(sK392) % 0.53/0.70 k04_buttercup10012(sK118) % 0.53/0.70 k04_buttercup10012(sK250) % 0.53/0.70 k04_buttercup10012(sK393) % 0.53/0.70 k04_buttercup10012(sK119) % 0.53/0.70 k04_buttercup10012(sK251) % 0.53/0.70 k04_buttercup10012(sK18) % 0.53/0.70 k04_buttercup10012(sK120) % 0.53/0.70 k04_buttercup10012(sK395) % 0.53/0.70 k04_buttercup10012(sK121) % 0.53/0.70 k04_buttercup10012(sK253) % 0.53/0.70 k04_buttercup10012(sK19) % 0.53/0.70 k04_buttercup10012(sK396) % 0.53/0.70 k04_buttercup10012(sK122) % 0.53/0.70 k04_buttercup10012(sK254) % 0.53/0.70 k04_buttercup10012(sK397) % 0.53/0.70 k04_buttercup10012(sK123) % 0.53/0.70 k04_buttercup10012(sK255) % 0.53/0.70 k04_buttercup10012(sK20) % 0.53/0.70 k04_buttercup10012(sK398) % 0.53/0.70 k04_buttercup10012(sK124) % 0.53/0.70 k04_buttercup10012(sK256) % 0.53/0.70 k04_buttercup10012(sK399) % 0.53/0.70 k04_buttercup10012(sK125) % 0.53/0.70 k04_buttercup10012(sK257) % 0.53/0.70 k04_buttercup10012(sK400) % 0.53/0.70 k04_buttercup10012(sK126) % 0.53/0.70 k04_buttercup10012(sK258) % 0.53/0.70 k04_buttercup10012(sK401) % 0.53/0.70 k04_buttercup10012(sK259) % 0.53/0.70 k04_buttercup10012(sK22) % 0.53/0.70 k04_buttercup10012(sK402) % 0.53/0.70 k04_buttercup10012(sK260) % 0.53/0.70 k04_buttercup10012(sK23) % 0.53/0.70 k04_buttercup10012(sK261) % 0.53/0.70 k04_buttercup10012(sK404) % 0.53/0.70 k04_buttercup10012(sK262) % 0.53/0.70 k04_buttercup10012(sK25) % 0.53/0.70 k04_buttercup10012(sK405) % 0.53/0.70 k04_buttercup10012(sK263) % 0.53/0.70 k04_buttercup10012(sK26) % 0.53/0.70 k04_buttercup10012(sK406) % 0.53/0.70 k04_buttercup10012(sK264) % 0.53/0.70 k04_buttercup10012(sK27) % 0.53/0.70 k04_buttercup10012(sK265) % 0.53/0.70 k04_buttercup10012(sK408) % 0.53/0.70 k04_buttercup10012(sK130) % 0.53/0.70 k04_buttercup10012(sK266) % 0.53/0.70 k04_buttercup10012(sK267) % 0.53/0.70 k04_buttercup10012(sK410) % 0.53/0.70 k04_buttercup10012(sK268) % 0.53/0.70 k04_buttercup10012(sK31) % 0.53/0.70 k04_buttercup10012(sK411) % 0.53/0.70 k04_buttercup10012(sK269) % 0.53/0.70 k04_buttercup10012(sK412) % 0.53/0.70 k04_buttercup10012(sK270) % 0.53/0.70 k04_buttercup10012(sK413) % 0.53/0.70 k04_buttercup10012(sK271) % 0.53/0.70 k04_buttercup10012(sK414) % 0.53/0.70 k04_buttercup10012(sK272) % 0.53/0.70 k04_buttercup10012(sK415) % 0.53/0.70 k04_buttercup10012(sK273) % 0.53/0.70 k04_buttercup10012(sK416) % 0.53/0.70 k04_buttercup10012(sK133) % 0.53/0.70 k04_buttercup10012(sK274) % 0.53/0.70 k04_buttercup10012(sK417) % 0.53/0.70 k04_buttercup10012(sK134) % 0.53/0.70 k04_buttercup10012(sK275) % 0.53/0.70 k04_buttercup10012(sK135) % 0.53/0.70 k04_buttercup10012(sK276) % 0.53/0.70 k04_buttercup10012(sK37) % 0.53/0.70 k04_buttercup10012(sK419) % 0.53/0.70 k04_buttercup10012(sK136) % 0.53/0.70 k04_buttercup10012(sK277) % 0.53/0.70 k04_buttercup10012(sK420) % 0.53/0.70 k04_buttercup10012(sK278) % 0.53/0.70 k04_buttercup10012(sK421) % 0.53/0.70 k04_buttercup10012(sK137) % 0.53/0.70 k04_buttercup10012(sK279) % 0.53/0.70 k04_buttercup10012(sK422) % 0.53/0.70 k04_buttercup10012(sK280) % 0.53/0.70 k04_buttercup10012(sK423) % 0.53/0.70 k04_buttercup10012(sK281) % 0.53/0.70 k04_buttercup10012(sK424) % 0.53/0.70 k04_buttercup10012(sK282) % 0.53/0.70 k04_buttercup10012(sK425) % 0.53/0.70 k04_buttercup10012(sK283) % 0.53/0.70 k04_buttercup10012(sK42) % 0.53/0.70 k04_buttercup10012(sK284) % 0.53/0.70 k04_buttercup10012(sK427) % 0.53/0.70 k04_buttercup10012(sK285) % 0.53/0.70 k04_buttercup10012(sK428) % 0.53/0.70 k04_buttercup10012(sK286) % 0.53/0.70 k04_buttercup10012(sK143) % 0.53/0.70 k04_buttercup10012(sK429) % 0.53/0.70 k04_buttercup10012(sK287) % 0.53/0.70 k04_buttercup10012(sK144) % 0.53/0.70 k04_buttercup10012(sK430) % 0.53/0.70 k04_buttercup10012(sK431) % 0.53/0.70 k04_buttercup10012(sK289) % 0.53/0.70 k04_buttercup10012(sK146) % 0.53/0.70 k04_buttercup10012(sK432) % 0.53/0.70 k04_buttercup10012(sK290) % 0.53/0.70 k04_buttercup10012(sK47) % 0.53/0.70 k04_buttercup10012(sK147) % 0.53/0.70 k04_buttercup10012(sK291) % 0.53/0.70 k04_buttercup10012(sK148) % 0.53/0.70 k04_buttercup10012(sK434) % 0.53/0.70 k04_buttercup10012(sK435) % 0.53/0.70 k04_buttercup10012(sK293) % 0.53/0.70 k04_buttercup10012(sK150) % 0.53/0.70 k04_buttercup10012(sK436) % 0.53/0.70 k04_buttercup10012(sK294) % 0.53/0.70 k04_buttercup10012(sK295) % 0.53/0.70 k04_buttercup10012(sK152) % 0.53/0.70 k04_buttercup10012(sK438) % 0.53/0.70 k04_buttercup10012(sK296) % 0.53/0.70 k04_buttercup10012(sK297) % 0.53/0.70 k04_buttercup10012(sK52) % 0.53/0.70 k04_buttercup10012(sK154) % 0.53/0.70 k04_buttercup10012(sK440) % 0.53/0.70 k04_buttercup10012(sK298) % 0.53/0.70 k04_buttercup10012(sK441) % 0.53/0.70 k04_buttercup10012(sK442) % 0.53/0.70 k04_buttercup10012(sK157) % 0.53/0.70 k04_buttercup10012(sK443) % 0.53/0.70 k04_buttercup10012(sK54) % 0.53/0.70 k04_buttercup10012(sK444) % 0.53/0.70 k04_buttercup10012(sK302) % 0.53/0.70 k04_buttercup10012(sK159) % 0.53/0.70 k04_buttercup10012(sK160) % 0.53/0.70 k04_buttercup10012(sK446) % 0.53/0.70 k04_buttercup10012(sK304) % 0.53/0.70 k04_buttercup10012(sK161) % 0.53/0.70 k04_buttercup10012(sK305) % 0.53/0.70 k04_buttercup10012(sK58) % 0.53/0.70 k04_buttercup10012(sK162) % 0.53/0.70 k04_buttercup10012(sK448) % 0.53/0.70 k04_buttercup10012(sK163) % 0.53/0.70 k04_buttercup10012(sK449) % 0.53/0.70 k04_buttercup10012(sK164) % 0.53/0.70 k04_buttercup10012(sK450) % 0.53/0.70 k04_buttercup10012(sK308) % 0.53/0.70 k04_buttercup10012(sK165) % 0.53/0.70 k04_buttercup10012(sK60) % 0.53/0.70 k04_buttercup10012(sK166) % 0.53/0.70 k04_buttercup10012(sK452) % 0.53/0.70 k04_buttercup10012(sK310) % 0.53/0.70 k04_buttercup10012(sK167) % 0.53/0.70 k04_buttercup10012(sK453) % 0.53/0.70 k04_buttercup10012(sK454) % 0.53/0.70 k04_buttercup10012(sK61) % 0.53/0.70 k04_buttercup10012(sK312) % 0.53/0.70 k04_buttercup10012(sK169) % 0.53/0.70 k04_buttercup10012(sK455) % 0.53/0.70 k04_buttercup10012(sK313) % 0.53/0.70 k04_buttercup10012(sK170) % 0.53/0.70 k04_buttercup10012(sK456) % 0.53/0.70 k04_buttercup10012(sK62) % 0.53/0.70 k04_buttercup10012(sK171) % 0.53/0.70 k04_buttercup10012(sK457) % 0.53/0.70 k04_buttercup10012(sK63) % 0.53/0.70 k04_buttercup10012(sK315) % 0.53/0.70 k04_buttercup10012(sK172) % 0.53/0.70 k04_buttercup10012(sK458) % 0.53/0.70 k04_buttercup10012(sK64) % 0.53/0.70 k04_buttercup10012(sK173) % 0.53/0.70 k04_buttercup10012(sK459) % 0.53/0.70 k04_buttercup10012(sK65) % 0.53/0.70 k04_buttercup10012(sK174) % 0.53/0.70 k04_buttercup10012(sK460) % 0.53/0.70 k04_buttercup10012(sK66) % 0.53/0.70 k04_buttercup10012(sK175) % 0.53/0.70 k04_buttercup10012(sK318) % 0.53/0.70 k04_buttercup10012(sK176) % 0.53/0.70 k04_buttercup10012(sK462) % 0.53/0.70 k04_buttercup10012(sK67) % 0.53/0.70 k04_buttercup10012(sK319) % 0.53/0.70 k04_buttercup10016(sK450) % 0.53/0.70 k04_buttercup10016(sK18) % 0.53/0.70 k04_buttercup10016(sK20) % 0.53/0.70 k04_buttercup10016(sK212) % 0.53/0.70 k04_buttercup10016(sK360) % 0.53/0.70 k04_buttercup10016(sK384) % 0.53/0.70 k04_buttercup10016(sK19) % 0.53/0.70 k04_buttercup10016(sK449) % 0.53/0.70 k04_buttercup10026(sK430) % 0.53/0.70 k04_buttercup10026(sK16) % 0.53/0.70 k04_buttercup10026(sK260) % 0.53/0.70 k04_buttercup10026(sK261) % 0.53/0.70 k04_buttercup10026(sK432) % 0.53/0.70 k04_buttercup10026(sK229) % 0.53/0.70 k04_buttercup10026(sK246) % 0.53/0.70 k04_buttercup10026(sK453) % 0.53/0.70 k04_buttercup10028(sK430) % 0.53/0.70 k04_buttercup10028(sK261) % 0.53/0.70 k04_buttercup10033(sK432) % 0.53/0.70 k04_buttercup10033(sK246) % 0.53/0.70 k04_buttercup10039(sK247) % 0.53/0.70 k04_buttercup10039(sK431) % 0.53/0.70 k04_buttercup10042(sK300) % 0.53/0.70 k04_buttercup10042(sK158) % 0.53/0.70 k04_buttercup10044(sK303) % 0.53/0.70 k04_buttercup10044(sK156) % 0.53/0.70 k04_buttercup10048(sK160) % 0.53/0.70 k04_buttercup10048(sK487) % 0.53/0.70 k04_buttercup10048(sK161) % 0.53/0.70 k04_buttercup10048(sK282) % 0.53/0.70 k04_buttercup10048(sK302) % 0.53/0.70 k04_buttercup10048(sK489) % 0.53/0.70 k04_buttercup10049(sK160) % 0.53/0.70 k04_buttercup10049(sK487) % 0.53/0.70 k04_buttercup10051(sK282) % 0.53/0.70 k04_buttercup10051(sK489) % 0.53/0.70 k04_buttercup10053(sK229) % 0.53/0.70 k04_buttercup10053(sK453) % 0.53/0.70 k04_buttercup10057(sK62) % 0.53/0.70 k04_buttercup10057(sK66) % 0.53/0.70 k04_buttercup10057(sK195) % 0.53/0.70 k04_buttercup10057(sK354) % 0.53/0.70 k04_buttercup10057(sK494) % 0.53/0.70 k04_buttercup10057(sK176) % 0.53/0.70 k04_buttercup10057(sK245) % 0.53/0.70 k04_buttercup10057(sK328) % 0.53/0.70 k04_buttercup10057(sK332) % 0.53/0.70 k04_buttercup10057(sK352) % 0.53/0.70 k04_buttercup10057(sK278) % 0.53/0.70 k04_buttercup10057(sK65) % 0.53/0.70 k04_buttercup10057(sK194) % 0.53/0.70 k04_buttercup10057(sK485) % 0.53/0.70 k04_buttercup10057(sK329) % 0.53/0.70 k04_buttercup10061(sK195) % 0.53/0.70 k04_buttercup10061(sK494) % 0.53/0.70 k04_buttercup10064(sK62) % 0.53/0.70 k04_buttercup10064(sK66) % 0.53/0.70 k04_buttercup10064(sK328) % 0.53/0.70 k04_buttercup10064(sK332) % 0.53/0.70 k04_buttercup10064(sK352) % 0.53/0.70 k04_buttercup10064(sK65) % 0.53/0.70 k04_buttercup10064(sK194) % 0.53/0.70 k04_buttercup10067(sK354) % 0.53/0.70 k04_buttercup10067(sK245) % 0.53/0.70 k04_buttercup10074(sK176) % 0.53/0.70 k04_buttercup10074(sK329) % 0.53/0.70 k04_buttercup10079(sK172) % 0.53/0.70 k04_buttercup10079(sK333) % 0.53/0.70 k04_buttercup10084(sK391) % 0.53/0.70 k04_buttercup10084(sK157) % 0.53/0.70 k04_buttercup10089(sK241) % 0.53/0.70 k04_buttercup10089(sK404) % 0.53/0.70 k04_buttercup10095(sK223) % 0.53/0.70 k04_buttercup10095(sK101) % 0.53/0.70 k04_buttercup10095(sK355) % 0.53/0.70 k04_buttercup10095(sK130) % 0.53/0.70 k04_buttercup10095(sK258) % 0.53/0.70 k04_buttercup10095(sK222) % 0.53/0.70 k04_buttercup10095(sK397) % 0.53/0.70 k04_buttercup10096(sK222) % 0.53/0.70 k04_buttercup10096(sK397) % 0.53/0.70 k04_buttercup10097(sK223) % 0.53/0.70 k04_buttercup10097(sK355) % 0.53/0.70 k04_buttercup10100(sK27) % 0.53/0.70 k04_buttercup10100(sK47) % 0.53/0.70 k04_buttercup10100(sK42) % 0.53/0.70 k04_buttercup10100(sK60) % 0.53/0.70 k04_buttercup10100(sK54) % 0.53/0.70 k04_buttercup10100(sK455) % 0.53/0.70 k04_buttercup10100(sK37) % 0.53/0.70 k04_buttercup10100(sK456) % 0.53/0.70 k04_buttercup10100(sK31) % 0.53/0.70 k04_buttercup10100(sK262) % 0.53/0.70 k04_buttercup10100(sK482) % 0.53/0.70 k04_buttercup10100(sK96) % 0.53/0.70 k04_buttercup10100(sK186) % 0.53/0.70 k04_buttercup10100(sK483) % 0.53/0.70 k04_buttercup10100(sK97) % 0.53/0.70 k04_buttercup10100(sK458) % 0.53/0.70 k04_buttercup10100(sK106) % 0.53/0.70 k04_buttercup10100(sK272) % 0.53/0.70 k04_buttercup10100(sK98) % 0.53/0.70 k04_buttercup10100(sK459) % 0.53/0.70 k04_buttercup10100(sK205) % 0.53/0.70 k04_buttercup10100(sK58) % 0.53/0.70 k04_buttercup10100(sK52) % 0.53/0.70 k04_buttercup10100(sK460) % 0.53/0.70 k04_buttercup10117(sK275) % 0.53/0.70 k04_buttercup10117(sK478) % 0.53/0.70 k04_buttercup10117(sK135) % 0.53/0.70 k04_buttercup10117(sK412) % 0.53/0.70 k04_buttercup10117(sK480) % 0.53/0.70 k04_buttercup10125(sK234) % 0.53/0.70 k04_buttercup10125(sK413) % 0.53/0.70 k04_buttercup10132(sK119) % 0.53/0.70 k04_buttercup10132(sK434) % 0.53/0.70 k04_buttercup10132(sK120) % 0.53/0.70 k04_buttercup10132(sK435) % 0.53/0.70 k04_buttercup10132(sK249) % 0.53/0.70 k04_buttercup10132(sK436) % 0.53/0.70 k04_buttercup10135(sK248) % 0.53/0.70 k04_buttercup10139(sK82) % 0.53/0.70 k04_buttercup10139(sK191) % 0.53/0.70 k04_buttercup10139(sK169) % 0.53/0.70 k04_buttercup10139(sK421) % 0.53/0.70 k04_buttercup10142(sK191) % 0.53/0.70 k04_buttercup10142(sK421) % 0.53/0.70 k04_buttercup10147(sK448) % 0.53/0.70 k04_buttercup10147(sK230) % 0.53/0.70 k04_buttercup10153(sK93) % 0.53/0.70 k04_buttercup10153(sK382) % 0.53/0.70 k04_buttercup10153(sK386) % 0.53/0.70 k04_buttercup10153(sK2) % 0.53/0.70 k04_buttercup10153(sK94) % 0.53/0.70 k04_buttercup10153(sK208) % 0.53/0.70 k04_buttercup10153(sK383) % 0.53/0.70 k04_buttercup10153(sK3) % 0.53/0.70 k04_buttercup10153(sK92) % 0.53/0.70 k04_buttercup10153(sK321) % 0.53/0.70 k04_buttercup10153(sK381) % 0.53/0.70 k04_buttercup10153(sK385) % 0.53/0.70 k04_buttercup10164(sK123) % 0.53/0.70 k04_buttercup10164(sK124) % 0.53/0.70 k04_buttercup10164(sK296) % 0.53/0.70 k04_buttercup10164(sK125) % 0.53/0.70 k04_buttercup10164(sK293) % 0.53/0.70 k04_buttercup10164(sK297) % 0.53/0.70 k04_buttercup10164(sK154) % 0.53/0.70 k04_buttercup10164(sK298) % 0.53/0.70 k04_buttercup10172(sK326) % 0.53/0.70 k04_buttercup10172(sK173) % 0.53/0.70 k04_buttercup10172(sK324) % 0.53/0.70 k04_buttercup10172(sK122) % 0.53/0.70 k04_buttercup10172(sK126) % 0.53/0.70 k04_buttercup10172(sK325) % 0.53/0.70 k04_buttercup10181(sK506) % 0.53/0.70 k04_buttercup10181(sK270) % 0.53/0.70 k04_buttercup10184(sK152) % 0.53/0.70 k04_buttercup10190(sK25) % 0.53/0.70 k04_buttercup10190(sK287) % 0.53/0.70 k04_buttercup10190(sK474) % 0.53/0.70 k04_buttercup10190(sK498) % 0.53/0.70 k04_buttercup10190(sK502) % 0.53/0.70 k04_buttercup10190(sK26) % 0.53/0.70 k04_buttercup10190(sK500) % 0.53/0.70 k04_buttercup10190(sK133) % 0.53/0.70 k04_buttercup10200(sK159) % 0.53/0.70 k04_buttercup10200(sK504) % 0.53/0.70 k04_buttercup10204(sK163) % 0.53/0.70 k04_buttercup10204(sK410) % 0.53/0.70 k04_buttercup10204(sK350) % 0.53/0.70 k04_buttercup10204(sK216) % 0.53/0.70 k04_buttercup10204(sK281) % 0.53/0.70 k04_buttercup10204(sK285) % 0.53/0.70 k04_buttercup10204(sK492) % 0.53/0.70 k04_buttercup10204(sK77) % 0.53/0.70 k04_buttercup10204(sK206) % 0.53/0.70 k04_buttercup10204(sK465) % 0.53/0.70 k04_buttercup10204(sK493) % 0.53/0.70 k04_buttercup10204(sK72) % 0.53/0.70 k04_buttercup10204(sK266) % 0.53/0.70 k04_buttercup10206(sK206) % 0.53/0.70 k04_buttercup10206(sK465) % 0.53/0.70 k04_buttercup10213(sK285) % 0.53/0.70 k04_buttercup10213(sK493) % 0.53/0.70 k04_buttercup10219(sK281) % 0.53/0.70 k04_buttercup10219(sK492) % 0.53/0.70 k04_buttercup10221(sK350) % 0.53/0.70 k04_buttercup10221(sK266) % 0.53/0.70 k04_buttercup10225(sK5) % 0.53/0.70 k04_buttercup10225(sK470) % 0.53/0.70 k04_buttercup10225(sK269) % 0.53/0.70 k04_buttercup10225(sK4) % 0.53/0.70 k04_buttercup10225(sK501) % 0.53/0.70 k04_buttercup10234(sK184) % 0.53/0.70 k04_buttercup10234(sK177) % 0.53/0.70 k04_buttercup10234(sK257) % 0.53/0.70 k04_buttercup10234(sK441) % 0.53/0.70 k04_buttercup10236(sK177) % 0.53/0.70 k04_buttercup10238(sK257) % 0.53/0.70 k04_buttercup10244(sK239) % 0.53/0.70 k04_buttercup10244(sK423) % 0.53/0.70 k04_buttercup10252(sK415) % 0.53/0.70 k04_buttercup10252(sK225) % 0.53/0.70 k04_buttercup10255(sK227) % 0.53/0.70 k04_buttercup10255(sK451) % 0.53/0.70 k04_buttercup10259(_0) % 0.53/0.70 k04_buttercup10282(sK150) % 0.53/0.70 k04_buttercup10286(sK151) % 0.53/0.70 k04_buttercup10286(sK292) % 0.53/0.70 k04_buttercup10288(sK153) % 0.53/0.70 k04_buttercup10288(sK476) % 0.53/0.70 k04_buttercup10293(sK276) % 0.53/0.70 k04_buttercup10293(sK475) % 0.53/0.70 k04_buttercup10293(sK273) % 0.53/0.70 k04_buttercup10293(sK274) % 0.53/0.70 k04_buttercup10293(sK477) % 0.53/0.70 k04_buttercup10293(sK389) % 0.53/0.70 k04_buttercup10296(sK475) % 0.53/0.70 k04_buttercup10296(sK273) % 0.53/0.70 k04_buttercup10298(sK276) % 0.53/0.70 k04_buttercup10298(sK389) % 0.53/0.70 k04_buttercup10303(sK1) % 0.53/0.70 k04_buttercup10303(sK510) % 0.53/0.70 k04_buttercup10303(sK371) % 0.53/0.70 k04_buttercup10303(sK121) % 0.53/0.70 k04_buttercup10303(sK512) % 0.53/0.70 k04_buttercup10303(sK508) % 0.53/0.70 k04_buttercup10303(sK0) % 0.53/0.70 k04_buttercup10303(sK202) % 0.53/0.70 k04_buttercup10303(sK373) % 0.53/0.70 k04_buttercup10303(sK481) % 0.53/0.70 k04_buttercup10312(sK221) % 0.53/0.70 k04_buttercup10312(sK457) % 0.53/0.70 k04_buttercup10316(sK283) % 0.53/0.70 k04_buttercup10316(sK398) % 0.53/0.70 k04_buttercup10316(sK402) % 0.53/0.70 k04_buttercup10316(sK114) % 0.53/0.70 k04_buttercup10316(sK416) % 0.53/0.70 k04_buttercup10325(sK237) % 0.53/0.70 k04_buttercup10325(sK417) % 0.53/0.70 k04_buttercup10329(sK235) % 0.53/0.70 k04_buttercup10329(sK414) % 0.53/0.70 k04_buttercup10333(sK304) % 0.53/0.70 k04_buttercup10333(sK250) % 0.53/0.70 k04_buttercup10337(sK251) % 0.53/0.70 k04_buttercup10337(sK134) % 0.53/0.70 k04_buttercup10337(sK271) % 0.53/0.70 k04_buttercup10337(sK291) % 0.53/0.70 k04_buttercup10337(sK438) % 0.53/0.70 k04_buttercup10337(sK63) % 0.53/0.70 k04_buttercup10337(sK327) % 0.53/0.70 k04_buttercup10337(sK395) % 0.53/0.70 k04_buttercup10337(sK61) % 0.53/0.70 k04_buttercup10337(sK64) % 0.53/0.70 k04_buttercup10337(sK468) % 0.53/0.70 k04_buttercup10337(sK472) % 0.53/0.70 k04_buttercup10337(sK115) % 0.53/0.70 k04_buttercup10337(sK290) % 0.53/0.70 k04_buttercup10337(sK473) % 0.53/0.70 k04_buttercup10337(sK505) % 0.53/0.70 k04_buttercup10342(sK271) % 0.53/0.70 k04_buttercup10342(sK395) % 0.53/0.70 k04_buttercup10347(sK134) % 0.53/0.70 k04_buttercup10347(sK291) % 0.53/0.70 k04_buttercup10347(sK63) % 0.53/0.70 k04_buttercup10347(sK64) % 0.53/0.70 k04_buttercup10347(sK468) % 0.53/0.70 k04_buttercup10347(sK472) % 0.53/0.70 k04_buttercup10347(sK115) % 0.53/0.70 k04_buttercup10347(sK473) % 0.53/0.70 k04_buttercup10347(sK505) % 0.53/0.70 k04_buttercup10351(sK327) % 0.53/0.70 k04_buttercup10351(sK290) % 0.53/0.70 k04_buttercup10356(sK289) % 0.53/0.70 k04_buttercup10356(sK429) % 0.53/0.70 k04_buttercup10357(sK288) % 0.53/0.70 k04_buttercup10357(sK314) % 0.53/0.70 k04_buttercup10360(sK168) % 0.53/0.70 k04_buttercup10360(sK437) % 0.53/0.70 k04_buttercup10364(sK112) % 0.53/0.70 k04_buttercup10364(sK315) % 0.53/0.70 k04_buttercup10364(sK111) % 0.53/0.70 k04_buttercup10364(sK308) % 0.53/0.70 k04_buttercup10364(sK108) % 0.53/0.70 k04_buttercup10364(sK109) % 0.53/0.70 k04_buttercup10364(sK170) % 0.53/0.70 k04_buttercup10369(sK183) % 0.53/0.70 k04_buttercup10369(sK338) % 0.53/0.70 k04_buttercup10369(sK164) % 0.53/0.70 k04_buttercup10369(sK319) % 0.53/0.70 k04_buttercup10369(sK181) % 0.53/0.70 k04_buttercup10369(sK185) % 0.53/0.70 k04_buttercup10369(sK336) % 0.53/0.70 k04_buttercup10369(sK341) % 0.53/0.70 k04_buttercup10371(sK185) % 0.53/0.70 k04_buttercup10371(sK341) % 0.53/0.70 k04_buttercup10373(sK183) % 0.53/0.70 k04_buttercup10373(sK336) % 0.53/0.70 k04_buttercup10376(sK338) % 0.53/0.70 k04_buttercup10376(sK181) % 0.53/0.70 k04_buttercup10380(sK193) % 0.53/0.70 k04_buttercup10380(sK349) % 0.53/0.70 k04_buttercup10382(sK192) % 0.53/0.70 k04_buttercup10382(sK353) % 0.53/0.70 k04_buttercup10385(sK370) % 0.53/0.70 k04_buttercup10385(sK196) % 0.53/0.70 k04_buttercup10389(sK356) % 0.53/0.70 k04_buttercup10389(sK190) % 0.53/0.70 k04_buttercup10391(sK207) % 0.53/0.70 k04_buttercup10391(sK372) % 0.53/0.70 k04_buttercup10397(sK213) % 0.53/0.70 k04_buttercup10397(sK388) % 0.53/0.70 k04_buttercup10400(sK322) % 0.53/0.70 k04_buttercup10400(sK387) % 0.53/0.70 k04_buttercup10400(sK80) % 0.53/0.70 k04_buttercup10400(sK233) % 0.53/0.70 k04_buttercup10400(sK81) % 0.53/0.70 k04_buttercup10404(sK243) % 0.53/0.70 k04_buttercup10404(sK240) % 0.53/0.70 k04_buttercup10404(sK428) % 0.53/0.70 k04_buttercup10404(sK424) % 0.53/0.70 k04_buttercup10404(sK242) % 0.53/0.70 k04_buttercup10404(sK405) % 0.53/0.70 k04_buttercup10406(sK243) % 0.53/0.70 k04_buttercup10406(sK424) % 0.53/0.70 k04_buttercup10408(sK240) % 0.53/0.70 k04_buttercup10408(sK405) % 0.53/0.70 k04_buttercup10415(sK406) % 0.53/0.70 k04_buttercup10415(sK226) % 0.53/0.70 k04_buttercup10419(sK137) % 0.53/0.70 k04_buttercup10419(sK143) % 0.53/0.70 k04_buttercup10419(sK147) % 0.53/0.70 k04_buttercup10419(sK144) % 0.53/0.70 k04_buttercup10419(sK148) % 0.53/0.70 k04_buttercup10419(sK224) % 0.53/0.70 k04_buttercup10419(sK467) % 0.53/0.70 k04_buttercup10419(sK471) % 0.53/0.70 k04_buttercup10419(sK146) % 0.53/0.70 k04_buttercup10424(sK267) % 0.53/0.70 k04_buttercup10424(sK268) % 0.53/0.70 k04_buttercup10425(sK267) % 0.53/0.70 k04_buttercup10430(sK256) % 0.53/0.70 k04_buttercup10430(sK464) % 0.53/0.70 k04_buttercup10437(sK259) % 0.53/0.70 k04_buttercup10437(sK446) % 0.53/0.70 k04_buttercup10445(sK166) % 0.53/0.70 k04_buttercup10445(sK310) % 0.53/0.70 k04_buttercup10449(sK367) % 0.53/0.70 k04_buttercup10449(sK10) % 0.53/0.70 k04_buttercup10449(sK479) % 0.53/0.70 k04_buttercup10449(sK6) % 0.53/0.70 k04_buttercup10449(sK200) % 0.53/0.70 k04_buttercup10449(sK454) % 0.53/0.70 k04_buttercup10449(sK11) % 0.53/0.70 k04_buttercup10449(sK286) % 0.53/0.70 k04_buttercup10449(sK201) % 0.53/0.70 k04_buttercup10449(sK84) % 0.53/0.70 k04_buttercup10449(sK7) % 0.53/0.70 k04_buttercup10449(sK313) % 0.53/0.70 k04_buttercup10449(sK228) % 0.53/0.70 k04_buttercup10449(sK499) % 0.53/0.70 k04_buttercup10449(sK79) % 0.53/0.70 k04_buttercup10449(sK364) % 0.53/0.70 k04_buttercup10449(sK8) % 0.53/0.70 k04_buttercup10449(sK365) % 0.53/0.70 k04_buttercup10449(sK366) % 0.53/0.70 k04_buttercup10449(sK248) % 0.53/0.70 k04_buttercup10449(sK9) % 0.53/0.70 k04_buttercup10453(sK499) % 0.53/0.70 k04_buttercup10453(sK286) % 0.53/0.70 k04_buttercup10462(sK200) % 0.53/0.70 k04_buttercup10462(sK364) % 0.53/0.70 k04_buttercup10464(sK7) % 0.53/0.70 k04_buttercup10464(sK9) % 0.53/0.70 k04_buttercup10464(sK366) % 0.53/0.70 k04_buttercup10464(sK454) % 0.53/0.70 k04_buttercup10464(sK10) % 0.53/0.70 k04_buttercup10464(sK367) % 0.53/0.70 k04_buttercup10464(sK479) % 0.53/0.70 k04_buttercup10464(sK6) % 0.53/0.70 k04_buttercup10464(sK8) % 0.53/0.70 k04_buttercup10464(sK201) % 0.53/0.70 k04_buttercup10464(sK11) % 0.53/0.70 k04_buttercup10464(sK79) % 0.53/0.70 k04_buttercup10464(sK365) % 0.53/0.70 k04_buttercup10470(sK179) % 0.53/0.70 k04_buttercup10470(sK359) % 0.53/0.70 k04_buttercup10473(sK180) % 0.53/0.70 k04_buttercup10473(sK335) % 0.53/0.70 k04_buttercup10477(sK100) % 0.53/0.70 k04_buttercup10477(sK334) % 0.53/0.70 k04_buttercup10477(sK374) % 0.53/0.70 k04_buttercup10477(sK22) % 0.53/0.70 k04_buttercup10477(sK236) % 0.53/0.70 k04_buttercup10477(sK331) % 0.53/0.70 k04_buttercup10477(sK351) % 0.53/0.70 k04_buttercup10477(sK411) % 0.53/0.70 k04_buttercup10477(sK23) % 0.53/0.70 k04_buttercup10477(sK189) % 0.53/0.70 k04_buttercup10477(sK178) % 0.53/0.70 k04_buttercup10477(sK99) % 0.53/0.70 k04_buttercup10477(sK509) % 0.53/0.70 k04_buttercup10482(sK236) % 0.53/0.70 k04_buttercup10482(sK509) % 0.53/0.70 k04_buttercup10486(sK100) % 0.53/0.70 k04_buttercup10486(sK374) % 0.53/0.70 k04_buttercup10486(sK22) % 0.53/0.70 k04_buttercup10486(sK331) % 0.53/0.70 k04_buttercup10486(sK351) % 0.53/0.70 k04_buttercup10486(sK411) % 0.53/0.70 k04_buttercup10486(sK23) % 0.53/0.70 k04_buttercup10486(sK189) % 0.53/0.70 k04_buttercup10486(sK99) % 0.53/0.70 k04_buttercup10492(sK215) % 0.53/0.70 k04_buttercup10492(sK393) % 0.53/0.70 k04_buttercup10495(sK392) % 0.53/0.70 k04_buttercup10495(sK214) % 0.53/0.70 k04_buttercup10499(sK219) % 0.53/0.70 k04_buttercup10499(sK390) % 0.53/0.70 k04_buttercup10504(sK175) % 0.53/0.70 k04_buttercup10504(sK174) % 0.53/0.70 k04_buttercup10504(sK294) % 0.53/0.70 k04_buttercup10506(sK175) % 0.53/0.70 k04_buttercup10506(sK294) % 0.53/0.70 k04_buttercup10510(sK330) % 0.53/0.70 k04_buttercup10510(sK197) % 0.53/0.70 k04_buttercup10516(sK199) % 0.53/0.70 k04_buttercup10516(sK462) % 0.53/0.70 k04_buttercup10516(sK363) % 0.53/0.70 k04_buttercup10516(sK491) % 0.53/0.70 k04_buttercup10516(sK67) % 0.53/0.70 k04_buttercup10516(sK320) % 0.53/0.70 k04_buttercup10516(sK420) % 0.53/0.70 k04_buttercup10516(sK198) % 0.53/0.70 k04_buttercup10516(sK361) % 0.53/0.70 k04_buttercup10517(sK320) % 0.53/0.70 k04_buttercup10517(sK198) % 0.53/0.70 k04_buttercup10524(sK284) % 0.53/0.70 k04_buttercup10529(sK280) % 0.53/0.70 k04_buttercup10529(sK425) % 0.53/0.70 k04_buttercup10535(sK305) % 0.53/0.70 k04_buttercup10535(sK162) % 0.53/0.70 k04_buttercup10539(sK155) % 0.53/0.70 k04_buttercup10539(sK301) % 0.53/0.70 k04_buttercup10540(sK252) % 0.53/0.70 k04_buttercup10540(sK439) % 0.53/0.70 k04_buttercup10544(sK255) % 0.53/0.70 k04_buttercup10544(sK442) % 0.53/0.70 k04_buttercup10544(sK443) % 0.53/0.70 k04_buttercup10544(sK253) % 0.53/0.70 k04_buttercup10544(sK440) % 0.53/0.70 k04_buttercup10544(sK254) % 0.53/0.70 k04_buttercup10546(sK442) % 0.53/0.70 k04_buttercup10546(sK254) % 0.53/0.70 k04_buttercup10547(sK255) % 0.53/0.70 k04_buttercup10547(sK443) % 0.53/0.70 k04_buttercup10551(sK265) % 0.53/0.70 k04_buttercup10551(sK444) % 0.53/0.70 k04_buttercup10555(sK263) % 0.53/0.70 k04_buttercup10555(sK264) % 0.53/0.70 k04_buttercup10555(sK463) % 0.53/0.70 k04_buttercup10555(sK399) % 0.53/0.70 k04_buttercup10555(sK401) % 0.53/0.70 k04_buttercup10559(sK263) % 0.53/0.70 k04_buttercup10559(sK399) % 0.53/0.70 k04_buttercup10567(sK422) % 0.53/0.70 k04_buttercup10567(sK419) % 0.53/0.70 k04_buttercup10567(sK507) % 0.53/0.70 k04_buttercup10567(sK117) % 0.53/0.70 k04_buttercup10567(sK136) % 0.53/0.70 k04_buttercup10567(sK217) % 0.53/0.70 k04_buttercup10567(sK400) % 0.53/0.70 k04_buttercup10567(sK118) % 0.53/0.70 k04_buttercup10578(sK244) % 0.53/0.70 k04_buttercup10578(sK380) % 0.53/0.70 k04_buttercup10581(sK427) % 0.53/0.70 k04_buttercup10581(sK238) % 0.53/0.70 k04_buttercup10586(sK187) % 0.53/0.70 k04_buttercup10586(sK348) % 0.53/0.70 k04_buttercup10593(sK203) % 0.53/0.70 k04_buttercup10593(sK378) % 0.53/0.70 k04_buttercup10593(sK204) % 0.53/0.70 k04_buttercup10593(sK339) % 0.53/0.70 k04_buttercup10593(sK396) % 0.53/0.70 k04_buttercup10593(sK218) % 0.53/0.70 k04_buttercup10599(sK203) % 0.53/0.70 k04_buttercup10599(sK378) % 0.53/0.70 k04_buttercup10602(sK396) % 0.53/0.70 k04_buttercup10602(sK218) % 0.53/0.70 k04_buttercup10608(sK410) % 0.53/0.70 k04_buttercup10608(sK216) % 0.53/0.70 k04_buttercup10611(sK211) % 0.53/0.70 k04_buttercup10611(sK408) % 0.53/0.70 k04_buttercup10619(sK96) % 0.53/0.70 k04_buttercup10619(sK458) % 0.53/0.70 k04_buttercup10619(sK482) % 0.53/0.70 k04_buttercup10619(sK97) % 0.53/0.70 k04_buttercup10619(sK272) % 0.53/0.70 k04_buttercup10619(sK455) % 0.53/0.70 k04_buttercup10619(sK459) % 0.53/0.70 k04_buttercup10619(sK483) % 0.53/0.70 k04_buttercup10619(sK205) % 0.53/0.70 k04_buttercup10619(sK27) % 0.53/0.70 k04_buttercup10619(sK98) % 0.53/0.70 k04_buttercup10619(sK456) % 0.53/0.70 k04_buttercup10619(sK31) % 0.53/0.70 k04_buttercup10619(sK186) % 0.53/0.70 k04_buttercup10620(sK458) % 0.53/0.70 k04_buttercup10620(sK272) % 0.53/0.70 k04_buttercup10622(sK96) % 0.53/0.70 k04_buttercup10622(sK97) % 0.53/0.70 k04_buttercup10622(sK455) % 0.53/0.70 k04_buttercup10622(sK459) % 0.53/0.70 k04_buttercup10622(sK483) % 0.53/0.70 k04_buttercup10622(sK27) % 0.53/0.70 k04_buttercup10622(sK98) % 0.53/0.70 k04_buttercup10622(sK456) % 0.53/0.70 k04_buttercup10622(sK186) % 0.53/0.70 k04_buttercup10626(sK182) % 0.53/0.70 k04_buttercup10626(sK337) % 0.53/0.70 k04_buttercup10628(sK295) % 0.53/0.70 k04_buttercup10628(sK188) % 0.53/0.70 k04_buttercup10628(sK91) % 0.53/0.70 k04_buttercup10628(sK150) % 0.53/0.70 k04_buttercup10631(sK167) % 0.53/0.70 k04_buttercup10631(sK346) % 0.53/0.70 k04_buttercup10635(sK171) % 0.53/0.70 k04_buttercup10635(sK279) % 0.53/0.70 k04_buttercup10635(sK318) % 0.53/0.70 k04_buttercup10635(sK486) % 0.53/0.70 k04_buttercup10635(sK312) % 0.53/0.70 k04_buttercup10635(sK165) % 0.53/0.70 k04_buttercup10635(sK209) % 0.53/0.70 k04_buttercup10635(sK452) % 0.53/0.70 k04_buttercup10637(sK209) % 0.53/0.70 k04_buttercup10637(sK452) % 0.53/0.70 k04_buttercup10639(sK171) % 0.53/0.70 k04_buttercup10639(sK318) % 0.53/0.70 k04_buttercup10641(sK279) % 0.53/0.70 k04_buttercup10641(sK486) % 0.53/0.70 k04_buttercup10643(sK277) % 0.53/0.70 k04_buttercup10643(sK484) % 0.53/0.70 sP0(_0) % 0.53/0.70 sP10(_0) % 0.53/0.70 sP12(_0) % 0.53/0.70 sP14(_0) % 0.53/0.70 sP16(_0) % 0.53/0.70 sP2(_0) % 0.53/0.70 sP20(_0) % 0.53/0.70 sP24 % 0.53/0.70 sP6(_0) % 0.53/0.70 sP8(_0) % 0.53/0.70 END OF MODEL %------------------------------------------------------------------------------