p cnf 70 174 -67 69 0 67 68 0 67 0 -61 66 0 61 65 0 64 0 63 0 -51 57 60 62 0 -51 56 0 51 55 0 -48 57 0 48 52 0 48 -51 -67 -70 0 -48 51 -67 -70 0 -48 -51 -67 70 0 -47 57 58 59 0 -47 54 0 47 53 0 41 -70 0 40 70 0 -38 50 0 38 -47 -48 -61 0 -38 47 -48 -61 0 -38 -47 48 -61 0 -38 -47 -48 61 0 38 39 0 38 0 -36 -37 0 -35 45 0 -35 -37 0 -35 -36 0 -34 -37 0 -34 -36 0 -34 -35 0 -33 0 -31 43 0 -31 -32 0 31 0 -30 -32 0 -30 -31 0 -28 -29 0 -27 -29 0 -27 -28 0 -26 51 0 -26 48 0 -25 -26 0 -24 70 0 -24 48 0 -24 34 0 -24 27 0 -24 25 0 -23 51 0 -23 49 0 -23 48 0 -23 37 0 -23 29 0 -23 25 0 -22 70 0 -22 48 0 -22 35 0 -22 27 0 -22 25 0 -21 70 0 -21 48 0 -21 44 0 -21 36 0 -21 29 0 -21 25 0 -20 70 0 -20 48 0 -20 35 0 -20 27 0 -20 25 0 19 -26 -37 0 -19 -26 37 0 19 -24 0 18 -26 -36 0 -18 -26 36 0 18 -23 0 18 -22 0 -18 -19 0 -17 44 0 17 -26 -35 0 -17 -26 35 0 17 -21 0 -17 -19 0 -17 -18 0 16 -26 -34 0 -16 -26 34 0 16 -20 0 -16 -19 0 -16 -18 0 -16 -17 0 16 0 -15 48 0 -15 47 0 -15 -26 0 -14 -15 0 -13 61 0 -13 48 0 -13 30 0 -13 27 0 -13 14 0 -12 48 0 -12 47 0 -12 46 0 -12 33 0 -12 28 0 -12 14 0 -11 61 0 -11 48 0 -11 27 0 -11 14 0 -10 61 0 -10 48 0 -10 42 0 -10 32 0 -10 28 0 -10 14 0 -9 61 0 -9 48 0 -9 27 0 -9 14 0 -8 -15 33 0 8 -13 0 7 -15 -32 0 -7 -15 32 0 7 -12 0 7 -11 0 -7 -8 0 -6 42 0 6 -15 -31 0 6 -10 0 -6 -8 0 -6 -7 0 5 -15 -30 0 -5 -15 30 0 5 -9 0 -5 -8 0 -5 -7 0 -5 -6 0 5 0 4 -23 0 3 -12 0 -3 -4 0 2 -22 0 2 -20 0 2 -11 0 2 -9 0 -2 -4 0 -2 -3 0 2 0 -1 52 0 -1 51 0 -1 47 0 -1 -25 0 1 20 21 24 22 23 26 0 -1 19 -37 0 -1 -19 37 0 -1 18 -36 0 -1 -18 36 0 -1 17 -35 0 -1 -17 35 0 -1 -16 34 0 -1 -14 0 1 9 10 13 11 12 15 0 -1 -8 33 0 -1 7 -32 0 -1 -7 32 0 -1 6 -31 0 -1 -5 30 0 -1 -4 29 0 -1 -3 28 0 -1 -2 27 0 c 1: AT0_DELTA c 2: AT0_ID0 c 3: AT0_ID1 c 4: AT0_ID2 c 5: AT0_PROC1_A c 6: AT0_PROC1_B c 7: AT0_PROC1_C c 8: AT0_PROC1_CS c 9: AT0_PROC1_SW_A_B_TAU c 10: AT0_PROC1_SW_B_C_TAU c 11: AT0_PROC1_SW_C_B_TAU c 12: AT0_PROC1_SW_C_CS_TAU c 13: AT0_PROC1_SW_CS_A_TAU c 14: AT0_PROC1_TAU c 15: AT0_PROC1_WAIT c 16: AT0_PROC2_A c 17: AT0_PROC2_B c 18: AT0_PROC2_C c 19: AT0_PROC2_CS c 20: AT0_PROC2_SW_A_B_TAU c 21: AT0_PROC2_SW_B_C_TAU c 22: AT0_PROC2_SW_C_B_TAU c 23: AT0_PROC2_SW_C_CS_TAU c 24: AT0_PROC2_SW_CS_A_TAU c 25: AT0_PROC2_TAU c 26: AT0_PROC2_WAIT c 27: AT1_ID0 c 28: AT1_ID1 c 29: AT1_ID2 c 30: AT1_PROC1_A c 31: AT1_PROC1_B c 32: AT1_PROC1_C c 33: AT1_PROC1_CS c 34: AT1_PROC2_A c 35: AT1_PROC2_B c 36: AT1_PROC2_C c 37: AT1_PROC2_CS c def int 38 ( AT0_PROC1_X ) - AT0_Z = 0 c def int 39 ( AT0_PROC1_X ) - AT0_Z > 0 c def int 50 ( AT0_PROC1_X ) - AT0_Z <= 0 c def int 61 ( AT1_PROC1_X ) - AT1_Z = 0 c def int 65 ( AT1_PROC1_X ) - AT1_Z > 0 c def int 66 ( AT1_PROC1_X ) - AT1_Z <= 0 c def int 67 ( AT0_PROC2_X ) - AT0_Z = 0 c def int 68 ( AT0_PROC2_X ) - AT0_Z > 0 c def int 69 ( AT0_PROC2_X ) - AT0_Z <= 0 c def int 70 ( AT1_PROC2_X ) - AT1_Z = 0 c def int 40 ( AT1_PROC2_X ) - AT1_Z > 0 c def int 41 ( AT1_PROC2_X ) - AT1_Z <= 0 c def int 42 ( ( AT0_PROC1_X - AT0_Z ) ) - 10 <= 0 c def int 43 ( ( AT1_PROC1_X - AT1_Z ) ) - 10 <= 0 c def int 44 ( ( AT0_PROC2_X - AT0_Z ) ) - 10 <= 0 c def int 45 ( ( AT1_PROC2_X - AT1_Z ) ) - 10 <= 0 c def int 46 ( ( AT0_PROC1_X - AT0_Z ) ) - 10 > 0 c def int 47 ( AT1_PROC1_X ) - AT0_PROC1_X = 0 c def int 48 ( AT1_Z ) - AT0_Z = 0 c def int 49 ( ( AT0_PROC2_X - AT0_Z ) ) - 10 > 0 c def int 51 ( AT1_PROC2_X ) - AT0_PROC2_X = 0 c def int 52 ( AT1_Z ) - AT0_Z < 0 c def int 53 ( AT1_PROC1_X ) - AT0_PROC1_X < 0 c def int 54 ( AT1_PROC1_X ) - AT0_PROC1_X >= 0 c def int 55 ( AT1_PROC2_X ) - AT0_PROC2_X < 0 c def int 56 ( AT1_PROC2_X ) - AT0_PROC2_X >= 0 c def int 57 ( AT1_Z ) - AT0_Z >= 0 c def int 58 ( AT0_Z ) - AT0_PROC1_X >= 0 c def int 59 ( AT1_Z ) - AT1_PROC1_X < 0 c def int 60 ( AT0_Z ) - AT0_PROC2_X >= 0 c def int 62 ( AT1_Z ) - AT1_PROC2_X < 0 c def int 63 ( ( AT1_PROC1_X - AT1_Z ) ) - ( AT1_PROC1_X - AT1_Z ) = 0 c def int 64 ( ( AT1_PROC2_X - AT1_Z ) ) - ( AT1_PROC2_X - AT1_Z ) = 0