NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f1(A,B,C,D,E) -> f0(A,B,C,D,E) True (1,1) 1. f0(A,B,C,D,E) -> f0(F,B,C,H,F) [2*F >= 1 && G >= 1 && A = 2*F] (?,1) 2. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && 2*G >= 1 + A && 3*A >= 3*F && 3*F >= 3*A && 2*G >= 1 + F && F >= 1] (?,1) 3. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && A >= 1 + 2*G && 3*A >= 3*F && 3*F >= 3*A && F >= 1 + 2*G && F >= 1] (?,1) 4. f0(A,B,C,D,E) -> f2(A,F,C,D,E) [0 >= A] (?,1) Signature: {(f0,5);(f1,5);(f2,5)} Flow Graph: [0->{1,2,3,4},1->{1,2,3,4},2->{1,2,3,4},3->{1,2,3,4},4->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f1(A,B,C,D,E) -> f0(A,B,C,D,E) True (1,1) 1. f0(A,B,C,D,E) -> f0(F,B,C,H,F) [2*F >= 1 && G >= 1 && A = 2*F] (?,1) 2. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && 2*G >= 1 + A && 3*A >= 3*F && 3*F >= 3*A && 2*G >= 1 + F && F >= 1] (?,1) 3. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && A >= 1 + 2*G && 3*A >= 3*F && 3*F >= 3*A && F >= 1 + 2*G && F >= 1] (?,1) 4. f0(A,B,C,D,E) -> f2(A,F,C,D,E) [0 >= A] (1,1) Signature: {(f0,5);(f1,5);(f2,5)} Flow Graph: [0->{1,2,3,4},1->{1,2,3,4},2->{1,2,3,4},3->{1,2,3,4},4->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(2,4),(3,4)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f1(A,B,C,D,E) -> f0(A,B,C,D,E) True (1,1) 1. f0(A,B,C,D,E) -> f0(F,B,C,H,F) [2*F >= 1 && G >= 1 && A = 2*F] (?,1) 2. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && 2*G >= 1 + A && 3*A >= 3*F && 3*F >= 3*A && 2*G >= 1 + F && F >= 1] (?,1) 3. f0(A,B,C,D,E) -> f0(1 + 3*A,B,F,H,G) [A >= 1 && A >= 1 + 2*G && 3*A >= 3*F && 3*F >= 3*A && F >= 1 + 2*G && F >= 1] (?,1) 4. f0(A,B,C,D,E) -> f2(A,F,C,D,E) [0 >= A] (1,1) Signature: {(f0,5);(f1,5);(f2,5)} Flow Graph: [0->{1,2,3,4},1->{1,2,3},2->{1,2,3},3->{1,2,3},4->{}] + Applied Processor: Looptree + Details: We construct a looptree: P: [0,1,2,3,4] | `- p:[1,2,3] c: [] NO