MAYBE * Step 1: UnsatRules MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 9. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && 1 >= B && A = 2*B] (?,1) 10. f2(A,B) -> f2(B,C) [B >= 5 && 0 >= B && B >= 3 && A = 2*B] (?,1) 11. f2(A,B) -> f2(B,C) [B >= 5 && 0 >= B && 1 >= B && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 13. f2(A,B) -> f2(B,C) [3 >= B && B >= 2 && 1 >= B && A = 2*B] (?,1) 14. f2(A,B) -> f2(B,C) [0 >= 3 && B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 17. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 18. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 0 >= 4 + 6*B && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 19. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 21. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) 22. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},1->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23} ,2->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},3->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},4->{8 ,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},5->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},6->{8,9,10 ,11,12,13,14,15,16,17,18,19,20,21,22,23},7->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},8->{8,9,10,11,12 ,13,14,15,16,17,18,19,20,21,22,23},9->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},10->{8,9,10,11,12,13 ,14,15,16,17,18,19,20,21,22,23},11->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},12->{8,9,10,11,12,13,14 ,15,16,17,18,19,20,21,22,23},13->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},14->{8,9,10,11,12,13,14,15 ,16,17,18,19,20,21,22,23},15->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},16->{8,9,10,11,12,13,14,15,16 ,17,18,19,20,21,22,23},17->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},18->{8,9,10,11,12,13,14,15,16,17 ,18,19,20,21,22,23},19->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},20->{8,9,10,11,12,13,14,15,16,17,18 ,19,20,21,22,23},21->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23},22->{8,9,10,11,12,13,14,15,16,17,18,19 ,20,21,22,23},23->{8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [9,10,11,13,14,17,18,19,21,22] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,12,15,16,20,23},1->{8,12,15,16,20,23},2->{8,12,15,16,20,23},3->{8,12,15,16,20,23},4->{8,12,15,16,20 ,23},5->{8,12,15,16,20,23},6->{8,12,15,16,20,23},7->{8,12,15,16,20,23},8->{8,12,15,16,20,23},12->{8,12,15,16 ,20,23},15->{8,12,15,16,20,23},16->{8,12,15,16,20,23},20->{8,12,15,16,20,23},23->{8,12,15,16,20,23}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,15) ,(0,20) ,(0,23) ,(1,8) ,(1,12) ,(1,15) ,(1,16) ,(1,20) ,(1,23) ,(2,8) ,(2,12) ,(2,15) ,(2,16) ,(2,20) ,(2,23) ,(3,8) ,(3,12) ,(3,15) ,(3,16) ,(3,20) ,(3,23) ,(4,8) ,(4,12) ,(4,15) ,(4,20) ,(4,23) ,(5,8) ,(5,12) ,(5,15) ,(5,16) ,(5,20) ,(5,23) ,(6,8) ,(6,12) ,(6,15) ,(6,16) ,(6,20) ,(6,23) ,(7,8) ,(7,12) ,(7,15) ,(7,16) ,(7,20) ,(7,23) ,(8,15) ,(8,20) ,(8,23) ,(12,8) ,(12,12) ,(12,15) ,(12,20) ,(12,23) ,(15,8) ,(15,12) ,(15,16) ,(15,20) ,(16,15) ,(16,20) ,(16,23) ,(20,8) ,(20,12) ,(20,15) ,(20,20) ,(20,23) ,(23,8) ,(23,12) ,(23,16) ,(23,20)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] (1,1) 1. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 2. f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] (1,1) 3. f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] (1,1) 4. f0(A,B) -> f2(3,C) True (1,1) 5. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 6. f0(A,B) -> f2(3,C) [0 >= 3] (1,1) 7. f0(A,B) -> f2(1,C) [0 >= 1] (1,1) 8. f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] (?,1) 12. f2(A,B) -> f2(B,C) [B = 3 && A = 6] (?,1) 15. f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] (?,1) 16. f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 20. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1) 23. f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] (?,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{8,12,16},1->{},2->{},3->{},4->{16},5->{},6->{},7->{},8->{8,12,16},12->{16},15->{15,23},16->{8,12,16} ,20->{16},23->{15,23}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] f0(A,B) -> f2(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] f0(A,B) -> f2(1,C) [0 >= 4 && 0 >= 1] f0(A,B) -> f2(3,C) True f0(A,B) -> f2(1,C) [0 >= 1] f0(A,B) -> f2(3,C) [0 >= 3] f0(A,B) -> f2(1,C) [0 >= 1] f2(A,B) -> f2(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2(A,B) -> f2(B,C) [B = 3 && A = 6] f2(A,B) -> f2(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] f2(A,B) -> f2(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2(A,B) -> f2(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{8,12,16},1->{},2->{},3->{},4->{16},5->{},6->{},7->{},8->{8,12,16},12->{16},15->{15,23},16->{8,12,16} ,20->{16},23->{15,23}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f0.0(A,B) -> f2.8(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.0(A,B) -> f2.12(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.0(A,B) -> f2.16(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.1(A,B) -> f2.24(1,C) [0 >= 4 && 0 >= 1] f0.2(A,B) -> f2.24(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] f0.3(A,B) -> f2.24(1,C) [0 >= 4 && 0 >= 1] f0.4(A,B) -> f2.16(3,C) True f0.5(A,B) -> f2.24(1,C) [0 >= 1] f0.6(A,B) -> f2.24(3,C) [0 >= 3] f0.7(A,B) -> f2.24(1,C) [0 >= 1] f2.8(A,B) -> f2.8(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.8(A,B) -> f2.12(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.8(A,B) -> f2.16(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.12(A,B) -> f2.16(B,C) [B = 3 && A = 6] f2.15(A,B) -> f2.15(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] f2.15(A,B) -> f2.23(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] f2.16(A,B) -> f2.8(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.16(A,B) -> f2.12(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.16(A,B) -> f2.16(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.20(A,B) -> f2.16(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.23(A,B) -> f2.15(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] f2.23(A,B) -> f2.23(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] Signature: {(f0.0,2) ;(f0.1,2) ;(f0.2,2) ;(f0.3,2) ;(f0.4,2) ;(f0.5,2) ;(f0.6,2) ;(f0.7,2) ;(f2.12,2) ;(f2.15,2) ;(f2.16,2) ;(f2.20,2) ;(f2.23,2) ;(f2.24,2) ;(f2.8,2)} Rule Graph: [0->{10,11,12},1->{13},2->{16,17,18},3->{},4->{},5->{},6->{16,17,18},7->{},8->{},9->{},10->{10,11,12} ,11->{13},12->{16,17,18},13->{16,17,18},14->{14,15},15->{20,21},16->{10,11,12},17->{13},18->{16,17,18} ,19->{16,17,18},20->{14,15},21->{20,21}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f0.0(A,B) -> f2.8(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.0(A,B) -> f2.12(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.0(A,B) -> f2.16(C,D) [C >= 1 && C >= 5 && C >= 2 && C >= 3] f0.1(A,B) -> f2.24(1,C) [0 >= 4 && 0 >= 1] f0.2(A,B) -> f2.24(C,D) [C >= 1 && C >= 5 && 0 >= C && C >= 3] f0.3(A,B) -> f2.24(1,C) [0 >= 4 && 0 >= 1] f0.4(A,B) -> f2.16(3,C) True f0.5(A,B) -> f2.24(1,C) [0 >= 1] f0.6(A,B) -> f2.24(3,C) [0 >= 3] f0.7(A,B) -> f2.24(1,C) [0 >= 1] f2.8(A,B) -> f2.8(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.8(A,B) -> f2.12(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.8(A,B) -> f2.16(B,C) [B >= 5 && B >= 2 && B >= 3 && A = 2*B] f2.12(A,B) -> f2.16(B,C) [B = 3 && A = 6] f2.15(A,B) -> f2.15(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] f2.15(A,B) -> f2.23(B,C) [3 >= B && 0 >= B && 1 >= B && A = 2*B] f2.16(A,B) -> f2.8(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.16(A,B) -> f2.12(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.16(A,B) -> f2.16(4 + 6*B,C) [6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.20(A,B) -> f2.16(4 + 6*B,C) [0 >= 1 + 6*B && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] f2.23(A,B) -> f2.15(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] f2.23(A,B) -> f2.23(4 + 6*B,C) [0 >= 1 + 6*B && 0 >= 4 + 6*B && 0 >= 3 + 6*B && A = 1 + 2*B] f2.8(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.15(A,B) -> exitus616(A,B) True f2.15(A,B) -> exitus616(A,B) True f2.23(A,B) -> exitus616(A,B) True f2.23(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.24(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.8(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.12(A,B) -> exitus616(A,B) True f2.16(A,B) -> exitus616(A,B) True Signature: {(exitus616,2) ;(f0.0,2) ;(f0.1,2) ;(f0.2,2) ;(f0.3,2) ;(f0.4,2) ;(f0.5,2) ;(f0.6,2) ;(f0.7,2) ;(f2.12,2) ;(f2.15,2) ;(f2.16,2) ;(f2.20,2) ;(f2.23,2) ;(f2.24,2) ;(f2.8,2)} Rule Graph: [0->{10,11,12},1->{13},2->{16,17,18},3->{45},4->{44},5->{43},6->{16,17,18},7->{35},8->{34},9->{33},10->{10 ,11,12,22,36,46,53,60},11->{13,26,40,50,57,64},12->{16,17,18,24,38,48,55,62},13->{16,17,18,25,39,49,56,63} ,14->{14,15,29},15->{20,21,31},16->{10,11,12,23,37,47,54,61},17->{13,27,41,51,58,65},18->{16,17,18,28,42,52 ,59,66},19->{16,17,18},20->{14,15,30},21->{20,21,32}] + 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] | +- p:[14,20,15,21] c: [] | `- p:[10,16,12,13,11,17,18] c: [] MAYBE