MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(S,T,U,V,W,F,G,H,I,J,K,L,M,N,O,P,Q,R) True (1,1) 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,256,S,T,U,V,W,Y,O,P,Q,R) [G >= 1 + F && X >= 1 && H = 256] (?,1) 2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,S,T,U,V,W,N,O,P,Q,R) [G >= 1 + F && 0 >= H] (?,1) 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f3(A,B,C,D,E,F,G,H,S,T,K,L,M,N,0,0,0,R) [F >= G] (?,1) 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f2(A,B,C,D,E,F,G,H,S,T,U,V,W,Y,H,H,H,X) [H >= 1 && G >= 1 + F && H >= 257] (?,1) 5. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f2(A,B,C,D,E,F,G,H,S,T,U,V,W,Y,H,H,H,X) [H >= 1 && G >= 1 + F && 255 >= H] (?,1) Signature: {(f1,18);(f2,18);(f3,18);(f300,18)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{},4->{},5->{}] + Applied Processor: ArgumentFilter [0,1,2,3,4,8,9,10,11,12,13,14,15,16,17] + Details: We remove following argument positions: [0,1,2,3,4,8,9,10,11,12,13,14,15,16,17]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f300(F,G,H) -> f1(F,G,H) True (1,1) 1. f1(F,G,H) -> f1(F,G,256) [G >= 1 + F && X >= 1 && H = 256] (?,1) 2. f1(F,G,H) -> f1(F,G,H) [G >= 1 + F && 0 >= H] (?,1) 3. f1(F,G,H) -> f3(F,G,H) [F >= G] (?,1) 4. f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && H >= 257] (?,1) 5. f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && 255 >= H] (?,1) Signature: {(f1,18);(f2,18);(f3,18);(f300,18)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{},4->{},5->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3),(1,4),(1,5),(2,1),(2,3),(2,4),(2,5)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f300(F,G,H) -> f1(F,G,H) True (1,1) 1. f1(F,G,H) -> f1(F,G,256) [G >= 1 + F && X >= 1 && H = 256] (?,1) 2. f1(F,G,H) -> f1(F,G,H) [G >= 1 + F && 0 >= H] (?,1) 3. f1(F,G,H) -> f3(F,G,H) [F >= G] (?,1) 4. f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && H >= 257] (?,1) 5. f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && 255 >= H] (?,1) Signature: {(f1,18);(f2,18);(f3,18);(f300,18)} Flow Graph: [0->{1,2,3,4,5},1->{1},2->{2},3->{},4->{},5->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f300(F,G,H) -> f1(F,G,H) True f1(F,G,H) -> f1(F,G,256) [G >= 1 + F && X >= 1 && H = 256] f1(F,G,H) -> f1(F,G,H) [G >= 1 + F && 0 >= H] f1(F,G,H) -> f3(F,G,H) [F >= G] f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && H >= 257] f1(F,G,H) -> f2(F,G,H) [H >= 1 && G >= 1 + F && 255 >= H] Signature: {(f1,18);(f2,18);(f3,18);(f300,18)} Rule Graph: [0->{1,2,3,4,5},1->{1},2->{2},3->{},4->{},5->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f300.0(F,G,H) -> f1.1(F,G,H) True f300.0(F,G,H) -> f1.2(F,G,H) True f300.0(F,G,H) -> f1.3(F,G,H) True f300.0(F,G,H) -> f1.4(F,G,H) True f300.0(F,G,H) -> f1.5(F,G,H) True f1.1(F,G,H) -> f1.1(F,G,256) [G >= 1 + F && X >= 1 && H = 256] f1.2(F,G,H) -> f1.2(F,G,H) [G >= 1 + F && 0 >= H] f1.3(F,G,H) -> f3.6(F,G,H) [F >= G] f1.4(F,G,H) -> f2.6(F,G,H) [H >= 1 && G >= 1 + F && H >= 257] f1.5(F,G,H) -> f2.6(F,G,H) [H >= 1 && G >= 1 + F && 255 >= H] Signature: {(f1.1,3);(f1.2,3);(f1.3,3);(f1.4,3);(f1.5,3);(f2.6,3);(f3.6,3);(f300.0,3)} Rule Graph: [0->{5},1->{6},2->{7},3->{8},4->{9},5->{5},6->{6},7->{},8->{},9->{}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f300.0(F,G,H) -> f1.1(F,G,H) True f300.0(F,G,H) -> f1.2(F,G,H) True f300.0(F,G,H) -> f1.3(F,G,H) True f300.0(F,G,H) -> f1.4(F,G,H) True f300.0(F,G,H) -> f1.5(F,G,H) True f1.1(F,G,H) -> f1.1(F,G,256) [G >= 1 + F && X >= 1 && H = 256] f1.2(F,G,H) -> f1.2(F,G,H) [G >= 1 + F && 0 >= H] f1.3(F,G,H) -> f3.6(F,G,H) [F >= G] f1.4(F,G,H) -> f2.6(F,G,H) [H >= 1 && G >= 1 + F && H >= 257] f1.5(F,G,H) -> f2.6(F,G,H) [H >= 1 && G >= 1 + F && 255 >= H] f2.6(F,G,H) -> exitus616(F,G,H) True f2.6(F,G,H) -> exitus616(F,G,H) True f3.6(F,G,H) -> exitus616(F,G,H) True f1.2(F,G,H) -> exitus616(F,G,H) True f1.1(F,G,H) -> exitus616(F,G,H) True Signature: {(exitus616,3);(f1.1,3);(f1.2,3);(f1.3,3);(f1.4,3);(f1.5,3);(f2.6,3);(f3.6,3);(f300.0,3)} Rule Graph: [0->{5},1->{6},2->{7},3->{8},4->{9},5->{5,14},6->{6,13},7->{12},8->{11},9->{10}] + 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] | +- p:[6] c: [] | `- p:[5] c: [] MAYBE