MAYBE * Step 1: UnsatRules MAYBE + Considered Problem: Rules: 0. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) 1. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 2. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 3. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 4. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 1 >= B && A = 1] (?,1) 5. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 6. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && B >= 2] (?,1) 7. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 8. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && B >= 2] (?,1) 9. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 10. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 11. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 0 >= B && 2 >= D && A = 1] (?,1) 12. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 13. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 0 >= B && A = 2] (?,1) 14. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 15. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A && 0 >= B] (?,1) 16. f1(A,B,C) -> f2(A,B,C) True (1,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{},1->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},2->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},3->{0,1,2,3,4 ,5,6,7,8,9,10,11,12,13,14,15},4->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},5->{0,1,2,3,4,5,6,7,8,9,10,11,12,13 ,14,15},6->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},7->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},8->{0,1,2,3,4 ,5,6,7,8,9,10,11,12,13,14,15},9->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},10->{0,1,2,3,4,5,6,7,8,9,10,11,12 ,13,14,15},11->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},12->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},13->{0,1 ,2,3,4,5,6,7,8,9,10,11,12,13,14,15},14->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15},15->{0,1,2,3,4,5,6,7,8,9,10 ,11,12,13,14,15},16->{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [4,6,8,11,13,15] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) 1. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 2. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 3. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 5. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 9. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 10. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 12. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 14. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 16. f1(A,B,C) -> f2(A,B,C) True (1,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{},1->{0,1,2,3,5,7,9,10,12,14},2->{0,1,2,3,5,7,9,10,12,14},3->{0,1,2,3,5,7,9,10,12,14},5->{0,1,2,3,5,7 ,9,10,12,14},7->{0,1,2,3,5,7,9,10,12,14},9->{0,1,2,3,5,7,9,10,12,14},10->{0,1,2,3,5,7,9,10,12,14},12->{0,1,2 ,3,5,7,9,10,12,14},14->{0,1,2,3,5,7,9,10,12,14},16->{0,1,2,3,5,7,9,10,12,14}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,0) ,(1,1) ,(1,2) ,(1,3) ,(1,5) ,(1,7) ,(1,9) ,(1,12) ,(1,14) ,(2,1) ,(2,2) ,(2,3) ,(2,5) ,(2,7) ,(2,9) ,(2,10) ,(2,12) ,(2,14) ,(3,0) ,(3,1) ,(3,2) ,(3,3) ,(3,5) ,(3,7) ,(3,9) ,(3,12) ,(5,0) ,(5,2) ,(5,3) ,(5,7) ,(5,9) ,(5,10) ,(5,12) ,(5,14) ,(7,0) ,(7,1) ,(7,3) ,(7,5) ,(7,9) ,(7,10) ,(7,12) ,(7,14) ,(9,0) ,(9,2) ,(9,7) ,(9,10) ,(9,12) ,(9,14) ,(10,0) ,(10,1) ,(10,2) ,(10,3) ,(10,5) ,(10,7) ,(10,9) ,(10,12) ,(10,14) ,(12,1) ,(12,2) ,(12,3) ,(12,5) ,(12,7) ,(12,9) ,(12,10) ,(12,12) ,(12,14) ,(14,0) ,(14,1) ,(14,2) ,(14,3) ,(14,5) ,(14,7) ,(14,9) ,(14,12)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] (?,1) 1. f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] (?,1) 2. f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] (?,1) 3. f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] (?,1) 5. f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] (?,1) 7. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] (?,1) 9. f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] (?,1) 10. f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] (?,1) 12. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] (?,1) 14. f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] (?,1) 16. f1(A,B,C) -> f2(A,B,C) True (1,1) Signature: {(f1,3);(f2,3);(f300,3)} Flow Graph: [0->{},1->{10},2->{0},3->{10,14},5->{1,5},7->{2,7},9->{1,3,5,9},10->{10},12->{0},14->{10,14},16->{0,1,2,3 ,5,7,9,10,12,14}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f2(A,B,C) -> f300(A,B,D) [A >= 3 && B >= 2] f2(A,B,C) -> f2(1,2,C) [1 >= D && B = 1 && A = 1] f2(A,B,C) -> f2(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] f2(A,B,C) -> f2(1 + A,2,C) [0 >= A && 1 >= D && B = 1] f2(A,B,C) -> f2(1,1 + B,C) [0 >= B && 1 >= B && A = 1] f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] f2(A,B,C) -> f2(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2(A,B,C) -> f2(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && A = 2] f2(A,B,C) -> f2(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] f1(A,B,C) -> f2(A,B,C) True Signature: {(f1,3);(f2,3);(f300,3)} Rule Graph: [0->{},1->{10},2->{0},3->{10,14},5->{1,5},7->{2,7},9->{1,3,5,9},10->{10},12->{0},14->{10,14},16->{0,1,2,3 ,5,7,9,10,12,14}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f2.0(A,B,C) -> f300.17(A,B,D) [A >= 3 && B >= 2] f2.1(A,B,C) -> f2.10(1,2,C) [1 >= D && B = 1 && A = 1] f2.2(A,B,C) -> f2.0(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] f2.3(A,B,C) -> f2.10(1 + A,2,C) [0 >= A && 1 >= D && B = 1] f2.3(A,B,C) -> f2.14(1 + A,2,C) [0 >= A && 1 >= D && B = 1] f2.5(A,B,C) -> f2.1(1,1 + B,C) [0 >= B && 1 >= B && A = 1] f2.5(A,B,C) -> f2.5(1,1 + B,C) [0 >= B && 1 >= B && A = 1] f2.7(A,B,C) -> f2.2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] f2.7(A,B,C) -> f2.7(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] f2.9(A,B,C) -> f2.1(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.3(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.5(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.9(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.10(A,B,C) -> f2.10(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] f2.12(A,B,C) -> f2.0(1 + A,1 + B,C) [B >= 2 && A = 2] f2.14(A,B,C) -> f2.10(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] f2.14(A,B,C) -> f2.14(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] f1.16(A,B,C) -> f2.0(A,B,C) True f1.16(A,B,C) -> f2.1(A,B,C) True f1.16(A,B,C) -> f2.2(A,B,C) True f1.16(A,B,C) -> f2.3(A,B,C) True f1.16(A,B,C) -> f2.5(A,B,C) True f1.16(A,B,C) -> f2.7(A,B,C) True f1.16(A,B,C) -> f2.9(A,B,C) True f1.16(A,B,C) -> f2.10(A,B,C) True f1.16(A,B,C) -> f2.12(A,B,C) True f1.16(A,B,C) -> f2.14(A,B,C) True Signature: {(f1.16,3) ;(f2.0,3) ;(f2.1,3) ;(f2.10,3) ;(f2.12,3) ;(f2.14,3) ;(f2.2,3) ;(f2.3,3) ;(f2.5,3) ;(f2.7,3) ;(f2.9,3) ;(f300.17,3)} Rule Graph: [0->{},1->{13},2->{0},3->{13},4->{15,16},5->{1},6->{5,6},7->{2},8->{7,8},9->{1},10->{3,4},11->{5,6},12->{9 ,10,11,12},13->{13},14->{0},15->{13},16->{15,16},17->{0},18->{1},19->{2},20->{3,4},21->{5,6},22->{7,8} ,23->{9,10,11,12},24->{13},25->{14},26->{15,16}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f2.0(A,B,C) -> f300.17(A,B,D) [A >= 3 && B >= 2] f2.1(A,B,C) -> f2.10(1,2,C) [1 >= D && B = 1 && A = 1] f2.2(A,B,C) -> f2.0(1 + A,2,C) [A >= 2 && 1 >= D && B = 1] f2.3(A,B,C) -> f2.10(1 + A,2,C) [0 >= A && 1 >= D && B = 1] f2.3(A,B,C) -> f2.14(1 + A,2,C) [0 >= A && 1 >= D && B = 1] f2.5(A,B,C) -> f2.1(1,1 + B,C) [0 >= B && 1 >= B && A = 1] f2.5(A,B,C) -> f2.5(1,1 + B,C) [0 >= B && 1 >= B && A = 1] f2.7(A,B,C) -> f2.2(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] f2.7(A,B,C) -> f2.7(1 + A,1 + B,C) [1 >= B && A >= 2 && 0 >= B] f2.9(A,B,C) -> f2.1(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.3(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.5(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.9(A,B,C) -> f2.9(1 + A,1 + B,C) [1 >= B && 0 >= A && 0 >= B] f2.10(A,B,C) -> f2.10(1,1 + B,C) [B >= 2 && 2 >= D && A = 1] f2.12(A,B,C) -> f2.0(1 + A,1 + B,C) [B >= 2 && A = 2] f2.14(A,B,C) -> f2.10(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] f2.14(A,B,C) -> f2.14(1 + A,1 + B,C) [B >= 2 && 2 >= A && 0 >= A] f1.16(A,B,C) -> f2.0(A,B,C) True f1.16(A,B,C) -> f2.1(A,B,C) True f1.16(A,B,C) -> f2.2(A,B,C) True f1.16(A,B,C) -> f2.3(A,B,C) True f1.16(A,B,C) -> f2.5(A,B,C) True f1.16(A,B,C) -> f2.7(A,B,C) True f1.16(A,B,C) -> f2.9(A,B,C) True f1.16(A,B,C) -> f2.10(A,B,C) True f1.16(A,B,C) -> f2.12(A,B,C) True f1.16(A,B,C) -> f2.14(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f300.17(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f300.17(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f300.17(A,B,C) -> exitus616(A,B,C) True f2.10(A,B,C) -> exitus616(A,B,C) True f300.17(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3) ;(f1.16,3) ;(f2.0,3) ;(f2.1,3) ;(f2.10,3) ;(f2.12,3) ;(f2.14,3) ;(f2.2,3) ;(f2.3,3) ;(f2.5,3) ;(f2.7,3) ;(f2.9,3) ;(f300.17,3)} Rule Graph: [0->{28,34,38,40},1->{13},2->{0},3->{13},4->{15,16},5->{1},6->{5,6},7->{2},8->{7,8},9->{1},10->{3,4} ,11->{5,6},12->{9,10,11,12},13->{13,27,29,30,31,32,33,35,36,37,39},14->{0},15->{13},16->{15,16},17->{0} ,18->{1},19->{2},20->{3,4},21->{5,6},22->{7,8},23->{9,10,11,12},24->{13},25->{14},26->{15,16}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40] | +- p:[12] c: [12] | +- p:[8] c: [8] | +- p:[6] c: [6] | +- p:[16] c: [16] | `- p:[13] c: [] MAYBE