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