%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : CSR154+1 : TPTP v9.0.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 05:54:39 PM UTC 2025
% Result : Satisfiable 7.33s 2.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR154+1 : TPTP v9.0.0. Released v6.4.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 17:55:39 EDT 2025
% 0.13/0.34 % CPUTime :
% 7.33/2.72
% 7.33/2.72 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.33/2.72
% 7.33/2.72 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.33/2.73 %$ trajectory > antitrajectory > terminates > stoppedIn > startedIn > releases > initiates > releasedAt > less > holdsAt > happens > plus > #nlpp > n1 > n0 > #skF_6 > #skF_1 > #skF_4 > #skF_2 > #skF_8 > #skF_3 > #skF_7 > #skF_5
% 7.33/2.73
% 7.33/2.73 %Foreground sorts:
% 7.33/2.73
% 7.33/2.73
% 7.33/2.73 %Background operators:
% 7.33/2.73
% 7.33/2.73
% 7.33/2.73 %Foreground operators:
% 7.33/2.73 tff('#skF_6', type, '#skF_6': ($i * $i) > $i).
% 7.33/2.73 tff(stoppedIn, type, stoppedIn: ($i * $i * $i) > $o).
% 7.33/2.73 tff('#skF_1', type, '#skF_1': ($i * $i * $i) > $i).
% 7.33/2.73 tff(terminates, type, terminates: ($i * $i * $i) > $o).
% 7.33/2.73 tff(releasedAt, type, releasedAt: ($i * $i) > $o).
% 7.33/2.73 tff('#skF_4', type, '#skF_4': ($i * $i * $i) > $i).
% 7.33/2.73 tff(startedIn, type, startedIn: ($i * $i * $i) > $o).
% 7.33/2.73 tff(trajectory, type, trajectory: ($i * $i * $i * $i) > $o).
% 7.33/2.73 tff(n1, type, n1: $i).
% 7.33/2.73 tff(less, type, less: ($i * $i) > $o).
% 7.33/2.73 tff(plus, type, plus: ($i * $i) > $i).
% 7.33/2.73 tff('#skF_2', type, '#skF_2': ($i * $i * $i) > $i).
% 7.33/2.73 tff(n0, type, n0: $i).
% 7.33/2.73 tff('#skF_8', type, '#skF_8': ($i * $i) > $i).
% 7.33/2.73 tff(antitrajectory, type, antitrajectory: ($i * $i * $i * $i) > $o).
% 7.33/2.73 tff(happens, type, happens: ($i * $i) > $o).
% 7.33/2.73 tff(initiates, type, initiates: ($i * $i * $i) > $o).
% 7.33/2.73 tff('#skF_3', type, '#skF_3': ($i * $i * $i) > $i).
% 7.33/2.73 tff(releases, type, releases: ($i * $i * $i) > $o).
% 7.33/2.73 tff(holdsAt, type, holdsAt: ($i * $i) > $o).
% 7.33/2.73 tff('#skF_7', type, '#skF_7': ($i * $i) > $i).
% 7.33/2.73 tff('#skF_5', type, '#skF_5': ($i * $i) > $i).
% 7.33/2.73
% 7.33/2.73 %Saturated clause set:
% 7.33/2.73 tff(c_1198, plain, (![Fluent_1448, Time2_1449, Fluent_35, Time1_1451, Fluent_1447, Fluent_1452, Time2_1455, Time1_1453, Time1_1454]: (startedIn(Time1_1453, Fluent_35, '#skF_2'('#skF_2'(Time1_1454, Fluent_1452, Time2_1455), Fluent_1448, Time2_1449)) | ~less(Time1_1453, '#skF_2'(Time1_1454, Fluent_1452, Time2_1455)) | stoppedIn('#skF_2'(Time1_1451, Fluent_1447, '#skF_2'(Time1_1454, Fluent_1452, Time2_1455)), Fluent_35, Time2_1455) | ~stoppedIn(Time1_1454, Fluent_1452, Time2_1455) | ~stoppedIn(Time1_1451, Fluent_1447, '#skF_2'(Time1_1454, Fluent_1452, Time2_1455)) | ~stoppedIn('#skF_2'(Time1_1454, Fluent_1452, Time2_1455), Fluent_1448, Time2_1449) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1454, Fluent_1452, Time2_1455), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1454, Fluent_1452, Time2_1455))))).
% 7.33/2.73 tff(c_1192, plain, (![Fluent_1437, Fluent_35, Time1_1434, Time2_1436, Fluent_1429, Fluent_1430, Time2_1433, Time1_1431, Time1_1432]: (startedIn('#skF_2'(Time1_1432, Fluent_1430, '#skF_4'(Time1_1434, Time2_1433, Fluent_1429)), Fluent_35, Time2_1433) | stoppedIn(Time1_1431, Fluent_35, '#skF_2'('#skF_4'(Time1_1434, Time2_1433, Fluent_1429), Fluent_1437, Time2_1436)) | ~less(Time1_1431, '#skF_4'(Time1_1434, Time2_1433, Fluent_1429)) | ~stoppedIn('#skF_4'(Time1_1434, Time2_1433, Fluent_1429), Fluent_1437, Time2_1436) | ~startedIn(Time1_1434, Fluent_1429, Time2_1433) | ~stoppedIn(Time1_1432, Fluent_1430, '#skF_4'(Time1_1434, Time2_1433, Fluent_1429)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1434, Time2_1433, Fluent_1429), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1434, Time2_1433, Fluent_1429))))).
% 7.33/2.74 tff(c_1186, plain, (![Fluent_1417, Time2_1416, Fluent_35, Time2_1411, Time1_1419, Fluent_1412, Time1_1414, Time1_1418, Fluent_1415]: (startedIn(Time1_1414, Fluent_35, '#skF_4'('#skF_4'(Time1_1419, Time2_1411, Fluent_1415), Time2_1416, Fluent_1412)) | ~less(Time1_1414, '#skF_4'(Time1_1419, Time2_1411, Fluent_1415)) | stoppedIn('#skF_4'(Time1_1418, '#skF_4'(Time1_1419, Time2_1411, Fluent_1415), Fluent_1417), Fluent_35, Time2_1411) | ~startedIn(Time1_1419, Fluent_1415, Time2_1411) | ~startedIn(Time1_1418, Fluent_1417, '#skF_4'(Time1_1419, Time2_1411, Fluent_1415)) | ~startedIn('#skF_4'(Time1_1419, Time2_1411, Fluent_1415), Fluent_1412, Time2_1416) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1419, Time2_1411, Fluent_1415), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1419, Time2_1411, Fluent_1415))))).
% 7.33/2.74 tff(c_1180, plain, (![Time2_1397, Time1_1398, Time1_1400, Fluent_35, Time2_1393, Fluent_1396, Fluent_1401, Fluent_1395, Time1_1399]: (startedIn(Time1_1399, Fluent_35, '#skF_2'('#skF_2'(Time1_1400, Fluent_1396, Time2_1393), Fluent_1395, Time2_1397)) | ~less(Time1_1399, '#skF_2'(Time1_1400, Fluent_1396, Time2_1393)) | stoppedIn('#skF_4'(Time1_1398, '#skF_2'(Time1_1400, Fluent_1396, Time2_1393), Fluent_1401), Fluent_35, Time2_1393) | ~stoppedIn(Time1_1400, Fluent_1396, Time2_1393) | ~startedIn(Time1_1398, Fluent_1401, '#skF_2'(Time1_1400, Fluent_1396, Time2_1393)) | ~stoppedIn('#skF_2'(Time1_1400, Fluent_1396, Time2_1393), Fluent_1395, Time2_1397) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1400, Fluent_1396, Time2_1393), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1400, Fluent_1396, Time2_1393))))).
% 7.33/2.74 tff(c_1174, plain, (![Fluent_1375, Time1_1382, Fluent_35, Time1_1380, Time2_1376, Time1_1381, Fluent_1378, Time2_1379, Fluent_1383]: (startedIn(Time1_1381, Fluent_35, '#skF_4'('#skF_2'(Time1_1382, Fluent_1378, Time2_1376), Time2_1379, Fluent_1375)) | ~less(Time1_1381, '#skF_2'(Time1_1382, Fluent_1378, Time2_1376)) | stoppedIn('#skF_4'(Time1_1380, '#skF_2'(Time1_1382, Fluent_1378, Time2_1376), Fluent_1383), Fluent_35, Time2_1376) | ~stoppedIn(Time1_1382, Fluent_1378, Time2_1376) | ~startedIn(Time1_1380, Fluent_1383, '#skF_2'(Time1_1382, Fluent_1378, Time2_1376)) | ~startedIn('#skF_2'(Time1_1382, Fluent_1378, Time2_1376), Fluent_1375, Time2_1379) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1382, Fluent_1378, Time2_1376), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1382, Fluent_1378, Time2_1376))))).
% 7.33/2.74 tff(c_1168, plain, (![Fluent_1357, Fluent_35, Time1_1361, Time2_1360, Fluent_1358, Time2_1365, Time1_1363, Fluent_1359, Time1_1362]: (startedIn(Time1_1362, Fluent_35, '#skF_2'('#skF_4'(Time1_1363, Time2_1365, Fluent_1357), Fluent_1359, Time2_1360)) | ~less(Time1_1362, '#skF_4'(Time1_1363, Time2_1365, Fluent_1357)) | stoppedIn('#skF_2'(Time1_1361, Fluent_1358, '#skF_4'(Time1_1363, Time2_1365, Fluent_1357)), Fluent_35, Time2_1365) | ~startedIn(Time1_1363, Fluent_1357, Time2_1365) | ~stoppedIn(Time1_1361, Fluent_1358, '#skF_4'(Time1_1363, Time2_1365, Fluent_1357)) | ~stoppedIn('#skF_4'(Time1_1363, Time2_1365, Fluent_1357), Fluent_1359, Time2_1360) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1363, Time2_1365, Fluent_1357), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1363, Time2_1365, Fluent_1357))))).
% 7.33/2.74 tff(c_1162, plain, (![Time2_1342, Fluent_35, Fluent_1340, Time1_1343, Time1_1344, Fluent_1339, Time1_1345, Fluent_1341, Time2_1347]: (startedIn(Time1_1344, Fluent_35, '#skF_4'('#skF_4'(Time1_1345, Time2_1347, Fluent_1339), Time2_1342, Fluent_1340)) | ~less(Time1_1344, '#skF_4'(Time1_1345, Time2_1347, Fluent_1339)) | stoppedIn('#skF_2'(Time1_1343, Fluent_1341, '#skF_4'(Time1_1345, Time2_1347, Fluent_1339)), Fluent_35, Time2_1347) | ~startedIn(Time1_1345, Fluent_1339, Time2_1347) | ~stoppedIn(Time1_1343, Fluent_1341, '#skF_4'(Time1_1345, Time2_1347, Fluent_1339)) | ~startedIn('#skF_4'(Time1_1345, Time2_1347, Fluent_1339), Fluent_1340, Time2_1342) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1345, Time2_1347, Fluent_1339), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1345, Time2_1347, Fluent_1339))))).
% 7.33/2.74 tff(c_1156, plain, (![Time2_1323, Time1_1327, Time1_1321, Time1_1324, Time2_1329, Fluent_35, Fluent_1328, Fluent_1325, Fluent_1326]: (startedIn('#skF_2'(Time1_1327, Fluent_1326, '#skF_2'(Time1_1321, Fluent_1325, Time2_1329)), Fluent_35, Time2_1329) | stoppedIn(Time1_1324, Fluent_35, '#skF_4'('#skF_2'(Time1_1321, Fluent_1325, Time2_1329), Time2_1323, Fluent_1328)) | ~less(Time1_1324, '#skF_2'(Time1_1321, Fluent_1325, Time2_1329)) | ~startedIn('#skF_2'(Time1_1321, Fluent_1325, Time2_1329), Fluent_1328, Time2_1323) | ~stoppedIn(Time1_1321, Fluent_1325, Time2_1329) | ~stoppedIn(Time1_1327, Fluent_1326, '#skF_2'(Time1_1321, Fluent_1325, Time2_1329)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1321, Fluent_1325, Time2_1329), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1321, Fluent_1325, Time2_1329))))).
% 7.33/2.74 tff(c_1150, plain, (![Time1_1305, Time1_1309, Fluent_1307, Fluent_35, Fluent_1311, Time1_1308, Time2_1303, Time2_1310, Fluent_1304]: (startedIn('#skF_2'(Time1_1305, Fluent_1304, '#skF_2'(Time1_1308, Fluent_1307, Time2_1303)), Fluent_35, Time2_1303) | stoppedIn(Time1_1309, Fluent_35, '#skF_2'('#skF_2'(Time1_1308, Fluent_1307, Time2_1303), Fluent_1311, Time2_1310)) | ~less(Time1_1309, '#skF_2'(Time1_1308, Fluent_1307, Time2_1303)) | ~stoppedIn('#skF_2'(Time1_1308, Fluent_1307, Time2_1303), Fluent_1311, Time2_1310) | ~stoppedIn(Time1_1308, Fluent_1307, Time2_1303) | ~stoppedIn(Time1_1305, Fluent_1304, '#skF_2'(Time1_1308, Fluent_1307, Time2_1303)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1308, Fluent_1307, Time2_1303), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1308, Fluent_1307, Time2_1303))))).
% 7.33/2.74 tff(c_1144, plain, (![Fluent_1291, Time1_1292, Fluent_35, Time2_1287, Time1_1285, Fluent_1290, Time1_1288, Time2_1293, Fluent_1289]: (startedIn('#skF_4'(Time1_1292, '#skF_2'(Time1_1285, Fluent_1289, Time2_1293), Fluent_1290), Fluent_35, Time2_1293) | stoppedIn(Time1_1288, Fluent_35, '#skF_4'('#skF_2'(Time1_1285, Fluent_1289, Time2_1293), Time2_1287, Fluent_1291)) | ~less(Time1_1288, '#skF_2'(Time1_1285, Fluent_1289, Time2_1293)) | ~startedIn('#skF_2'(Time1_1285, Fluent_1289, Time2_1293), Fluent_1291, Time2_1287) | ~stoppedIn(Time1_1285, Fluent_1289, Time2_1293) | ~startedIn(Time1_1292, Fluent_1290, '#skF_2'(Time1_1285, Fluent_1289, Time2_1293)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1285, Fluent_1289, Time2_1293), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1285, Fluent_1289, Time2_1293))))).
% 7.33/2.74 tff(c_1138, plain, (![Time1_1270, Time2_1273, Fluent_35, Fluent_1274, Time1_1269, Time1_1272, Fluent_1275, Time2_1268, Fluent_1267]: (startedIn('#skF_2'(Time1_1269, Fluent_1267, '#skF_4'(Time1_1272, Time2_1268, Fluent_1274)), Fluent_35, Time2_1268) | stoppedIn(Time1_1270, Fluent_35, '#skF_4'('#skF_4'(Time1_1272, Time2_1268, Fluent_1274), Time2_1273, Fluent_1275)) | ~less(Time1_1270, '#skF_4'(Time1_1272, Time2_1268, Fluent_1274)) | ~startedIn('#skF_4'(Time1_1272, Time2_1268, Fluent_1274), Fluent_1275, Time2_1273) | ~startedIn(Time1_1272, Fluent_1274, Time2_1268) | ~stoppedIn(Time1_1269, Fluent_1267, '#skF_4'(Time1_1272, Time2_1268, Fluent_1274)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1272, Time2_1268, Fluent_1274), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1272, Time2_1268, Fluent_1274))))).
% 7.33/2.74 tff(c_1132, plain, (![Fluent_35, Time2_1252, Time1_1253, Time1_1256, Fluent_1250, Time1_1255, Time2_1257, Fluent_1249, Fluent_1254]: (startedIn(Time1_1255, Fluent_35, '#skF_4'('#skF_2'(Time1_1256, Fluent_1254, Time2_1257), Time2_1252, Fluent_1250)) | ~less(Time1_1255, '#skF_2'(Time1_1256, Fluent_1254, Time2_1257)) | stoppedIn('#skF_2'(Time1_1253, Fluent_1249, '#skF_2'(Time1_1256, Fluent_1254, Time2_1257)), Fluent_35, Time2_1257) | ~stoppedIn(Time1_1256, Fluent_1254, Time2_1257) | ~stoppedIn(Time1_1253, Fluent_1249, '#skF_2'(Time1_1256, Fluent_1254, Time2_1257)) | ~startedIn('#skF_2'(Time1_1256, Fluent_1254, Time2_1257), Fluent_1250, Time2_1252) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1256, Fluent_1254, Time2_1257), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1256, Fluent_1254, Time2_1257))))).
% 7.33/2.74 tff(c_1126, plain, (![Fluent_1239, Time1_1235, Time2_1238, Fluent_35, Fluent_1234, Time1_1237, Time2_1231, Time1_1236, Fluent_1232]: (startedIn('#skF_4'(Time1_1235, '#skF_2'(Time1_1236, Fluent_1234, Time2_1231), Fluent_1232), Fluent_35, Time2_1231) | stoppedIn(Time1_1237, Fluent_35, '#skF_2'('#skF_2'(Time1_1236, Fluent_1234, Time2_1231), Fluent_1239, Time2_1238)) | ~less(Time1_1237, '#skF_2'(Time1_1236, Fluent_1234, Time2_1231)) | ~stoppedIn('#skF_2'(Time1_1236, Fluent_1234, Time2_1231), Fluent_1239, Time2_1238) | ~stoppedIn(Time1_1236, Fluent_1234, Time2_1231) | ~startedIn(Time1_1235, Fluent_1232, '#skF_2'(Time1_1236, Fluent_1234, Time2_1231)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1236, Fluent_1234, Time2_1231), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1236, Fluent_1234, Time2_1231))))).
% 7.33/2.74 tff(c_1120, plain, (![Fluent_1214, Fluent_35, Time2_1217, Fluent_1213, Time1_1218, Time2_1220, Fluent_1221, Time1_1215, Time1_1216]: (startedIn('#skF_4'(Time1_1216, '#skF_4'(Time1_1218, Time2_1217, Fluent_1213), Fluent_1214), Fluent_35, Time2_1217) | stoppedIn(Time1_1215, Fluent_35, '#skF_2'('#skF_4'(Time1_1218, Time2_1217, Fluent_1213), Fluent_1221, Time2_1220)) | ~less(Time1_1215, '#skF_4'(Time1_1218, Time2_1217, Fluent_1213)) | ~stoppedIn('#skF_4'(Time1_1218, Time2_1217, Fluent_1213), Fluent_1221, Time2_1220) | ~startedIn(Time1_1218, Fluent_1213, Time2_1217) | ~startedIn(Time1_1216, Fluent_1214, '#skF_4'(Time1_1218, Time2_1217, Fluent_1213)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1218, Time2_1217, Fluent_1213), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1218, Time2_1217, Fluent_1213))))).
% 7.33/2.74 tff(c_1114, plain, (![Fluent_1198, Time1_1197, Time2_1201, Fluent_35, Fluent_1202, Fluent_1200, Time1_1203, Time1_1199]: (startedIn('#skF_4'(Time1_1199, '#skF_4'(Time1_1197, Time2_1201, Fluent_1200), Fluent_1198), Fluent_35, Time2_1201) | stoppedIn('#skF_4'(Time1_1203, '#skF_4'(Time1_1197, Time2_1201, Fluent_1200), Fluent_1202), Fluent_35, Time2_1201) | ~startedIn(Time1_1203, Fluent_1202, '#skF_4'(Time1_1197, Time2_1201, Fluent_1200)) | ~startedIn(Time1_1197, Fluent_1200, Time2_1201) | ~startedIn(Time1_1199, Fluent_1198, '#skF_4'(Time1_1197, Time2_1201, Fluent_1200)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1197, Time2_1201, Fluent_1200), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1197, Time2_1201, Fluent_1200))))).
% 7.33/2.74 tff(c_1108, plain, (![Fluent_1182, Time1_1184, Fluent_35, Time1_1188, Fluent_1185, Fluent_1186, Time2_1187, Time1_1183]: (startedIn('#skF_2'(Time1_1183, Fluent_1182, '#skF_2'(Time1_1188, Fluent_1186, Time2_1187)), Fluent_35, Time2_1187) | stoppedIn('#skF_2'(Time1_1184, Fluent_1185, '#skF_2'(Time1_1188, Fluent_1186, Time2_1187)), Fluent_35, Time2_1187) | ~stoppedIn(Time1_1184, Fluent_1185, '#skF_2'(Time1_1188, Fluent_1186, Time2_1187)) | ~stoppedIn(Time1_1188, Fluent_1186, Time2_1187) | ~stoppedIn(Time1_1183, Fluent_1182, '#skF_2'(Time1_1188, Fluent_1186, Time2_1187)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1188, Fluent_1186, Time2_1187), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1188, Fluent_1186, Time2_1187))))).
% 7.33/2.74 tff(c_1102, plain, (![Time1_1166, Fluent_1171, Time2_1164, Fluent_35, Fluent_1163, Time2_1169, Fluent_1170, Time1_1165, Time1_1168]: (startedIn('#skF_4'(Time1_1165, '#skF_4'(Time1_1168, Time2_1164, Fluent_1170), Fluent_1163), Fluent_35, Time2_1164) | stoppedIn(Time1_1166, Fluent_35, '#skF_4'('#skF_4'(Time1_1168, Time2_1164, Fluent_1170), Time2_1169, Fluent_1171)) | ~less(Time1_1166, '#skF_4'(Time1_1168, Time2_1164, Fluent_1170)) | ~startedIn('#skF_4'(Time1_1168, Time2_1164, Fluent_1170), Fluent_1171, Time2_1169) | ~startedIn(Time1_1168, Fluent_1170, Time2_1164) | ~startedIn(Time1_1165, Fluent_1163, '#skF_4'(Time1_1168, Time2_1164, Fluent_1170)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1168, Time2_1164, Fluent_1170), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1168, Time2_1164, Fluent_1170))))).
% 7.33/2.74 tff(c_1096, plain, (![Time1_1151, Time2_1154, Fluent_1149, Fluent_35, Fluent_1147, Time1_1153, Time1_1150, Fluent_1148]: (startedIn('#skF_2'(Time1_1150, Fluent_1148, '#skF_4'(Time1_1153, Time2_1154, Fluent_1147)), Fluent_35, Time2_1154) | stoppedIn('#skF_2'(Time1_1151, Fluent_1149, '#skF_4'(Time1_1153, Time2_1154, Fluent_1147)), Fluent_35, Time2_1154) | ~stoppedIn(Time1_1151, Fluent_1149, '#skF_4'(Time1_1153, Time2_1154, Fluent_1147)) | ~startedIn(Time1_1153, Fluent_1147, Time2_1154) | ~stoppedIn(Time1_1150, Fluent_1148, '#skF_4'(Time1_1153, Time2_1154, Fluent_1147)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1153, Time2_1154, Fluent_1147), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1153, Time2_1154, Fluent_1147))))).
% 7.33/2.74 tff(c_1090, plain, (![Time1_1134, Time1_1131, Fluent_35, Time1_1137, Fluent_1138, Time2_1135, Fluent_1132, Fluent_1133]: (startedIn('#skF_2'(Time1_1134, Fluent_1133, '#skF_2'(Time1_1137, Fluent_1138, Time2_1135)), Fluent_35, Time2_1135) | stoppedIn('#skF_4'(Time1_1131, '#skF_2'(Time1_1137, Fluent_1138, Time2_1135), Fluent_1132), Fluent_35, Time2_1135) | ~startedIn(Time1_1131, Fluent_1132, '#skF_2'(Time1_1137, Fluent_1138, Time2_1135)) | ~stoppedIn(Time1_1137, Fluent_1138, Time2_1135) | ~stoppedIn(Time1_1134, Fluent_1133, '#skF_2'(Time1_1137, Fluent_1138, Time2_1135)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1137, Fluent_1138, Time2_1135), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1137, Fluent_1138, Time2_1135))))).
% 7.33/2.74 tff(c_1084, plain, (![Time2_1119, Time1_1117, Fluent_35, Time1_1115, Fluent_1116, Fluent_1118, Time1_1121, Fluent_1120]: (startedIn('#skF_2'(Time1_1117, Fluent_1116, '#skF_4'(Time1_1115, Time2_1119, Fluent_1118)), Fluent_35, Time2_1119) | stoppedIn('#skF_4'(Time1_1121, '#skF_4'(Time1_1115, Time2_1119, Fluent_1118), Fluent_1120), Fluent_35, Time2_1119) | ~startedIn(Time1_1121, Fluent_1120, '#skF_4'(Time1_1115, Time2_1119, Fluent_1118)) | ~startedIn(Time1_1115, Fluent_1118, Time2_1119) | ~stoppedIn(Time1_1117, Fluent_1116, '#skF_4'(Time1_1115, Time2_1119, Fluent_1118)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1115, Time2_1119, Fluent_1118), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1115, Time2_1119, Fluent_1118))))).
% 7.33/2.74 tff(c_1078, plain, (![Fluent_35, Time1_1101, Time1_1106, Fluent_1100, Time2_1105, Fluent_1104, Time1_1102, Fluent_1103]: (startedIn('#skF_4'(Time1_1102, '#skF_2'(Time1_1106, Fluent_1104, Time2_1105), Fluent_1100), Fluent_35, Time2_1105) | stoppedIn('#skF_2'(Time1_1101, Fluent_1103, '#skF_2'(Time1_1106, Fluent_1104, Time2_1105)), Fluent_35, Time2_1105) | ~stoppedIn(Time1_1101, Fluent_1103, '#skF_2'(Time1_1106, Fluent_1104, Time2_1105)) | ~stoppedIn(Time1_1106, Fluent_1104, Time2_1105) | ~startedIn(Time1_1102, Fluent_1100, '#skF_2'(Time1_1106, Fluent_1104, Time2_1105)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1106, Fluent_1104, Time2_1105), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1106, Fluent_1104, Time2_1105))))).
% 7.33/2.74 tff(c_1072, plain, (![Fluent_1087, Time1_1088, Fluent_1085, Fluent_35, Time1_1089, Time1_1084, Time2_1086, Fluent_1083, Time2_1081]: (startedIn(Time1_1084, Fluent_35, '#skF_2'('#skF_4'(Time1_1089, Time2_1081, Fluent_1085), Fluent_1083, Time2_1086)) | ~less(Time1_1084, '#skF_4'(Time1_1089, Time2_1081, Fluent_1085)) | stoppedIn('#skF_4'(Time1_1088, '#skF_4'(Time1_1089, Time2_1081, Fluent_1085), Fluent_1087), Fluent_35, Time2_1081) | ~startedIn(Time1_1089, Fluent_1085, Time2_1081) | ~startedIn(Time1_1088, Fluent_1087, '#skF_4'(Time1_1089, Time2_1081, Fluent_1085)) | ~stoppedIn('#skF_4'(Time1_1089, Time2_1081, Fluent_1085), Fluent_1083, Time2_1086) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1089, Time2_1081, Fluent_1085), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1089, Time2_1081, Fluent_1085))))).
% 7.33/2.74 tff(c_1066, plain, (![Time1_1071, Time1_1066, Fluent_35, Time1_1069, Fluent_1067, Fluent_1072, Fluent_1065, Time2_1068]: (startedIn('#skF_4'(Time1_1069, '#skF_2'(Time1_1071, Fluent_1072, Time2_1068), Fluent_1065), Fluent_35, Time2_1068) | stoppedIn('#skF_4'(Time1_1066, '#skF_2'(Time1_1071, Fluent_1072, Time2_1068), Fluent_1067), Fluent_35, Time2_1068) | ~startedIn(Time1_1066, Fluent_1067, '#skF_2'(Time1_1071, Fluent_1072, Time2_1068)) | ~stoppedIn(Time1_1071, Fluent_1072, Time2_1068) | ~startedIn(Time1_1069, Fluent_1065, '#skF_2'(Time1_1071, Fluent_1072, Time2_1068)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1071, Fluent_1072, Time2_1068), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1071, Fluent_1072, Time2_1068))))).
% 7.33/2.74 tff(c_1060, plain, (![Fluent_35, Fluent_1051, Fluent_1049, Time2_1056, Time1_1052, Fluent_1050, Time1_1055, Time1_1053]: (startedIn('#skF_4'(Time1_1053, '#skF_4'(Time1_1055, Time2_1056, Fluent_1050), Fluent_1049), Fluent_35, Time2_1056) | stoppedIn('#skF_2'(Time1_1052, Fluent_1051, '#skF_4'(Time1_1055, Time2_1056, Fluent_1050)), Fluent_35, Time2_1056) | ~stoppedIn(Time1_1052, Fluent_1051, '#skF_4'(Time1_1055, Time2_1056, Fluent_1050)) | ~startedIn(Time1_1055, Fluent_1050, Time2_1056) | ~startedIn(Time1_1053, Fluent_1049, '#skF_4'(Time1_1055, Time2_1056, Fluent_1050)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_1055, Time2_1056, Fluent_1050), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_1055, Time2_1056, Fluent_1050))))).
% 7.33/2.74 tff(c_1054, plain, (![Time1_1036, Fluent_35, Fluent_1041, Time2_1038, Fluent_1035, Time1_1039, Time2_1040]: (startedIn(Time1_1036, Fluent_35, Time2_1038) | stoppedIn(Time1_1039, Fluent_35, '#skF_2'('#skF_2'(Time1_1036, Fluent_1035, Time2_1038), Fluent_1041, Time2_1040)) | ~less(Time1_1039, '#skF_2'(Time1_1036, Fluent_1035, Time2_1038)) | ~stoppedIn('#skF_2'(Time1_1036, Fluent_1035, Time2_1038), Fluent_1041, Time2_1040) | ~stoppedIn(Time1_1036, Fluent_1035, Time2_1038) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1036, Fluent_1035, Time2_1038), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1036, Fluent_1035, Time2_1038))))).
% 7.33/2.75 tff(c_371, plain, (![Time2_346, Fluent_347, Time2_3, Time1_352, Time1_348, Time1_1, Fluent_350, Fluent_2]: (startedIn(Time1_348, Fluent_347, Time2_3) | ~less(Time1_348, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | stoppedIn(Time1_352, Fluent_347, '#skF_2'('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_350, Time2_346)) | ~less(Time1_352, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_7'(Fluent_347, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_347, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_347, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_350, Time2_346) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.75 tff(c_1036, plain, (![Time1_1015, Fluent_1016, Fluent_1018, Time2_1014, Fluent_35, Time2_1019, Time1_1017]: (startedIn(Time1_1017, Fluent_35, Time2_1019) | stoppedIn(Time1_1015, Fluent_35, '#skF_4'('#skF_2'(Time1_1017, Fluent_1016, Time2_1019), Time2_1014, Fluent_1018)) | ~less(Time1_1015, '#skF_2'(Time1_1017, Fluent_1016, Time2_1019)) | ~startedIn('#skF_2'(Time1_1017, Fluent_1016, Time2_1019), Fluent_1018, Time2_1014) | ~stoppedIn(Time1_1017, Fluent_1016, Time2_1019) | releasedAt(Fluent_35, plus('#skF_2'(Time1_1017, Fluent_1016, Time2_1019), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_1017, Fluent_1016, Time2_1019))))).
% 7.33/2.75 tff(c_358, plain, (![Fluent_341, Time1_342, Time2_339, Time2_3, Time1_1, Time1_344, Fluent_2, Fluent_340]: (startedIn(Time1_342, Fluent_340, Time2_3) | ~less(Time1_342, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | stoppedIn(Time1_344, Fluent_340, '#skF_4'('#skF_2'(Time1_1, Fluent_2, Time2_3), Time2_339, Fluent_341)) | ~less(Time1_344, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_7'(Fluent_340, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_340, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_340, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~startedIn('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_341, Time2_339) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.75 tff(c_1018, plain, (![Fluent_35, Time2_993, Time1_992, Time2_996, Time1_994, Fluent_991, Fluent_997]: (startedIn(Time1_992, Fluent_35, Time2_993) | stoppedIn(Time1_994, Fluent_35, '#skF_4'('#skF_4'(Time1_992, Time2_993, Fluent_991), Time2_996, Fluent_997)) | ~less(Time1_994, '#skF_4'(Time1_992, Time2_993, Fluent_991)) | ~startedIn('#skF_4'(Time1_992, Time2_993, Fluent_991), Fluent_997, Time2_996) | ~startedIn(Time1_992, Fluent_991, Time2_993) | releasedAt(Fluent_35, plus('#skF_4'(Time1_992, Time2_993, Fluent_991), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_992, Time2_993, Fluent_991))))).
% 7.33/2.75 tff(c_360, plain, (![Fluent_341, Fluent_12, Time1_342, Time2_339, Time2_11, Time1_344, Time1_10, Fluent_340]: (startedIn(Time1_342, Fluent_340, Time2_11) | ~less(Time1_342, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | stoppedIn(Time1_344, Fluent_340, '#skF_4'('#skF_4'(Time1_10, Time2_11, Fluent_12), Time2_339, Fluent_341)) | ~less(Time1_344, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_7'(Fluent_340, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_340, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_340, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_341, Time2_339) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.75 tff(c_1000, plain, (![Time2_975, Fluent_973, Fluent_35, Time1_974, Time1_971, Fluent_972]: (startedIn(Time1_974, Fluent_35, Time2_975) | stoppedIn('#skF_4'(Time1_971, '#skF_2'(Time1_974, Fluent_973, Time2_975), Fluent_972), Fluent_35, Time2_975) | ~startedIn(Time1_971, Fluent_972, '#skF_2'(Time1_974, Fluent_973, Time2_975)) | ~stoppedIn(Time1_974, Fluent_973, Time2_975) | releasedAt(Fluent_35, plus('#skF_2'(Time1_974, Fluent_973, Time2_975), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_974, Fluent_973, Time2_975))))).
% 7.33/2.75 tff(c_963, plain, (![Time1_944, Time1_940, Time2_3, Fluent_938, Time1_1, Fluent_939, Fluent_2]: (startedIn(Time1_940, Fluent_938, Time2_3) | ~less(Time1_940, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | stoppedIn('#skF_4'(Time1_944, '#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_939), Fluent_938, Time2_3) | ~happens('#skF_7'(Fluent_938, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_938, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_938, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~startedIn(Time1_944, Fluent_939, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.75 tff(c_982, plain, (![Time1_955, Fluent_35, Fluent_952, Time1_954, Fluent_953, Time2_956]: (startedIn(Time1_955, Fluent_35, Time2_956) | stoppedIn('#skF_2'(Time1_954, Fluent_953, '#skF_4'(Time1_955, Time2_956, Fluent_952)), Fluent_35, Time2_956) | ~stoppedIn(Time1_954, Fluent_953, '#skF_4'(Time1_955, Time2_956, Fluent_952)) | ~startedIn(Time1_955, Fluent_952, Time2_956) | releasedAt(Fluent_35, plus('#skF_4'(Time1_955, Time2_956, Fluent_952), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_955, Time2_956, Fluent_952))))).
% 7.33/2.75 tff(c_952, plain, (![Fluent_929, Time1_936, Fluent_12, Time1_932, Time2_11, Fluent_935, Time1_10]: (startedIn(Time1_932, Fluent_935, Time2_11) | ~less(Time1_932, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | stoppedIn('#skF_2'(Time1_936, Fluent_929, '#skF_4'(Time1_10, Time2_11, Fluent_12)), Fluent_935, Time2_11) | ~happens('#skF_7'(Fluent_935, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_935, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_935, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~stoppedIn(Time1_936, Fluent_929, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.75 tff(c_789, plain, (![Fluent_740, Fluent_739, Time2_742, Time2_11, Time1_743, Time1_10, Time1_741, Fluent_744]: (startedIn(Time1_10, Fluent_740, Time2_11) | ~less('#skF_2'(Time1_743, Fluent_744, Time2_742), Time2_11) | ~less(Time1_10, '#skF_2'(Time1_743, Fluent_744, Time2_742)) | stoppedIn('#skF_4'(Time1_741, '#skF_2'(Time1_743, Fluent_744, Time2_742), Fluent_739), Fluent_740, Time2_742) | ~happens('#skF_7'(Fluent_740, '#skF_2'(Time1_743, Fluent_744, Time2_742)), '#skF_2'(Time1_743, Fluent_744, Time2_742)) | releasedAt(Fluent_740, plus('#skF_2'(Time1_743, Fluent_744, Time2_742), n1)) | ~releasedAt(Fluent_740, '#skF_2'(Time1_743, Fluent_744, Time2_742)) | ~stoppedIn(Time1_743, Fluent_744, Time2_742) | ~startedIn(Time1_741, Fluent_739, '#skF_2'(Time1_743, Fluent_744, Time2_742))))).
% 7.33/2.75 tff(c_833, plain, (![Time2_810, Time1_809, Time1_807, Time2_11, Fluent_808, Fluent_805, Time1_10, Fluent_806]: (startedIn(Time1_10, Fluent_808, Time2_11) | ~less('#skF_4'(Time1_809, Time2_810, Fluent_805), Time2_11) | ~less(Time1_10, '#skF_4'(Time1_809, Time2_810, Fluent_805)) | stoppedIn('#skF_2'(Time1_807, Fluent_806, '#skF_4'(Time1_809, Time2_810, Fluent_805)), Fluent_808, Time2_810) | ~happens('#skF_7'(Fluent_808, '#skF_4'(Time1_809, Time2_810, Fluent_805)), '#skF_4'(Time1_809, Time2_810, Fluent_805)) | releasedAt(Fluent_808, plus('#skF_4'(Time1_809, Time2_810, Fluent_805), n1)) | ~releasedAt(Fluent_808, '#skF_4'(Time1_809, Time2_810, Fluent_805)) | ~startedIn(Time1_809, Fluent_805, Time2_810) | ~stoppedIn(Time1_807, Fluent_806, '#skF_4'(Time1_809, Time2_810, Fluent_805))))).
% 7.33/2.75 tff(c_940, plain, (![Time1_917, Fluent_35, Fluent_915, Fluent_921, Time2_920, Time1_916, Time2_918]: (startedIn(Time1_917, Fluent_35, Time2_918) | stoppedIn(Time1_916, Fluent_35, '#skF_2'('#skF_4'(Time1_917, Time2_918, Fluent_915), Fluent_921, Time2_920)) | ~less(Time1_916, '#skF_4'(Time1_917, Time2_918, Fluent_915)) | ~stoppedIn('#skF_4'(Time1_917, Time2_918, Fluent_915), Fluent_921, Time2_920) | ~startedIn(Time1_917, Fluent_915, Time2_918) | releasedAt(Fluent_35, plus('#skF_4'(Time1_917, Time2_918, Fluent_915), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_917, Time2_918, Fluent_915))))).
% 7.33/2.75 tff(c_373, plain, (![Time2_346, Fluent_347, Fluent_12, Time1_352, Time1_348, Time2_11, Fluent_350, Time1_10]: (startedIn(Time1_348, Fluent_347, Time2_11) | ~less(Time1_348, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | stoppedIn(Time1_352, Fluent_347, '#skF_2'('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_350, Time2_346)) | ~less(Time1_352, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_7'(Fluent_347, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_347, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_347, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~stoppedIn('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_350, Time2_346) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.75 tff(c_922, plain, (![Fluent_35, Fluent_898, Fluent_895, Time1_896, Time2_897, Time1_899]: (startedIn(Time1_896, Fluent_35, Time2_897) | stoppedIn('#skF_4'(Time1_899, '#skF_4'(Time1_896, Time2_897, Fluent_895), Fluent_898), Fluent_35, Time2_897) | ~startedIn(Time1_899, Fluent_898, '#skF_4'(Time1_896, Time2_897, Fluent_895)) | ~startedIn(Time1_896, Fluent_895, Time2_897) | releasedAt(Fluent_35, plus('#skF_4'(Time1_896, Time2_897, Fluent_895), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_896, Time2_897, Fluent_895))))).
% 7.33/2.75 tff(c_898, plain, (![Fluent_868, Fluent_12, Time1_870, Fluent_873, Time1_872, Time2_11, Time1_10]: (startedIn(Time1_870, Fluent_873, Time2_11) | ~less(Time1_870, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | stoppedIn('#skF_4'(Time1_872, '#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_868), Fluent_873, Time2_11) | ~happens('#skF_7'(Fluent_873, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_873, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_873, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_872, Fluent_868, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.75 tff(c_904, plain, (![Time1_879, Fluent_35, Fluent_877, Fluent_880, Time1_878, Time2_881]: (startedIn(Time1_878, Fluent_35, Time2_881) | stoppedIn('#skF_2'(Time1_879, Fluent_880, '#skF_2'(Time1_878, Fluent_877, Time2_881)), Fluent_35, Time2_881) | ~stoppedIn(Time1_879, Fluent_880, '#skF_2'(Time1_878, Fluent_877, Time2_881)) | ~stoppedIn(Time1_878, Fluent_877, Time2_881) | releasedAt(Fluent_35, plus('#skF_2'(Time1_878, Fluent_877, Time2_881), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_878, Fluent_877, Time2_881))))).
% 7.33/2.75 tff(c_855, plain, (![Time2_840, Fluent_836, Time1_837, Fluent_835, Time2_11, Time1_839, Time1_10, Fluent_838]: (startedIn(Time1_10, Fluent_838, Time2_11) | ~less('#skF_4'(Time1_839, Time2_840, Fluent_836), Time2_11) | ~less(Time1_10, '#skF_4'(Time1_839, Time2_840, Fluent_836)) | stoppedIn('#skF_4'(Time1_837, '#skF_4'(Time1_839, Time2_840, Fluent_836), Fluent_835), Fluent_838, Time2_840) | ~happens('#skF_7'(Fluent_838, '#skF_4'(Time1_839, Time2_840, Fluent_836)), '#skF_4'(Time1_839, Time2_840, Fluent_836)) | releasedAt(Fluent_838, plus('#skF_4'(Time1_839, Time2_840, Fluent_836), n1)) | ~releasedAt(Fluent_838, '#skF_4'(Time1_839, Time2_840, Fluent_836)) | ~startedIn(Time1_839, Fluent_836, Time2_840) | ~startedIn(Time1_837, Fluent_835, '#skF_4'(Time1_839, Time2_840, Fluent_836))))).
% 7.33/2.75 tff(c_873, plain, (![Time1_858, Fluent_857, Time1_854, Time2_3, Time1_1, Fluent_856, Fluent_2]: (startedIn(Time1_854, Fluent_856, Time2_3) | ~less(Time1_854, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | stoppedIn('#skF_2'(Time1_858, Fluent_857, '#skF_2'(Time1_1, Fluent_2, Time2_3)), Fluent_856, Time2_3) | ~happens('#skF_7'(Fluent_856, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_856, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_856, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_858, Fluent_857, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.75 tff(c_823, plain, (![Fluent_800, Time2_802, Fluent_804, Time1_803, Time2_11, Time1_10, Fluent_799, Time1_801]: (startedIn(Time1_10, Fluent_799, Time2_11) | ~less('#skF_2'(Time1_803, Fluent_804, Time2_802), Time2_11) | ~less(Time1_10, '#skF_2'(Time1_803, Fluent_804, Time2_802)) | stoppedIn('#skF_2'(Time1_801, Fluent_800, '#skF_2'(Time1_803, Fluent_804, Time2_802)), Fluent_799, Time2_802) | ~happens('#skF_7'(Fluent_799, '#skF_2'(Time1_803, Fluent_804, Time2_802)), '#skF_2'(Time1_803, Fluent_804, Time2_802)) | releasedAt(Fluent_799, plus('#skF_2'(Time1_803, Fluent_804, Time2_802), n1)) | ~releasedAt(Fluent_799, '#skF_2'(Time1_803, Fluent_804, Time2_802)) | ~stoppedIn(Time1_803, Fluent_804, Time2_802) | ~stoppedIn(Time1_801, Fluent_800, '#skF_2'(Time1_803, Fluent_804, Time2_802))))).
% 7.33/2.75 tff(c_862, plain, (![Time1_843, Fluent_35, Fluent_842, Time2_846, Time1_845, Fluent_841]: (holdsAt(Fluent_35, plus('#skF_4'(Time1_845, Time2_846, Fluent_842), n1)) | stoppedIn('#skF_4'(Time1_843, '#skF_4'(Time1_845, Time2_846, Fluent_842), Fluent_841), Fluent_35, Time2_846) | ~startedIn(Time1_845, Fluent_842, Time2_846) | ~startedIn(Time1_843, Fluent_841, '#skF_4'(Time1_845, Time2_846, Fluent_842)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_845, Time2_846, Fluent_842), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_845, Time2_846, Fluent_842))))).
% 7.33/2.75 tff(c_560, plain, (![Time2_512, Time1_511, Fluent_510, Fluent_12, Fluent_509, Time1_10]: (stoppedIn('#skF_4'(Time1_10, '#skF_4'(Time1_511, Time2_512, Fluent_510), Fluent_12), Fluent_509, Time2_512) | ~happens('#skF_7'(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)), '#skF_4'(Time1_511, Time2_512, Fluent_510)) | initiates('#skF_7'(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)), Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)) | releasedAt(Fluent_509, plus('#skF_4'(Time1_511, Time2_512, Fluent_510), n1)) | ~releasedAt(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)) | ~startedIn(Time1_511, Fluent_510, Time2_512) | ~startedIn(Time1_10, Fluent_12, '#skF_4'(Time1_511, Time2_512, Fluent_510))))).
% 7.33/2.75 tff(c_846, plain, (![Fluent_35, Time2_825, Fluent_824, Time1_826, Time1_828, Fluent_823]: (holdsAt(Fluent_35, plus('#skF_4'(Time1_826, Time2_825, Fluent_824), n1)) | stoppedIn('#skF_2'(Time1_828, Fluent_823, '#skF_4'(Time1_826, Time2_825, Fluent_824)), Fluent_35, Time2_825) | ~startedIn(Time1_826, Fluent_824, Time2_825) | ~stoppedIn(Time1_828, Fluent_823, '#skF_4'(Time1_826, Time2_825, Fluent_824)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_826, Time2_825, Fluent_824), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_826, Time2_825, Fluent_824))))).
% 7.33/2.75 tff(c_840, plain, (![Time1_811, Time2_815, Fluent_35, Time1_814, Fluent_813, Fluent_816]: (holdsAt(Fluent_35, plus('#skF_2'(Time1_811, Fluent_816, Time2_815), n1)) | stoppedIn('#skF_2'(Time1_814, Fluent_813, '#skF_2'(Time1_811, Fluent_816, Time2_815)), Fluent_35, Time2_815) | ~stoppedIn(Time1_811, Fluent_816, Time2_815) | ~stoppedIn(Time1_814, Fluent_813, '#skF_2'(Time1_811, Fluent_816, Time2_815)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_811, Fluent_816, Time2_815), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_811, Fluent_816, Time2_815))))).
% 7.33/2.75 tff(c_559, plain, (![Time2_512, Time1_511, Fluent_510, Time1_1, Fluent_509, Fluent_2]: (stoppedIn('#skF_2'(Time1_1, Fluent_2, '#skF_4'(Time1_511, Time2_512, Fluent_510)), Fluent_509, Time2_512) | ~happens('#skF_7'(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)), '#skF_4'(Time1_511, Time2_512, Fluent_510)) | initiates('#skF_7'(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)), Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)) | releasedAt(Fluent_509, plus('#skF_4'(Time1_511, Time2_512, Fluent_510), n1)) | ~releasedAt(Fluent_509, '#skF_4'(Time1_511, Time2_512, Fluent_510)) | ~startedIn(Time1_511, Fluent_510, Time2_512) | ~stoppedIn(Time1_1, Fluent_2, '#skF_4'(Time1_511, Time2_512, Fluent_510))))).
% 7.33/2.75 tff(c_581, plain, (![Fluent_519, Time1_520, Fluent_518, Time1_1, Time2_521, Fluent_2]: (stoppedIn('#skF_2'(Time1_1, Fluent_2, '#skF_2'(Time1_520, Fluent_519, Time2_521)), Fluent_518, Time2_521) | ~happens('#skF_7'(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)), '#skF_2'(Time1_520, Fluent_519, Time2_521)) | initiates('#skF_7'(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)), Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)) | releasedAt(Fluent_518, plus('#skF_2'(Time1_520, Fluent_519, Time2_521), n1)) | ~releasedAt(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)) | ~stoppedIn(Time1_520, Fluent_519, Time2_521) | ~stoppedIn(Time1_1, Fluent_2, '#skF_2'(Time1_520, Fluent_519, Time2_521))))).
% 7.33/2.75 tff(c_814, plain, (![Fluent_789, Fluent_35, Time1_786, Time2_788, Time2_790, Fluent_787, Time1_785]: (startedIn(Time1_786, Fluent_35, '#skF_4'('#skF_4'(Time1_785, Time2_788, Fluent_789), Time2_790, Fluent_787)) | ~less(Time1_786, '#skF_4'(Time1_785, Time2_788, Fluent_789)) | stoppedIn(Time1_785, Fluent_35, Time2_788) | ~startedIn(Time1_785, Fluent_789, Time2_788) | ~startedIn('#skF_4'(Time1_785, Time2_788, Fluent_789), Fluent_787, Time2_790) | releasedAt(Fluent_35, plus('#skF_4'(Time1_785, Time2_788, Fluent_789), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_785, Time2_788, Fluent_789))))).
% 7.33/2.75 tff(c_808, plain, (![Time2_776, Fluent_35, Fluent_772, Time1_775, Time2_774, Fluent_777, Time1_773]: (startedIn(Time1_773, Fluent_35, '#skF_2'('#skF_2'(Time1_775, Fluent_777, Time2_776), Fluent_772, Time2_774)) | ~less(Time1_773, '#skF_2'(Time1_775, Fluent_777, Time2_776)) | stoppedIn(Time1_775, Fluent_35, Time2_776) | ~stoppedIn(Time1_775, Fluent_777, Time2_776) | ~stoppedIn('#skF_2'(Time1_775, Fluent_777, Time2_776), Fluent_772, Time2_774) | releasedAt(Fluent_35, plus('#skF_2'(Time1_775, Fluent_777, Time2_776), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_775, Fluent_777, Time2_776))))).
% 7.33/2.75 tff(c_802, plain, (![Fluent_35, Time1_757, Time2_760, Time1_758, Fluent_761, Fluent_759, Time2_762]: (startedIn(Time1_758, Fluent_35, '#skF_2'('#skF_4'(Time1_757, Time2_760, Fluent_761), Fluent_759, Time2_762)) | ~less(Time1_758, '#skF_4'(Time1_757, Time2_760, Fluent_761)) | stoppedIn(Time1_757, Fluent_35, Time2_760) | ~startedIn(Time1_757, Fluent_761, Time2_760) | ~stoppedIn('#skF_4'(Time1_757, Time2_760, Fluent_761), Fluent_759, Time2_762) | releasedAt(Fluent_35, plus('#skF_4'(Time1_757, Time2_760, Fluent_761), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_757, Time2_760, Fluent_761))))).
% 7.33/2.75 tff(c_796, plain, (![Time1_745, Time1_750, Time2_749, Fluent_35, Fluent_747, Fluent_748]: (holdsAt(Fluent_35, plus('#skF_2'(Time1_745, Fluent_748, Time2_749), n1)) | stoppedIn('#skF_4'(Time1_750, '#skF_2'(Time1_745, Fluent_748, Time2_749), Fluent_747), Fluent_35, Time2_749) | ~stoppedIn(Time1_745, Fluent_748, Time2_749) | ~startedIn(Time1_750, Fluent_747, '#skF_2'(Time1_745, Fluent_748, Time2_749)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_745, Fluent_748, Time2_749), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_745, Fluent_748, Time2_749))))).
% 7.33/2.75 tff(c_583, plain, (![Fluent_519, Time1_520, Fluent_12, Fluent_518, Time2_521, Time1_10]: (stoppedIn('#skF_4'(Time1_10, '#skF_2'(Time1_520, Fluent_519, Time2_521), Fluent_12), Fluent_518, Time2_521) | ~happens('#skF_7'(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)), '#skF_2'(Time1_520, Fluent_519, Time2_521)) | initiates('#skF_7'(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)), Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)) | releasedAt(Fluent_518, plus('#skF_2'(Time1_520, Fluent_519, Time2_521), n1)) | ~releasedAt(Fluent_518, '#skF_2'(Time1_520, Fluent_519, Time2_521)) | ~stoppedIn(Time1_520, Fluent_519, Time2_521) | ~startedIn(Time1_10, Fluent_12, '#skF_2'(Time1_520, Fluent_519, Time2_521))))).
% 7.33/2.75 tff(c_780, plain, (![Fluent_35, Time2_730, Time1_729, Fluent_731, Time2_728, Time1_727, Fluent_726]: (startedIn(Time1_727, Fluent_35, '#skF_4'('#skF_2'(Time1_729, Fluent_731, Time2_730), Time2_728, Fluent_726)) | ~less(Time1_727, '#skF_2'(Time1_729, Fluent_731, Time2_730)) | stoppedIn(Time1_729, Fluent_35, Time2_730) | ~stoppedIn(Time1_729, Fluent_731, Time2_730) | ~startedIn('#skF_2'(Time1_729, Fluent_731, Time2_730), Fluent_726, Time2_728) | releasedAt(Fluent_35, plus('#skF_2'(Time1_729, Fluent_731, Time2_730), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_729, Fluent_731, Time2_730))))).
% 7.33/2.75 tff(c_774, plain, (![Time2_715, Fluent_713, Fluent_717, Time1_714, Time1_716, Fluent_29]: (stoppedIn('#skF_4'(Time1_716, '#skF_4'(Time1_714, Time2_715, Fluent_717), Fluent_713), Fluent_29, Time2_715) | ~startedIn(Time1_714, Fluent_717, Time2_715) | ~startedIn(Time1_716, Fluent_713, '#skF_4'(Time1_714, Time2_715, Fluent_717)) | holdsAt(Fluent_29, plus('#skF_4'(Time1_714, Time2_715, Fluent_717), n1)) | releasedAt(Fluent_29, plus('#skF_4'(Time1_714, Time2_715, Fluent_717), n1)) | ~holdsAt(Fluent_29, '#skF_4'(Time1_714, Time2_715, Fluent_717))))).
% 7.33/2.75 tff(c_768, plain, (![Fluent_703, Time1_702, Time1_704, Fluent_701, Fluent_32, Time2_705]: (startedIn('#skF_4'(Time1_702, '#skF_4'(Time1_704, Time2_705, Fluent_703), Fluent_701), Fluent_32, Time2_705) | ~startedIn(Time1_704, Fluent_703, Time2_705) | ~startedIn(Time1_702, Fluent_701, '#skF_4'(Time1_704, Time2_705, Fluent_703)) | ~holdsAt(Fluent_32, plus('#skF_4'(Time1_704, Time2_705, Fluent_703), n1)) | releasedAt(Fluent_32, plus('#skF_4'(Time1_704, Time2_705, Fluent_703), n1)) | holdsAt(Fluent_32, '#skF_4'(Time1_704, Time2_705, Fluent_703))))).
% 7.33/2.75 tff(c_759, plain, (![Time1_689, Time2_692, Time1_691, Fluent_32, Fluent_690, Fluent_694]: (startedIn('#skF_2'(Time1_691, Fluent_690, '#skF_2'(Time1_689, Fluent_694, Time2_692)), Fluent_32, Time2_692) | ~stoppedIn(Time1_689, Fluent_694, Time2_692) | ~stoppedIn(Time1_691, Fluent_690, '#skF_2'(Time1_689, Fluent_694, Time2_692)) | ~holdsAt(Fluent_32, plus('#skF_2'(Time1_689, Fluent_694, Time2_692), n1)) | releasedAt(Fluent_32, plus('#skF_2'(Time1_689, Fluent_694, Time2_692), n1)) | holdsAt(Fluent_32, '#skF_2'(Time1_689, Fluent_694, Time2_692))))).
% 7.33/2.75 tff(c_753, plain, (![Time1_678, Fluent_677, Time1_681, Time2_679, Fluent_29, Fluent_680]: (stoppedIn('#skF_4'(Time1_678, '#skF_2'(Time1_681, Fluent_680, Time2_679), Fluent_677), Fluent_29, Time2_679) | ~stoppedIn(Time1_681, Fluent_680, Time2_679) | ~startedIn(Time1_678, Fluent_677, '#skF_2'(Time1_681, Fluent_680, Time2_679)) | holdsAt(Fluent_29, plus('#skF_2'(Time1_681, Fluent_680, Time2_679), n1)) | releasedAt(Fluent_29, plus('#skF_2'(Time1_681, Fluent_680, Time2_679), n1)) | ~holdsAt(Fluent_29, '#skF_2'(Time1_681, Fluent_680, Time2_679))))).
% 7.33/2.75 tff(c_747, plain, (![Time2_667, Time1_669, Fluent_668, Fluent_665, Fluent_29, Time1_666]: (stoppedIn('#skF_2'(Time1_666, Fluent_665, '#skF_2'(Time1_669, Fluent_668, Time2_667)), Fluent_29, Time2_667) | ~stoppedIn(Time1_669, Fluent_668, Time2_667) | ~stoppedIn(Time1_666, Fluent_665, '#skF_2'(Time1_669, Fluent_668, Time2_667)) | holdsAt(Fluent_29, plus('#skF_2'(Time1_669, Fluent_668, Time2_667), n1)) | releasedAt(Fluent_29, plus('#skF_2'(Time1_669, Fluent_668, Time2_667), n1)) | ~holdsAt(Fluent_29, '#skF_2'(Time1_669, Fluent_668, Time2_667))))).
% 7.33/2.75 tff(c_741, plain, (![Fluent_655, Time2_657, Time1_654, Fluent_653, Fluent_32, Time1_656]: (startedIn('#skF_2'(Time1_654, Fluent_653, '#skF_4'(Time1_656, Time2_657, Fluent_655)), Fluent_32, Time2_657) | ~startedIn(Time1_656, Fluent_655, Time2_657) | ~stoppedIn(Time1_654, Fluent_653, '#skF_4'(Time1_656, Time2_657, Fluent_655)) | ~holdsAt(Fluent_32, plus('#skF_4'(Time1_656, Time2_657, Fluent_655), n1)) | releasedAt(Fluent_32, plus('#skF_4'(Time1_656, Time2_657, Fluent_655), n1)) | holdsAt(Fluent_32, '#skF_4'(Time1_656, Time2_657, Fluent_655))))).
% 7.33/2.75 tff(c_732, plain, (![Time2_646, Time1_645, Fluent_35, Time1_643, Fluent_642, Fluent_641]: (startedIn('#skF_4'(Time1_643, '#skF_2'(Time1_645, Fluent_641, Time2_646), Fluent_642), Fluent_35, Time2_646) | stoppedIn(Time1_645, Fluent_35, Time2_646) | ~stoppedIn(Time1_645, Fluent_641, Time2_646) | ~startedIn(Time1_643, Fluent_642, '#skF_2'(Time1_645, Fluent_641, Time2_646)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_645, Fluent_641, Time2_646), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_645, Fluent_641, Time2_646))))).
% 7.33/2.75 tff(c_726, plain, (![Fluent_35, Time2_634, Time1_633, Time1_631, Fluent_629, Fluent_630]: (startedIn('#skF_2'(Time1_631, Fluent_630, '#skF_2'(Time1_633, Fluent_629, Time2_634)), Fluent_35, Time2_634) | stoppedIn(Time1_633, Fluent_35, Time2_634) | ~stoppedIn(Time1_633, Fluent_629, Time2_634) | ~stoppedIn(Time1_631, Fluent_630, '#skF_2'(Time1_633, Fluent_629, Time2_634)) | releasedAt(Fluent_35, plus('#skF_2'(Time1_633, Fluent_629, Time2_634), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_633, Fluent_629, Time2_634))))).
% 7.33/2.76 tff(c_720, plain, (![Time2_620, Time1_618, Time1_619, Fluent_617, Fluent_29, Fluent_621]: (stoppedIn('#skF_2'(Time1_619, Fluent_617, '#skF_4'(Time1_618, Time2_620, Fluent_621)), Fluent_29, Time2_620) | ~startedIn(Time1_618, Fluent_621, Time2_620) | ~stoppedIn(Time1_619, Fluent_617, '#skF_4'(Time1_618, Time2_620, Fluent_621)) | holdsAt(Fluent_29, plus('#skF_4'(Time1_618, Time2_620, Fluent_621), n1)) | releasedAt(Fluent_29, plus('#skF_4'(Time1_618, Time2_620, Fluent_621), n1)) | ~holdsAt(Fluent_29, '#skF_4'(Time1_618, Time2_620, Fluent_621))))).
% 7.33/2.76 tff(c_714, plain, (![Fluent_35, Time1_607, Time1_610, Time2_605, Fluent_606, Fluent_609]: (startedIn('#skF_2'(Time1_607, Fluent_606, '#skF_4'(Time1_610, Time2_605, Fluent_609)), Fluent_35, Time2_605) | stoppedIn(Time1_610, Fluent_35, Time2_605) | ~startedIn(Time1_610, Fluent_609, Time2_605) | ~stoppedIn(Time1_607, Fluent_606, '#skF_4'(Time1_610, Time2_605, Fluent_609)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_610, Time2_605, Fluent_609), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_610, Time2_605, Fluent_609))))).
% 7.33/2.76 tff(c_708, plain, (![Fluent_35, Time1_595, Time2_594, Fluent_593, Fluent_597, Time1_598]: (startedIn('#skF_4'(Time1_595, '#skF_4'(Time1_598, Time2_594, Fluent_597), Fluent_593), Fluent_35, Time2_594) | stoppedIn(Time1_598, Fluent_35, Time2_594) | ~startedIn(Time1_598, Fluent_597, Time2_594) | ~startedIn(Time1_595, Fluent_593, '#skF_4'(Time1_598, Time2_594, Fluent_597)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_598, Time2_594, Fluent_597), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_598, Time2_594, Fluent_597))))).
% 7.33/2.76 tff(c_695, plain, (![Time1_585, Fluent_35, Time2_587, Fluent_588]: (startedIn(Time1_585, Fluent_35, Time2_587) | stoppedIn(Time1_585, Fluent_35, Time2_587) | ~startedIn(Time1_585, Fluent_588, Time2_587) | releasedAt(Fluent_35, plus('#skF_4'(Time1_585, Time2_587, Fluent_588), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_585, Time2_587, Fluent_588))))).
% 7.33/2.76 tff(c_676, plain, (![Time1_574, Fluent_12, Time2_11, Fluent_576, Time1_10]: (startedIn(Time1_574, Fluent_576, Time2_11) | ~less(Time1_574, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | stoppedIn(Time1_10, Fluent_576, Time2_11) | ~happens('#skF_7'(Fluent_576, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_576, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_576, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_569, plain, (![Time2_516, Time1_514, Fluent_515, Time2_11, Time1_10, Fluent_517]: (startedIn(Time1_10, Fluent_515, Time2_11) | ~less('#skF_4'(Time1_514, Time2_516, Fluent_517), Time2_11) | ~less(Time1_10, '#skF_4'(Time1_514, Time2_516, Fluent_517)) | stoppedIn(Time1_514, Fluent_515, Time2_516) | ~happens('#skF_7'(Fluent_515, '#skF_4'(Time1_514, Time2_516, Fluent_517)), '#skF_4'(Time1_514, Time2_516, Fluent_517)) | releasedAt(Fluent_515, plus('#skF_4'(Time1_514, Time2_516, Fluent_517), n1)) | ~releasedAt(Fluent_515, '#skF_4'(Time1_514, Time2_516, Fluent_517)) | ~startedIn(Time1_514, Fluent_517, Time2_516)))).
% 7.33/2.76 tff(c_664, plain, (![Fluent_567, Time1_562, Fluent_32, Fluent_563, Time2_564, Time1_565]: (startedIn('#skF_4'(Time1_565, '#skF_2'(Time1_562, Fluent_567, Time2_564), Fluent_563), Fluent_32, Time2_564) | ~stoppedIn(Time1_562, Fluent_567, Time2_564) | ~startedIn(Time1_565, Fluent_563, '#skF_2'(Time1_562, Fluent_567, Time2_564)) | ~holdsAt(Fluent_32, plus('#skF_2'(Time1_562, Fluent_567, Time2_564), n1)) | releasedAt(Fluent_32, plus('#skF_2'(Time1_562, Fluent_567, Time2_564), n1)) | holdsAt(Fluent_32, '#skF_2'(Time1_562, Fluent_567, Time2_564))))).
% 7.33/2.76 tff(c_651, plain, (![Time1_554, Fluent_35, Time2_556, Fluent_557]: (startedIn(Time1_554, Fluent_35, Time2_556) | stoppedIn(Time1_554, Fluent_35, Time2_556) | ~stoppedIn(Time1_554, Fluent_557, Time2_556) | releasedAt(Fluent_35, plus('#skF_2'(Time1_554, Fluent_557, Time2_556), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_554, Fluent_557, Time2_556))))).
% 7.33/2.76 tff(c_631, plain, (![Fluent_544, Time2_3, Time1_545, Time1_1, Fluent_2]: (startedIn(Time1_545, Fluent_544, Time2_3) | ~less(Time1_545, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | stoppedIn(Time1_1, Fluent_544, Time2_3) | ~happens('#skF_7'(Fluent_544, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_544, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_544, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_605, plain, (![Fluent_532, Time1_531, Time2_533, Fluent_534, Time2_11, Time1_10]: (startedIn(Time1_10, Fluent_532, Time2_11) | ~less('#skF_2'(Time1_531, Fluent_534, Time2_533), Time2_11) | ~less(Time1_10, '#skF_2'(Time1_531, Fluent_534, Time2_533)) | stoppedIn(Time1_531, Fluent_532, Time2_533) | ~happens('#skF_7'(Fluent_532, '#skF_2'(Time1_531, Fluent_534, Time2_533)), '#skF_2'(Time1_531, Fluent_534, Time2_533)) | releasedAt(Fluent_532, plus('#skF_2'(Time1_531, Fluent_534, Time2_533), n1)) | ~releasedAt(Fluent_532, '#skF_2'(Time1_531, Fluent_534, Time2_533)) | ~stoppedIn(Time1_531, Fluent_534, Time2_533)))).
% 7.33/2.76 tff(c_613, plain, (![Fluent_35, Time1_536, Fluent_537, Time2_538]: (holdsAt(Fluent_35, plus('#skF_2'(Time1_536, Fluent_537, Time2_538), n1)) | stoppedIn(Time1_536, Fluent_35, Time2_538) | ~stoppedIn(Time1_536, Fluent_537, Time2_538) | releasedAt(Fluent_35, plus('#skF_2'(Time1_536, Fluent_537, Time2_538), n1)) | ~releasedAt(Fluent_35, '#skF_2'(Time1_536, Fluent_537, Time2_538))))).
% 7.33/2.76 tff(c_582, plain, (![Time1_1, Fluent_518, Time2_3, Fluent_2]: (stoppedIn(Time1_1, Fluent_518, Time2_3) | ~happens('#skF_7'(Fluent_518, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | initiates('#skF_7'(Fluent_518, '#skF_2'(Time1_1, Fluent_2, Time2_3)), Fluent_518, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_518, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_518, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_589, plain, (![Fluent_35, Time1_524, Time2_525, Fluent_526]: (holdsAt(Fluent_35, plus('#skF_4'(Time1_524, Time2_525, Fluent_526), n1)) | stoppedIn(Time1_524, Fluent_35, Time2_525) | ~startedIn(Time1_524, Fluent_526, Time2_525) | releasedAt(Fluent_35, plus('#skF_4'(Time1_524, Time2_525, Fluent_526), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_524, Time2_525, Fluent_526))))).
% 7.33/2.76 tff(c_207, plain, (![Fluent_160, Time2_3, Time1_159, Time1_1, Fluent_2]: (stoppedIn(Time1_159, Fluent_160, Time2_3) | ~less(Time1_159, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_7'(Fluent_160, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | initiates('#skF_7'(Fluent_160, '#skF_2'(Time1_1, Fluent_2, Time2_3)), Fluent_160, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_160, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~releasedAt(Fluent_160, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_561, plain, (![Time1_10, Fluent_509, Time2_11, Fluent_12]: (stoppedIn(Time1_10, Fluent_509, Time2_11) | ~happens('#skF_7'(Fluent_509, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | initiates('#skF_7'(Fluent_509, '#skF_4'(Time1_10, Time2_11, Fluent_12)), Fluent_509, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_509, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_509, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_209, plain, (![Fluent_160, Fluent_12, Time1_159, Time2_11, Time1_10]: (stoppedIn(Time1_159, Fluent_160, Time2_11) | ~less(Time1_159, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_7'(Fluent_160, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | initiates('#skF_7'(Fluent_160, '#skF_4'(Time1_10, Time2_11, Fluent_12)), Fluent_160, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_160, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_160, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_171, plain, (![Time1_1, Fluent_2, Time2_3]: (~happens('#skF_1'(Time1_1, Fluent_2, Time2_3), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | happens('#skF_8'(Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | releasedAt(Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | happens('#skF_5'(Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~holdsAt(Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_547, plain, (![Fluent_499, Time1_498, Time2_500, Fluent_501]: (happens('#skF_8'(Fluent_499, '#skF_4'(Time1_498, Time2_500, Fluent_501)), '#skF_4'(Time1_498, Time2_500, Fluent_501)) | releasedAt(Fluent_499, '#skF_4'(Time1_498, Time2_500, Fluent_501)) | startedIn(Time1_498, Fluent_499, Time2_500) | ~startedIn(Time1_498, Fluent_501, Time2_500) | ~holdsAt(Fluent_499, plus('#skF_4'(Time1_498, Time2_500, Fluent_501), n1)) | holdsAt(Fluent_499, '#skF_4'(Time1_498, Time2_500, Fluent_501))))).
% 7.33/2.76 tff(c_539, plain, (![Time1_494, Fluent_32, Time2_496, Fluent_497]: (startedIn(Time1_494, Fluent_32, Time2_496) | ~startedIn(Time1_494, Fluent_497, Time2_496) | ~holdsAt(Fluent_32, plus('#skF_4'(Time1_494, Time2_496, Fluent_497), n1)) | releasedAt(Fluent_32, plus('#skF_4'(Time1_494, Time2_496, Fluent_497), n1)) | holdsAt(Fluent_32, '#skF_4'(Time1_494, Time2_496, Fluent_497))))).
% 7.33/2.76 tff(c_509, plain, (![Fluent_476, Time1_475, Fluent_478, Time2_477]: (happens('#skF_8'(Fluent_476, '#skF_2'(Time1_475, Fluent_478, Time2_477)), '#skF_2'(Time1_475, Fluent_478, Time2_477)) | releasedAt(Fluent_476, '#skF_2'(Time1_475, Fluent_478, Time2_477)) | startedIn(Time1_475, Fluent_476, Time2_477) | ~stoppedIn(Time1_475, Fluent_478, Time2_477) | ~holdsAt(Fluent_476, plus('#skF_2'(Time1_475, Fluent_478, Time2_477), n1)) | holdsAt(Fluent_476, '#skF_2'(Time1_475, Fluent_478, Time2_477))))).
% 7.33/2.76 tff(c_525, plain, (![Time1_1, Fluent_2, Time2_3]: (startedIn(Time1_1, Fluent_2, Time2_3) | ~holdsAt(Fluent_2, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | holdsAt(Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_196, plain, (![Time1_155, Fluent_156, Fluent_12, Time2_11, Time1_10]: (startedIn(Time1_155, Fluent_156, Time2_11) | ~less(Time1_155, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_6'(Fluent_156, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~holdsAt(Fluent_156, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | releasedAt(Fluent_156, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | holdsAt(Fluent_156, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_501, plain, (![Time1_471, Fluent_32, Time2_473, Fluent_474]: (startedIn(Time1_471, Fluent_32, Time2_473) | ~stoppedIn(Time1_471, Fluent_474, Time2_473) | ~holdsAt(Fluent_32, plus('#skF_2'(Time1_471, Fluent_474, Time2_473), n1)) | releasedAt(Fluent_32, plus('#skF_2'(Time1_471, Fluent_474, Time2_473), n1)) | holdsAt(Fluent_32, '#skF_2'(Time1_471, Fluent_474, Time2_473))))).
% 7.33/2.76 tff(c_194, plain, (![Time1_155, Fluent_156, Time2_3, Time1_1, Fluent_2]: (startedIn(Time1_155, Fluent_156, Time2_3) | ~less(Time1_155, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_6'(Fluent_156, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~holdsAt(Fluent_156, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | releasedAt(Fluent_156, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | holdsAt(Fluent_156, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_470, plain, (![Time1_459, Fluent_12, Time2_11, Time1_10]: (startedIn(Time1_459, Fluent_12, Time2_11) | ~less(Time1_459, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_7'(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_12, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~releasedAt(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_383, plain, (![Time1_357, Time2_358, Time2_11, Fluent_356, Time1_10]: (startedIn(Time1_10, Fluent_356, Time2_11) | ~less('#skF_4'(Time1_357, Time2_358, Fluent_356), Time2_11) | ~less(Time1_10, '#skF_4'(Time1_357, Time2_358, Fluent_356)) | ~happens('#skF_7'(Fluent_356, '#skF_4'(Time1_357, Time2_358, Fluent_356)), '#skF_4'(Time1_357, Time2_358, Fluent_356)) | ~startedIn(Time1_357, Fluent_356, Time2_358) | releasedAt(Fluent_356, plus('#skF_4'(Time1_357, Time2_358, Fluent_356), n1)) | ~releasedAt(Fluent_356, '#skF_4'(Time1_357, Time2_358, Fluent_356))))).
% 7.33/2.76 tff(c_458, plain, (![Fluent_450, Time1_449, Time2_451, Fluent_452]: (happens('#skF_8'(Fluent_450, '#skF_4'(Time1_449, Time2_451, Fluent_452)), '#skF_4'(Time1_449, Time2_451, Fluent_452)) | releasedAt(Fluent_450, '#skF_4'(Time1_449, Time2_451, Fluent_452)) | stoppedIn(Time1_449, Fluent_450, Time2_451) | ~startedIn(Time1_449, Fluent_452, Time2_451) | holdsAt(Fluent_450, plus('#skF_4'(Time1_449, Time2_451, Fluent_452), n1)) | ~holdsAt(Fluent_450, '#skF_4'(Time1_449, Time2_451, Fluent_452))))).
% 7.33/2.76 tff(c_450, plain, (![Time1_445, Fluent_29, Time2_447, Fluent_448]: (stoppedIn(Time1_445, Fluent_29, Time2_447) | ~startedIn(Time1_445, Fluent_448, Time2_447) | holdsAt(Fluent_29, plus('#skF_4'(Time1_445, Time2_447, Fluent_448), n1)) | releasedAt(Fluent_29, plus('#skF_4'(Time1_445, Time2_447, Fluent_448), n1)) | ~holdsAt(Fluent_29, '#skF_4'(Time1_445, Time2_447, Fluent_448))))).
% 7.33/2.76 tff(c_431, plain, (![Fluent_430, Fluent_35, Time_36, Fluent_425, Time1_428, Time2_427, Time2_431, Time1_424]: (startedIn(Time1_428, Fluent_35, '#skF_2'(Time_36, Fluent_425, Time2_427)) | ~less(Time1_428, Time_36) | stoppedIn(Time1_424, Fluent_35, '#skF_2'(Time_36, Fluent_430, Time2_431)) | ~less(Time1_424, Time_36) | ~stoppedIn(Time_36, Fluent_430, Time2_431) | ~stoppedIn(Time_36, Fluent_425, Time2_427) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_183, plain, (![Time1_151, Fluent_12, Time2_11, Time1_10, Fluent_152]: (stoppedIn(Time1_151, Fluent_152, Time2_11) | ~less(Time1_151, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_5'(Fluent_152, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | holdsAt(Fluent_152, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | releasedAt(Fluent_152, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~holdsAt(Fluent_152, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_426, plain, (![Time1_408, Time2_412, Fluent_35, Time_36, Fluent_409, Time1_411, Fluent_415, Time2_413]: (startedIn(Time1_408, Fluent_35, '#skF_4'(Time_36, Time2_412, Fluent_409)) | ~less(Time1_408, Time_36) | stoppedIn(Time1_411, Fluent_35, '#skF_4'(Time_36, Time2_413, Fluent_415)) | ~less(Time1_411, Time_36) | ~startedIn(Time_36, Fluent_415, Time2_413) | ~startedIn(Time_36, Fluent_409, Time2_412) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_421, plain, (![Fluent_399, Time2_397, Time1_392, Fluent_35, Time2_396, Time_36, Fluent_393, Time1_395]: (startedIn(Time1_392, Fluent_35, '#skF_2'(Time_36, Fluent_393, Time2_396)) | ~less(Time1_392, Time_36) | stoppedIn(Time1_395, Fluent_35, '#skF_4'(Time_36, Time2_397, Fluent_399)) | ~less(Time1_395, Time_36) | ~startedIn(Time_36, Fluent_399, Time2_397) | ~stoppedIn(Time_36, Fluent_393, Time2_396) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_416, plain, (![Fluent_385, Time1_384, Fluent_387, Time2_386]: (happens('#skF_8'(Fluent_385, '#skF_2'(Time1_384, Fluent_387, Time2_386)), '#skF_2'(Time1_384, Fluent_387, Time2_386)) | releasedAt(Fluent_385, '#skF_2'(Time1_384, Fluent_387, Time2_386)) | stoppedIn(Time1_384, Fluent_385, Time2_386) | ~stoppedIn(Time1_384, Fluent_387, Time2_386) | holdsAt(Fluent_385, plus('#skF_2'(Time1_384, Fluent_387, Time2_386), n1)) | ~holdsAt(Fluent_385, '#skF_2'(Time1_384, Fluent_387, Time2_386))))).
% 7.33/2.76 tff(c_408, plain, (![Time1_380, Fluent_29, Time2_382, Fluent_383]: (stoppedIn(Time1_380, Fluent_29, Time2_382) | ~stoppedIn(Time1_380, Fluent_383, Time2_382) | holdsAt(Fluent_29, plus('#skF_2'(Time1_380, Fluent_383, Time2_382), n1)) | releasedAt(Fluent_29, plus('#skF_2'(Time1_380, Fluent_383, Time2_382), n1)) | ~holdsAt(Fluent_29, '#skF_2'(Time1_380, Fluent_383, Time2_382))))).
% 7.33/2.76 tff(c_389, plain, (![Fluent_35, Time_36, Fluent_360, Time2_366, Fluent_365, Time1_359, Time1_363, Time2_362]: (startedIn(Time1_363, Fluent_35, '#skF_4'(Time_36, Time2_362, Fluent_360)) | ~less(Time1_363, Time_36) | stoppedIn(Time1_359, Fluent_35, '#skF_2'(Time_36, Fluent_365, Time2_366)) | ~less(Time1_359, Time_36) | ~stoppedIn(Time_36, Fluent_365, Time2_366) | ~startedIn(Time_36, Fluent_360, Time2_362) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_181, plain, (![Time1_151, Time2_3, Time1_1, Fluent_152, Fluent_2]: (stoppedIn(Time1_151, Fluent_152, Time2_3) | ~less(Time1_151, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_5'(Fluent_152, '#skF_2'(Time1_1, Fluent_2, Time2_3)), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | holdsAt(Fluent_152, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | releasedAt(Fluent_152, plus('#skF_2'(Time1_1, Fluent_2, Time2_3), n1)) | ~holdsAt(Fluent_152, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_148, plain, (![Fluent_35, Time1_136, Time2_137]: (~happens('#skF_7'(Fluent_35, '#skF_4'(Time1_136, Time2_137, Fluent_35)), '#skF_4'(Time1_136, Time2_137, Fluent_35)) | ~startedIn(Time1_136, Fluent_35, Time2_137) | initiates('#skF_7'(Fluent_35, '#skF_4'(Time1_136, Time2_137, Fluent_35)), Fluent_35, '#skF_4'(Time1_136, Time2_137, Fluent_35)) | releasedAt(Fluent_35, plus('#skF_4'(Time1_136, Time2_137, Fluent_35), n1)) | ~releasedAt(Fluent_35, '#skF_4'(Time1_136, Time2_137, Fluent_35))))).
% 7.33/2.76 tff(c_160, plain, (![Fluent_12, Time1_10, Time2_11]: (happens('#skF_8'(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | releasedAt(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | happens('#skF_6'(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | holdsAt(Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_305, plain, (![Fluent_256, Time1_260, Fluent_257, Time2_259, Time1_258, Time2_11, Time1_10]: (startedIn(Time1_10, Fluent_256, Time2_11) | ~less(Time1_258, Time2_11) | ~less(Time1_10, Time1_258) | stoppedIn(Time1_260, Fluent_256, '#skF_2'(Time1_258, Fluent_257, Time2_259)) | ~less(Time1_260, Time1_258) | ~happens('#skF_7'(Fluent_256, Time1_258), Time1_258) | releasedAt(Fluent_256, plus(Time1_258, n1)) | ~releasedAt(Fluent_256, Time1_258) | ~stoppedIn(Time1_258, Fluent_257, Time2_259)))).
% 7.33/2.76 tff(c_321, plain, (![Time1_278, Fluent_276, Fluent_277, Time2_11, Time1_10, Time1_280, Time2_279]: (startedIn(Time1_10, Fluent_276, Time2_11) | ~less(Time1_278, Time2_11) | ~less(Time1_10, Time1_278) | stoppedIn(Time1_280, Fluent_276, '#skF_4'(Time1_278, Time2_279, Fluent_277)) | ~less(Time1_280, Time1_278) | ~happens('#skF_7'(Fluent_276, Time1_278), Time1_278) | releasedAt(Fluent_276, plus(Time1_278, n1)) | ~releasedAt(Fluent_276, Time1_278) | ~startedIn(Time1_278, Fluent_277, Time2_279)))).
% 7.33/2.76 tff(c_347, plain, (![Time1_331, Time2_328, Time2_3, Time1_1, Fluent_327, Fluent_2]: (stoppedIn(Time1_331, Fluent_2, '#skF_2'('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_327, Time2_328)) | ~less(Time1_331, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_327, Time2_328) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_341, plain, (![Fluent_309, Time2_310, Time2_3, Time1_1, Time1_313, Fluent_2]: (stoppedIn(Time1_313, Fluent_2, '#skF_4'('#skF_2'(Time1_1, Fluent_2, Time2_3), Time2_310, Fluent_309)) | ~less(Time1_313, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~startedIn('#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_309, Time2_310) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_337, plain, (![Fluent_304, Fluent_12, Time2_306, Time1_308, Time2_11, Time1_10]: (startedIn(Time1_308, Fluent_12, '#skF_2'('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_304, Time2_306)) | ~less(Time1_308, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~stoppedIn('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_304, Time2_306) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_332, plain, (![Time1_296, Fluent_12, Fluent_292, Time2_11, Time2_294, Time1_10]: (startedIn(Time1_296, Fluent_12, '#skF_4'('#skF_4'(Time1_10, Time2_11, Fluent_12), Time2_294, Fluent_292)) | ~less(Time1_296, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn('#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_292, Time2_294) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_327, plain, (![Time2_281, Fluent_35, Fluent_283, Time_36, Time1_284]: (holdsAt(Fluent_35, plus(Time_36, n1)) | stoppedIn(Time1_284, Fluent_35, '#skF_4'(Time_36, Time2_281, Fluent_283)) | ~less(Time1_284, Time_36) | ~startedIn(Time_36, Fluent_283, Time2_281) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_210, plain, (![Fluent_160, Fluent_12, Time1_159, Time2_11, Time1_10]: (stoppedIn(Time1_159, Fluent_160, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~less(Time1_159, Time1_10) | ~happens('#skF_7'(Fluent_160, Time1_10), Time1_10) | initiates('#skF_7'(Fluent_160, Time1_10), Fluent_160, Time1_10) | releasedAt(Fluent_160, plus(Time1_10, n1)) | ~releasedAt(Fluent_160, Time1_10) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.76 tff(c_312, plain, (![Time2_266, Fluent_35, Time_36, Fluent_268, Time1_270]: (holdsAt(Fluent_35, plus(Time_36, n1)) | stoppedIn(Time1_270, Fluent_35, '#skF_2'(Time_36, Fluent_268, Time2_266)) | ~less(Time1_270, Time_36) | ~stoppedIn(Time_36, Fluent_268, Time2_266) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.76 tff(c_297, plain, (![Time2_255, Fluent_252, Time1_251, Time_30, Fluent_29]: (stoppedIn(Time1_251, Fluent_29, '#skF_2'(Time_30, Fluent_252, Time2_255)) | ~less(Time1_251, Time_30) | ~stoppedIn(Time_30, Fluent_252, Time2_255) | holdsAt(Fluent_29, plus(Time_30, n1)) | releasedAt(Fluent_29, plus(Time_30, n1)) | ~holdsAt(Fluent_29, Time_30)))).
% 7.33/2.76 tff(c_208, plain, (![Fluent_160, Time2_3, Time1_159, Time1_1, Fluent_2]: (stoppedIn(Time1_159, Fluent_160, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~less(Time1_159, Time1_1) | ~happens('#skF_7'(Fluent_160, Time1_1), Time1_1) | initiates('#skF_7'(Fluent_160, Time1_1), Fluent_160, Time1_1) | releasedAt(Fluent_160, plus(Time1_1, n1)) | ~releasedAt(Fluent_160, Time1_1) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.76 tff(c_292, plain, (![Time1_242, Time2_244, Time_33, Fluent_241, Fluent_32]: (startedIn(Time1_242, Fluent_32, '#skF_4'(Time_33, Time2_244, Fluent_241)) | ~less(Time1_242, Time_33) | ~startedIn(Time_33, Fluent_241, Time2_244) | ~holdsAt(Fluent_32, plus(Time_33, n1)) | releasedAt(Fluent_32, plus(Time_33, n1)) | holdsAt(Fluent_32, Time_33)))).
% 7.33/2.76 tff(c_287, plain, (![Time_33, Time2_234, Time1_233, Fluent_32, Fluent_231]: (startedIn(Time1_233, Fluent_32, '#skF_2'(Time_33, Fluent_231, Time2_234)) | ~less(Time1_233, Time_33) | ~stoppedIn(Time_33, Fluent_231, Time2_234) | ~holdsAt(Fluent_32, plus(Time_33, n1)) | releasedAt(Fluent_32, plus(Time_33, n1)) | holdsAt(Fluent_32, Time_33)))).
% 7.33/2.76 tff(c_282, plain, (![Time2_3, Time1_223, Time1_1, Fluent_221, Fluent_2]: (stoppedIn('#skF_4'(Time1_223, '#skF_2'(Time1_1, Fluent_2, Time2_3), Fluent_221), Fluent_2, Time2_3) | ~startedIn(Time1_223, Fluent_221, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_276, plain, (![Time1_206, Time_30, Time2_210, Fluent_207, Fluent_29]: (stoppedIn(Time1_206, Fluent_29, '#skF_4'(Time_30, Time2_210, Fluent_207)) | ~less(Time1_206, Time_30) | ~startedIn(Time_30, Fluent_207, Time2_210) | holdsAt(Fluent_29, plus(Time_30, n1)) | releasedAt(Fluent_29, plus(Time_30, n1)) | ~holdsAt(Fluent_29, Time_30)))).
% 7.33/2.77 tff(c_272, plain, (![Fluent_202, Time1_203, Time2_3, Time1_1, Fluent_2]: (stoppedIn('#skF_2'(Time1_203, Fluent_202, '#skF_2'(Time1_1, Fluent_2, Time2_3)), Fluent_2, Time2_3) | ~stoppedIn(Time1_203, Fluent_202, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_267, plain, (![Time1_194, Fluent_12, Fluent_193, Time2_11, Time1_10]: (startedIn('#skF_2'(Time1_194, Fluent_193, '#skF_4'(Time1_10, Time2_11, Fluent_12)), Fluent_12, Time2_11) | ~stoppedIn(Time1_194, Fluent_193, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_262, plain, (![Fluent_183, Fluent_12, Time1_184, Time2_11, Time1_10]: (startedIn('#skF_4'(Time1_184, '#skF_4'(Time1_10, Time2_11, Fluent_12), Fluent_183), Fluent_12, Time2_11) | ~startedIn(Time1_184, Fluent_183, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_244, plain, (![Time1_175, Fluent_2, Time2_3, Time1_1]: (stoppedIn(Time1_175, Fluent_2, Time2_3) | ~less(Time1_175, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_1'(Time1_1, Fluent_2, Time2_3), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_85, plain, (![Time1_99, Time2_3, Time2_101, Time1_1, Fluent_2]: (stoppedIn(Time1_99, Fluent_2, Time2_101) | ~less('#skF_2'(Time1_1, Fluent_2, Time2_3), Time2_101) | ~less(Time1_99, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~happens('#skF_1'(Time1_1, Fluent_2, Time2_3), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_221, plain, (![Time1_166, Fluent_12, Time2_11, Time1_10]: (startedIn(Time1_166, Fluent_12, Time2_11) | ~less(Time1_166, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_3'(Time1_10, Time2_11, Fluent_12), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_89, plain, (![Time1_104, Fluent_12, Time2_11, Time1_10, Time2_105]: (startedIn(Time1_104, Fluent_12, Time2_105) | ~less('#skF_4'(Time1_10, Time2_11, Fluent_12), Time2_105) | ~less(Time1_104, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~happens('#skF_3'(Time1_10, Time2_11, Fluent_12), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_120, plain, (![Time1_1, Fluent_116, Time2_3, Time_117]: (stoppedIn(Time1_1, Fluent_116, Time2_3) | ~less(Time_117, Time2_3) | ~less(Time1_1, Time_117) | ~happens('#skF_7'(Fluent_116, Time_117), Time_117) | initiates('#skF_7'(Fluent_116, Time_117), Fluent_116, Time_117) | releasedAt(Fluent_116, plus(Time_117, n1)) | ~releasedAt(Fluent_116, Time_117)))).
% 7.33/2.77 tff(c_112, plain, (![Time1_10, Fluent_114, Time2_11, Time_115]: (startedIn(Time1_10, Fluent_114, Time2_11) | ~less(Time_115, Time2_11) | ~less(Time1_10, Time_115) | ~happens('#skF_6'(Fluent_114, Time_115), Time_115) | ~holdsAt(Fluent_114, plus(Time_115, n1)) | releasedAt(Fluent_114, plus(Time_115, n1)) | holdsAt(Fluent_114, Time_115)))).
% 7.33/2.77 tff(c_103, plain, (![Time1_1, Fluent_112, Time2_3, Time_113]: (stoppedIn(Time1_1, Fluent_112, Time2_3) | ~less(Time_113, Time2_3) | ~less(Time1_1, Time_113) | ~happens('#skF_5'(Fluent_112, Time_113), Time_113) | holdsAt(Fluent_112, plus(Time_113, n1)) | releasedAt(Fluent_112, plus(Time_113, n1)) | ~holdsAt(Fluent_112, Time_113)))).
% 7.33/2.77 tff(c_125, plain, (![Event_44, Fluent_118, Time_119]: (~terminates(Event_44, Fluent_118, Time_119) | ~happens(Event_44, Time_119) | happens('#skF_8'(Fluent_118, Time_119), Time_119) | releasedAt(Fluent_118, Time_119) | happens('#skF_5'(Fluent_118, Time_119), Time_119) | ~holdsAt(Fluent_118, Time_119)))).
% 7.33/2.77 tff(c_97, plain, (![Fluent_110, Time_111]: (happens('#skF_8'(Fluent_110, Time_111), Time_111) | releasedAt(Fluent_110, Time_111) | happens('#skF_6'(Fluent_110, Time_111), Time_111) | ~holdsAt(Fluent_110, plus(Time_111, n1)) | holdsAt(Fluent_110, Time_111)))).
% 7.33/2.77 tff(c_77, plain, (![Fluent_94, Time1_93, Time2_95]: (~releasedAt(Fluent_94, plus('#skF_2'(Time1_93, Fluent_94, Time2_95), n1)) | ~happens('#skF_1'(Time1_93, Fluent_94, Time2_95), '#skF_2'(Time1_93, Fluent_94, Time2_95)) | ~stoppedIn(Time1_93, Fluent_94, Time2_95)))).
% 7.33/2.77 tff(c_22, plain, (![Event_19, Offset_23, Fluent2_22, Fluent_21, Time_20]: (holdsAt(Fluent2_22, plus(Time_20, Offset_23)) | stoppedIn(Time_20, Fluent_21, plus(Time_20, Offset_23)) | ~trajectory(Fluent_21, Time_20, Fluent2_22, Offset_23) | ~less(n0, Offset_23) | ~initiates(Event_19, Fluent_21, Time_20) | ~happens(Event_19, Time_20)))).
% 7.33/2.77 tff(c_138, plain, (![Event_44, Fluent_131, Time1_132, Time2_133]: (~terminates(Event_44, Fluent_131, '#skF_4'(Time1_132, Time2_133, Fluent_131)) | ~happens(Event_44, '#skF_4'(Time1_132, Time2_133, Fluent_131)) | ~startedIn(Time1_132, Fluent_131, Time2_133)))).
% 7.33/2.77 tff(c_134, plain, (![Fluent_12, Time1_10, Time2_11]: (holdsAt(Fluent_12, plus('#skF_4'(Time1_10, Time2_11, Fluent_12), n1)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_24, plain, (![Fluent2_28, Fluent1_26, Time2_27, Event_24, Time1_25]: (holdsAt(Fluent2_28, plus(Time1_25, Time2_27)) | startedIn(Time1_25, Fluent1_26, plus(Time1_25, Time2_27)) | ~antitrajectory(Fluent1_26, Time1_25, Fluent2_28, Time2_27) | ~less(n0, Time2_27) | ~terminates(Event_24, Fluent1_26, Time1_25) | ~happens(Event_24, Time1_25)))).
% 7.33/2.77 tff(c_73, plain, (![Fluent_92, Time1_90, Time2_91]: (~releasedAt(Fluent_92, plus('#skF_4'(Time1_90, Time2_91, Fluent_92), n1)) | ~happens('#skF_3'(Time1_90, Time2_91, Fluent_92), '#skF_4'(Time1_90, Time2_91, Fluent_92)) | ~startedIn(Time1_90, Fluent_92, Time2_91)))).
% 7.33/2.77 tff(c_93, plain, (![Fluent_108, Time_109]: (happens('#skF_8'(Fluent_108, Time_109), Time_109) | releasedAt(Fluent_108, Time_109) | happens('#skF_5'(Fluent_108, Time_109), Time_109) | holdsAt(Fluent_108, plus(Time_109, n1)) | ~holdsAt(Fluent_108, Time_109)))).
% 7.33/2.77 tff(c_34, plain, (![Fluent_35, Time_36]: (terminates('#skF_7'(Fluent_35, Time_36), Fluent_35, Time_36) | initiates('#skF_7'(Fluent_35, Time_36), Fluent_35, Time_36) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.77 tff(c_30, plain, (![Fluent_32, Time_33]: (initiates('#skF_6'(Fluent_32, Time_33), Fluent_32, Time_33) | ~holdsAt(Fluent_32, plus(Time_33, n1)) | releasedAt(Fluent_32, plus(Time_33, n1)) | holdsAt(Fluent_32, Time_33)))).
% 7.33/2.77 tff(c_26, plain, (![Fluent_29, Time_30]: (terminates('#skF_5'(Fluent_29, Time_30), Fluent_29, Time_30) | holdsAt(Fluent_29, plus(Time_30, n1)) | releasedAt(Fluent_29, plus(Time_30, n1)) | ~holdsAt(Fluent_29, Time_30)))).
% 7.33/2.77 tff(c_32, plain, (![Fluent_32, Time_33]: (happens('#skF_6'(Fluent_32, Time_33), Time_33) | ~holdsAt(Fluent_32, plus(Time_33, n1)) | releasedAt(Fluent_32, plus(Time_33, n1)) | holdsAt(Fluent_32, Time_33)))).
% 7.33/2.77 tff(c_28, plain, (![Fluent_29, Time_30]: (happens('#skF_5'(Fluent_29, Time_30), Time_30) | holdsAt(Fluent_29, plus(Time_30, n1)) | releasedAt(Fluent_29, plus(Time_30, n1)) | ~holdsAt(Fluent_29, Time_30)))).
% 7.33/2.77 tff(c_12, plain, (![Fluent_12, Time_18, Time2_11, Time1_10, Event_17]: (startedIn(Time1_10, Fluent_12, Time2_11) | ~initiates(Event_17, Fluent_12, Time_18) | ~less(Time_18, Time2_11) | ~less(Time1_10, Time_18) | ~happens(Event_17, Time_18)))).
% 7.33/2.77 tff(c_2, plain, (![Time_9, Event_8, Time2_3, Time1_1, Fluent_2]: (stoppedIn(Time1_1, Fluent_2, Time2_3) | ~terminates(Event_8, Fluent_2, Time_9) | ~less(Time_9, Time2_3) | ~less(Time1_1, Time_9) | ~happens(Event_8, Time_9)))).
% 7.33/2.77 tff(c_38, plain, (![Fluent_38, Time_39]: (releases('#skF_8'(Fluent_38, Time_39), Fluent_38, Time_39) | ~releasedAt(Fluent_38, plus(Time_39, n1)) | releasedAt(Fluent_38, Time_39)))).
% 7.33/2.77 tff(c_4, plain, (![Time1_1, Fluent_2, Time2_3]: (terminates('#skF_1'(Time1_1, Fluent_2, Time2_3), Fluent_2, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_14, plain, (![Time1_10, Time2_11, Fluent_12]: (initiates('#skF_3'(Time1_10, Time2_11, Fluent_12), Fluent_12, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_40, plain, (![Fluent_38, Time_39]: (happens('#skF_8'(Fluent_38, Time_39), Time_39) | ~releasedAt(Fluent_38, plus(Time_39, n1)) | releasedAt(Fluent_38, Time_39)))).
% 7.33/2.77 tff(c_10, plain, (![Time1_1, Fluent_2, Time2_3]: (happens('#skF_1'(Time1_1, Fluent_2, Time2_3), '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_36, plain, (![Fluent_35, Time_36]: (happens('#skF_7'(Fluent_35, Time_36), Time_36) | releasedAt(Fluent_35, plus(Time_36, n1)) | ~releasedAt(Fluent_35, Time_36)))).
% 7.33/2.77 tff(c_20, plain, (![Time1_10, Time2_11, Fluent_12]: (happens('#skF_3'(Time1_10, Time2_11, Fluent_12), '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_48, plain, (![Event_50, Fluent_52, Time_51]: (~terminates(Event_50, Fluent_52, Time_51) | ~releasedAt(Fluent_52, plus(Time_51, n1)) | ~happens(Event_50, Time_51)))).
% 7.33/2.77 tff(c_42, plain, (![Fluent_43, Time_42, Event_41]: (holdsAt(Fluent_43, plus(Time_42, n1)) | ~initiates(Event_41, Fluent_43, Time_42) | ~happens(Event_41, Time_42)))).
% 7.33/2.77 tff(c_46, plain, (![Fluent_49, Time_48, Event_47]: (releasedAt(Fluent_49, plus(Time_48, n1)) | ~releases(Event_47, Fluent_49, Time_48) | ~happens(Event_47, Time_48)))).
% 7.33/2.77 tff(c_44, plain, (![Fluent_46, Time_45, Event_44]: (~holdsAt(Fluent_46, plus(Time_45, n1)) | ~terminates(Event_44, Fluent_46, Time_45) | ~happens(Event_44, Time_45)))).
% 7.33/2.77 tff(c_50, plain, (![Event_50, Fluent_52, Time_51]: (~initiates(Event_50, Fluent_52, Time_51) | ~releasedAt(Fluent_52, plus(Time_51, n1)) | ~happens(Event_50, Time_51)))).
% 7.33/2.77 tff(c_6, plain, (![Time1_1, Fluent_2, Time2_3]: (less('#skF_2'(Time1_1, Fluent_2, Time2_3), Time2_3) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_8, plain, (![Time1_1, Fluent_2, Time2_3]: (less(Time1_1, '#skF_2'(Time1_1, Fluent_2, Time2_3)) | ~stoppedIn(Time1_1, Fluent_2, Time2_3)))).
% 7.33/2.77 tff(c_16, plain, (![Time1_10, Time2_11, Fluent_12]: (less('#skF_4'(Time1_10, Time2_11, Fluent_12), Time2_11) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 tff(c_18, plain, (![Time1_10, Time2_11, Fluent_12]: (less(Time1_10, '#skF_4'(Time1_10, Time2_11, Fluent_12)) | ~startedIn(Time1_10, Fluent_12, Time2_11)))).
% 7.33/2.77 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.33/2.77
%------------------------------------------------------------------------------