MAYBE * Step 1: 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) 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 2: 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,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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank 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,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,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (1,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 2 + -1*x2 p(f2) = 2 + -1*x2 p(f300) = 2 + -1*x2 Following rules are strictly oriented: [0 >= B && 1 >= B && A = 1] ==> f2(A,B,C) = 2 + -1*B > 1 + -1*B = f2(1,1 + B,C) [0 >= A && 1 >= D && B = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1 + A,2,C) [1 >= D && B = 1 && A = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1,2,C) Following rules are weakly oriented: True ==> f1(A,B,C) = 2 + -1*B >= 2 + -1*B = f2(A,B,C) [B >= 2 && 2 >= A && 0 >= A] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [B >= 2 && A = 2] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [B >= 2 && 2 >= D && A = 1] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1,1 + B,C) [1 >= B && 0 >= A && 0 >= B] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [A >= 3 && B >= 2] ==> f2(A,B,C) = 2 + -1*B >= 2 + -1*B = f300(A,B,D) * Step 4: PolyRank 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,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] (2 + B,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (1,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (1,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 2 + -1*x2 p(f2) = 2 + -1*x2 p(f300) = 2 + -1*x2 Following rules are strictly oriented: [1 >= B && A >= 2 && 0 >= B] ==> f2(A,B,C) = 2 + -1*B > 1 + -1*B = f2(1 + A,1 + B,C) [0 >= B && 1 >= B && A = 1] ==> f2(A,B,C) = 2 + -1*B > 1 + -1*B = f2(1,1 + B,C) [0 >= A && 1 >= D && B = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1 + A,2,C) [1 >= D && B = 1 && A = 1] ==> f2(A,B,C) = 2 + -1*B > 0 = f2(1,2,C) Following rules are weakly oriented: True ==> f1(A,B,C) = 2 + -1*B >= 2 + -1*B = f2(A,B,C) [B >= 2 && 2 >= A && 0 >= A] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [B >= 2 && A = 2] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [B >= 2 && 2 >= D && A = 1] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1,1 + B,C) [1 >= B && 0 >= A && 0 >= B] ==> f2(A,B,C) = 2 + -1*B >= 1 + -1*B = f2(1 + A,1 + B,C) [A >= 3 && B >= 2] ==> f2(A,B,C) = 2 + -1*B >= 2 + -1*B = f300(A,B,D) * Step 5: PolyRank 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,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] (2 + B,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (2 + B,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (1,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (1,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 3 + -1*x1 p(f2) = 3 + -1*x1 p(f300) = 3 + -1*x1 Following rules are strictly oriented: [B >= 2 && A = 2] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,1 + B,C) [0 >= A && 1 >= D && B = 1] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,2,C) Following rules are weakly oriented: True ==> f1(A,B,C) = 3 + -1*A >= 3 + -1*A = f2(A,B,C) [B >= 2 && 2 >= A && 0 >= A] ==> f2(A,B,C) = 3 + -1*A >= 2 + -1*A = f2(1 + A,1 + B,C) [B >= 2 && 2 >= D && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,1 + B,C) [1 >= B && A >= 2 && 0 >= B] ==> f2(A,B,C) = 3 + -1*A >= 2 + -1*A = f2(1 + A,1 + B,C) [0 >= B && 1 >= B && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,1 + B,C) [A >= 2 && 1 >= D && B = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 + -1*A = f2(1 + A,2,C) [1 >= D && B = 1 && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,2,C) [A >= 3 && B >= 2] ==> f2(A,B,C) = 3 + -1*A >= 3 + -1*A = f300(A,B,D) * Step 6: PolyRank 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,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] (3 + A,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (2 + B,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (2 + B,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (1,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (1,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f1) = 3 + -1*x1 p(f2) = 3 + -1*x1 p(f300) = 3 + -1*x1 Following rules are strictly oriented: [B >= 2 && 2 >= A && 0 >= A] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,1 + B,C) [B >= 2 && A = 2] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,1 + B,C) [0 >= A && 1 >= D && B = 1] ==> f2(A,B,C) = 3 + -1*A > 2 + -1*A = f2(1 + A,2,C) Following rules are weakly oriented: True ==> f1(A,B,C) = 3 + -1*A >= 3 + -1*A = f2(A,B,C) [B >= 2 && 2 >= D && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,1 + B,C) [1 >= B && A >= 2 && 0 >= B] ==> f2(A,B,C) = 3 + -1*A >= 2 + -1*A = f2(1 + A,1 + B,C) [0 >= B && 1 >= B && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,1 + B,C) [A >= 2 && 1 >= D && B = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 + -1*A = f2(1 + A,2,C) [1 >= D && B = 1 && A = 1] ==> f2(A,B,C) = 3 + -1*A >= 2 = f2(1,2,C) [A >= 3 && B >= 2] ==> f2(A,B,C) = 3 + -1*A >= 3 + -1*A = f300(A,B,D) * Step 7: 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] (3 + A,1) 2. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (1,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] (3 + A,1) 5. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (2 + B,1) 6. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (2 + B,1) 7. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (1,1) 8. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (1,1) 9. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (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: Failing "Open problems left." + Details: Open problems left. MAYBE