YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True (1,1) 1. evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 2. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] (?,1) 3. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] (?,1) 4. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 (?,1) && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] 12. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] 13. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True (?,1) Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12} ,12->{2,3},13->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,5)] * Step 2: FromIts YES + Considered Problem: Rules: 0. evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True (1,1) 1. evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 2. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] (?,1) 3. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] (?,1) 4. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 (?,1) && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] 12. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] 13. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True (?,1) Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,12,11,5,9,7,4,8,6] c: [2,5,11,12] | `- p:[4,9,7,8,6] c: [4,6,7,8,9] * Step 4: CloseWith YES + Considered Problem: (Rules: evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,12,11,5,9,7,4,8,6] c: [2,5,11,12] | `- p:[4,9,7,8,6] c: [4,6,7,8,9]) + Applied Processor: CloseWith True + Details: () YES