prop aux1001 := [[[[[~ pc1_at_0] & [~ pc2_at_0]] & [t_aux_at_0 = 2]] & [e_aux_at_0 = 20]] & [p_aux_at_0 = 10]].
prop aux1002 := [[[[[d_at_0 >= 0] & [t_at_0 = (t_aux_at_0 + d_at_0)]] & [e_at_0 = (e_aux_at_0 + (5 * d_at_0))]] & [(2 * p_at_0) >= ((2 * p_aux_at_0) - d_at_0)]] & [p_at_0 <= (p_aux_at_0 + (6 * d_at_0))]].
prop aux1003 := [[[t_at_0 <= 2] & [e_at_0 >= 0]] & [p_at_0 <= 40]].
prop aux1004 := [[~ pc1_at_0] & [~ pc2_at_0]].
prop aux1005 := [pc1_at_0 & [~ pc2_at_0]].
prop aux1006 := [[~ pc1_at_0] & pc2_at_0].
prop aux1007 := [[~ pc1_at_1] & [~ pc2_at_1]].
prop aux1008 := [pc1_at_1 & [~ pc2_at_1]].
prop aux1009 := [[~ pc1_at_1] & pc2_at_1].
prop aux1010 := [[[[[[e_at_0 = 40] & [e_aux_at_1 = 0]] & [p_aux_at_1 = p_at_0]] & [t_aux_at_1 = t_at_0]] | [[[[p_at_0 = 40] & [p_aux_at_1 = 0]] & [e_aux_at_1 = e_at_0]] & [t_aux_at_1 = t_at_0]]] | [[[[p_at_0 = 0] & [p_aux_at_1 = 40]] & [e_aux_at_1 = e_at_0]] & [t_aux_at_1 = t_at_0]]].
prop aux1011 := [(((5 * p_at_0) - (6 * e_at_0)) + 40) < 0].
prop aux1012 := [[[t_aux_at_1 = 0] & [p_aux_at_1 = p_at_0]] & [e_aux_at_1 = e_at_0]].
prop aux1013 := [[[t_aux_at_1 = t_at_0] & [p_aux_at_1 = p_at_0]] & [e_aux_at_1 = e_at_0]].
prop aux1014 := [[[[[[aux1004 & aux1007] & [t_at_0 = 2]] & [e_at_0 <> 0]] & [e_at_0 <> 40]] & aux1011] & aux1012].
prop aux1015 := [[aux1004 & aux1007] & aux1010].
prop aux1016 := [[[[[[aux1004 & aux1008] & [t_at_0 = 2]] & [e_at_0 <> 0]] & [e_at_0 <> 40]] & [~ aux1011]] & aux1012].
prop aux1017 := [[[[[[aux1005 & aux1008] & [t_at_0 = 2]] & [e_at_0 <> 0]] & [e_at_0 <> 40]] & [~ aux1011]] & aux1012].
prop aux1018 := [[aux1005 & aux1008] & aux1010].
prop aux1019 := [[[[[[aux1005 & aux1007] & [t_at_0 = 2]] & [e_at_0 <> 0]] & [e_at_0 <> 40]] & aux1011] & aux1012].
prop aux1020 := [[[aux1004 & aux1009] & [e_at_0 = 0]] & aux1013].
prop aux1021 := [[[aux1005 & aux1009] & [e_at_0 = 0]] & aux1013].
prop aux1022 := [[[[[[[aux1014 | aux1015] | aux1016] | aux1017] | aux1018] | aux1019] | aux1020] | aux1021].
prop aux1023 := [[[[[d_at_1 >= 0] & [t_at_1 = (t_aux_at_1 + d_at_1)]] & [e_at_1 = (e_aux_at_1 + (5 * d_at_1))]] & [(2 * p_at_1) >= ((2 * p_aux_at_1) - d_at_1)]] & [p_at_1 <= (p_aux_at_1 + (6 * d_at_1))]].
prop aux1024 := [[aux1007 | aux1008] => [[[t_at_1 <= 2] & [e_at_1 >= 0]] & [p_at_1 <= 40]]].
prop aux1025 := [aux1009 => [d_at_1 = 0]].
prop aux1026 := [~ [pc1_at_1 & pc2_at_1]].
prop aux1027 := [[~ pc1_at_1] & [~ pc2_at_1]].
prop aux1028 := [pc1_at_1 & [~ pc2_at_1]].
prop aux1029 := [[~ pc1_at_1] & pc2_at_1].
prop aux1030 := [[~ pc1_at_2] & [~ pc2_at_2]].
prop aux1031 := [pc1_at_2 & [~ pc2_at_2]].
prop aux1032 := [[~ pc1_at_2] & pc2_at_2].
prop aux1033 := [[[[[[e_at_1 = 40] & [e_aux_at_2 = 0]] & [p_aux_at_2 = p_at_1]] & [t_aux_at_2 = t_at_1]] | [[[[p_at_1 = 40] & [p_aux_at_2 = 0]] & [e_aux_at_2 = e_at_1]] & [t_aux_at_2 = t_at_1]]] | [[[[p_at_1 = 0] & [p_aux_at_2 = 40]] & [e_aux_at_2 = e_at_1]] & [t_aux_at_2 = t_at_1]]].
prop aux1034 := [(((5 * p_at_1) - (6 * e_at_1)) + 40) < 0].
prop aux1035 := [[[t_aux_at_2 = 0] & [p_aux_at_2 = p_at_1]] & [e_aux_at_2 = e_at_1]].
prop aux1036 := [[[t_aux_at_2 = t_at_1] & [p_aux_at_2 = p_at_1]] & [e_aux_at_2 = e_at_1]].
prop aux1037 := [[[[[[aux1027 & aux1030] & [t_at_1 = 2]] & [e_at_1 <> 0]] & [e_at_1 <> 40]] & aux1034] & aux1035].
prop aux1038 := [[aux1027 & aux1030] & aux1033].
prop aux1039 := [[[[[[aux1027 & aux1031] & [t_at_1 = 2]] & [e_at_1 <> 0]] & [e_at_1 <> 40]] & [~ aux1034]] & aux1035].
prop aux1040 := [[[[[[aux1028 & aux1031] & [t_at_1 = 2]] & [e_at_1 <> 0]] & [e_at_1 <> 40]] & [~ aux1034]] & aux1035].
prop aux1041 := [[aux1028 & aux1031] & aux1033].
prop aux1042 := [[[[[[aux1028 & aux1030] & [t_at_1 = 2]] & [e_at_1 <> 0]] & [e_at_1 <> 40]] & aux1034] & aux1035].
prop aux1043 := [[[aux1027 & aux1032] & [e_at_1 = 0]] & aux1036].
prop aux1044 := [[[aux1028 & aux1032] & [e_at_1 = 0]] & aux1036].
prop aux1045 := [[[[[[[aux1037 | aux1038] | aux1039] | aux1040] | aux1041] | aux1042] | aux1043] | aux1044].
prop aux1046 := [[[[[d_at_2 >= 0] & [t_at_2 = (t_aux_at_2 + d_at_2)]] & [e_at_2 = (e_aux_at_2 + (5 * d_at_2))]] & [(2 * p_at_2) >= ((2 * p_aux_at_2) - d_at_2)]] & [p_at_2 <= (p_aux_at_2 + (6 * d_at_2))]].
prop aux1047 := [[aux1030 | aux1031] => [[[t_at_2 <= 2] & [e_at_2 >= 0]] & [p_at_2 <= 40]]].
prop aux1048 := [aux1032 => [d_at_2 = 0]].
prop aux1049 := [~ [pc1_at_2 & pc2_at_2]].
prop aux1050 := [[~ pc1_at_2] & [~ pc2_at_2]].
prop aux1051 := [pc1_at_2 & [~ pc2_at_2]].
prop aux1052 := [[~ pc1_at_2] & pc2_at_2].
prop aux1053 := [[~ pc1_at_3] & [~ pc2_at_3]].
prop aux1054 := [pc1_at_3 & [~ pc2_at_3]].
prop aux1055 := [[~ pc1_at_3] & pc2_at_3].
prop aux1056 := [[[[[[e_at_2 = 40] & [e_aux_at_3 = 0]] & [p_aux_at_3 = p_at_2]] & [t_aux_at_3 = t_at_2]] | [[[[p_at_2 = 40] & [p_aux_at_3 = 0]] & [e_aux_at_3 = e_at_2]] & [t_aux_at_3 = t_at_2]]] | [[[[p_at_2 = 0] & [p_aux_at_3 = 40]] & [e_aux_at_3 = e_at_2]] & [t_aux_at_3 = t_at_2]]].
prop aux1057 := [(((5 * p_at_2) - (6 * e_at_2)) + 40) < 0].
prop aux1058 := [[[t_aux_at_3 = 0] & [p_aux_at_3 = p_at_2]] & [e_aux_at_3 = e_at_2]].
prop aux1059 := [[[t_aux_at_3 = t_at_2] & [p_aux_at_3 = p_at_2]] & [e_aux_at_3 = e_at_2]].
prop aux1060 := [[[[[[aux1050 & aux1053] & [t_at_2 = 2]] & [e_at_2 <> 0]] & [e_at_2 <> 40]] & aux1057] & aux1058].
prop aux1061 := [[aux1050 & aux1053] & aux1056].
prop aux1062 := [[[[[[aux1050 & aux1054] & [t_at_2 = 2]] & [e_at_2 <> 0]] & [e_at_2 <> 40]] & [~ aux1057]] & aux1058].
prop aux1063 := [[[[[[aux1051 & aux1054] & [t_at_2 = 2]] & [e_at_2 <> 0]] & [e_at_2 <> 40]] & [~ aux1057]] & aux1058].
prop aux1064 := [[aux1051 & aux1054] & aux1056].
prop aux1065 := [[[[[[aux1051 & aux1053] & [t_at_2 = 2]] & [e_at_2 <> 0]] & [e_at_2 <> 40]] & aux1057] & aux1058].
prop aux1066 := [[[aux1050 & aux1055] & [e_at_2 = 0]] & aux1059].
prop aux1067 := [[[aux1051 & aux1055] & [e_at_2 = 0]] & aux1059].
prop aux1068 := [[[[[[[aux1060 | aux1061] | aux1062] | aux1063] | aux1064] | aux1065] | aux1066] | aux1067].
prop aux1069 := [[[[[d_at_3 >= 0] & [t_at_3 = (t_aux_at_3 + d_at_3)]] & [e_at_3 = (e_aux_at_3 + (5 * d_at_3))]] & [(2 * p_at_3) >= ((2 * p_aux_at_3) - d_at_3)]] & [p_at_3 <= (p_aux_at_3 + (6 * d_at_3))]].
prop aux1070 := [[aux1053 | aux1054] => [[[t_at_3 <= 2] & [e_at_3 >= 0]] & [p_at_3 <= 40]]].
prop aux1071 := [aux1055 => [d_at_3 = 0]].
prop aux1072 := [~ [pc1_at_3 & pc2_at_3]].
prop aux1073 := [[~ pc1_at_3] & [~ pc2_at_3]].
prop aux1074 := [pc1_at_3 & [~ pc2_at_3]].
prop aux1075 := [[~ pc1_at_3] & pc2_at_3].
prop aux1076 := [[~ pc1_at_4] & [~ pc2_at_4]].
prop aux1077 := [pc1_at_4 & [~ pc2_at_4]].
prop aux1078 := [[~ pc1_at_4] & pc2_at_4].
prop aux1079 := [[[[[[e_at_3 = 40] & [e_aux_at_4 = 0]] & [p_aux_at_4 = p_at_3]] & [t_aux_at_4 = t_at_3]] | [[[[p_at_3 = 40] & [p_aux_at_4 = 0]] & [e_aux_at_4 = e_at_3]] & [t_aux_at_4 = t_at_3]]] | [[[[p_at_3 = 0] & [p_aux_at_4 = 40]] & [e_aux_at_4 = e_at_3]] & [t_aux_at_4 = t_at_3]]].
prop aux1080 := [(((5 * p_at_3) - (6 * e_at_3)) + 40) < 0].
prop aux1081 := [[[t_aux_at_4 = 0] & [p_aux_at_4 = p_at_3]] & [e_aux_at_4 = e_at_3]].
prop aux1082 := [[[t_aux_at_4 = t_at_3] & [p_aux_at_4 = p_at_3]] & [e_aux_at_4 = e_at_3]].
prop aux1083 := [[[[[[aux1073 & aux1076] & [t_at_3 = 2]] & [e_at_3 <> 0]] & [e_at_3 <> 40]] & aux1080] & aux1081].
prop aux1084 := [[aux1073 & aux1076] & aux1079].
prop aux1085 := [[[[[[aux1073 & aux1077] & [t_at_3 = 2]] & [e_at_3 <> 0]] & [e_at_3 <> 40]] & [~ aux1080]] & aux1081].
prop aux1086 := [[[[[[aux1074 & aux1077] & [t_at_3 = 2]] & [e_at_3 <> 0]] & [e_at_3 <> 40]] & [~ aux1080]] & aux1081].
prop aux1087 := [[aux1074 & aux1077] & aux1079].
prop aux1088 := [[[[[[aux1074 & aux1076] & [t_at_3 = 2]] & [e_at_3 <> 0]] & [e_at_3 <> 40]] & aux1080] & aux1081].
prop aux1089 := [[[aux1073 & aux1078] & [e_at_3 = 0]] & aux1082].
prop aux1090 := [[[aux1074 & aux1078] & [e_at_3 = 0]] & aux1082].
prop aux1091 := [[[[[[[aux1083 | aux1084] | aux1085] | aux1086] | aux1087] | aux1088] | aux1089] | aux1090].
prop aux1092 := [[[[[d_at_4 >= 0] & [t_at_4 = (t_aux_at_4 + d_at_4)]] & [e_at_4 = (e_aux_at_4 + (5 * d_at_4))]] & [(2 * p_at_4) >= ((2 * p_aux_at_4) - d_at_4)]] & [p_at_4 <= (p_aux_at_4 + (6 * d_at_4))]].
prop aux1093 := [[aux1076 | aux1077] => [[[t_at_4 <= 2] & [e_at_4 >= 0]] & [p_at_4 <= 40]]].
prop aux1094 := [aux1078 => [d_at_4 = 0]].
prop aux1095 := [~ [pc1_at_4 & pc2_at_4]].
sat ~[
[[[[aux1001 & aux1002] & aux1003] & [[[[[aux1022 & aux1023] & aux1024] & aux1025] & aux1026] & [[[[aux1045 & aux1046] & aux1047] & aux1048] & aux1049] & [[[[aux1068 & aux1069] & aux1070] & aux1071] & aux1072] & [[[[aux1091 & aux1092] & aux1093] & aux1094] & aux1095]] & tt] => [[~ [e_at_0 = p_at_0]] & [~ [e_at_1 = p_at_1]] & [~ [e_at_2 = p_at_2]] & [~ [e_at_3 = p_at_3]] & [~ [e_at_4 = p_at_4]]]]].