-
Notifications
You must be signed in to change notification settings - Fork 0
/
asserts-h4.txt
115 lines (115 loc) · 3.06 KB
/
asserts-h4.txt
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
h_1_1 == 1
h_2_2 == 3
h_2_3 == 1
h_3_1 == 4
h_3_3 == 5
h_4_1 == 1
h_4_2 == 6
h_4_3 == 7
h_4_4 == 3
And(h_1_1 >= 1, h_1_1 <= 1)
And(h_1_2 >= 1, h_1_2 <= 3)
And(h_1_3 >= 1, h_1_3 <= 3)
And(h_1_4 >= 1, h_1_4 <= 3)
And(h_2_1 >= 1, h_2_1 <= 7)
And(h_2_2 >= 1, h_2_2 <= 7)
And(h_2_3 >= 1, h_2_3 <= 1)
And(h_2_4 >= 1, h_2_4 <= 3)
And(h_3_1 >= 1, h_3_1 <= 7)
And(h_3_2 >= 1, h_3_2 <= 7)
And(h_3_3 >= 1, h_3_3 <= 7)
And(h_3_4 >= 1, h_3_4 <= 3)
And(h_4_1 >= 1, h_4_1 <= 1)
And(h_4_2 >= 1, h_4_2 <= 7)
And(h_4_3 >= 1, h_4_3 <= 7)
And(h_4_4 >= 1, h_4_4 <= 3)
Distinct(h_1_1)
Distinct(h_1_2, h_1_3, h_1_4)
Distinct(h_1_2, h_1_3, h_1_4)
Distinct(h_1_2, h_1_3, h_1_4)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_3)
Distinct(h_2_4, h_3_4, h_4_4)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_4, h_3_4, h_4_4)
Distinct(h_4_1)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_1, h_2_2, h_3_1, h_3_2, h_3_3, h_4_2, h_4_3)
Distinct(h_2_4, h_3_4, h_4_4)
h_2_1 != 1
h_1_2 != 1
Implies(h_1_2 == 1, h_1_3 != 1)
Implies(h_1_2 == 2, h_3_2 != 2)
Implies(h_1_2 == 2, h_1_3 != 2)
Implies(h_1_2 == 2, h_1_4 != 2)
Implies(h_1_2 == 3, h_3_2 != 3)
Implies(h_1_2 == 3, h_1_3 != 3)
Implies(h_1_2 == 3, h_1_4 != 3)
Implies(h_1_3 == 1, h_1_4 != 1)
Implies(h_1_3 == 1, h_1_2 != 1)
Implies(h_1_3 == 2, h_1_4 != 2)
Implies(h_1_3 == 2, h_1_2 != 2)
Implies(h_1_3 == 3, h_1_4 != 3)
Implies(h_1_3 == 3, h_1_2 != 3)
Implies(h_1_4 == 1, h_2_4 != 1)
Implies(h_1_4 == 1, h_1_3 != 1)
Implies(h_1_4 == 2, h_2_4 != 2)
Implies(h_1_4 == 2, h_3_4 != 2)
Implies(h_1_4 == 2, h_1_2 != 2)
Implies(h_1_4 == 2, h_1_3 != 2)
Implies(h_1_4 == 3, h_2_4 != 3)
Implies(h_1_4 == 3, h_3_4 != 3)
Implies(h_1_4 == 3, h_1_2 != 3)
Implies(h_1_4 == 3, h_1_3 != 3)
Implies(h_2_1 == 3, h_2_4 != 3)
Implies(h_2_1 == 4, h_2_4 != 4)
Implies(h_2_1 == 5, h_2_4 != 5)
Implies(h_2_1 == 6, h_2_4 != 6)
Implies(h_2_1 == 7, h_2_4 != 7)
h_3_2 != 3
h_1_2 != 3
h_2_4 != 3
h_2_1 != 3
h_1_3 != 1
h_2_4 != 1
Implies(h_2_4 == 1, h_3_4 != 1)
Implies(h_2_4 == 1, h_1_4 != 1)
Implies(h_2_4 == 2, h_3_4 != 2)
Implies(h_2_4 == 2, h_1_4 != 2)
Implies(h_2_4 == 3, h_3_4 != 3)
Implies(h_2_4 == 3, h_1_4 != 3)
Implies(h_2_4 == 3, h_2_1 != 3)
h_2_1 != 4
h_3_2 != 4
h_3_4 != 4
Implies(h_3_2 == 2, h_1_2 != 2)
Implies(h_3_2 == 2, h_3_4 != 2)
Implies(h_3_2 == 3, h_1_2 != 3)
Implies(h_3_2 == 3, h_3_4 != 3)
Implies(h_3_2 == 4, h_1_2 != 4)
Implies(h_3_2 == 4, h_3_4 != 4)
Implies(h_3_2 == 5, h_1_2 != 5)
Implies(h_3_2 == 5, h_3_4 != 5)
Implies(h_3_2 == 6, h_1_2 != 6)
Implies(h_3_2 == 6, h_3_4 != 6)
Implies(h_3_2 == 7, h_1_2 != 7)
Implies(h_3_2 == 7, h_3_4 != 7)
h_1_3 != 5
h_3_4 != 5
h_3_2 != 5
Implies(h_3_4 == 1, h_2_4 != 1)
Implies(h_3_4 == 2, h_1_4 != 2)
Implies(h_3_4 == 2, h_2_4 != 2)
Implies(h_3_4 == 2, h_3_2 != 2)
Implies(h_3_4 == 3, h_1_4 != 3)
Implies(h_3_4 == 3, h_2_4 != 3)
Implies(h_3_4 == 3, h_3_2 != 3)
h_1_2 != 6
h_3_2 != 6
h_1_3 != 7
h_1_4 != 3
h_2_4 != 3
h_3_4 != 3