YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f7(30,30,1,0,2,F,G,H,I) True (1,1) 1. f7(A,B,C,D,E,F,G,H,I) -> f7(A,B,C + D,C,1 + E,C,G,H,I) [-2 + E >= 0 (?,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && B >= E] 2. f7(A,B,C,D,E,F,G,H,I) -> f19(A,B,C,D,E,F,C,C,C) [-2 + E >= 0 (?,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && E >= 1 + B] Signature: {(f0,9);(f19,9);(f7,9)} Flow Graph: [0->{1,2},1->{1,2},2->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2)] * Step 2: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f7(30,30,1,0,2,F,G,H,I) True (1,1) 1. f7(A,B,C,D,E,F,G,H,I) -> f7(A,B,C + D,C,1 + E,C,G,H,I) [-2 + E >= 0 (?,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && B >= E] 2. f7(A,B,C,D,E,F,G,H,I) -> f19(A,B,C,D,E,F,C,C,C) [-2 + E >= 0 (?,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && E >= 1 + B] Signature: {(f0,9);(f19,9);(f7,9)} Flow Graph: [0->{1},1->{1,2},2->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f7(30,30,1,0,2,F,G,H,I) True (1,1) 1. f7(A,B,C,D,E,F,G,H,I) -> f7(A,B,C + D,C,1 + E,C,G,H,I) [-2 + E >= 0 (?,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && B >= E] 2. f7(A,B,C,D,E,F,G,H,I) -> f19(A,B,C,D,E,F,C,C,C) [-2 + E >= 0 (1,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && E >= 1 + B] Signature: {(f0,9);(f19,9);(f7,9)} Flow Graph: [0->{1},1->{1,2},2->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 29 p(f19) = 1 + x2 + -1*x5 p(f7) = 1 + x2 + -1*x5 Following rules are strictly oriented: [-2 + E >= 0 ==> && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && B >= E] f7(A,B,C,D,E,F,G,H,I) = 1 + B + -1*E > B + -1*E = f7(A,B,C + D,C,1 + E,C,G,H,I) Following rules are weakly oriented: True ==> f0(A,B,C,D,E,F,G,H,I) = 29 >= 29 = f7(30,30,1,0,2,F,G,H,I) [-2 + E >= 0 ==> && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && E >= 1 + B] f7(A,B,C,D,E,F,G,H,I) = 1 + B + -1*E >= 1 + B + -1*E = f19(A,B,C,D,E,F,C,C,C) * Step 4: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f7(30,30,1,0,2,F,G,H,I) True (1,1) 1. f7(A,B,C,D,E,F,G,H,I) -> f7(A,B,C + D,C,1 + E,C,G,H,I) [-2 + E >= 0 (29,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && B >= E] 2. f7(A,B,C,D,E,F,G,H,I) -> f19(A,B,C,D,E,F,C,C,C) [-2 + E >= 0 (1,1) && -2 + D + E >= 0 && -3 + C + E >= 0 && -32 + B + E >= 0 && 28 + -1*B + E >= 0 && -32 + A + E >= 0 && 28 + -1*A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -30 + B + D >= 0 && 30 + -1*B + D >= 0 && -30 + A + D >= 0 && 30 + -1*A + D >= 0 && -1 + C >= 0 && -31 + B + C >= 0 && 29 + -1*B + C >= 0 && -31 + A + C >= 0 && 29 + -1*A + C >= 0 && 30 + -1*B >= 0 && A + -1*B >= 0 && 60 + -1*A + -1*B >= 0 && -30 + B >= 0 && -60 + A + B >= 0 && -1*A + B >= 0 && 30 + -1*A >= 0 && -30 + A >= 0 && E >= 1 + B] Signature: {(f0,9);(f19,9);(f7,9)} Flow Graph: [0->{1},1->{1,2},2->{}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(1))