MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] (?,1) 1. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] (?,1) 2. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,0,E,F,G,H) [A >= 1 + B] (?,1) 3. f1(A,B,C,D,E,F,G,H) -> f300(A,B,J,D,E,I,G,H) [B >= A] (?,1) 4. f2(A,B,C,D,E,F,G,H) -> f1(A,B,C,D,E,F,J,J) True (1,1) Signature: {(f1,8);(f2,8);(f300,8)} 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. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] (?,1) 1. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] (?,1) 2. f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,0,E,F,G,H) [A >= 1 + B] (?,1) 3. f1(A,B,C,D,E,F,G,H) -> f300(A,B,J,D,E,I,G,H) [B >= A] (?,1) 4. f2(A,B,C,D,E,F,G,H) -> f1(A,B,C,D,E,F,J,J) True (1,1) Signature: {(f1,8);(f2,8);(f300,8)} 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: f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1(A,B,C,D,E,F,G,H) -> f1(A,B,J,0,E,F,G,H) [A >= 1 + B] f1(A,B,C,D,E,F,G,H) -> f300(A,B,J,D,E,I,G,H) [B >= A] f2(A,B,C,D,E,F,G,H) -> f1(A,B,C,D,E,F,J,J) True Signature: {(f1,8);(f2,8);(f300,8)} 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: f1.0(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.0(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.0(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.3(A,B,C,D,E,F,G,H) -> f300.5(A,B,J,D,E,I,G,H) [B >= A] f2.4(A,B,C,D,E,F,G,H) -> f1.0(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.1(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.2(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.3(A,B,C,D,E,F,J,J) True Signature: {(f1.0,8);(f1.1,8);(f1.2,8);(f1.3,8);(f2.4,8);(f300.5,8)} 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: f1.0(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.0(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.0(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,I,K,F,G,H) [I >= 1 && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.1(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,I,K,F,G,H) [0 >= 1 + I && A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.0(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.1(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.2(A,B,C,D,E,F,G,H) -> f1.2(A,B,J,0,E,F,G,H) [A >= 1 + B] f1.3(A,B,C,D,E,F,G,H) -> f300.5(A,B,J,D,E,I,G,H) [B >= A] f2.4(A,B,C,D,E,F,G,H) -> f1.0(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.1(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.2(A,B,C,D,E,F,J,J) True f2.4(A,B,C,D,E,F,G,H) -> f1.3(A,B,C,D,E,F,J,J) True f300.5(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.0(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.1(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True f1.2(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True Signature: {(exitus616,8);(f1.0,8);(f1.1,8);(f1.2,8);(f1.3,8);(f2.4,8);(f300.5,8)} 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