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