; %%% A sample EC axiomatization sort: object(O1). ; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% fluent: F1(object). fluent: F2(object). fluent: F3(object). fluent: F4(object). fluent: F5(object). fluent: F6(object). fluent: F7(object). fluent: F8(object). fluent: F9(object). fluent: F10(object). fluent: F11(object). fluent: F12(object). fluent: F13(object). fluent: F14(object). fluent: F15(object). fluent: F16(object). fluent: F17(object). fluent: F18(object). fluent: F19(object). fluent: F20(object). fluent: F21(object). fluent: F22(object). fluent: F23(object). fluent: F24(object). fluent: F25(object). fluent: F26(object). fluent: F27(object). fluent: F28(object). fluent: F29(object). fluent: F30(object). fluent: F31(object). fluent: F32(object). fluent: F33(object). fluent: F34(object). fluent: F35(object). fluent: F36(object). fluent: F37(object). fluent: F38(object). fluent: F39(object). fluent: F40(object). fluent: F41(object). fluent: F42(object). fluent: F43(object). fluent: F44(object). fluent: F45(object). fluent: F46(object). fluent: F47(object). fluent: F48(object). fluent: F49(object). fluent: F50(object). fluent: F51(object). fluent: F52(object). fluent: F53(object). fluent: F54(object). fluent: F55(object). fluent: F56(object). fluent: F57(object). fluent: F58(object). fluent: F59(object). fluent: F60(object). fluent: F61(object). fluent: F62(object). fluent: F63(object). fluent: F64(object). fluent: F65(object). fluent: F66(object). fluent: F67(object). fluent: F68(object). fluent: F69(object). fluent: F70(object). fluent: F71(object). fluent: F72(object). fluent: F73(object). fluent: F74(object). fluent: F75(object). fluent: F76(object). fluent: F77(object). fluent: F78(object). fluent: F79(object). fluent: F80(object). fluent: F81(object). fluent: F82(object). fluent: F83(object). fluent: F84(object). fluent: F85(object). fluent: F86(object). fluent: F87(object). fluent: F88(object). fluent: F89(object). fluent: F90(object). fluent: F91(object). fluent: F92(object). fluent: F93(object). fluent: F94(object). fluent: F95(object). fluent: F96(object). fluent: F97(object). fluent: F98(object). fluent: F99(object). fluent: F100(object). fluent: F101(object). fluent: F102(object). fluent: F103(object). fluent: F104(object). fluent: F105(object). fluent: F106(object). fluent: F107(object). fluent: F108(object). fluent: F109(object). fluent: F110(object). fluent: F111(object). fluent: F112(object). fluent: F113(object). fluent: F114(object). fluent: F115(object). fluent: F116(object). fluent: F117(object). fluent: F118(object). fluent: F119(object). fluent: F120(object). fluent: F121(object). fluent: F122(object). fluent: F123(object). fluent: F124(object). fluent: F125(object). fluent: F126(object). fluent: F127(object). fluent: F128(object). fluent: F129(object). fluent: F130(object). fluent: F131(object). fluent: F132(object). fluent: F133(object). fluent: F134(object). fluent: F135(object). fluent: F136(object). fluent: F137(object). fluent: F138(object). fluent: F139(object). fluent: F140(object). fluent: F141(object). fluent: F142(object). fluent: F143(object). fluent: F144(object). fluent: F145(object). fluent: F146(object). fluent: F147(object). fluent: F148(object). fluent: F149(object). fluent: F150(object). fluent: F151(object). fluent: F152(object). fluent: F153(object). fluent: F154(object). fluent: F155(object). fluent: F156(object). fluent: F157(object). fluent: F158(object). fluent: F159(object). fluent: F160(object). fluent: F161(object). fluent: F162(object). fluent: F163(object). fluent: F164(object). fluent: F165(object). fluent: F166(object). fluent: F167(object). fluent: F168(object). fluent: F169(object). fluent: F170(object). fluent: F171(object). fluent: F172(object). fluent: F173(object). fluent: F174(object). fluent: F175(object). fluent: F176(object). fluent: F177(object). fluent: F178(object). fluent: F179(object). fluent: F180(object). fluent: F181(object). fluent: F182(object). fluent: F183(object). fluent: F184(object). fluent: F185(object). fluent: F186(object). fluent: F187(object). fluent: F188(object). fluent: F189(object). fluent: F190(object). fluent: F191(object). fluent: F192(object). fluent: F193(object). fluent: F194(object). fluent: F195(object). fluent: F196(object). fluent: F197(object). fluent: F198(object). fluent: F199(object). fluent: F200(object). fluent: F201(object). fluent: F202(object). fluent: F203(object). fluent: F204(object). fluent: F205(object). fluent: F206(object). fluent: F207(object). fluent: F208(object). fluent: F209(object). fluent: F210(object). fluent: F211(object). fluent: F212(object). fluent: F213(object). fluent: F214(object). fluent: F215(object). fluent: F216(object). fluent: F217(object). fluent: F218(object). fluent: F219(object). fluent: F220(object). fluent: F221(object). fluent: F222(object). fluent: F223(object). fluent: F224(object). fluent: F225(object). fluent: F226(object). fluent: F227(object). fluent: F228(object). fluent: F229(object). fluent: F230(object). fluent: F231(object). fluent: F232(object). fluent: F233(object). fluent: F234(object). fluent: F235(object). fluent: F236(object). fluent: F237(object). fluent: F238(object). fluent: F239(object). fluent: F240(object). fluent: F241(object). fluent: F242(object). fluent: F243(object). fluent: F244(object). fluent: F245(object). fluent: F246(object). fluent: F247(object). fluent: F248(object). fluent: F249(object). fluent: F250(object). fluent: F251(object). fluent: F252(object). fluent: F253(object). fluent: F254(object). fluent: F255(object). fluent: F256(object). fluent: F257(object). fluent: F258(object). fluent: F259(object). fluent: F260(object). fluent: F261(object). fluent: F262(object). fluent: F263(object). fluent: F264(object). fluent: F265(object). fluent: F266(object). fluent: F267(object). fluent: F268(object). fluent: F269(object). fluent: F270(object). fluent: F271(object). fluent: F272(object). fluent: F273(object). fluent: F274(object). fluent: F275(object). fluent: F276(object). fluent: F277(object). fluent: F278(object). fluent: F279(object). fluent: F280(object). fluent: F281(object). fluent: F282(object). fluent: F283(object). fluent: F284(object). fluent: F285(object). fluent: F286(object). fluent: F287(object). fluent: F288(object). fluent: F289(object). fluent: F290(object). fluent: F291(object). fluent: F292(object). fluent: F293(object). fluent: F294(object). fluent: F295(object). fluent: F296(object). fluent: F297(object). fluent: F298(object). fluent: F299(object). fluent: F300(object). fluent: F301(object). fluent: F302(object). fluent: F303(object). fluent: F304(object). fluent: F305(object). fluent: F306(object). fluent: F307(object). fluent: F308(object). fluent: F309(object). fluent: F310(object). fluent: F311(object). fluent: F312(object). fluent: F313(object). fluent: F314(object). fluent: F315(object). fluent: F316(object). fluent: F317(object). fluent: F318(object). fluent: F319(object). fluent: F320(object). fluent: F321(object). fluent: F322(object). fluent: F323(object). fluent: F324(object). fluent: F325(object). fluent: F326(object). fluent: F327(object). fluent: F328(object). fluent: F329(object). fluent: F330(object). fluent: F331(object). fluent: F332(object). fluent: F333(object). fluent: F334(object). fluent: F335(object). fluent: F336(object). fluent: F337(object). fluent: F338(object). fluent: F339(object). fluent: F340(object). fluent: F341(object). fluent: F342(object). fluent: F343(object). fluent: F344(object). fluent: F345(object). fluent: F346(object). fluent: F347(object). fluent: F348(object). fluent: F349(object). fluent: F350(object). fluent: F351(object). fluent: F352(object). fluent: F353(object). fluent: F354(object). fluent: F355(object). fluent: F356(object). fluent: F357(object). fluent: F358(object). fluent: F359(object). fluent: F360(object). fluent: F361(object). fluent: F362(object). fluent: F363(object). fluent: F364(object). fluent: F365(object). fluent: F366(object). fluent: F367(object). fluent: F368(object). fluent: F369(object). fluent: F370(object). fluent: F371(object). fluent: F372(object). fluent: F373(object). fluent: F374(object). fluent: F375(object). fluent: F376(object). fluent: F377(object). fluent: F378(object). fluent: F379(object). fluent: F380(object). fluent: F381(object). fluent: F382(object). fluent: F383(object). fluent: F384(object). fluent: F385(object). fluent: F386(object). fluent: F387(object). fluent: F388(object). fluent: F389(object). fluent: F390(object). fluent: F391(object). fluent: F392(object). fluent: F393(object). fluent: F394(object). fluent: F395(object). fluent: F396(object). fluent: F397(object). fluent: F398(object). fluent: F399(object). fluent: F400(object). fluent: F401(object). fluent: F402(object). fluent: F403(object). fluent: F404(object). fluent: F405(object). fluent: F406(object). fluent: F407(object). fluent: F408(object). fluent: F409(object). fluent: F410(object). fluent: F411(object). fluent: F412(object). fluent: F413(object). fluent: F414(object). fluent: F415(object). fluent: F416(object). fluent: F417(object). fluent: F418(object). fluent: F419(object). fluent: F420(object). fluent: F421(object). fluent: F422(object). fluent: F423(object). fluent: F424(object). fluent: F425(object). fluent: F426(object). fluent: F427(object). fluent: F428(object). fluent: F429(object). fluent: F430(object). fluent: F431(object). fluent: F432(object). fluent: F433(object). fluent: F434(object). fluent: F435(object). fluent: F436(object). fluent: F437(object). fluent: F438(object). fluent: F439(object). fluent: F440(object). fluent: F441(object). fluent: F442(object). fluent: F443(object). fluent: F444(object). fluent: F445(object). fluent: F446(object). fluent: F447(object). fluent: F448(object). fluent: F449(object). fluent: F450(object). fluent: F451(object). fluent: F452(object). fluent: F453(object). fluent: F454(object). fluent: F455(object). fluent: F456(object). fluent: F457(object). fluent: F458(object). fluent: F459(object). fluent: F460(object). fluent: F461(object). fluent: F462(object). fluent: F463(object). fluent: F464(object). fluent: F465(object). fluent: F466(object). fluent: F467(object). fluent: F468(object). fluent: F469(object). fluent: F470(object). fluent: F471(object). fluent: F472(object). fluent: F473(object). fluent: F474(object). fluent: F475(object). fluent: F476(object). fluent: F477(object). fluent: F478(object). fluent: F479(object). fluent: F480(object). fluent: F481(object). fluent: F482(object). fluent: F483(object). fluent: F484(object). fluent: F485(object). fluent: F486(object). fluent: F487(object). fluent: F488(object). fluent: F489(object). fluent: F490(object). fluent: F491(object). fluent: F492(object). fluent: F493(object). fluent: F494(object). fluent: F495(object). fluent: F496(object). fluent: F497(object). fluent: F498(object). fluent: F499(object). fluent: F500(object). fluent: F501(object). fluent: F502(object). fluent: F503(object). fluent: F504(object). fluent: F505(object). fluent: F506(object). fluent: F507(object). fluent: F508(object). fluent: F509(object). fluent: F510(object). fluent: F511(object). fluent: F512(object). fluent: F513(object). fluent: F514(object). fluent: F515(object). fluent: F516(object). fluent: F517(object). fluent: F518(object). fluent: F519(object). fluent: F520(object). fluent: F521(object). fluent: F522(object). fluent: F523(object). fluent: F524(object). fluent: F525(object). fluent: F526(object). fluent: F527(object). fluent: F528(object). fluent: F529(object). fluent: F530(object). fluent: F531(object). fluent: F532(object). fluent: F533(object). fluent: F534(object). fluent: F535(object). fluent: F536(object). fluent: F537(object). fluent: F538(object). fluent: F539(object). fluent: F540(object). fluent: F541(object). fluent: F542(object). fluent: F543(object). fluent: F544(object). fluent: F545(object). fluent: F546(object). fluent: F547(object). fluent: F548(object). fluent: F549(object). fluent: F550(object). fluent: F551(object). fluent: F552(object). fluent: F553(object). fluent: F554(object). fluent: F555(object). fluent: F556(object). fluent: F557(object). fluent: F558(object). fluent: F559(object). fluent: F560(object). fluent: F561(object). fluent: F562(object). fluent: F563(object). fluent: F564(object). fluent: F565(object). fluent: F566(object). fluent: F567(object). fluent: F568(object). fluent: F569(object). fluent: F570(object). fluent: F571(object). fluent: F572(object). fluent: F573(object). fluent: F574(object). fluent: F575(object). fluent: F576(object). fluent: F577(object). fluent: F578(object). fluent: F579(object). fluent: F580(object). fluent: F581(object). fluent: F582(object). fluent: F583(object). fluent: F584(object). fluent: F585(object). fluent: F586(object). fluent: F587(object). fluent: F588(object). fluent: F589(object). fluent: F590(object). fluent: F591(object). fluent: F592(object). fluent: F593(object). fluent: F594(object). fluent: F595(object). fluent: F596(object). fluent: F597(object). fluent: F598(object). fluent: F599(object). fluent: F600(object). fluent: F601(object). fluent: F602(object). fluent: F603(object). fluent: F604(object). fluent: F605(object). fluent: F606(object). fluent: F607(object). fluent: F608(object). fluent: F609(object). fluent: F610(object). fluent: F611(object). fluent: F612(object). fluent: F613(object). fluent: F614(object). fluent: F615(object). fluent: F616(object). fluent: F617(object). fluent: F618(object). fluent: F619(object). fluent: F620(object). fluent: F621(object). fluent: F622(object). fluent: F623(object). fluent: F624(object). fluent: F625(object). fluent: F626(object). fluent: F627(object). fluent: F628(object). fluent: F629(object). fluent: F630(object). fluent: F631(object). fluent: F632(object). fluent: F633(object). fluent: F634(object). fluent: F635(object). fluent: F636(object). fluent: F637(object). fluent: F638(object). fluent: F639(object). fluent: F640(object). fluent: F641(object). fluent: F642(object). fluent: F643(object). fluent: F644(object). fluent: F645(object). fluent: F646(object). fluent: F647(object). fluent: F648(object). fluent: F649(object). fluent: F650(object). fluent: F651(object). fluent: F652(object). fluent: F653(object). fluent: F654(object). fluent: F655(object). fluent: F656(object). fluent: F657(object). fluent: F658(object). fluent: F659(object). fluent: F660(object). fluent: F661(object). fluent: F662(object). fluent: F663(object). fluent: F664(object). fluent: F665(object). fluent: F666(object). fluent: F667(object). fluent: F668(object). fluent: F669(object). fluent: F670(object). fluent: F671(object). fluent: F672(object). fluent: F673(object). fluent: F674(object). fluent: F675(object). fluent: F676(object). fluent: F677(object). fluent: F678(object). fluent: F679(object). fluent: F680(object). fluent: F681(object). fluent: F682(object). fluent: F683(object). fluent: F684(object). fluent: F685(object). fluent: F686(object). fluent: F687(object). fluent: F688(object). fluent: F689(object). fluent: F690(object). fluent: F691(object). fluent: F692(object). fluent: F693(object). fluent: F694(object). fluent: F695(object). fluent: F696(object). fluent: F697(object). fluent: F698(object). fluent: F699(object). fluent: F700(object). fluent: F701(object). fluent: F702(object). fluent: F703(object). fluent: F704(object). fluent: F705(object). fluent: F706(object). fluent: F707(object). fluent: F708(object). fluent: F709(object). fluent: F710(object). fluent: F711(object). fluent: F712(object). fluent: F713(object). fluent: F714(object). fluent: F715(object). fluent: F716(object). fluent: F717(object). fluent: F718(object). fluent: F719(object). fluent: F720(object). fluent: F721(object). fluent: F722(object). fluent: F723(object). fluent: F724(object). fluent: F725(object). fluent: F726(object). fluent: F727(object). fluent: F728(object). fluent: F729(object). fluent: F730(object). fluent: F731(object). fluent: F732(object). fluent: F733(object). fluent: F734(object). fluent: F735(object). fluent: F736(object). fluent: F737(object). fluent: F738(object). fluent: F739(object). fluent: F740(object). fluent: F741(object). fluent: F742(object). fluent: F743(object). fluent: F744(object). fluent: F745(object). fluent: F746(object). fluent: F747(object). fluent: F748(object). fluent: F749(object). fluent: F750(object). fluent: F751(object). fluent: F752(object). fluent: F753(object). fluent: F754(object). fluent: F755(object). fluent: F756(object). fluent: F757(object). fluent: F758(object). fluent: F759(object). fluent: F760(object). fluent: F761(object). fluent: F762(object). fluent: F763(object). fluent: F764(object). fluent: F765(object). fluent: F766(object). fluent: F767(object). fluent: F768(object). fluent: F769(object). fluent: F770(object). fluent: F771(object). fluent: F772(object). fluent: F773(object). fluent: F774(object). fluent: F775(object). fluent: F776(object). fluent: F777(object). fluent: F778(object). fluent: F779(object). fluent: F780(object). fluent: F781(object). fluent: F782(object). fluent: F783(object). fluent: F784(object). fluent: F785(object). fluent: F786(object). fluent: F787(object). fluent: F788(object). fluent: F789(object). fluent: F790(object). fluent: F791(object). fluent: F792(object). fluent: F793(object). fluent: F794(object). fluent: F795(object). fluent: F796(object). fluent: F797(object). fluent: F798(object). fluent: F799(object). fluent: F800(object). fluent: F801(object). fluent: F802(object). fluent: F803(object). fluent: F804(object). fluent: F805(object). fluent: F806(object). fluent: F807(object). fluent: F808(object). fluent: F809(object). fluent: F810(object). fluent: F811(object). fluent: F812(object). fluent: F813(object). fluent: F814(object). fluent: F815(object). fluent: F816(object). fluent: F817(object). fluent: F818(object). fluent: F819(object). fluent: F820(object). fluent: F821(object). fluent: F822(object). fluent: F823(object). fluent: F824(object). fluent: F825(object). fluent: F826(object). fluent: F827(object). fluent: F828(object). fluent: F829(object). fluent: F830(object). fluent: F831(object). fluent: F832(object). fluent: F833(object). fluent: F834(object). fluent: F835(object). fluent: F836(object). fluent: F837(object). fluent: F838(object). fluent: F839(object). fluent: F840(object). fluent: F841(object). fluent: F842(object). fluent: F843(object). fluent: F844(object). fluent: F845(object). fluent: F846(object). fluent: F847(object). fluent: F848(object). fluent: F849(object). fluent: F850(object). fluent: F851(object). fluent: F852(object). fluent: F853(object). fluent: F854(object). fluent: F855(object). fluent: F856(object). fluent: F857(object). fluent: F858(object). fluent: F859(object). fluent: F860(object). fluent: F861(object). fluent: F862(object). fluent: F863(object). fluent: F864(object). fluent: F865(object). fluent: F866(object). fluent: F867(object). fluent: F868(object). fluent: F869(object). fluent: F870(object). fluent: F871(object). fluent: F872(object). fluent: F873(object). fluent: F874(object). fluent: F875(object). fluent: F876(object). fluent: F877(object). fluent: F878(object). fluent: F879(object). fluent: F880(object). fluent: F881(object). fluent: F882(object). fluent: F883(object). fluent: F884(object). fluent: F885(object). fluent: F886(object). fluent: F887(object). fluent: F888(object). fluent: F889(object). fluent: F890(object). fluent: F891(object). fluent: F892(object). fluent: F893(object). fluent: F894(object). fluent: F895(object). fluent: F896(object). fluent: F897(object). fluent: F898(object). fluent: F899(object). fluent: F900(object). fluent: F901(object). fluent: F902(object). fluent: F903(object). fluent: F904(object). fluent: F905(object). fluent: F906(object). fluent: F907(object). fluent: F908(object). fluent: F909(object). fluent: F910(object). fluent: F911(object). fluent: F912(object). fluent: F913(object). fluent: F914(object). fluent: F915(object). fluent: F916(object). fluent: F917(object). fluent: F918(object). fluent: F919(object). fluent: F920(object). fluent: F921(object). fluent: F922(object). fluent: F923(object). fluent: F924(object). fluent: F925(object). fluent: F926(object). fluent: F927(object). fluent: F928(object). fluent: F929(object). fluent: F930(object). fluent: F931(object). fluent: F932(object). fluent: F933(object). fluent: F934(object). fluent: F935(object). fluent: F936(object). fluent: F937(object). fluent: F938(object). fluent: F939(object). fluent: F940(object). fluent: F941(object). fluent: F942(object). fluent: F943(object). fluent: F944(object). fluent: F945(object). fluent: F946(object). fluent: F947(object). fluent: F948(object). fluent: F949(object). fluent: F950(object). fluent: F951(object). fluent: F952(object). fluent: F953(object). fluent: F954(object). fluent: F955(object). fluent: F956(object). fluent: F957(object). fluent: F958(object). fluent: F959(object). fluent: F960(object). fluent: F961(object). fluent: F962(object). fluent: F963(object). fluent: F964(object). fluent: F965(object). fluent: F966(object). fluent: F967(object). fluent: F968(object). fluent: F969(object). fluent: F970(object). fluent: F971(object). fluent: F972(object). fluent: F973(object). fluent: F974(object). fluent: F975(object). fluent: F976(object). fluent: F977(object). fluent: F978(object). fluent: F979(object). fluent: F980(object). fluent: F981(object). fluent: F982(object). fluent: F983(object). fluent: F984(object). fluent: F985(object). fluent: F986(object). fluent: F987(object). fluent: F988(object). fluent: F989(object). fluent: F990(object). fluent: F991(object). fluent: F992(object). fluent: F993(object). fluent: F994(object). fluent: F995(object). fluent: F996(object). fluent: F997(object). fluent: F998(object). fluent: F999(object). fluent: F1000(object). ; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% event: E(object). event: E1(object). event: E2(object). event: E3(object). event: E4(object). event: E5(object). event: E6(object). event: E7(object). event: E8(object). event: E9(object). event: E10(object). event: E11(object). event: E12(object). event: E13(object). event: E14(object). event: E15(object). event: E16(object). event: E17(object). event: E18(object). event: E19(object). event: E20(object). event: E21(object). event: E22(object). event: E23(object). event: E24(object). event: E25(object). event: E26(object). event: E27(object). event: E28(object). event: E29(object). event: E30(object). event: E31(object). event: E32(object). event: E33(object). event: E34(object). event: E35(object). event: E36(object). event: E37(object). event: E38(object). event: E39(object). event: E40(object). event: E41(object). event: E42(object). event: E43(object). event: E44(object). event: E45(object). event: E46(object). event: E47(object). event: E48(object). event: E49(object). event: E50(object). event: E51(object). event: E52(object). event: E53(object). event: E54(object). event: E55(object). event: E56(object). event: E57(object). event: E58(object). event: E59(object). event: E60(object). event: E61(object). event: E62(object). event: E63(object). event: E64(object). event: E65(object). event: E66(object). event: E67(object). event: E68(object). event: E69(object). event: E70(object). event: E71(object). event: E72(object). event: E73(object). event: E74(object). event: E75(object). event: E76(object). event: E77(object). event: E78(object). event: E79(object). event: E80(object). event: E81(object). event: E82(object). event: E83(object). event: E84(object). event: E85(object). event: E86(object). event: E87(object). event: E88(object). event: E89(object). event: E90(object). event: E91(object). event: E92(object). event: E93(object). event: E94(object). event: E95(object). event: E96(object). event: E97(object). event: E98(object). event: E99(object). event: E100(object). event: E101(object). event: E102(object). event: E103(object). event: E104(object). event: E105(object). event: E106(object). event: E107(object). event: E108(object). event: E109(object). event: E110(object). event: E111(object). event: E112(object). event: E113(object). event: E114(object). event: E115(object). event: E116(object). event: E117(object). event: E118(object). event: E119(object). event: E120(object). event: E121(object). event: E122(object). event: E123(object). event: E124(object). event: E125(object). event: E126(object). event: E127(object). event: E128(object). event: E129(object). event: E130(object). event: E131(object). event: E132(object). event: E133(object). event: E134(object). event: E135(object). event: E136(object). event: E137(object). event: E138(object). event: E139(object). event: E140(object). event: E141(object). event: E142(object). event: E143(object). event: E144(object). event: E145(object). event: E146(object). event: E147(object). event: E148(object). event: E149(object). event: E150(object). event: E151(object). event: E152(object). event: E153(object). event: E154(object). event: E155(object). event: E156(object). event: E157(object). event: E158(object). event: E159(object). event: E160(object). event: E161(object). event: E162(object). event: E163(object). event: E164(object). event: E165(object). event: E166(object). event: E167(object). event: E168(object). event: E169(object). event: E170(object). event: E171(object). event: E172(object). event: E173(object). event: E174(object). event: E175(object). event: E176(object). event: E177(object). event: E178(object). event: E179(object). event: E180(object). event: E181(object). event: E182(object). event: E183(object). event: E184(object). event: E185(object). event: E186(object). event: E187(object). event: E188(object). event: E189(object). event: E190(object). event: E191(object). event: E192(object). event: E193(object). event: E194(object). event: E195(object). event: E196(object). event: E197(object). event: E198(object). event: E199(object). event: E200(object). event: E201(object). event: E202(object). event: E203(object). event: E204(object). event: E205(object). event: E206(object). event: E207(object). event: E208(object). event: E209(object). event: E210(object). event: E211(object). event: E212(object). event: E213(object). event: E214(object). event: E215(object). event: E216(object). event: E217(object). event: E218(object). event: E219(object). event: E220(object). event: E221(object). event: E222(object). event: E223(object). event: E224(object). event: E225(object). event: E226(object). event: E227(object). event: E228(object). event: E229(object). event: E230(object). event: E231(object). event: E232(object). event: E233(object). event: E234(object). event: E235(object). event: E236(object). event: E237(object). event: E238(object). event: E239(object). event: E240(object). event: E241(object). event: E242(object). event: E243(object). event: E244(object). event: E245(object). event: E246(object). event: E247(object). event: E248(object). event: E249(object). event: E250(object). event: E251(object). event: E252(object). event: E253(object). event: E254(object). event: E255(object). event: E256(object). event: E257(object). event: E258(object). event: E259(object). event: E260(object). event: E261(object). event: E262(object). event: E263(object). event: E264(object). event: E265(object). event: E266(object). event: E267(object). event: E268(object). event: E269(object). event: E270(object). event: E271(object). event: E272(object). event: E273(object). event: E274(object). event: E275(object). event: E276(object). event: E277(object). event: E278(object). event: E279(object). event: E280(object). event: E281(object). event: E282(object). event: E283(object). event: E284(object). event: E285(object). event: E286(object). event: E287(object). event: E288(object). event: E289(object). event: E290(object). event: E291(object). event: E292(object). event: E293(object). event: E294(object). event: E295(object). event: E296(object). event: E297(object). event: E298(object). event: E299(object). event: E300(object). event: E301(object). event: E302(object). event: E303(object). event: E304(object). event: E305(object). event: E306(object). event: E307(object). event: E308(object). event: E309(object). event: E310(object). event: E311(object). event: E312(object). event: E313(object). event: E314(object). event: E315(object). event: E316(object). event: E317(object). event: E318(object). event: E319(object). event: E320(object). event: E321(object). event: E322(object). event: E323(object). event: E324(object). event: E325(object). event: E326(object). event: E327(object). event: E328(object). event: E329(object). event: E330(object). event: E331(object). event: E332(object). event: E333(object). event: E334(object). event: E335(object). event: E336(object). event: E337(object). event: E338(object). event: E339(object). event: E340(object). event: E341(object). event: E342(object). event: E343(object). event: E344(object). event: E345(object). event: E346(object). event: E347(object). event: E348(object). event: E349(object). event: E350(object). event: E351(object). event: E352(object). event: E353(object). event: E354(object). event: E355(object). event: E356(object). event: E357(object). event: E358(object). event: E359(object). event: E360(object). event: E361(object). event: E362(object). event: E363(object). event: E364(object). event: E365(object). event: E366(object). event: E367(object). event: E368(object). event: E369(object). event: E370(object). event: E371(object). event: E372(object). event: E373(object). event: E374(object). event: E375(object). event: E376(object). event: E377(object). event: E378(object). event: E379(object). event: E380(object). event: E381(object). event: E382(object). event: E383(object). event: E384(object). event: E385(object). event: E386(object). event: E387(object). event: E388(object). event: E389(object). event: E390(object). event: E391(object). event: E392(object). event: E393(object). event: E394(object). event: E395(object). event: E396(object). event: E397(object). event: E398(object). event: E399(object). event: E400(object). event: E401(object). event: E402(object). event: E403(object). event: E404(object). event: E405(object). event: E406(object). event: E407(object). event: E408(object). event: E409(object). event: E410(object). event: E411(object). event: E412(object). event: E413(object). event: E414(object). event: E415(object). event: E416(object). event: E417(object). event: E418(object). event: E419(object). event: E420(object). event: E421(object). event: E422(object). event: E423(object). event: E424(object). event: E425(object). event: E426(object). event: E427(object). event: E428(object). event: E429(object). event: E430(object). event: E431(object). event: E432(object). event: E433(object). event: E434(object). event: E435(object). event: E436(object). event: E437(object). event: E438(object). event: E439(object). event: E440(object). event: E441(object). event: E442(object). event: E443(object). event: E444(object). event: E445(object). event: E446(object). event: E447(object). event: E448(object). event: E449(object). event: E450(object). event: E451(object). event: E452(object). event: E453(object). event: E454(object). event: E455(object). event: E456(object). event: E457(object). event: E458(object). event: E459(object). event: E460(object). event: E461(object). event: E462(object). event: E463(object). event: E464(object). event: E465(object). event: E466(object). event: E467(object). event: E468(object). event: E469(object). event: E470(object). event: E471(object). event: E472(object). event: E473(object). event: E474(object). event: E475(object). event: E476(object). event: E477(object). event: E478(object). event: E479(object). event: E480(object). event: E481(object). event: E482(object). event: E483(object). event: E484(object). event: E485(object). event: E486(object). event: E487(object). event: E488(object). event: E489(object). event: E490(object). event: E491(object). event: E492(object). event: E493(object). event: E494(object). event: E495(object). event: E496(object). event: E497(object). event: E498(object). event: E499(object). event: E500(object). event: E501(object). event: E502(object). event: E503(object). event: E504(object). event: E505(object). event: E506(object). event: E507(object). event: E508(object). event: E509(object). event: E510(object). event: E511(object). event: E512(object). event: E513(object). event: E514(object). event: E515(object). event: E516(object). event: E517(object). event: E518(object). event: E519(object). event: E520(object). event: E521(object). event: E522(object). event: E523(object). event: E524(object). event: E525(object). event: E526(object). event: E527(object). event: E528(object). event: E529(object). event: E530(object). event: E531(object). event: E532(object). event: E533(object). event: E534(object). event: E535(object). event: E536(object). event: E537(object). event: E538(object). event: E539(object). event: E540(object). event: E541(object). event: E542(object). event: E543(object). event: E544(object). event: E545(object). event: E546(object). event: E547(object). event: E548(object). event: E549(object). event: E550(object). event: E551(object). event: E552(object). event: E553(object). event: E554(object). event: E555(object). event: E556(object). event: E557(object). event: E558(object). event: E559(object). event: E560(object). event: E561(object). event: E562(object). event: E563(object). event: E564(object). event: E565(object). event: E566(object). event: E567(object). event: E568(object). event: E569(object). event: E570(object). event: E571(object). event: E572(object). event: E573(object). event: E574(object). event: E575(object). event: E576(object). event: E577(object). event: E578(object). event: E579(object). event: E580(object). event: E581(object). event: E582(object). event: E583(object). event: E584(object). event: E585(object). event: E586(object). event: E587(object). event: E588(object). event: E589(object). event: E590(object). event: E591(object). event: E592(object). event: E593(object). event: E594(object). event: E595(object). event: E596(object). event: E597(object). event: E598(object). event: E599(object). event: E600(object). event: E601(object). event: E602(object). event: E603(object). event: E604(object). event: E605(object). event: E606(object). event: E607(object). event: E608(object). event: E609(object). event: E610(object). event: E611(object). event: E612(object). event: E613(object). event: E614(object). event: E615(object). event: E616(object). event: E617(object). event: E618(object). event: E619(object). event: E620(object). event: E621(object). event: E622(object). event: E623(object). event: E624(object). event: E625(object). event: E626(object). event: E627(object). event: E628(object). event: E629(object). event: E630(object). event: E631(object). event: E632(object). event: E633(object). event: E634(object). event: E635(object). event: E636(object). event: E637(object). event: E638(object). event: E639(object). event: E640(object). event: E641(object). event: E642(object). event: E643(object). event: E644(object). event: E645(object). event: E646(object). event: E647(object). event: E648(object). event: E649(object). event: E650(object). event: E651(object). event: E652(object). event: E653(object). event: E654(object). event: E655(object). event: E656(object). event: E657(object). event: E658(object). event: E659(object). event: E660(object). event: E661(object). event: E662(object). event: E663(object). event: E664(object). event: E665(object). event: E666(object). event: E667(object). event: E668(object). event: E669(object). event: E670(object). event: E671(object). event: E672(object). event: E673(object). event: E674(object). event: E675(object). event: E676(object). event: E677(object). event: E678(object). event: E679(object). event: E680(object). event: E681(object). event: E682(object). event: E683(object). event: E684(object). event: E685(object). event: E686(object). event: E687(object). event: E688(object). event: E689(object). event: E690(object). event: E691(object). event: E692(object). event: E693(object). event: E694(object). event: E695(object). event: E696(object). event: E697(object). event: E698(object). event: E699(object). event: E700(object). event: E701(object). event: E702(object). event: E703(object). event: E704(object). event: E705(object). event: E706(object). event: E707(object). event: E708(object). event: E709(object). event: E710(object). event: E711(object). event: E712(object). event: E713(object). event: E714(object). event: E715(object). event: E716(object). event: E717(object). event: E718(object). event: E719(object). event: E720(object). event: E721(object). event: E722(object). event: E723(object). event: E724(object). event: E725(object). event: E726(object). event: E727(object). event: E728(object). event: E729(object). event: E730(object). event: E731(object). event: E732(object). event: E733(object). event: E734(object). event: E735(object). event: E736(object). event: E737(object). event: E738(object). event: E739(object). event: E740(object). event: E741(object). event: E742(object). event: E743(object). event: E744(object). event: E745(object). event: E746(object). event: E747(object). event: E748(object). event: E749(object). event: E750(object). event: E751(object). event: E752(object). event: E753(object). event: E754(object). event: E755(object). event: E756(object). event: E757(object). event: E758(object). event: E759(object). event: E760(object). event: E761(object). event: E762(object). event: E763(object). event: E764(object). event: E765(object). event: E766(object). event: E767(object). event: E768(object). event: E769(object). event: E770(object). event: E771(object). event: E772(object). event: E773(object). event: E774(object). event: E775(object). event: E776(object). event: E777(object). event: E778(object). event: E779(object). event: E780(object). event: E781(object). event: E782(object). event: E783(object). event: E784(object). event: E785(object). event: E786(object). event: E787(object). event: E788(object). event: E789(object). event: E790(object). event: E791(object). event: E792(object). event: E793(object). event: E794(object). event: E795(object). event: E796(object). event: E797(object). event: E798(object). event: E799(object). event: E800(object). event: E801(object). event: E802(object). event: E803(object). event: E804(object). event: E805(object). event: E806(object). event: E807(object). event: E808(object). event: E809(object). event: E810(object). event: E811(object). event: E812(object). event: E813(object). event: E814(object). event: E815(object). event: E816(object). event: E817(object). event: E818(object). event: E819(object). event: E820(object). event: E821(object). event: E822(object). event: E823(object). event: E824(object). event: E825(object). event: E826(object). event: E827(object). event: E828(object). event: E829(object). event: E830(object). event: E831(object). event: E832(object). event: E833(object). event: E834(object). event: E835(object). event: E836(object). event: E837(object). event: E838(object). event: E839(object). event: E840(object). event: E841(object). event: E842(object). event: E843(object). event: E844(object). event: E845(object). event: E846(object). event: E847(object). event: E848(object). event: E849(object). event: E850(object). event: E851(object). event: E852(object). event: E853(object). event: E854(object). event: E855(object). event: E856(object). event: E857(object). event: E858(object). event: E859(object). event: E860(object). event: E861(object). event: E862(object). event: E863(object). event: E864(object). event: E865(object). event: E866(object). event: E867(object). event: E868(object). event: E869(object). event: E870(object). event: E871(object). event: E872(object). event: E873(object). event: E874(object). event: E875(object). event: E876(object). event: E877(object). event: E878(object). event: E879(object). event: E880(object). event: E881(object). event: E882(object). event: E883(object). event: E884(object). event: E885(object). event: E886(object). event: E887(object). event: E888(object). event: E889(object). event: E890(object). event: E891(object). event: E892(object). event: E893(object). event: E894(object). event: E895(object). event: E896(object). event: E897(object). event: E898(object). event: E899(object). event: E900(object). event: E901(object). event: E902(object). event: E903(object). event: E904(object). event: E905(object). event: E906(object). event: E907(object). event: E908(object). event: E909(object). event: E910(object). event: E911(object). event: E912(object). event: E913(object). event: E914(object). event: E915(object). event: E916(object). event: E917(object). event: E918(object). event: E919(object). event: E920(object). event: E921(object). event: E922(object). event: E923(object). event: E924(object). event: E925(object). event: E926(object). event: E927(object). event: E928(object). event: E929(object). event: E930(object). event: E931(object). event: E932(object). event: E933(object). event: E934(object). event: E935(object). event: E936(object). event: E937(object). event: E938(object). event: E939(object). event: E940(object). event: E941(object). event: E942(object). event: E943(object). event: E944(object). event: E945(object). event: E946(object). event: E947(object). event: E948(object). event: E949(object). event: E950(object). event: E951(object). event: E952(object). event: E953(object). event: E954(object). event: E955(object). event: E956(object). event: E957(object). event: E958(object). event: E959(object). event: E960(object). event: E961(object). event: E962(object). event: E963(object). event: E964(object). event: E965(object). event: E966(object). event: E967(object). event: E968(object). event: E969(object). event: E970(object). event: E971(object). event: E972(object). event: E973(object). event: E974(object). event: E975(object). event: E976(object). event: E977(object). event: E978(object). event: E979(object). event: E980(object). event: E981(object). event: E982(object). event: E983(object). event: E984(object). event: E985(object). event: E986(object). event: E987(object). event: E988(object). event: E989(object). event: E990(object). event: E991(object). event: E992(object). event: E993(object). event: E994(object). event: E995(object). event: E996(object). event: E997(object). event: E998(object). event: E999(object). event: E1000(object). ; %%%% Domain Axiomatization ; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Initiates(E1(?o1), F1(?o1), ?t). Initiates(E2(?o1), F2(?o1), ?t). Initiates(E3(?o1), F3(?o1), ?t). Initiates(E4(?o1), F4(?o1), ?t). Initiates(E5(?o1), F5(?o1), ?t). Initiates(E6(?o1), F6(?o1), ?t). Initiates(E7(?o1), F7(?o1), ?t). Initiates(E8(?o1), F8(?o1), ?t). Initiates(E9(?o1), F9(?o1), ?t). Initiates(E10(?o1), F10(?o1), ?t). Initiates(E11(?o1), F11(?o1), ?t). Initiates(E12(?o1), F12(?o1), ?t). Initiates(E13(?o1), F13(?o1), ?t). Initiates(E14(?o1), F14(?o1), ?t). Initiates(E15(?o1), F15(?o1), ?t). Initiates(E16(?o1), F16(?o1), ?t). Initiates(E17(?o1), F17(?o1), ?t). Initiates(E18(?o1), F18(?o1), ?t). Initiates(E19(?o1), F19(?o1), ?t). Initiates(E20(?o1), F20(?o1), ?t). Initiates(E21(?o1), F21(?o1), ?t). Initiates(E22(?o1), F22(?o1), ?t). Initiates(E23(?o1), F23(?o1), ?t). Initiates(E24(?o1), F24(?o1), ?t). Initiates(E25(?o1), F25(?o1), ?t). Initiates(E26(?o1), F26(?o1), ?t). Initiates(E27(?o1), F27(?o1), ?t). Initiates(E28(?o1), F28(?o1), ?t). Initiates(E29(?o1), F29(?o1), ?t). Initiates(E30(?o1), F30(?o1), ?t). Initiates(E31(?o1), F31(?o1), ?t). Initiates(E32(?o1), F32(?o1), ?t). Initiates(E33(?o1), F33(?o1), ?t). Initiates(E34(?o1), F34(?o1), ?t). Initiates(E35(?o1), F35(?o1), ?t). Initiates(E36(?o1), F36(?o1), ?t). Initiates(E37(?o1), F37(?o1), ?t). Initiates(E38(?o1), F38(?o1), ?t). Initiates(E39(?o1), F39(?o1), ?t). Initiates(E40(?o1), F40(?o1), ?t). Initiates(E41(?o1), F41(?o1), ?t). Initiates(E42(?o1), F42(?o1), ?t). Initiates(E43(?o1), F43(?o1), ?t). Initiates(E44(?o1), F44(?o1), ?t). Initiates(E45(?o1), F45(?o1), ?t). Initiates(E46(?o1), F46(?o1), ?t). Initiates(E47(?o1), F47(?o1), ?t). Initiates(E48(?o1), F48(?o1), ?t). Initiates(E49(?o1), F49(?o1), ?t). Initiates(E50(?o1), F50(?o1), ?t). Initiates(E51(?o1), F51(?o1), ?t). Initiates(E52(?o1), F52(?o1), ?t). Initiates(E53(?o1), F53(?o1), ?t). Initiates(E54(?o1), F54(?o1), ?t). Initiates(E55(?o1), F55(?o1), ?t). Initiates(E56(?o1), F56(?o1), ?t). Initiates(E57(?o1), F57(?o1), ?t). Initiates(E58(?o1), F58(?o1), ?t). Initiates(E59(?o1), F59(?o1), ?t). Initiates(E60(?o1), F60(?o1), ?t). Initiates(E61(?o1), F61(?o1), ?t). Initiates(E62(?o1), F62(?o1), ?t). Initiates(E63(?o1), F63(?o1), ?t). Initiates(E64(?o1), F64(?o1), ?t). Initiates(E65(?o1), F65(?o1), ?t). Initiates(E66(?o1), F66(?o1), ?t). Initiates(E67(?o1), F67(?o1), ?t). Initiates(E68(?o1), F68(?o1), ?t). Initiates(E69(?o1), F69(?o1), ?t). Initiates(E70(?o1), F70(?o1), ?t). Initiates(E71(?o1), F71(?o1), ?t). Initiates(E72(?o1), F72(?o1), ?t). Initiates(E73(?o1), F73(?o1), ?t). Initiates(E74(?o1), F74(?o1), ?t). Initiates(E75(?o1), F75(?o1), ?t). Initiates(E76(?o1), F76(?o1), ?t). Initiates(E77(?o1), F77(?o1), ?t). Initiates(E78(?o1), F78(?o1), ?t). Initiates(E79(?o1), F79(?o1), ?t). Initiates(E80(?o1), F80(?o1), ?t). Initiates(E81(?o1), F81(?o1), ?t). Initiates(E82(?o1), F82(?o1), ?t). Initiates(E83(?o1), F83(?o1), ?t). Initiates(E84(?o1), F84(?o1), ?t). Initiates(E85(?o1), F85(?o1), ?t). Initiates(E86(?o1), F86(?o1), ?t). Initiates(E87(?o1), F87(?o1), ?t). Initiates(E88(?o1), F88(?o1), ?t). Initiates(E89(?o1), F89(?o1), ?t). Initiates(E90(?o1), F90(?o1), ?t). Initiates(E91(?o1), F91(?o1), ?t). Initiates(E92(?o1), F92(?o1), ?t). Initiates(E93(?o1), F93(?o1), ?t). Initiates(E94(?o1), F94(?o1), ?t). Initiates(E95(?o1), F95(?o1), ?t). Initiates(E96(?o1), F96(?o1), ?t). Initiates(E97(?o1), F97(?o1), ?t). Initiates(E98(?o1), F98(?o1), ?t). Initiates(E99(?o1), F99(?o1), ?t). Initiates(E100(?o1), F100(?o1), ?t). Initiates(E101(?o1), F101(?o1), ?t). Initiates(E102(?o1), F102(?o1), ?t). Initiates(E103(?o1), F103(?o1), ?t). Initiates(E104(?o1), F104(?o1), ?t). Initiates(E105(?o1), F105(?o1), ?t). Initiates(E106(?o1), F106(?o1), ?t). Initiates(E107(?o1), F107(?o1), ?t). Initiates(E108(?o1), F108(?o1), ?t). Initiates(E109(?o1), F109(?o1), ?t). Initiates(E110(?o1), F110(?o1), ?t). Initiates(E111(?o1), F111(?o1), ?t). Initiates(E112(?o1), F112(?o1), ?t). Initiates(E113(?o1), F113(?o1), ?t). Initiates(E114(?o1), F114(?o1), ?t). Initiates(E115(?o1), F115(?o1), ?t). Initiates(E116(?o1), F116(?o1), ?t). Initiates(E117(?o1), F117(?o1), ?t). Initiates(E118(?o1), F118(?o1), ?t). Initiates(E119(?o1), F119(?o1), ?t). Initiates(E120(?o1), F120(?o1), ?t). Initiates(E121(?o1), F121(?o1), ?t). Initiates(E122(?o1), F122(?o1), ?t). Initiates(E123(?o1), F123(?o1), ?t). Initiates(E124(?o1), F124(?o1), ?t). Initiates(E125(?o1), F125(?o1), ?t). Initiates(E126(?o1), F126(?o1), ?t). Initiates(E127(?o1), F127(?o1), ?t). Initiates(E128(?o1), F128(?o1), ?t). Initiates(E129(?o1), F129(?o1), ?t). Initiates(E130(?o1), F130(?o1), ?t). Initiates(E131(?o1), F131(?o1), ?t). Initiates(E132(?o1), F132(?o1), ?t). Initiates(E133(?o1), F133(?o1), ?t). Initiates(E134(?o1), F134(?o1), ?t). Initiates(E135(?o1), F135(?o1), ?t). Initiates(E136(?o1), F136(?o1), ?t). Initiates(E137(?o1), F137(?o1), ?t). Initiates(E138(?o1), F138(?o1), ?t). Initiates(E139(?o1), F139(?o1), ?t). Initiates(E140(?o1), F140(?o1), ?t). Initiates(E141(?o1), F141(?o1), ?t). Initiates(E142(?o1), F142(?o1), ?t). Initiates(E143(?o1), F143(?o1), ?t). Initiates(E144(?o1), F144(?o1), ?t). Initiates(E145(?o1), F145(?o1), ?t). Initiates(E146(?o1), F146(?o1), ?t). Initiates(E147(?o1), F147(?o1), ?t). Initiates(E148(?o1), F148(?o1), ?t). Initiates(E149(?o1), F149(?o1), ?t). Initiates(E150(?o1), F150(?o1), ?t). Initiates(E151(?o1), F151(?o1), ?t). Initiates(E152(?o1), F152(?o1), ?t). Initiates(E153(?o1), F153(?o1), ?t). Initiates(E154(?o1), F154(?o1), ?t). Initiates(E155(?o1), F155(?o1), ?t). Initiates(E156(?o1), F156(?o1), ?t). Initiates(E157(?o1), F157(?o1), ?t). Initiates(E158(?o1), F158(?o1), ?t). Initiates(E159(?o1), F159(?o1), ?t). Initiates(E160(?o1), F160(?o1), ?t). Initiates(E161(?o1), F161(?o1), ?t). Initiates(E162(?o1), F162(?o1), ?t). Initiates(E163(?o1), F163(?o1), ?t). Initiates(E164(?o1), F164(?o1), ?t). Initiates(E165(?o1), F165(?o1), ?t). Initiates(E166(?o1), F166(?o1), ?t). Initiates(E167(?o1), F167(?o1), ?t). Initiates(E168(?o1), F168(?o1), ?t). Initiates(E169(?o1), F169(?o1), ?t). Initiates(E170(?o1), F170(?o1), ?t). Initiates(E171(?o1), F171(?o1), ?t). Initiates(E172(?o1), F172(?o1), ?t). Initiates(E173(?o1), F173(?o1), ?t). Initiates(E174(?o1), F174(?o1), ?t). Initiates(E175(?o1), F175(?o1), ?t). Initiates(E176(?o1), F176(?o1), ?t). Initiates(E177(?o1), F177(?o1), ?t). Initiates(E178(?o1), F178(?o1), ?t). Initiates(E179(?o1), F179(?o1), ?t). Initiates(E180(?o1), F180(?o1), ?t). Initiates(E181(?o1), F181(?o1), ?t). Initiates(E182(?o1), F182(?o1), ?t). Initiates(E183(?o1), F183(?o1), ?t). Initiates(E184(?o1), F184(?o1), ?t). Initiates(E185(?o1), F185(?o1), ?t). Initiates(E186(?o1), F186(?o1), ?t). Initiates(E187(?o1), F187(?o1), ?t). Initiates(E188(?o1), F188(?o1), ?t). Initiates(E189(?o1), F189(?o1), ?t). Initiates(E190(?o1), F190(?o1), ?t). Initiates(E191(?o1), F191(?o1), ?t). Initiates(E192(?o1), F192(?o1), ?t). Initiates(E193(?o1), F193(?o1), ?t). Initiates(E194(?o1), F194(?o1), ?t). Initiates(E195(?o1), F195(?o1), ?t). Initiates(E196(?o1), F196(?o1), ?t). Initiates(E197(?o1), F197(?o1), ?t). Initiates(E198(?o1), F198(?o1), ?t). Initiates(E199(?o1), F199(?o1), ?t). Initiates(E200(?o1), F200(?o1), ?t). Initiates(E201(?o1), F201(?o1), ?t). Initiates(E202(?o1), F202(?o1), ?t). Initiates(E203(?o1), F203(?o1), ?t). Initiates(E204(?o1), F204(?o1), ?t). Initiates(E205(?o1), F205(?o1), ?t). Initiates(E206(?o1), F206(?o1), ?t). Initiates(E207(?o1), F207(?o1), ?t). Initiates(E208(?o1), F208(?o1), ?t). Initiates(E209(?o1), F209(?o1), ?t). Initiates(E210(?o1), F210(?o1), ?t). Initiates(E211(?o1), F211(?o1), ?t). Initiates(E212(?o1), F212(?o1), ?t). Initiates(E213(?o1), F213(?o1), ?t). Initiates(E214(?o1), F214(?o1), ?t). Initiates(E215(?o1), F215(?o1), ?t). Initiates(E216(?o1), F216(?o1), ?t). Initiates(E217(?o1), F217(?o1), ?t). Initiates(E218(?o1), F218(?o1), ?t). Initiates(E219(?o1), F219(?o1), ?t). Initiates(E220(?o1), F220(?o1), ?t). Initiates(E221(?o1), F221(?o1), ?t). Initiates(E222(?o1), F222(?o1), ?t). Initiates(E223(?o1), F223(?o1), ?t). Initiates(E224(?o1), F224(?o1), ?t). Initiates(E225(?o1), F225(?o1), ?t). Initiates(E226(?o1), F226(?o1), ?t). Initiates(E227(?o1), F227(?o1), ?t). Initiates(E228(?o1), F228(?o1), ?t). Initiates(E229(?o1), F229(?o1), ?t). Initiates(E230(?o1), F230(?o1), ?t). Initiates(E231(?o1), F231(?o1), ?t). Initiates(E232(?o1), F232(?o1), ?t). Initiates(E233(?o1), F233(?o1), ?t). Initiates(E234(?o1), F234(?o1), ?t). Initiates(E235(?o1), F235(?o1), ?t). Initiates(E236(?o1), F236(?o1), ?t). Initiates(E237(?o1), F237(?o1), ?t). Initiates(E238(?o1), F238(?o1), ?t). Initiates(E239(?o1), F239(?o1), ?t). Initiates(E240(?o1), F240(?o1), ?t). Initiates(E241(?o1), F241(?o1), ?t). Initiates(E242(?o1), F242(?o1), ?t). Initiates(E243(?o1), F243(?o1), ?t). Initiates(E244(?o1), F244(?o1), ?t). Initiates(E245(?o1), F245(?o1), ?t). Initiates(E246(?o1), F246(?o1), ?t). Initiates(E247(?o1), F247(?o1), ?t). Initiates(E248(?o1), F248(?o1), ?t). Initiates(E249(?o1), F249(?o1), ?t). Initiates(E250(?o1), F250(?o1), ?t). Initiates(E251(?o1), F251(?o1), ?t). Initiates(E252(?o1), F252(?o1), ?t). Initiates(E253(?o1), F253(?o1), ?t). Initiates(E254(?o1), F254(?o1), ?t). Initiates(E255(?o1), F255(?o1), ?t). Initiates(E256(?o1), F256(?o1), ?t). Initiates(E257(?o1), F257(?o1), ?t). Initiates(E258(?o1), F258(?o1), ?t). Initiates(E259(?o1), F259(?o1), ?t). Initiates(E260(?o1), F260(?o1), ?t). Initiates(E261(?o1), F261(?o1), ?t). Initiates(E262(?o1), F262(?o1), ?t). Initiates(E263(?o1), F263(?o1), ?t). Initiates(E264(?o1), F264(?o1), ?t). Initiates(E265(?o1), F265(?o1), ?t). Initiates(E266(?o1), F266(?o1), ?t). Initiates(E267(?o1), F267(?o1), ?t). Initiates(E268(?o1), F268(?o1), ?t). Initiates(E269(?o1), F269(?o1), ?t). Initiates(E270(?o1), F270(?o1), ?t). Initiates(E271(?o1), F271(?o1), ?t). Initiates(E272(?o1), F272(?o1), ?t). Initiates(E273(?o1), F273(?o1), ?t). Initiates(E274(?o1), F274(?o1), ?t). Initiates(E275(?o1), F275(?o1), ?t). Initiates(E276(?o1), F276(?o1), ?t). Initiates(E277(?o1), F277(?o1), ?t). Initiates(E278(?o1), F278(?o1), ?t). Initiates(E279(?o1), F279(?o1), ?t). Initiates(E280(?o1), F280(?o1), ?t). Initiates(E281(?o1), F281(?o1), ?t). Initiates(E282(?o1), F282(?o1), ?t). Initiates(E283(?o1), F283(?o1), ?t). Initiates(E284(?o1), F284(?o1), ?t). Initiates(E285(?o1), F285(?o1), ?t). Initiates(E286(?o1), F286(?o1), ?t). Initiates(E287(?o1), F287(?o1), ?t). Initiates(E288(?o1), F288(?o1), ?t). Initiates(E289(?o1), F289(?o1), ?t). Initiates(E290(?o1), F290(?o1), ?t). Initiates(E291(?o1), F291(?o1), ?t). Initiates(E292(?o1), F292(?o1), ?t). Initiates(E293(?o1), F293(?o1), ?t). Initiates(E294(?o1), F294(?o1), ?t). Initiates(E295(?o1), F295(?o1), ?t). Initiates(E296(?o1), F296(?o1), ?t). Initiates(E297(?o1), F297(?o1), ?t). Initiates(E298(?o1), F298(?o1), ?t). Initiates(E299(?o1), F299(?o1), ?t). Initiates(E300(?o1), F300(?o1), ?t). Initiates(E301(?o1), F301(?o1), ?t). Initiates(E302(?o1), F302(?o1), ?t). Initiates(E303(?o1), F303(?o1), ?t). Initiates(E304(?o1), F304(?o1), ?t). Initiates(E305(?o1), F305(?o1), ?t). Initiates(E306(?o1), F306(?o1), ?t). Initiates(E307(?o1), F307(?o1), ?t). Initiates(E308(?o1), F308(?o1), ?t). Initiates(E309(?o1), F309(?o1), ?t). Initiates(E310(?o1), F310(?o1), ?t). Initiates(E311(?o1), F311(?o1), ?t). Initiates(E312(?o1), F312(?o1), ?t). Initiates(E313(?o1), F313(?o1), ?t). Initiates(E314(?o1), F314(?o1), ?t). Initiates(E315(?o1), F315(?o1), ?t). Initiates(E316(?o1), F316(?o1), ?t). Initiates(E317(?o1), F317(?o1), ?t). Initiates(E318(?o1), F318(?o1), ?t). Initiates(E319(?o1), F319(?o1), ?t). Initiates(E320(?o1), F320(?o1), ?t). Initiates(E321(?o1), F321(?o1), ?t). Initiates(E322(?o1), F322(?o1), ?t). Initiates(E323(?o1), F323(?o1), ?t). Initiates(E324(?o1), F324(?o1), ?t). Initiates(E325(?o1), F325(?o1), ?t). Initiates(E326(?o1), F326(?o1), ?t). Initiates(E327(?o1), F327(?o1), ?t). Initiates(E328(?o1), F328(?o1), ?t). Initiates(E329(?o1), F329(?o1), ?t). Initiates(E330(?o1), F330(?o1), ?t). Initiates(E331(?o1), F331(?o1), ?t). Initiates(E332(?o1), F332(?o1), ?t). Initiates(E333(?o1), F333(?o1), ?t). Initiates(E334(?o1), F334(?o1), ?t). Initiates(E335(?o1), F335(?o1), ?t). Initiates(E336(?o1), F336(?o1), ?t). Initiates(E337(?o1), F337(?o1), ?t). Initiates(E338(?o1), F338(?o1), ?t). Initiates(E339(?o1), F339(?o1), ?t). Initiates(E340(?o1), F340(?o1), ?t). Initiates(E341(?o1), F341(?o1), ?t). Initiates(E342(?o1), F342(?o1), ?t). Initiates(E343(?o1), F343(?o1), ?t). Initiates(E344(?o1), F344(?o1), ?t). Initiates(E345(?o1), F345(?o1), ?t). Initiates(E346(?o1), F346(?o1), ?t). Initiates(E347(?o1), F347(?o1), ?t). Initiates(E348(?o1), F348(?o1), ?t). Initiates(E349(?o1), F349(?o1), ?t). Initiates(E350(?o1), F350(?o1), ?t). Initiates(E351(?o1), F351(?o1), ?t). Initiates(E352(?o1), F352(?o1), ?t). Initiates(E353(?o1), F353(?o1), ?t). Initiates(E354(?o1), F354(?o1), ?t). Initiates(E355(?o1), F355(?o1), ?t). Initiates(E356(?o1), F356(?o1), ?t). Initiates(E357(?o1), F357(?o1), ?t). Initiates(E358(?o1), F358(?o1), ?t). Initiates(E359(?o1), F359(?o1), ?t). Initiates(E360(?o1), F360(?o1), ?t). Initiates(E361(?o1), F361(?o1), ?t). Initiates(E362(?o1), F362(?o1), ?t). Initiates(E363(?o1), F363(?o1), ?t). Initiates(E364(?o1), F364(?o1), ?t). Initiates(E365(?o1), F365(?o1), ?t). Initiates(E366(?o1), F366(?o1), ?t). Initiates(E367(?o1), F367(?o1), ?t). Initiates(E368(?o1), F368(?o1), ?t). Initiates(E369(?o1), F369(?o1), ?t). Initiates(E370(?o1), F370(?o1), ?t). Initiates(E371(?o1), F371(?o1), ?t). Initiates(E372(?o1), F372(?o1), ?t). Initiates(E373(?o1), F373(?o1), ?t). Initiates(E374(?o1), F374(?o1), ?t). Initiates(E375(?o1), F375(?o1), ?t). Initiates(E376(?o1), F376(?o1), ?t). Initiates(E377(?o1), F377(?o1), ?t). Initiates(E378(?o1), F378(?o1), ?t). Initiates(E379(?o1), F379(?o1), ?t). Initiates(E380(?o1), F380(?o1), ?t). Initiates(E381(?o1), F381(?o1), ?t). Initiates(E382(?o1), F382(?o1), ?t). Initiates(E383(?o1), F383(?o1), ?t). Initiates(E384(?o1), F384(?o1), ?t). Initiates(E385(?o1), F385(?o1), ?t). Initiates(E386(?o1), F386(?o1), ?t). Initiates(E387(?o1), F387(?o1), ?t). Initiates(E388(?o1), F388(?o1), ?t). Initiates(E389(?o1), F389(?o1), ?t). Initiates(E390(?o1), F390(?o1), ?t). Initiates(E391(?o1), F391(?o1), ?t). Initiates(E392(?o1), F392(?o1), ?t). Initiates(E393(?o1), F393(?o1), ?t). Initiates(E394(?o1), F394(?o1), ?t). Initiates(E395(?o1), F395(?o1), ?t). Initiates(E396(?o1), F396(?o1), ?t). Initiates(E397(?o1), F397(?o1), ?t). Initiates(E398(?o1), F398(?o1), ?t). Initiates(E399(?o1), F399(?o1), ?t). Initiates(E400(?o1), F400(?o1), ?t). Initiates(E401(?o1), F401(?o1), ?t). Initiates(E402(?o1), F402(?o1), ?t). Initiates(E403(?o1), F403(?o1), ?t). Initiates(E404(?o1), F404(?o1), ?t). Initiates(E405(?o1), F405(?o1), ?t). Initiates(E406(?o1), F406(?o1), ?t). Initiates(E407(?o1), F407(?o1), ?t). Initiates(E408(?o1), F408(?o1), ?t). Initiates(E409(?o1), F409(?o1), ?t). Initiates(E410(?o1), F410(?o1), ?t). Initiates(E411(?o1), F411(?o1), ?t). Initiates(E412(?o1), F412(?o1), ?t). Initiates(E413(?o1), F413(?o1), ?t). Initiates(E414(?o1), F414(?o1), ?t). Initiates(E415(?o1), F415(?o1), ?t). Initiates(E416(?o1), F416(?o1), ?t). Initiates(E417(?o1), F417(?o1), ?t). Initiates(E418(?o1), F418(?o1), ?t). Initiates(E419(?o1), F419(?o1), ?t). Initiates(E420(?o1), F420(?o1), ?t). Initiates(E421(?o1), F421(?o1), ?t). Initiates(E422(?o1), F422(?o1), ?t). Initiates(E423(?o1), F423(?o1), ?t). Initiates(E424(?o1), F424(?o1), ?t). Initiates(E425(?o1), F425(?o1), ?t). Initiates(E426(?o1), F426(?o1), ?t). Initiates(E427(?o1), F427(?o1), ?t). Initiates(E428(?o1), F428(?o1), ?t). Initiates(E429(?o1), F429(?o1), ?t). Initiates(E430(?o1), F430(?o1), ?t). Initiates(E431(?o1), F431(?o1), ?t). Initiates(E432(?o1), F432(?o1), ?t). Initiates(E433(?o1), F433(?o1), ?t). Initiates(E434(?o1), F434(?o1), ?t). Initiates(E435(?o1), F435(?o1), ?t). Initiates(E436(?o1), F436(?o1), ?t). Initiates(E437(?o1), F437(?o1), ?t). Initiates(E438(?o1), F438(?o1), ?t). Initiates(E439(?o1), F439(?o1), ?t). Initiates(E440(?o1), F440(?o1), ?t). Initiates(E441(?o1), F441(?o1), ?t). Initiates(E442(?o1), F442(?o1), ?t). Initiates(E443(?o1), F443(?o1), ?t). Initiates(E444(?o1), F444(?o1), ?t). Initiates(E445(?o1), F445(?o1), ?t). Initiates(E446(?o1), F446(?o1), ?t). Initiates(E447(?o1), F447(?o1), ?t). Initiates(E448(?o1), F448(?o1), ?t). Initiates(E449(?o1), F449(?o1), ?t). Initiates(E450(?o1), F450(?o1), ?t). Initiates(E451(?o1), F451(?o1), ?t). Initiates(E452(?o1), F452(?o1), ?t). Initiates(E453(?o1), F453(?o1), ?t). Initiates(E454(?o1), F454(?o1), ?t). Initiates(E455(?o1), F455(?o1), ?t). Initiates(E456(?o1), F456(?o1), ?t). Initiates(E457(?o1), F457(?o1), ?t). Initiates(E458(?o1), F458(?o1), ?t). Initiates(E459(?o1), F459(?o1), ?t). Initiates(E460(?o1), F460(?o1), ?t). Initiates(E461(?o1), F461(?o1), ?t). Initiates(E462(?o1), F462(?o1), ?t). Initiates(E463(?o1), F463(?o1), ?t). Initiates(E464(?o1), F464(?o1), ?t). Initiates(E465(?o1), F465(?o1), ?t). Initiates(E466(?o1), F466(?o1), ?t). Initiates(E467(?o1), F467(?o1), ?t). Initiates(E468(?o1), F468(?o1), ?t). Initiates(E469(?o1), F469(?o1), ?t). Initiates(E470(?o1), F470(?o1), ?t). Initiates(E471(?o1), F471(?o1), ?t). Initiates(E472(?o1), F472(?o1), ?t). Initiates(E473(?o1), F473(?o1), ?t). Initiates(E474(?o1), F474(?o1), ?t). Initiates(E475(?o1), F475(?o1), ?t). Initiates(E476(?o1), F476(?o1), ?t). Initiates(E477(?o1), F477(?o1), ?t). Initiates(E478(?o1), F478(?o1), ?t). Initiates(E479(?o1), F479(?o1), ?t). Initiates(E480(?o1), F480(?o1), ?t). Initiates(E481(?o1), F481(?o1), ?t). Initiates(E482(?o1), F482(?o1), ?t). Initiates(E483(?o1), F483(?o1), ?t). Initiates(E484(?o1), F484(?o1), ?t). Initiates(E485(?o1), F485(?o1), ?t). Initiates(E486(?o1), F486(?o1), ?t). Initiates(E487(?o1), F487(?o1), ?t). Initiates(E488(?o1), F488(?o1), ?t). Initiates(E489(?o1), F489(?o1), ?t). Initiates(E490(?o1), F490(?o1), ?t). Initiates(E491(?o1), F491(?o1), ?t). Initiates(E492(?o1), F492(?o1), ?t). Initiates(E493(?o1), F493(?o1), ?t). Initiates(E494(?o1), F494(?o1), ?t). Initiates(E495(?o1), F495(?o1), ?t). Initiates(E496(?o1), F496(?o1), ?t). Initiates(E497(?o1), F497(?o1), ?t). Initiates(E498(?o1), F498(?o1), ?t). Initiates(E499(?o1), F499(?o1), ?t). Initiates(E500(?o1), F500(?o1), ?t). Terminates(E501(?o1), F501(?o1), ?t). Terminates(E502(?o1), F502(?o1), ?t). Terminates(E503(?o1), F503(?o1), ?t). Terminates(E504(?o1), F504(?o1), ?t). Terminates(E505(?o1), F505(?o1), ?t). Terminates(E506(?o1), F506(?o1), ?t). Terminates(E507(?o1), F507(?o1), ?t). Terminates(E508(?o1), F508(?o1), ?t). Terminates(E509(?o1), F509(?o1), ?t). Terminates(E510(?o1), F510(?o1), ?t). Terminates(E511(?o1), F511(?o1), ?t). Terminates(E512(?o1), F512(?o1), ?t). Terminates(E513(?o1), F513(?o1), ?t). Terminates(E514(?o1), F514(?o1), ?t). Terminates(E515(?o1), F515(?o1), ?t). Terminates(E516(?o1), F516(?o1), ?t). Terminates(E517(?o1), F517(?o1), ?t). Terminates(E518(?o1), F518(?o1), ?t). Terminates(E519(?o1), F519(?o1), ?t). Terminates(E520(?o1), F520(?o1), ?t). Terminates(E521(?o1), F521(?o1), ?t). Terminates(E522(?o1), F522(?o1), ?t). Terminates(E523(?o1), F523(?o1), ?t). Terminates(E524(?o1), F524(?o1), ?t). Terminates(E525(?o1), F525(?o1), ?t). Terminates(E526(?o1), F526(?o1), ?t). Terminates(E527(?o1), F527(?o1), ?t). Terminates(E528(?o1), F528(?o1), ?t). Terminates(E529(?o1), F529(?o1), ?t). Terminates(E530(?o1), F530(?o1), ?t). Terminates(E531(?o1), F531(?o1), ?t). Terminates(E532(?o1), F532(?o1), ?t). Terminates(E533(?o1), F533(?o1), ?t). Terminates(E534(?o1), F534(?o1), ?t). Terminates(E535(?o1), F535(?o1), ?t). Terminates(E536(?o1), F536(?o1), ?t). Terminates(E537(?o1), F537(?o1), ?t). Terminates(E538(?o1), F538(?o1), ?t). Terminates(E539(?o1), F539(?o1), ?t). Terminates(E540(?o1), F540(?o1), ?t). Terminates(E541(?o1), F541(?o1), ?t). Terminates(E542(?o1), F542(?o1), ?t). Terminates(E543(?o1), F543(?o1), ?t). Terminates(E544(?o1), F544(?o1), ?t). Terminates(E545(?o1), F545(?o1), ?t). Terminates(E546(?o1), F546(?o1), ?t). Terminates(E547(?o1), F547(?o1), ?t). Terminates(E548(?o1), F548(?o1), ?t). Terminates(E549(?o1), F549(?o1), ?t). Terminates(E550(?o1), F550(?o1), ?t). Terminates(E551(?o1), F551(?o1), ?t). Terminates(E552(?o1), F552(?o1), ?t). Terminates(E553(?o1), F553(?o1), ?t). Terminates(E554(?o1), F554(?o1), ?t). Terminates(E555(?o1), F555(?o1), ?t). Terminates(E556(?o1), F556(?o1), ?t). Terminates(E557(?o1), F557(?o1), ?t). Terminates(E558(?o1), F558(?o1), ?t). Terminates(E559(?o1), F559(?o1), ?t). Terminates(E560(?o1), F560(?o1), ?t). Terminates(E561(?o1), F561(?o1), ?t). Terminates(E562(?o1), F562(?o1), ?t). Terminates(E563(?o1), F563(?o1), ?t). Terminates(E564(?o1), F564(?o1), ?t). Terminates(E565(?o1), F565(?o1), ?t). Terminates(E566(?o1), F566(?o1), ?t). Terminates(E567(?o1), F567(?o1), ?t). Terminates(E568(?o1), F568(?o1), ?t). Terminates(E569(?o1), F569(?o1), ?t). Terminates(E570(?o1), F570(?o1), ?t). Terminates(E571(?o1), F571(?o1), ?t). Terminates(E572(?o1), F572(?o1), ?t). Terminates(E573(?o1), F573(?o1), ?t). Terminates(E574(?o1), F574(?o1), ?t). Terminates(E575(?o1), F575(?o1), ?t). Terminates(E576(?o1), F576(?o1), ?t). Terminates(E577(?o1), F577(?o1), ?t). Terminates(E578(?o1), F578(?o1), ?t). Terminates(E579(?o1), F579(?o1), ?t). Terminates(E580(?o1), F580(?o1), ?t). Terminates(E581(?o1), F581(?o1), ?t). Terminates(E582(?o1), F582(?o1), ?t). Terminates(E583(?o1), F583(?o1), ?t). Terminates(E584(?o1), F584(?o1), ?t). Terminates(E585(?o1), F585(?o1), ?t). Terminates(E586(?o1), F586(?o1), ?t). Terminates(E587(?o1), F587(?o1), ?t). Terminates(E588(?o1), F588(?o1), ?t). Terminates(E589(?o1), F589(?o1), ?t). Terminates(E590(?o1), F590(?o1), ?t). Terminates(E591(?o1), F591(?o1), ?t). Terminates(E592(?o1), F592(?o1), ?t). Terminates(E593(?o1), F593(?o1), ?t). Terminates(E594(?o1), F594(?o1), ?t). Terminates(E595(?o1), F595(?o1), ?t). Terminates(E596(?o1), F596(?o1), ?t). Terminates(E597(?o1), F597(?o1), ?t). Terminates(E598(?o1), F598(?o1), ?t). Terminates(E599(?o1), F599(?o1), ?t). Terminates(E600(?o1), F600(?o1), ?t). Terminates(E601(?o1), F601(?o1), ?t). Terminates(E602(?o1), F602(?o1), ?t). Terminates(E603(?o1), F603(?o1), ?t). Terminates(E604(?o1), F604(?o1), ?t). Terminates(E605(?o1), F605(?o1), ?t). Terminates(E606(?o1), F606(?o1), ?t). Terminates(E607(?o1), F607(?o1), ?t). Terminates(E608(?o1), F608(?o1), ?t). Terminates(E609(?o1), F609(?o1), ?t). Terminates(E610(?o1), F610(?o1), ?t). Terminates(E611(?o1), F611(?o1), ?t). Terminates(E612(?o1), F612(?o1), ?t). Terminates(E613(?o1), F613(?o1), ?t). Terminates(E614(?o1), F614(?o1), ?t). Terminates(E615(?o1), F615(?o1), ?t). Terminates(E616(?o1), F616(?o1), ?t). Terminates(E617(?o1), F617(?o1), ?t). Terminates(E618(?o1), F618(?o1), ?t). Terminates(E619(?o1), F619(?o1), ?t). Terminates(E620(?o1), F620(?o1), ?t). Terminates(E621(?o1), F621(?o1), ?t). Terminates(E622(?o1), F622(?o1), ?t). Terminates(E623(?o1), F623(?o1), ?t). Terminates(E624(?o1), F624(?o1), ?t). Terminates(E625(?o1), F625(?o1), ?t). Terminates(E626(?o1), F626(?o1), ?t). Terminates(E627(?o1), F627(?o1), ?t). Terminates(E628(?o1), F628(?o1), ?t). Terminates(E629(?o1), F629(?o1), ?t). Terminates(E630(?o1), F630(?o1), ?t). Terminates(E631(?o1), F631(?o1), ?t). Terminates(E632(?o1), F632(?o1), ?t). Terminates(E633(?o1), F633(?o1), ?t). Terminates(E634(?o1), F634(?o1), ?t). Terminates(E635(?o1), F635(?o1), ?t). Terminates(E636(?o1), F636(?o1), ?t). Terminates(E637(?o1), F637(?o1), ?t). Terminates(E638(?o1), F638(?o1), ?t). Terminates(E639(?o1), F639(?o1), ?t). Terminates(E640(?o1), F640(?o1), ?t). Terminates(E641(?o1), F641(?o1), ?t). Terminates(E642(?o1), F642(?o1), ?t). Terminates(E643(?o1), F643(?o1), ?t). Terminates(E644(?o1), F644(?o1), ?t). Terminates(E645(?o1), F645(?o1), ?t). Terminates(E646(?o1), F646(?o1), ?t). Terminates(E647(?o1), F647(?o1), ?t). Terminates(E648(?o1), F648(?o1), ?t). Terminates(E649(?o1), F649(?o1), ?t). Terminates(E650(?o1), F650(?o1), ?t). Terminates(E651(?o1), F651(?o1), ?t). Terminates(E652(?o1), F652(?o1), ?t). Terminates(E653(?o1), F653(?o1), ?t). Terminates(E654(?o1), F654(?o1), ?t). Terminates(E655(?o1), F655(?o1), ?t). Terminates(E656(?o1), F656(?o1), ?t). Terminates(E657(?o1), F657(?o1), ?t). Terminates(E658(?o1), F658(?o1), ?t). Terminates(E659(?o1), F659(?o1), ?t). Terminates(E660(?o1), F660(?o1), ?t). Terminates(E661(?o1), F661(?o1), ?t). Terminates(E662(?o1), F662(?o1), ?t). Terminates(E663(?o1), F663(?o1), ?t). Terminates(E664(?o1), F664(?o1), ?t). Terminates(E665(?o1), F665(?o1), ?t). Terminates(E666(?o1), F666(?o1), ?t). Terminates(E667(?o1), F667(?o1), ?t). Terminates(E668(?o1), F668(?o1), ?t). Terminates(E669(?o1), F669(?o1), ?t). Terminates(E670(?o1), F670(?o1), ?t). Terminates(E671(?o1), F671(?o1), ?t). Terminates(E672(?o1), F672(?o1), ?t). Terminates(E673(?o1), F673(?o1), ?t). Terminates(E674(?o1), F674(?o1), ?t). Terminates(E675(?o1), F675(?o1), ?t). Terminates(E676(?o1), F676(?o1), ?t). Terminates(E677(?o1), F677(?o1), ?t). Terminates(E678(?o1), F678(?o1), ?t). Terminates(E679(?o1), F679(?o1), ?t). Terminates(E680(?o1), F680(?o1), ?t). Terminates(E681(?o1), F681(?o1), ?t). Terminates(E682(?o1), F682(?o1), ?t). Terminates(E683(?o1), F683(?o1), ?t). Terminates(E684(?o1), F684(?o1), ?t). Terminates(E685(?o1), F685(?o1), ?t). Terminates(E686(?o1), F686(?o1), ?t). Terminates(E687(?o1), F687(?o1), ?t). Terminates(E688(?o1), F688(?o1), ?t). Terminates(E689(?o1), F689(?o1), ?t). Terminates(E690(?o1), F690(?o1), ?t). Terminates(E691(?o1), F691(?o1), ?t). Terminates(E692(?o1), F692(?o1), ?t). Terminates(E693(?o1), F693(?o1), ?t). Terminates(E694(?o1), F694(?o1), ?t). Terminates(E695(?o1), F695(?o1), ?t). Terminates(E696(?o1), F696(?o1), ?t). Terminates(E697(?o1), F697(?o1), ?t). Terminates(E698(?o1), F698(?o1), ?t). Terminates(E699(?o1), F699(?o1), ?t). Terminates(E700(?o1), F700(?o1), ?t). Terminates(E701(?o1), F701(?o1), ?t). Terminates(E702(?o1), F702(?o1), ?t). Terminates(E703(?o1), F703(?o1), ?t). Terminates(E704(?o1), F704(?o1), ?t). Terminates(E705(?o1), F705(?o1), ?t). Terminates(E706(?o1), F706(?o1), ?t). Terminates(E707(?o1), F707(?o1), ?t). Terminates(E708(?o1), F708(?o1), ?t). Terminates(E709(?o1), F709(?o1), ?t). Terminates(E710(?o1), F710(?o1), ?t). Terminates(E711(?o1), F711(?o1), ?t). Terminates(E712(?o1), F712(?o1), ?t). Terminates(E713(?o1), F713(?o1), ?t). Terminates(E714(?o1), F714(?o1), ?t). Terminates(E715(?o1), F715(?o1), ?t). Terminates(E716(?o1), F716(?o1), ?t). Terminates(E717(?o1), F717(?o1), ?t). Terminates(E718(?o1), F718(?o1), ?t). Terminates(E719(?o1), F719(?o1), ?t). Terminates(E720(?o1), F720(?o1), ?t). Terminates(E721(?o1), F721(?o1), ?t). Terminates(E722(?o1), F722(?o1), ?t). Terminates(E723(?o1), F723(?o1), ?t). Terminates(E724(?o1), F724(?o1), ?t). Terminates(E725(?o1), F725(?o1), ?t). Terminates(E726(?o1), F726(?o1), ?t). Terminates(E727(?o1), F727(?o1), ?t). Terminates(E728(?o1), F728(?o1), ?t). Terminates(E729(?o1), F729(?o1), ?t). Terminates(E730(?o1), F730(?o1), ?t). Terminates(E731(?o1), F731(?o1), ?t). Terminates(E732(?o1), F732(?o1), ?t). Terminates(E733(?o1), F733(?o1), ?t). Terminates(E734(?o1), F734(?o1), ?t). Terminates(E735(?o1), F735(?o1), ?t). Terminates(E736(?o1), F736(?o1), ?t). Terminates(E737(?o1), F737(?o1), ?t). Terminates(E738(?o1), F738(?o1), ?t). Terminates(E739(?o1), F739(?o1), ?t). Terminates(E740(?o1), F740(?o1), ?t). Terminates(E741(?o1), F741(?o1), ?t). Terminates(E742(?o1), F742(?o1), ?t). Terminates(E743(?o1), F743(?o1), ?t). Terminates(E744(?o1), F744(?o1), ?t). Terminates(E745(?o1), F745(?o1), ?t). Terminates(E746(?o1), F746(?o1), ?t). Terminates(E747(?o1), F747(?o1), ?t). Terminates(E748(?o1), F748(?o1), ?t). Terminates(E749(?o1), F749(?o1), ?t). Terminates(E750(?o1), F750(?o1), ?t). Terminates(E751(?o1), F751(?o1), ?t). Terminates(E752(?o1), F752(?o1), ?t). Terminates(E753(?o1), F753(?o1), ?t). Terminates(E754(?o1), F754(?o1), ?t). Terminates(E755(?o1), F755(?o1), ?t). Terminates(E756(?o1), F756(?o1), ?t). Terminates(E757(?o1), F757(?o1), ?t). Terminates(E758(?o1), F758(?o1), ?t). Terminates(E759(?o1), F759(?o1), ?t). Terminates(E760(?o1), F760(?o1), ?t). Terminates(E761(?o1), F761(?o1), ?t). Terminates(E762(?o1), F762(?o1), ?t). Terminates(E763(?o1), F763(?o1), ?t). Terminates(E764(?o1), F764(?o1), ?t). Terminates(E765(?o1), F765(?o1), ?t). Terminates(E766(?o1), F766(?o1), ?t). Terminates(E767(?o1), F767(?o1), ?t). Terminates(E768(?o1), F768(?o1), ?t). Terminates(E769(?o1), F769(?o1), ?t). Terminates(E770(?o1), F770(?o1), ?t). Terminates(E771(?o1), F771(?o1), ?t). Terminates(E772(?o1), F772(?o1), ?t). Terminates(E773(?o1), F773(?o1), ?t). Terminates(E774(?o1), F774(?o1), ?t). Terminates(E775(?o1), F775(?o1), ?t). Terminates(E776(?o1), F776(?o1), ?t). Terminates(E777(?o1), F777(?o1), ?t). Terminates(E778(?o1), F778(?o1), ?t). Terminates(E779(?o1), F779(?o1), ?t). Terminates(E780(?o1), F780(?o1), ?t). Terminates(E781(?o1), F781(?o1), ?t). Terminates(E782(?o1), F782(?o1), ?t). Terminates(E783(?o1), F783(?o1), ?t). Terminates(E784(?o1), F784(?o1), ?t). Terminates(E785(?o1), F785(?o1), ?t). Terminates(E786(?o1), F786(?o1), ?t). Terminates(E787(?o1), F787(?o1), ?t). Terminates(E788(?o1), F788(?o1), ?t). Terminates(E789(?o1), F789(?o1), ?t). Terminates(E790(?o1), F790(?o1), ?t). Terminates(E791(?o1), F791(?o1), ?t). Terminates(E792(?o1), F792(?o1), ?t). Terminates(E793(?o1), F793(?o1), ?t). Terminates(E794(?o1), F794(?o1), ?t). Terminates(E795(?o1), F795(?o1), ?t). Terminates(E796(?o1), F796(?o1), ?t). Terminates(E797(?o1), F797(?o1), ?t). Terminates(E798(?o1), F798(?o1), ?t). Terminates(E799(?o1), F799(?o1), ?t). Terminates(E800(?o1), F800(?o1), ?t). Terminates(E801(?o1), F801(?o1), ?t). Terminates(E802(?o1), F802(?o1), ?t). Terminates(E803(?o1), F803(?o1), ?t). Terminates(E804(?o1), F804(?o1), ?t). Terminates(E805(?o1), F805(?o1), ?t). Terminates(E806(?o1), F806(?o1), ?t). Terminates(E807(?o1), F807(?o1), ?t). Terminates(E808(?o1), F808(?o1), ?t). Terminates(E809(?o1), F809(?o1), ?t). Terminates(E810(?o1), F810(?o1), ?t). Terminates(E811(?o1), F811(?o1), ?t). Terminates(E812(?o1), F812(?o1), ?t). Terminates(E813(?o1), F813(?o1), ?t). Terminates(E814(?o1), F814(?o1), ?t). Terminates(E815(?o1), F815(?o1), ?t). Terminates(E816(?o1), F816(?o1), ?t). Terminates(E817(?o1), F817(?o1), ?t). Terminates(E818(?o1), F818(?o1), ?t). Terminates(E819(?o1), F819(?o1), ?t). Terminates(E820(?o1), F820(?o1), ?t). Terminates(E821(?o1), F821(?o1), ?t). Terminates(E822(?o1), F822(?o1), ?t). Terminates(E823(?o1), F823(?o1), ?t). Terminates(E824(?o1), F824(?o1), ?t). Terminates(E825(?o1), F825(?o1), ?t). Terminates(E826(?o1), F826(?o1), ?t). Terminates(E827(?o1), F827(?o1), ?t). Terminates(E828(?o1), F828(?o1), ?t). Terminates(E829(?o1), F829(?o1), ?t). Terminates(E830(?o1), F830(?o1), ?t). Terminates(E831(?o1), F831(?o1), ?t). Terminates(E832(?o1), F832(?o1), ?t). Terminates(E833(?o1), F833(?o1), ?t). Terminates(E834(?o1), F834(?o1), ?t). Terminates(E835(?o1), F835(?o1), ?t). Terminates(E836(?o1), F836(?o1), ?t). Terminates(E837(?o1), F837(?o1), ?t). Terminates(E838(?o1), F838(?o1), ?t). Terminates(E839(?o1), F839(?o1), ?t). Terminates(E840(?o1), F840(?o1), ?t). Terminates(E841(?o1), F841(?o1), ?t). Terminates(E842(?o1), F842(?o1), ?t). Terminates(E843(?o1), F843(?o1), ?t). Terminates(E844(?o1), F844(?o1), ?t). Terminates(E845(?o1), F845(?o1), ?t). Terminates(E846(?o1), F846(?o1), ?t). Terminates(E847(?o1), F847(?o1), ?t). Terminates(E848(?o1), F848(?o1), ?t). Terminates(E849(?o1), F849(?o1), ?t). Terminates(E850(?o1), F850(?o1), ?t). Terminates(E851(?o1), F851(?o1), ?t). Terminates(E852(?o1), F852(?o1), ?t). Terminates(E853(?o1), F853(?o1), ?t). Terminates(E854(?o1), F854(?o1), ?t). Terminates(E855(?o1), F855(?o1), ?t). Terminates(E856(?o1), F856(?o1), ?t). Terminates(E857(?o1), F857(?o1), ?t). Terminates(E858(?o1), F858(?o1), ?t). Terminates(E859(?o1), F859(?o1), ?t). Terminates(E860(?o1), F860(?o1), ?t). Terminates(E861(?o1), F861(?o1), ?t). Terminates(E862(?o1), F862(?o1), ?t). Terminates(E863(?o1), F863(?o1), ?t). Terminates(E864(?o1), F864(?o1), ?t). Terminates(E865(?o1), F865(?o1), ?t). Terminates(E866(?o1), F866(?o1), ?t). Terminates(E867(?o1), F867(?o1), ?t). Terminates(E868(?o1), F868(?o1), ?t). Terminates(E869(?o1), F869(?o1), ?t). Terminates(E870(?o1), F870(?o1), ?t). Terminates(E871(?o1), F871(?o1), ?t). Terminates(E872(?o1), F872(?o1), ?t). Terminates(E873(?o1), F873(?o1), ?t). Terminates(E874(?o1), F874(?o1), ?t). Terminates(E875(?o1), F875(?o1), ?t). Terminates(E876(?o1), F876(?o1), ?t). Terminates(E877(?o1), F877(?o1), ?t). Terminates(E878(?o1), F878(?o1), ?t). Terminates(E879(?o1), F879(?o1), ?t). Terminates(E880(?o1), F880(?o1), ?t). Terminates(E881(?o1), F881(?o1), ?t). Terminates(E882(?o1), F882(?o1), ?t). Terminates(E883(?o1), F883(?o1), ?t). Terminates(E884(?o1), F884(?o1), ?t). Terminates(E885(?o1), F885(?o1), ?t). Terminates(E886(?o1), F886(?o1), ?t). Terminates(E887(?o1), F887(?o1), ?t). Terminates(E888(?o1), F888(?o1), ?t). Terminates(E889(?o1), F889(?o1), ?t). Terminates(E890(?o1), F890(?o1), ?t). Terminates(E891(?o1), F891(?o1), ?t). Terminates(E892(?o1), F892(?o1), ?t). Terminates(E893(?o1), F893(?o1), ?t). Terminates(E894(?o1), F894(?o1), ?t). Terminates(E895(?o1), F895(?o1), ?t). Terminates(E896(?o1), F896(?o1), ?t). Terminates(E897(?o1), F897(?o1), ?t). Terminates(E898(?o1), F898(?o1), ?t). Terminates(E899(?o1), F899(?o1), ?t). Terminates(E900(?o1), F900(?o1), ?t). Terminates(E901(?o1), F901(?o1), ?t). Terminates(E902(?o1), F902(?o1), ?t). Terminates(E903(?o1), F903(?o1), ?t). Terminates(E904(?o1), F904(?o1), ?t). Terminates(E905(?o1), F905(?o1), ?t). Terminates(E906(?o1), F906(?o1), ?t). Terminates(E907(?o1), F907(?o1), ?t). Terminates(E908(?o1), F908(?o1), ?t). Terminates(E909(?o1), F909(?o1), ?t). Terminates(E910(?o1), F910(?o1), ?t). Terminates(E911(?o1), F911(?o1), ?t). Terminates(E912(?o1), F912(?o1), ?t). Terminates(E913(?o1), F913(?o1), ?t). Terminates(E914(?o1), F914(?o1), ?t). Terminates(E915(?o1), F915(?o1), ?t). Terminates(E916(?o1), F916(?o1), ?t). Terminates(E917(?o1), F917(?o1), ?t). Terminates(E918(?o1), F918(?o1), ?t). Terminates(E919(?o1), F919(?o1), ?t). Terminates(E920(?o1), F920(?o1), ?t). Terminates(E921(?o1), F921(?o1), ?t). Terminates(E922(?o1), F922(?o1), ?t). Terminates(E923(?o1), F923(?o1), ?t). Terminates(E924(?o1), F924(?o1), ?t). Terminates(E925(?o1), F925(?o1), ?t). Terminates(E926(?o1), F926(?o1), ?t). Terminates(E927(?o1), F927(?o1), ?t). Terminates(E928(?o1), F928(?o1), ?t). Terminates(E929(?o1), F929(?o1), ?t). Terminates(E930(?o1), F930(?o1), ?t). Terminates(E931(?o1), F931(?o1), ?t). Terminates(E932(?o1), F932(?o1), ?t). Terminates(E933(?o1), F933(?o1), ?t). Terminates(E934(?o1), F934(?o1), ?t). Terminates(E935(?o1), F935(?o1), ?t). Terminates(E936(?o1), F936(?o1), ?t). Terminates(E937(?o1), F937(?o1), ?t). Terminates(E938(?o1), F938(?o1), ?t). Terminates(E939(?o1), F939(?o1), ?t). Terminates(E940(?o1), F940(?o1), ?t). Terminates(E941(?o1), F941(?o1), ?t). Terminates(E942(?o1), F942(?o1), ?t). Terminates(E943(?o1), F943(?o1), ?t). Terminates(E944(?o1), F944(?o1), ?t). Terminates(E945(?o1), F945(?o1), ?t). Terminates(E946(?o1), F946(?o1), ?t). Terminates(E947(?o1), F947(?o1), ?t). Terminates(E948(?o1), F948(?o1), ?t). Terminates(E949(?o1), F949(?o1), ?t). Terminates(E950(?o1), F950(?o1), ?t). Terminates(E951(?o1), F951(?o1), ?t). Terminates(E952(?o1), F952(?o1), ?t). Terminates(E953(?o1), F953(?o1), ?t). Terminates(E954(?o1), F954(?o1), ?t). Terminates(E955(?o1), F955(?o1), ?t). Terminates(E956(?o1), F956(?o1), ?t). Terminates(E957(?o1), F957(?o1), ?t). Terminates(E958(?o1), F958(?o1), ?t). Terminates(E959(?o1), F959(?o1), ?t). Terminates(E960(?o1), F960(?o1), ?t). Terminates(E961(?o1), F961(?o1), ?t). Terminates(E962(?o1), F962(?o1), ?t). Terminates(E963(?o1), F963(?o1), ?t). Terminates(E964(?o1), F964(?o1), ?t). Terminates(E965(?o1), F965(?o1), ?t). Terminates(E966(?o1), F966(?o1), ?t). Terminates(E967(?o1), F967(?o1), ?t). Terminates(E968(?o1), F968(?o1), ?t). Terminates(E969(?o1), F969(?o1), ?t). Terminates(E970(?o1), F970(?o1), ?t). Terminates(E971(?o1), F971(?o1), ?t). Terminates(E972(?o1), F972(?o1), ?t). Terminates(E973(?o1), F973(?o1), ?t). Terminates(E974(?o1), F974(?o1), ?t). Terminates(E975(?o1), F975(?o1), ?t). Terminates(E976(?o1), F976(?o1), ?t). Terminates(E977(?o1), F977(?o1), ?t). Terminates(E978(?o1), F978(?o1), ?t). Terminates(E979(?o1), F979(?o1), ?t). Terminates(E980(?o1), F980(?o1), ?t). Terminates(E981(?o1), F981(?o1), ?t). Terminates(E982(?o1), F982(?o1), ?t). Terminates(E983(?o1), F983(?o1), ?t). Terminates(E984(?o1), F984(?o1), ?t). Terminates(E985(?o1), F985(?o1), ?t). Terminates(E986(?o1), F986(?o1), ?t). Terminates(E987(?o1), F987(?o1), ?t). Terminates(E988(?o1), F988(?o1), ?t). Terminates(E989(?o1), F989(?o1), ?t). Terminates(E990(?o1), F990(?o1), ?t). Terminates(E991(?o1), F991(?o1), ?t). Terminates(E992(?o1), F992(?o1), ?t). Terminates(E993(?o1), F993(?o1), ?t). Terminates(E994(?o1), F994(?o1), ?t). Terminates(E995(?o1), F995(?o1), ?t). Terminates(E996(?o1), F996(?o1), ?t). Terminates(E997(?o1), F997(?o1), ?t). Terminates(E998(?o1), F998(?o1), ?t). Terminates(E999(?o1), F999(?o1), ?t). Terminates(E1000(?o1), F1000(?o1), ?t). Terminates(E(?o1), F1(?o1), ?t). Terminates(E(?o1), F2(?o1), ?t). Terminates(E(?o1), F3(?o1), ?t). Terminates(E(?o1), F4(?o1), ?t). Terminates(E(?o1), F5(?o1), ?t). Terminates(E(?o1), F6(?o1), ?t). Terminates(E(?o1), F7(?o1), ?t). Terminates(E(?o1), F8(?o1), ?t). Terminates(E(?o1), F9(?o1), ?t). Terminates(E(?o1), F10(?o1), ?t). Terminates(E(?o1), F11(?o1), ?t). Terminates(E(?o1), F12(?o1), ?t). Terminates(E(?o1), F13(?o1), ?t). Terminates(E(?o1), F14(?o1), ?t). Terminates(E(?o1), F15(?o1), ?t). Terminates(E(?o1), F16(?o1), ?t). Terminates(E(?o1), F17(?o1), ?t). Terminates(E(?o1), F18(?o1), ?t). Terminates(E(?o1), F19(?o1), ?t). Terminates(E(?o1), F20(?o1), ?t). Terminates(E(?o1), F21(?o1), ?t). Terminates(E(?o1), F22(?o1), ?t). Terminates(E(?o1), F23(?o1), ?t). Terminates(E(?o1), F24(?o1), ?t). Terminates(E(?o1), F25(?o1), ?t). Terminates(E(?o1), F26(?o1), ?t). Terminates(E(?o1), F27(?o1), ?t). Terminates(E(?o1), F28(?o1), ?t). Terminates(E(?o1), F29(?o1), ?t). Terminates(E(?o1), F30(?o1), ?t). Terminates(E(?o1), F31(?o1), ?t). Terminates(E(?o1), F32(?o1), ?t). Terminates(E(?o1), F33(?o1), ?t). Terminates(E(?o1), F34(?o1), ?t). Terminates(E(?o1), F35(?o1), ?t). Terminates(E(?o1), F36(?o1), ?t). Terminates(E(?o1), F37(?o1), ?t). Terminates(E(?o1), F38(?o1), ?t). Terminates(E(?o1), F39(?o1), ?t). Terminates(E(?o1), F40(?o1), ?t). Terminates(E(?o1), F41(?o1), ?t). Terminates(E(?o1), F42(?o1), ?t). Terminates(E(?o1), F43(?o1), ?t). Terminates(E(?o1), F44(?o1), ?t). Terminates(E(?o1), F45(?o1), ?t). Terminates(E(?o1), F46(?o1), ?t). Terminates(E(?o1), F47(?o1), ?t). Terminates(E(?o1), F48(?o1), ?t). Terminates(E(?o1), F49(?o1), ?t). Terminates(E(?o1), F50(?o1), ?t). Terminates(E(?o1), F51(?o1), ?t). Terminates(E(?o1), F52(?o1), ?t). Terminates(E(?o1), F53(?o1), ?t). Terminates(E(?o1), F54(?o1), ?t). Terminates(E(?o1), F55(?o1), ?t). Terminates(E(?o1), F56(?o1), ?t). Terminates(E(?o1), F57(?o1), ?t). Terminates(E(?o1), F58(?o1), ?t). Terminates(E(?o1), F59(?o1), ?t). Terminates(E(?o1), F60(?o1), ?t). Terminates(E(?o1), F61(?o1), ?t). Terminates(E(?o1), F62(?o1), ?t). Terminates(E(?o1), F63(?o1), ?t). Terminates(E(?o1), F64(?o1), ?t). Terminates(E(?o1), F65(?o1), ?t). Terminates(E(?o1), F66(?o1), ?t). Terminates(E(?o1), F67(?o1), ?t). Terminates(E(?o1), F68(?o1), ?t). Terminates(E(?o1), F69(?o1), ?t). Terminates(E(?o1), F70(?o1), ?t). Terminates(E(?o1), F71(?o1), ?t). Terminates(E(?o1), F72(?o1), ?t). Terminates(E(?o1), F73(?o1), ?t). Terminates(E(?o1), F74(?o1), ?t). Terminates(E(?o1), F75(?o1), ?t). Terminates(E(?o1), F76(?o1), ?t). Terminates(E(?o1), F77(?o1), ?t). Terminates(E(?o1), F78(?o1), ?t). Terminates(E(?o1), F79(?o1), ?t). Terminates(E(?o1), F80(?o1), ?t). Terminates(E(?o1), F81(?o1), ?t). Terminates(E(?o1), F82(?o1), ?t). Terminates(E(?o1), F83(?o1), ?t). Terminates(E(?o1), F84(?o1), ?t). Terminates(E(?o1), F85(?o1), ?t). Terminates(E(?o1), F86(?o1), ?t). Terminates(E(?o1), F87(?o1), ?t). Terminates(E(?o1), F88(?o1), ?t). Terminates(E(?o1), F89(?o1), ?t). Terminates(E(?o1), F90(?o1), ?t). Terminates(E(?o1), F91(?o1), ?t). Terminates(E(?o1), F92(?o1), ?t). Terminates(E(?o1), F93(?o1), ?t). Terminates(E(?o1), F94(?o1), ?t). Terminates(E(?o1), F95(?o1), ?t). Terminates(E(?o1), F96(?o1), ?t). Terminates(E(?o1), F97(?o1), ?t). Terminates(E(?o1), F98(?o1), ?t). Terminates(E(?o1), F99(?o1), ?t). Terminates(E(?o1), F100(?o1), ?t). Terminates(E(?o1), F101(?o1), ?t). Terminates(E(?o1), F102(?o1), ?t). Terminates(E(?o1), F103(?o1), ?t). Terminates(E(?o1), F104(?o1), ?t). Terminates(E(?o1), F105(?o1), ?t). Terminates(E(?o1), F106(?o1), ?t). Terminates(E(?o1), F107(?o1), ?t). Terminates(E(?o1), F108(?o1), ?t). Terminates(E(?o1), F109(?o1), ?t). Terminates(E(?o1), F110(?o1), ?t). Terminates(E(?o1), F111(?o1), ?t). Terminates(E(?o1), F112(?o1), ?t). Terminates(E(?o1), F113(?o1), ?t). Terminates(E(?o1), F114(?o1), ?t). Terminates(E(?o1), F115(?o1), ?t). Terminates(E(?o1), F116(?o1), ?t). Terminates(E(?o1), F117(?o1), ?t). Terminates(E(?o1), F118(?o1), ?t). Terminates(E(?o1), F119(?o1), ?t). Terminates(E(?o1), F120(?o1), ?t). Terminates(E(?o1), F121(?o1), ?t). Terminates(E(?o1), F122(?o1), ?t). Terminates(E(?o1), F123(?o1), ?t). Terminates(E(?o1), F124(?o1), ?t). Terminates(E(?o1), F125(?o1), ?t). Terminates(E(?o1), F126(?o1), ?t). Terminates(E(?o1), F127(?o1), ?t). Terminates(E(?o1), F128(?o1), ?t). Terminates(E(?o1), F129(?o1), ?t). Terminates(E(?o1), F130(?o1), ?t). Terminates(E(?o1), F131(?o1), ?t). Terminates(E(?o1), F132(?o1), ?t). Terminates(E(?o1), F133(?o1), ?t). Terminates(E(?o1), F134(?o1), ?t). Terminates(E(?o1), F135(?o1), ?t). Terminates(E(?o1), F136(?o1), ?t). Terminates(E(?o1), F137(?o1), ?t). Terminates(E(?o1), F138(?o1), ?t). Terminates(E(?o1), F139(?o1), ?t). Terminates(E(?o1), F140(?o1), ?t). Terminates(E(?o1), F141(?o1), ?t). Terminates(E(?o1), F142(?o1), ?t). Terminates(E(?o1), F143(?o1), ?t). Terminates(E(?o1), F144(?o1), ?t). Terminates(E(?o1), F145(?o1), ?t). Terminates(E(?o1), F146(?o1), ?t). Terminates(E(?o1), F147(?o1), ?t). Terminates(E(?o1), F148(?o1), ?t). Terminates(E(?o1), F149(?o1), ?t). Terminates(E(?o1), F150(?o1), ?t). Terminates(E(?o1), F151(?o1), ?t). Terminates(E(?o1), F152(?o1), ?t). Terminates(E(?o1), F153(?o1), ?t). Terminates(E(?o1), F154(?o1), ?t). Terminates(E(?o1), F155(?o1), ?t). Terminates(E(?o1), F156(?o1), ?t). Terminates(E(?o1), F157(?o1), ?t). Terminates(E(?o1), F158(?o1), ?t). Terminates(E(?o1), F159(?o1), ?t). Terminates(E(?o1), F160(?o1), ?t). Terminates(E(?o1), F161(?o1), ?t). Terminates(E(?o1), F162(?o1), ?t). Terminates(E(?o1), F163(?o1), ?t). Terminates(E(?o1), F164(?o1), ?t). Terminates(E(?o1), F165(?o1), ?t). Terminates(E(?o1), F166(?o1), ?t). Terminates(E(?o1), F167(?o1), ?t). Terminates(E(?o1), F168(?o1), ?t). Terminates(E(?o1), F169(?o1), ?t). Terminates(E(?o1), F170(?o1), ?t). Terminates(E(?o1), F171(?o1), ?t). Terminates(E(?o1), F172(?o1), ?t). Terminates(E(?o1), F173(?o1), ?t). Terminates(E(?o1), F174(?o1), ?t). Terminates(E(?o1), F175(?o1), ?t). Terminates(E(?o1), F176(?o1), ?t). Terminates(E(?o1), F177(?o1), ?t). Terminates(E(?o1), F178(?o1), ?t). Terminates(E(?o1), F179(?o1), ?t). Terminates(E(?o1), F180(?o1), ?t). Terminates(E(?o1), F181(?o1), ?t). Terminates(E(?o1), F182(?o1), ?t). Terminates(E(?o1), F183(?o1), ?t). Terminates(E(?o1), F184(?o1), ?t). Terminates(E(?o1), F185(?o1), ?t). Terminates(E(?o1), F186(?o1), ?t). Terminates(E(?o1), F187(?o1), ?t). Terminates(E(?o1), F188(?o1), ?t). Terminates(E(?o1), F189(?o1), ?t). Terminates(E(?o1), F190(?o1), ?t). Terminates(E(?o1), F191(?o1), ?t). Terminates(E(?o1), F192(?o1), ?t). Terminates(E(?o1), F193(?o1), ?t). Terminates(E(?o1), F194(?o1), ?t). Terminates(E(?o1), F195(?o1), ?t). Terminates(E(?o1), F196(?o1), ?t). Terminates(E(?o1), F197(?o1), ?t). Terminates(E(?o1), F198(?o1), ?t). Terminates(E(?o1), F199(?o1), ?t). Terminates(E(?o1), F200(?o1), ?t). Terminates(E(?o1), F201(?o1), ?t). Terminates(E(?o1), F202(?o1), ?t). Terminates(E(?o1), F203(?o1), ?t). Terminates(E(?o1), F204(?o1), ?t). Terminates(E(?o1), F205(?o1), ?t). Terminates(E(?o1), F206(?o1), ?t). Terminates(E(?o1), F207(?o1), ?t). Terminates(E(?o1), F208(?o1), ?t). Terminates(E(?o1), F209(?o1), ?t). Terminates(E(?o1), F210(?o1), ?t). Terminates(E(?o1), F211(?o1), ?t). Terminates(E(?o1), F212(?o1), ?t). Terminates(E(?o1), F213(?o1), ?t). Terminates(E(?o1), F214(?o1), ?t). Terminates(E(?o1), F215(?o1), ?t). Terminates(E(?o1), F216(?o1), ?t). Terminates(E(?o1), F217(?o1), ?t). Terminates(E(?o1), F218(?o1), ?t). Terminates(E(?o1), F219(?o1), ?t). Terminates(E(?o1), F220(?o1), ?t). Terminates(E(?o1), F221(?o1), ?t). Terminates(E(?o1), F222(?o1), ?t). Terminates(E(?o1), F223(?o1), ?t). Terminates(E(?o1), F224(?o1), ?t). Terminates(E(?o1), F225(?o1), ?t). Terminates(E(?o1), F226(?o1), ?t). Terminates(E(?o1), F227(?o1), ?t). Terminates(E(?o1), F228(?o1), ?t). Terminates(E(?o1), F229(?o1), ?t). Terminates(E(?o1), F230(?o1), ?t). Terminates(E(?o1), F231(?o1), ?t). Terminates(E(?o1), F232(?o1), ?t). Terminates(E(?o1), F233(?o1), ?t). Terminates(E(?o1), F234(?o1), ?t). Terminates(E(?o1), F235(?o1), ?t). Terminates(E(?o1), F236(?o1), ?t). Terminates(E(?o1), F237(?o1), ?t). Terminates(E(?o1), F238(?o1), ?t). Terminates(E(?o1), F239(?o1), ?t). Terminates(E(?o1), F240(?o1), ?t). Terminates(E(?o1), F241(?o1), ?t). Terminates(E(?o1), F242(?o1), ?t). Terminates(E(?o1), F243(?o1), ?t). Terminates(E(?o1), F244(?o1), ?t). Terminates(E(?o1), F245(?o1), ?t). Terminates(E(?o1), F246(?o1), ?t). Terminates(E(?o1), F247(?o1), ?t). Terminates(E(?o1), F248(?o1), ?t). Terminates(E(?o1), F249(?o1), ?t). Terminates(E(?o1), F250(?o1), ?t). Terminates(E(?o1), F251(?o1), ?t). Terminates(E(?o1), F252(?o1), ?t). Terminates(E(?o1), F253(?o1), ?t). Terminates(E(?o1), F254(?o1), ?t). Terminates(E(?o1), F255(?o1), ?t). Terminates(E(?o1), F256(?o1), ?t). Terminates(E(?o1), F257(?o1), ?t). Terminates(E(?o1), F258(?o1), ?t). Terminates(E(?o1), F259(?o1), ?t). Terminates(E(?o1), F260(?o1), ?t). Terminates(E(?o1), F261(?o1), ?t). Terminates(E(?o1), F262(?o1), ?t). Terminates(E(?o1), F263(?o1), ?t). Terminates(E(?o1), F264(?o1), ?t). Terminates(E(?o1), F265(?o1), ?t). Terminates(E(?o1), F266(?o1), ?t). Terminates(E(?o1), F267(?o1), ?t). Terminates(E(?o1), F268(?o1), ?t). Terminates(E(?o1), F269(?o1), ?t). Terminates(E(?o1), F270(?o1), ?t). Terminates(E(?o1), F271(?o1), ?t). Terminates(E(?o1), F272(?o1), ?t). Terminates(E(?o1), F273(?o1), ?t). Terminates(E(?o1), F274(?o1), ?t). Terminates(E(?o1), F275(?o1), ?t). Terminates(E(?o1), F276(?o1), ?t). Terminates(E(?o1), F277(?o1), ?t). Terminates(E(?o1), F278(?o1), ?t). Terminates(E(?o1), F279(?o1), ?t). Terminates(E(?o1), F280(?o1), ?t). Terminates(E(?o1), F281(?o1), ?t). Terminates(E(?o1), F282(?o1), ?t). Terminates(E(?o1), F283(?o1), ?t). Terminates(E(?o1), F284(?o1), ?t). Terminates(E(?o1), F285(?o1), ?t). Terminates(E(?o1), F286(?o1), ?t). Terminates(E(?o1), F287(?o1), ?t). Terminates(E(?o1), F288(?o1), ?t). Terminates(E(?o1), F289(?o1), ?t). Terminates(E(?o1), F290(?o1), ?t). Terminates(E(?o1), F291(?o1), ?t). Terminates(E(?o1), F292(?o1), ?t). Terminates(E(?o1), F293(?o1), ?t). Terminates(E(?o1), F294(?o1), ?t). Terminates(E(?o1), F295(?o1), ?t). Terminates(E(?o1), F296(?o1), ?t). Terminates(E(?o1), F297(?o1), ?t). Terminates(E(?o1), F298(?o1), ?t). Terminates(E(?o1), F299(?o1), ?t). Terminates(E(?o1), F300(?o1), ?t). Terminates(E(?o1), F301(?o1), ?t). Terminates(E(?o1), F302(?o1), ?t). Terminates(E(?o1), F303(?o1), ?t). Terminates(E(?o1), F304(?o1), ?t). Terminates(E(?o1), F305(?o1), ?t). Terminates(E(?o1), F306(?o1), ?t). Terminates(E(?o1), F307(?o1), ?t). Terminates(E(?o1), F308(?o1), ?t). Terminates(E(?o1), F309(?o1), ?t). Terminates(E(?o1), F310(?o1), ?t). Terminates(E(?o1), F311(?o1), ?t). Terminates(E(?o1), F312(?o1), ?t). Terminates(E(?o1), F313(?o1), ?t). Terminates(E(?o1), F314(?o1), ?t). Terminates(E(?o1), F315(?o1), ?t). Terminates(E(?o1), F316(?o1), ?t). Terminates(E(?o1), F317(?o1), ?t). Terminates(E(?o1), F318(?o1), ?t). Terminates(E(?o1), F319(?o1), ?t). Terminates(E(?o1), F320(?o1), ?t). Terminates(E(?o1), F321(?o1), ?t). Terminates(E(?o1), F322(?o1), ?t). Terminates(E(?o1), F323(?o1), ?t). Terminates(E(?o1), F324(?o1), ?t). Terminates(E(?o1), F325(?o1), ?t). Terminates(E(?o1), F326(?o1), ?t). Terminates(E(?o1), F327(?o1), ?t). Terminates(E(?o1), F328(?o1), ?t). Terminates(E(?o1), F329(?o1), ?t). Terminates(E(?o1), F330(?o1), ?t). Terminates(E(?o1), F331(?o1), ?t). Terminates(E(?o1), F332(?o1), ?t). Terminates(E(?o1), F333(?o1), ?t). Terminates(E(?o1), F334(?o1), ?t). Terminates(E(?o1), F335(?o1), ?t). Terminates(E(?o1), F336(?o1), ?t). Terminates(E(?o1), F337(?o1), ?t). Terminates(E(?o1), F338(?o1), ?t). Terminates(E(?o1), F339(?o1), ?t). Terminates(E(?o1), F340(?o1), ?t). Terminates(E(?o1), F341(?o1), ?t). Terminates(E(?o1), F342(?o1), ?t). Terminates(E(?o1), F343(?o1), ?t). Terminates(E(?o1), F344(?o1), ?t). Terminates(E(?o1), F345(?o1), ?t). Terminates(E(?o1), F346(?o1), ?t). Terminates(E(?o1), F347(?o1), ?t). Terminates(E(?o1), F348(?o1), ?t). Terminates(E(?o1), F349(?o1), ?t). Terminates(E(?o1), F350(?o1), ?t). Terminates(E(?o1), F351(?o1), ?t). Terminates(E(?o1), F352(?o1), ?t). Terminates(E(?o1), F353(?o1), ?t). Terminates(E(?o1), F354(?o1), ?t). Terminates(E(?o1), F355(?o1), ?t). Terminates(E(?o1), F356(?o1), ?t). Terminates(E(?o1), F357(?o1), ?t). Terminates(E(?o1), F358(?o1), ?t). Terminates(E(?o1), F359(?o1), ?t). Terminates(E(?o1), F360(?o1), ?t). Terminates(E(?o1), F361(?o1), ?t). Terminates(E(?o1), F362(?o1), ?t). Terminates(E(?o1), F363(?o1), ?t). Terminates(E(?o1), F364(?o1), ?t). Terminates(E(?o1), F365(?o1), ?t). Terminates(E(?o1), F366(?o1), ?t). Terminates(E(?o1), F367(?o1), ?t). Terminates(E(?o1), F368(?o1), ?t). Terminates(E(?o1), F369(?o1), ?t). Terminates(E(?o1), F370(?o1), ?t). Terminates(E(?o1), F371(?o1), ?t). Terminates(E(?o1), F372(?o1), ?t). Terminates(E(?o1), F373(?o1), ?t). Terminates(E(?o1), F374(?o1), ?t). Terminates(E(?o1), F375(?o1), ?t). Terminates(E(?o1), F376(?o1), ?t). Terminates(E(?o1), F377(?o1), ?t). Terminates(E(?o1), F378(?o1), ?t). Terminates(E(?o1), F379(?o1), ?t). Terminates(E(?o1), F380(?o1), ?t). Terminates(E(?o1), F381(?o1), ?t). Terminates(E(?o1), F382(?o1), ?t). Terminates(E(?o1), F383(?o1), ?t). Terminates(E(?o1), F384(?o1), ?t). Terminates(E(?o1), F385(?o1), ?t). Terminates(E(?o1), F386(?o1), ?t). Terminates(E(?o1), F387(?o1), ?t). Terminates(E(?o1), F388(?o1), ?t). Terminates(E(?o1), F389(?o1), ?t). Terminates(E(?o1), F390(?o1), ?t). Terminates(E(?o1), F391(?o1), ?t). Terminates(E(?o1), F392(?o1), ?t). Terminates(E(?o1), F393(?o1), ?t). Terminates(E(?o1), F394(?o1), ?t). Terminates(E(?o1), F395(?o1), ?t). Terminates(E(?o1), F396(?o1), ?t). Terminates(E(?o1), F397(?o1), ?t). Terminates(E(?o1), F398(?o1), ?t). Terminates(E(?o1), F399(?o1), ?t). Terminates(E(?o1), F400(?o1), ?t). Terminates(E(?o1), F401(?o1), ?t). Terminates(E(?o1), F402(?o1), ?t). Terminates(E(?o1), F403(?o1), ?t). Terminates(E(?o1), F404(?o1), ?t). Terminates(E(?o1), F405(?o1), ?t). Terminates(E(?o1), F406(?o1), ?t). Terminates(E(?o1), F407(?o1), ?t). Terminates(E(?o1), F408(?o1), ?t). Terminates(E(?o1), F409(?o1), ?t). Terminates(E(?o1), F410(?o1), ?t). Terminates(E(?o1), F411(?o1), ?t). Terminates(E(?o1), F412(?o1), ?t). Terminates(E(?o1), F413(?o1), ?t). Terminates(E(?o1), F414(?o1), ?t). Terminates(E(?o1), F415(?o1), ?t). Terminates(E(?o1), F416(?o1), ?t). Terminates(E(?o1), F417(?o1), ?t). Terminates(E(?o1), F418(?o1), ?t). Terminates(E(?o1), F419(?o1), ?t). Terminates(E(?o1), F420(?o1), ?t). Terminates(E(?o1), F421(?o1), ?t). Terminates(E(?o1), F422(?o1), ?t). Terminates(E(?o1), F423(?o1), ?t). Terminates(E(?o1), F424(?o1), ?t). Terminates(E(?o1), F425(?o1), ?t). Terminates(E(?o1), F426(?o1), ?t). Terminates(E(?o1), F427(?o1), ?t). Terminates(E(?o1), F428(?o1), ?t). Terminates(E(?o1), F429(?o1), ?t). Terminates(E(?o1), F430(?o1), ?t). Terminates(E(?o1), F431(?o1), ?t). Terminates(E(?o1), F432(?o1), ?t). Terminates(E(?o1), F433(?o1), ?t). Terminates(E(?o1), F434(?o1), ?t). Terminates(E(?o1), F435(?o1), ?t). Terminates(E(?o1), F436(?o1), ?t). Terminates(E(?o1), F437(?o1), ?t). Terminates(E(?o1), F438(?o1), ?t). Terminates(E(?o1), F439(?o1), ?t). Terminates(E(?o1), F440(?o1), ?t). Terminates(E(?o1), F441(?o1), ?t). Terminates(E(?o1), F442(?o1), ?t). Terminates(E(?o1), F443(?o1), ?t). Terminates(E(?o1), F444(?o1), ?t). Terminates(E(?o1), F445(?o1), ?t). Terminates(E(?o1), F446(?o1), ?t). Terminates(E(?o1), F447(?o1), ?t). Terminates(E(?o1), F448(?o1), ?t). Terminates(E(?o1), F449(?o1), ?t). Terminates(E(?o1), F450(?o1), ?t). Terminates(E(?o1), F451(?o1), ?t). Terminates(E(?o1), F452(?o1), ?t). Terminates(E(?o1), F453(?o1), ?t). Terminates(E(?o1), F454(?o1), ?t). Terminates(E(?o1), F455(?o1), ?t). Terminates(E(?o1), F456(?o1), ?t). Terminates(E(?o1), F457(?o1), ?t). Terminates(E(?o1), F458(?o1), ?t). Terminates(E(?o1), F459(?o1), ?t). Terminates(E(?o1), F460(?o1), ?t). Terminates(E(?o1), F461(?o1), ?t). Terminates(E(?o1), F462(?o1), ?t). Terminates(E(?o1), F463(?o1), ?t). Terminates(E(?o1), F464(?o1), ?t). Terminates(E(?o1), F465(?o1), ?t). Terminates(E(?o1), F466(?o1), ?t). Terminates(E(?o1), F467(?o1), ?t). Terminates(E(?o1), F468(?o1), ?t). Terminates(E(?o1), F469(?o1), ?t). Terminates(E(?o1), F470(?o1), ?t). Terminates(E(?o1), F471(?o1), ?t). Terminates(E(?o1), F472(?o1), ?t). Terminates(E(?o1), F473(?o1), ?t). Terminates(E(?o1), F474(?o1), ?t). Terminates(E(?o1), F475(?o1), ?t). Terminates(E(?o1), F476(?o1), ?t). Terminates(E(?o1), F477(?o1), ?t). Terminates(E(?o1), F478(?o1), ?t). Terminates(E(?o1), F479(?o1), ?t). Terminates(E(?o1), F480(?o1), ?t). Terminates(E(?o1), F481(?o1), ?t). Terminates(E(?o1), F482(?o1), ?t). Terminates(E(?o1), F483(?o1), ?t). Terminates(E(?o1), F484(?o1), ?t). Terminates(E(?o1), F485(?o1), ?t). Terminates(E(?o1), F486(?o1), ?t). Terminates(E(?o1), F487(?o1), ?t). Terminates(E(?o1), F488(?o1), ?t). Terminates(E(?o1), F489(?o1), ?t). Terminates(E(?o1), F490(?o1), ?t). Terminates(E(?o1), F491(?o1), ?t). Terminates(E(?o1), F492(?o1), ?t). Terminates(E(?o1), F493(?o1), ?t). Terminates(E(?o1), F494(?o1), ?t). Terminates(E(?o1), F495(?o1), ?t). Terminates(E(?o1), F496(?o1), ?t). Terminates(E(?o1), F497(?o1), ?t). Terminates(E(?o1), F498(?o1), ?t). Terminates(E(?o1), F499(?o1), ?t). Terminates(E(?o1), F500(?o1), ?t). ; %%%% Observations and Narrative ; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% HoldsAt(F1(O1),0). HoldsAt(F2(O1),0). HoldsAt(F3(O1),0). HoldsAt(F4(O1),0). HoldsAt(F5(O1),0). HoldsAt(F6(O1),0). HoldsAt(F7(O1),0). HoldsAt(F8(O1),0). HoldsAt(F9(O1),0). HoldsAt(F10(O1),0). HoldsAt(F11(O1),0). HoldsAt(F12(O1),0). HoldsAt(F13(O1),0). HoldsAt(F14(O1),0). HoldsAt(F15(O1),0). HoldsAt(F16(O1),0). HoldsAt(F17(O1),0). HoldsAt(F18(O1),0). HoldsAt(F19(O1),0). HoldsAt(F20(O1),0). HoldsAt(F21(O1),0). HoldsAt(F22(O1),0). HoldsAt(F23(O1),0). HoldsAt(F24(O1),0). HoldsAt(F25(O1),0). HoldsAt(F26(O1),0). HoldsAt(F27(O1),0). HoldsAt(F28(O1),0). HoldsAt(F29(O1),0). HoldsAt(F30(O1),0). HoldsAt(F31(O1),0). HoldsAt(F32(O1),0). HoldsAt(F33(O1),0). HoldsAt(F34(O1),0). HoldsAt(F35(O1),0). HoldsAt(F36(O1),0). HoldsAt(F37(O1),0). HoldsAt(F38(O1),0). HoldsAt(F39(O1),0). HoldsAt(F40(O1),0). HoldsAt(F41(O1),0). HoldsAt(F42(O1),0). HoldsAt(F43(O1),0). HoldsAt(F44(O1),0). HoldsAt(F45(O1),0). HoldsAt(F46(O1),0). HoldsAt(F47(O1),0). HoldsAt(F48(O1),0). HoldsAt(F49(O1),0). HoldsAt(F50(O1),0). HoldsAt(F51(O1),0). HoldsAt(F52(O1),0). HoldsAt(F53(O1),0). HoldsAt(F54(O1),0). HoldsAt(F55(O1),0). HoldsAt(F56(O1),0). HoldsAt(F57(O1),0). HoldsAt(F58(O1),0). HoldsAt(F59(O1),0). HoldsAt(F60(O1),0). HoldsAt(F61(O1),0). HoldsAt(F62(O1),0). HoldsAt(F63(O1),0). HoldsAt(F64(O1),0). HoldsAt(F65(O1),0). HoldsAt(F66(O1),0). HoldsAt(F67(O1),0). HoldsAt(F68(O1),0). HoldsAt(F69(O1),0). HoldsAt(F70(O1),0). HoldsAt(F71(O1),0). HoldsAt(F72(O1),0). HoldsAt(F73(O1),0). HoldsAt(F74(O1),0). HoldsAt(F75(O1),0). HoldsAt(F76(O1),0). HoldsAt(F77(O1),0). HoldsAt(F78(O1),0). HoldsAt(F79(O1),0). HoldsAt(F80(O1),0). HoldsAt(F81(O1),0). HoldsAt(F82(O1),0). HoldsAt(F83(O1),0). HoldsAt(F84(O1),0). HoldsAt(F85(O1),0). HoldsAt(F86(O1),0). HoldsAt(F87(O1),0). HoldsAt(F88(O1),0). HoldsAt(F89(O1),0). HoldsAt(F90(O1),0). HoldsAt(F91(O1),0). HoldsAt(F92(O1),0). HoldsAt(F93(O1),0). HoldsAt(F94(O1),0). HoldsAt(F95(O1),0). HoldsAt(F96(O1),0). HoldsAt(F97(O1),0). HoldsAt(F98(O1),0). HoldsAt(F99(O1),0). HoldsAt(F100(O1),0). HoldsAt(F101(O1),0). HoldsAt(F102(O1),0). HoldsAt(F103(O1),0). HoldsAt(F104(O1),0). HoldsAt(F105(O1),0). HoldsAt(F106(O1),0). HoldsAt(F107(O1),0). HoldsAt(F108(O1),0). HoldsAt(F109(O1),0). HoldsAt(F110(O1),0). HoldsAt(F111(O1),0). HoldsAt(F112(O1),0). HoldsAt(F113(O1),0). HoldsAt(F114(O1),0). HoldsAt(F115(O1),0). HoldsAt(F116(O1),0). HoldsAt(F117(O1),0). HoldsAt(F118(O1),0). HoldsAt(F119(O1),0). HoldsAt(F120(O1),0). HoldsAt(F121(O1),0). HoldsAt(F122(O1),0). HoldsAt(F123(O1),0). HoldsAt(F124(O1),0). HoldsAt(F125(O1),0). HoldsAt(F126(O1),0). HoldsAt(F127(O1),0). HoldsAt(F128(O1),0). HoldsAt(F129(O1),0). HoldsAt(F130(O1),0). HoldsAt(F131(O1),0). HoldsAt(F132(O1),0). HoldsAt(F133(O1),0). HoldsAt(F134(O1),0). HoldsAt(F135(O1),0). HoldsAt(F136(O1),0). HoldsAt(F137(O1),0). HoldsAt(F138(O1),0). HoldsAt(F139(O1),0). HoldsAt(F140(O1),0). HoldsAt(F141(O1),0). HoldsAt(F142(O1),0). HoldsAt(F143(O1),0). HoldsAt(F144(O1),0). HoldsAt(F145(O1),0). HoldsAt(F146(O1),0). HoldsAt(F147(O1),0). HoldsAt(F148(O1),0). HoldsAt(F149(O1),0). HoldsAt(F150(O1),0). HoldsAt(F151(O1),0). HoldsAt(F152(O1),0). HoldsAt(F153(O1),0). HoldsAt(F154(O1),0). HoldsAt(F155(O1),0). HoldsAt(F156(O1),0). HoldsAt(F157(O1),0). HoldsAt(F158(O1),0). HoldsAt(F159(O1),0). HoldsAt(F160(O1),0). HoldsAt(F161(O1),0). HoldsAt(F162(O1),0). HoldsAt(F163(O1),0). HoldsAt(F164(O1),0). HoldsAt(F165(O1),0). HoldsAt(F166(O1),0). HoldsAt(F167(O1),0). HoldsAt(F168(O1),0). HoldsAt(F169(O1),0). HoldsAt(F170(O1),0). HoldsAt(F171(O1),0). HoldsAt(F172(O1),0). HoldsAt(F173(O1),0). HoldsAt(F174(O1),0). HoldsAt(F175(O1),0). HoldsAt(F176(O1),0). HoldsAt(F177(O1),0). HoldsAt(F178(O1),0). HoldsAt(F179(O1),0). HoldsAt(F180(O1),0). HoldsAt(F181(O1),0). HoldsAt(F182(O1),0). HoldsAt(F183(O1),0). HoldsAt(F184(O1),0). HoldsAt(F185(O1),0). HoldsAt(F186(O1),0). HoldsAt(F187(O1),0). HoldsAt(F188(O1),0). HoldsAt(F189(O1),0). HoldsAt(F190(O1),0). HoldsAt(F191(O1),0). HoldsAt(F192(O1),0). HoldsAt(F193(O1),0). HoldsAt(F194(O1),0). HoldsAt(F195(O1),0). HoldsAt(F196(O1),0). HoldsAt(F197(O1),0). HoldsAt(F198(O1),0). HoldsAt(F199(O1),0). HoldsAt(F200(O1),0). HoldsAt(F201(O1),0). HoldsAt(F202(O1),0). HoldsAt(F203(O1),0). HoldsAt(F204(O1),0). HoldsAt(F205(O1),0). HoldsAt(F206(O1),0). HoldsAt(F207(O1),0). HoldsAt(F208(O1),0). HoldsAt(F209(O1),0). HoldsAt(F210(O1),0). HoldsAt(F211(O1),0). HoldsAt(F212(O1),0). HoldsAt(F213(O1),0). HoldsAt(F214(O1),0). HoldsAt(F215(O1),0). HoldsAt(F216(O1),0). HoldsAt(F217(O1),0). HoldsAt(F218(O1),0). HoldsAt(F219(O1),0). HoldsAt(F220(O1),0). HoldsAt(F221(O1),0). HoldsAt(F222(O1),0). HoldsAt(F223(O1),0). HoldsAt(F224(O1),0). HoldsAt(F225(O1),0). HoldsAt(F226(O1),0). HoldsAt(F227(O1),0). HoldsAt(F228(O1),0). HoldsAt(F229(O1),0). HoldsAt(F230(O1),0). HoldsAt(F231(O1),0). HoldsAt(F232(O1),0). HoldsAt(F233(O1),0). HoldsAt(F234(O1),0). HoldsAt(F235(O1),0). HoldsAt(F236(O1),0). HoldsAt(F237(O1),0). HoldsAt(F238(O1),0). HoldsAt(F239(O1),0). HoldsAt(F240(O1),0). HoldsAt(F241(O1),0). HoldsAt(F242(O1),0). HoldsAt(F243(O1),0). HoldsAt(F244(O1),0). HoldsAt(F245(O1),0). HoldsAt(F246(O1),0). HoldsAt(F247(O1),0). HoldsAt(F248(O1),0). HoldsAt(F249(O1),0). HoldsAt(F250(O1),0). HoldsAt(F251(O1),0). HoldsAt(F252(O1),0). HoldsAt(F253(O1),0). HoldsAt(F254(O1),0). HoldsAt(F255(O1),0). HoldsAt(F256(O1),0). HoldsAt(F257(O1),0). HoldsAt(F258(O1),0). HoldsAt(F259(O1),0). HoldsAt(F260(O1),0). HoldsAt(F261(O1),0). HoldsAt(F262(O1),0). HoldsAt(F263(O1),0). HoldsAt(F264(O1),0). HoldsAt(F265(O1),0). HoldsAt(F266(O1),0). HoldsAt(F267(O1),0). HoldsAt(F268(O1),0). HoldsAt(F269(O1),0). HoldsAt(F270(O1),0). HoldsAt(F271(O1),0). HoldsAt(F272(O1),0). HoldsAt(F273(O1),0). HoldsAt(F274(O1),0). HoldsAt(F275(O1),0). HoldsAt(F276(O1),0). HoldsAt(F277(O1),0). HoldsAt(F278(O1),0). HoldsAt(F279(O1),0). HoldsAt(F280(O1),0). HoldsAt(F281(O1),0). HoldsAt(F282(O1),0). HoldsAt(F283(O1),0). HoldsAt(F284(O1),0). HoldsAt(F285(O1),0). HoldsAt(F286(O1),0). HoldsAt(F287(O1),0). HoldsAt(F288(O1),0). HoldsAt(F289(O1),0). HoldsAt(F290(O1),0). HoldsAt(F291(O1),0). HoldsAt(F292(O1),0). HoldsAt(F293(O1),0). HoldsAt(F294(O1),0). HoldsAt(F295(O1),0). HoldsAt(F296(O1),0). HoldsAt(F297(O1),0). HoldsAt(F298(O1),0). HoldsAt(F299(O1),0). HoldsAt(F300(O1),0). HoldsAt(F301(O1),0). HoldsAt(F302(O1),0). HoldsAt(F303(O1),0). HoldsAt(F304(O1),0). HoldsAt(F305(O1),0). HoldsAt(F306(O1),0). HoldsAt(F307(O1),0). HoldsAt(F308(O1),0). HoldsAt(F309(O1),0). HoldsAt(F310(O1),0). HoldsAt(F311(O1),0). HoldsAt(F312(O1),0). HoldsAt(F313(O1),0). HoldsAt(F314(O1),0). HoldsAt(F315(O1),0). HoldsAt(F316(O1),0). HoldsAt(F317(O1),0). HoldsAt(F318(O1),0). HoldsAt(F319(O1),0). HoldsAt(F320(O1),0). HoldsAt(F321(O1),0). HoldsAt(F322(O1),0). HoldsAt(F323(O1),0). HoldsAt(F324(O1),0). HoldsAt(F325(O1),0). HoldsAt(F326(O1),0). HoldsAt(F327(O1),0). HoldsAt(F328(O1),0). HoldsAt(F329(O1),0). HoldsAt(F330(O1),0). HoldsAt(F331(O1),0). HoldsAt(F332(O1),0). HoldsAt(F333(O1),0). HoldsAt(F334(O1),0). HoldsAt(F335(O1),0). HoldsAt(F336(O1),0). HoldsAt(F337(O1),0). HoldsAt(F338(O1),0). HoldsAt(F339(O1),0). HoldsAt(F340(O1),0). HoldsAt(F341(O1),0). HoldsAt(F342(O1),0). HoldsAt(F343(O1),0). HoldsAt(F344(O1),0). HoldsAt(F345(O1),0). HoldsAt(F346(O1),0). HoldsAt(F347(O1),0). HoldsAt(F348(O1),0). HoldsAt(F349(O1),0). HoldsAt(F350(O1),0). HoldsAt(F351(O1),0). HoldsAt(F352(O1),0). HoldsAt(F353(O1),0). HoldsAt(F354(O1),0). HoldsAt(F355(O1),0). HoldsAt(F356(O1),0). HoldsAt(F357(O1),0). HoldsAt(F358(O1),0). HoldsAt(F359(O1),0). HoldsAt(F360(O1),0). HoldsAt(F361(O1),0). HoldsAt(F362(O1),0). HoldsAt(F363(O1),0). HoldsAt(F364(O1),0). HoldsAt(F365(O1),0). HoldsAt(F366(O1),0). HoldsAt(F367(O1),0). HoldsAt(F368(O1),0). HoldsAt(F369(O1),0). HoldsAt(F370(O1),0). HoldsAt(F371(O1),0). HoldsAt(F372(O1),0). HoldsAt(F373(O1),0). HoldsAt(F374(O1),0). HoldsAt(F375(O1),0). HoldsAt(F376(O1),0). HoldsAt(F377(O1),0). HoldsAt(F378(O1),0). HoldsAt(F379(O1),0). HoldsAt(F380(O1),0). HoldsAt(F381(O1),0). HoldsAt(F382(O1),0). HoldsAt(F383(O1),0). HoldsAt(F384(O1),0). HoldsAt(F385(O1),0). HoldsAt(F386(O1),0). HoldsAt(F387(O1),0). HoldsAt(F388(O1),0). HoldsAt(F389(O1),0). HoldsAt(F390(O1),0). HoldsAt(F391(O1),0). HoldsAt(F392(O1),0). HoldsAt(F393(O1),0). HoldsAt(F394(O1),0). HoldsAt(F395(O1),0). HoldsAt(F396(O1),0). HoldsAt(F397(O1),0). HoldsAt(F398(O1),0). HoldsAt(F399(O1),0). HoldsAt(F400(O1),0). HoldsAt(F401(O1),0). HoldsAt(F402(O1),0). HoldsAt(F403(O1),0). HoldsAt(F404(O1),0). HoldsAt(F405(O1),0). HoldsAt(F406(O1),0). HoldsAt(F407(O1),0). HoldsAt(F408(O1),0). HoldsAt(F409(O1),0). HoldsAt(F410(O1),0). HoldsAt(F411(O1),0). HoldsAt(F412(O1),0). HoldsAt(F413(O1),0). HoldsAt(F414(O1),0). HoldsAt(F415(O1),0). HoldsAt(F416(O1),0). HoldsAt(F417(O1),0). HoldsAt(F418(O1),0). HoldsAt(F419(O1),0). HoldsAt(F420(O1),0). HoldsAt(F421(O1),0). HoldsAt(F422(O1),0). HoldsAt(F423(O1),0). HoldsAt(F424(O1),0). HoldsAt(F425(O1),0). HoldsAt(F426(O1),0). HoldsAt(F427(O1),0). HoldsAt(F428(O1),0). HoldsAt(F429(O1),0). HoldsAt(F430(O1),0). HoldsAt(F431(O1),0). HoldsAt(F432(O1),0). HoldsAt(F433(O1),0). HoldsAt(F434(O1),0). HoldsAt(F435(O1),0). HoldsAt(F436(O1),0). HoldsAt(F437(O1),0). HoldsAt(F438(O1),0). HoldsAt(F439(O1),0). HoldsAt(F440(O1),0). HoldsAt(F441(O1),0). HoldsAt(F442(O1),0). HoldsAt(F443(O1),0). HoldsAt(F444(O1),0). HoldsAt(F445(O1),0). HoldsAt(F446(O1),0). HoldsAt(F447(O1),0). HoldsAt(F448(O1),0). HoldsAt(F449(O1),0). HoldsAt(F450(O1),0). HoldsAt(F451(O1),0). HoldsAt(F452(O1),0). HoldsAt(F453(O1),0). HoldsAt(F454(O1),0). HoldsAt(F455(O1),0). HoldsAt(F456(O1),0). HoldsAt(F457(O1),0). HoldsAt(F458(O1),0). HoldsAt(F459(O1),0). HoldsAt(F460(O1),0). HoldsAt(F461(O1),0). HoldsAt(F462(O1),0). HoldsAt(F463(O1),0). HoldsAt(F464(O1),0). HoldsAt(F465(O1),0). HoldsAt(F466(O1),0). HoldsAt(F467(O1),0). HoldsAt(F468(O1),0). HoldsAt(F469(O1),0). HoldsAt(F470(O1),0). HoldsAt(F471(O1),0). HoldsAt(F472(O1),0). HoldsAt(F473(O1),0). HoldsAt(F474(O1),0). HoldsAt(F475(O1),0). HoldsAt(F476(O1),0). HoldsAt(F477(O1),0). HoldsAt(F478(O1),0). HoldsAt(F479(O1),0). HoldsAt(F480(O1),0). HoldsAt(F481(O1),0). HoldsAt(F482(O1),0). HoldsAt(F483(O1),0). HoldsAt(F484(O1),0). HoldsAt(F485(O1),0). HoldsAt(F486(O1),0). HoldsAt(F487(O1),0). HoldsAt(F488(O1),0). HoldsAt(F489(O1),0). HoldsAt(F490(O1),0). HoldsAt(F491(O1),0). HoldsAt(F492(O1),0). HoldsAt(F493(O1),0). HoldsAt(F494(O1),0). HoldsAt(F495(O1),0). HoldsAt(F496(O1),0). HoldsAt(F497(O1),0). HoldsAt(F498(O1),0). HoldsAt(F499(O1),0). HoldsAt(F500(O1),0). HoldsAt(F501(O1),0). HoldsAt(F502(O1),0). HoldsAt(F503(O1),0). HoldsAt(F504(O1),0). HoldsAt(F505(O1),0). HoldsAt(F506(O1),0). HoldsAt(F507(O1),0). HoldsAt(F508(O1),0). HoldsAt(F509(O1),0). HoldsAt(F510(O1),0). HoldsAt(F511(O1),0). HoldsAt(F512(O1),0). HoldsAt(F513(O1),0). HoldsAt(F514(O1),0). HoldsAt(F515(O1),0). HoldsAt(F516(O1),0). HoldsAt(F517(O1),0). HoldsAt(F518(O1),0). HoldsAt(F519(O1),0). HoldsAt(F520(O1),0). HoldsAt(F521(O1),0). HoldsAt(F522(O1),0). HoldsAt(F523(O1),0). HoldsAt(F524(O1),0). HoldsAt(F525(O1),0). HoldsAt(F526(O1),0). HoldsAt(F527(O1),0). HoldsAt(F528(O1),0). HoldsAt(F529(O1),0). HoldsAt(F530(O1),0). HoldsAt(F531(O1),0). HoldsAt(F532(O1),0). HoldsAt(F533(O1),0). HoldsAt(F534(O1),0). HoldsAt(F535(O1),0). HoldsAt(F536(O1),0). HoldsAt(F537(O1),0). HoldsAt(F538(O1),0). HoldsAt(F539(O1),0). HoldsAt(F540(O1),0). HoldsAt(F541(O1),0). HoldsAt(F542(O1),0). HoldsAt(F543(O1),0). HoldsAt(F544(O1),0). HoldsAt(F545(O1),0). HoldsAt(F546(O1),0). HoldsAt(F547(O1),0). HoldsAt(F548(O1),0). HoldsAt(F549(O1),0). HoldsAt(F550(O1),0). HoldsAt(F551(O1),0). HoldsAt(F552(O1),0). HoldsAt(F553(O1),0). HoldsAt(F554(O1),0). HoldsAt(F555(O1),0). HoldsAt(F556(O1),0). HoldsAt(F557(O1),0). HoldsAt(F558(O1),0). HoldsAt(F559(O1),0). HoldsAt(F560(O1),0). HoldsAt(F561(O1),0). HoldsAt(F562(O1),0). HoldsAt(F563(O1),0). HoldsAt(F564(O1),0). HoldsAt(F565(O1),0). HoldsAt(F566(O1),0). HoldsAt(F567(O1),0). HoldsAt(F568(O1),0). HoldsAt(F569(O1),0). HoldsAt(F570(O1),0). HoldsAt(F571(O1),0). HoldsAt(F572(O1),0). HoldsAt(F573(O1),0). HoldsAt(F574(O1),0). HoldsAt(F575(O1),0). HoldsAt(F576(O1),0). HoldsAt(F577(O1),0). HoldsAt(F578(O1),0). HoldsAt(F579(O1),0). HoldsAt(F580(O1),0). HoldsAt(F581(O1),0). HoldsAt(F582(O1),0). HoldsAt(F583(O1),0). HoldsAt(F584(O1),0). HoldsAt(F585(O1),0). HoldsAt(F586(O1),0). HoldsAt(F587(O1),0). HoldsAt(F588(O1),0). HoldsAt(F589(O1),0). HoldsAt(F590(O1),0). HoldsAt(F591(O1),0). HoldsAt(F592(O1),0). HoldsAt(F593(O1),0). HoldsAt(F594(O1),0). HoldsAt(F595(O1),0). HoldsAt(F596(O1),0). HoldsAt(F597(O1),0). HoldsAt(F598(O1),0). HoldsAt(F599(O1),0). HoldsAt(F600(O1),0). HoldsAt(F601(O1),0). HoldsAt(F602(O1),0). HoldsAt(F603(O1),0). HoldsAt(F604(O1),0). HoldsAt(F605(O1),0). HoldsAt(F606(O1),0). HoldsAt(F607(O1),0). HoldsAt(F608(O1),0). HoldsAt(F609(O1),0). HoldsAt(F610(O1),0). HoldsAt(F611(O1),0). HoldsAt(F612(O1),0). HoldsAt(F613(O1),0). HoldsAt(F614(O1),0). HoldsAt(F615(O1),0). HoldsAt(F616(O1),0). HoldsAt(F617(O1),0). HoldsAt(F618(O1),0). HoldsAt(F619(O1),0). HoldsAt(F620(O1),0). HoldsAt(F621(O1),0). HoldsAt(F622(O1),0). HoldsAt(F623(O1),0). HoldsAt(F624(O1),0). HoldsAt(F625(O1),0). HoldsAt(F626(O1),0). HoldsAt(F627(O1),0). HoldsAt(F628(O1),0). HoldsAt(F629(O1),0). HoldsAt(F630(O1),0). HoldsAt(F631(O1),0). HoldsAt(F632(O1),0). HoldsAt(F633(O1),0). HoldsAt(F634(O1),0). HoldsAt(F635(O1),0). HoldsAt(F636(O1),0). HoldsAt(F637(O1),0). HoldsAt(F638(O1),0). HoldsAt(F639(O1),0). HoldsAt(F640(O1),0). HoldsAt(F641(O1),0). HoldsAt(F642(O1),0). HoldsAt(F643(O1),0). HoldsAt(F644(O1),0). HoldsAt(F645(O1),0). HoldsAt(F646(O1),0). HoldsAt(F647(O1),0). HoldsAt(F648(O1),0). HoldsAt(F649(O1),0). HoldsAt(F650(O1),0). HoldsAt(F651(O1),0). HoldsAt(F652(O1),0). HoldsAt(F653(O1),0). HoldsAt(F654(O1),0). HoldsAt(F655(O1),0). HoldsAt(F656(O1),0). HoldsAt(F657(O1),0). HoldsAt(F658(O1),0). HoldsAt(F659(O1),0). HoldsAt(F660(O1),0). HoldsAt(F661(O1),0). HoldsAt(F662(O1),0). HoldsAt(F663(O1),0). HoldsAt(F664(O1),0). HoldsAt(F665(O1),0). HoldsAt(F666(O1),0). HoldsAt(F667(O1),0). HoldsAt(F668(O1),0). HoldsAt(F669(O1),0). HoldsAt(F670(O1),0). HoldsAt(F671(O1),0). HoldsAt(F672(O1),0). HoldsAt(F673(O1),0). HoldsAt(F674(O1),0). HoldsAt(F675(O1),0). HoldsAt(F676(O1),0). HoldsAt(F677(O1),0). HoldsAt(F678(O1),0). HoldsAt(F679(O1),0). HoldsAt(F680(O1),0). HoldsAt(F681(O1),0). HoldsAt(F682(O1),0). HoldsAt(F683(O1),0). HoldsAt(F684(O1),0). HoldsAt(F685(O1),0). HoldsAt(F686(O1),0). HoldsAt(F687(O1),0). HoldsAt(F688(O1),0). HoldsAt(F689(O1),0). HoldsAt(F690(O1),0). HoldsAt(F691(O1),0). HoldsAt(F692(O1),0). HoldsAt(F693(O1),0). HoldsAt(F694(O1),0). HoldsAt(F695(O1),0). HoldsAt(F696(O1),0). HoldsAt(F697(O1),0). HoldsAt(F698(O1),0). HoldsAt(F699(O1),0). HoldsAt(F700(O1),0). HoldsAt(F701(O1),0). HoldsAt(F702(O1),0). HoldsAt(F703(O1),0). HoldsAt(F704(O1),0). HoldsAt(F705(O1),0). HoldsAt(F706(O1),0). HoldsAt(F707(O1),0). HoldsAt(F708(O1),0). HoldsAt(F709(O1),0). HoldsAt(F710(O1),0). HoldsAt(F711(O1),0). HoldsAt(F712(O1),0). HoldsAt(F713(O1),0). HoldsAt(F714(O1),0). HoldsAt(F715(O1),0). HoldsAt(F716(O1),0). HoldsAt(F717(O1),0). HoldsAt(F718(O1),0). HoldsAt(F719(O1),0). HoldsAt(F720(O1),0). HoldsAt(F721(O1),0). HoldsAt(F722(O1),0). HoldsAt(F723(O1),0). HoldsAt(F724(O1),0). HoldsAt(F725(O1),0). HoldsAt(F726(O1),0). HoldsAt(F727(O1),0). HoldsAt(F728(O1),0). HoldsAt(F729(O1),0). HoldsAt(F730(O1),0). HoldsAt(F731(O1),0). HoldsAt(F732(O1),0). HoldsAt(F733(O1),0). HoldsAt(F734(O1),0). HoldsAt(F735(O1),0). HoldsAt(F736(O1),0). HoldsAt(F737(O1),0). HoldsAt(F738(O1),0). HoldsAt(F739(O1),0). HoldsAt(F740(O1),0). HoldsAt(F741(O1),0). HoldsAt(F742(O1),0). HoldsAt(F743(O1),0). HoldsAt(F744(O1),0). HoldsAt(F745(O1),0). HoldsAt(F746(O1),0). HoldsAt(F747(O1),0). HoldsAt(F748(O1),0). HoldsAt(F749(O1),0). HoldsAt(F750(O1),0). HoldsAt(F751(O1),0). HoldsAt(F752(O1),0). HoldsAt(F753(O1),0). HoldsAt(F754(O1),0). HoldsAt(F755(O1),0). HoldsAt(F756(O1),0). HoldsAt(F757(O1),0). HoldsAt(F758(O1),0). HoldsAt(F759(O1),0). HoldsAt(F760(O1),0). HoldsAt(F761(O1),0). HoldsAt(F762(O1),0). HoldsAt(F763(O1),0). HoldsAt(F764(O1),0). HoldsAt(F765(O1),0). HoldsAt(F766(O1),0). HoldsAt(F767(O1),0). HoldsAt(F768(O1),0). HoldsAt(F769(O1),0). HoldsAt(F770(O1),0). HoldsAt(F771(O1),0). HoldsAt(F772(O1),0). HoldsAt(F773(O1),0). HoldsAt(F774(O1),0). HoldsAt(F775(O1),0). HoldsAt(F776(O1),0). HoldsAt(F777(O1),0). HoldsAt(F778(O1),0). HoldsAt(F779(O1),0). HoldsAt(F780(O1),0). HoldsAt(F781(O1),0). HoldsAt(F782(O1),0). HoldsAt(F783(O1),0). HoldsAt(F784(O1),0). HoldsAt(F785(O1),0). HoldsAt(F786(O1),0). HoldsAt(F787(O1),0). HoldsAt(F788(O1),0). HoldsAt(F789(O1),0). HoldsAt(F790(O1),0). HoldsAt(F791(O1),0). HoldsAt(F792(O1),0). HoldsAt(F793(O1),0). HoldsAt(F794(O1),0). HoldsAt(F795(O1),0). HoldsAt(F796(O1),0). HoldsAt(F797(O1),0). HoldsAt(F798(O1),0). HoldsAt(F799(O1),0). HoldsAt(F800(O1),0). HoldsAt(F801(O1),0). HoldsAt(F802(O1),0). HoldsAt(F803(O1),0). HoldsAt(F804(O1),0). HoldsAt(F805(O1),0). HoldsAt(F806(O1),0). HoldsAt(F807(O1),0). HoldsAt(F808(O1),0). HoldsAt(F809(O1),0). HoldsAt(F810(O1),0). HoldsAt(F811(O1),0). HoldsAt(F812(O1),0). HoldsAt(F813(O1),0). HoldsAt(F814(O1),0). HoldsAt(F815(O1),0). HoldsAt(F816(O1),0). HoldsAt(F817(O1),0). HoldsAt(F818(O1),0). HoldsAt(F819(O1),0). HoldsAt(F820(O1),0). HoldsAt(F821(O1),0). HoldsAt(F822(O1),0). HoldsAt(F823(O1),0). HoldsAt(F824(O1),0). HoldsAt(F825(O1),0). HoldsAt(F826(O1),0). HoldsAt(F827(O1),0). HoldsAt(F828(O1),0). HoldsAt(F829(O1),0). HoldsAt(F830(O1),0). HoldsAt(F831(O1),0). HoldsAt(F832(O1),0). HoldsAt(F833(O1),0). HoldsAt(F834(O1),0). HoldsAt(F835(O1),0). HoldsAt(F836(O1),0). HoldsAt(F837(O1),0). HoldsAt(F838(O1),0). HoldsAt(F839(O1),0). HoldsAt(F840(O1),0). HoldsAt(F841(O1),0). HoldsAt(F842(O1),0). HoldsAt(F843(O1),0). HoldsAt(F844(O1),0). HoldsAt(F845(O1),0). HoldsAt(F846(O1),0). HoldsAt(F847(O1),0). HoldsAt(F848(O1),0). HoldsAt(F849(O1),0). HoldsAt(F850(O1),0). HoldsAt(F851(O1),0). HoldsAt(F852(O1),0). HoldsAt(F853(O1),0). HoldsAt(F854(O1),0). HoldsAt(F855(O1),0). HoldsAt(F856(O1),0). HoldsAt(F857(O1),0). HoldsAt(F858(O1),0). HoldsAt(F859(O1),0). HoldsAt(F860(O1),0). HoldsAt(F861(O1),0). HoldsAt(F862(O1),0). HoldsAt(F863(O1),0). HoldsAt(F864(O1),0). HoldsAt(F865(O1),0). HoldsAt(F866(O1),0). HoldsAt(F867(O1),0). HoldsAt(F868(O1),0). HoldsAt(F869(O1),0). HoldsAt(F870(O1),0). HoldsAt(F871(O1),0). HoldsAt(F872(O1),0). HoldsAt(F873(O1),0). HoldsAt(F874(O1),0). HoldsAt(F875(O1),0). HoldsAt(F876(O1),0). HoldsAt(F877(O1),0). HoldsAt(F878(O1),0). HoldsAt(F879(O1),0). HoldsAt(F880(O1),0). HoldsAt(F881(O1),0). HoldsAt(F882(O1),0). HoldsAt(F883(O1),0). HoldsAt(F884(O1),0). HoldsAt(F885(O1),0). HoldsAt(F886(O1),0). HoldsAt(F887(O1),0). HoldsAt(F888(O1),0). HoldsAt(F889(O1),0). HoldsAt(F890(O1),0). HoldsAt(F891(O1),0). HoldsAt(F892(O1),0). HoldsAt(F893(O1),0). HoldsAt(F894(O1),0). HoldsAt(F895(O1),0). HoldsAt(F896(O1),0). HoldsAt(F897(O1),0). HoldsAt(F898(O1),0). HoldsAt(F899(O1),0). HoldsAt(F900(O1),0). HoldsAt(F901(O1),0). HoldsAt(F902(O1),0). HoldsAt(F903(O1),0). HoldsAt(F904(O1),0). HoldsAt(F905(O1),0). HoldsAt(F906(O1),0). HoldsAt(F907(O1),0). HoldsAt(F908(O1),0). HoldsAt(F909(O1),0). HoldsAt(F910(O1),0). HoldsAt(F911(O1),0). HoldsAt(F912(O1),0). HoldsAt(F913(O1),0). HoldsAt(F914(O1),0). HoldsAt(F915(O1),0). HoldsAt(F916(O1),0). HoldsAt(F917(O1),0). HoldsAt(F918(O1),0). HoldsAt(F919(O1),0). HoldsAt(F920(O1),0). HoldsAt(F921(O1),0). HoldsAt(F922(O1),0). HoldsAt(F923(O1),0). HoldsAt(F924(O1),0). HoldsAt(F925(O1),0). HoldsAt(F926(O1),0). HoldsAt(F927(O1),0). HoldsAt(F928(O1),0). HoldsAt(F929(O1),0). HoldsAt(F930(O1),0). HoldsAt(F931(O1),0). HoldsAt(F932(O1),0). HoldsAt(F933(O1),0). HoldsAt(F934(O1),0). HoldsAt(F935(O1),0). HoldsAt(F936(O1),0). HoldsAt(F937(O1),0). HoldsAt(F938(O1),0). HoldsAt(F939(O1),0). HoldsAt(F940(O1),0). HoldsAt(F941(O1),0). HoldsAt(F942(O1),0). HoldsAt(F943(O1),0). HoldsAt(F944(O1),0). HoldsAt(F945(O1),0). HoldsAt(F946(O1),0). HoldsAt(F947(O1),0). HoldsAt(F948(O1),0). HoldsAt(F949(O1),0). HoldsAt(F950(O1),0). HoldsAt(F951(O1),0). HoldsAt(F952(O1),0). HoldsAt(F953(O1),0). HoldsAt(F954(O1),0). HoldsAt(F955(O1),0). HoldsAt(F956(O1),0). HoldsAt(F957(O1),0). HoldsAt(F958(O1),0). HoldsAt(F959(O1),0). HoldsAt(F960(O1),0). HoldsAt(F961(O1),0). HoldsAt(F962(O1),0). HoldsAt(F963(O1),0). HoldsAt(F964(O1),0). HoldsAt(F965(O1),0). HoldsAt(F966(O1),0). HoldsAt(F967(O1),0). HoldsAt(F968(O1),0). HoldsAt(F969(O1),0). HoldsAt(F970(O1),0). HoldsAt(F971(O1),0). HoldsAt(F972(O1),0). HoldsAt(F973(O1),0). HoldsAt(F974(O1),0). HoldsAt(F975(O1),0). HoldsAt(F976(O1),0). HoldsAt(F977(O1),0). HoldsAt(F978(O1),0). HoldsAt(F979(O1),0). HoldsAt(F980(O1),0). HoldsAt(F981(O1),0). HoldsAt(F982(O1),0). HoldsAt(F983(O1),0). HoldsAt(F984(O1),0). HoldsAt(F985(O1),0). HoldsAt(F986(O1),0). HoldsAt(F987(O1),0). HoldsAt(F988(O1),0). HoldsAt(F989(O1),0). HoldsAt(F990(O1),0). HoldsAt(F991(O1),0). HoldsAt(F992(O1),0). HoldsAt(F993(O1),0). HoldsAt(F994(O1),0). HoldsAt(F995(O1),0). HoldsAt(F996(O1),0). HoldsAt(F997(O1),0). HoldsAt(F998(O1),0). HoldsAt(F999(O1),0). HoldsAt(F1000(O1),0). Happens(E(O1), 0). Happens(E1(?o),3). Happens(E2(?o),3). Happens(E3(?o),3). Happens(E4(?o),3). Happens(E5(?o),3). Happens(E6(?o),3). Happens(E7(?o),3). Happens(E8(?o),3). Happens(E9(?o),3). Happens(E10(?o),3). Happens(E11(?o),3). Happens(E12(?o),3). Happens(E13(?o),3). Happens(E14(?o),3). Happens(E15(?o),3). Happens(E16(?o),3). Happens(E17(?o),3). Happens(E18(?o),3). Happens(E19(?o),3). Happens(E20(?o),3). Happens(E21(?o),3). Happens(E22(?o),3). Happens(E23(?o),3). Happens(E24(?o),3). Happens(E25(?o),3). Happens(E26(?o),3). Happens(E27(?o),3). Happens(E28(?o),3). Happens(E29(?o),3). Happens(E30(?o),3). Happens(E31(?o),3). Happens(E32(?o),3). Happens(E33(?o),3). Happens(E34(?o),3). Happens(E35(?o),3). Happens(E36(?o),3). Happens(E37(?o),3). Happens(E38(?o),3). Happens(E39(?o),3). Happens(E40(?o),3). Happens(E41(?o),3). Happens(E42(?o),3). Happens(E43(?o),3). Happens(E44(?o),3). Happens(E45(?o),3). Happens(E46(?o),3). Happens(E47(?o),3). Happens(E48(?o),3). Happens(E49(?o),3). Happens(E50(?o),3). Happens(E51(?o),3). Happens(E52(?o),3). Happens(E53(?o),3). Happens(E54(?o),3). Happens(E55(?o),3). Happens(E56(?o),3). Happens(E57(?o),3). Happens(E58(?o),3). Happens(E59(?o),3). Happens(E60(?o),3). Happens(E61(?o),3). Happens(E62(?o),3). Happens(E63(?o),3). Happens(E64(?o),3). Happens(E65(?o),3). Happens(E66(?o),3). Happens(E67(?o),3). Happens(E68(?o),3). Happens(E69(?o),3). Happens(E70(?o),3). Happens(E71(?o),3). Happens(E72(?o),3). Happens(E73(?o),3). Happens(E74(?o),3). Happens(E75(?o),3). Happens(E76(?o),3). Happens(E77(?o),3). Happens(E78(?o),3). Happens(E79(?o),3). Happens(E80(?o),3). Happens(E81(?o),3). Happens(E82(?o),3). Happens(E83(?o),3). Happens(E84(?o),3). Happens(E85(?o),3). Happens(E86(?o),3). Happens(E87(?o),3). Happens(E88(?o),3). Happens(E89(?o),3). Happens(E90(?o),3). Happens(E91(?o),3). Happens(E92(?o),3). Happens(E93(?o),3). Happens(E94(?o),3). Happens(E95(?o),3). Happens(E96(?o),3). Happens(E97(?o),3). Happens(E98(?o),3). Happens(E99(?o),3). Happens(E100(?o),3). Happens(E101(?o),3). Happens(E102(?o),3). Happens(E103(?o),3). Happens(E104(?o),3). Happens(E105(?o),3). Happens(E106(?o),3). Happens(E107(?o),3). Happens(E108(?o),3). Happens(E109(?o),3). Happens(E110(?o),3). Happens(E111(?o),3). Happens(E112(?o),3). Happens(E113(?o),3). Happens(E114(?o),3). Happens(E115(?o),3). Happens(E116(?o),3). Happens(E117(?o),3). Happens(E118(?o),3). Happens(E119(?o),3). Happens(E120(?o),3). Happens(E121(?o),3). Happens(E122(?o),3). Happens(E123(?o),3). Happens(E124(?o),3). Happens(E125(?o),3). Happens(E126(?o),3). Happens(E127(?o),3). Happens(E128(?o),3). Happens(E129(?o),3). Happens(E130(?o),3). Happens(E131(?o),3). Happens(E132(?o),3). Happens(E133(?o),3). Happens(E134(?o),3). Happens(E135(?o),3). Happens(E136(?o),3). Happens(E137(?o),3). Happens(E138(?o),3). Happens(E139(?o),3). Happens(E140(?o),3). Happens(E141(?o),3). Happens(E142(?o),3). Happens(E143(?o),3). Happens(E144(?o),3). Happens(E145(?o),3). Happens(E146(?o),3). Happens(E147(?o),3). Happens(E148(?o),3). Happens(E149(?o),3). Happens(E150(?o),3). Happens(E151(?o),3). Happens(E152(?o),3). Happens(E153(?o),3). Happens(E154(?o),3). Happens(E155(?o),3). Happens(E156(?o),3). Happens(E157(?o),3). Happens(E158(?o),3). Happens(E159(?o),3). Happens(E160(?o),3). Happens(E161(?o),3). Happens(E162(?o),3). Happens(E163(?o),3). Happens(E164(?o),3). Happens(E165(?o),3). Happens(E166(?o),3). Happens(E167(?o),3). Happens(E168(?o),3). Happens(E169(?o),3). Happens(E170(?o),3). Happens(E171(?o),3). Happens(E172(?o),3). Happens(E173(?o),3). Happens(E174(?o),3). Happens(E175(?o),3). Happens(E176(?o),3). Happens(E177(?o),3). Happens(E178(?o),3). Happens(E179(?o),3). Happens(E180(?o),3). Happens(E181(?o),3). Happens(E182(?o),3). Happens(E183(?o),3). Happens(E184(?o),3). Happens(E185(?o),3). Happens(E186(?o),3). Happens(E187(?o),3). Happens(E188(?o),3). Happens(E189(?o),3). Happens(E190(?o),3). Happens(E191(?o),3). Happens(E192(?o),3). Happens(E193(?o),3). Happens(E194(?o),3). Happens(E195(?o),3). Happens(E196(?o),3). Happens(E197(?o),3). Happens(E198(?o),3). Happens(E199(?o),3). Happens(E200(?o),3). Happens(E201(?o),3). Happens(E202(?o),3). Happens(E203(?o),3). Happens(E204(?o),3). Happens(E205(?o),3). Happens(E206(?o),3). Happens(E207(?o),3). Happens(E208(?o),3). Happens(E209(?o),3). Happens(E210(?o),3). Happens(E211(?o),3). Happens(E212(?o),3). Happens(E213(?o),3). Happens(E214(?o),3). Happens(E215(?o),3). Happens(E216(?o),3). Happens(E217(?o),3). Happens(E218(?o),3). Happens(E219(?o),3). Happens(E220(?o),3). Happens(E221(?o),3). Happens(E222(?o),3). Happens(E223(?o),3). Happens(E224(?o),3). Happens(E225(?o),3). Happens(E226(?o),3). Happens(E227(?o),3). Happens(E228(?o),3). Happens(E229(?o),3). Happens(E230(?o),3). Happens(E231(?o),3). Happens(E232(?o),3). Happens(E233(?o),3). Happens(E234(?o),3). Happens(E235(?o),3). Happens(E236(?o),3). Happens(E237(?o),3). Happens(E238(?o),3). Happens(E239(?o),3). Happens(E240(?o),3). Happens(E241(?o),3). Happens(E242(?o),3). Happens(E243(?o),3). Happens(E244(?o),3). Happens(E245(?o),3). Happens(E246(?o),3). Happens(E247(?o),3). Happens(E248(?o),3). Happens(E249(?o),3). Happens(E250(?o),3). Happens(E251(?o),3). Happens(E252(?o),3). Happens(E253(?o),3). Happens(E254(?o),3). Happens(E255(?o),3). Happens(E256(?o),3). Happens(E257(?o),3). Happens(E258(?o),3). Happens(E259(?o),3). Happens(E260(?o),3). Happens(E261(?o),3). Happens(E262(?o),3). Happens(E263(?o),3). Happens(E264(?o),3). Happens(E265(?o),3). Happens(E266(?o),3). Happens(E267(?o),3). Happens(E268(?o),3). Happens(E269(?o),3). Happens(E270(?o),3). Happens(E271(?o),3). Happens(E272(?o),3). Happens(E273(?o),3). Happens(E274(?o),3). Happens(E275(?o),3). Happens(E276(?o),3). Happens(E277(?o),3). Happens(E278(?o),3). Happens(E279(?o),3). Happens(E280(?o),3). Happens(E281(?o),3). Happens(E282(?o),3). Happens(E283(?o),3). Happens(E284(?o),3). Happens(E285(?o),3). Happens(E286(?o),3). Happens(E287(?o),3). Happens(E288(?o),3). Happens(E289(?o),3). Happens(E290(?o),3). Happens(E291(?o),3). Happens(E292(?o),3). Happens(E293(?o),3). Happens(E294(?o),3). Happens(E295(?o),3). Happens(E296(?o),3). Happens(E297(?o),3). Happens(E298(?o),3). Happens(E299(?o),3). Happens(E300(?o),3). Happens(E301(?o),3). Happens(E302(?o),3). Happens(E303(?o),3). Happens(E304(?o),3). Happens(E305(?o),3). Happens(E306(?o),3). Happens(E307(?o),3). Happens(E308(?o),3). Happens(E309(?o),3). Happens(E310(?o),3). Happens(E311(?o),3). Happens(E312(?o),3). Happens(E313(?o),3). Happens(E314(?o),3). Happens(E315(?o),3). Happens(E316(?o),3). Happens(E317(?o),3). Happens(E318(?o),3). Happens(E319(?o),3). Happens(E320(?o),3). Happens(E321(?o),3). Happens(E322(?o),3). Happens(E323(?o),3). Happens(E324(?o),3). Happens(E325(?o),3). Happens(E326(?o),3). Happens(E327(?o),3). Happens(E328(?o),3). Happens(E329(?o),3). Happens(E330(?o),3). Happens(E331(?o),3). Happens(E332(?o),3). Happens(E333(?o),3). Happens(E334(?o),3). Happens(E335(?o),3). Happens(E336(?o),3). Happens(E337(?o),3). Happens(E338(?o),3). Happens(E339(?o),3). Happens(E340(?o),3). Happens(E341(?o),3). Happens(E342(?o),3). Happens(E343(?o),3). Happens(E344(?o),3). Happens(E345(?o),3). Happens(E346(?o),3). Happens(E347(?o),3). Happens(E348(?o),3). Happens(E349(?o),3). Happens(E350(?o),3). Happens(E351(?o),3). Happens(E352(?o),3). Happens(E353(?o),3). Happens(E354(?o),3). Happens(E355(?o),3). Happens(E356(?o),3). Happens(E357(?o),3). Happens(E358(?o),3). Happens(E359(?o),3). Happens(E360(?o),3). Happens(E361(?o),3). Happens(E362(?o),3). Happens(E363(?o),3). Happens(E364(?o),3). Happens(E365(?o),3). Happens(E366(?o),3). Happens(E367(?o),3). Happens(E368(?o),3). Happens(E369(?o),3). Happens(E370(?o),3). Happens(E371(?o),3). Happens(E372(?o),3). Happens(E373(?o),3). Happens(E374(?o),3). Happens(E375(?o),3). Happens(E376(?o),3). Happens(E377(?o),3). Happens(E378(?o),3). Happens(E379(?o),3). Happens(E380(?o),3). Happens(E381(?o),3). Happens(E382(?o),3). Happens(E383(?o),3). Happens(E384(?o),3). Happens(E385(?o),3). Happens(E386(?o),3). Happens(E387(?o),3). Happens(E388(?o),3). Happens(E389(?o),3). Happens(E390(?o),3). Happens(E391(?o),3). Happens(E392(?o),3). Happens(E393(?o),3). Happens(E394(?o),3). Happens(E395(?o),3). Happens(E396(?o),3). Happens(E397(?o),3). Happens(E398(?o),3). Happens(E399(?o),3). Happens(E400(?o),3). Happens(E401(?o),3). Happens(E402(?o),3). Happens(E403(?o),3). Happens(E404(?o),3). Happens(E405(?o),3). Happens(E406(?o),3). Happens(E407(?o),3). Happens(E408(?o),3). Happens(E409(?o),3). Happens(E410(?o),3). Happens(E411(?o),3). Happens(E412(?o),3). Happens(E413(?o),3). Happens(E414(?o),3). Happens(E415(?o),3). Happens(E416(?o),3). Happens(E417(?o),3). Happens(E418(?o),3). Happens(E419(?o),3). Happens(E420(?o),3). Happens(E421(?o),3). Happens(E422(?o),3). Happens(E423(?o),3). Happens(E424(?o),3). Happens(E425(?o),3). Happens(E426(?o),3). Happens(E427(?o),3). Happens(E428(?o),3). Happens(E429(?o),3). Happens(E430(?o),3). Happens(E431(?o),3). Happens(E432(?o),3). Happens(E433(?o),3). Happens(E434(?o),3). Happens(E435(?o),3). Happens(E436(?o),3). Happens(E437(?o),3). Happens(E438(?o),3). Happens(E439(?o),3). Happens(E440(?o),3). Happens(E441(?o),3). Happens(E442(?o),3). Happens(E443(?o),3). Happens(E444(?o),3). Happens(E445(?o),3). Happens(E446(?o),3). Happens(E447(?o),3). Happens(E448(?o),3). Happens(E449(?o),3). Happens(E450(?o),3). Happens(E451(?o),3). Happens(E452(?o),3). Happens(E453(?o),3). Happens(E454(?o),3). Happens(E455(?o),3). Happens(E456(?o),3). Happens(E457(?o),3). Happens(E458(?o),3). Happens(E459(?o),3). Happens(E460(?o),3). Happens(E461(?o),3). Happens(E462(?o),3). Happens(E463(?o),3). Happens(E464(?o),3). Happens(E465(?o),3). Happens(E466(?o),3). Happens(E467(?o),3). Happens(E468(?o),3). Happens(E469(?o),3). Happens(E470(?o),3). Happens(E471(?o),3). Happens(E472(?o),3). Happens(E473(?o),3). Happens(E474(?o),3). Happens(E475(?o),3). Happens(E476(?o),3). Happens(E477(?o),3). Happens(E478(?o),3). Happens(E479(?o),3). Happens(E480(?o),3). Happens(E481(?o),3). Happens(E482(?o),3). Happens(E483(?o),3). Happens(E484(?o),3). Happens(E485(?o),3). Happens(E486(?o),3). Happens(E487(?o),3). Happens(E488(?o),3). Happens(E489(?o),3). Happens(E490(?o),3). Happens(E491(?o),3). Happens(E492(?o),3). Happens(E493(?o),3). Happens(E494(?o),3). Happens(E495(?o),3). Happens(E496(?o),3). Happens(E497(?o),3). Happens(E498(?o),3). Happens(E499(?o),3). Happens(E500(?o),3). Happens(E501(?o),3). Happens(E502(?o),3). Happens(E503(?o),3). Happens(E504(?o),3). Happens(E505(?o),3). Happens(E506(?o),3). Happens(E507(?o),3). Happens(E508(?o),3). Happens(E509(?o),3). Happens(E510(?o),3). Happens(E511(?o),3). Happens(E512(?o),3). Happens(E513(?o),3). Happens(E514(?o),3). Happens(E515(?o),3). Happens(E516(?o),3). Happens(E517(?o),3). Happens(E518(?o),3). Happens(E519(?o),3). Happens(E520(?o),3). Happens(E521(?o),3). Happens(E522(?o),3). Happens(E523(?o),3). Happens(E524(?o),3). Happens(E525(?o),3). Happens(E526(?o),3). Happens(E527(?o),3). Happens(E528(?o),3). Happens(E529(?o),3). Happens(E530(?o),3). Happens(E531(?o),3). Happens(E532(?o),3). Happens(E533(?o),3). Happens(E534(?o),3). Happens(E535(?o),3). Happens(E536(?o),3). Happens(E537(?o),3). Happens(E538(?o),3). Happens(E539(?o),3). Happens(E540(?o),3). Happens(E541(?o),3). Happens(E542(?o),3). Happens(E543(?o),3). Happens(E544(?o),3). Happens(E545(?o),3). Happens(E546(?o),3). Happens(E547(?o),3). Happens(E548(?o),3). Happens(E549(?o),3). Happens(E550(?o),3). Happens(E551(?o),3). Happens(E552(?o),3). Happens(E553(?o),3). Happens(E554(?o),3). Happens(E555(?o),3). Happens(E556(?o),3). Happens(E557(?o),3). Happens(E558(?o),3). Happens(E559(?o),3). Happens(E560(?o),3). Happens(E561(?o),3). Happens(E562(?o),3). Happens(E563(?o),3). Happens(E564(?o),3). Happens(E565(?o),3). Happens(E566(?o),3). Happens(E567(?o),3). Happens(E568(?o),3). Happens(E569(?o),3). Happens(E570(?o),3). Happens(E571(?o),3). Happens(E572(?o),3). Happens(E573(?o),3). Happens(E574(?o),3). Happens(E575(?o),3). Happens(E576(?o),3). Happens(E577(?o),3). Happens(E578(?o),3). Happens(E579(?o),3). Happens(E580(?o),3). Happens(E581(?o),3). Happens(E582(?o),3). Happens(E583(?o),3). Happens(E584(?o),3). Happens(E585(?o),3). Happens(E586(?o),3). Happens(E587(?o),3). Happens(E588(?o),3). Happens(E589(?o),3). Happens(E590(?o),3). Happens(E591(?o),3). Happens(E592(?o),3). Happens(E593(?o),3). Happens(E594(?o),3). Happens(E595(?o),3). Happens(E596(?o),3). Happens(E597(?o),3). Happens(E598(?o),3). Happens(E599(?o),3). Happens(E600(?o),3). Happens(E601(?o),3). Happens(E602(?o),3). Happens(E603(?o),3). Happens(E604(?o),3). Happens(E605(?o),3). Happens(E606(?o),3). Happens(E607(?o),3). Happens(E608(?o),3). Happens(E609(?o),3). Happens(E610(?o),3). Happens(E611(?o),3). Happens(E612(?o),3). Happens(E613(?o),3). Happens(E614(?o),3). Happens(E615(?o),3). Happens(E616(?o),3). Happens(E617(?o),3). Happens(E618(?o),3). Happens(E619(?o),3). Happens(E620(?o),3). Happens(E621(?o),3). Happens(E622(?o),3). Happens(E623(?o),3). Happens(E624(?o),3). Happens(E625(?o),3). Happens(E626(?o),3). Happens(E627(?o),3). Happens(E628(?o),3). Happens(E629(?o),3). Happens(E630(?o),3). Happens(E631(?o),3). Happens(E632(?o),3). Happens(E633(?o),3). Happens(E634(?o),3). Happens(E635(?o),3). Happens(E636(?o),3). Happens(E637(?o),3). Happens(E638(?o),3). Happens(E639(?o),3). Happens(E640(?o),3). Happens(E641(?o),3). Happens(E642(?o),3). Happens(E643(?o),3). Happens(E644(?o),3). Happens(E645(?o),3). Happens(E646(?o),3). Happens(E647(?o),3). Happens(E648(?o),3). Happens(E649(?o),3). Happens(E650(?o),3). Happens(E651(?o),3). Happens(E652(?o),3). Happens(E653(?o),3). Happens(E654(?o),3). Happens(E655(?o),3). Happens(E656(?o),3). Happens(E657(?o),3). Happens(E658(?o),3). Happens(E659(?o),3). Happens(E660(?o),3). Happens(E661(?o),3). Happens(E662(?o),3). Happens(E663(?o),3). Happens(E664(?o),3). Happens(E665(?o),3). Happens(E666(?o),3). Happens(E667(?o),3). Happens(E668(?o),3). Happens(E669(?o),3). Happens(E670(?o),3). Happens(E671(?o),3). Happens(E672(?o),3). Happens(E673(?o),3). Happens(E674(?o),3). Happens(E675(?o),3). Happens(E676(?o),3). Happens(E677(?o),3). Happens(E678(?o),3). Happens(E679(?o),3). Happens(E680(?o),3). Happens(E681(?o),3). Happens(E682(?o),3). Happens(E683(?o),3). Happens(E684(?o),3). Happens(E685(?o),3). Happens(E686(?o),3). Happens(E687(?o),3). Happens(E688(?o),3). Happens(E689(?o),3). Happens(E690(?o),3). Happens(E691(?o),3). Happens(E692(?o),3). Happens(E693(?o),3). Happens(E694(?o),3). Happens(E695(?o),3). Happens(E696(?o),3). Happens(E697(?o),3). Happens(E698(?o),3). Happens(E699(?o),3). Happens(E700(?o),3). Happens(E701(?o),3). Happens(E702(?o),3). Happens(E703(?o),3). Happens(E704(?o),3). Happens(E705(?o),3). Happens(E706(?o),3). Happens(E707(?o),3). Happens(E708(?o),3). Happens(E709(?o),3). Happens(E710(?o),3). Happens(E711(?o),3). Happens(E712(?o),3). Happens(E713(?o),3). Happens(E714(?o),3). Happens(E715(?o),3). Happens(E716(?o),3). Happens(E717(?o),3). Happens(E718(?o),3). Happens(E719(?o),3). Happens(E720(?o),3). Happens(E721(?o),3). Happens(E722(?o),3). Happens(E723(?o),3). Happens(E724(?o),3). Happens(E725(?o),3). Happens(E726(?o),3). Happens(E727(?o),3). Happens(E728(?o),3). Happens(E729(?o),3). Happens(E730(?o),3). Happens(E731(?o),3). Happens(E732(?o),3). Happens(E733(?o),3). Happens(E734(?o),3). Happens(E735(?o),3). Happens(E736(?o),3). Happens(E737(?o),3). Happens(E738(?o),3). Happens(E739(?o),3). Happens(E740(?o),3). Happens(E741(?o),3). Happens(E742(?o),3). Happens(E743(?o),3). Happens(E744(?o),3). Happens(E745(?o),3). Happens(E746(?o),3). Happens(E747(?o),3). Happens(E748(?o),3). Happens(E749(?o),3). Happens(E750(?o),3). Happens(E751(?o),3). Happens(E752(?o),3). Happens(E753(?o),3). Happens(E754(?o),3). Happens(E755(?o),3). Happens(E756(?o),3). Happens(E757(?o),3). Happens(E758(?o),3). Happens(E759(?o),3). Happens(E760(?o),3). Happens(E761(?o),3). Happens(E762(?o),3). Happens(E763(?o),3). Happens(E764(?o),3). Happens(E765(?o),3). Happens(E766(?o),3). Happens(E767(?o),3). Happens(E768(?o),3). Happens(E769(?o),3). Happens(E770(?o),3). Happens(E771(?o),3). Happens(E772(?o),3). Happens(E773(?o),3). Happens(E774(?o),3). Happens(E775(?o),3). Happens(E776(?o),3). Happens(E777(?o),3). Happens(E778(?o),3). Happens(E779(?o),3). Happens(E780(?o),3). Happens(E781(?o),3). Happens(E782(?o),3). Happens(E783(?o),3). Happens(E784(?o),3). Happens(E785(?o),3). Happens(E786(?o),3). Happens(E787(?o),3). Happens(E788(?o),3). Happens(E789(?o),3). Happens(E790(?o),3). Happens(E791(?o),3). Happens(E792(?o),3). Happens(E793(?o),3). Happens(E794(?o),3). Happens(E795(?o),3). Happens(E796(?o),3). Happens(E797(?o),3). Happens(E798(?o),3). Happens(E799(?o),3). Happens(E800(?o),3). Happens(E801(?o),3). Happens(E802(?o),3). Happens(E803(?o),3). Happens(E804(?o),3). Happens(E805(?o),3). Happens(E806(?o),3). Happens(E807(?o),3). Happens(E808(?o),3). Happens(E809(?o),3). Happens(E810(?o),3). Happens(E811(?o),3). Happens(E812(?o),3). Happens(E813(?o),3). Happens(E814(?o),3). Happens(E815(?o),3). Happens(E816(?o),3). Happens(E817(?o),3). Happens(E818(?o),3). Happens(E819(?o),3). Happens(E820(?o),3). Happens(E821(?o),3). Happens(E822(?o),3). Happens(E823(?o),3). Happens(E824(?o),3). Happens(E825(?o),3). Happens(E826(?o),3). Happens(E827(?o),3). Happens(E828(?o),3). Happens(E829(?o),3). Happens(E830(?o),3). Happens(E831(?o),3). Happens(E832(?o),3). Happens(E833(?o),3). Happens(E834(?o),3). Happens(E835(?o),3). Happens(E836(?o),3). Happens(E837(?o),3). Happens(E838(?o),3). Happens(E839(?o),3). Happens(E840(?o),3). Happens(E841(?o),3). Happens(E842(?o),3). Happens(E843(?o),3). Happens(E844(?o),3). Happens(E845(?o),3). Happens(E846(?o),3). Happens(E847(?o),3). Happens(E848(?o),3). Happens(E849(?o),3). Happens(E850(?o),3). Happens(E851(?o),3). Happens(E852(?o),3). Happens(E853(?o),3). Happens(E854(?o),3). Happens(E855(?o),3). Happens(E856(?o),3). Happens(E857(?o),3). Happens(E858(?o),3). Happens(E859(?o),3). Happens(E860(?o),3). Happens(E861(?o),3). Happens(E862(?o),3). Happens(E863(?o),3). Happens(E864(?o),3). Happens(E865(?o),3). Happens(E866(?o),3). Happens(E867(?o),3). Happens(E868(?o),3). Happens(E869(?o),3). Happens(E870(?o),3). Happens(E871(?o),3). Happens(E872(?o),3). Happens(E873(?o),3). Happens(E874(?o),3). Happens(E875(?o),3). Happens(E876(?o),3). Happens(E877(?o),3). Happens(E878(?o),3). Happens(E879(?o),3). Happens(E880(?o),3). Happens(E881(?o),3). Happens(E882(?o),3). Happens(E883(?o),3). Happens(E884(?o),3). Happens(E885(?o),3). Happens(E886(?o),3). Happens(E887(?o),3). Happens(E888(?o),3). Happens(E889(?o),3). Happens(E890(?o),3). Happens(E891(?o),3). Happens(E892(?o),3). Happens(E893(?o),3). Happens(E894(?o),3). Happens(E895(?o),3). Happens(E896(?o),3). Happens(E897(?o),3). Happens(E898(?o),3). Happens(E899(?o),3). Happens(E900(?o),3). Happens(E901(?o),3). Happens(E902(?o),3). Happens(E903(?o),3). Happens(E904(?o),3). Happens(E905(?o),3). Happens(E906(?o),3). Happens(E907(?o),3). Happens(E908(?o),3). Happens(E909(?o),3). Happens(E910(?o),3). Happens(E911(?o),3). Happens(E912(?o),3). Happens(E913(?o),3). Happens(E914(?o),3). Happens(E915(?o),3). Happens(E916(?o),3). Happens(E917(?o),3). Happens(E918(?o),3). Happens(E919(?o),3). Happens(E920(?o),3). Happens(E921(?o),3). Happens(E922(?o),3). Happens(E923(?o),3). Happens(E924(?o),3). Happens(E925(?o),3). Happens(E926(?o),3). Happens(E927(?o),3). Happens(E928(?o),3). Happens(E929(?o),3). Happens(E930(?o),3). Happens(E931(?o),3). Happens(E932(?o),3). Happens(E933(?o),3). Happens(E934(?o),3). Happens(E935(?o),3). Happens(E936(?o),3). Happens(E937(?o),3). Happens(E938(?o),3). Happens(E939(?o),3). Happens(E940(?o),3). Happens(E941(?o),3). Happens(E942(?o),3). Happens(E943(?o),3). Happens(E944(?o),3). Happens(E945(?o),3). Happens(E946(?o),3). Happens(E947(?o),3). Happens(E948(?o),3). Happens(E949(?o),3). Happens(E950(?o),3). Happens(E951(?o),3). Happens(E952(?o),3). Happens(E953(?o),3). Happens(E954(?o),3). Happens(E955(?o),3). Happens(E956(?o),3). Happens(E957(?o),3). Happens(E958(?o),3). Happens(E959(?o),3). Happens(E960(?o),3). Happens(E961(?o),3). Happens(E962(?o),3). Happens(E963(?o),3). Happens(E964(?o),3). Happens(E965(?o),3). Happens(E966(?o),3). Happens(E967(?o),3). Happens(E968(?o),3). Happens(E969(?o),3). Happens(E970(?o),3). Happens(E971(?o),3). Happens(E972(?o),3). Happens(E973(?o),3). Happens(E974(?o),3). Happens(E975(?o),3). Happens(E976(?o),3). Happens(E977(?o),3). Happens(E978(?o),3). Happens(E979(?o),3). Happens(E980(?o),3). Happens(E981(?o),3). Happens(E982(?o),3). Happens(E983(?o),3). Happens(E984(?o),3). Happens(E985(?o),3). Happens(E986(?o),3). Happens(E987(?o),3). Happens(E988(?o),3). Happens(E989(?o),3). Happens(E990(?o),3). Happens(E991(?o),3). Happens(E992(?o),3). Happens(E993(?o),3). Happens(E994(?o),3). Happens(E995(?o),3). Happens(E996(?o),3). Happens(E997(?o),3). Happens(E998(?o),3). Happens(E999(?o),3). Happens(E1000(?o),3).