LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
l5 l5 l5: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l22 l22 l22: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l77 l77 l77: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l48 l48 l48: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l18 l18 l18: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l17 l17 l17: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l52 l52 l52: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l35 l35 l35: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l21 l21 l21: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l6 l6 l6: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l76 l76 l76: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l46 l46 l46: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l53 l53 l53: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l19 l19 l19: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l33 l33 l33: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l40 l40 l40: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l47 l47 l47: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l58 l58 l58: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l75 l75 l75: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l37 l37 l37: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l11 l11 l11: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l67 l67 l67: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l79 l79 l79: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l49 l49 l49: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l32 l32 l32: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l63 l63 l63: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l28 l28 l28: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l42 l42 l42: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l2 l2 l2: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l23 l23 l23: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l72 l72 l72: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l4 l4 l4: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l70 l70 l70: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l44 l44 l44: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l51 l51 l51: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l16 l16 l16: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l65 l65 l65: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l30 l30 l30: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l56 l56 l56: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l39 l39 l39: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l43 l43 l43: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l60 l60 l60: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l69 l69 l69: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l1 l1 l1: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l13 l13 l13: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l31 l31 l31: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l9 l9 l9: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l14 l14 l14: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l73 l73 l73: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l25 l25 l25: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l55 l55 l55: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l8 l8 l8: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l74 l74 l74: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l27 l27 l27: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l0 l0 l0: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l12 l12 l12: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l61 l61 l61: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l68 l68 l68: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l26 l26 l26: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l54 l54 l54: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l71 l71 l71: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l7 l7 l7: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l24 l24 l24: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l3 l3 l3: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l41 l41 l41: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l20 l20 l20: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l62 l62 l62: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l45 l45 l45: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l59 l59 l59: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l66 l66 l66: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l57 l57 l57: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l38 l38 l38: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l10 l10 l10: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l36 l36 l36: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l29 l29 l29: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l15 l15 l15: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l64 l64 l64: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l50 l50 l50: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
l78 l78 l78: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15 ∧ x16 = x16 ∧ x17 = x17 ∧ x18 = x18 ∧ x19 = x19 ∧ x20 = x20 ∧ x21 = x21 ∧ x22 = x22 ∧ x23 = x23 ∧ x24 = x24 ∧ x25 = x25 ∧ x26 = x26 ∧ x27 = x27 ∧ x28 = x28 ∧ x29 = x29 ∧ x30 = x30 ∧ x31 = x31 ∧ x32 = x32 ∧ x33 = x33 ∧ x34 = x34 ∧ x35 = x35 ∧ x36 = x36 ∧ x37 = x37 ∧ x38 = x38 ∧ x39 = x39 ∧ x40 = x40 ∧ x41 = x41 ∧ x42 = x42 ∧ x43 = x43 ∧ x44 = x44 ∧ x45 = x45 ∧ x46 = x46 ∧ x47 = x47 ∧ x48 = x48 ∧ x49 = x49 ∧ x50 = x50 ∧ x51 = x51 ∧ x52 = x52 ∧ x53 = x53 ∧ x54 = x54 ∧ x55 = x55 ∧ x56 = x56 ∧ x57 = x57 ∧ x58 = x58 ∧ x59 = x59 ∧ x60 = x60 ∧ x61 = x61 ∧ x62 = x62 ∧ x63 = x63 ∧ x64 = x64 ∧ x65 = x65 ∧ x66 = x66 ∧ x67 = x67
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

2.1 SCC Subproblem 1/3

Here we consider the SCC { l53, l47 }.

2.1.1 Transition Removal

We remove transition 85 using the following ranking functions, which are bounded by 0.

l47: −1 − x14 + x19
l53: −1 − x14 + x19

2.1.2 Transition Removal

We remove transition 86 using the following ranking functions, which are bounded by 0.

l53: 0
l47: −1

2.1.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/3

Here we consider the SCC { l5, l7, l10, l6, l11, l8, l0, l12, l9 }.

2.2.1 Transition Removal

We remove transition 7 using the following ranking functions, which are bounded by 0.

l0: 2⋅x3 + x16
l6: −1 + 2⋅x3 + x16
l5: 2⋅x3 + x16
l12: 2⋅x4 + x17
l11: 2⋅x4 + x17
l10: 2⋅x4 + x17
l9: 2⋅x4 + x17
l8: 2⋅x4 + x17
l7: −1 + 2⋅x3 + x16

2.2.2 Transition Removal

We remove transitions 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8 using the following ranking functions, which are bounded by 0.

l5: 0
l0: −1
l12: 1
l11: 2
l10: 3
l9: 4
l8: 5
l7: 6
l6: 7

2.2.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/3

Here we consider the SCC { l56, l57, l55, l58, l60, l62, l61, l59 }.

2.3.1 Transition Removal

We remove transition 90 using the following ranking functions, which are bounded by 0.

l55: x6
l57: −1 + x6
l56: x6
l62: x7
l61: x7
l60: x7
l59: x7
l58: −1 + x6

2.3.2 Transition Removal

We remove transitions 101, 100, 99, 98, 97, 96, 95, 94, 93, 92, 91 using the following ranking functions, which are bounded by 0.

l56: 0
l55: −1
l62: 1
l61: 2
l60: 3
l59: 4
l58: 5
l57: 6

2.3.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE