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