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


tff(false_decl, type, false: $o).
tff(p1_decl, type, p1: $o).
tff(p10_decl, type, p10: $o).
tff(p11_decl, type, p11: $o).
tff(p12_decl, type, p12: $o).
tff(p13_decl, type, p13: $o).
tff(p14_decl, type, p14: $o).
tff(p15_decl, type, p15: $o).
tff(p16_decl, type, p16: $o).
tff(p17_decl, type, p17: $o).
tff(p18_decl, type, p18: $o).
tff(p19_decl, type, p19: $o).
tff(p2_decl, type, p2: $o).
tff(p20_decl, type, p20: $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(p27_decl, type, p27: $o).
tff(p28_decl, type, p28: $o).
tff(p29_decl, type, p29: $o).
tff(p3_decl, type, p3: $o).
tff(p30_decl, type, p30: $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(p37_decl, type, p37: $o).
tff(p38_decl, type, p38: $o).
tff(p39_decl, type, p39: $o).
tff(p4_decl, type, p4: $o).
tff(p40_decl, type, p40: $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(p47_decl, type, p47: $o).
tff(p48_decl, type, p48: $o).
tff(p49_decl, type, p49: $o).
tff(p5_decl, type, p5: $o).
tff(p50_decl, type, p50: $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(p57_decl, type, p57: $o).
tff(p58_decl, type, p58: $o).
tff(p59_decl, type, p59: $o).
tff(p6_decl, type, p6: $o).
tff(p60_decl, type, p60: $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(p67_decl, type, p67: $o).
tff(p68_decl, type, p68: $o).
tff(p69_decl, type, p69: $o).
tff(p7_decl, type, p7: $o).
tff(p70_decl, type, p70: $o).
tff(p71_decl, type, p71: $o).
tff(p72_decl, type, p72: $o).
tff(p73_decl, type, p73: $o).
tff(p78_decl, type, p78: $o).
tff(p8_decl, type, p8: $o).
tff(p9_decl, type, p9: $o).


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

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

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~false
	& ~p1
	& ~p10
	& ~p11
	& ~p12
	& ~p13
	& ~p14
	& ~p15
	& ~p16
	& ~p17
	& ~p18
	& ~p19
	& ~p2
	& ~p20
	& ~p21
	& ~p22
	& ~p23
	& ~p24
	& ~p25
	& ~p26
	& ~p27
	& ~p28
	& ~p29
	& ~p3
	& ~p30
	& ~p31
	& ~p32
	& ~p33
	& ~p34
	& ~p35
	& ~p36
	& ~p37
	& ~p38
	& ~p39
	& ~p4
	& ~p40
	& ~p41
	& ~p42
	& ~p43
	& ~p44
	& ~p45
	& ~p46
	& ~p47
	& ~p48
	& ~p49
	& ~p5
	& ~p50
	& ~p51
	& ~p52
	& ~p53
	& ~p54
	& ~p55
	& ~p56
	& ~p57
	& ~p58
	& ~p59
	& ~p6
	& ~p60
	& ~p61
	& ~p62
	& ~p63
	& ~p64
	& ~p65
	& ~p66
	& ~p67
	& ~p68
	& ~p69
	& ~p7
	& ~p70
	& ~p71
	& ~p72
	& ~p73
	& ~p78
	& ~p8
	& ~p9))
& $in_world(world_1,
	(~false
	& p1
	& p10
	& p11
	& p12
	& p13
	& p14
	& p15
	& p16
	& p17
	& p18
	& p19
	& p2
	& p20
	& p21
	& p22
	& p23
	& p24
	& p25
	& p26
	& p27
	& p28
	& p29
	& p3
	& p30
	& p31
	& p32
	& p33
	& p34
	& p35
	& p36
	& p37
	& p38
	& p39
	& p4
	& p40
	& p41
	& p42
	& p43
	& p44
	& p45
	& p46
	& p47
	& p48
	& p49
	& p5
	& p50
	& p51
	& p52
	& p53
	& p54
	& p55
	& p56
	& p57
	& p58
	& p59
	& p6
	& p60
	& p61
	& p62
	& p63
	& p64
	& p65
	& p66
	& p67
	& p68
	& p69
	& p7
	& p70
	& p71
	& p72
	& p73
	& p78
	& p8
	& p9))
)).