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