MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F) -> f0(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] (?,1) 1. f0(A,B,C,D,E,F) -> f0(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] (?,1) 2. f0(A,B,C,D,E,F) -> f0(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] (?,1) 3. f0(A,B,C,D,E,F) -> f0(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] (?,1) 4. f0(A,B,C,D,E,F) -> f0(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] (?,1) 5. f1(A,B,C,D,E,F) -> f0(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] (1,1) Signature: {(f0,6);(f1,6)} Flow Graph: [0->{0,1,2,3,4},1->{0,1,2,3,4},2->{0,1,2,3,4},3->{0,1,2,3,4},4->{0,1,2,3,4},5->{0,1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,0),(1,1),(2,2),(3,3),(4,4)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F) -> f0(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] (?,1) 1. f0(A,B,C,D,E,F) -> f0(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] (?,1) 2. f0(A,B,C,D,E,F) -> f0(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] (?,1) 3. f0(A,B,C,D,E,F) -> f0(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] (?,1) 4. f0(A,B,C,D,E,F) -> f0(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] (?,1) 5. f1(A,B,C,D,E,F) -> f0(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] (1,1) Signature: {(f0,6);(f1,6)} Flow Graph: [0->{1,2,3,4},1->{0,2,3,4},2->{0,1,3,4},3->{0,1,2,4},4->{0,1,2,3},5->{0,1,2,3,4}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f0(A,B,C,D,E,F) -> f0(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0(A,B,C,D,E,F) -> f0(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0(A,B,C,D,E,F) -> f0(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0(A,B,C,D,E,F) -> f0(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0(A,B,C,D,E,F) -> f0(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f1(A,B,C,D,E,F) -> f0(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] Signature: {(f0,6);(f1,6)} Rule Graph: [0->{1,2,3,4},1->{0,2,3,4},2->{0,1,3,4},3->{0,1,2,4},4->{0,1,2,3},5->{0,1,2,3,4}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,B,C,D,E,F) -> f0.1(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.2(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.3(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.4(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.1(A,B,C,D,E,F) -> f0.0(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.2(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.3(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.4(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.2(A,B,C,D,E,F) -> f0.0(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.1(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.3(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.4(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.3(A,B,C,D,E,F) -> f0.0(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.1(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.2(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.4(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.4(A,B,C,D,E,F) -> f0.0(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.1(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.2(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.3(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f1.5(A,B,C,D,E,F) -> f0.0(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.1(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.2(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.3(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.4(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] Signature: {(f0.0,6);(f0.1,6);(f0.2,6);(f0.3,6);(f0.4,6);(f1.5,6)} Rule Graph: [0->{4,5,6,7},1->{8,9,10,11},2->{12,13,14,15},3->{16,17,18,19},4->{0,1,2,3},5->{8,9,10,11},6->{12,13,14 ,15},7->{16,17,18,19},8->{0,1,2,3},9->{4,5,6,7},10->{12,13,14,15},11->{16,17,18,19},12->{0,1,2,3},13->{4,5,6 ,7},14->{8,9,10,11},15->{16,17,18,19},16->{0,1,2,3},17->{4,5,6,7},18->{8,9,10,11},19->{12,13,14,15},20->{0,1 ,2,3},21->{4,5,6,7},22->{8,9,10,11},23->{12,13,14,15},24->{16,17,18,19}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f0.0(A,B,C,D,E,F) -> f0.1(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.2(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.3(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.0(A,B,C,D,E,F) -> f0.4(-1*A,A + B,A + C,D,E,F) [0 >= 1 + A] f0.1(A,B,C,D,E,F) -> f0.0(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.2(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.3(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.1(A,B,C,D,E,F) -> f0.4(A + B,-1*B,C,B + D,E,F) [0 >= 1 + B] f0.2(A,B,C,D,E,F) -> f0.0(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.1(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.3(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.2(A,B,C,D,E,F) -> f0.4(A,B + D,C,-1*D,D + E,F) [0 >= 1 + D] f0.3(A,B,C,D,E,F) -> f0.0(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.1(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.2(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.3(A,B,C,D,E,F) -> f0.4(A,B,C + E,D + E,-1*E,F) [0 >= 1 + E] f0.4(A,B,C,D,E,F) -> f0.0(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.1(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.2(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f0.4(A,B,C,D,E,F) -> f0.3(A + C,B,-1*C,D,C + E,F) [0 >= 1 + C] f1.5(A,B,C,D,E,F) -> f0.0(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.1(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.2(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.3(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f1.5(A,B,C,D,E,F) -> f0.4(G,H,K,I,J,G + H + I + J + K) [G + H + I + J + K >= 1] f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.1(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.0(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.2(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.4(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f0.3(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True Signature: {(exitus616,6);(f0.0,6);(f0.1,6);(f0.2,6);(f0.3,6);(f0.4,6);(f1.5,6)} Rule Graph: [0->{4,5,6,7,25,45,65,85,105},1->{8,9,10,11,28,48,68,88,108},2->{12,13,14,15,32,52,72,92,112},3->{16,17,18 ,19,36,56,76,96,116},4->{0,1,2,3,26,46,66,86,106},5->{8,9,10,11,30,50,70,90,110},6->{12,13,14,15,34,54,74,94 ,114},7->{16,17,18,19,38,58,78,98,118},8->{0,1,2,3,29,49,69,89,109},9->{4,5,6,7,27,47,67,87,107},10->{12,13 ,14,15,41,61,81,101,121},11->{16,17,18,19,39,59,79,99,119},12->{0,1,2,3,33,53,73,93,113},13->{4,5,6,7,31,51 ,71,91,111},14->{8,9,10,11,40,60,80,100,120},15->{16,17,18,19,43,63,83,103,123},16->{0,1,2,3,37,57,77,97 ,117},17->{4,5,6,7,35,55,75,95,115},18->{8,9,10,11,42,62,82,102,122},19->{12,13,14,15,44,64,84,104,124} ,20->{0,1,2,3},21->{4,5,6,7},22->{8,9,10,11},23->{12,13,14,15},24->{16,17,18,19}] + 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] | `- p:[0,4,9,1,8,5,13,2,12,6,17,3,16,7,11,14,10,18,15,19] c: [] MAYBE