MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c) -> f1(a, b, c) (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a, b, c) with all transitions in problem 1, the following new transition is obtained: f0(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] We thus obtain the following problem: 2: T: (1, 2) f0(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] with all transitions in problem 2, the following new transition is obtained: f0(a, b, c) -> f1(a + 2*b - c, b - 2*c - 1, c + 2) [ a >= 1 /\ a + b >= 1 ] We thus obtain the following problem: 3: T: (1, 3) f0(a, b, c) -> f1(a + 2*b - c, b - 2*c - 1, c + 2) [ a >= 1 /\ a + b >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 2*b - c, b - 2*c - 1, c + 2) [ a >= 1 /\ a + b >= 1 ] with all transitions in problem 3, the following new transition is obtained: f0(a, b, c) -> f1(a + 3*b - 3*c - 1, b - 3*c - 3, c + 3) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 ] We thus obtain the following problem: 4: T: (1, 4) f0(a, b, c) -> f1(a + 3*b - 3*c - 1, b - 3*c - 3, c + 3) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 3*b - 3*c - 1, b - 3*c - 3, c + 3) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 ] with all transitions in problem 4, the following new transition is obtained: f0(a, b, c) -> f1(a + 4*b - 6*c - 4, b - 4*c - 6, c + 4) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 ] We thus obtain the following problem: 5: T: (1, 5) f0(a, b, c) -> f1(a + 4*b - 6*c - 4, b - 4*c - 6, c + 4) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 4*b - 6*c - 4, b - 4*c - 6, c + 4) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 ] with all transitions in problem 5, the following new transition is obtained: f0(a, b, c) -> f1(a + 5*b - 10*c - 10, b - 5*c - 10, c + 5) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 ] We thus obtain the following problem: 6: T: (1, 6) f0(a, b, c) -> f1(a + 5*b - 10*c - 10, b - 5*c - 10, c + 5) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 5*b - 10*c - 10, b - 5*c - 10, c + 5) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 ] with all transitions in problem 6, the following new transition is obtained: f0(a, b, c) -> f1(a + 6*b - 15*c - 20, b - 6*c - 15, c + 6) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 ] We thus obtain the following problem: 7: T: (1, 7) f0(a, b, c) -> f1(a + 6*b - 15*c - 20, b - 6*c - 15, c + 6) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 6*b - 15*c - 20, b - 6*c - 15, c + 6) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 ] with all transitions in problem 7, the following new transition is obtained: f0(a, b, c) -> f1(a + 7*b - 21*c - 35, b - 7*c - 21, c + 7) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 ] We thus obtain the following problem: 8: T: (1, 8) f0(a, b, c) -> f1(a + 7*b - 21*c - 35, b - 7*c - 21, c + 7) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 7*b - 21*c - 35, b - 7*c - 21, c + 7) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 ] with all transitions in problem 8, the following new transition is obtained: f0(a, b, c) -> f1(a + 8*b - 28*c - 56, b - 8*c - 28, c + 8) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 ] We thus obtain the following problem: 9: T: (1, 9) f0(a, b, c) -> f1(a + 8*b - 28*c - 56, b - 8*c - 28, c + 8) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 8*b - 28*c - 56, b - 8*c - 28, c + 8) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 ] with all transitions in problem 9, the following new transition is obtained: f0(a, b, c) -> f1(a + 9*b - 36*c - 84, b - 9*c - 36, c + 9) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 ] We thus obtain the following problem: 10: T: (1, 10) f0(a, b, c) -> f1(a + 9*b - 36*c - 84, b - 9*c - 36, c + 9) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 9*b - 36*c - 84, b - 9*c - 36, c + 9) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 ] with all transitions in problem 10, the following new transition is obtained: f0(a, b, c) -> f1(a + 10*b - 45*c - 120, b - 10*c - 45, c + 10) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 ] We thus obtain the following problem: 11: T: (1, 11) f0(a, b, c) -> f1(a + 10*b - 45*c - 120, b - 10*c - 45, c + 10) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 10*b - 45*c - 120, b - 10*c - 45, c + 10) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 ] with all transitions in problem 11, the following new transition is obtained: f0(a, b, c) -> f1(a + 11*b - 55*c - 165, b - 11*c - 55, c + 11) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 ] We thus obtain the following problem: 12: T: (1, 12) f0(a, b, c) -> f1(a + 11*b - 55*c - 165, b - 11*c - 55, c + 11) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 11*b - 55*c - 165, b - 11*c - 55, c + 11) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 ] with all transitions in problem 12, the following new transition is obtained: f0(a, b, c) -> f1(a + 12*b - 66*c - 220, b - 12*c - 66, c + 12) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 ] We thus obtain the following problem: 13: T: (1, 13) f0(a, b, c) -> f1(a + 12*b - 66*c - 220, b - 12*c - 66, c + 12) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 12*b - 66*c - 220, b - 12*c - 66, c + 12) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 ] with all transitions in problem 13, the following new transition is obtained: f0(a, b, c) -> f1(a + 13*b - 78*c - 286, b - 13*c - 78, c + 13) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 ] We thus obtain the following problem: 14: T: (1, 14) f0(a, b, c) -> f1(a + 13*b - 78*c - 286, b - 13*c - 78, c + 13) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 13*b - 78*c - 286, b - 13*c - 78, c + 13) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 ] with all transitions in problem 14, the following new transition is obtained: f0(a, b, c) -> f1(a + 14*b - 91*c - 364, b - 14*c - 91, c + 14) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 /\ a + 13*b - 78*c - 286 >= 1 ] We thus obtain the following problem: 15: T: (1, 15) f0(a, b, c) -> f1(a + 14*b - 91*c - 364, b - 14*c - 91, c + 14) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 /\ a + 13*b - 78*c - 286 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b, c) -> f1(a + 14*b - 91*c - 364, b - 14*c - 91, c + 14) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 /\ a + 13*b - 78*c - 286 >= 1 ] with all transitions in problem 15, the following new transition is obtained: f0(a, b, c) -> f1(a + 15*b - 105*c - 455, b - 15*c - 105, c + 15) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 /\ a + 13*b - 78*c - 286 >= 1 /\ a + 14*b - 91*c - 364 >= 1 ] We thus obtain the following problem: 16: T: (1, 16) f0(a, b, c) -> f1(a + 15*b - 105*c - 455, b - 15*c - 105, c + 15) [ a >= 1 /\ a + b >= 1 /\ a + 2*b - c >= 1 /\ a + 3*b - 3*c - 1 >= 1 /\ a + 4*b - 6*c - 4 >= 1 /\ a + 5*b - 10*c - 10 >= 1 /\ a + 6*b - 15*c - 20 >= 1 /\ a + 7*b - 21*c - 35 >= 1 /\ a + 8*b - 28*c - 56 >= 1 /\ a + 9*b - 36*c - 84 >= 1 /\ a + 10*b - 45*c - 120 >= 1 /\ a + 11*b - 55*c - 165 >= 1 /\ a + 12*b - 66*c - 220 >= 1 /\ a + 13*b - 78*c - 286 >= 1 /\ a + 14*b - 91*c - 364 >= 1 ] (?, 1) f1(a, b, c) -> f1(a + b, b - c, c + 1) [ a >= 1 ] start location: f0 leaf cost: 0 Complexity upper bound ? Time: 5.276 sec (SMT: 5.073 sec)