MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval0(A,B,C,D) -> eval1(B,B,1,D) True (1,1) 1. eval1(A,B,C,D) -> end(A,B,C,D) [A >= 101] (?,1) 2. eval1(A,B,C,D) -> eval3(A,B,C,D) [100 >= A] (?,1) 3. eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [100 >= A] (?,1) 4. eval3(A,B,C,D) -> eval5(A,B,C,D) [A >= 101] (?,1) 5. eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [C >= 2] (?,1) 6. eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [A >= 101 && C = 1] (?,1) 7. eval7(A,B,C,D) -> eval9(A,B,C,D) [100 >= A] (?,1) 8. eval7(A,B,C,D) -> eval9(A,B,C,D) [2 >= C] (?,1) 9. eval7(A,B,C,D) -> eval9(A,B,C,D) [C >= 0] (?,1) 10. eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [A >= 101] (?,1) 11. eval9(A,B,C,D) -> eval11(A,B,C,D) [100 >= A] (?,1) 12. eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) True (?,1) Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Flow Graph: [0->{1,2},1->{},2->{3,4},3->{3,4},4->{5},5->{6,7,8,9},6->{5},7->{10,11},8->{10,11},9->{10,11},10->{12} ,11->{12},12->{5}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4),(6,5),(7,10)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. eval0(A,B,C,D) -> eval1(B,B,1,D) True (1,1) 1. eval1(A,B,C,D) -> end(A,B,C,D) [A >= 101] (?,1) 2. eval1(A,B,C,D) -> eval3(A,B,C,D) [100 >= A] (?,1) 3. eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [100 >= A] (?,1) 4. eval3(A,B,C,D) -> eval5(A,B,C,D) [A >= 101] (?,1) 5. eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [C >= 2] (?,1) 6. eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [A >= 101 && C = 1] (?,1) 7. eval7(A,B,C,D) -> eval9(A,B,C,D) [100 >= A] (?,1) 8. eval7(A,B,C,D) -> eval9(A,B,C,D) [2 >= C] (?,1) 9. eval7(A,B,C,D) -> eval9(A,B,C,D) [C >= 0] (?,1) 10. eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [A >= 101] (?,1) 11. eval9(A,B,C,D) -> eval11(A,B,C,D) [100 >= A] (?,1) 12. eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) True (?,1) Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Flow Graph: [0->{1,2},1->{},2->{3},3->{3,4},4->{5},5->{6,7,8,9},6->{},7->{11},8->{10,11},9->{10,11},10->{12},11->{12} ,12->{5}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: eval0(A,B,C,D) -> eval1(B,B,1,D) True eval1(A,B,C,D) -> end(A,B,C,D) [A >= 101] eval1(A,B,C,D) -> eval3(A,B,C,D) [100 >= A] eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [100 >= A] eval3(A,B,C,D) -> eval5(A,B,C,D) [A >= 101] eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [C >= 2] eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [A >= 101 && C = 1] eval7(A,B,C,D) -> eval9(A,B,C,D) [100 >= A] eval7(A,B,C,D) -> eval9(A,B,C,D) [2 >= C] eval7(A,B,C,D) -> eval9(A,B,C,D) [C >= 0] eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [A >= 101] eval9(A,B,C,D) -> eval11(A,B,C,D) [100 >= A] eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) True Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Rule Graph: [0->{1,2},1->{},2->{3},3->{3,4},4->{5},5->{6,7,8,9},6->{},7->{11},8->{10,11},9->{10,11},10->{12},11->{12} ,12->{5}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: eval0.0(A,B,C,D) -> eval1.1(B,B,1,D) True eval0.0(A,B,C,D) -> eval1.2(B,B,1,D) True eval1.1(A,B,C,D) -> end.13(A,B,C,D) [A >= 101] eval1.2(A,B,C,D) -> eval3.3(A,B,C,D) [100 >= A] eval3.3(A,B,C,D) -> eval3.3(11 + A,B,1 + C,D) [100 >= A] eval3.3(A,B,C,D) -> eval3.4(11 + A,B,1 + C,D) [100 >= A] eval3.4(A,B,C,D) -> eval5.5(A,B,C,D) [A >= 101] eval5.5(A,B,C,D) -> eval7.6(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.7(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.8(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.9(-10 + A,B,-1 + C,D) [C >= 2] eval7.6(A,B,C,D) -> eval5.13(A,B,C,-10 + A) [A >= 101 && C = 1] eval7.7(A,B,C,D) -> eval9.11(A,B,C,D) [100 >= A] eval7.8(A,B,C,D) -> eval9.10(A,B,C,D) [2 >= C] eval7.8(A,B,C,D) -> eval9.11(A,B,C,D) [2 >= C] eval7.9(A,B,C,D) -> eval9.10(A,B,C,D) [C >= 0] eval7.9(A,B,C,D) -> eval9.11(A,B,C,D) [C >= 0] eval9.10(A,B,C,D) -> eval11.12(-10 + A,B,-1 + C,D) [A >= 101] eval9.11(A,B,C,D) -> eval11.12(A,B,C,D) [100 >= A] eval11.12(A,B,C,D) -> eval5.5(11 + A,B,1 + C,D) True Signature: {(end.13,4) ;(eval0.0,4) ;(eval1.1,4) ;(eval1.2,4) ;(eval11.12,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval5.13,4) ;(eval5.5,4) ;(eval7.6,4) ;(eval7.7,4) ;(eval7.8,4) ;(eval7.9,4) ;(eval9.10,4) ;(eval9.11,4)} Rule Graph: [0->{2},1->{3},2->{},3->{4,5},4->{4,5},5->{6},6->{7,8,9,10},7->{11},8->{12},9->{13,14},10->{15,16},11->{} ,12->{18},13->{17},14->{18},15->{17},16->{18},17->{19},18->{19},19->{7,8,9,10}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: eval0.0(A,B,C,D) -> eval1.1(B,B,1,D) True eval0.0(A,B,C,D) -> eval1.2(B,B,1,D) True eval1.1(A,B,C,D) -> end.13(A,B,C,D) [A >= 101] eval1.2(A,B,C,D) -> eval3.3(A,B,C,D) [100 >= A] eval3.3(A,B,C,D) -> eval3.3(11 + A,B,1 + C,D) [100 >= A] eval3.3(A,B,C,D) -> eval3.4(11 + A,B,1 + C,D) [100 >= A] eval3.4(A,B,C,D) -> eval5.5(A,B,C,D) [A >= 101] eval5.5(A,B,C,D) -> eval7.6(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.7(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.8(-10 + A,B,-1 + C,D) [C >= 2] eval5.5(A,B,C,D) -> eval7.9(-10 + A,B,-1 + C,D) [C >= 2] eval7.6(A,B,C,D) -> eval5.13(A,B,C,-10 + A) [A >= 101 && C = 1] eval7.7(A,B,C,D) -> eval9.11(A,B,C,D) [100 >= A] eval7.8(A,B,C,D) -> eval9.10(A,B,C,D) [2 >= C] eval7.8(A,B,C,D) -> eval9.11(A,B,C,D) [2 >= C] eval7.9(A,B,C,D) -> eval9.10(A,B,C,D) [C >= 0] eval7.9(A,B,C,D) -> eval9.11(A,B,C,D) [C >= 0] eval9.10(A,B,C,D) -> eval11.12(-10 + A,B,-1 + C,D) [A >= 101] eval9.11(A,B,C,D) -> eval11.12(A,B,C,D) [100 >= A] eval11.12(A,B,C,D) -> eval5.5(11 + A,B,1 + C,D) True eval5.13(A,B,C,D) -> exitus616(A,B,C,D) True end.13(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(end.13,4) ;(eval0.0,4) ;(eval1.1,4) ;(eval1.2,4) ;(eval11.12,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval5.13,4) ;(eval5.5,4) ;(eval7.6,4) ;(eval7.7,4) ;(eval7.8,4) ;(eval7.9,4) ;(eval9.10,4) ;(eval9.11,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{21},3->{4,5},4->{4,5},5->{6},6->{7,8,9,10},7->{11},8->{12},9->{13,14},10->{15,16} ,11->{20},12->{18},13->{17},14->{18},15->{17},16->{18},17->{19},18->{19},19->{7,8,9,10}] + 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] | +- p:[4] c: [4] | `- p:[8,19,17,13,9,15,10,18,12,14,16] c: [15] | `- p:[8,19,17,13,9,18,12,14,16,10] c: [] MAYBE