tff('s4_path_n.0017', logic, ($modal) == ([($modalities) == ($modal_system_S4)])).


tff(false_decl, type, false: $o).
tff(p101_decl, type, p101: $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(p11_decl, type, p11: $o).
tff(p111_decl, type, p111: $o).
tff(p112_decl, type, p112: $o).
tff(p113_decl, type, p113: $o).
tff(p114_decl, type, p114: $o).
tff(p115_decl, type, p115: $o).
tff(p116_decl, type, p116: $o).
tff(p12_decl, type, p12: $o).
tff(p121_decl, type, p121: $o).
tff(p122_decl, type, p122: $o).
tff(p123_decl, type, p123: $o).
tff(p124_decl, type, p124: $o).
tff(p125_decl, type, p125: $o).
tff(p126_decl, type, p126: $o).
tff(p13_decl, type, p13: $o).
tff(p131_decl, type, p131: $o).
tff(p132_decl, type, p132: $o).
tff(p133_decl, type, p133: $o).
tff(p134_decl, type, p134: $o).
tff(p135_decl, type, p135: $o).
tff(p136_decl, type, p136: $o).
tff(p14_decl, type, p14: $o).
tff(p141_decl, type, p141: $o).
tff(p142_decl, type, p142: $o).
tff(p143_decl, type, p143: $o).
tff(p144_decl, type, p144: $o).
tff(p145_decl, type, p145: $o).
tff(p146_decl, type, p146: $o).
tff(p15_decl, type, p15: $o).
tff(p151_decl, type, p151: $o).
tff(p152_decl, type, p152: $o).
tff(p153_decl, type, p153: $o).
tff(p154_decl, type, p154: $o).
tff(p155_decl, type, p155: $o).
tff(p156_decl, type, p156: $o).
tff(p16_decl, type, p16: $o).
tff(p161_decl, type, p161: $o).
tff(p162_decl, type, p162: $o).
tff(p163_decl, type, p163: $o).
tff(p164_decl, type, p164: $o).
tff(p165_decl, type, p165: $o).
tff(p166_decl, type, p166: $o).
tff(p171_decl, type, p171: $o).
tff(p172_decl, type, p172: $o).
tff(p173_decl, type, p173: $o).
tff(p174_decl, type, p174: $o).
tff(p175_decl, type, p175: $o).
tff(p176_decl, type, p176: $o).
tff(p181_decl, type, p181: $o).
tff(p182_decl, type, p182: $o).
tff(p183_decl, type, p183: $o).
tff(p184_decl, type, p184: $o).
tff(p185_decl, type, p185: $o).
tff(p186_decl, type, p186: $o).
tff(p21_decl, type, p21: $o).
tff(p22_decl, type, p22: $o).
tff(p23_decl, type, p23: $o).
tff(p24_decl, type, p24: $o).
tff(p25_decl, type, p25: $o).
tff(p26_decl, type, p26: $o).
tff(p31_decl, type, p31: $o).
tff(p32_decl, type, p32: $o).
tff(p33_decl, type, p33: $o).
tff(p34_decl, type, p34: $o).
tff(p35_decl, type, p35: $o).
tff(p36_decl, type, p36: $o).
tff(p41_decl, type, p41: $o).
tff(p42_decl, type, p42: $o).
tff(p43_decl, type, p43: $o).
tff(p44_decl, type, p44: $o).
tff(p45_decl, type, p45: $o).
tff(p46_decl, type, p46: $o).
tff(p51_decl, type, p51: $o).
tff(p52_decl, type, p52: $o).
tff(p53_decl, type, p53: $o).
tff(p54_decl, type, p54: $o).
tff(p55_decl, type, p55: $o).
tff(p56_decl, type, p56: $o).
tff(p61_decl, type, p61: $o).
tff(p62_decl, type, p62: $o).
tff(p63_decl, type, p63: $o).
tff(p64_decl, type, p64: $o).
tff(p65_decl, type, p65: $o).
tff(p66_decl, type, p66: $o).
tff(p71_decl, type, p71: $o).
tff(p72_decl, type, p72: $o).
tff(p73_decl, type, p73: $o).
tff(p74_decl, type, p74: $o).
tff(p75_decl, type, p75: $o).
tff(p76_decl, type, p76: $o).
tff(p81_decl, type, p81: $o).
tff(p82_decl, type, p82: $o).
tff(p83_decl, type, p83: $o).
tff(p84_decl, type, p84: $o).
tff(p85_decl, type, p85: $o).
tff(p86_decl, type, p86: $o).
tff(p91_decl, type, p91: $o).
tff(p92_decl, type, p92: $o).
tff(p93_decl, type, p93: $o).
tff(p94_decl, type, p94: $o).
tff(p95_decl, type, p95: $o).
tff(p96_decl, type, p96: $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,
	(~false
	& ~p101
	& p102
	& p103
	& p104
	& ~p105
	& p106
	& ~p11
	& ~p111
	& p112
	& ~p113
	& p114
	& ~p115
	& p116
	& ~p12
	& ~p121
	& p122
	& p123
	& p124
	& ~p125
	& p126
	& ~p13
	& ~p131
	& p132
	& ~p133
	& p134
	& ~p135
	& p136
	& p14
	& ~p141
	& p142
	& p143
	& p144
	& ~p145
	& p146
	& ~p15
	& ~p151
	& p152
	& ~p153
	& p154
	& ~p155
	& p156
	& p16
	& ~p161
	& p162
	& p163
	& p164
	& ~p165
	& p166
	& ~p171
	& p172
	& ~p173
	& p174
	& ~p175
	& p176
	& ~p181
	& p182
	& p183
	& p184
	& ~p185
	& p186
	& ~p21
	& p22
	& ~p23
	& p24
	& ~p25
	& p26
	& ~p31
	& p32
	& ~p33
	& p34
	& ~p35
	& ~p36
	& ~p41
	& p42
	& ~p43
	& p44
	& ~p45
	& p46
	& ~p51
	& p52
	& ~p53
	& ~p54
	& ~p55
	& p56
	& ~p61
	& p62
	& ~p63
	& p64
	& ~p65
	& p66
	& ~p71
	& ~p72
	& ~p73
	& p74
	& ~p75
	& p76
	& ~p81
	& p82
	& ~p83
	& p84
	& ~p85
	& p86
	& ~p91
	& p92
	& ~p93
	& p94
	& ~p95
	& ~p96))
)).