MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G) -> f4(A + -1*B,B,C,D,E,F,G) [-1 + -1*B >= 0 && A >= 0] (?,1) 1. f4(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [-1 + -1*B >= 0 && 0 >= 1 + A] (?,1) 2. f5(A,B,C,D,E,F,G) -> f4(A,B,C,D,E,F,G) [0 >= 1 + B] (1,1) 3. f5(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [B >= 0] (1,1) Signature: {(f4,7);(f5,7);(f6,7)} Flow Graph: [0->{0,1},1->{},2->{0,1},3->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,1)] * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G) -> f4(A + -1*B,B,C,D,E,F,G) [-1 + -1*B >= 0 && A >= 0] (?,1) 1. f4(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [-1 + -1*B >= 0 && 0 >= 1 + A] (?,1) 2. f5(A,B,C,D,E,F,G) -> f4(A,B,C,D,E,F,G) [0 >= 1 + B] (1,1) 3. f5(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [B >= 0] (1,1) Signature: {(f4,7);(f5,7);(f6,7)} Flow Graph: [0->{0},1->{},2->{0,1},3->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: Failure MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G) -> f4(A + -1*B,B,C,D,E,F,G) [-1 + -1*B >= 0 && A >= 0] (?,1) 1. f4(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [-1 + -1*B >= 0 && 0 >= 1 + A] (1,1) 2. f5(A,B,C,D,E,F,G) -> f4(A,B,C,D,E,F,G) [0 >= 1 + B] (1,1) 3. f5(A,B,C,D,E,F,G) -> f6(A,B,0,0,0,0,0) [B >= 0] (1,1) Signature: {(f4,7);(f5,7);(f6,7)} Flow Graph: [0->{0},1->{},2->{0,1},3->{}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE