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]].
prop aux1096 := [[~ pc1_at_4] & [~ pc2_at_4]].
prop aux1097 := [pc1_at_4 & [~ pc2_at_4]].
prop aux1098 := [[~ pc1_at_4] & pc2_at_4].
prop aux1099 := [[~ pc1_at_5] & [~ pc2_at_5]].
prop aux1100 := [pc1_at_5 & [~ pc2_at_5]].
prop aux1101 := [[~ pc1_at_5] & pc2_at_5].
prop aux1102 := [[[[[[e_at_4 = 40] & [e_aux_at_5 = 0]] & [p_aux_at_5 = p_at_4]] & [t_aux_at_5 = t_at_4]] | [[[[p_at_4 = 40] & [p_aux_at_5 = 0]] & [e_aux_at_5 = e_at_4]] & [t_aux_at_5 = t_at_4]]] | [[[[p_at_4 = 0] & [p_aux_at_5 = 40]] & [e_aux_at_5 = e_at_4]] & [t_aux_at_5 = t_at_4]]].
prop aux1103 := [(((5 * p_at_4) - (6 * e_at_4)) + 40) < 0].
prop aux1104 := [[[t_aux_at_5 = 0] & [p_aux_at_5 = p_at_4]] & [e_aux_at_5 = e_at_4]].
prop aux1105 := [[[t_aux_at_5 = t_at_4] & [p_aux_at_5 = p_at_4]] & [e_aux_at_5 = e_at_4]].
prop aux1106 := [[[[[[aux1096 & aux1099] & [t_at_4 = 2]] & [e_at_4 <> 0]] & [e_at_4 <> 40]] & aux1103] & aux1104].
prop aux1107 := [[aux1096 & aux1099] & aux1102].
prop aux1108 := [[[[[[aux1096 & aux1100] & [t_at_4 = 2]] & [e_at_4 <> 0]] & [e_at_4 <> 40]] & [~ aux1103]] & aux1104].
prop aux1109 := [[[[[[aux1097 & aux1100] & [t_at_4 = 2]] & [e_at_4 <> 0]] & [e_at_4 <> 40]] & [~ aux1103]] & aux1104].
prop aux1110 := [[aux1097 & aux1100] & aux1102].
prop aux1111 := [[[[[[aux1097 & aux1099] & [t_at_4 = 2]] & [e_at_4 <> 0]] & [e_at_4 <> 40]] & aux1103] & aux1104].
prop aux1112 := [[[aux1096 & aux1101] & [e_at_4 = 0]] & aux1105].
prop aux1113 := [[[aux1097 & aux1101] & [e_at_4 = 0]] & aux1105].
prop aux1114 := [[[[[[[aux1106 | aux1107] | aux1108] | aux1109] | aux1110] | aux1111] | aux1112] | aux1113].
prop aux1115 := [[[[[d_at_5 >= 0] & [t_at_5 = (t_aux_at_5 + d_at_5)]] & [e_at_5 = (e_aux_at_5 + (5 * d_at_5))]] & [(2 * p_at_5) >= ((2 * p_aux_at_5) - d_at_5)]] & [p_at_5 <= (p_aux_at_5 + (6 * d_at_5))]].
prop aux1116 := [[aux1099 | aux1100] => [[[t_at_5 <= 2] & [e_at_5 >= 0]] & [p_at_5 <= 40]]].
prop aux1117 := [aux1101 => [d_at_5 = 0]].
prop aux1118 := [~ [pc1_at_5 & pc2_at_5]].
prop aux1119 := [[~ pc1_at_5] & [~ pc2_at_5]].
prop aux1120 := [pc1_at_5 & [~ pc2_at_5]].
prop aux1121 := [[~ pc1_at_5] & pc2_at_5].
prop aux1122 := [[~ pc1_at_6] & [~ pc2_at_6]].
prop aux1123 := [pc1_at_6 & [~ pc2_at_6]].
prop aux1124 := [[~ pc1_at_6] & pc2_at_6].
prop aux1125 := [[[[[[e_at_5 = 40] & [e_aux_at_6 = 0]] & [p_aux_at_6 = p_at_5]] & [t_aux_at_6 = t_at_5]] | [[[[p_at_5 = 40] & [p_aux_at_6 = 0]] & [e_aux_at_6 = e_at_5]] & [t_aux_at_6 = t_at_5]]] | [[[[p_at_5 = 0] & [p_aux_at_6 = 40]] & [e_aux_at_6 = e_at_5]] & [t_aux_at_6 = t_at_5]]].
prop aux1126 := [(((5 * p_at_5) - (6 * e_at_5)) + 40) < 0].
prop aux1127 := [[[t_aux_at_6 = 0] & [p_aux_at_6 = p_at_5]] & [e_aux_at_6 = e_at_5]].
prop aux1128 := [[[t_aux_at_6 = t_at_5] & [p_aux_at_6 = p_at_5]] & [e_aux_at_6 = e_at_5]].
prop aux1129 := [[[[[[aux1119 & aux1122] & [t_at_5 = 2]] & [e_at_5 <> 0]] & [e_at_5 <> 40]] & aux1126] & aux1127].
prop aux1130 := [[aux1119 & aux1122] & aux1125].
prop aux1131 := [[[[[[aux1119 & aux1123] & [t_at_5 = 2]] & [e_at_5 <> 0]] & [e_at_5 <> 40]] & [~ aux1126]] & aux1127].
prop aux1132 := [[[[[[aux1120 & aux1123] & [t_at_5 = 2]] & [e_at_5 <> 0]] & [e_at_5 <> 40]] & [~ aux1126]] & aux1127].
prop aux1133 := [[aux1120 & aux1123] & aux1125].
prop aux1134 := [[[[[[aux1120 & aux1122] & [t_at_5 = 2]] & [e_at_5 <> 0]] & [e_at_5 <> 40]] & aux1126] & aux1127].
prop aux1135 := [[[aux1119 & aux1124] & [e_at_5 = 0]] & aux1128].
prop aux1136 := [[[aux1120 & aux1124] & [e_at_5 = 0]] & aux1128].
prop aux1137 := [[[[[[[aux1129 | aux1130] | aux1131] | aux1132] | aux1133] | aux1134] | aux1135] | aux1136].
prop aux1138 := [[[[[d_at_6 >= 0] & [t_at_6 = (t_aux_at_6 + d_at_6)]] & [e_at_6 = (e_aux_at_6 + (5 * d_at_6))]] & [(2 * p_at_6) >= ((2 * p_aux_at_6) - d_at_6)]] & [p_at_6 <= (p_aux_at_6 + (6 * d_at_6))]].
prop aux1139 := [[aux1122 | aux1123] => [[[t_at_6 <= 2] & [e_at_6 >= 0]] & [p_at_6 <= 40]]].
prop aux1140 := [aux1124 => [d_at_6 = 0]].
prop aux1141 := [~ [pc1_at_6 & pc2_at_6]].
prop aux1142 := [[~ pc1_at_6] & [~ pc2_at_6]].
prop aux1143 := [pc1_at_6 & [~ pc2_at_6]].
prop aux1144 := [[~ pc1_at_6] & pc2_at_6].
prop aux1145 := [[~ pc1_at_7] & [~ pc2_at_7]].
prop aux1146 := [pc1_at_7 & [~ pc2_at_7]].
prop aux1147 := [[~ pc1_at_7] & pc2_at_7].
prop aux1148 := [[[[[[e_at_6 = 40] & [e_aux_at_7 = 0]] & [p_aux_at_7 = p_at_6]] & [t_aux_at_7 = t_at_6]] | [[[[p_at_6 = 40] & [p_aux_at_7 = 0]] & [e_aux_at_7 = e_at_6]] & [t_aux_at_7 = t_at_6]]] | [[[[p_at_6 = 0] & [p_aux_at_7 = 40]] & [e_aux_at_7 = e_at_6]] & [t_aux_at_7 = t_at_6]]].
prop aux1149 := [(((5 * p_at_6) - (6 * e_at_6)) + 40) < 0].
prop aux1150 := [[[t_aux_at_7 = 0] & [p_aux_at_7 = p_at_6]] & [e_aux_at_7 = e_at_6]].
prop aux1151 := [[[t_aux_at_7 = t_at_6] & [p_aux_at_7 = p_at_6]] & [e_aux_at_7 = e_at_6]].
prop aux1152 := [[[[[[aux1142 & aux1145] & [t_at_6 = 2]] & [e_at_6 <> 0]] & [e_at_6 <> 40]] & aux1149] & aux1150].
prop aux1153 := [[aux1142 & aux1145] & aux1148].
prop aux1154 := [[[[[[aux1142 & aux1146] & [t_at_6 = 2]] & [e_at_6 <> 0]] & [e_at_6 <> 40]] & [~ aux1149]] & aux1150].
prop aux1155 := [[[[[[aux1143 & aux1146] & [t_at_6 = 2]] & [e_at_6 <> 0]] & [e_at_6 <> 40]] & [~ aux1149]] & aux1150].
prop aux1156 := [[aux1143 & aux1146] & aux1148].
prop aux1157 := [[[[[[aux1143 & aux1145] & [t_at_6 = 2]] & [e_at_6 <> 0]] & [e_at_6 <> 40]] & aux1149] & aux1150].
prop aux1158 := [[[aux1142 & aux1147] & [e_at_6 = 0]] & aux1151].
prop aux1159 := [[[aux1143 & aux1147] & [e_at_6 = 0]] & aux1151].
prop aux1160 := [[[[[[[aux1152 | aux1153] | aux1154] | aux1155] | aux1156] | aux1157] | aux1158] | aux1159].
prop aux1161 := [[[[[d_at_7 >= 0] & [t_at_7 = (t_aux_at_7 + d_at_7)]] & [e_at_7 = (e_aux_at_7 + (5 * d_at_7))]] & [(2 * p_at_7) >= ((2 * p_aux_at_7) - d_at_7)]] & [p_at_7 <= (p_aux_at_7 + (6 * d_at_7))]].
prop aux1162 := [[aux1145 | aux1146] => [[[t_at_7 <= 2] & [e_at_7 >= 0]] & [p_at_7 <= 40]]].
prop aux1163 := [aux1147 => [d_at_7 = 0]].
prop aux1164 := [~ [pc1_at_7 & pc2_at_7]].
prop aux1165 := [[~ pc1_at_7] & [~ pc2_at_7]].
prop aux1166 := [pc1_at_7 & [~ pc2_at_7]].
prop aux1167 := [[~ pc1_at_7] & pc2_at_7].
prop aux1168 := [[~ pc1_at_8] & [~ pc2_at_8]].
prop aux1169 := [pc1_at_8 & [~ pc2_at_8]].
prop aux1170 := [[~ pc1_at_8] & pc2_at_8].
prop aux1171 := [[[[[[e_at_7 = 40] & [e_aux_at_8 = 0]] & [p_aux_at_8 = p_at_7]] & [t_aux_at_8 = t_at_7]] | [[[[p_at_7 = 40] & [p_aux_at_8 = 0]] & [e_aux_at_8 = e_at_7]] & [t_aux_at_8 = t_at_7]]] | [[[[p_at_7 = 0] & [p_aux_at_8 = 40]] & [e_aux_at_8 = e_at_7]] & [t_aux_at_8 = t_at_7]]].
prop aux1172 := [(((5 * p_at_7) - (6 * e_at_7)) + 40) < 0].
prop aux1173 := [[[t_aux_at_8 = 0] & [p_aux_at_8 = p_at_7]] & [e_aux_at_8 = e_at_7]].
prop aux1174 := [[[t_aux_at_8 = t_at_7] & [p_aux_at_8 = p_at_7]] & [e_aux_at_8 = e_at_7]].
prop aux1175 := [[[[[[aux1165 & aux1168] & [t_at_7 = 2]] & [e_at_7 <> 0]] & [e_at_7 <> 40]] & aux1172] & aux1173].
prop aux1176 := [[aux1165 & aux1168] & aux1171].
prop aux1177 := [[[[[[aux1165 & aux1169] & [t_at_7 = 2]] & [e_at_7 <> 0]] & [e_at_7 <> 40]] & [~ aux1172]] & aux1173].
prop aux1178 := [[[[[[aux1166 & aux1169] & [t_at_7 = 2]] & [e_at_7 <> 0]] & [e_at_7 <> 40]] & [~ aux1172]] & aux1173].
prop aux1179 := [[aux1166 & aux1169] & aux1171].
prop aux1180 := [[[[[[aux1166 & aux1168] & [t_at_7 = 2]] & [e_at_7 <> 0]] & [e_at_7 <> 40]] & aux1172] & aux1173].
prop aux1181 := [[[aux1165 & aux1170] & [e_at_7 = 0]] & aux1174].
prop aux1182 := [[[aux1166 & aux1170] & [e_at_7 = 0]] & aux1174].
prop aux1183 := [[[[[[[aux1175 | aux1176] | aux1177] | aux1178] | aux1179] | aux1180] | aux1181] | aux1182].
prop aux1184 := [[[[[d_at_8 >= 0] & [t_at_8 = (t_aux_at_8 + d_at_8)]] & [e_at_8 = (e_aux_at_8 + (5 * d_at_8))]] & [(2 * p_at_8) >= ((2 * p_aux_at_8) - d_at_8)]] & [p_at_8 <= (p_aux_at_8 + (6 * d_at_8))]].
prop aux1185 := [[aux1168 | aux1169] => [[[t_at_8 <= 2] & [e_at_8 >= 0]] & [p_at_8 <= 40]]].
prop aux1186 := [aux1170 => [d_at_8 = 0]].
prop aux1187 := [~ [pc1_at_8 & pc2_at_8]].
prop aux1188 := [[~ pc1_at_8] & [~ pc2_at_8]].
prop aux1189 := [pc1_at_8 & [~ pc2_at_8]].
prop aux1190 := [[~ pc1_at_8] & pc2_at_8].
prop aux1191 := [[~ pc1_at_9] & [~ pc2_at_9]].
prop aux1192 := [pc1_at_9 & [~ pc2_at_9]].
prop aux1193 := [[~ pc1_at_9] & pc2_at_9].
prop aux1194 := [[[[[[e_at_8 = 40] & [e_aux_at_9 = 0]] & [p_aux_at_9 = p_at_8]] & [t_aux_at_9 = t_at_8]] | [[[[p_at_8 = 40] & [p_aux_at_9 = 0]] & [e_aux_at_9 = e_at_8]] & [t_aux_at_9 = t_at_8]]] | [[[[p_at_8 = 0] & [p_aux_at_9 = 40]] & [e_aux_at_9 = e_at_8]] & [t_aux_at_9 = t_at_8]]].
prop aux1195 := [(((5 * p_at_8) - (6 * e_at_8)) + 40) < 0].
prop aux1196 := [[[t_aux_at_9 = 0] & [p_aux_at_9 = p_at_8]] & [e_aux_at_9 = e_at_8]].
prop aux1197 := [[[t_aux_at_9 = t_at_8] & [p_aux_at_9 = p_at_8]] & [e_aux_at_9 = e_at_8]].
prop aux1198 := [[[[[[aux1188 & aux1191] & [t_at_8 = 2]] & [e_at_8 <> 0]] & [e_at_8 <> 40]] & aux1195] & aux1196].
prop aux1199 := [[aux1188 & aux1191] & aux1194].
prop aux1200 := [[[[[[aux1188 & aux1192] & [t_at_8 = 2]] & [e_at_8 <> 0]] & [e_at_8 <> 40]] & [~ aux1195]] & aux1196].
prop aux1201 := [[[[[[aux1189 & aux1192] & [t_at_8 = 2]] & [e_at_8 <> 0]] & [e_at_8 <> 40]] & [~ aux1195]] & aux1196].
prop aux1202 := [[aux1189 & aux1192] & aux1194].
prop aux1203 := [[[[[[aux1189 & aux1191] & [t_at_8 = 2]] & [e_at_8 <> 0]] & [e_at_8 <> 40]] & aux1195] & aux1196].
prop aux1204 := [[[aux1188 & aux1193] & [e_at_8 = 0]] & aux1197].
prop aux1205 := [[[aux1189 & aux1193] & [e_at_8 = 0]] & aux1197].
prop aux1206 := [[[[[[[aux1198 | aux1199] | aux1200] | aux1201] | aux1202] | aux1203] | aux1204] | aux1205].
prop aux1207 := [[[[[d_at_9 >= 0] & [t_at_9 = (t_aux_at_9 + d_at_9)]] & [e_at_9 = (e_aux_at_9 + (5 * d_at_9))]] & [(2 * p_at_9) >= ((2 * p_aux_at_9) - d_at_9)]] & [p_at_9 <= (p_aux_at_9 + (6 * d_at_9))]].
prop aux1208 := [[aux1191 | aux1192] => [[[t_at_9 <= 2] & [e_at_9 >= 0]] & [p_at_9 <= 40]]].
prop aux1209 := [aux1193 => [d_at_9 = 0]].
prop aux1210 := [~ [pc1_at_9 & pc2_at_9]].
prop aux1211 := [[~ pc1_at_9] & [~ pc2_at_9]].
prop aux1212 := [pc1_at_9 & [~ pc2_at_9]].
prop aux1213 := [[~ pc1_at_9] & pc2_at_9].
prop aux1214 := [[~ pc1_at_10] & [~ pc2_at_10]].
prop aux1215 := [pc1_at_10 & [~ pc2_at_10]].
prop aux1216 := [[~ pc1_at_10] & pc2_at_10].
prop aux1217 := [[[[[[e_at_9 = 40] & [e_aux_at_10 = 0]] & [p_aux_at_10 = p_at_9]] & [t_aux_at_10 = t_at_9]] | [[[[p_at_9 = 40] & [p_aux_at_10 = 0]] & [e_aux_at_10 = e_at_9]] & [t_aux_at_10 = t_at_9]]] | [[[[p_at_9 = 0] & [p_aux_at_10 = 40]] & [e_aux_at_10 = e_at_9]] & [t_aux_at_10 = t_at_9]]].
prop aux1218 := [(((5 * p_at_9) - (6 * e_at_9)) + 40) < 0].
prop aux1219 := [[[t_aux_at_10 = 0] & [p_aux_at_10 = p_at_9]] & [e_aux_at_10 = e_at_9]].
prop aux1220 := [[[t_aux_at_10 = t_at_9] & [p_aux_at_10 = p_at_9]] & [e_aux_at_10 = e_at_9]].
prop aux1221 := [[[[[[aux1211 & aux1214] & [t_at_9 = 2]] & [e_at_9 <> 0]] & [e_at_9 <> 40]] & aux1218] & aux1219].
prop aux1222 := [[aux1211 & aux1214] & aux1217].
prop aux1223 := [[[[[[aux1211 & aux1215] & [t_at_9 = 2]] & [e_at_9 <> 0]] & [e_at_9 <> 40]] & [~ aux1218]] & aux1219].
prop aux1224 := [[[[[[aux1212 & aux1215] & [t_at_9 = 2]] & [e_at_9 <> 0]] & [e_at_9 <> 40]] & [~ aux1218]] & aux1219].
prop aux1225 := [[aux1212 & aux1215] & aux1217].
prop aux1226 := [[[[[[aux1212 & aux1214] & [t_at_9 = 2]] & [e_at_9 <> 0]] & [e_at_9 <> 40]] & aux1218] & aux1219].
prop aux1227 := [[[aux1211 & aux1216] & [e_at_9 = 0]] & aux1220].
prop aux1228 := [[[aux1212 & aux1216] & [e_at_9 = 0]] & aux1220].
prop aux1229 := [[[[[[[aux1221 | aux1222] | aux1223] | aux1224] | aux1225] | aux1226] | aux1227] | aux1228].
prop aux1230 := [[[[[d_at_10 >= 0] & [t_at_10 = (t_aux_at_10 + d_at_10)]] & [e_at_10 = (e_aux_at_10 + (5 * d_at_10))]] & [(2 * p_at_10) >= ((2 * p_aux_at_10) - d_at_10)]] & [p_at_10 <= (p_aux_at_10 + (6 * d_at_10))]].
prop aux1231 := [[aux1214 | aux1215] => [[[t_at_10 <= 2] & [e_at_10 >= 0]] & [p_at_10 <= 40]]].
prop aux1232 := [aux1216 => [d_at_10 = 0]].
prop aux1233 := [~ [pc1_at_10 & pc2_at_10]].
prop aux1234 := [[~ pc1_at_10] & [~ pc2_at_10]].
prop aux1235 := [pc1_at_10 & [~ pc2_at_10]].
prop aux1236 := [[~ pc1_at_10] & pc2_at_10].
prop aux1237 := [[~ pc1_at_11] & [~ pc2_at_11]].
prop aux1238 := [pc1_at_11 & [~ pc2_at_11]].
prop aux1239 := [[~ pc1_at_11] & pc2_at_11].
prop aux1240 := [[[[[[e_at_10 = 40] & [e_aux_at_11 = 0]] & [p_aux_at_11 = p_at_10]] & [t_aux_at_11 = t_at_10]] | [[[[p_at_10 = 40] & [p_aux_at_11 = 0]] & [e_aux_at_11 = e_at_10]] & [t_aux_at_11 = t_at_10]]] | [[[[p_at_10 = 0] & [p_aux_at_11 = 40]] & [e_aux_at_11 = e_at_10]] & [t_aux_at_11 = t_at_10]]].
prop aux1241 := [(((5 * p_at_10) - (6 * e_at_10)) + 40) < 0].
prop aux1242 := [[[t_aux_at_11 = 0] & [p_aux_at_11 = p_at_10]] & [e_aux_at_11 = e_at_10]].
prop aux1243 := [[[t_aux_at_11 = t_at_10] & [p_aux_at_11 = p_at_10]] & [e_aux_at_11 = e_at_10]].
prop aux1244 := [[[[[[aux1234 & aux1237] & [t_at_10 = 2]] & [e_at_10 <> 0]] & [e_at_10 <> 40]] & aux1241] & aux1242].
prop aux1245 := [[aux1234 & aux1237] & aux1240].
prop aux1246 := [[[[[[aux1234 & aux1238] & [t_at_10 = 2]] & [e_at_10 <> 0]] & [e_at_10 <> 40]] & [~ aux1241]] & aux1242].
prop aux1247 := [[[[[[aux1235 & aux1238] & [t_at_10 = 2]] & [e_at_10 <> 0]] & [e_at_10 <> 40]] & [~ aux1241]] & aux1242].
prop aux1248 := [[aux1235 & aux1238] & aux1240].
prop aux1249 := [[[[[[aux1235 & aux1237] & [t_at_10 = 2]] & [e_at_10 <> 0]] & [e_at_10 <> 40]] & aux1241] & aux1242].
prop aux1250 := [[[aux1234 & aux1239] & [e_at_10 = 0]] & aux1243].
prop aux1251 := [[[aux1235 & aux1239] & [e_at_10 = 0]] & aux1243].
prop aux1252 := [[[[[[[aux1244 | aux1245] | aux1246] | aux1247] | aux1248] | aux1249] | aux1250] | aux1251].
prop aux1253 := [[[[[d_at_11 >= 0] & [t_at_11 = (t_aux_at_11 + d_at_11)]] & [e_at_11 = (e_aux_at_11 + (5 * d_at_11))]] & [(2 * p_at_11) >= ((2 * p_aux_at_11) - d_at_11)]] & [p_at_11 <= (p_aux_at_11 + (6 * d_at_11))]].
prop aux1254 := [[aux1237 | aux1238] => [[[t_at_11 <= 2] & [e_at_11 >= 0]] & [p_at_11 <= 40]]].
prop aux1255 := [aux1239 => [d_at_11 = 0]].
prop aux1256 := [~ [pc1_at_11 & pc2_at_11]].
prop aux1257 := [[~ pc1_at_11] & [~ pc2_at_11]].
prop aux1258 := [pc1_at_11 & [~ pc2_at_11]].
prop aux1259 := [[~ pc1_at_11] & pc2_at_11].
prop aux1260 := [[~ pc1_at_12] & [~ pc2_at_12]].
prop aux1261 := [pc1_at_12 & [~ pc2_at_12]].
prop aux1262 := [[~ pc1_at_12] & pc2_at_12].
prop aux1263 := [[[[[[e_at_11 = 40] & [e_aux_at_12 = 0]] & [p_aux_at_12 = p_at_11]] & [t_aux_at_12 = t_at_11]] | [[[[p_at_11 = 40] & [p_aux_at_12 = 0]] & [e_aux_at_12 = e_at_11]] & [t_aux_at_12 = t_at_11]]] | [[[[p_at_11 = 0] & [p_aux_at_12 = 40]] & [e_aux_at_12 = e_at_11]] & [t_aux_at_12 = t_at_11]]].
prop aux1264 := [(((5 * p_at_11) - (6 * e_at_11)) + 40) < 0].
prop aux1265 := [[[t_aux_at_12 = 0] & [p_aux_at_12 = p_at_11]] & [e_aux_at_12 = e_at_11]].
prop aux1266 := [[[t_aux_at_12 = t_at_11] & [p_aux_at_12 = p_at_11]] & [e_aux_at_12 = e_at_11]].
prop aux1267 := [[[[[[aux1257 & aux1260] & [t_at_11 = 2]] & [e_at_11 <> 0]] & [e_at_11 <> 40]] & aux1264] & aux1265].
prop aux1268 := [[aux1257 & aux1260] & aux1263].
prop aux1269 := [[[[[[aux1257 & aux1261] & [t_at_11 = 2]] & [e_at_11 <> 0]] & [e_at_11 <> 40]] & [~ aux1264]] & aux1265].
prop aux1270 := [[[[[[aux1258 & aux1261] & [t_at_11 = 2]] & [e_at_11 <> 0]] & [e_at_11 <> 40]] & [~ aux1264]] & aux1265].
prop aux1271 := [[aux1258 & aux1261] & aux1263].
prop aux1272 := [[[[[[aux1258 & aux1260] & [t_at_11 = 2]] & [e_at_11 <> 0]] & [e_at_11 <> 40]] & aux1264] & aux1265].
prop aux1273 := [[[aux1257 & aux1262] & [e_at_11 = 0]] & aux1266].
prop aux1274 := [[[aux1258 & aux1262] & [e_at_11 = 0]] & aux1266].
prop aux1275 := [[[[[[[aux1267 | aux1268] | aux1269] | aux1270] | aux1271] | aux1272] | aux1273] | aux1274].
prop aux1276 := [[[[[d_at_12 >= 0] & [t_at_12 = (t_aux_at_12 + d_at_12)]] & [e_at_12 = (e_aux_at_12 + (5 * d_at_12))]] & [(2 * p_at_12) >= ((2 * p_aux_at_12) - d_at_12)]] & [p_at_12 <= (p_aux_at_12 + (6 * d_at_12))]].
prop aux1277 := [[aux1260 | aux1261] => [[[t_at_12 <= 2] & [e_at_12 >= 0]] & [p_at_12 <= 40]]].
prop aux1278 := [aux1262 => [d_at_12 = 0]].
prop aux1279 := [~ [pc1_at_12 & pc2_at_12]].
prop aux1280 := [[~ pc1_at_12] & [~ pc2_at_12]].
prop aux1281 := [pc1_at_12 & [~ pc2_at_12]].
prop aux1282 := [[~ pc1_at_12] & pc2_at_12].
prop aux1283 := [[~ pc1_at_13] & [~ pc2_at_13]].
prop aux1284 := [pc1_at_13 & [~ pc2_at_13]].
prop aux1285 := [[~ pc1_at_13] & pc2_at_13].
prop aux1286 := [[[[[[e_at_12 = 40] & [e_aux_at_13 = 0]] & [p_aux_at_13 = p_at_12]] & [t_aux_at_13 = t_at_12]] | [[[[p_at_12 = 40] & [p_aux_at_13 = 0]] & [e_aux_at_13 = e_at_12]] & [t_aux_at_13 = t_at_12]]] | [[[[p_at_12 = 0] & [p_aux_at_13 = 40]] & [e_aux_at_13 = e_at_12]] & [t_aux_at_13 = t_at_12]]].
prop aux1287 := [(((5 * p_at_12) - (6 * e_at_12)) + 40) < 0].
prop aux1288 := [[[t_aux_at_13 = 0] & [p_aux_at_13 = p_at_12]] & [e_aux_at_13 = e_at_12]].
prop aux1289 := [[[t_aux_at_13 = t_at_12] & [p_aux_at_13 = p_at_12]] & [e_aux_at_13 = e_at_12]].
prop aux1290 := [[[[[[aux1280 & aux1283] & [t_at_12 = 2]] & [e_at_12 <> 0]] & [e_at_12 <> 40]] & aux1287] & aux1288].
prop aux1291 := [[aux1280 & aux1283] & aux1286].
prop aux1292 := [[[[[[aux1280 & aux1284] & [t_at_12 = 2]] & [e_at_12 <> 0]] & [e_at_12 <> 40]] & [~ aux1287]] & aux1288].
prop aux1293 := [[[[[[aux1281 & aux1284] & [t_at_12 = 2]] & [e_at_12 <> 0]] & [e_at_12 <> 40]] & [~ aux1287]] & aux1288].
prop aux1294 := [[aux1281 & aux1284] & aux1286].
prop aux1295 := [[[[[[aux1281 & aux1283] & [t_at_12 = 2]] & [e_at_12 <> 0]] & [e_at_12 <> 40]] & aux1287] & aux1288].
prop aux1296 := [[[aux1280 & aux1285] & [e_at_12 = 0]] & aux1289].
prop aux1297 := [[[aux1281 & aux1285] & [e_at_12 = 0]] & aux1289].
prop aux1298 := [[[[[[[aux1290 | aux1291] | aux1292] | aux1293] | aux1294] | aux1295] | aux1296] | aux1297].
prop aux1299 := [[[[[d_at_13 >= 0] & [t_at_13 = (t_aux_at_13 + d_at_13)]] & [e_at_13 = (e_aux_at_13 + (5 * d_at_13))]] & [(2 * p_at_13) >= ((2 * p_aux_at_13) - d_at_13)]] & [p_at_13 <= (p_aux_at_13 + (6 * d_at_13))]].
prop aux1300 := [[aux1283 | aux1284] => [[[t_at_13 <= 2] & [e_at_13 >= 0]] & [p_at_13 <= 40]]].
prop aux1301 := [aux1285 => [d_at_13 = 0]].
prop aux1302 := [~ [pc1_at_13 & pc2_at_13]].
prop aux1303 := [[~ pc1_at_13] & [~ pc2_at_13]].
prop aux1304 := [pc1_at_13 & [~ pc2_at_13]].
prop aux1305 := [[~ pc1_at_13] & pc2_at_13].
prop aux1306 := [[~ pc1_at_14] & [~ pc2_at_14]].
prop aux1307 := [pc1_at_14 & [~ pc2_at_14]].
prop aux1308 := [[~ pc1_at_14] & pc2_at_14].
prop aux1309 := [[[[[[e_at_13 = 40] & [e_aux_at_14 = 0]] & [p_aux_at_14 = p_at_13]] & [t_aux_at_14 = t_at_13]] | [[[[p_at_13 = 40] & [p_aux_at_14 = 0]] & [e_aux_at_14 = e_at_13]] & [t_aux_at_14 = t_at_13]]] | [[[[p_at_13 = 0] & [p_aux_at_14 = 40]] & [e_aux_at_14 = e_at_13]] & [t_aux_at_14 = t_at_13]]].
prop aux1310 := [(((5 * p_at_13) - (6 * e_at_13)) + 40) < 0].
prop aux1311 := [[[t_aux_at_14 = 0] & [p_aux_at_14 = p_at_13]] & [e_aux_at_14 = e_at_13]].
prop aux1312 := [[[t_aux_at_14 = t_at_13] & [p_aux_at_14 = p_at_13]] & [e_aux_at_14 = e_at_13]].
prop aux1313 := [[[[[[aux1303 & aux1306] & [t_at_13 = 2]] & [e_at_13 <> 0]] & [e_at_13 <> 40]] & aux1310] & aux1311].
prop aux1314 := [[aux1303 & aux1306] & aux1309].
prop aux1315 := [[[[[[aux1303 & aux1307] & [t_at_13 = 2]] & [e_at_13 <> 0]] & [e_at_13 <> 40]] & [~ aux1310]] & aux1311].
prop aux1316 := [[[[[[aux1304 & aux1307] & [t_at_13 = 2]] & [e_at_13 <> 0]] & [e_at_13 <> 40]] & [~ aux1310]] & aux1311].
prop aux1317 := [[aux1304 & aux1307] & aux1309].
prop aux1318 := [[[[[[aux1304 & aux1306] & [t_at_13 = 2]] & [e_at_13 <> 0]] & [e_at_13 <> 40]] & aux1310] & aux1311].
prop aux1319 := [[[aux1303 & aux1308] & [e_at_13 = 0]] & aux1312].
prop aux1320 := [[[aux1304 & aux1308] & [e_at_13 = 0]] & aux1312].
prop aux1321 := [[[[[[[aux1313 | aux1314] | aux1315] | aux1316] | aux1317] | aux1318] | aux1319] | aux1320].
prop aux1322 := [[[[[d_at_14 >= 0] & [t_at_14 = (t_aux_at_14 + d_at_14)]] & [e_at_14 = (e_aux_at_14 + (5 * d_at_14))]] & [(2 * p_at_14) >= ((2 * p_aux_at_14) - d_at_14)]] & [p_at_14 <= (p_aux_at_14 + (6 * d_at_14))]].
prop aux1323 := [[aux1306 | aux1307] => [[[t_at_14 <= 2] & [e_at_14 >= 0]] & [p_at_14 <= 40]]].
prop aux1324 := [aux1308 => [d_at_14 = 0]].
prop aux1325 := [~ [pc1_at_14 & pc2_at_14]].
prop aux1326 := [[~ pc1_at_14] & [~ pc2_at_14]].
prop aux1327 := [pc1_at_14 & [~ pc2_at_14]].
prop aux1328 := [[~ pc1_at_14] & pc2_at_14].
prop aux1329 := [[~ pc1_at_15] & [~ pc2_at_15]].
prop aux1330 := [pc1_at_15 & [~ pc2_at_15]].
prop aux1331 := [[~ pc1_at_15] & pc2_at_15].
prop aux1332 := [[[[[[e_at_14 = 40] & [e_aux_at_15 = 0]] & [p_aux_at_15 = p_at_14]] & [t_aux_at_15 = t_at_14]] | [[[[p_at_14 = 40] & [p_aux_at_15 = 0]] & [e_aux_at_15 = e_at_14]] & [t_aux_at_15 = t_at_14]]] | [[[[p_at_14 = 0] & [p_aux_at_15 = 40]] & [e_aux_at_15 = e_at_14]] & [t_aux_at_15 = t_at_14]]].
prop aux1333 := [(((5 * p_at_14) - (6 * e_at_14)) + 40) < 0].
prop aux1334 := [[[t_aux_at_15 = 0] & [p_aux_at_15 = p_at_14]] & [e_aux_at_15 = e_at_14]].
prop aux1335 := [[[t_aux_at_15 = t_at_14] & [p_aux_at_15 = p_at_14]] & [e_aux_at_15 = e_at_14]].
prop aux1336 := [[[[[[aux1326 & aux1329] & [t_at_14 = 2]] & [e_at_14 <> 0]] & [e_at_14 <> 40]] & aux1333] & aux1334].
prop aux1337 := [[aux1326 & aux1329] & aux1332].
prop aux1338 := [[[[[[aux1326 & aux1330] & [t_at_14 = 2]] & [e_at_14 <> 0]] & [e_at_14 <> 40]] & [~ aux1333]] & aux1334].
prop aux1339 := [[[[[[aux1327 & aux1330] & [t_at_14 = 2]] & [e_at_14 <> 0]] & [e_at_14 <> 40]] & [~ aux1333]] & aux1334].
prop aux1340 := [[aux1327 & aux1330] & aux1332].
prop aux1341 := [[[[[[aux1327 & aux1329] & [t_at_14 = 2]] & [e_at_14 <> 0]] & [e_at_14 <> 40]] & aux1333] & aux1334].
prop aux1342 := [[[aux1326 & aux1331] & [e_at_14 = 0]] & aux1335].
prop aux1343 := [[[aux1327 & aux1331] & [e_at_14 = 0]] & aux1335].
prop aux1344 := [[[[[[[aux1336 | aux1337] | aux1338] | aux1339] | aux1340] | aux1341] | aux1342] | aux1343].
prop aux1345 := [[[[[d_at_15 >= 0] & [t_at_15 = (t_aux_at_15 + d_at_15)]] & [e_at_15 = (e_aux_at_15 + (5 * d_at_15))]] & [(2 * p_at_15) >= ((2 * p_aux_at_15) - d_at_15)]] & [p_at_15 <= (p_aux_at_15 + (6 * d_at_15))]].
prop aux1346 := [[aux1329 | aux1330] => [[[t_at_15 <= 2] & [e_at_15 >= 0]] & [p_at_15 <= 40]]].
prop aux1347 := [aux1331 => [d_at_15 = 0]].
prop aux1348 := [~ [pc1_at_15 & pc2_at_15]].
prop aux1349 := [[~ pc1_at_15] & [~ pc2_at_15]].
prop aux1350 := [pc1_at_15 & [~ pc2_at_15]].
prop aux1351 := [[~ pc1_at_15] & pc2_at_15].
prop aux1352 := [[~ pc1_at_16] & [~ pc2_at_16]].
prop aux1353 := [pc1_at_16 & [~ pc2_at_16]].
prop aux1354 := [[~ pc1_at_16] & pc2_at_16].
prop aux1355 := [[[[[[e_at_15 = 40] & [e_aux_at_16 = 0]] & [p_aux_at_16 = p_at_15]] & [t_aux_at_16 = t_at_15]] | [[[[p_at_15 = 40] & [p_aux_at_16 = 0]] & [e_aux_at_16 = e_at_15]] & [t_aux_at_16 = t_at_15]]] | [[[[p_at_15 = 0] & [p_aux_at_16 = 40]] & [e_aux_at_16 = e_at_15]] & [t_aux_at_16 = t_at_15]]].
prop aux1356 := [(((5 * p_at_15) - (6 * e_at_15)) + 40) < 0].
prop aux1357 := [[[t_aux_at_16 = 0] & [p_aux_at_16 = p_at_15]] & [e_aux_at_16 = e_at_15]].
prop aux1358 := [[[t_aux_at_16 = t_at_15] & [p_aux_at_16 = p_at_15]] & [e_aux_at_16 = e_at_15]].
prop aux1359 := [[[[[[aux1349 & aux1352] & [t_at_15 = 2]] & [e_at_15 <> 0]] & [e_at_15 <> 40]] & aux1356] & aux1357].
prop aux1360 := [[aux1349 & aux1352] & aux1355].
prop aux1361 := [[[[[[aux1349 & aux1353] & [t_at_15 = 2]] & [e_at_15 <> 0]] & [e_at_15 <> 40]] & [~ aux1356]] & aux1357].
prop aux1362 := [[[[[[aux1350 & aux1353] & [t_at_15 = 2]] & [e_at_15 <> 0]] & [e_at_15 <> 40]] & [~ aux1356]] & aux1357].
prop aux1363 := [[aux1350 & aux1353] & aux1355].
prop aux1364 := [[[[[[aux1350 & aux1352] & [t_at_15 = 2]] & [e_at_15 <> 0]] & [e_at_15 <> 40]] & aux1356] & aux1357].
prop aux1365 := [[[aux1349 & aux1354] & [e_at_15 = 0]] & aux1358].
prop aux1366 := [[[aux1350 & aux1354] & [e_at_15 = 0]] & aux1358].
prop aux1367 := [[[[[[[aux1359 | aux1360] | aux1361] | aux1362] | aux1363] | aux1364] | aux1365] | aux1366].
prop aux1368 := [[[[[d_at_16 >= 0] & [t_at_16 = (t_aux_at_16 + d_at_16)]] & [e_at_16 = (e_aux_at_16 + (5 * d_at_16))]] & [(2 * p_at_16) >= ((2 * p_aux_at_16) - d_at_16)]] & [p_at_16 <= (p_aux_at_16 + (6 * d_at_16))]].
prop aux1369 := [[aux1352 | aux1353] => [[[t_at_16 <= 2] & [e_at_16 >= 0]] & [p_at_16 <= 40]]].
prop aux1370 := [aux1354 => [d_at_16 = 0]].
prop aux1371 := [~ [pc1_at_16 & pc2_at_16]].
prop aux1372 := [[~ pc1_at_16] & [~ pc2_at_16]].
prop aux1373 := [pc1_at_16 & [~ pc2_at_16]].
prop aux1374 := [[~ pc1_at_16] & pc2_at_16].
prop aux1375 := [[~ pc1_at_17] & [~ pc2_at_17]].
prop aux1376 := [pc1_at_17 & [~ pc2_at_17]].
prop aux1377 := [[~ pc1_at_17] & pc2_at_17].
prop aux1378 := [[[[[[e_at_16 = 40] & [e_aux_at_17 = 0]] & [p_aux_at_17 = p_at_16]] & [t_aux_at_17 = t_at_16]] | [[[[p_at_16 = 40] & [p_aux_at_17 = 0]] & [e_aux_at_17 = e_at_16]] & [t_aux_at_17 = t_at_16]]] | [[[[p_at_16 = 0] & [p_aux_at_17 = 40]] & [e_aux_at_17 = e_at_16]] & [t_aux_at_17 = t_at_16]]].
prop aux1379 := [(((5 * p_at_16) - (6 * e_at_16)) + 40) < 0].
prop aux1380 := [[[t_aux_at_17 = 0] & [p_aux_at_17 = p_at_16]] & [e_aux_at_17 = e_at_16]].
prop aux1381 := [[[t_aux_at_17 = t_at_16] & [p_aux_at_17 = p_at_16]] & [e_aux_at_17 = e_at_16]].
prop aux1382 := [[[[[[aux1372 & aux1375] & [t_at_16 = 2]] & [e_at_16 <> 0]] & [e_at_16 <> 40]] & aux1379] & aux1380].
prop aux1383 := [[aux1372 & aux1375] & aux1378].
prop aux1384 := [[[[[[aux1372 & aux1376] & [t_at_16 = 2]] & [e_at_16 <> 0]] & [e_at_16 <> 40]] & [~ aux1379]] & aux1380].
prop aux1385 := [[[[[[aux1373 & aux1376] & [t_at_16 = 2]] & [e_at_16 <> 0]] & [e_at_16 <> 40]] & [~ aux1379]] & aux1380].
prop aux1386 := [[aux1373 & aux1376] & aux1378].
prop aux1387 := [[[[[[aux1373 & aux1375] & [t_at_16 = 2]] & [e_at_16 <> 0]] & [e_at_16 <> 40]] & aux1379] & aux1380].
prop aux1388 := [[[aux1372 & aux1377] & [e_at_16 = 0]] & aux1381].
prop aux1389 := [[[aux1373 & aux1377] & [e_at_16 = 0]] & aux1381].
prop aux1390 := [[[[[[[aux1382 | aux1383] | aux1384] | aux1385] | aux1386] | aux1387] | aux1388] | aux1389].
prop aux1391 := [[[[[d_at_17 >= 0] & [t_at_17 = (t_aux_at_17 + d_at_17)]] & [e_at_17 = (e_aux_at_17 + (5 * d_at_17))]] & [(2 * p_at_17) >= ((2 * p_aux_at_17) - d_at_17)]] & [p_at_17 <= (p_aux_at_17 + (6 * d_at_17))]].
prop aux1392 := [[aux1375 | aux1376] => [[[t_at_17 <= 2] & [e_at_17 >= 0]] & [p_at_17 <= 40]]].
prop aux1393 := [aux1377 => [d_at_17 = 0]].
prop aux1394 := [~ [pc1_at_17 & pc2_at_17]].
prop aux1395 := [[~ pc1_at_17] & [~ pc2_at_17]].
prop aux1396 := [pc1_at_17 & [~ pc2_at_17]].
prop aux1397 := [[~ pc1_at_17] & pc2_at_17].
prop aux1398 := [[~ pc1_at_18] & [~ pc2_at_18]].
prop aux1399 := [pc1_at_18 & [~ pc2_at_18]].
prop aux1400 := [[~ pc1_at_18] & pc2_at_18].
prop aux1401 := [[[[[[e_at_17 = 40] & [e_aux_at_18 = 0]] & [p_aux_at_18 = p_at_17]] & [t_aux_at_18 = t_at_17]] | [[[[p_at_17 = 40] & [p_aux_at_18 = 0]] & [e_aux_at_18 = e_at_17]] & [t_aux_at_18 = t_at_17]]] | [[[[p_at_17 = 0] & [p_aux_at_18 = 40]] & [e_aux_at_18 = e_at_17]] & [t_aux_at_18 = t_at_17]]].
prop aux1402 := [(((5 * p_at_17) - (6 * e_at_17)) + 40) < 0].
prop aux1403 := [[[t_aux_at_18 = 0] & [p_aux_at_18 = p_at_17]] & [e_aux_at_18 = e_at_17]].
prop aux1404 := [[[t_aux_at_18 = t_at_17] & [p_aux_at_18 = p_at_17]] & [e_aux_at_18 = e_at_17]].
prop aux1405 := [[[[[[aux1395 & aux1398] & [t_at_17 = 2]] & [e_at_17 <> 0]] & [e_at_17 <> 40]] & aux1402] & aux1403].
prop aux1406 := [[aux1395 & aux1398] & aux1401].
prop aux1407 := [[[[[[aux1395 & aux1399] & [t_at_17 = 2]] & [e_at_17 <> 0]] & [e_at_17 <> 40]] & [~ aux1402]] & aux1403].
prop aux1408 := [[[[[[aux1396 & aux1399] & [t_at_17 = 2]] & [e_at_17 <> 0]] & [e_at_17 <> 40]] & [~ aux1402]] & aux1403].
prop aux1409 := [[aux1396 & aux1399] & aux1401].
prop aux1410 := [[[[[[aux1396 & aux1398] & [t_at_17 = 2]] & [e_at_17 <> 0]] & [e_at_17 <> 40]] & aux1402] & aux1403].
prop aux1411 := [[[aux1395 & aux1400] & [e_at_17 = 0]] & aux1404].
prop aux1412 := [[[aux1396 & aux1400] & [e_at_17 = 0]] & aux1404].
prop aux1413 := [[[[[[[aux1405 | aux1406] | aux1407] | aux1408] | aux1409] | aux1410] | aux1411] | aux1412].
prop aux1414 := [[[[[d_at_18 >= 0] & [t_at_18 = (t_aux_at_18 + d_at_18)]] & [e_at_18 = (e_aux_at_18 + (5 * d_at_18))]] & [(2 * p_at_18) >= ((2 * p_aux_at_18) - d_at_18)]] & [p_at_18 <= (p_aux_at_18 + (6 * d_at_18))]].
prop aux1415 := [[aux1398 | aux1399] => [[[t_at_18 <= 2] & [e_at_18 >= 0]] & [p_at_18 <= 40]]].
prop aux1416 := [aux1400 => [d_at_18 = 0]].
prop aux1417 := [~ [pc1_at_18 & pc2_at_18]].
prop aux1418 := [[~ pc1_at_18] & [~ pc2_at_18]].
prop aux1419 := [pc1_at_18 & [~ pc2_at_18]].
prop aux1420 := [[~ pc1_at_18] & pc2_at_18].
prop aux1421 := [[~ pc1_at_19] & [~ pc2_at_19]].
prop aux1422 := [pc1_at_19 & [~ pc2_at_19]].
prop aux1423 := [[~ pc1_at_19] & pc2_at_19].
prop aux1424 := [[[[[[e_at_18 = 40] & [e_aux_at_19 = 0]] & [p_aux_at_19 = p_at_18]] & [t_aux_at_19 = t_at_18]] | [[[[p_at_18 = 40] & [p_aux_at_19 = 0]] & [e_aux_at_19 = e_at_18]] & [t_aux_at_19 = t_at_18]]] | [[[[p_at_18 = 0] & [p_aux_at_19 = 40]] & [e_aux_at_19 = e_at_18]] & [t_aux_at_19 = t_at_18]]].
prop aux1425 := [(((5 * p_at_18) - (6 * e_at_18)) + 40) < 0].
prop aux1426 := [[[t_aux_at_19 = 0] & [p_aux_at_19 = p_at_18]] & [e_aux_at_19 = e_at_18]].
prop aux1427 := [[[t_aux_at_19 = t_at_18] & [p_aux_at_19 = p_at_18]] & [e_aux_at_19 = e_at_18]].
prop aux1428 := [[[[[[aux1418 & aux1421] & [t_at_18 = 2]] & [e_at_18 <> 0]] & [e_at_18 <> 40]] & aux1425] & aux1426].
prop aux1429 := [[aux1418 & aux1421] & aux1424].
prop aux1430 := [[[[[[aux1418 & aux1422] & [t_at_18 = 2]] & [e_at_18 <> 0]] & [e_at_18 <> 40]] & [~ aux1425]] & aux1426].
prop aux1431 := [[[[[[aux1419 & aux1422] & [t_at_18 = 2]] & [e_at_18 <> 0]] & [e_at_18 <> 40]] & [~ aux1425]] & aux1426].
prop aux1432 := [[aux1419 & aux1422] & aux1424].
prop aux1433 := [[[[[[aux1419 & aux1421] & [t_at_18 = 2]] & [e_at_18 <> 0]] & [e_at_18 <> 40]] & aux1425] & aux1426].
prop aux1434 := [[[aux1418 & aux1423] & [e_at_18 = 0]] & aux1427].
prop aux1435 := [[[aux1419 & aux1423] & [e_at_18 = 0]] & aux1427].
prop aux1436 := [[[[[[[aux1428 | aux1429] | aux1430] | aux1431] | aux1432] | aux1433] | aux1434] | aux1435].
prop aux1437 := [[[[[d_at_19 >= 0] & [t_at_19 = (t_aux_at_19 + d_at_19)]] & [e_at_19 = (e_aux_at_19 + (5 * d_at_19))]] & [(2 * p_at_19) >= ((2 * p_aux_at_19) - d_at_19)]] & [p_at_19 <= (p_aux_at_19 + (6 * d_at_19))]].
prop aux1438 := [[aux1421 | aux1422] => [[[t_at_19 <= 2] & [e_at_19 >= 0]] & [p_at_19 <= 40]]].
prop aux1439 := [aux1423 => [d_at_19 = 0]].
prop aux1440 := [~ [pc1_at_19 & pc2_at_19]].
sat ~[
[[[[aux1001 & aux1002] & aux1003] & [[[[[aux1022 & aux1023] & aux1024] & aux1025] & aux1026] & [[[[aux1045 & aux1046] & aux1047] & aux1048] & aux1049] & [[[[aux1068 & aux1069] & aux1070] & aux1071] & aux1072] & [[[[aux1091 & aux1092] & aux1093] & aux1094] & aux1095] & [[[[aux1114 & aux1115] & aux1116] & aux1117] & aux1118] & [[[[aux1137 & aux1138] & aux1139] & aux1140] & aux1141] & [[[[aux1160 & aux1161] & aux1162] & aux1163] & aux1164] & [[[[aux1183 & aux1184] & aux1185] & aux1186] & aux1187] & [[[[aux1206 & aux1207] & aux1208] & aux1209] & aux1210] & [[[[aux1229 & aux1230] & aux1231] & aux1232] & aux1233] & [[[[aux1252 & aux1253] & aux1254] & aux1255] & aux1256] & [[[[aux1275 & aux1276] & aux1277] & aux1278] & aux1279] & [[[[aux1298 & aux1299] & aux1300] & aux1301] & aux1302] & [[[[aux1321 & aux1322] & aux1323] & aux1324] & aux1325] & [[[[aux1344 & aux1345] & aux1346] & aux1347] & aux1348] & [[[[aux1367 & aux1368] & aux1369] & aux1370] & aux1371] & [[[[aux1390 & aux1391] & aux1392] & aux1393] & aux1394] & [[[[aux1413 & aux1414] & aux1415] & aux1416] & aux1417] & [[[[aux1436 & aux1437] & aux1438] & aux1439] & aux1440]] & 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]] & [~ [e_at_5 = p_at_5]] & [~ [e_at_6 = p_at_6]] & [~ [e_at_7 = p_at_7]] & [~ [e_at_8 = p_at_8]] & [~ [e_at_9 = p_at_9]] & [~ [e_at_10 = p_at_10]] & [~ [e_at_11 = p_at_11]] & [~ [e_at_12 = p_at_12]] & [~ [e_at_13 = p_at_13]] & [~ [e_at_14 = p_at_14]] & [~ [e_at_15 = p_at_15]] & [~ [e_at_16 = p_at_16]] & [~ [e_at_17 = p_at_17]] & [~ [e_at_18 = p_at_18]] & [~ [e_at_19 = p_at_19]]]]].