MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f2(A,B,C) -> f300(A,B,E) [A = 0] (?,1) 1. f2(A,B,C) -> f300(0,B,E) [A >= 1] (?,1) 2. f2(A,B,C) -> f300(0,B,E) [0 >= 1 + A] (?,1) 3. f2(A,B,C) -> f2(1 + E,B,C) [D >= 0 && A >= 1] (?,1) 4. f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] (?,1) 6. f2(A,B,C) -> f2(1 + E,B,C) [D >= 2 && 0 >= 1 + A] (?,1) 7. f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] (?,1) 8. f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] (?,1) 9. f3(A,B,C) -> f2(A,B,C) True (1,1) Signature: {(f2,3);(f3,3);(f300,3)} Flow Graph: [0->{},1->{},2->{},3->{0,1,2,3,4,5,6,7,8},4->{0,1,2,3,4,5,6,7,8},5->{0,1,2,3,4,5,6,7,8},6->{0,1,2,3,4,5,6 ,7,8},7->{0,1,2,3,4,5,6,7,8},8->{0,1,2,3,4,5,6,7,8},9->{0,1,2,3,4,5,6,7,8}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,5),(4,8),(5,4),(5,7),(7,5),(7,8),(8,4),(8,7)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f2(A,B,C) -> f300(A,B,E) [A = 0] (?,1) 1. f2(A,B,C) -> f300(0,B,E) [A >= 1] (?,1) 2. f2(A,B,C) -> f300(0,B,E) [0 >= 1 + A] (?,1) 3. f2(A,B,C) -> f2(1 + E,B,C) [D >= 0 && A >= 1] (?,1) 4. f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] (?,1) 5. f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] (?,1) 6. f2(A,B,C) -> f2(1 + E,B,C) [D >= 2 && 0 >= 1 + A] (?,1) 7. f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] (?,1) 8. f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] (?,1) 9. f3(A,B,C) -> f2(A,B,C) True (1,1) Signature: {(f2,3);(f3,3);(f300,3)} Flow Graph: [0->{},1->{},2->{},3->{0,1,2,3,4,5,6,7,8},4->{0,1,2,3,4,6,7},5->{0,1,2,3,5,6,8},6->{0,1,2,3,4,5,6,7,8} ,7->{0,1,2,3,4,6,7},8->{0,1,2,3,5,6,8},9->{0,1,2,3,4,5,6,7,8}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f2(A,B,C) -> f300(A,B,E) [A = 0] f2(A,B,C) -> f300(0,B,E) [A >= 1] f2(A,B,C) -> f300(0,B,E) [0 >= 1 + A] f2(A,B,C) -> f2(1 + E,B,C) [D >= 0 && A >= 1] f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2(A,B,C) -> f2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2(A,B,C) -> f2(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2(A,B,C) -> f2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f3(A,B,C) -> f2(A,B,C) True Signature: {(f2,3);(f3,3);(f300,3)} Rule Graph: [0->{},1->{},2->{},3->{0,1,2,3,4,5,6,7,8},4->{0,1,2,3,4,6,7},5->{0,1,2,3,5,6,8},6->{0,1,2,3,4,5,6,7,8} ,7->{0,1,2,3,4,6,7},8->{0,1,2,3,5,6,8},9->{0,1,2,3,4,5,6,7,8}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f2.0(A,B,C) -> f300.10(A,B,E) [A = 0] f2.1(A,B,C) -> f300.10(0,B,E) [A >= 1] f2.2(A,B,C) -> f300.10(0,B,E) [0 >= 1 + A] f2.3(A,B,C) -> f2.0(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.1(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.2(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.3(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.4(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.5(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.6(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.7(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.8(1 + E,B,C) [D >= 0 && A >= 1] f2.4(A,B,C) -> f2.0(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.1(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.3(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.4(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.6(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.7(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.5(A,B,C) -> f2.0(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.1(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.3(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.5(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.6(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.8(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.6(A,B,C) -> f2.0(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.1(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.2(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.3(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.4(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.5(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.6(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.7(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.8(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.7(A,B,C) -> f2.0(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.1(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.3(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.4(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.6(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.7(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.8(A,B,C) -> f2.0(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.1(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.3(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.5(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.6(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.8(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f3.9(A,B,C) -> f2.0(A,B,C) True f3.9(A,B,C) -> f2.1(A,B,C) True f3.9(A,B,C) -> f2.2(A,B,C) True f3.9(A,B,C) -> f2.3(A,B,C) True f3.9(A,B,C) -> f2.4(A,B,C) True f3.9(A,B,C) -> f2.5(A,B,C) True f3.9(A,B,C) -> f2.6(A,B,C) True f3.9(A,B,C) -> f2.7(A,B,C) True f3.9(A,B,C) -> f2.8(A,B,C) True Signature: {(f2.0,3);(f2.1,3);(f2.2,3);(f2.3,3);(f2.4,3);(f2.5,3);(f2.6,3);(f2.7,3);(f2.8,3);(f3.9,3);(f300.10,3)} Rule Graph: [0->{},1->{},2->{},3->{0},4->{1},5->{2},6->{3,4,5,6,7,8,9,10,11},7->{12,13,14,15,16,17,18},8->{19,20,21,22 ,23,24,25},9->{26,27,28,29,30,31,32,33,34},10->{35,36,37,38,39,40,41},11->{42,43,44,45,46,47,48},12->{0} ,13->{1},14->{2},15->{3,4,5,6,7,8,9,10,11},16->{12,13,14,15,16,17,18},17->{26,27,28,29,30,31,32,33,34} ,18->{35,36,37,38,39,40,41},19->{0},20->{1},21->{2},22->{3,4,5,6,7,8,9,10,11},23->{19,20,21,22,23,24,25} ,24->{26,27,28,29,30,31,32,33,34},25->{42,43,44,45,46,47,48},26->{0},27->{1},28->{2},29->{3,4,5,6,7,8,9,10 ,11},30->{12,13,14,15,16,17,18},31->{19,20,21,22,23,24,25},32->{26,27,28,29,30,31,32,33,34},33->{35,36,37,38 ,39,40,41},34->{42,43,44,45,46,47,48},35->{0},36->{1},37->{2},38->{3,4,5,6,7,8,9,10,11},39->{12,13,14,15,16 ,17,18},40->{26,27,28,29,30,31,32,33,34},41->{35,36,37,38,39,40,41},42->{0},43->{1},44->{2},45->{3,4,5,6,7,8 ,9,10,11},46->{19,20,21,22,23,24,25},47->{26,27,28,29,30,31,32,33,34},48->{42,43,44,45,46,47,48},49->{0} ,50->{1},51->{2},52->{3,4,5,6,7,8,9,10,11},53->{12,13,14,15,16,17,18},54->{19,20,21,22,23,24,25},55->{26,27 ,28,29,30,31,32,33,34},56->{35,36,37,38,39,40,41},57->{42,43,44,45,46,47,48}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f2.0(A,B,C) -> f300.10(A,B,E) [A = 0] f2.1(A,B,C) -> f300.10(0,B,E) [A >= 1] f2.2(A,B,C) -> f300.10(0,B,E) [0 >= 1 + A] f2.3(A,B,C) -> f2.0(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.1(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.2(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.3(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.4(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.5(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.6(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.7(1 + E,B,C) [D >= 0 && A >= 1] f2.3(A,B,C) -> f2.8(1 + E,B,C) [D >= 0 && A >= 1] f2.4(A,B,C) -> f2.0(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.1(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.3(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.4(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.6(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.4(A,B,C) -> f2.7(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && 0 >= B] f2.5(A,B,C) -> f2.0(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.1(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.2(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.3(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.5(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.6(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.5(A,B,C) -> f2.8(-1 + E,B,C) [A >= 1 && 0 >= 2 + D && B >= 1] f2.6(A,B,C) -> f2.0(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.1(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.2(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.3(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.4(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.5(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.6(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.7(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.6(A,B,C) -> f2.8(1 + E,B,C) [D >= 2 && 0 >= 1 + A] f2.7(A,B,C) -> f2.0(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.1(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.3(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.4(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.6(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.7(A,B,C) -> f2.7(-1 + E,B,C) [0 >= 1 + A && 0 >= D && 0 >= B] f2.8(A,B,C) -> f2.0(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.1(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.2(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.3(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.5(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.6(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f2.8(A,B,C) -> f2.8(-1 + E,B,C) [0 >= 1 + A && 0 >= D && B >= 1] f3.9(A,B,C) -> f2.0(A,B,C) True f3.9(A,B,C) -> f2.1(A,B,C) True f3.9(A,B,C) -> f2.2(A,B,C) True f3.9(A,B,C) -> f2.3(A,B,C) True f3.9(A,B,C) -> f2.4(A,B,C) True f3.9(A,B,C) -> f2.5(A,B,C) True f3.9(A,B,C) -> f2.6(A,B,C) True f3.9(A,B,C) -> f2.7(A,B,C) True f3.9(A,B,C) -> f2.8(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True f300.10(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3) ;(f2.0,3) ;(f2.1,3) ;(f2.2,3) ;(f2.3,3) ;(f2.4,3) ;(f2.5,3) ;(f2.6,3) ;(f2.7,3) ;(f2.8,3) ;(f3.9,3) ;(f300.10,3)} Rule Graph: [0->{60,63,66,69,72,75,78,81,84,87,90,93,96,99,102,105,108,111,114,117,120,123,126,129,132,135,138,141,144 ,147,150,153,156,159,162,165,168},1->{59,62,65,68,71,74,77,80,83,86,89,92,95,98,101,104,107,110,113,116,119 ,122,125,128,131,134,137,140,143,146,149,152,155,158,161,164,167},2->{58,61,64,67,70,73,76,79,82,85,88,91,94 ,97,100,103,106,109,112,115,118,121,124,127,130,133,136,139,142,145,148,151,154,157,160,163,166},3->{0} ,4->{1},5->{2},6->{3,4,5,6,7,8,9,10,11},7->{12,13,14,15,16,17,18},8->{19,20,21,22,23,24,25},9->{26,27,28,29 ,30,31,32,33,34},10->{35,36,37,38,39,40,41},11->{42,43,44,45,46,47,48},12->{0},13->{1},14->{2},15->{3,4,5,6 ,7,8,9,10,11},16->{12,13,14,15,16,17,18},17->{26,27,28,29,30,31,32,33,34},18->{35,36,37,38,39,40,41},19->{0} ,20->{1},21->{2},22->{3,4,5,6,7,8,9,10,11},23->{19,20,21,22,23,24,25},24->{26,27,28,29,30,31,32,33,34} ,25->{42,43,44,45,46,47,48},26->{0},27->{1},28->{2},29->{3,4,5,6,7,8,9,10,11},30->{12,13,14,15,16,17,18} ,31->{19,20,21,22,23,24,25},32->{26,27,28,29,30,31,32,33,34},33->{35,36,37,38,39,40,41},34->{42,43,44,45,46 ,47,48},35->{0},36->{1},37->{2},38->{3,4,5,6,7,8,9,10,11},39->{12,13,14,15,16,17,18},40->{26,27,28,29,30,31 ,32,33,34},41->{35,36,37,38,39,40,41},42->{0},43->{1},44->{2},45->{3,4,5,6,7,8,9,10,11},46->{19,20,21,22,23 ,24,25},47->{26,27,28,29,30,31,32,33,34},48->{42,43,44,45,46,47,48},49->{0},50->{1},51->{2},52->{3,4,5,6,7,8 ,9,10,11},53->{12,13,14,15,16,17,18},54->{19,20,21,22,23,24,25},55->{26,27,28,29,30,31,32,33,34},56->{35,36 ,37,38,39,40,41},57->{42,43,44,45,46,47,48}] + 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,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168] | `- p:[6,15,7,22,8,29,9,38,10,45,11,25,23,31,17,16,30,24,46,34,32,40,18,39,33,47,48,41] c: [] MAYBE