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