MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m) (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f2(0, o, p, 3, n, 0, o, p, 3, n, 2, l, m) [ 7 >= n /\ n >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f2(0, o, p, n, q, 0, o, p, n, q, 2, l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(o, p, n, 2, q, o, p, n, 2, q, 1, l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(o, p, n, 2, q, o, p, n, 2, q, 1, l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(o, p, n, 2, q, o, p, n, 2, q, 1, l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f1(o, p, n, 2, q, o, p, n, 2, q, 1, l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f4(o, p, n, q, 2, o, p, n, q, 2, 4, l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m) -> f4(o, p, n, q, 7, o, p, n, q, 7, 4, l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [l, m]. We thus obtain the following problem: 2: T: (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] with all transitions in problem 2, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 ] We thus obtain the following problem: 3: T: (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 ] with all transitions in problem 3, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 ] We thus obtain the following problem: 4: T: (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 ] with all transitions in problem 4, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 ] We thus obtain the following problem: 5: T: (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 ] with all transitions in problem 5, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 ] We thus obtain the following problem: 6: T: (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 ] with all transitions in problem 6, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 ] We thus obtain the following problem: 7: T: (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 ] with all transitions in problem 7, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 ] We thus obtain the following problem: 8: T: (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 ] with all transitions in problem 8, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 ] We thus obtain the following problem: 9: T: (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 ] with all transitions in problem 9, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 ] We thus obtain the following problem: 10: T: (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 ] with all transitions in problem 10, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 ] We thus obtain the following problem: 11: T: (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 ] with all transitions in problem 11, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 ] We thus obtain the following problem: 12: T: (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 11) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 ] with all transitions in problem 12, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 ] We thus obtain the following problem: 13: T: (?, 12) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 12) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 ] (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 ] with all transitions in problem 13, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 ] We thus obtain the following problem: 14: T: (?, 13) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 13) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 ] (?, 12) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 ] with all transitions in problem 14, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 ] We thus obtain the following problem: 15: T: (?, 14) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 14) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 ] (?, 13) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 12) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 ] with all transitions in problem 15, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 ] We thus obtain the following problem: 16: T: (?, 15) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 15) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 ] (?, 14) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 13) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 12) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 By chaining the transition f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 ] with all transitions in problem 16, the following new transitions are obtained: f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 /\ r''''''''''''''' >= 1 /\ 7 >= r''''''''''''''' /\ s''''''''''''''' >= 1 /\ 7 >= s''''''''''''''' /\ q''''''''''''''' >= 1 /\ 7 >= q''''''''''''''' /\ 1 >= o''''''''''''''' /\ o''''''''''''''' >= 0 ] We thus obtain the following problem: 17: T: (?, 16) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 16) f4(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ r'''''''''''''' >= 1 /\ 7 >= r'''''''''''''' /\ s'''''''''''''' >= 1 /\ 7 >= s'''''''''''''' /\ q'''''''''''''' >= 1 /\ 7 >= q'''''''''''''' /\ 1 >= o'''''''''''''' /\ o'''''''''''''' >= 0 /\ r''''''''''''''' >= 1 /\ 7 >= r''''''''''''''' /\ s''''''''''''''' >= 1 /\ 7 >= s''''''''''''''' /\ q''''''''''''''' >= 1 /\ 7 >= q''''''''''''''' /\ 1 >= o''''''''''''''' /\ o''''''''''''''' >= 0 ] (?, 15) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ r''''''''''''' >= 1 /\ 7 >= r''''''''''''' /\ s''''''''''''' >= 1 /\ 7 >= s''''''''''''' /\ q''''''''''''' >= 1 /\ 7 >= q''''''''''''' /\ 1 >= o''''''''''''' /\ o''''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 14) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ r'''''''''''' >= 1 /\ 7 >= r'''''''''''' /\ s'''''''''''' >= 1 /\ 7 >= s'''''''''''' /\ q'''''''''''' >= 1 /\ 7 >= q'''''''''''' /\ 1 >= o'''''''''''' /\ o'''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 13) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ r''''''''''' >= 1 /\ 7 >= r''''''''''' /\ s''''''''''' >= 1 /\ 7 >= s''''''''''' /\ q''''''''''' >= 1 /\ 7 >= q''''''''''' /\ 1 >= o''''''''''' /\ o''''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 12) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ r'''''''''' >= 1 /\ 7 >= r'''''''''' /\ s'''''''''' >= 1 /\ 7 >= s'''''''''' /\ q'''''''''' >= 1 /\ 7 >= q'''''''''' /\ 1 >= o'''''''''' /\ o'''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 11) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ r''''''''' >= 1 /\ 7 >= r''''''''' /\ s''''''''' >= 1 /\ 7 >= s''''''''' /\ q''''''''' >= 1 /\ 7 >= q''''''''' /\ 1 >= o''''''''' /\ o''''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 10) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ r'''''''' >= 1 /\ 7 >= r'''''''' /\ s'''''''' >= 1 /\ 7 >= s'''''''' /\ q'''''''' >= 1 /\ 7 >= q'''''''' /\ 1 >= o'''''''' /\ o'''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 9) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ r''''''' >= 1 /\ 7 >= r''''''' /\ s''''''' >= 1 /\ 7 >= s''''''' /\ q''''''' >= 1 /\ 7 >= q''''''' /\ 1 >= o''''''' /\ o''''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 8) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ r'''''' >= 1 /\ 7 >= r'''''' /\ s'''''' >= 1 /\ 7 >= s'''''' /\ q'''''' >= 1 /\ 7 >= q'''''' /\ 1 >= o'''''' /\ o'''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 7) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ r''''' >= 1 /\ 7 >= r''''' /\ s''''' >= 1 /\ 7 >= s''''' /\ q''''' >= 1 /\ 7 >= q''''' /\ 1 >= o''''' /\ o''''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 6) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ r'''' >= 1 /\ 7 >= r'''' /\ s'''' >= 1 /\ 7 >= s'''' /\ q'''' >= 1 /\ 7 >= q'''' /\ 1 >= o'''' /\ o'''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 5) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ r''' >= 1 /\ 7 >= r''' /\ s''' >= 1 /\ 7 >= s''' /\ q''' >= 1 /\ 7 >= q''' /\ 1 >= o''' /\ o''' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 4) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ r'' >= 1 /\ 7 >= r'' /\ s'' >= 1 /\ 7 >= s'' /\ q'' >= 1 /\ 7 >= q'' /\ 1 >= o'' /\ o'' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 3) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ r' >= 1 /\ 7 >= r' /\ s' >= 1 /\ 7 >= s' /\ q' >= 1 /\ 7 >= q' /\ 1 >= o' /\ o' >= 0 /\ 7 >= n /\ n >= 1 ] (?, 2) f4(l, m) -> f2(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 /\ 7 >= n /\ n >= 1 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f4(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f1(l, m) [ r >= l /\ s >= m /\ t >= 1 /\ 7 >= t /\ u >= 1 /\ 7 >= u /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f2(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f1(l, m) -> f1(l, m) [ r >= 1 /\ 7 >= r /\ s >= 1 /\ 7 >= s /\ q >= 1 /\ 7 >= q /\ 1 >= o /\ o >= 0 ] (?, 1) f4(l, m) -> f2(l, m) [ l >= 1 /\ l >= p + 1 /\ m >= 1 /\ m >= o + 1 /\ 7 >= q /\ 7 >= n /\ q >= 1 /\ n >= 1 ] (?, 1) f1(l, m) -> f2(l, m) [ 7 >= n /\ n >= 1 ] (1, 1) f0(l, m) -> f1(l, m) start location: f0 leaf cost: 0 Complexity upper bound ? Time: 23.419 sec (SMT: 9.271 sec)