MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f6(8,0,14,-1,E,F,G) True (1,1) 1. f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] (?,1) 2. f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B] (?,1) 3. f6(A,B,C,D,E,F,G) -> f6(A,B,-1 + B,I,H,F,G) [C >= B] (?,1) 4. f12(A,B,C,D,E,F,G) -> f6(A,B,-1 + E,D,E,F,G) True (?,1) 5. f12(A,B,C,D,E,F,G) -> f6(A,1 + E,C,D,E,F,G) True (?,1) 6. f6(A,B,C,D,E,F,G) -> f20(A,B,C,D,E,D,D) [B >= 1 + C] (?,1) Signature: {(f0,7);(f12,7);(f20,7);(f6,7)} Flow Graph: [0->{1,2,3,6},1->{4,5},2->{4,5},3->{1,2,3,6},4->{1,2,3,6},5->{1,2,3,6},6->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,6),(3,1),(3,2),(3,3)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f6(8,0,14,-1,E,F,G) True (1,1) 1. f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] (?,1) 2. f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B] (?,1) 3. f6(A,B,C,D,E,F,G) -> f6(A,B,-1 + B,I,H,F,G) [C >= B] (?,1) 4. f12(A,B,C,D,E,F,G) -> f6(A,B,-1 + E,D,E,F,G) True (?,1) 5. f12(A,B,C,D,E,F,G) -> f6(A,1 + E,C,D,E,F,G) True (?,1) 6. f6(A,B,C,D,E,F,G) -> f20(A,B,C,D,E,D,D) [B >= 1 + C] (?,1) Signature: {(f0,7);(f12,7);(f20,7);(f6,7)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{6},4->{1,2,3,6},5->{1,2,3,6},6->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f0(A,B,C,D,E,F,G) -> f6(8,0,14,-1,E,F,G) True f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] f6(A,B,C,D,E,F,G) -> f12(A,B,C,D,I,F,G) [C >= B] f6(A,B,C,D,E,F,G) -> f6(A,B,-1 + B,I,H,F,G) [C >= B] f12(A,B,C,D,E,F,G) -> f6(A,B,-1 + E,D,E,F,G) True f12(A,B,C,D,E,F,G) -> f6(A,1 + E,C,D,E,F,G) True f6(A,B,C,D,E,F,G) -> f20(A,B,C,D,E,D,D) [B >= 1 + C] Signature: {(f0,7);(f12,7);(f20,7);(f6,7)} Rule Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{6},4->{1,2,3,6},5->{1,2,3,6},6->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,B,C,D,E,F,G) -> f6.1(8,0,14,-1,E,F,G) True f0.0(A,B,C,D,E,F,G) -> f6.2(8,0,14,-1,E,F,G) True f0.0(A,B,C,D,E,F,G) -> f6.3(8,0,14,-1,E,F,G) True f6.1(A,B,C,D,E,F,G) -> f12.4(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] f6.1(A,B,C,D,E,F,G) -> f12.5(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] f6.2(A,B,C,D,E,F,G) -> f12.4(A,B,C,D,I,F,G) [C >= B] f6.2(A,B,C,D,E,F,G) -> f12.5(A,B,C,D,I,F,G) [C >= B] f6.3(A,B,C,D,E,F,G) -> f6.6(A,B,-1 + B,I,H,F,G) [C >= B] f12.4(A,B,C,D,E,F,G) -> f6.1(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.2(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.3(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.6(A,B,-1 + E,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.1(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.2(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.3(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.6(A,1 + E,C,D,E,F,G) True f6.6(A,B,C,D,E,F,G) -> f20.7(A,B,C,D,E,D,D) [B >= 1 + C] Signature: {(f0.0,7);(f12.4,7);(f12.5,7);(f20.7,7);(f6.1,7);(f6.2,7);(f6.3,7);(f6.6,7)} Rule Graph: [0->{3,4},1->{5,6},2->{7},3->{8,9,10,11},4->{12,13,14,15},5->{8,9,10,11},6->{12,13,14,15},7->{16},8->{3,4} ,9->{5,6},10->{7},11->{16},12->{3,4},13->{5,6},14->{7},15->{16},16->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f0.0(A,B,C,D,E,F,G) -> f6.1(8,0,14,-1,E,F,G) True f0.0(A,B,C,D,E,F,G) -> f6.2(8,0,14,-1,E,F,G) True f0.0(A,B,C,D,E,F,G) -> f6.3(8,0,14,-1,E,F,G) True f6.1(A,B,C,D,E,F,G) -> f12.4(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] f6.1(A,B,C,D,E,F,G) -> f12.5(A,B,C,D,I,F,G) [C >= B && A >= 1 + H] f6.2(A,B,C,D,E,F,G) -> f12.4(A,B,C,D,I,F,G) [C >= B] f6.2(A,B,C,D,E,F,G) -> f12.5(A,B,C,D,I,F,G) [C >= B] f6.3(A,B,C,D,E,F,G) -> f6.6(A,B,-1 + B,I,H,F,G) [C >= B] f12.4(A,B,C,D,E,F,G) -> f6.1(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.2(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.3(A,B,-1 + E,D,E,F,G) True f12.4(A,B,C,D,E,F,G) -> f6.6(A,B,-1 + E,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.1(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.2(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.3(A,1 + E,C,D,E,F,G) True f12.5(A,B,C,D,E,F,G) -> f6.6(A,1 + E,C,D,E,F,G) True f6.6(A,B,C,D,E,F,G) -> f20.7(A,B,C,D,E,D,D) [B >= 1 + C] f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True f20.7(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True Signature: {(exitus616,7);(f0.0,7);(f12.4,7);(f12.5,7);(f20.7,7);(f6.1,7);(f6.2,7);(f6.3,7);(f6.6,7)} Rule Graph: [0->{3,4},1->{5,6},2->{7},3->{8,9,10,11},4->{12,13,14,15},5->{8,9,10,11},6->{12,13,14,15},7->{16},8->{3,4} ,9->{5,6},10->{7},11->{16},12->{3,4},13->{5,6},14->{7},15->{16},16->{17,18,19,20,21,22,23,24,25}] + 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] | `- p:[3,8,5,9,13,4,12,6] c: [] MAYBE