YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 5. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && 0 >= 1 + A && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 7. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && 0 >= 1 + A && A + B >= 2] (?,1) 8. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && B >= 1] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 10. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && B >= 1] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 12. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && A >= 1 && 0 >= 1 + A + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 14. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && A >= 1 && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 17. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && 0 >= 1 + B] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) 19. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && 0 >= 1 + B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},1->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},2->{4,5,6,7 ,8,9,10,11,12,13,14,15,16,17,18,19},3->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},4->{4,5,6,7,8,9,10,11,12 ,13,14,15,16,17,18,19},5->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},6->{4,5,6,7,8,9,10,11,12,13,14,15,16 ,17,18,19},7->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},8->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19} ,9->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},10->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},11->{4,5,6,7 ,8,9,10,11,12,13,14,15,16,17,18,19},12->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},13->{4,5,6,7,8,9,10,11 ,12,13,14,15,16,17,18,19},14->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},15->{4,5,6,7,8,9,10,11,12,13,14,15 ,16,17,18,19},16->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},17->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18 ,19},18->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19},19->{4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [5,7,8,10,12,14,17,19] * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,6,9,11,13,15,16,18},1->{4,6,9,11,13,15,16,18},2->{4,6,9,11,13,15,16,18},3->{4,6,9,11,13,15,16,18} ,4->{4,6,9,11,13,15,16,18},6->{4,6,9,11,13,15,16,18},9->{4,6,9,11,13,15,16,18},11->{4,6,9,11,13,15,16,18} ,13->{4,6,9,11,13,15,16,18},15->{4,6,9,11,13,15,16,18},16->{4,6,9,11,13,15,16,18},18->{4,6,9,11,13,15,16 ,18}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,6) ,(0,9) ,(0,11) ,(0,13) ,(0,15) ,(0,18) ,(1,4) ,(1,11) ,(1,13) ,(1,15) ,(1,16) ,(1,18) ,(2,4) ,(2,6) ,(2,9) ,(2,11) ,(2,15) ,(2,16) ,(3,4) ,(3,6) ,(3,9) ,(3,13) ,(3,16) ,(3,18) ,(4,6) ,(4,9) ,(4,11) ,(4,13) ,(4,15) ,(4,16) ,(4,18) ,(6,4) ,(6,11) ,(6,13) ,(6,15) ,(6,16) ,(6,18) ,(9,4) ,(9,6) ,(9,11) ,(9,13) ,(9,15) ,(9,16) ,(9,18) ,(11,4) ,(11,6) ,(11,9) ,(11,13) ,(11,16) ,(11,18) ,(13,4) ,(13,6) ,(13,9) ,(13,11) ,(13,15) ,(13,16) ,(15,4) ,(15,6) ,(15,9) ,(15,11) ,(15,13) ,(15,16) ,(15,18) ,(16,6) ,(16,9) ,(16,11) ,(16,13) ,(16,15) ,(16,18) ,(18,4) ,(18,6) ,(18,9) ,(18,11) ,(18,13) ,(18,15) ,(18,16)] * Step 3: FromIts YES + Considered Problem: Rules: 0. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) 1. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 2. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 3. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 4. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 9. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 11. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 13. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 15. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 16. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 18. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{4,16},1->{6,9},2->{13,18},3->{11,15},4->{4},6->{6,9},9->{9},11->{11,15},13->{13,18},15->{15},16->{4 ,16},18->{18}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{4,16},1->{6,9},2->{13,18},3->{11,15},4->{4},6->{6,9},9->{9},11->{11,15},13->{13,18},15->{15},16->{4 ,16},18->{18}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,6,9,11,13,15,16,18] | +- p:[11] c: [11] | +- p:[15] c: [15] | +- p:[13] c: [13] | +- p:[18] c: [18] | +- p:[6] c: [6] | +- p:[9] c: [9] | +- p:[16] c: [16] | `- p:[4] c: [4] * Step 5: CloseWith YES + Considered Problem: (Rules: f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{4,16},1->{6,9},2->{13,18},3->{11,15},4->{4},6->{6,9},9->{9},11->{11,15},13->{13,18},15->{15},16->{4 ,16},18->{18}] ,We construct a looptree: P: [0,1,2,3,4,6,9,11,13,15,16,18] | +- p:[11] c: [11] | +- p:[15] c: [15] | +- p:[13] c: [13] | +- p:[18] c: [18] | +- p:[6] c: [6] | +- p:[9] c: [9] | +- p:[16] c: [16] | `- p:[4] c: [4]) + Applied Processor: CloseWith True + Details: () YES