summaryrefslogtreecommitdiff
path: root/tex/thesis/implementation/experiments/bubble-output
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/implementation/experiments/bubble-output')
-rw-r--r--tex/thesis/implementation/experiments/bubble-output407
1 files changed, 0 insertions, 407 deletions
diff --git a/tex/thesis/implementation/experiments/bubble-output b/tex/thesis/implementation/experiments/bubble-output
deleted file mode 100644
index 4217fe7..0000000
--- a/tex/thesis/implementation/experiments/bubble-output
+++ /dev/null
@@ -1,407 +0,0 @@
-
- [B10 (ENTRY)]
- Succs (1): B9
-
- [B1]
- 1: k
- 2: [B1.1] (ImplicitCastExpr, LValueToRValue, int)
- 3: return [B1.2];
- Preds (1): B2
- Succs (1): B0
-
- [B2]
- 1: i
- 2: [B2.1] (ImplicitCastExpr, LValueToRValue, int)
- 3: 4
- 4: [B2.2] <= [B2.3]
- T: while [B2.4]
- Preds (2): B3 B9
- Succs (2): B8 B1
-
- [B3]
- Preds (1): B4
- Succs (1): B2
-
- [B4]
- 1: i
- 2: [B4.1] (ImplicitCastExpr, LValueToRValue, int)
- 3: 1
- 4: [B4.2] + [B4.3]
- 5: i
- 6: [B4.5] = [B4.4]
- Preds (1): B5
- Succs (1): B3
-
- [B5]
- 1: j
- 2: [B5.1] (ImplicitCastExpr, LValueToRValue, int)
- 3: 4
- 4: [B5.2] <= [B5.3]
- T: while [B5.4]
- Preds (2): B6 B8
- Succs (2): B7 B4
-
- [B6]
- Preds (1): B7
- Succs (1): B5
-
- [B7]
- 1: j
- 2: [B7.1] (ImplicitCastExpr, LValueToRValue, int)
- 3: 1
- 4: [B7.2] + [B7.3]
- 5: j
- 6: [B7.5] = [B7.4]
- 7: k
- 8: [B7.7] (ImplicitCastExpr, LValueToRValue, int)
- 9: 1
- 10: [B7.8] + [B7.9]
- 11: k
- 12: [B7.11] = [B7.10]
- Preds (1): B5
- Succs (1): B6
-
- [B8]
- 1: 0
- 2: j
- 3: [B8.2] = [B8.1]
- Preds (1): B2
- Succs (1): B5
-
- [B9]
- 1: 0
- 2: int k = 0;
- 3: 0
- 4: int i = 0;
- 5: 0
- 6: int j = 0;
- Preds (1): B10
- Succs (1): B2
-
- [B0 (EXIT)]
- Preds (1): B1
-
-0-10-pre = max(-inf, inf)
-1-10-pre = max(-inf, inf)
-2-10-pre = max(-inf, inf)
-3-10-pre = max(-inf, inf)
-4-10-pre = max(-inf, inf)
-5-10-pre = max(-inf, inf)
-6-10-pre = max(-inf, inf)
-7-10-pre = max(-inf, inf)
-8-10-pre = max(-inf, inf)
-9-10-pre = max(-inf, inf)
-10-10-pre = max(-inf, inf)
-11-10-pre = max(-inf, inf)
-0-9-pre = max(-inf, 0-10-pre)
-1-9-pre = max(-inf, 1-10-pre)
-2-9-pre = max(-inf, 2-10-pre)
-3-9-pre = max(-inf, 3-10-pre)
-4-9-pre = max(-inf, 4-10-pre)
-5-9-pre = max(-inf, 5-10-pre)
-6-9-pre = max(-inf, 6-10-pre)
-7-9-pre = max(-inf, 7-10-pre)
-8-9-pre = max(-inf, 8-10-pre)
-9-9-pre = max(-inf, 9-10-pre)
-10-9-pre = max(-inf, 10-10-pre)
-11-9-pre = max(-inf, 11-10-pre)
-0-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-1-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-2-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-3-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-4-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-5-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-6-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-7-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-8-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-9-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-10-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-11-9-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-9-pre, 1-9-pre, 2-9-pre, 3-9-pre, 4-9-pre, 5-9-pre, 6-9-pre, 7-9-pre, 8-9-pre, 9-9-pre, 10-9-pre, 11-9-pre))
-0-2-pre = max(-inf, 0-9-0, 0-3-pre)
-1-2-pre = max(-inf, 1-9-0, 1-3-pre)
-2-2-pre = max(-inf, 2-9-0, 2-3-pre)
-3-2-pre = max(-inf, 3-9-0, 3-3-pre)
-4-2-pre = max(-inf, 4-9-0, 4-3-pre)
-5-2-pre = max(-inf, 5-9-0, 5-3-pre)
-6-2-pre = max(-inf, 6-9-0, 6-3-pre)
-7-2-pre = max(-inf, 7-9-0, 7-3-pre)
-8-2-pre = max(-inf, 8-9-0, 8-3-pre)
-9-2-pre = max(-inf, 9-9-0, 9-3-pre)
-10-2-pre = max(-inf, 10-9-0, 10-3-pre)
-11-2-pre = max(-inf, 11-9-0, 11-3-pre)
-0-8-pre = max(-inf, min(4, 0-2-pre))
-1-8-pre = max(-inf, 1-2-pre)
-2-8-pre = max(-inf, 2-2-pre)
-3-8-pre = max(-inf, 3-2-pre)
-4-8-pre = max(-inf, 4-2-pre)
-5-8-pre = max(-inf, 5-2-pre)
-6-8-pre = max(-inf, 6-2-pre)
-7-8-pre = max(-inf, 7-2-pre)
-8-8-pre = max(-inf, 8-2-pre)
-9-8-pre = max(-inf, 9-2-pre)
-10-8-pre = max(-inf, 10-2-pre)
-11-8-pre = max(-inf, 11-2-pre)
-0-1-pre = max(-inf, 0-2-pre)
-1-1-pre = max(-inf, min(-5, 1-2-pre))
-2-1-pre = max(-inf, 2-2-pre)
-3-1-pre = max(-inf, 3-2-pre)
-4-1-pre = max(-inf, 4-2-pre)
-5-1-pre = max(-inf, 5-2-pre)
-6-1-pre = max(-inf, 6-2-pre)
-7-1-pre = max(-inf, 7-2-pre)
-8-1-pre = max(-inf, 8-2-pre)
-9-1-pre = max(-inf, 9-2-pre)
-10-1-pre = max(-inf, 10-2-pre)
-11-1-pre = max(-inf, 11-2-pre)
-0-8-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-1-8-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-2-8-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-3-8-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-4-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-5-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-6-8-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-7-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-8-8-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-9-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-10-8-0 = max(-inf, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-11-8-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-0-5-pre = max(-inf, 0-8-0, 0-6-pre)
-1-5-pre = max(-inf, 1-8-0, 1-6-pre)
-2-5-pre = max(-inf, 2-8-0, 2-6-pre)
-3-5-pre = max(-inf, 3-8-0, 3-6-pre)
-4-5-pre = max(-inf, 4-8-0, 4-6-pre)
-5-5-pre = max(-inf, 5-8-0, 5-6-pre)
-6-5-pre = max(-inf, 6-8-0, 6-6-pre)
-7-5-pre = max(-inf, 7-8-0, 7-6-pre)
-8-5-pre = max(-inf, 8-8-0, 8-6-pre)
-9-5-pre = max(-inf, 9-8-0, 9-6-pre)
-10-5-pre = max(-inf, 10-8-0, 10-6-pre)
-11-5-pre = max(-inf, 11-8-0, 11-6-pre)
-0-0-pre = max(-inf, 0-1-pre)
-1-0-pre = max(-inf, 1-1-pre)
-2-0-pre = max(-inf, 2-1-pre)
-3-0-pre = max(-inf, 3-1-pre)
-4-0-pre = max(-inf, 4-1-pre)
-5-0-pre = max(-inf, 5-1-pre)
-6-0-pre = max(-inf, 6-1-pre)
-7-0-pre = max(-inf, 7-1-pre)
-8-0-pre = max(-inf, 8-1-pre)
-9-0-pre = max(-inf, 9-1-pre)
-10-0-pre = max(-inf, 10-1-pre)
-11-0-pre = max(-inf, 11-1-pre)
-0-7-pre = max(-inf, 0-5-pre)
-1-7-pre = max(-inf, 1-5-pre)
-2-7-pre = max(-inf, 2-5-pre)
-3-7-pre = max(-inf, 3-5-pre)
-4-7-pre = max(-inf, min(4, 4-5-pre))
-5-7-pre = max(-inf, 5-5-pre)
-6-7-pre = max(-inf, 6-5-pre)
-7-7-pre = max(-inf, 7-5-pre)
-8-7-pre = max(-inf, 8-5-pre)
-9-7-pre = max(-inf, 9-5-pre)
-10-7-pre = max(-inf, 10-5-pre)
-11-7-pre = max(-inf, 11-5-pre)
-0-4-pre = max(-inf, 0-5-pre)
-1-4-pre = max(-inf, 1-5-pre)
-2-4-pre = max(-inf, 2-5-pre)
-3-4-pre = max(-inf, 3-5-pre)
-4-4-pre = max(-inf, 4-5-pre)
-5-4-pre = max(-inf, min(-5, 5-5-pre))
-6-4-pre = max(-inf, 6-5-pre)
-7-4-pre = max(-inf, 7-5-pre)
-8-4-pre = max(-inf, 8-5-pre)
-9-4-pre = max(-inf, 9-5-pre)
-10-4-pre = max(-inf, 10-5-pre)
-11-4-pre = max(-inf, 11-5-pre)
-0-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-1-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-2-7-0 = max(-inf, add(-1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-3-7-0 = max(-inf, add(-1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-4-7-0 = max(-inf, add(1, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-5-7-0 = max(-inf, add(-1, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-6-7-0 = max(-inf, add(1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-7-7-0 = max(-inf, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-8-7-0 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-9-7-0 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-10-7-0 = max(-inf, add(1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre)))
-11-7-0 = max(-inf, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-0-6-pre = max(-inf, 0-7-0)
-1-6-pre = max(-inf, 1-7-0)
-2-6-pre = max(-inf, 2-7-0)
-3-6-pre = max(-inf, 3-7-0)
-4-6-pre = max(-inf, 4-7-0)
-5-6-pre = max(-inf, 5-7-0)
-6-6-pre = max(-inf, 6-7-0)
-7-6-pre = max(-inf, 7-7-0)
-8-6-pre = max(-inf, 8-7-0)
-9-6-pre = max(-inf, 9-7-0)
-10-6-pre = max(-inf, 10-7-0)
-11-6-pre = max(-inf, 11-7-0)
-0-4-0 = max(-inf, add(1, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-1-4-0 = max(-inf, add(-1, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-2-4-0 = max(-inf, add(1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-3-4-0 = max(-inf, add(1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-4-4-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-5-4-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-6-4-0 = max(-inf, add(-1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-7-4-0 = max(-inf, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-8-4-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-9-4-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-10-4-0 = max(-inf, add(-1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre)))
-11-4-0 = max(-inf, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre))
-0-3-pre = max(-inf, 0-4-0)
-1-3-pre = max(-inf, 1-4-0)
-2-3-pre = max(-inf, 2-4-0)
-3-3-pre = max(-inf, 3-4-0)
-4-3-pre = max(-inf, 4-4-0)
-5-3-pre = max(-inf, 5-4-0)
-6-3-pre = max(-inf, 6-4-0)
-7-3-pre = max(-inf, 7-4-0)
-8-3-pre = max(-inf, 8-4-0)
-9-3-pre = max(-inf, 9-4-0)
-10-3-pre = max(-inf, 10-4-0)
-11-3-pre = max(-inf, 11-4-0)
-
-Block 0:
- i <= 5
- -i <= -5
- i - j <= 0
- i - k <= 0
- j <= 5
- -j <= 0
- j - i <= 4
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 1:
- i <= 5
- -i <= -5
- i - j <= 0
- i - k <= 0
- j <= 5
- -j <= 0
- j - i <= 4
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 2:
- i <= 5
- -i <= 0
- i - j <= 0
- i - k <= 0
- j <= 5
- -j <= 0
- j - i <= 4
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 3:
- i <= 5
- -i <= -1
- i - j <= 0
- i - k <= 0
- j <= 5
- -j <= -5
- j - i <= 4
- j - k <= 0
- k <= inf
- -k <= -5
- k - i <= inf
- k - j <= inf
-Block 4:
- i <= 4
- -i <= 0
- i - j <= 4
- i - k <= 0
- j <= 5
- -j <= -5
- j - i <= 5
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 5:
- i <= 4
- -i <= 0
- i - j <= 4
- i - k <= 0
- j <= 5
- -j <= 0
- j - i <= 5
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 6:
- i <= 4
- -i <= 0
- i - j <= 3
- i - k <= -1
- j <= 5
- -j <= -1
- j - i <= 5
- j - k <= 0
- k <= inf
- -k <= -1
- k - i <= inf
- k - j <= inf
-Block 7:
- i <= 4
- -i <= 0
- i - j <= 4
- i - k <= 0
- j <= 4
- -j <= 0
- j - i <= 5
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 8:
- i <= 4
- -i <= 0
- i - j <= 0
- i - k <= 0
- j <= 5
- -j <= 0
- j - i <= 4
- j - k <= 0
- k <= inf
- -k <= 0
- k - i <= inf
- k - j <= inf
-Block 9:
- i <= inf
- -i <= inf
- i - j <= inf
- i - k <= inf
- j <= inf
- -j <= inf
- j - i <= inf
- j - k <= inf
- k <= inf
- -k <= inf
- k - i <= inf
- k - j <= inf
-Block 10:
- i <= inf
- -i <= inf
- i - j <= inf
- i - k <= inf
- j <= inf
- -j <= inf
- j - i <= inf
- j - k <= inf
- k <= inf
- -k <= inf
- k - i <= inf
- k - j <= inf