MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f1(A,B,C) -> f2(A,B,C) True (1,1) 1. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 3. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 4. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 10. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{1,2,3,4,5,6,7,8,9,10},1->{1,2,3,4,5,6,7,8,9,10},2->{1,2,3,4,5,6,7,8,9,10},3->{1,2,3,4,5,6,7,8,9,10} ,4->{1,2,3,4,5,6,7,8,9,10},5->{1,2,3,4,5,6,7,8,9,10},6->{1,2,3,4,5,6,7,8,9,10},7->{1,2,3,4,5,6,7,8,9,10} ,8->{1,2,3,4,5,6,7,8,9,10},9->{1,2,3,4,5,6,7,8,9,10},10->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C) -> f2(A,B,C) True (1,1) 1. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 3. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 4. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 10. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (1,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{1,2,3,4,5,6,7,8,9,10},1->{1,2,3,4,5,6,7,8,9,10},2->{1,2,3,4,5,6,7,8,9,10},3->{1,2,3,4,5,6,7,8,9,10} ,4->{1,2,3,4,5,6,7,8,9,10},5->{1,2,3,4,5,6,7,8,9,10},6->{1,2,3,4,5,6,7,8,9,10},7->{1,2,3,4,5,6,7,8,9,10} ,8->{1,2,3,4,5,6,7,8,9,10},9->{1,2,3,4,5,6,7,8,9,10},10->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,4) ,(1,5) ,(1,6) ,(1,7) ,(1,8) ,(1,9) ,(1,10) ,(2,1) ,(2,2) ,(2,3) ,(2,4) ,(2,5) ,(2,6) ,(2,7) ,(2,8) ,(2,9) ,(3,1) ,(3,2) ,(3,4) ,(3,5) ,(3,6) ,(3,7) ,(3,8) ,(3,9) ,(3,10) ,(4,1) ,(4,2) ,(4,3) ,(4,5) ,(4,8) ,(4,10) ,(5,1) ,(5,2) ,(5,3) ,(5,4) ,(5,6) ,(5,7) ,(5,9) ,(5,10) ,(6,1) ,(6,2) ,(6,3) ,(6,4) ,(6,5) ,(6,7) ,(6,8) ,(6,10) ,(7,2) ,(7,4) ,(7,5) ,(7,6) ,(7,7) ,(7,8) ,(7,9) ,(7,10) ,(8,1) ,(8,2) ,(8,3) ,(8,4) ,(8,5) ,(8,6) ,(8,7) ,(8,8) ,(8,9) ,(9,1) ,(9,2) ,(9,4) ,(9,5) ,(9,6) ,(9,7) ,(9,8) ,(9,9) ,(9,10)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f1(A,B,C) -> f2(A,B,C) True (1,1) 1. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 3. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 4. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 10. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (1,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{1,2,3,4,5,6,7,8,9,10},1->{1,3},2->{10},3->{3},4->{4,6,7,9},5->{5,8},6->{6,9},7->{1,3},8->{10},9->{3} ,10->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C) -> f2(A,B,C) True (1,1) 1. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 3. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 4. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 10. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) 11. f2(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(exitus616,3);(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{1,2,3,4,5,6,7,8,9,10,11},1->{1,2,3,4,5,6,7,8,9,10,11},2->{1,2,3,4,5,6,7,8,9,10,11},3->{1,2,3,4,5,6,7 ,8,9,10,11},4->{1,2,3,4,5,6,7,8,9,10,11},5->{1,2,3,4,5,6,7,8,9,10,11},6->{1,2,3,4,5,6,7,8,9,10,11},7->{1,2,3 ,4,5,6,7,8,9,10,11},8->{1,2,3,4,5,6,7,8,9,10,11},9->{1,2,3,4,5,6,7,8,9,10,11},10->{},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,4) ,(1,5) ,(1,6) ,(1,7) ,(1,8) ,(1,9) ,(1,10) ,(2,1) ,(2,2) ,(2,3) ,(2,4) ,(2,5) ,(2,6) ,(2,7) ,(2,8) ,(2,9) ,(3,1) ,(3,2) ,(3,4) ,(3,5) ,(3,6) ,(3,7) ,(3,8) ,(3,9) ,(3,10) ,(4,1) ,(4,2) ,(4,3) ,(4,5) ,(4,8) ,(4,10) ,(5,1) ,(5,2) ,(5,3) ,(5,4) ,(5,6) ,(5,7) ,(5,9) ,(5,10) ,(6,1) ,(6,2) ,(6,3) ,(6,4) ,(6,5) ,(6,7) ,(6,8) ,(6,10) ,(7,2) ,(7,4) ,(7,5) ,(7,6) ,(7,7) ,(7,8) ,(7,9) ,(7,10) ,(8,1) ,(8,2) ,(8,3) ,(8,4) ,(8,5) ,(8,6) ,(8,7) ,(8,8) ,(8,9) ,(9,1) ,(9,2) ,(9,4) ,(9,5) ,(9,6) ,(9,7) ,(9,8) ,(9,9) ,(9,10)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f1(A,B,C) -> f2(A,B,C) True (1,1) 1. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 3. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 4. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 10. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) 11. f2(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(exitus616,3);(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{1,2,3,4,5,6,7,8,9,10,11},1->{1,3,11},2->{10,11},3->{3,11},4->{4,6,7,9,11},5->{5,8,11},6->{6,9,11} ,7->{1,3,11},8->{10,11},9->{3,11},10->{},11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | +- p:[5] c: [5] | +- p:[4] c: [4] | +- p:[6] c: [6] | +- p:[1] c: [1] | `- p:[3] c: [] MAYBE