tff('s4_ph_n.0013', logic, ($modal) == ([($modalities) == ($modal_system_S4)])).


tff(p1001_decl, type, p1001: $o).
tff(p1002_decl, type, p1002: $o).
tff(p1003_decl, type, p1003: $o).
tff(p1004_decl, type, p1004: $o).
tff(p1005_decl, type, p1005: $o).
tff(p1006_decl, type, p1006: $o).
tff(p1007_decl, type, p1007: $o).
tff(p1008_decl, type, p1008: $o).
tff(p1009_decl, type, p1009: $o).
tff(p101_decl, type, p101: $o).
tff(p1010_decl, type, p1010: $o).
tff(p1011_decl, type, p1011: $o).
tff(p1012_decl, type, p1012: $o).
tff(p1013_decl, type, p1013: $o).
tff(p102_decl, type, p102: $o).
tff(p103_decl, type, p103: $o).
tff(p104_decl, type, p104: $o).
tff(p105_decl, type, p105: $o).
tff(p106_decl, type, p106: $o).
tff(p107_decl, type, p107: $o).
tff(p108_decl, type, p108: $o).
tff(p109_decl, type, p109: $o).
tff(p110_decl, type, p110: $o).
tff(p1101_decl, type, p1101: $o).
tff(p1102_decl, type, p1102: $o).
tff(p1103_decl, type, p1103: $o).
tff(p1104_decl, type, p1104: $o).
tff(p1105_decl, type, p1105: $o).
tff(p1106_decl, type, p1106: $o).
tff(p1107_decl, type, p1107: $o).
tff(p1108_decl, type, p1108: $o).
tff(p1109_decl, type, p1109: $o).
tff(p111_decl, type, p111: $o).
tff(p1110_decl, type, p1110: $o).
tff(p1111_decl, type, p1111: $o).
tff(p1112_decl, type, p1112: $o).
tff(p1113_decl, type, p1113: $o).
tff(p112_decl, type, p112: $o).
tff(p113_decl, type, p113: $o).
tff(p1201_decl, type, p1201: $o).
tff(p1202_decl, type, p1202: $o).
tff(p1203_decl, type, p1203: $o).
tff(p1204_decl, type, p1204: $o).
tff(p1205_decl, type, p1205: $o).
tff(p1206_decl, type, p1206: $o).
tff(p1207_decl, type, p1207: $o).
tff(p1208_decl, type, p1208: $o).
tff(p1209_decl, type, p1209: $o).
tff(p1210_decl, type, p1210: $o).
tff(p1211_decl, type, p1211: $o).
tff(p1212_decl, type, p1212: $o).
tff(p1213_decl, type, p1213: $o).
tff(p1301_decl, type, p1301: $o).
tff(p1302_decl, type, p1302: $o).
tff(p1303_decl, type, p1303: $o).
tff(p1304_decl, type, p1304: $o).
tff(p1305_decl, type, p1305: $o).
tff(p1306_decl, type, p1306: $o).
tff(p1307_decl, type, p1307: $o).
tff(p1308_decl, type, p1308: $o).
tff(p1309_decl, type, p1309: $o).
tff(p1310_decl, type, p1310: $o).
tff(p1311_decl, type, p1311: $o).
tff(p1312_decl, type, p1312: $o).
tff(p1313_decl, type, p1313: $o).
tff(p1401_decl, type, p1401: $o).
tff(p1402_decl, type, p1402: $o).
tff(p1403_decl, type, p1403: $o).
tff(p1404_decl, type, p1404: $o).
tff(p1405_decl, type, p1405: $o).
tff(p1406_decl, type, p1406: $o).
tff(p1407_decl, type, p1407: $o).
tff(p1408_decl, type, p1408: $o).
tff(p1409_decl, type, p1409: $o).
tff(p1410_decl, type, p1410: $o).
tff(p1411_decl, type, p1411: $o).
tff(p1412_decl, type, p1412: $o).
tff(p1413_decl, type, p1413: $o).
tff(p201_decl, type, p201: $o).
tff(p202_decl, type, p202: $o).
tff(p203_decl, type, p203: $o).
tff(p204_decl, type, p204: $o).
tff(p205_decl, type, p205: $o).
tff(p206_decl, type, p206: $o).
tff(p207_decl, type, p207: $o).
tff(p208_decl, type, p208: $o).
tff(p209_decl, type, p209: $o).
tff(p210_decl, type, p210: $o).
tff(p211_decl, type, p211: $o).
tff(p212_decl, type, p212: $o).
tff(p213_decl, type, p213: $o).
tff(p301_decl, type, p301: $o).
tff(p302_decl, type, p302: $o).
tff(p303_decl, type, p303: $o).
tff(p304_decl, type, p304: $o).
tff(p305_decl, type, p305: $o).
tff(p306_decl, type, p306: $o).
tff(p307_decl, type, p307: $o).
tff(p308_decl, type, p308: $o).
tff(p309_decl, type, p309: $o).
tff(p310_decl, type, p310: $o).
tff(p311_decl, type, p311: $o).
tff(p312_decl, type, p312: $o).
tff(p313_decl, type, p313: $o).
tff(p401_decl, type, p401: $o).
tff(p402_decl, type, p402: $o).
tff(p403_decl, type, p403: $o).
tff(p404_decl, type, p404: $o).
tff(p405_decl, type, p405: $o).
tff(p406_decl, type, p406: $o).
tff(p407_decl, type, p407: $o).
tff(p408_decl, type, p408: $o).
tff(p409_decl, type, p409: $o).
tff(p410_decl, type, p410: $o).
tff(p411_decl, type, p411: $o).
tff(p412_decl, type, p412: $o).
tff(p413_decl, type, p413: $o).
tff(p501_decl, type, p501: $o).
tff(p502_decl, type, p502: $o).
tff(p503_decl, type, p503: $o).
tff(p504_decl, type, p504: $o).
tff(p505_decl, type, p505: $o).
tff(p506_decl, type, p506: $o).
tff(p507_decl, type, p507: $o).
tff(p508_decl, type, p508: $o).
tff(p509_decl, type, p509: $o).
tff(p510_decl, type, p510: $o).
tff(p511_decl, type, p511: $o).
tff(p512_decl, type, p512: $o).
tff(p513_decl, type, p513: $o).
tff(p601_decl, type, p601: $o).
tff(p602_decl, type, p602: $o).
tff(p603_decl, type, p603: $o).
tff(p604_decl, type, p604: $o).
tff(p605_decl, type, p605: $o).
tff(p606_decl, type, p606: $o).
tff(p607_decl, type, p607: $o).
tff(p608_decl, type, p608: $o).
tff(p609_decl, type, p609: $o).
tff(p610_decl, type, p610: $o).
tff(p611_decl, type, p611: $o).
tff(p612_decl, type, p612: $o).
tff(p613_decl, type, p613: $o).
tff(p701_decl, type, p701: $o).
tff(p702_decl, type, p702: $o).
tff(p703_decl, type, p703: $o).
tff(p704_decl, type, p704: $o).
tff(p705_decl, type, p705: $o).
tff(p706_decl, type, p706: $o).
tff(p707_decl, type, p707: $o).
tff(p708_decl, type, p708: $o).
tff(p709_decl, type, p709: $o).
tff(p710_decl, type, p710: $o).
tff(p711_decl, type, p711: $o).
tff(p712_decl, type, p712: $o).
tff(p713_decl, type, p713: $o).
tff(p801_decl, type, p801: $o).
tff(p802_decl, type, p802: $o).
tff(p803_decl, type, p803: $o).
tff(p804_decl, type, p804: $o).
tff(p805_decl, type, p805: $o).
tff(p806_decl, type, p806: $o).
tff(p807_decl, type, p807: $o).
tff(p808_decl, type, p808: $o).
tff(p809_decl, type, p809: $o).
tff(p810_decl, type, p810: $o).
tff(p811_decl, type, p811: $o).
tff(p812_decl, type, p812: $o).
tff(p813_decl, type, p813: $o).
tff(p901_decl, type, p901: $o).
tff(p902_decl, type, p902: $o).
tff(p903_decl, type, p903: $o).
tff(p904_decl, type, p904: $o).
tff(p905_decl, type, p905: $o).
tff(p906_decl, type, p906: $o).
tff(p907_decl, type, p907: $o).
tff(p908_decl, type, p908: $o).
tff(p909_decl, type, p909: $o).
tff(p910_decl, type, p910: $o).
tff(p911_decl, type, p911: $o).
tff(p912_decl, type, p912: $o).
tff(p913_decl, type, p913: $o).


tff(world_0_decl, type, world_0: $world).

tff(model_worlds, interpretation-worlds, 
((! [W: $world] : ( (W = world_0) ))
& ($local_world = world_0)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~p1001
	& ~p1002
	& ~p1003
	& ~p1004
	& ~p1005
	& ~p1006
	& ~p1007
	& ~p1008
	& p1009
	& p101
	& ~p1010
	& ~p1011
	& ~p1012
	& ~p1013
	& ~p102
	& ~p103
	& ~p104
	& ~p105
	& ~p106
	& ~p107
	& ~p108
	& ~p109
	& ~p110
	& ~p1101
	& ~p1102
	& ~p1103
	& ~p1104
	& ~p1105
	& ~p1106
	& ~p1107
	& ~p1108
	& ~p1109
	& ~p111
	& p1110
	& ~p1111
	& ~p1112
	& ~p1113
	& ~p112
	& ~p113
	& ~p1201
	& ~p1202
	& ~p1203
	& ~p1204
	& ~p1205
	& ~p1206
	& ~p1207
	& ~p1208
	& ~p1209
	& ~p1210
	& p1211
	& ~p1212
	& ~p1213
	& ~p1301
	& ~p1302
	& ~p1303
	& ~p1304
	& ~p1305
	& ~p1306
	& ~p1307
	& ~p1308
	& ~p1309
	& ~p1310
	& ~p1311
	& p1312
	& ~p1313
	& ~p1401
	& ~p1402
	& ~p1403
	& ~p1404
	& ~p1405
	& ~p1406
	& ~p1407
	& ~p1408
	& ~p1409
	& ~p1410
	& ~p1411
	& ~p1412
	& p1413
	& ~p201
	& p202
	& ~p203
	& ~p204
	& ~p205
	& ~p206
	& ~p207
	& ~p208
	& ~p209
	& ~p210
	& ~p211
	& ~p212
	& ~p213
	& ~p301
	& ~p302
	& p303
	& ~p304
	& ~p305
	& ~p306
	& ~p307
	& ~p308
	& ~p309
	& ~p310
	& ~p311
	& ~p312
	& ~p313
	& ~p401
	& ~p402
	& ~p403
	& p404
	& ~p405
	& ~p406
	& ~p407
	& ~p408
	& ~p409
	& ~p410
	& ~p411
	& ~p412
	& ~p413
	& ~p501
	& ~p502
	& ~p503
	& ~p504
	& p505
	& ~p506
	& ~p507
	& ~p508
	& ~p509
	& ~p510
	& ~p511
	& ~p512
	& ~p513
	& ~p601
	& ~p602
	& ~p603
	& ~p604
	& ~p605
	& p606
	& ~p607
	& ~p608
	& ~p609
	& ~p610
	& ~p611
	& ~p612
	& ~p613
	& ~p701
	& ~p702
	& ~p703
	& ~p704
	& ~p705
	& ~p706
	& p707
	& ~p708
	& ~p709
	& ~p710
	& ~p711
	& ~p712
	& ~p713
	& ~p801
	& ~p802
	& ~p803
	& ~p804
	& ~p805
	& ~p806
	& ~p807
	& p808
	& ~p809
	& ~p810
	& ~p811
	& ~p812
	& ~p813
	& ~p901
	& ~p902
	& ~p903
	& ~p904
	& ~p905
	& ~p906
	& ~p907
	& ~p908
	& p909
	& ~p910
	& ~p911
	& ~p912
	& ~p913))
)).