No optimization function
Ongoing
My interest is to find only one common solution for a binary integer problem. My problems are like this:
Subject To
A1 : a0 + 9 a1 + 5 a2 - 2 a3 >= 10
A2 : a0 + 9 a1 + 5 a2 - 2 a3 <= 20
A3 : 2 a0 + 3 a1 + 7 a2 + 5 a3 >= 10
A4 : 2 a0 + 3 a1 + 7 a2 + 5 a3 <= 20
A3 : 6 a0 + 9 a1 - 2 a2 + 3 a3 >= 10
A4 : 6 a0 + 9 a1 - 2 a2 + 3 a3 <= 20
A5 : 3 a0 - a1 + 4 a2 + 8 a3 >= 10
A6 : 3 a0 - a1 + 4 a2 + 8 a3 <= 20
Binaries
a0 a1 a2 a3
End
So inequalities are
10 <= linear equation <= 20
However when I have 230 many equations over 115 variables, it is running more than 5 days. How to make it fast. I know in general Integer Programming Problem is difficult but for this type of problem where all bounds are same may be one can get a better idea. Any suggestions?
0
-
Hi,
You could try systematically solving only subparts of your large problem, i.e., instead of using all 230 constraints, try solving it with only 50 first, then 100 etc. to better locate the source of complexity. You could also vary the number of variables.
Could you provide a minimal working example where you observe the slow convergence?
Best regards,
Jaromił0 -
Hi,
Thank you so much for your comments. I see if I take 2*113=226 constraints, it gives the solution very fast.
But can not solve 228 constraints.
Regards,
Santanu
0 -
Hi Santanu,
Could you try solving the 226 constraints problem + 1 of the remaining 4 constraints to see what happens?
Are the 4 remaining constraints somewhat different from the rest? Is it possible that the 4 remaining constraints are (almost) linearly dependent of the 226 constraints?
You could try feeding the solution \(x^*\) of the 226 constraints problem to the 228 and 230 constraints problems as starting point, see MIPStart. \(x^*\) may be feasible to the larger problems or even optimal and speed up convergence.Best regards,
Jaromił0 -
This is a cross-post from https://stackoverflow.com/questions/63764318/no-optimization-function
0 -
Dear Jaromił,
Thank you so much for your help. If we include another constraint
v0 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 + v32 + v33 + v34 + v35 + v36 + v37 + v38 + v39 + v40 + v41 + v42 + v43 + v44 + v45 + v46 + v47 + v48 + v49 + v50 + v51 + v52 + v53 + v54 + v55 + v56 + v57 + v58 + v59 + v60 + v61 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + v69 + v70 + v71 + v72 + v73 + v74 + v75 + v76 + v77 + v78 + v79 + v80 + v81 + v82 + v83 + v84 + v85 + v86 + v87 + v88 + v89 + v90 + v91 + v92 + v94 + v95 + v96 + v97 + v98 + v99 + v100 + v101 + v102 + v103 + v104 + v105 + v106 + v107 + v108 + v109 + v110 + v111 + v112 + v113 + v114 = 57
it becomes faster.
But still I am not able to solve. I run as follows: gurobi_cl ResultFile=Test_115.sol Test_115.lp
Kindly help me.
This is my code.
Subject To
C1: 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 <= 66
D1: 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 >= 63
C2: 2 v1 + 2 v3 + v5 + 2 v6 + 2 v7 + v8 + 2 v9 + v10 + 2 v11 + v12 + 2 v13 + 3 v15 + 3 v16 + v19 + 2 v20 + 5 v21 + v23 + 2 v24 + v27 + v29 + v30 + 3 v31 + v32 + v33 + 2 v34 + 3 v35 + 2 v36 + v37 + v39 + 3 v40 + v42 + v47 + v48 + 2 v49 + 2 v52 + 3 v53 + 2 v54 + v57 + v59 + 3 v61 + v62 + 2 v63 + 3 v66 + v67 + 2 v68 + v69 + v70 + v71 + 2 v72 + 3 v73 + v74 + v75 + v77 + 3 v78 + 2 v80 + v81 + v84 + v86 + 2 v87 + v88 + v89 + v90 + 2 v91 + v92 + v93 + v94 + v95 + v97 + 3 v98 + 3 v101 + v102 + v106 + v108 + 2 v109 + v110 + v111 + 3 v112 + v113 <= 72
D2: 2 v1 + 2 v3 + v5 + 2 v6 + 2 v7 + v8 + 2 v9 + v10 + 2 v11 + v12 + 2 v13 + 3 v15 + 3 v16 + v19 + 2 v20 + 5 v21 + v23 + 2 v24 + v27 + v29 + v30 + 3 v31 + v32 + v33 + 2 v34 + 3 v35 + 2 v36 + v37 + v39 + 3 v40 + v42 + v47 + v48 + 2 v49 + 2 v52 + 3 v53 + 2 v54 + v57 + v59 + 3 v61 + v62 + 2 v63 + 3 v66 + v67 + 2 v68 + v69 + v70 + v71 + 2 v72 + 3 v73 + v74 + v75 + v77 + 3 v78 + 2 v80 + v81 + v84 + v86 + 2 v87 + v88 + v89 + v90 + 2 v91 + v92 + v93 + v94 + v95 + v97 + 3 v98 + 3 v101 + v102 + v106 + v108 + 2 v109 + v110 + v111 + 3 v112 + v113 >= 57
C3: v4 + 3 v5 + v8 + v9 + 3 v10 + 4 v11 + v12 + v13 + 2 v14 + v15 + v16 + 2 v17 + v18 + 4 v19 + v20 + 3 v21 + v22 + v23 + v24 + v25 + v26 + v27 + v29 + 2 v30 + 2 v32 + v33 + v35 + v36 + v37 + v39 + 2 v40 + v41 + v42 + v44 + v47 + 2 v48 + v49 + v50 + v53 + 3 v56 + v57 + v58 + v59 + 2 v60 + v61 + v62 + 2 v63 + 2 v64 + 2 v66 + v67 + v69 + 2 v70 + v72 + 4 v75 + v76 + 2 v78 + 2 v79 + v80 + v82 + 3 v83 + v84 + v85 + v86 + v88 + v89 + 2 v90 + 2 v91 + 2 v92 + v94 + v96 + 2 v97 + 2 v98 + 6 v99 + v100 + v101 + v103 + v104 + v105 + v106 + v108 + v109 + 4 v111 + 2 v113 <= 72
D3: v4 + 3 v5 + v8 + v9 + 3 v10 + 4 v11 + v12 + v13 + 2 v14 + v15 + v16 + 2 v17 + v18 + 4 v19 + v20 + 3 v21 + v22 + v23 + v24 + v25 + v26 + v27 + v29 + 2 v30 + 2 v32 + v33 + v35 + v36 + v37 + v39 + 2 v40 + v41 + v42 + v44 + v47 + 2 v48 + v49 + v50 + v53 + 3 v56 + v57 + v58 + v59 + 2 v60 + v61 + v62 + 2 v63 + 2 v64 + 2 v66 + v67 + v69 + 2 v70 + v72 + 4 v75 + v76 + 2 v78 + 2 v79 + v80 + v82 + 3 v83 + v84 + v85 + v86 + v88 + v89 + 2 v90 + 2 v91 + 2 v92 + v94 + v96 + 2 v97 + 2 v98 + 6 v99 + v100 + v101 + v103 + v104 + v105 + v106 + v108 + v109 + 4 v111 + 2 v113 >= 57
C4: 2 v1 + 2 v3 + v4 + v5 + 2 v7 + v10 + v12 + 5 v13 + v17 + v18 + v19 + 3 v20 + 2 v21 + 2 v22 + 3 v24 + 3 v27 + 3 v28 + 2 v29 + 3 v30 + 2 v31 + v33 + v34 + v35 + v36 + v37 + 2 v38 + 3 v40 + v42 + 2 v44 + v46 + v47 + v49 + v50 + 3 v51 + 2 v52 + 3 v53 + v55 + 2 v56 + 2 v57 + 2 v58 + 2 v59 + 2 v60 + 2 v62 + v64 + 3 v65 + v66 + v67 + v68 + v69 + v71 + 2 v72 + v74 + v75 + v76 + v77 + 4 v79 + v84 + 3 v85 + v86 + v87 + v89 + 2 v90 + v91 + 2 v92 + 2 v94 + 2 v97 + v99 + 3 v100 + v101 + v102 + v103 + 2 v105 + v107 + v109 + 2 v111 + 2 v112 <= 72
D4: 2 v1 + 2 v3 + v4 + v5 + 2 v7 + v10 + v12 + 5 v13 + v17 + v18 + v19 + 3 v20 + 2 v21 + 2 v22 + 3 v24 + 3 v27 + 3 v28 + 2 v29 + 3 v30 + 2 v31 + v33 + v34 + v35 + v36 + v37 + 2 v38 + 3 v40 + v42 + 2 v44 + v46 + v47 + v49 + v50 + 3 v51 + 2 v52 + 3 v53 + v55 + 2 v56 + 2 v57 + 2 v58 + 2 v59 + 2 v60 + 2 v62 + v64 + 3 v65 + v66 + v67 + v68 + v69 + v71 + 2 v72 + v74 + v75 + v76 + v77 + 4 v79 + v84 + 3 v85 + v86 + v87 + v89 + 2 v90 + v91 + 2 v92 + 2 v94 + 2 v97 + v99 + 3 v100 + v101 + v102 + v103 + 2 v105 + v107 + v109 + 2 v111 + 2 v112 >= 57
C5: v2 + v3 + 2 v5 + 3 v7 + v8 + 2 v9 + 4 v10 + v12 + v13 + v16 + v19 + v20 + v22 + 3 v23 + 2 v24 + 2 v25 + 2 v27 + 2 v28 + 3 v29 + v30 + v31 + 2 v32 + v33 + 2 v34 + v35 + v36 + 2 v37 + v39 + 2 v40 + v41 + v42 + v43 + v45 + v46 + v47 + 4 v48 + 2 v50 + 2 v51 + 2 v52 + v53 + 2 v54 + 2 v55 + 2 v58 + v59 + 4 v60 + v63 + 2 v64 + v65 + 2 v66 + v71 + v72 + 2 v73 + 2 v77 + 3 v78 + v79 + v80 + v82 + v83 + v84 + 3 v86 + v87 + v89 + v90 + 2 v91 + 3 v94 + 4 v95 + 3 v96 + v99 + v100 + 2 v101 + 3 v102 + v104 + v105 + v106 + v108 + v111 + 3 v113 <= 72
D5: v2 + v3 + 2 v5 + 3 v7 + v8 + 2 v9 + 4 v10 + v12 + v13 + v16 + v19 + v20 + v22 + 3 v23 + 2 v24 + 2 v25 + 2 v27 + 2 v28 + 3 v29 + v30 + v31 + 2 v32 + v33 + 2 v34 + v35 + v36 + 2 v37 + v39 + 2 v40 + v41 + v42 + v43 + v45 + v46 + v47 + 4 v48 + 2 v50 + 2 v51 + 2 v52 + v53 + 2 v54 + 2 v55 + 2 v58 + v59 + 4 v60 + v63 + 2 v64 + v65 + 2 v66 + v71 + v72 + 2 v73 + 2 v77 + 3 v78 + v79 + v80 + v82 + v83 + v84 + 3 v86 + v87 + v89 + v90 + 2 v91 + 3 v94 + 4 v95 + 3 v96 + v99 + v100 + 2 v101 + 3 v102 + v104 + v105 + v106 + v108 + v111 + 3 v113 >= 57
C6: v1 + 3 v2 + v3 + 2 v4 + 4 v5 + 3 v6 + 2 v8 + v9 + 2 v11 + 2 v13 + v14 + v15 + v16 + v17 + v18 + v20 + v21 + 2 v22 + v23 + 2 v24 + 3 v26 + 2 v27 + 3 v29 + v30 + 3 v32 + v35 + 2 v37 + 2 v38 + 2 v39 + v40 + 4 v42 + 2 v43 + v44 + v46 + v47 + 3 v48 + v49 + 2 v52 + v53 + 2 v54 + v55 + v57 + 2 v58 + 2 v59 + 2 v61 + 2 v62 + 3 v63 + 2 v64 + 2 v66 + v67 + v70 + v71 + v72 + v73 + v76 + 3 v77 + 3 v78 + v79 + v80 + v81 + v82 + 3 v85 + 2 v86 + 2 v89 + 2 v90 + v99 + 3 v100 + 2 v104 + v105 + v106 + 2 v107 + v109 + v110 + v111 + 2 v112 + v114 <= 72
D6: v1 + 3 v2 + v3 + 2 v4 + 4 v5 + 3 v6 + 2 v8 + v9 + 2 v11 + 2 v13 + v14 + v15 + v16 + v17 + v18 + v20 + v21 + 2 v22 + v23 + 2 v24 + 3 v26 + 2 v27 + 3 v29 + v30 + 3 v32 + v35 + 2 v37 + 2 v38 + 2 v39 + v40 + 4 v42 + 2 v43 + v44 + v46 + v47 + 3 v48 + v49 + 2 v52 + v53 + 2 v54 + v55 + v57 + 2 v58 + 2 v59 + 2 v61 + 2 v62 + 3 v63 + 2 v64 + 2 v66 + v67 + v70 + v71 + v72 + v73 + v76 + 3 v77 + 3 v78 + v79 + v80 + v81 + v82 + 3 v85 + 2 v86 + 2 v89 + 2 v90 + v99 + 3 v100 + 2 v104 + v105 + v106 + 2 v107 + v109 + v110 + v111 + 2 v112 + v114 >= 57
C7: 2 v1 + 3 v5 + 2 v6 + 3 v9 + 2 v12 + v14 + v15 + v16 + 3 v18 + v19 + 2 v21 + 2 v24 + v25 + 2 v26 + 2 v27 + v28 + v29 + v33 + 3 v34 + 3 v36 + 2 v37 + 2 v38 + 3 v39 + 2 v40 + 2 v41 + 3 v43 + 2 v45 + v46 + v48 + 3 v49 + 2 v52 + v53 + 2 v54 + 2 v56 + v57 + 2 v58 + 3 v59 + 3 v60 + v61 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + v69 + v70 + 2 v71 + 3 v72 + v73 + v74 + 3 v75 + 2 v76 + v78 + v82 + v83 + v84 + 2 v85 + 2 v86 + 2 v89 + v91 + 2 v92 + v94 + 2 v95 + 2 v96 + 4 v97 + 2 v100 + v103 + v107 + 4 v108 + v109 + v112 + v113 <= 72
D7: 2 v1 + 3 v5 + 2 v6 + 3 v9 + 2 v12 + v14 + v15 + v16 + 3 v18 + v19 + 2 v21 + 2 v24 + v25 + 2 v26 + 2 v27 + v28 + v29 + v33 + 3 v34 + 3 v36 + 2 v37 + 2 v38 + 3 v39 + 2 v40 + 2 v41 + 3 v43 + 2 v45 + v46 + v48 + 3 v49 + 2 v52 + v53 + 2 v54 + 2 v56 + v57 + 2 v58 + 3 v59 + 3 v60 + v61 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + v69 + v70 + 2 v71 + 3 v72 + v73 + v74 + 3 v75 + 2 v76 + v78 + v82 + v83 + v84 + 2 v85 + 2 v86 + 2 v89 + v91 + 2 v92 + v94 + 2 v95 + 2 v96 + 4 v97 + 2 v100 + v103 + v107 + 4 v108 + v109 + v112 + v113 >= 57
C8: 2 v1 + 2 v3 + 3 v4 + 3 v8 + 2 v9 + 3 v10 + v11 + v12 + v13 + v14 + 4 v15 + v17 + v19 + 2 v21 + 2 v22 + v24 + v25 + 3 v26 + v27 + v28 + v29 + 3 v31 + v32 + 3 v35 + v37 + 2 v39 + 2 v41 + 4 v43 + v44 + 2 v47 + v49 + v50 + 2 v51 + 2 v52 + v53 + 2 v55 + v58 + 2 v59 + 2 v60 + 2 v62 + v63 + v64 + v65 + v66 + v67 + 2 v68 + v69 + v71 + 2 v72 + 2 v73 + v74 + 2 v75 + v76 + 2 v80 + v81 + v83 + 2 v84 + 4 v85 + 3 v86 + v87 + 2 v88 + v91 + v92 + v94 + 2 v95 + 3 v96 + v98 + 2 v99 + v102 + v103 + 3 v105 + v107 + v109 + 2 v111 + 2 v112 + v113 + v114 <= 72
D8: 2 v1 + 2 v3 + 3 v4 + 3 v8 + 2 v9 + 3 v10 + v11 + v12 + v13 + v14 + 4 v15 + v17 + v19 + 2 v21 + 2 v22 + v24 + v25 + 3 v26 + v27 + v28 + v29 + 3 v31 + v32 + 3 v35 + v37 + 2 v39 + 2 v41 + 4 v43 + v44 + 2 v47 + v49 + v50 + 2 v51 + 2 v52 + v53 + 2 v55 + v58 + 2 v59 + 2 v60 + 2 v62 + v63 + v64 + v65 + v66 + v67 + 2 v68 + v69 + v71 + 2 v72 + 2 v73 + v74 + 2 v75 + v76 + 2 v80 + v81 + v83 + 2 v84 + 4 v85 + 3 v86 + v87 + 2 v88 + v91 + v92 + v94 + 2 v95 + 3 v96 + v98 + 2 v99 + v102 + v103 + 3 v105 + v107 + v109 + 2 v111 + 2 v112 + v113 + v114 >= 57
C9: v1 + v2 + v4 + 2 v5 + 3 v7 + 2 v8 + v10 + 2 v11 + 2 v12 + v15 + 2 v17 + v18 + v19 + v20 + v22 + v23 + 2 v24 + 3 v25 + v28 + 2 v29 + 2 v30 + 2 v31 + v33 + v34 + 2 v35 + 2 v36 + v38 + 2 v39 + 4 v41 + v42 + 3 v43 + 2 v44 + v45 + 3 v48 + 2 v50 + 2 v52 + 2 v53 + v55 + v56 + 2 v57 + v58 + v59 + v60 + v61 + 3 v62 + v63 + v64 + 2 v66 + v67 + v68 + 4 v71 + 2 v72 + v74 + v76 + 2 v77 + v79 + 3 v81 + v82 + v83 + v85 + v87 + v88 + 4 v89 + 4 v92 + 2 v94 + 2 v95 + v97 + 4 v98 + v99 + v100 + v101 + v104 + 2 v106 + v109 + v110 + 2 v111 + 2 v112 <= 72
D9: v1 + v2 + v4 + 2 v5 + 3 v7 + 2 v8 + v10 + 2 v11 + 2 v12 + v15 + 2 v17 + v18 + v19 + v20 + v22 + v23 + 2 v24 + 3 v25 + v28 + 2 v29 + 2 v30 + 2 v31 + v33 + v34 + 2 v35 + 2 v36 + v38 + 2 v39 + 4 v41 + v42 + 3 v43 + 2 v44 + v45 + 3 v48 + 2 v50 + 2 v52 + 2 v53 + v55 + v56 + 2 v57 + v58 + v59 + v60 + v61 + 3 v62 + v63 + v64 + 2 v66 + v67 + v68 + 4 v71 + 2 v72 + v74 + v76 + 2 v77 + v79 + 3 v81 + v82 + v83 + v85 + v87 + v88 + 4 v89 + 4 v92 + 2 v94 + 2 v95 + v97 + 4 v98 + v99 + v100 + v101 + v104 + 2 v106 + v109 + v110 + 2 v111 + 2 v112 >= 57
C10: 2 v1 + v2 + 2 v4 + v5 + 3 v6 + 2 v7 + 3 v10 + v11 + v12 + 3 v14 + 2 v16 + 2 v17 + v18 + 3 v20 + 2 v21 + v22 + 2 v23 + 3 v24 + 2 v25 + v27 + v29 + v30 + v31 + 3 v32 + v33 + 2 v34 + 2 v36 + v37 + v38 + v42 + 3 v43 + v45 + v47 + v49 + v50 + v51 + v52 + 3 v53 + 2 v54 + 2 v55 + v56 + v57 + 4 v58 + v59 + v60 + 2 v61 + 2 v62 + v63 + 2 v66 + v67 + 2 v68 + 5 v69 + v70 + v71 + v72 + v75 + v76 + v77 + 2 v82 + 2 v83 + 5 v84 + 2 v85 + v87 + v88 + v89 + 2 v90 + v92 + 2 v94 + v95 + v96 + v98 + v99 + v102 + v105 + v106 + 2 v107 + 2 v110 + v111 + v113 <= 72
D10: 2 v1 + v2 + 2 v4 + v5 + 3 v6 + 2 v7 + 3 v10 + v11 + v12 + 3 v14 + 2 v16 + 2 v17 + v18 + 3 v20 + 2 v21 + v22 + 2 v23 + 3 v24 + 2 v25 + v27 + v29 + v30 + v31 + 3 v32 + v33 + 2 v34 + 2 v36 + v37 + v38 + v42 + 3 v43 + v45 + v47 + v49 + v50 + v51 + v52 + 3 v53 + 2 v54 + 2 v55 + v56 + v57 + 4 v58 + v59 + v60 + 2 v61 + 2 v62 + v63 + 2 v66 + v67 + 2 v68 + 5 v69 + v70 + v71 + v72 + v75 + v76 + v77 + 2 v82 + 2 v83 + 5 v84 + 2 v85 + v87 + v88 + v89 + 2 v90 + v92 + 2 v94 + v95 + v96 + v98 + v99 + v102 + v105 + v106 + 2 v107 + 2 v110 + v111 + v113 >= 57
C11: v1 + 3 v2 + v3 + 4 v4 + 3 v7 + v8 + 3 v9 + 4 v12 + v15 + v16 + v17 + 3 v18 + v19 + 3 v20 + 3 v21 + v22 + v23 + v24 + v25 + v28 + v31 + v32 + 2 v34 + 2 v36 + v37 + v38 + 2 v39 + 3 v40 + 2 v41 + 2 v43 + v44 + 2 v47 + 3 v48 + v54 + v56 + v57 + v58 + 2 v60 + 2 v61 + v63 + v64 + 2 v67 + 3 v68 + v69 + 2 v70 + 2 v71 + v72 + 2 v73 + 2 v74 + v77 + v78 + 4 v79 + 3 v80 + v81 + v82 + 3 v83 + 2 v85 + v86 + v87 + v88 + 3 v90 + v94 + v95 + v96 + v97 + v99 + 2 v100 + v102 + 2 v104 + 2 v105 + v106 + 2 v107 + v109 + v110 + 2 v111 + v112 + v113 <= 72
D11: v1 + 3 v2 + v3 + 4 v4 + 3 v7 + v8 + 3 v9 + 4 v12 + v15 + v16 + v17 + 3 v18 + v19 + 3 v20 + 3 v21 + v22 + v23 + v24 + v25 + v28 + v31 + v32 + 2 v34 + 2 v36 + v37 + v38 + 2 v39 + 3 v40 + 2 v41 + 2 v43 + v44 + 2 v47 + 3 v48 + v54 + v56 + v57 + v58 + 2 v60 + 2 v61 + v63 + v64 + 2 v67 + 3 v68 + v69 + 2 v70 + 2 v71 + v72 + 2 v73 + 2 v74 + v77 + v78 + 4 v79 + 3 v80 + v81 + v82 + 3 v83 + 2 v85 + v86 + v87 + v88 + 3 v90 + v94 + v95 + v96 + v97 + v99 + 2 v100 + v102 + 2 v104 + 2 v105 + v106 + 2 v107 + v109 + v110 + 2 v111 + v112 + v113 >= 57
C12: 2 v1 + 4 v2 + 2 v5 + v7 + 2 v8 + v9 + v13 + v14 + v15 + v16 + 2 v17 + v18 + 3 v19 + 2 v20 + 2 v21 + 2 v22 + 2 v23 + 2 v24 + v25 + 3 v26 + 3 v30 + 4 v31 + 2 v33 + v34 + v35 + v37 + v38 + v39 + v40 + v42 + 4 v43 + 2 v45 + v46 + v49 + 3 v50 + v51 + v53 + 2 v54 + 3 v55 + 2 v57 + v58 + v59 + v60 + v61 + v62 + 2 v63 + 4 v65 + 2 v66 + v67 + 2 v68 + 2 v70 + v71 + v73 + v74 + v76 + 2 v78 + 2 v79 + v80 + 4 v82 + 3 v83 + 2 v86 + v89 + v90 + v92 + v93 + v94 + v95 + v96 + 2 v97 + v98 + 2 v99 + v100 + v101 + v102 + v103 + v105 + v108 + v109 + v112 + v113 <= 72
D12: 2 v1 + 4 v2 + 2 v5 + v7 + 2 v8 + v9 + v13 + v14 + v15 + v16 + 2 v17 + v18 + 3 v19 + 2 v20 + 2 v21 + 2 v22 + 2 v23 + 2 v24 + v25 + 3 v26 + 3 v30 + 4 v31 + 2 v33 + v34 + v35 + v37 + v38 + v39 + v40 + v42 + 4 v43 + 2 v45 + v46 + v49 + 3 v50 + v51 + v53 + 2 v54 + 3 v55 + 2 v57 + v58 + v59 + v60 + v61 + v62 + 2 v63 + 4 v65 + 2 v66 + v67 + 2 v68 + 2 v70 + v71 + v73 + v74 + v76 + 2 v78 + 2 v79 + v80 + 4 v82 + 3 v83 + 2 v86 + v89 + v90 + v92 + v93 + v94 + v95 + v96 + 2 v97 + v98 + 2 v99 + v100 + v101 + v102 + v103 + v105 + v108 + v109 + v112 + v113 >= 57
C13: v1 + v2 + v3 + v4 + 2 v6 + v7 + 2 v8 + v9 + 4 v10 + v13 + v14 + 2 v15 + 3 v17 + v18 + v21 + v22 + v23 + 2 v24 + 2 v25 + v26 + v27 + v28 + v29 + v30 + 2 v32 + 2 v33 + v34 + 2 v35 + 2 v37 + v38 + 2 v40 + 4 v41 + v43 + v45 + 4 v46 + 3 v48 + 2 v49 + v50 + v51 + v52 + v53 + v54 + 2 v56 + 4 v57 + 2 v58 + 2 v61 + v64 + v66 + v67 + 2 v68 + 2 v70 + v72 + v73 + 2 v74 + v75 + v76 + v77 + v78 + v79 + v82 + v83 + v84 + 3 v85 + v87 + v89 + 2 v90 + v91 + 2 v92 + 2 v93 + 2 v95 + v96 + v99 + 2 v100 + 2 v101 + 2 v103 + v104 + 3 v105 + v106 + v107 + 2 v108 + v109 + v110 + v111 + v112 <= 72
D13: v1 + v2 + v3 + v4 + 2 v6 + v7 + 2 v8 + v9 + 4 v10 + v13 + v14 + 2 v15 + 3 v17 + v18 + v21 + v22 + v23 + 2 v24 + 2 v25 + v26 + v27 + v28 + v29 + v30 + 2 v32 + 2 v33 + v34 + 2 v35 + 2 v37 + v38 + 2 v40 + 4 v41 + v43 + v45 + 4 v46 + 3 v48 + 2 v49 + v50 + v51 + v52 + v53 + v54 + 2 v56 + 4 v57 + 2 v58 + 2 v61 + v64 + v66 + v67 + 2 v68 + 2 v70 + v72 + v73 + 2 v74 + v75 + v76 + v77 + v78 + v79 + v82 + v83 + v84 + 3 v85 + v87 + v89 + 2 v90 + v91 + 2 v92 + 2 v93 + 2 v95 + v96 + v99 + 2 v100 + 2 v101 + 2 v103 + v104 + 3 v105 + v106 + v107 + 2 v108 + v109 + v110 + v111 + v112 >= 57
C14: 2 v1 + v2 + 5 v3 + v4 + 2 v5 + v7 + v11 + v12 + v14 + 2 v15 + 2 v16 + 2 v17 + v18 + 2 v19 + 2 v20 + 2 v23 + 2 v24 + v25 + v26 + v28 + 3 v29 + v30 + v31 + v32 + v33 + v34 + v35 + v36 + 3 v37 + 3 v38 + 2 v40 + 2 v41 + v44 + v45 + v46 + 2 v47 + v48 + 2 v49 + 2 v50 + v51 + v54 + 3 v55 + v56 + v57 + v59 + v62 + 2 v65 + 2 v66 + 3 v67 + 5 v69 + 2 v70 + v71 + 2 v72 + 2 v73 + 2 v75 + v76 + 3 v78 + v79 + 2 v80 + 2 v81 + v83 + 2 v85 + v86 + v87 + 2 v89 + v92 + 4 v95 + v98 + 2 v99 + v100 + 2 v104 + 2 v105 + 2 v106 + v107 + 2 v108 + v111 + v112 <= 72
D14: 2 v1 + v2 + 5 v3 + v4 + 2 v5 + v7 + v11 + v12 + v14 + 2 v15 + 2 v16 + 2 v17 + v18 + 2 v19 + 2 v20 + 2 v23 + 2 v24 + v25 + v26 + v28 + 3 v29 + v30 + v31 + v32 + v33 + v34 + v35 + v36 + 3 v37 + 3 v38 + 2 v40 + 2 v41 + v44 + v45 + v46 + 2 v47 + v48 + 2 v49 + 2 v50 + v51 + v54 + 3 v55 + v56 + v57 + v59 + v62 + 2 v65 + 2 v66 + 3 v67 + 5 v69 + 2 v70 + v71 + 2 v72 + 2 v73 + 2 v75 + v76 + 3 v78 + v79 + 2 v80 + 2 v81 + v83 + 2 v85 + v86 + v87 + 2 v89 + v92 + 4 v95 + v98 + 2 v99 + v100 + 2 v104 + 2 v105 + 2 v106 + v107 + 2 v108 + v111 + v112 >= 57
C15: 2 v2 + v5 + v6 + v7 + 3 v9 + v11 + v12 + v13 + 2 v14 + 4 v15 + v17 + v19 + v22 + 2 v23 + 2 v25 + v26 + 4 v29 + v30 + 2 v32 + 2 v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + 3 v40 + v41 + v42 + v43 + v44 + v46 + v49 + 3 v50 + 2 v51 + 2 v52 + v53 + 2 v54 + 2 v56 + v57 + 2 v58 + 2 v59 + v60 + v61 + 5 v62 + v64 + 2 v65 + 2 v67 + v68 + v69 + 2 v70 + v72 + 3 v73 + v74 + v77 + v78 + v79 + v80 + 3 v81 + 3 v83 + v84 + v85 + v86 + 2 v87 + v88 + 4 v90 + v91 + 2 v92 + 2 v94 + 2 v96 + 3 v97 + v99 + v101 + v103 + v104 + v106 + 2 v107 + v110 + v112 + v113 <= 72
D15: 2 v2 + v5 + v6 + v7 + 3 v9 + v11 + v12 + v13 + 2 v14 + 4 v15 + v17 + v19 + v22 + 2 v23 + 2 v25 + v26 + 4 v29 + v30 + 2 v32 + 2 v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + 3 v40 + v41 + v42 + v43 + v44 + v46 + v49 + 3 v50 + 2 v51 + 2 v52 + v53 + 2 v54 + 2 v56 + v57 + 2 v58 + 2 v59 + v60 + v61 + 5 v62 + v64 + 2 v65 + 2 v67 + v68 + v69 + 2 v70 + v72 + 3 v73 + v74 + v77 + v78 + v79 + v80 + 3 v81 + 3 v83 + v84 + v85 + v86 + 2 v87 + v88 + 4 v90 + v91 + 2 v92 + 2 v94 + 2 v96 + 3 v97 + v99 + v101 + v103 + v104 + v106 + 2 v107 + v110 + v112 + v113 >= 57
C16: 3 v1 + v2 + v5 + v6 + 4 v7 + v8 + v10 + v11 + 2 v12 + 2 v13 + 4 v14 + 2 v15 + v17 + v18 + v19 + v21 + v22 + v24 + v25 + 2 v26 + 2 v27 + 3 v29 + v30 + 2 v31 + v32 + 2 v33 + 2 v36 + v37 + v39 + v40 + 2 v41 + 2 v42 + 2 v43 + 3 v45 + 2 v46 + v48 + v49 + v50 + v51 + 2 v52 + v53 + v55 + 2 v56 + v58 + v59 + v60 + v61 + v64 + 2 v65 + v66 + v67 + 3 v68 + 2 v69 + 3 v71 + v72 + v73 + 2 v75 + 2 v78 + v79 + 3 v80 + v82 + v84 + v86 + v87 + 2 v88 + 2 v89 + 3 v90 + 4 v91 + v95 + v99 + v100 + 2 v103 + 5 v104 + v105 + 3 v109 + v110 + v111 + v112 + v113 <= 72
D16: 3 v1 + v2 + v5 + v6 + 4 v7 + v8 + v10 + v11 + 2 v12 + 2 v13 + 4 v14 + 2 v15 + v17 + v18 + v19 + v21 + v22 + v24 + v25 + 2 v26 + 2 v27 + 3 v29 + v30 + 2 v31 + v32 + 2 v33 + 2 v36 + v37 + v39 + v40 + 2 v41 + 2 v42 + 2 v43 + 3 v45 + 2 v46 + v48 + v49 + v50 + v51 + 2 v52 + v53 + v55 + 2 v56 + v58 + v59 + v60 + v61 + v64 + 2 v65 + v66 + v67 + 3 v68 + 2 v69 + 3 v71 + v72 + v73 + 2 v75 + 2 v78 + v79 + 3 v80 + v82 + v84 + v86 + v87 + 2 v88 + 2 v89 + 3 v90 + 4 v91 + v95 + v99 + v100 + 2 v103 + 5 v104 + v105 + 3 v109 + v110 + v111 + v112 + v113 >= 57
C17: 3 v1 + v2 + v4 + v5 + v6 + 2 v9 + v10 + v11 + 2 v13 + 2 v16 + v17 + 3 v18 + 3 v19 + v21 + 2 v22 + v23 + v24 + 2 v25 + v26 + v27 + v28 + v29 + v30 + v31 + v32 + v33 + 2 v34 + v35 + 2 v37 + 2 v38 + v39 + v40 + 2 v41 + v42 + 2 v43 + 2 v45 + 2 v47 + v48 + v49 + 5 v51 + v52 + 3 v54 + 3 v56 + v60 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + 2 v69 + v71 + v72 + 4 v73 + 2 v75 + 2 v77 + v78 + 2 v79 + v82 + v83 + v87 + v88 + 3 v89 + v90 + v91 + 2 v92 + v93 + 2 v94 + 2 v96 + 2 v98 + v99 + 2 v102 + v103 + 2 v104 + v106 + 2 v107 + 4 v110 + 3 v111 + 2 v112 + v114 <= 72
D17: 3 v1 + v2 + v4 + v5 + v6 + 2 v9 + v10 + v11 + 2 v13 + 2 v16 + v17 + 3 v18 + 3 v19 + v21 + 2 v22 + v23 + v24 + 2 v25 + v26 + v27 + v28 + v29 + v30 + v31 + v32 + v33 + 2 v34 + v35 + 2 v37 + 2 v38 + v39 + v40 + 2 v41 + v42 + 2 v43 + 2 v45 + 2 v47 + v48 + v49 + 5 v51 + v52 + 3 v54 + 3 v56 + v60 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + 2 v69 + v71 + v72 + 4 v73 + 2 v75 + 2 v77 + v78 + 2 v79 + v82 + v83 + v87 + v88 + 3 v89 + v90 + v91 + 2 v92 + v93 + 2 v94 + 2 v96 + 2 v98 + v99 + 2 v102 + v103 + 2 v104 + v106 + 2 v107 + 4 v110 + 3 v111 + 2 v112 + v114 >= 57
C18: v0 + 2 v2 + v3 + v5 + v7 + 2 v8 + 2 v9 + v10 + 2 v11 + 3 v12 + 2 v13 + v14 + v15 + v16 + v17 + 3 v18 + 3 v19 + 2 v20 + v21 + v24 + 3 v25 + v27 + v28 + 3 v29 + 2 v30 + v32 + 2 v33 + 2 v34 + 3 v37 + v41 + v42 + v43 + 2 v44 + 2 v45 + v46 + 2 v47 + 2 v49 + 2 v51 + v52 + v53 + v55 + v57 + 3 v59 + v60 + 2 v61 + v62 + 2 v63 + 2 v64 + 2 v65 + v66 + 2 v70 + 3 v71 + v73 + 2 v74 + v75 + v76 + v77 + 2 v78 + 2 v80 + 2 v81 + v83 + 5 v84 + 2 v85 + 2 v86 + v87 + v88 + v89 + v90 + v92 + v93 + v95 + v96 + v97 + v98 + v100 + v101 + v102 + v104 + v105 + v107 + v109 + v110 + 2 v111 <= 72
D18: v0 + 2 v2 + v3 + v5 + v7 + 2 v8 + 2 v9 + v10 + 2 v11 + 3 v12 + 2 v13 + v14 + v15 + v16 + v17 + 3 v18 + 3 v19 + 2 v20 + v21 + v24 + 3 v25 + v27 + v28 + 3 v29 + 2 v30 + v32 + 2 v33 + 2 v34 + 3 v37 + v41 + v42 + v43 + 2 v44 + 2 v45 + v46 + 2 v47 + 2 v49 + 2 v51 + v52 + v53 + v55 + v57 + 3 v59 + v60 + 2 v61 + v62 + 2 v63 + 2 v64 + 2 v65 + v66 + 2 v70 + 3 v71 + v73 + 2 v74 + v75 + v76 + v77 + 2 v78 + 2 v80 + 2 v81 + v83 + 5 v84 + 2 v85 + 2 v86 + v87 + v88 + v89 + v90 + v92 + v93 + v95 + v96 + v97 + v98 + v100 + v101 + v102 + v104 + v105 + v107 + v109 + v110 + 2 v111 >= 57
C19: v2 + v3 + v5 + 3 v6 + v8 + v9 + 3 v10 + v11 + v12 + v13 + v15 + 3 v16 + 3 v17 + 2 v18 + v20 + v21 + 2 v22 + 2 v23 + 2 v24 + v25 + 2 v26 + v29 + 2 v31 + v32 + v34 + v39 + v40 + v41 + v43 + 5 v44 + v46 + 2 v48 + 3 v49 + 4 v51 + v52 + v53 + v55 + 2 v56 + v57 + 3 v59 + v60 + v61 + 2 v62 + 2 v63 + v64 + 3 v65 + v66 + 2 v68 + v69 + v70 + 2 v71 + 3 v72 + v73 + 2 v75 + v76 + v77 + v79 + 4 v80 + v81 + 2 v82 + 2 v83 + v87 + v88 + v89 + 3 v90 + 2 v91 + v92 + 2 v95 + v96 + v98 + 3 v100 + v101 + v102 + 3 v106 + v107 + v108 + v109 + v110 + 2 v113 <= 72
D19: v2 + v3 + v5 + 3 v6 + v8 + v9 + 3 v10 + v11 + v12 + v13 + v15 + 3 v16 + 3 v17 + 2 v18 + v20 + v21 + 2 v22 + 2 v23 + 2 v24 + v25 + 2 v26 + v29 + 2 v31 + v32 + v34 + v39 + v40 + v41 + v43 + 5 v44 + v46 + 2 v48 + 3 v49 + 4 v51 + v52 + v53 + v55 + 2 v56 + v57 + 3 v59 + v60 + v61 + 2 v62 + 2 v63 + v64 + 3 v65 + v66 + 2 v68 + v69 + v70 + 2 v71 + 3 v72 + v73 + 2 v75 + v76 + v77 + v79 + 4 v80 + v81 + 2 v82 + 2 v83 + v87 + v88 + v89 + 3 v90 + 2 v91 + v92 + 2 v95 + v96 + v98 + 3 v100 + v101 + v102 + 3 v106 + v107 + v108 + v109 + v110 + 2 v113 >= 57
C20: v1 + 4 v2 + v3 + v4 + v6 + v7 + v8 + v10 + 3 v11 + 2 v13 + v14 + v15 + 3 v16 + 3 v17 + 2 v21 + v23 + 2 v24 + 2 v25 + 4 v28 + 2 v31 + v32 + v33 + 2 v34 + v35 + 4 v37 + v38 + v39 + 2 v40 + v41 + v42 + v43 + v45 + v47 + v48 + v50 + v51 + 3 v52 + v54 + v55 + 2 v56 + 2 v58 + 4 v59 + v60 + 2 v62 + 3 v64 + v66 + 2 v67 + 4 v68 + v73 + v75 + 2 v76 + v78 + 2 v79 + 2 v81 + v82 + 2 v83 + 2 v84 + 2 v86 + 2 v87 + 2 v88 + 2 v89 + v91 + v96 + v97 + 2 v98 + v99 + 2 v100 + v101 + v102 + v103 + 2 v104 + v105 + 2 v106 + v107 + 3 v108 + 2 v109 + v111 <= 72
D20: v1 + 4 v2 + v3 + v4 + v6 + v7 + v8 + v10 + 3 v11 + 2 v13 + v14 + v15 + 3 v16 + 3 v17 + 2 v21 + v23 + 2 v24 + 2 v25 + 4 v28 + 2 v31 + v32 + v33 + 2 v34 + v35 + 4 v37 + v38 + v39 + 2 v40 + v41 + v42 + v43 + v45 + v47 + v48 + v50 + v51 + 3 v52 + v54 + v55 + 2 v56 + 2 v58 + 4 v59 + v60 + 2 v62 + 3 v64 + v66 + 2 v67 + 4 v68 + v73 + v75 + 2 v76 + v78 + 2 v79 + 2 v81 + v82 + 2 v83 + 2 v84 + 2 v86 + 2 v87 + 2 v88 + 2 v89 + v91 + v96 + v97 + 2 v98 + v99 + 2 v100 + v101 + v102 + v103 + 2 v104 + v105 + 2 v106 + v107 + 3 v108 + 2 v109 + v111 >= 57
C21: 2 v1 + v2 + 3 v3 + v4 + v5 + v8 + 3 v9 + 3 v10 + 2 v11 + 2 v13 + 2 v17 + v18 + v21 + v22 + v23 + 3 v24 + 2 v25 + 2 v26 + 2 v27 + 3 v28 + v30 + v32 + v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + 2 v39 + v40 + 2 v42 + v45 + v46 + v48 + v49 + v50 + 3 v53 + v54 + 2 v55 + 4 v56 + v57 + 3 v58 + v61 + 2 v63 + v64 + 2 v65 + v66 + 2 v67 + v68 + v69 + 4 v70 + 5 v71 + v72 + 2 v73 + v74 + v78 + v79 + 3 v80 + 3 v81 + 2 v82 + v84 + v86 + v87 + 2 v88 + v89 + v91 + v92 + 3 v96 + v97 + v98 + v99 + v100 + v102 + v103 + v104 + 2 v107 + v110 + v111 + v113 <= 72
D21: 2 v1 + v2 + 3 v3 + v4 + v5 + v8 + 3 v9 + 3 v10 + 2 v11 + 2 v13 + 2 v17 + v18 + v21 + v22 + v23 + 3 v24 + 2 v25 + 2 v26 + 2 v27 + 3 v28 + v30 + v32 + v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + 2 v39 + v40 + 2 v42 + v45 + v46 + v48 + v49 + v50 + 3 v53 + v54 + 2 v55 + 4 v56 + v57 + 3 v58 + v61 + 2 v63 + v64 + 2 v65 + v66 + 2 v67 + v68 + v69 + 4 v70 + 5 v71 + v72 + 2 v73 + v74 + v78 + v79 + 3 v80 + 3 v81 + 2 v82 + v84 + v86 + v87 + 2 v88 + v89 + v91 + v92 + 3 v96 + v97 + v98 + v99 + v100 + v102 + v103 + v104 + 2 v107 + v110 + v111 + v113 >= 57
C22: 5 v1 + 3 v2 + 2 v3 + v5 + 2 v6 + 2 v7 + 2 v9 + 3 v10 + 2 v11 + v12 + v15 + v16 + v17 + v18 + 2 v19 + v20 + 2 v21 + v22 + v23 + 2 v27 + 2 v29 + 2 v30 + v31 + 2 v32 + v34 + v38 + v40 + 2 v41 + v42 + 3 v44 + 3 v45 + v46 + v49 + 2 v50 + v51 + v54 + v55 + v56 + v57 + 3 v58 + v59 + 3 v60 + 2 v61 + v62 + 2 v63 + 3 v64 + v66 + v67 + v70 + 2 v72 + v73 + v74 + v75 + v76 + v77 + 3 v79 + v80 + 3 v81 + 2 v82 + v83 + 2 v84 + 2 v86 + 3 v88 + v91 + 2 v92 + 2 v95 + v96 + v99 + v101 + v103 + v104 + v105 + v106 + 2 v107 + 2 v108 + v109 + v110 + 5 v112 <= 72
D22: 5 v1 + 3 v2 + 2 v3 + v5 + 2 v6 + 2 v7 + 2 v9 + 3 v10 + 2 v11 + v12 + v15 + v16 + v17 + v18 + 2 v19 + v20 + 2 v21 + v22 + v23 + 2 v27 + 2 v29 + 2 v30 + v31 + 2 v32 + v34 + v38 + v40 + 2 v41 + v42 + 3 v44 + 3 v45 + v46 + v49 + 2 v50 + v51 + v54 + v55 + v56 + v57 + 3 v58 + v59 + 3 v60 + 2 v61 + v62 + 2 v63 + 3 v64 + v66 + v67 + v70 + 2 v72 + v73 + v74 + v75 + v76 + v77 + 3 v79 + v80 + 3 v81 + 2 v82 + v83 + 2 v84 + 2 v86 + 3 v88 + v91 + 2 v92 + 2 v95 + v96 + v99 + v101 + v103 + v104 + v105 + v106 + 2 v107 + 2 v108 + v109 + v110 + 5 v112 >= 57
C23: v0 + v2 + 2 v3 + v4 + 2 v5 + 2 v7 + v8 + v9 + v10 + 2 v11 + v12 + v14 + v15 + 2 v16 + 2 v18 + v20 + v21 + v22 + 2 v23 + v24 + v25 + v26 + 3 v27 + v29 + 3 v31 + v32 + 3 v33 + v34 + 2 v35 + 3 v36 + v38 + 2 v39 + 3 v40 + 2 v41 + 2 v42 + v43 + v44 + v45 + v46 + v47 + 2 v48 + v49 + v50 + 2 v51 + v52 + v53 + v54 + 2 v55 + 2 v56 + 2 v57 + v58 + v59 + 2 v61 + 3 v62 + v65 + 2 v66 + v67 + v68 + v70 + v71 + 2 v75 + 2 v76 + v77 + v78 + 2 v79 + 2 v82 + v83 + v86 + v87 + 4 v88 + v90 + 2 v91 + 2 v92 + v95 + v99 + 3 v102 + 3 v105 + 3 v107 + 3 v108 + v110 + v111 + v114 <= 72
D23: v0 + v2 + 2 v3 + v4 + 2 v5 + 2 v7 + v8 + v9 + v10 + 2 v11 + v12 + v14 + v15 + 2 v16 + 2 v18 + v20 + v21 + v22 + 2 v23 + v24 + v25 + v26 + 3 v27 + v29 + 3 v31 + v32 + 3 v33 + v34 + 2 v35 + 3 v36 + v38 + 2 v39 + 3 v40 + 2 v41 + 2 v42 + v43 + v44 + v45 + v46 + v47 + 2 v48 + v49 + v50 + 2 v51 + v52 + v53 + v54 + 2 v55 + 2 v56 + 2 v57 + v58 + v59 + 2 v61 + 3 v62 + v65 + 2 v66 + v67 + v68 + v70 + v71 + 2 v75 + 2 v76 + v77 + v78 + 2 v79 + 2 v82 + v83 + v86 + v87 + 4 v88 + v90 + 2 v91 + 2 v92 + v95 + v99 + 3 v102 + 3 v105 + 3 v107 + 3 v108 + v110 + v111 + v114 >= 57
C24: v1 + v2 + 3 v4 + v5 + v8 + 2 v9 + v10 + 2 v11 + v12 + 2 v13 + 2 v14 + v16 + 2 v18 + v19 + v20 + v21 + 2 v22 + 2 v23 + v29 + v30 + v31 + 2 v33 + 5 v34 + v35 + v36 + 2 v37 + 3 v38 + v39 + v40 + 2 v41 + v42 + v43 + 2 v44 + v45 + v46 + v49 + 3 v50 + v51 + 2 v52 + 2 v53 + 3 v55 + v56 + v57 + 3 v58 + 3 v59 + v60 + 2 v61 + 2 v63 + 2 v66 + v69 + 2 v70 + v72 + 3 v73 + 2 v74 + v76 + 2 v77 + 2 v80 + v81 + 2 v83 + v85 + v87 + v88 + 3 v89 + 5 v91 + v92 + v96 + v98 + 2 v99 + 2 v100 + v101 + v102 + v103 + v104 + 4 v105 + v106 + v109 + v110 + v112 + v113 <= 72
D24: v1 + v2 + 3 v4 + v5 + v8 + 2 v9 + v10 + 2 v11 + v12 + 2 v13 + 2 v14 + v16 + 2 v18 + v19 + v20 + v21 + 2 v22 + 2 v23 + v29 + v30 + v31 + 2 v33 + 5 v34 + v35 + v36 + 2 v37 + 3 v38 + v39 + v40 + 2 v41 + v42 + v43 + 2 v44 + v45 + v46 + v49 + 3 v50 + v51 + 2 v52 + 2 v53 + 3 v55 + v56 + v57 + 3 v58 + 3 v59 + v60 + 2 v61 + 2 v63 + 2 v66 + v69 + 2 v70 + v72 + 3 v73 + 2 v74 + v76 + 2 v77 + 2 v80 + v81 + 2 v83 + v85 + v87 + v88 + 3 v89 + 5 v91 + v92 + v96 + v98 + 2 v99 + 2 v100 + v101 + v102 + v103 + v104 + 4 v105 + v106 + v109 + v110 + v112 + v113 >= 57
C25: 2 v1 + v2 + 3 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + 2 v8 + 3 v9 + v10 + 2 v11 + 2 v12 + 2 v13 + v15 + v16 + v17 + 2 v18 + 2 v19 + 3 v20 + v22 + 2 v24 + 3 v26 + v28 + 2 v29 + 2 v30 + v31 + 2 v33 + 2 v34 + 2 v35 + v39 + 2 v41 + v42 + v43 + v45 + 4 v46 + v48 + v50 + 3 v53 + v54 + 2 v56 + v57 + v59 + 3 v62 + v63 + 3 v64 + v68 + 2 v69 + 2 v72 + v73 + v74 + v75 + v78 + v79 + v82 + 4 v83 + 2 v84 + v85 + v86 + 2 v87 + v88 + 2 v89 + v91 + v92 + v94 + v98 + v100 + v101 + 4 v102 + 3 v104 + v105 + v106 + 2 v107 + 2 v108 + v109 + v112 + 4 v113 <= 72
D25: 2 v1 + v2 + 3 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + 2 v8 + 3 v9 + v10 + 2 v11 + 2 v12 + 2 v13 + v15 + v16 + v17 + 2 v18 + 2 v19 + 3 v20 + v22 + 2 v24 + 3 v26 + v28 + 2 v29 + 2 v30 + v31 + 2 v33 + 2 v34 + 2 v35 + v39 + 2 v41 + v42 + v43 + v45 + 4 v46 + v48 + v50 + 3 v53 + v54 + 2 v56 + v57 + v59 + 3 v62 + v63 + 3 v64 + v68 + 2 v69 + 2 v72 + v73 + v74 + v75 + v78 + v79 + v82 + 4 v83 + 2 v84 + v85 + v86 + 2 v87 + v88 + 2 v89 + v91 + v92 + v94 + v98 + v100 + v101 + 4 v102 + 3 v104 + v105 + v106 + 2 v107 + 2 v108 + v109 + v112 + 4 v113 >= 57
C26: v2 + 2 v4 + v6 + v7 + 3 v8 + 2 v9 + v10 + v11 + 2 v12 + v13 + 2 v14 + v15 + 2 v16 + 3 v17 + v18 + 2 v19 + 2 v20 + v22 + v26 + 2 v27 + v28 + v31 + 4 v32 + 2 v33 + v34 + 2 v37 + v38 + 2 v40 + v42 + v43 + 2 v45 + v46 + v47 + v48 + v51 + 2 v53 + v54 + 2 v56 + v57 + 3 v58 + v59 + v60 + v61 + 2 v62 + 3 v63 + 4 v65 + 2 v66 + 2 v67 + v71 + 3 v72 + 2 v73 + 2 v74 + v75 + 2 v77 + v79 + v81 + v82 + 2 v85 + v86 + 2 v87 + 2 v88 + v90 + 2 v91 + v92 + v94 + 4 v95 + 2 v97 + 5 v98 + v99 + v100 + 2 v102 + v103 + 3 v104 + v105 + v107 + 2 v108 + v112 <= 72
D26: v2 + 2 v4 + v6 + v7 + 3 v8 + 2 v9 + v10 + v11 + 2 v12 + v13 + 2 v14 + v15 + 2 v16 + 3 v17 + v18 + 2 v19 + 2 v20 + v22 + v26 + 2 v27 + v28 + v31 + 4 v32 + 2 v33 + v34 + 2 v37 + v38 + 2 v40 + v42 + v43 + 2 v45 + v46 + v47 + v48 + v51 + 2 v53 + v54 + 2 v56 + v57 + 3 v58 + v59 + v60 + v61 + 2 v62 + 3 v63 + 4 v65 + 2 v66 + 2 v67 + v71 + 3 v72 + 2 v73 + 2 v74 + v75 + 2 v77 + v79 + v81 + v82 + 2 v85 + v86 + 2 v87 + 2 v88 + v90 + 2 v91 + v92 + v94 + 4 v95 + 2 v97 + 5 v98 + v99 + v100 + 2 v102 + v103 + 3 v104 + v105 + v107 + 2 v108 + v112 >= 57
C27: v2 + 3 v5 + 2 v6 + 3 v7 + 3 v11 + v12 + v13 + v14 + 2 v15 + v16 + 2 v18 + 2 v20 + v22 + 3 v24 + v25 + v27 + 2 v28 + v29 + v30 + v31 + v33 + 3 v35 + v36 + 3 v37 + v38 + 2 v40 + v42 + 3 v43 + 4 v44 + v45 + 4 v46 + 3 v47 + v48 + v49 + 2 v50 + v51 + v52 + v54 + v56 + 2 v57 + v58 + v59 + v60 + v61 + 3 v63 + v64 + 3 v66 + 2 v68 + v69 + v70 + v71 + 3 v72 + 3 v73 + v74 + v75 + 2 v79 + v80 + v81 + v82 + v83 + v84 + v85 + v86 + 2 v88 + v94 + v95 + 2 v96 + v97 + 2 v98 + 2 v99 + v102 + 4 v103 + v104 + 2 v105 + v107 + v108 + 3 v110 + 2 v113 <= 72
D27: v2 + 3 v5 + 2 v6 + 3 v7 + 3 v11 + v12 + v13 + v14 + 2 v15 + v16 + 2 v18 + 2 v20 + v22 + 3 v24 + v25 + v27 + 2 v28 + v29 + v30 + v31 + v33 + 3 v35 + v36 + 3 v37 + v38 + 2 v40 + v42 + 3 v43 + 4 v44 + v45 + 4 v46 + 3 v47 + v48 + v49 + 2 v50 + v51 + v52 + v54 + v56 + 2 v57 + v58 + v59 + v60 + v61 + 3 v63 + v64 + 3 v66 + 2 v68 + v69 + v70 + v71 + 3 v72 + 3 v73 + v74 + v75 + 2 v79 + v80 + v81 + v82 + v83 + v84 + v85 + v86 + 2 v88 + v94 + v95 + 2 v96 + v97 + 2 v98 + 2 v99 + v102 + 4 v103 + v104 + 2 v105 + v107 + v108 + 3 v110 + 2 v113 >= 57
C28: v1 + v2 + 3 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v9 + v12 + 2 v15 + v16 + v17 + 2 v20 + 2 v21 + 3 v22 + 2 v25 + v26 + 4 v27 + v30 + v31 + 4 v33 + 3 v34 + 3 v35 + 2 v37 + v39 + v40 + v42 + 2 v43 + 2 v44 + 2 v45 + 2 v47 + 2 v48 + 2 v50 + 3 v51 + 2 v52 + v56 + 2 v58 + v59 + 2 v61 + v62 + v63 + 3 v64 + 2 v69 + 3 v70 + v71 + 2 v74 + 2 v75 + v78 + v80 + 3 v82 + v83 + v84 + v86 + 3 v87 + v89 + v90 + v91 + 2 v92 + 2 v94 + 3 v95 + v96 + v97 + 2 v98 + 2 v99 + 3 v100 + v101 + 2 v103 + 2 v104 + v106 + 2 v107 + 2 v109 + v111 + v112 <= 72
D28: v1 + v2 + 3 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v9 + v12 + 2 v15 + v16 + v17 + 2 v20 + 2 v21 + 3 v22 + 2 v25 + v26 + 4 v27 + v30 + v31 + 4 v33 + 3 v34 + 3 v35 + 2 v37 + v39 + v40 + v42 + 2 v43 + 2 v44 + 2 v45 + 2 v47 + 2 v48 + 2 v50 + 3 v51 + 2 v52 + v56 + 2 v58 + v59 + 2 v61 + v62 + v63 + 3 v64 + 2 v69 + 3 v70 + v71 + 2 v74 + 2 v75 + v78 + v80 + 3 v82 + v83 + v84 + v86 + 3 v87 + v89 + v90 + v91 + 2 v92 + 2 v94 + 3 v95 + v96 + v97 + 2 v98 + 2 v99 + 3 v100 + v101 + 2 v103 + 2 v104 + v106 + 2 v107 + 2 v109 + v111 + v112 >= 57
C29: 3 v3 + 2 v4 + v6 + v7 + v8 + v10 + v12 + v13 + v16 + v17 + 4 v19 + 3 v20 + v24 + v25 + 2 v26 + v29 + 3 v30 + v31 + 2 v32 + v33 + v34 + 2 v36 + 2 v37 + v38 + 3 v39 + 2 v40 + 3 v41 + 2 v42 + v43 + 2 v44 + v45 + v46 + v47 + v48 + 4 v49 + v51 + 2 v52 + v53 + 2 v55 + 2 v56 + 3 v58 + v59 + 2 v60 + 2 v61 + 2 v62 + v63 + 2 v64 + v66 + 2 v68 + v69 + v70 + 2 v71 + 2 v73 + v76 + v77 + 2 v78 + 2 v82 + v83 + v85 + 2 v86 + 3 v87 + 2 v88 + v89 + 3 v90 + 2 v96 + v97 + 2 v98 + v99 + v101 + 2 v102 + 5 v103 + v105 + 2 v106 + v108 + v110 + 2 v112 <= 72
D29: 3 v3 + 2 v4 + v6 + v7 + v8 + v10 + v12 + v13 + v16 + v17 + 4 v19 + 3 v20 + v24 + v25 + 2 v26 + v29 + 3 v30 + v31 + 2 v32 + v33 + v34 + 2 v36 + 2 v37 + v38 + 3 v39 + 2 v40 + 3 v41 + 2 v42 + v43 + 2 v44 + v45 + v46 + v47 + v48 + 4 v49 + v51 + 2 v52 + v53 + 2 v55 + 2 v56 + 3 v58 + v59 + 2 v60 + 2 v61 + 2 v62 + v63 + 2 v64 + v66 + 2 v68 + v69 + v70 + 2 v71 + 2 v73 + v76 + v77 + 2 v78 + 2 v82 + v83 + v85 + 2 v86 + 3 v87 + 2 v88 + v89 + 3 v90 + 2 v96 + v97 + 2 v98 + v99 + v101 + 2 v102 + 5 v103 + v105 + 2 v106 + v108 + v110 + 2 v112 >= 57
C30: v1 + v2 + 2 v3 + 3 v4 + 3 v5 + v6 + v7 + 2 v8 + v9 + v12 + 3 v13 + 4 v14 + 3 v15 + v16 + 3 v17 + v18 + 2 v21 + v22 + v23 + 2 v24 + v26 + v28 + 4 v29 + 2 v30 + v31 + v32 + 4 v34 + v38 + 2 v40 + v41 + v42 + v43 + 3 v44 + 3 v45 + 3 v48 + v49 + 2 v51 + v53 + v54 + 2 v56 + v57 + v58 + v60 + 2 v61 + v62 + v65 + 2 v66 + v67 + v68 + v69 + 2 v70 + v71 + 2 v74 + v75 + 2 v76 + 2 v81 + 2 v82 + 3 v86 + v87 + v88 + 2 v94 + 3 v96 + v97 + 2 v98 + v101 + 2 v102 + v103 + v104 + 2 v105 + v106 + 2 v108 + v109 + 2 v110 + 3 v111 + v112 + 2 v113 <= 72
D30: v1 + v2 + 2 v3 + 3 v4 + 3 v5 + v6 + v7 + 2 v8 + v9 + v12 + 3 v13 + 4 v14 + 3 v15 + v16 + 3 v17 + v18 + 2 v21 + v22 + v23 + 2 v24 + v26 + v28 + 4 v29 + 2 v30 + v31 + v32 + 4 v34 + v38 + 2 v40 + v41 + v42 + v43 + 3 v44 + 3 v45 + 3 v48 + v49 + 2 v51 + v53 + v54 + 2 v56 + v57 + v58 + v60 + 2 v61 + v62 + v65 + 2 v66 + v67 + v68 + v69 + 2 v70 + v71 + 2 v74 + v75 + 2 v76 + 2 v81 + 2 v82 + 3 v86 + v87 + v88 + 2 v94 + 3 v96 + v97 + 2 v98 + v101 + 2 v102 + v103 + v104 + 2 v105 + v106 + 2 v108 + v109 + 2 v110 + 3 v111 + v112 + 2 v113 >= 57
C31: v1 + 2 v2 + 3 v3 + v4 + v5 + 2 v8 + v9 + 3 v11 + v12 + v13 + v14 + v15 + v16 + 2 v17 + v20 + 2 v21 + v23 + 2 v24 + v26 + v27 + 3 v28 + 2 v29 + v31 + 3 v33 + v34 + v35 + 2 v36 + v37 + v38 + v41 + v42 + v43 + v44 + 2 v45 + v46 + v47 + v48 + v49 + v50 + 2 v51 + v53 + 2 v54 + 2 v55 + v56 + v57 + v58 + 3 v60 + 5 v63 + v64 + v67 + 2 v68 + v69 + v70 + 3 v74 + 2 v75 + v76 + v77 + v78 + v80 + v83 + 2 v85 + 2 v86 + 3 v88 + 4 v89 + 6 v90 + v91 + 3 v92 + 2 v94 + 2 v95 + v96 + v97 + v98 + v101 + v102 + v103 + v105 + v106 + v107 + v108 + v109 + 2 v110 + v112 + v113 <= 72
D31: v1 + 2 v2 + 3 v3 + v4 + v5 + 2 v8 + v9 + 3 v11 + v12 + v13 + v14 + v15 + v16 + 2 v17 + v20 + 2 v21 + v23 + 2 v24 + v26 + v27 + 3 v28 + 2 v29 + v31 + 3 v33 + v34 + v35 + 2 v36 + v37 + v38 + v41 + v42 + v43 + v44 + 2 v45 + v46 + v47 + v48 + v49 + v50 + 2 v51 + v53 + 2 v54 + 2 v55 + v56 + v57 + v58 + 3 v60 + 5 v63 + v64 + v67 + 2 v68 + v69 + v70 + 3 v74 + 2 v75 + v76 + v77 + v78 + v80 + v83 + 2 v85 + 2 v86 + 3 v88 + 4 v89 + 6 v90 + v91 + 3 v92 + 2 v94 + 2 v95 + v96 + v97 + v98 + v101 + v102 + v103 + v105 + v106 + v107 + v108 + v109 + 2 v110 + v112 + v113 >= 57
C32: 3 v1 + 2 v3 + v4 + 3 v7 + 2 v8 + v9 + v10 + 4 v11 + v13 + 2 v15 + v16 + 2 v18 + 2 v19 + v21 + 3 v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + 3 v32 + 2 v33 + v34 + 2 v36 + v37 + 2 v38 + v40 + 2 v41 + v43 + v44 + 2 v46 + 2 v47 + v48 + 2 v49 + v50 + v51 + v52 + v53 + v54 + 2 v57 + v58 + v59 + v60 + 2 v62 + v63 + v65 + v67 + 2 v68 + v69 + 2 v70 + v71 + v74 + v75 + v76 + 2 v77 + v78 + v79 + 2 v80 + v81 + 4 v82 + v83 + v84 + 2 v85 + 5 v86 + 3 v87 + v89 + 3 v91 + 3 v94 + v97 + 2 v98 + v99 + 3 v100 + v106 + 2 v108 + 4 v110 + v113 <= 72
D32: 3 v1 + 2 v3 + v4 + 3 v7 + 2 v8 + v9 + v10 + 4 v11 + v13 + 2 v15 + v16 + 2 v18 + 2 v19 + v21 + 3 v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + 3 v32 + 2 v33 + v34 + 2 v36 + v37 + 2 v38 + v40 + 2 v41 + v43 + v44 + 2 v46 + 2 v47 + v48 + 2 v49 + v50 + v51 + v52 + v53 + v54 + 2 v57 + v58 + v59 + v60 + 2 v62 + v63 + v65 + v67 + 2 v68 + v69 + 2 v70 + v71 + v74 + v75 + v76 + 2 v77 + v78 + v79 + 2 v80 + v81 + 4 v82 + v83 + v84 + 2 v85 + 5 v86 + 3 v87 + v89 + 3 v91 + 3 v94 + v97 + 2 v98 + v99 + 3 v100 + v106 + 2 v108 + 4 v110 + v113 >= 57
C33: v1 + 2 v2 + 2 v4 + 3 v5 + v7 + 3 v9 + v10 + 2 v12 + v13 + 2 v14 + v15 + v16 + v17 + v18 + v19 + v20 + 2 v21 + v22 + 4 v25 + 2 v28 + v29 + 3 v31 + 2 v32 + v35 + 2 v36 + v37 + v38 + v41 + 3 v42 + v44 + v45 + v48 + v49 + v50 + 4 v51 + 3 v53 + v54 + 2 v55 + 2 v57 + v58 + v59 + v60 + v62 + 2 v63 + v64 + 2 v68 + 2 v69 + v70 + v71 + 3 v72 + v74 + v76 + v77 + 3 v78 + 2 v80 + v81 + v82 + v83 + 2 v85 + 2 v86 + 2 v87 + v91 + 3 v92 + v98 + 2 v99 + 2 v100 + 3 v101 + v102 + 4 v103 + 2 v104 + v105 + 2 v107 + 4 v108 + 2 v110 + v111 + v112 + v113 <= 72
D33: v1 + 2 v2 + 2 v4 + 3 v5 + v7 + 3 v9 + v10 + 2 v12 + v13 + 2 v14 + v15 + v16 + v17 + v18 + v19 + v20 + 2 v21 + v22 + 4 v25 + 2 v28 + v29 + 3 v31 + 2 v32 + v35 + 2 v36 + v37 + v38 + v41 + 3 v42 + v44 + v45 + v48 + v49 + v50 + 4 v51 + 3 v53 + v54 + 2 v55 + 2 v57 + v58 + v59 + v60 + v62 + 2 v63 + v64 + 2 v68 + 2 v69 + v70 + v71 + 3 v72 + v74 + v76 + v77 + 3 v78 + 2 v80 + v81 + v82 + v83 + 2 v85 + 2 v86 + 2 v87 + v91 + 3 v92 + v98 + 2 v99 + 2 v100 + 3 v101 + v102 + 4 v103 + 2 v104 + v105 + 2 v107 + 4 v108 + 2 v110 + v111 + v112 + v113 >= 57
C34: v1 + v2 + v3 + v4 + v6 + v8 + v9 + 2 v11 + 2 v12 + v13 + 2 v14 + 2 v15 + v16 + 2 v17 + v19 + v20 + 3 v22 + 2 v23 + 2 v24 + 2 v25 + v26 + 4 v27 + v28 + 3 v30 + 2 v31 + 4 v33 + v34 + 2 v38 + 2 v40 + v41 + 2 v42 + v43 + v44 + v45 + v46 + v47 + 4 v48 + 2 v49 + v52 + 2 v54 + 2 v55 + v56 + v58 + v59 + 3 v60 + v61 + v63 + v65 + v67 + 2 v68 + v70 + v71 + 5 v72 + v73 + v74 + v75 + 3 v76 + 2 v78 + v80 + 2 v81 + 3 v83 + 2 v84 + 2 v85 + 3 v87 + v88 + v89 + v91 + v96 + v97 + 2 v99 + 2 v101 + 2 v102 + v104 + v106 + v107 + 3 v110 + v111 + 2 v112 <= 72
D34: v1 + v2 + v3 + v4 + v6 + v8 + v9 + 2 v11 + 2 v12 + v13 + 2 v14 + 2 v15 + v16 + 2 v17 + v19 + v20 + 3 v22 + 2 v23 + 2 v24 + 2 v25 + v26 + 4 v27 + v28 + 3 v30 + 2 v31 + 4 v33 + v34 + 2 v38 + 2 v40 + v41 + 2 v42 + v43 + v44 + v45 + v46 + v47 + 4 v48 + 2 v49 + v52 + 2 v54 + 2 v55 + v56 + v58 + v59 + 3 v60 + v61 + v63 + v65 + v67 + 2 v68 + v70 + v71 + 5 v72 + v73 + v74 + v75 + 3 v76 + 2 v78 + v80 + 2 v81 + 3 v83 + 2 v84 + 2 v85 + 3 v87 + v88 + v89 + v91 + v96 + v97 + 2 v99 + 2 v101 + 2 v102 + v104 + v106 + v107 + 3 v110 + v111 + 2 v112 >= 57
C35: 2 v1 + v3 + 2 v4 + 3 v6 + v8 + 2 v9 + 2 v10 + v11 + v12 + v13 + v14 + 2 v16 + 2 v17 + v18 + 2 v19 + v20 + v21 + v22 + 5 v23 + 2 v24 + v25 + 3 v27 + v28 + 4 v29 + v30 + v31 + v33 + v35 + 3 v37 + v38 + 4 v39 + v40 + v41 + 2 v42 + v43 + 2 v44 + 2 v45 + v47 + 2 v50 + v51 + v52 + 2 v54 + v62 + 2 v66 + v67 + v68 + 2 v70 + 2 v71 + v72 + v74 + v75 + v77 + 2 v79 + 3 v80 + 2 v82 + 2 v83 + v84 + 4 v85 + v86 + 2 v87 + 2 v88 + v89 + v90 + v91 + 2 v92 + v94 + 3 v97 + 2 v98 + 3 v101 + v102 + 2 v103 + 2 v104 + 2 v105 + 2 v108 + v109 + v110 + v113 <= 72
D35: 2 v1 + v3 + 2 v4 + 3 v6 + v8 + 2 v9 + 2 v10 + v11 + v12 + v13 + v14 + 2 v16 + 2 v17 + v18 + 2 v19 + v20 + v21 + v22 + 5 v23 + 2 v24 + v25 + 3 v27 + v28 + 4 v29 + v30 + v31 + v33 + v35 + 3 v37 + v38 + 4 v39 + v40 + v41 + 2 v42 + v43 + 2 v44 + 2 v45 + v47 + 2 v50 + v51 + v52 + 2 v54 + v62 + 2 v66 + v67 + v68 + 2 v70 + 2 v71 + v72 + v74 + v75 + v77 + 2 v79 + 3 v80 + 2 v82 + 2 v83 + v84 + 4 v85 + v86 + 2 v87 + 2 v88 + v89 + v90 + v91 + 2 v92 + v94 + 3 v97 + 2 v98 + 3 v101 + v102 + 2 v103 + 2 v104 + 2 v105 + 2 v108 + v109 + v110 + v113 >= 57
C36: 3 v1 + v2 + v3 + v4 + v5 + 3 v7 + 2 v8 + v11 + 2 v12 + v13 + 3 v14 + v16 + v19 + 3 v20 + 2 v22 + v23 + 2 v24 + 3 v26 + 3 v27 + v30 + v32 + v34 + 2 v35 + v36 + 2 v37 + v38 + v39 + 3 v40 + v41 + 2 v42 + v43 + v45 + v46 + v47 + v49 + v50 + 3 v51 + v52 + v53 + v54 + v56 + v57 + v59 + v61 + v63 + 2 v64 + v65 + v67 + 2 v68 + 2 v70 + v71 + v72 + v75 + v76 + 4 v77 + v78 + 2 v80 + 3 v81 + 3 v83 + 2 v84 + v85 + v89 + 2 v90 + v91 + 3 v92 + v95 + 5 v96 + 3 v98 + v99 + v100 + v101 + v102 + 2 v105 + 2 v106 + 4 v108 + v109 + v110 + v111 + v112 + v113 <= 72
D36: 3 v1 + v2 + v3 + v4 + v5 + 3 v7 + 2 v8 + v11 + 2 v12 + v13 + 3 v14 + v16 + v19 + 3 v20 + 2 v22 + v23 + 2 v24 + 3 v26 + 3 v27 + v30 + v32 + v34 + 2 v35 + v36 + 2 v37 + v38 + v39 + 3 v40 + v41 + 2 v42 + v43 + v45 + v46 + v47 + v49 + v50 + 3 v51 + v52 + v53 + v54 + v56 + v57 + v59 + v61 + v63 + 2 v64 + v65 + v67 + 2 v68 + 2 v70 + v71 + v72 + v75 + v76 + 4 v77 + v78 + 2 v80 + 3 v81 + 3 v83 + 2 v84 + v85 + v89 + 2 v90 + v91 + 3 v92 + v95 + 5 v96 + 3 v98 + v99 + v100 + v101 + v102 + 2 v105 + 2 v106 + 4 v108 + v109 + v110 + v111 + v112 + v113 >= 57
C37: v0 + 2 v1 + v2 + v3 + v4 + 3 v6 + 2 v8 + 2 v9 + 2 v10 + v13 + 2 v14 + 2 v15 + 2 v20 + 3 v22 + v23 + v26 + 2 v28 + 2 v30 + 2 v31 + 2 v32 + v35 + v36 + v38 + 2 v40 + v42 + v43 + v44 + 2 v45 + 2 v47 + 3 v48 + 2 v49 + v50 + v52 + v53 + v55 + v57 + v58 + v59 + 2 v60 + v61 + 2 v62 + 2 v63 + 2 v64 + v65 + v66 + v68 + 3 v69 + 2 v70 + 2 v71 + v72 + 3 v73 + v74 + v75 + v78 + 3 v79 + v80 + v81 + v82 + v83 + v84 + v85 + v87 + v88 + 5 v89 + v90 + v91 + v92 + 3 v94 + 2 v96 + 2 v97 + v98 + v99 + v100 + 2 v101 + v103 + 2 v104 + 2 v105 + v106 + 4 v108 + v109 + v110 + v111 <= 72
D37: v0 + 2 v1 + v2 + v3 + v4 + 3 v6 + 2 v8 + 2 v9 + 2 v10 + v13 + 2 v14 + 2 v15 + 2 v20 + 3 v22 + v23 + v26 + 2 v28 + 2 v30 + 2 v31 + 2 v32 + v35 + v36 + v38 + 2 v40 + v42 + v43 + v44 + 2 v45 + 2 v47 + 3 v48 + 2 v49 + v50 + v52 + v53 + v55 + v57 + v58 + v59 + 2 v60 + v61 + 2 v62 + 2 v63 + 2 v64 + v65 + v66 + v68 + 3 v69 + 2 v70 + 2 v71 + v72 + 3 v73 + v74 + v75 + v78 + 3 v79 + v80 + v81 + v82 + v83 + v84 + v85 + v87 + v88 + 5 v89 + v90 + v91 + v92 + 3 v94 + 2 v96 + 2 v97 + v98 + v99 + v100 + 2 v101 + v103 + 2 v104 + 2 v105 + v106 + 4 v108 + v109 + v110 + v111 >= 57
C38: v0 + v1 + v2 + v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v9 + v10 + v11 + 2 v12 + 3 v13 + v14 + v15 + 2 v16 + 3 v17 + 4 v19 + v20 + 2 v23 + 2 v25 + 3 v26 + 2 v27 + 2 v28 + v30 + v31 + v32 + 3 v34 + 2 v35 + v37 + 2 v38 + 2 v39 + v40 + v41 + v42 + v43 + v44 + 2 v46 + v48 + v50 + 2 v52 + v53 + v54 + v55 + v56 + 2 v57 + v58 + v60 + v61 + v63 + v64 + v66 + v67 + 3 v68 + 3 v69 + 3 v72 + v73 + v74 + v75 + 2 v77 + v79 + v80 + 3 v81 + 2 v82 + v85 + 3 v86 + 2 v90 + 2 v91 + 2 v92 + 2 v94 + 2 v95 + v96 + v97 + 2 v99 + v101 + v102 + v103 + v106 + v107 + 4 v109 + 2 v110 <= 72
D38: v0 + v1 + v2 + v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v9 + v10 + v11 + 2 v12 + 3 v13 + v14 + v15 + 2 v16 + 3 v17 + 4 v19 + v20 + 2 v23 + 2 v25 + 3 v26 + 2 v27 + 2 v28 + v30 + v31 + v32 + 3 v34 + 2 v35 + v37 + 2 v38 + 2 v39 + v40 + v41 + v42 + v43 + v44 + 2 v46 + v48 + v50 + 2 v52 + v53 + v54 + v55 + v56 + 2 v57 + v58 + v60 + v61 + v63 + v64 + v66 + v67 + 3 v68 + 3 v69 + 3 v72 + v73 + v74 + v75 + 2 v77 + v79 + v80 + 3 v81 + 2 v82 + v85 + 3 v86 + 2 v90 + 2 v91 + 2 v92 + 2 v94 + 2 v95 + v96 + v97 + 2 v99 + v101 + v102 + v103 + v106 + v107 + 4 v109 + 2 v110 >= 57
C39: 2 v3 + 2 v5 + 2 v6 + v8 + v9 + v10 + v11 + v12 + 3 v13 + v14 + 2 v16 + v19 + v20 + v21 + v22 + 3 v23 + v25 + v26 + v28 + v29 + v30 + 2 v31 + v32 + 2 v33 + v34 + v35 + v36 + 2 v37 + v40 + 4 v41 + 2 v42 + 3 v43 + v46 + 4 v47 + v48 + v50 + 2 v51 + 5 v53 + v54 + v56 + v57 + 2 v59 + 3 v60 + 2 v61 + v64 + v65 + v67 + 2 v68 + v69 + 3 v70 + 2 v72 + v73 + 2 v74 + 2 v75 + 2 v76 + 3 v77 + v78 + v79 + v80 + 3 v81 + 4 v82 + v84 + v85 + 3 v88 + v89 + v90 + v94 + v95 + v96 + 2 v97 + v99 + v100 + v103 + 3 v104 + v105 + v106 + v108 + v111 + 2 v112 + v113 <= 72
D39: 2 v3 + 2 v5 + 2 v6 + v8 + v9 + v10 + v11 + v12 + 3 v13 + v14 + 2 v16 + v19 + v20 + v21 + v22 + 3 v23 + v25 + v26 + v28 + v29 + v30 + 2 v31 + v32 + 2 v33 + v34 + v35 + v36 + 2 v37 + v40 + 4 v41 + 2 v42 + 3 v43 + v46 + 4 v47 + v48 + v50 + 2 v51 + 5 v53 + v54 + v56 + v57 + 2 v59 + 3 v60 + 2 v61 + v64 + v65 + v67 + 2 v68 + v69 + 3 v70 + 2 v72 + v73 + 2 v74 + 2 v75 + 2 v76 + 3 v77 + v78 + v79 + v80 + 3 v81 + 4 v82 + v84 + v85 + 3 v88 + v89 + v90 + v94 + v95 + v96 + 2 v97 + v99 + v100 + v103 + 3 v104 + v105 + v106 + v108 + v111 + 2 v112 + v113 >= 57
C40: v1 + v2 + v4 + 2 v5 + 3 v6 + 2 v7 + 2 v8 + 2 v10 + v11 + v15 + v16 + v18 + v19 + 2 v20 + 2 v22 + v23 + v24 + v27 + 3 v28 + 4 v34 + v35 + 2 v37 + v40 + 4 v41 + 3 v42 + v43 + v44 + 3 v45 + v46 + v47 + v48 + 2 v49 + v50 + 2 v52 + 2 v53 + v54 + 3 v55 + 3 v61 + 2 v62 + v63 + 3 v64 + 4 v65 + v66 + 3 v67 + 2 v68 + v69 + v70 + v72 + v73 + v74 + v75 + 2 v76 + v78 + v79 + 3 v80 + 2 v85 + 2 v86 + 2 v87 + v88 + 2 v90 + v91 + 3 v92 + v94 + v96 + 2 v97 + v98 + 3 v99 + v101 + v102 + v104 + 2 v107 + v108 + 2 v110 + 2 v111 + v112 + 2 v113 <= 72
D40: v1 + v2 + v4 + 2 v5 + 3 v6 + 2 v7 + 2 v8 + 2 v10 + v11 + v15 + v16 + v18 + v19 + 2 v20 + 2 v22 + v23 + v24 + v27 + 3 v28 + 4 v34 + v35 + 2 v37 + v40 + 4 v41 + 3 v42 + v43 + v44 + 3 v45 + v46 + v47 + v48 + 2 v49 + v50 + 2 v52 + 2 v53 + v54 + 3 v55 + 3 v61 + 2 v62 + v63 + 3 v64 + 4 v65 + v66 + 3 v67 + 2 v68 + v69 + v70 + v72 + v73 + v74 + v75 + 2 v76 + v78 + v79 + 3 v80 + 2 v85 + 2 v86 + 2 v87 + v88 + 2 v90 + v91 + 3 v92 + v94 + v96 + 2 v97 + v98 + 3 v99 + v101 + v102 + v104 + 2 v107 + v108 + 2 v110 + 2 v111 + v112 + 2 v113 >= 57
C41: 3 v1 + 2 v2 + 3 v3 + 2 v4 + v5 + 2 v6 + 3 v10 + v11 + 2 v12 + 2 v13 + 3 v14 + v15 + v16 + v18 + 2 v19 + v20 + v21 + 3 v22 + v23 + 2 v25 + 2 v26 + v27 + 2 v28 + 2 v29 + v31 + 2 v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + v39 + 2 v41 + v42 + 2 v47 + 2 v48 + v49 + v50 + v53 + v56 + v58 + 2 v59 + 3 v60 + 2 v61 + 2 v62 + v63 + v64 + 3 v65 + 5 v66 + 2 v67 + v68 + v71 + v73 + 3 v74 + v76 + 2 v77 + v78 + v79 + v80 + 3 v83 + v84 + v90 + v92 + 2 v95 + v97 + v98 + 2 v100 + v102 + 3 v103 + v106 + v107 + 2 v108 + 2 v109 + 4 v110 + v111 + v113 <= 72
D41: 3 v1 + 2 v2 + 3 v3 + 2 v4 + v5 + 2 v6 + 3 v10 + v11 + 2 v12 + 2 v13 + 3 v14 + v15 + v16 + v18 + 2 v19 + v20 + v21 + 3 v22 + v23 + 2 v25 + 2 v26 + v27 + 2 v28 + 2 v29 + v31 + 2 v33 + v34 + 3 v35 + 2 v36 + v37 + v38 + v39 + 2 v41 + v42 + 2 v47 + 2 v48 + v49 + v50 + v53 + v56 + v58 + 2 v59 + 3 v60 + 2 v61 + 2 v62 + v63 + v64 + 3 v65 + 5 v66 + 2 v67 + v68 + v71 + v73 + 3 v74 + v76 + 2 v77 + v78 + v79 + v80 + 3 v83 + v84 + v90 + v92 + 2 v95 + v97 + v98 + 2 v100 + v102 + 3 v103 + v106 + v107 + 2 v108 + 2 v109 + 4 v110 + v111 + v113 >= 57
C42: v2 + v4 + 2 v6 + 2 v7 + 4 v8 + 2 v10 + 4 v12 + 2 v13 + v14 + 2 v15 + 2 v16 + v17 + v18 + v19 + 2 v21 + 2 v22 + 2 v23 + 2 v24 + 3 v28 + v29 + v30 + 2 v31 + v32 + v33 + v34 + v35 + v37 + 4 v38 + 4 v39 + 2 v40 + v42 + 3 v45 + 4 v46 + 2 v47 + v48 + 2 v49 + 2 v50 + 2 v51 + v52 + v53 + 2 v56 + v58 + 2 v59 + 2 v60 + v61 + 3 v62 + 2 v63 + v67 + 2 v69 + v70 + v71 + 2 v74 + v75 + 2 v77 + 3 v78 + 2 v80 + v81 + 2 v82 + v83 + v84 + v87 + v88 + v89 + 2 v92 + v94 + v95 + v96 + 3 v99 + v103 + 2 v107 + v108 + v109 + v110 + v111 + 2 v112 + v113 <= 72
D42: v2 + v4 + 2 v6 + 2 v7 + 4 v8 + 2 v10 + 4 v12 + 2 v13 + v14 + 2 v15 + 2 v16 + v17 + v18 + v19 + 2 v21 + 2 v22 + 2 v23 + 2 v24 + 3 v28 + v29 + v30 + 2 v31 + v32 + v33 + v34 + v35 + v37 + 4 v38 + 4 v39 + 2 v40 + v42 + 3 v45 + 4 v46 + 2 v47 + v48 + 2 v49 + 2 v50 + 2 v51 + v52 + v53 + 2 v56 + v58 + 2 v59 + 2 v60 + v61 + 3 v62 + 2 v63 + v67 + 2 v69 + v70 + v71 + 2 v74 + v75 + 2 v77 + 3 v78 + 2 v80 + v81 + 2 v82 + v83 + v84 + v87 + v88 + v89 + 2 v92 + v94 + v95 + v96 + 3 v99 + v103 + 2 v107 + v108 + v109 + v110 + v111 + 2 v112 + v113 >= 57
C43: v1 + v2 + v3 + v4 + 4 v5 + v8 + v9 + v11 + v14 + 2 v15 + v16 + v17 + v19 + 2 v20 + v21 + 2 v22 + v23 + v24 + v25 + v26 + v27 + 2 v28 + v29 + v30 + 3 v32 + 2 v33 + 2 v34 + 2 v35 + v36 + v37 + 2 v38 + 3 v39 + v40 + v41 + v43 + v44 + 2 v45 + v47 + 2 v48 + 6 v49 + 3 v50 + 2 v51 + 2 v53 + v54 + v56 + v57 + v58 + v60 + v62 + 2 v63 + v64 + v65 + v67 + 3 v68 + v69 + v71 + 2 v73 + v74 + 3 v76 + 3 v77 + 4 v79 + v80 + v81 + v82 + v83 + 3 v84 + 2 v85 + v87 + 2 v88 + 2 v91 + v92 + 2 v95 + v98 + 2 v101 + v102 + v103 + 2 v104 + 3 v109 + 2 v111 + 2 v113 <= 72
D43: v1 + v2 + v3 + v4 + 4 v5 + v8 + v9 + v11 + v14 + 2 v15 + v16 + v17 + v19 + 2 v20 + v21 + 2 v22 + v23 + v24 + v25 + v26 + v27 + 2 v28 + v29 + v30 + 3 v32 + 2 v33 + 2 v34 + 2 v35 + v36 + v37 + 2 v38 + 3 v39 + v40 + v41 + v43 + v44 + 2 v45 + v47 + 2 v48 + 6 v49 + 3 v50 + 2 v51 + 2 v53 + v54 + v56 + v57 + v58 + v60 + v62 + 2 v63 + v64 + v65 + v67 + 3 v68 + v69 + v71 + 2 v73 + v74 + 3 v76 + 3 v77 + 4 v79 + v80 + v81 + v82 + v83 + 3 v84 + 2 v85 + v87 + 2 v88 + 2 v91 + v92 + 2 v95 + v98 + 2 v101 + v102 + v103 + 2 v104 + 3 v109 + 2 v111 + 2 v113 >= 57
C44: v4 + 2 v5 + 3 v6 + 4 v7 + 3 v8 + 3 v9 + 2 v10 + 4 v11 + v12 + v14 + 2 v15 + 2 v16 + v17 + v18 + v19 + v22 + v23 + v24 + v25 + 3 v26 + 2 v27 + v28 + v29 + v30 + v31 + v33 + v34 + v35 + v36 + v37 + 3 v38 + v39 + v42 + v44 + 2 v45 + v47 + v48 + 3 v51 + 2 v53 + 3 v55 + v56 + 2 v57 + v58 + v59 + v60 + 2 v64 + v65 + 2 v66 + 3 v68 + 2 v69 + 3 v70 + v71 + 2 v73 + 2 v74 + v76 + 2 v77 + v78 + 2 v79 + 2 v83 + v84 + v85 + v86 + 2 v87 + v89 + v90 + v91 + 2 v95 + 4 v97 + v102 + 2 v103 + v105 + 3 v106 + v107 + v108 + v109 + 3 v111 + 3 v112 <= 72
D44: v4 + 2 v5 + 3 v6 + 4 v7 + 3 v8 + 3 v9 + 2 v10 + 4 v11 + v12 + v14 + 2 v15 + 2 v16 + v17 + v18 + v19 + v22 + v23 + v24 + v25 + 3 v26 + 2 v27 + v28 + v29 + v30 + v31 + v33 + v34 + v35 + v36 + v37 + 3 v38 + v39 + v42 + v44 + 2 v45 + v47 + v48 + 3 v51 + 2 v53 + 3 v55 + v56 + 2 v57 + v58 + v59 + v60 + 2 v64 + v65 + 2 v66 + 3 v68 + 2 v69 + 3 v70 + v71 + 2 v73 + 2 v74 + v76 + 2 v77 + v78 + 2 v79 + 2 v83 + v84 + v85 + v86 + 2 v87 + v89 + v90 + v91 + 2 v95 + 4 v97 + v102 + 2 v103 + v105 + 3 v106 + v107 + v108 + v109 + 3 v111 + 3 v112 >= 57
C45: v2 + 2 v3 + v5 + v7 + 2 v8 + v10 + v13 + v14 + 2 v17 + 5 v18 + 3 v21 + v22 + 2 v23 + 4 v26 + 2 v27 + 2 v28 + 3 v29 + v30 + v31 + v32 + v33 + 2 v34 + v36 + v37 + v39 + v42 + v43 + v45 + v46 + v47 + v48 + v49 + v50 + 3 v52 + v53 + v55 + v56 + v57 + v59 + 2 v60 + v61 + 3 v62 + v63 + 2 v64 + v67 + 3 v68 + 2 v69 + 4 v70 + v71 + 2 v72 + 2 v73 + 2 v76 + 2 v77 + v78 + 2 v79 + v80 + v81 + v83 + 2 v84 + v88 + v90 + v91 + v92 + 2 v94 + 3 v95 + v97 + 3 v98 + 3 v99 + v100 + 3 v101 + 2 v102 + 2 v103 + v104 + 2 v105 + v107 + v108 + 3 v110 + 2 v112 <= 72
D45: v2 + 2 v3 + v5 + v7 + 2 v8 + v10 + v13 + v14 + 2 v17 + 5 v18 + 3 v21 + v22 + 2 v23 + 4 v26 + 2 v27 + 2 v28 + 3 v29 + v30 + v31 + v32 + v33 + 2 v34 + v36 + v37 + v39 + v42 + v43 + v45 + v46 + v47 + v48 + v49 + v50 + 3 v52 + v53 + v55 + v56 + v57 + v59 + 2 v60 + v61 + 3 v62 + v63 + 2 v64 + v67 + 3 v68 + 2 v69 + 4 v70 + v71 + 2 v72 + 2 v73 + 2 v76 + 2 v77 + v78 + 2 v79 + v80 + v81 + v83 + 2 v84 + v88 + v90 + v91 + v92 + 2 v94 + 3 v95 + v97 + 3 v98 + 3 v99 + v100 + 3 v101 + 2 v102 + 2 v103 + v104 + 2 v105 + v107 + v108 + 3 v110 + 2 v112 >= 57
C46: v4 + 2 v6 + v8 + v9 + 2 v11 + v12 + v13 + 3 v15 + 2 v16 + 2 v17 + v19 + v20 + 3 v21 + v22 + v23 + v24 + 2 v25 + v26 + 2 v27 + v28 + 3 v29 + 2 v30 + v32 + v33 + 2 v34 + v35 + 2 v36 + 3 v39 + 3 v41 + 2 v42 + 2 v43 + v44 + v46 + 2 v47 + 2 v50 + v51 + 2 v52 + 2 v54 + v56 + 3 v57 + 2 v58 + v60 + v61 + 3 v63 + v64 + 4 v65 + v66 + v68 + 3 v69 + v71 + 2 v74 + v76 + v77 + v78 + 3 v79 + 2 v80 + 2 v81 + 2 v84 + 2 v87 + 2 v89 + v90 + v91 + v95 + 2 v96 + 3 v99 + 2 v100 + 4 v102 + v103 + v104 + v105 + v106 + 4 v108 + v110 + v111 + 2 v112 <= 72
D46: v4 + 2 v6 + v8 + v9 + 2 v11 + v12 + v13 + 3 v15 + 2 v16 + 2 v17 + v19 + v20 + 3 v21 + v22 + v23 + v24 + 2 v25 + v26 + 2 v27 + v28 + 3 v29 + 2 v30 + v32 + v33 + 2 v34 + v35 + 2 v36 + 3 v39 + 3 v41 + 2 v42 + 2 v43 + v44 + v46 + 2 v47 + 2 v50 + v51 + 2 v52 + 2 v54 + v56 + 3 v57 + 2 v58 + v60 + v61 + 3 v63 + v64 + 4 v65 + v66 + v68 + 3 v69 + v71 + 2 v74 + v76 + v77 + v78 + 3 v79 + 2 v80 + 2 v81 + 2 v84 + 2 v87 + 2 v89 + v90 + v91 + v95 + 2 v96 + 3 v99 + 2 v100 + 4 v102 + v103 + v104 + v105 + v106 + 4 v108 + v110 + v111 + 2 v112 >= 57
C47: v3 + v4 + v5 + v6 + v11 + 4 v12 + v13 + v14 + 2 v15 + v17 + v18 + v20 + v21 + v22 + v23 + 4 v24 + v25 + 4 v26 + v28 + v30 + 2 v31 + v33 + v35 + 2 v37 + v38 + v39 + 4 v41 + v44 + v45 + v47 + v48 + v49 + 3 v51 + v54 + 2 v55 + v57 + 5 v58 + v59 + 2 v61 + v62 + v63 + v64 + v65 + 2 v66 + 2 v67 + 2 v70 + v71 + v72 + 2 v73 + v74 + 2 v75 + 3 v77 + 2 v78 + 3 v79 + v80 + v81 + v82 + 3 v84 + 2 v86 + v87 + v88 + v89 + v90 + 2 v91 + v92 + 3 v94 + 2 v97 + v98 + 2 v99 + 3 v101 + v102 + 2 v104 + v105 + v106 + 2 v107 + 2 v108 + 2 v109 + 2 v110 + v112 + 2 v113 <= 72
D47: v3 + v4 + v5 + v6 + v11 + 4 v12 + v13 + v14 + 2 v15 + v17 + v18 + v20 + v21 + v22 + v23 + 4 v24 + v25 + 4 v26 + v28 + v30 + 2 v31 + v33 + v35 + 2 v37 + v38 + v39 + 4 v41 + v44 + v45 + v47 + v48 + v49 + 3 v51 + v54 + 2 v55 + v57 + 5 v58 + v59 + 2 v61 + v62 + v63 + v64 + v65 + 2 v66 + 2 v67 + 2 v70 + v71 + v72 + 2 v73 + v74 + 2 v75 + 3 v77 + 2 v78 + 3 v79 + v80 + v81 + v82 + 3 v84 + 2 v86 + v87 + v88 + v89 + v90 + 2 v91 + v92 + 3 v94 + 2 v97 + v98 + 2 v99 + 3 v101 + v102 + 2 v104 + v105 + v106 + 2 v107 + 2 v108 + 2 v109 + 2 v110 + v112 + 2 v113 >= 57
C48: v1 + v2 + v3 + v4 + v5 + 2 v7 + v9 + 2 v10 + 2 v13 + 2 v16 + 2 v17 + v19 + v22 + v25 + 3 v26 + 2 v27 + v28 + v30 + 2 v31 + v33 + v34 + v35 + 2 v36 + 4 v38 + v39 + 2 v40 + 2 v41 + v42 + v43 + v44 + 2 v45 + v46 + v48 + v49 + 2 v51 + 5 v54 + v56 + 3 v57 + v59 + 2 v60 + 3 v61 + 3 v62 + 2 v63 + 3 v64 + 3 v66 + v68 + 2 v69 + v71 + v73 + 2 v74 + v75 + 2 v76 + v77 + v78 + 4 v80 + 2 v81 + v83 + 3 v84 + v85 + v86 + 2 v87 + 2 v88 + v89 + v90 + 2 v94 + v95 + 2 v97 + 2 v98 + 2 v99 + 2 v100 + v101 + v103 + 2 v104 + 3 v105 + v111 + 2 v113 <= 72
D48: v1 + v2 + v3 + v4 + v5 + 2 v7 + v9 + 2 v10 + 2 v13 + 2 v16 + 2 v17 + v19 + v22 + v25 + 3 v26 + 2 v27 + v28 + v30 + 2 v31 + v33 + v34 + v35 + 2 v36 + 4 v38 + v39 + 2 v40 + 2 v41 + v42 + v43 + v44 + 2 v45 + v46 + v48 + v49 + 2 v51 + 5 v54 + v56 + 3 v57 + v59 + 2 v60 + 3 v61 + 3 v62 + 2 v63 + 3 v64 + 3 v66 + v68 + 2 v69 + v71 + v73 + 2 v74 + v75 + 2 v76 + v77 + v78 + 4 v80 + 2 v81 + v83 + 3 v84 + v85 + v86 + 2 v87 + 2 v88 + v89 + v90 + 2 v94 + v95 + 2 v97 + 2 v98 + 2 v99 + 2 v100 + v101 + v103 + 2 v104 + 3 v105 + v111 + 2 v113 >= 57
C49: v1 + 2 v2 + 4 v4 + 3 v5 + v6 + 3 v8 + 3 v10 + 3 v12 + v13 + v15 + v16 + 2 v18 + v19 + v20 + 2 v22 + v24 + v25 + v26 + 2 v27 + v28 + 3 v29 + v30 + v31 + v32 + 4 v33 + 3 v36 + v37 + v38 + v39 + 2 v40 + v41 + 2 v42 + v43 + v44 + v46 + v47 + 2 v50 + v51 + v52 + v53 + v54 + 2 v55 + 3 v56 + v58 + v59 + v61 + 2 v63 + 2 v64 + v65 + v66 + v67 + 2 v68 + 2 v69 + v72 + 2 v73 + v74 + 2 v75 + 3 v76 + v78 + 2 v79 + 3 v80 + 2 v81 + v82 + v84 + v85 + v86 + v88 + v91 + v93 + 4 v94 + v96 + v97 + 2 v98 + 2 v101 + v103 + 4 v106 + v107 + 2 v108 + v109 + v112 <= 72
D49: v1 + 2 v2 + 4 v4 + 3 v5 + v6 + 3 v8 + 3 v10 + 3 v12 + v13 + v15 + v16 + 2 v18 + v19 + v20 + 2 v22 + v24 + v25 + v26 + 2 v27 + v28 + 3 v29 + v30 + v31 + v32 + 4 v33 + 3 v36 + v37 + v38 + v39 + 2 v40 + v41 + 2 v42 + v43 + v44 + v46 + v47 + 2 v50 + v51 + v52 + v53 + v54 + 2 v55 + 3 v56 + v58 + v59 + v61 + 2 v63 + 2 v64 + v65 + v66 + v67 + 2 v68 + 2 v69 + v72 + 2 v73 + v74 + 2 v75 + 3 v76 + v78 + 2 v79 + 3 v80 + 2 v81 + v82 + v84 + v85 + v86 + v88 + v91 + v93 + 4 v94 + v96 + v97 + 2 v98 + 2 v101 + v103 + 4 v106 + v107 + 2 v108 + v109 + v112 >= 57
C50: 2 v1 + v2 + v3 + v5 + 3 v6 + v7 + v9 + v11 + 2 v12 + 2 v13 + v14 + v15 + v16 + 2 v17 + 3 v18 + v20 + v21 + v22 + v23 + v26 + 4 v28 + v29 + v30 + 2 v31 + v32 + 2 v33 + v35 + 2 v36 + 2 v39 + v40 + 2 v41 + 6 v42 + v44 + v46 + v47 + 2 v49 + v50 + 2 v51 + v52 + v54 + v55 + v57 + 3 v58 + v60 + 2 v61 + v62 + v63 + v64 + v65 + 2 v69 + v70 + v71 + v72 + v73 + v75 + v76 + v77 + v78 + v79 + 2 v81 + v82 + 4 v83 + 2 v85 + 2 v86 + 2 v87 + 2 v88 + v89 + 2 v91 + v93 + v94 + 4 v95 + 2 v96 + 2 v97 + 2 v98 + v99 + v100 + 2 v105 + v106 + 2 v109 + v110 + 3 v111 + 2 v113 <= 72
D50: 2 v1 + v2 + v3 + v5 + 3 v6 + v7 + v9 + v11 + 2 v12 + 2 v13 + v14 + v15 + v16 + 2 v17 + 3 v18 + v20 + v21 + v22 + v23 + v26 + 4 v28 + v29 + v30 + 2 v31 + v32 + 2 v33 + v35 + 2 v36 + 2 v39 + v40 + 2 v41 + 6 v42 + v44 + v46 + v47 + 2 v49 + v50 + 2 v51 + v52 + v54 + v55 + v57 + 3 v58 + v60 + 2 v61 + v62 + v63 + v64 + v65 + 2 v69 + v70 + v71 + v72 + v73 + v75 + v76 + v77 + v78 + v79 + 2 v81 + v82 + 4 v83 + 2 v85 + 2 v86 + 2 v87 + 2 v88 + v89 + 2 v91 + v93 + v94 + 4 v95 + 2 v96 + 2 v97 + 2 v98 + v99 + v100 + 2 v105 + v106 + 2 v109 + v110 + 3 v111 + 2 v113 >= 57
C51: v2 + v3 + 2 v4 + v7 + 2 v8 + v9 + 3 v11 + v12 + 2 v13 + 3 v14 + v15 + v19 + v20 + 2 v21 + v22 + 3 v23 + v24 + 2 v26 + 2 v27 + v30 + v31 + v32 + 2 v34 + v35 + v36 + v37 + v38 + v39 + v40 + 2 v41 + 3 v42 + v44 + 2 v45 + 2 v48 + v49 + 2 v50 + v51 + 3 v52 + v53 + 2 v54 + 2 v55 + v56 + 2 v57 + 2 v59 + 3 v60 + v61 + v62 + v64 + v65 + 2 v69 + 2 v71 + v72 + 2 v73 + 2 v74 + 3 v75 + v78 + 4 v79 + v80 + 2 v81 + 2 v82 + 2 v84 + 2 v85 + v86 + v87 + v89 + v90 + v92 + v93 + 2 v95 + 3 v98 + v100 + 3 v103 + 2 v106 + 4 v107 + v108 + v110 + 4 v113 <= 72
D51: v2 + v3 + 2 v4 + v7 + 2 v8 + v9 + 3 v11 + v12 + 2 v13 + 3 v14 + v15 + v19 + v20 + 2 v21 + v22 + 3 v23 + v24 + 2 v26 + 2 v27 + v30 + v31 + v32 + 2 v34 + v35 + v36 + v37 + v38 + v39 + v40 + 2 v41 + 3 v42 + v44 + 2 v45 + 2 v48 + v49 + 2 v50 + v51 + 3 v52 + v53 + 2 v54 + 2 v55 + v56 + 2 v57 + 2 v59 + 3 v60 + v61 + v62 + v64 + v65 + 2 v69 + 2 v71 + v72 + 2 v73 + 2 v74 + 3 v75 + v78 + 4 v79 + v80 + 2 v81 + 2 v82 + 2 v84 + 2 v85 + v86 + v87 + v89 + v90 + v92 + v93 + 2 v95 + 3 v98 + v100 + 3 v103 + 2 v106 + 4 v107 + v108 + v110 + 4 v113 >= 57
C52: 3 v3 + 2 v4 + 2 v7 + v9 + v11 + v12 + v13 + 2 v14 + v15 + 5 v16 + 2 v17 + 4 v18 + v19 + v21 + 2 v22 + v23 + v25 + v26 + 3 v27 + v28 + 2 v29 + 2 v30 + v31 + 4 v32 + v34 + 3 v35 + 2 v38 + 2 v41 + 2 v42 + 3 v43 + v45 + 3 v46 + 2 v47 + v48 + 2 v49 + v50 + v53 + v54 + 3 v55 + v57 + 3 v58 + 3 v59 + v60 + v61 + v63 + v64 + v65 + v66 + 2 v68 + v71 + v73 + v74 + 2 v75 + v78 + 2 v79 + 2 v80 + v81 + v83 + v87 + v88 + v89 + v90 + 3 v92 + 2 v94 + 2 v96 + 2 v97 + v98 + v100 + 3 v101 + v103 + v104 + v106 + v107 + v108 + v109 + 2 v111 + v112 + 2 v113 <= 72
D52: 3 v3 + 2 v4 + 2 v7 + v9 + v11 + v12 + v13 + 2 v14 + v15 + 5 v16 + 2 v17 + 4 v18 + v19 + v21 + 2 v22 + v23 + v25 + v26 + 3 v27 + v28 + 2 v29 + 2 v30 + v31 + 4 v32 + v34 + 3 v35 + 2 v38 + 2 v41 + 2 v42 + 3 v43 + v45 + 3 v46 + 2 v47 + v48 + 2 v49 + v50 + v53 + v54 + 3 v55 + v57 + 3 v58 + 3 v59 + v60 + v61 + v63 + v64 + v65 + v66 + 2 v68 + v71 + v73 + v74 + 2 v75 + v78 + 2 v79 + 2 v80 + v81 + v83 + v87 + v88 + v89 + v90 + 3 v92 + 2 v94 + 2 v96 + 2 v97 + v98 + v100 + 3 v101 + v103 + v104 + v106 + v107 + v108 + v109 + 2 v111 + v112 + 2 v113 >= 57
C53: 2 v1 + 2 v3 + 2 v4 + 2 v5 + 2 v6 + 2 v7 + 2 v8 + v9 + v12 + 2 v14 + 2 v15 + v16 + v17 + v18 + 3 v19 + v22 + 2 v23 + v26 + 2 v27 + 2 v28 + v31 + v33 + v34 + v35 + v36 + 2 v37 + 2 v39 + v41 + 3 v44 + 2 v45 + v48 + v49 + 3 v50 + 2 v53 + 2 v54 + v55 + v56 + 2 v57 + 2 v58 + 3 v59 + v60 + v62 + v63 + v65 + v66 + 2 v68 + v69 + v70 + v71 + 2 v72 + v73 + v77 + 4 v78 + v79 + v81 + 2 v84 + v85 + v87 + 5 v88 + 2 v90 + v92 + v93 + 3 v94 + 2 v96 + v97 + v98 + 2 v99 + 5 v100 + 2 v102 + v104 + v105 + 2 v106 + v107 + v108 + v109 + 2 v110 + 2 v111 + v112 + v113 <= 72
D53: 2 v1 + 2 v3 + 2 v4 + 2 v5 + 2 v6 + 2 v7 + 2 v8 + v9 + v12 + 2 v14 + 2 v15 + v16 + v17 + v18 + 3 v19 + v22 + 2 v23 + v26 + 2 v27 + 2 v28 + v31 + v33 + v34 + v35 + v36 + 2 v37 + 2 v39 + v41 + 3 v44 + 2 v45 + v48 + v49 + 3 v50 + 2 v53 + 2 v54 + v55 + v56 + 2 v57 + 2 v58 + 3 v59 + v60 + v62 + v63 + v65 + v66 + 2 v68 + v69 + v70 + v71 + 2 v72 + v73 + v77 + 4 v78 + v79 + v81 + 2 v84 + v85 + v87 + 5 v88 + 2 v90 + v92 + v93 + 3 v94 + 2 v96 + v97 + v98 + 2 v99 + 5 v100 + 2 v102 + v104 + v105 + 2 v106 + v107 + v108 + v109 + 2 v110 + 2 v111 + v112 + v113 >= 57
C54: 3 v1 + v2 + 3 v3 + v4 + v5 + v6 + v7 + 2 v8 + 3 v9 + v11 + v12 + v14 + v15 + v17 + v18 + 3 v20 + v22 + 2 v23 + 3 v24 + 2 v25 + v28 + v29 + v30 + v31 + 3 v32 + v35 + v36 + v37 + 5 v38 + 2 v39 + v40 + v41 + 2 v42 + 2 v43 + v44 + v48 + v50 + v51 + 2 v52 + v55 + v56 + 3 v59 + 2 v61 + v62 + v63 + 3 v64 + 2 v65 + v66 + 2 v68 + v69 + v70 + v71 + v72 + 3 v74 + 3 v75 + v76 + v77 + 2 v81 + v82 + v84 + 2 v88 + 2 v90 + 3 v91 + v93 + 2 v94 + 2 v95 + 2 v97 + 3 v99 + v100 + 2 v101 + 3 v102 + 2 v103 + v104 + v108 + 2 v110 + 2 v111 + v112 + 2 v113 <= 72
D54: 3 v1 + v2 + 3 v3 + v4 + v5 + v6 + v7 + 2 v8 + 3 v9 + v11 + v12 + v14 + v15 + v17 + v18 + 3 v20 + v22 + 2 v23 + 3 v24 + 2 v25 + v28 + v29 + v30 + v31 + 3 v32 + v35 + v36 + v37 + 5 v38 + 2 v39 + v40 + v41 + 2 v42 + 2 v43 + v44 + v48 + v50 + v51 + 2 v52 + v55 + v56 + 3 v59 + 2 v61 + v62 + v63 + 3 v64 + 2 v65 + v66 + 2 v68 + v69 + v70 + v71 + v72 + 3 v74 + 3 v75 + v76 + v77 + 2 v81 + v82 + v84 + 2 v88 + 2 v90 + 3 v91 + v93 + 2 v94 + 2 v95 + 2 v97 + 3 v99 + v100 + 2 v101 + 3 v102 + 2 v103 + v104 + v108 + 2 v110 + 2 v111 + v112 + 2 v113 >= 57
C55: 2 v1 + 2 v4 + 2 v5 + 2 v6 + 2 v9 + v10 + 2 v11 + v12 + v13 + 2 v14 + 3 v16 + v19 + v20 + v21 + v22 + v24 + v25 + v26 + v29 + 2 v30 + v31 + v32 + 2 v33 + 2 v34 + v35 + v37 + v38 + v39 + v42 + 2 v45 + v46 + 5 v47 + v48 + v49 + 2 v50 + v51 + 2 v52 + 3 v55 + 3 v56 + 2 v57 + v58 + v60 + 3 v62 + v63 + v64 + v66 + 2 v67 + 2 v68 + 5 v71 + 2 v72 + v74 + v75 + 2 v76 + 2 v77 + v79 + v80 + 2 v81 + v83 + 2 v86 + 2 v87 + v88 + 3 v90 + v93 + 2 v94 + 2 v95 + v96 + v97 + 2 v99 + 2 v100 + 2 v101 + v104 + 3 v105 + v107 + 2 v108 + v109 + v110 + 2 v112 + 3 v113 <= 72
D55: 2 v1 + 2 v4 + 2 v5 + 2 v6 + 2 v9 + v10 + 2 v11 + v12 + v13 + 2 v14 + 3 v16 + v19 + v20 + v21 + v22 + v24 + v25 + v26 + v29 + 2 v30 + v31 + v32 + 2 v33 + 2 v34 + v35 + v37 + v38 + v39 + v42 + 2 v45 + v46 + 5 v47 + v48 + v49 + 2 v50 + v51 + 2 v52 + 3 v55 + 3 v56 + 2 v57 + v58 + v60 + 3 v62 + v63 + v64 + v66 + 2 v67 + 2 v68 + 5 v71 + 2 v72 + v74 + v75 + 2 v76 + 2 v77 + v79 + v80 + 2 v81 + v83 + 2 v86 + 2 v87 + v88 + 3 v90 + v93 + 2 v94 + 2 v95 + v96 + v97 + 2 v99 + 2 v100 + 2 v101 + v104 + 3 v105 + v107 + 2 v108 + v109 + v110 + 2 v112 + 3 v113 >= 57
C56: v3 + 2 v4 + v5 + 2 v7 + v8 + 2 v9 + 3 v11 + 3 v13 + v15 + v17 + v18 + v19 + 2 v20 + v21 + 2 v22 + 3 v23 + 2 v28 + 2 v30 + 2 v32 + 2 v33 + v36 + v37 + 3 v39 + 3 v43 + v44 + 2 v46 + 2 v48 + v49 + 2 v50 + 3 v51 + v52 + v53 + 3 v54 + 4 v55 + 3 v56 + v57 + v58 + v59 + v60 + 4 v61 + 2 v62 + 2 v64 + v65 + v66 + 2 v67 + v69 + v70 + v71 + 2 v72 + v73 + v74 + v75 + v78 + 2 v80 + v83 + 2 v84 + v85 + v86 + v88 + v90 + v92 + v94 + 2 v95 + v96 + v97 + v98 + v100 + v101 + v103 + 2 v104 + v105 + v106 + 4 v108 + 4 v109 + 3 v110 + 2 v111 + 2 v112 <= 72
D56: v3 + 2 v4 + v5 + 2 v7 + v8 + 2 v9 + 3 v11 + 3 v13 + v15 + v17 + v18 + v19 + 2 v20 + v21 + 2 v22 + 3 v23 + 2 v28 + 2 v30 + 2 v32 + 2 v33 + v36 + v37 + 3 v39 + 3 v43 + v44 + 2 v46 + 2 v48 + v49 + 2 v50 + 3 v51 + v52 + v53 + 3 v54 + 4 v55 + 3 v56 + v57 + v58 + v59 + v60 + 4 v61 + 2 v62 + 2 v64 + v65 + v66 + 2 v67 + v69 + v70 + v71 + 2 v72 + v73 + v74 + v75 + v78 + 2 v80 + v83 + 2 v84 + v85 + v86 + v88 + v90 + v92 + v94 + 2 v95 + v96 + v97 + v98 + v100 + v101 + v103 + 2 v104 + v105 + v106 + 4 v108 + 4 v109 + 3 v110 + 2 v111 + 2 v112 >= 57
C57: 3 v2 + 2 v3 + 2 v6 + v8 + v9 + v10 + 2 v12 + v13 + 2 v14 + 2 v15 + 3 v16 + 2 v18 + 2 v19 + 4 v20 + v21 + 2 v22 + v23 + 2 v24 + 2 v25 + v26 + v27 + 2 v28 + 2 v29 + v30 + v33 + v35 + v37 + v38 + v40 + 2 v41 + v42 + v43 + v44 + v45 + v47 + 3 v48 + v50 + v52 + v53 + 3 v54 + 3 v55 + 2 v56 + 4 v57 + v60 + 3 v62 + v63 + v67 + v68 + v69 + v70 + v71 + v73 + v75 + v76 + 2 v77 + 2 v80 + v82 + 2 v84 + v85 + v86 + 2 v88 + v89 + 5 v91 + v94 + v95 + 3 v96 + 2 v97 + 2 v98 + v99 + 2 v100 + 3 v103 + 2 v107 + v108 + 2 v109 + 2 v111 + 3 v112 + v113 <= 72
D57: 3 v2 + 2 v3 + 2 v6 + v8 + v9 + v10 + 2 v12 + v13 + 2 v14 + 2 v15 + 3 v16 + 2 v18 + 2 v19 + 4 v20 + v21 + 2 v22 + v23 + 2 v24 + 2 v25 + v26 + v27 + 2 v28 + 2 v29 + v30 + v33 + v35 + v37 + v38 + v40 + 2 v41 + v42 + v43 + v44 + v45 + v47 + 3 v48 + v50 + v52 + v53 + 3 v54 + 3 v55 + 2 v56 + 4 v57 + v60 + 3 v62 + v63 + v67 + v68 + v69 + v70 + v71 + v73 + v75 + v76 + 2 v77 + 2 v80 + v82 + 2 v84 + v85 + v86 + 2 v88 + v89 + 5 v91 + v94 + v95 + 3 v96 + 2 v97 + 2 v98 + v99 + 2 v100 + 3 v103 + 2 v107 + v108 + 2 v109 + 2 v111 + 3 v112 + v113 >= 57
C58: v1 + v2 + 2 v3 + v5 + v6 + 2 v8 + v9 + v10 + 2 v11 + 4 v12 + v13 + v14 + v17 + v18 + v20 + v21 + 2 v22 + v23 + v24 + v25 + 2 v26 + v29 + v30 + 2 v31 + 2 v32 + v35 + v36 + 2 v37 + v38 + v42 + 2 v43 + v44 + 3 v45 + v46 + 3 v47 + v49 + 2 v50 + v51 + 2 v52 + 2 v54 + v55 + 4 v56 + 2 v57 + 3 v60 + 4 v61 + v62 + v63 + v64 + 3 v66 + v67 + 2 v68 + 2 v69 + v70 + v73 + v76 + 2 v78 + 2 v79 + 2 v81 + v82 + 3 v85 + v86 + 3 v87 + v88 + 3 v91 + 4 v92 + v95 + 2 v96 + 2 v97 + 3 v100 + 2 v101 + 3 v102 + v104 + 2 v106 + v109 + v110 + v111 + v113 <= 72
D58: v1 + v2 + 2 v3 + v5 + v6 + 2 v8 + v9 + v10 + 2 v11 + 4 v12 + v13 + v14 + v17 + v18 + v20 + v21 + 2 v22 + v23 + v24 + v25 + 2 v26 + v29 + v30 + 2 v31 + 2 v32 + v35 + v36 + 2 v37 + v38 + v42 + 2 v43 + v44 + 3 v45 + v46 + 3 v47 + v49 + 2 v50 + v51 + 2 v52 + 2 v54 + v55 + 4 v56 + 2 v57 + 3 v60 + 4 v61 + v62 + v63 + v64 + 3 v66 + v67 + 2 v68 + 2 v69 + v70 + v73 + v76 + 2 v78 + 2 v79 + 2 v81 + v82 + 3 v85 + v86 + 3 v87 + v88 + 3 v91 + 4 v92 + v95 + 2 v96 + 2 v97 + 3 v100 + 2 v101 + 3 v102 + v104 + 2 v106 + v109 + v110 + v111 + v113 >= 57
C59: v2 + 2 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v8 + 4 v9 + v10 + v11 + 2 v12 + 2 v14 + v15 + 2 v19 + 3 v20 + 3 v21 + v22 + 3 v23 + 3 v25 + v26 + 2 v27 + 3 v28 + v29 + v30 + v31 + v32 + v33 + v36 + v37 + v40 + v41 + v42 + v43 + 2 v45 + 5 v46 + v48 + 3 v49 + 3 v51 + 2 v52 + v54 + v55 + 2 v58 + v60 + v62 + v64 + v65 + 3 v66 + 2 v67 + 2 v68 + v69 + v70 + v71 + v73 + v74 + v75 + 2 v76 + v79 + v80 + 3 v81 + v82 + v84 + v88 + 2 v89 + v90 + v91 + v92 + v94 + 2 v97 + 3 v98 + 2 v99 + 3 v100 + v102 + 2 v105 + 2 v106 + v109 + v110 + 2 v112 + 2 v113 + v114 <= 72
D59: v2 + 2 v3 + 2 v4 + 2 v5 + 2 v6 + v7 + v8 + 4 v9 + v10 + v11 + 2 v12 + 2 v14 + v15 + 2 v19 + 3 v20 + 3 v21 + v22 + 3 v23 + 3 v25 + v26 + 2 v27 + 3 v28 + v29 + v30 + v31 + v32 + v33 + v36 + v37 + v40 + v41 + v42 + v43 + 2 v45 + 5 v46 + v48 + 3 v49 + 3 v51 + 2 v52 + v54 + v55 + 2 v58 + v60 + v62 + v64 + v65 + 3 v66 + 2 v67 + 2 v68 + v69 + v70 + v71 + v73 + v74 + v75 + 2 v76 + v79 + v80 + 3 v81 + v82 + v84 + v88 + 2 v89 + v90 + v91 + v92 + v94 + 2 v97 + 3 v98 + 2 v99 + 3 v100 + v102 + 2 v105 + 2 v106 + v109 + v110 + 2 v112 + 2 v113 + v114 >= 57
C60: v1 + v2 + 2 v3 + v4 + 2 v5 + 3 v6 + 2 v7 + v8 + v9 + v11 + v13 + 2 v14 + v15 + 3 v17 + 3 v18 + 4 v19 + v21 + v22 + 3 v23 + v24 + v25 + v26 + v27 + v28 + v31 + v32 + v33 + v35 + v36 + 2 v38 + 2 v40 + 2 v41 + v43 + v44 + v46 + v47 + v48 + 2 v50 + 3 v51 + 3 v52 + 3 v53 + v55 + v60 + 3 v61 + v62 + 5 v63 + v64 + v66 + 4 v67 + v68 + 3 v71 + v74 + 2 v75 + 2 v76 + 2 v78 + 2 v79 + v81 + v83 + 2 v84 + v85 + 3 v87 + v89 + 2 v91 + 2 v94 + v95 + 3 v96 + v97 + v100 + v101 + v102 + 2 v103 + v104 + 2 v105 + v106 + 2 v107 + v108 + v109 + v112 + v113 <= 72
D60: v1 + v2 + 2 v3 + v4 + 2 v5 + 3 v6 + 2 v7 + v8 + v9 + v11 + v13 + 2 v14 + v15 + 3 v17 + 3 v18 + 4 v19 + v21 + v22 + 3 v23 + v24 + v25 + v26 + v27 + v28 + v31 + v32 + v33 + v35 + v36 + 2 v38 + 2 v40 + 2 v41 + v43 + v44 + v46 + v47 + v48 + 2 v50 + 3 v51 + 3 v52 + 3 v53 + v55 + v60 + 3 v61 + v62 + 5 v63 + v64 + v66 + 4 v67 + v68 + 3 v71 + v74 + 2 v75 + 2 v76 + 2 v78 + 2 v79 + v81 + v83 + 2 v84 + v85 + 3 v87 + v89 + 2 v91 + 2 v94 + v95 + 3 v96 + v97 + v100 + v101 + v102 + 2 v103 + v104 + 2 v105 + v106 + 2 v107 + v108 + v109 + v112 + v113 >= 57
C61: 2 v2 + 2 v3 + 4 v4 + 3 v6 + 2 v7 + v8 + v9 + 2 v10 + v11 + v14 + v15 + v16 + v17 + v18 + v19 + 3 v21 + v23 + v25 + v26 + 2 v28 + v29 + 3 v30 + v31 + v32 + 3 v33 + 2 v36 + v37 + 3 v38 + 3 v40 + 2 v41 + v42 + v43 + 2 v44 + v45 + 2 v47 + v49 + 3 v50 + v51 + v52 + v54 + v55 + v56 + 3 v57 + v58 + v59 + 2 v60 + v61 + v62 + v63 + 3 v64 + 3 v65 + v66 + 2 v68 + v69 + 3 v70 + 2 v71 + 3 v72 + 2 v75 + 3 v77 + 2 v78 + v84 + v85 + v86 + v89 + v91 + 2 v92 + 2 v96 + v97 + 2 v98 + v101 + 2 v102 + 2 v104 + v107 + 3 v109 + v110 + 3 v113 + v114 <= 72
D61: 2 v2 + 2 v3 + 4 v4 + 3 v6 + 2 v7 + v8 + v9 + 2 v10 + v11 + v14 + v15 + v16 + v17 + v18 + v19 + 3 v21 + v23 + v25 + v26 + 2 v28 + v29 + 3 v30 + v31 + v32 + 3 v33 + 2 v36 + v37 + 3 v38 + 3 v40 + 2 v41 + v42 + v43 + 2 v44 + v45 + 2 v47 + v49 + 3 v50 + v51 + v52 + v54 + v55 + v56 + 3 v57 + v58 + v59 + 2 v60 + v61 + v62 + v63 + 3 v64 + 3 v65 + v66 + 2 v68 + v69 + 3 v70 + 2 v71 + 3 v72 + 2 v75 + 3 v77 + 2 v78 + v84 + v85 + v86 + v89 + v91 + 2 v92 + 2 v96 + v97 + 2 v98 + v101 + 2 v102 + 2 v104 + v107 + 3 v109 + v110 + 3 v113 + v114 >= 57
C62: 3 v1 + v2 + 2 v5 + v6 + v8 + 2 v9 + 2 v10 + v11 + 2 v12 + v14 + v15 + 2 v17 + v18 + v20 + 2 v21 + 2 v22 + 2 v23 + v25 + v26 + 2 v27 + 2 v28 + 2 v29 + v33 + v35 + v36 + v37 + 2 v38 + 3 v39 + 2 v40 + v41 + v44 + v45 + 2 v46 + 3 v47 + v48 + 2 v49 + v50 + v51 + 2 v53 + 4 v55 + 4 v57 + 3 v59 + v60 + 4 v61 + v65 + v66 + v67 + v68 + v69 + v72 + v73 + 2 v75 + v76 + v77 + v79 + 2 v81 + v82 + 2 v83 + v84 + 3 v86 + 2 v87 + 2 v89 + 3 v90 + 2 v94 + 2 v96 + 4 v98 + v99 + v100 + v101 + 3 v102 + 2 v103 + 3 v104 + 2 v107 + v109 + v111 + v112 <= 72
D62: 3 v1 + v2 + 2 v5 + v6 + v8 + 2 v9 + 2 v10 + v11 + 2 v12 + v14 + v15 + 2 v17 + v18 + v20 + 2 v21 + 2 v22 + 2 v23 + v25 + v26 + 2 v27 + 2 v28 + 2 v29 + v33 + v35 + v36 + v37 + 2 v38 + 3 v39 + 2 v40 + v41 + v44 + v45 + 2 v46 + 3 v47 + v48 + 2 v49 + v50 + v51 + 2 v53 + 4 v55 + 4 v57 + 3 v59 + v60 + 4 v61 + v65 + v66 + v67 + v68 + v69 + v72 + v73 + 2 v75 + v76 + v77 + v79 + 2 v81 + v82 + 2 v83 + v84 + 3 v86 + 2 v87 + 2 v89 + 3 v90 + 2 v94 + 2 v96 + 4 v98 + v99 + v100 + v101 + 3 v102 + 2 v103 + 3 v104 + 2 v107 + v109 + v111 + v112 >= 57
C63: v1 + v2 + 2 v3 + 2 v5 + v6 + 2 v7 + 3 v8 + 2 v9 + v11 + v13 + 5 v14 + v16 + v17 + 2 v18 + 2 v19 + v21 + 3 v22 + 3 v24 + 2 v25 + v27 + 2 v28 + v29 + 2 v31 + v32 + v34 + 2 v36 + 2 v39 + 2 v40 + 3 v41 + v42 + 3 v44 + v46 + 3 v47 + v49 + v50 + v52 + v53 + 3 v54 + 2 v55 + 3 v56 + v57 + v58 + v59 + v60 + v63 + 3 v64 + v65 + v66 + v67 + v69 + v70 + v72 + 3 v73 + 2 v74 + v77 + v80 + v81 + 3 v82 + v83 + 2 v84 + v85 + 3 v87 + v89 + 2 v90 + v92 + v94 + 2 v95 + v97 + v98 + 2 v99 + v100 + 3 v101 + v102 + v105 + v107 + v108 + 3 v109 + v112 + v114 <= 72
D63: v1 + v2 + 2 v3 + 2 v5 + v6 + 2 v7 + 3 v8 + 2 v9 + v11 + v13 + 5 v14 + v16 + v17 + 2 v18 + 2 v19 + v21 + 3 v22 + 3 v24 + 2 v25 + v27 + 2 v28 + v29 + 2 v31 + v32 + v34 + 2 v36 + 2 v39 + 2 v40 + 3 v41 + v42 + 3 v44 + v46 + 3 v47 + v49 + v50 + v52 + v53 + 3 v54 + 2 v55 + 3 v56 + v57 + v58 + v59 + v60 + v63 + 3 v64 + v65 + v66 + v67 + v69 + v70 + v72 + 3 v73 + 2 v74 + v77 + v80 + v81 + 3 v82 + v83 + 2 v84 + v85 + 3 v87 + v89 + 2 v90 + v92 + v94 + 2 v95 + v97 + v98 + 2 v99 + v100 + 3 v101 + v102 + v105 + v107 + v108 + 3 v109 + v112 + v114 >= 57
C64: 2 v1 + 2 v2 + v4 + 3 v5 + v6 + v7 + v8 + v9 + v10 + 2 v11 + v16 + 2 v17 + 2 v18 + 2 v20 + 2 v21 + 2 v23 + v24 + 3 v25 + 3 v26 + v27 + v28 + 5 v30 + v31 + 2 v32 + v33 + v35 + 2 v36 + v37 + v39 + v40 + 2 v41 + 2 v42 + v44 + 3 v45 + v46 + 2 v47 + 2 v48 + v49 + v51 + v52 + v53 + v54 + v56 + v57 + 5 v59 + v60 + v62 + v65 + v66 + 3 v67 + 2 v69 + v70 + v72 + v73 + 4 v74 + v77 + v78 + v79 + 2 v80 + 2 v85 + 3 v87 + 2 v88 + v90 + 2 v91 + v92 + 3 v94 + v95 + 3 v96 + v98 + v99 + v102 + v103 + 2 v105 + v106 + v107 + v108 + 3 v109 + v110 + v112 + v113 <= 72
D64: 2 v1 + 2 v2 + v4 + 3 v5 + v6 + v7 + v8 + v9 + v10 + 2 v11 + v16 + 2 v17 + 2 v18 + 2 v20 + 2 v21 + 2 v23 + v24 + 3 v25 + 3 v26 + v27 + v28 + 5 v30 + v31 + 2 v32 + v33 + v35 + 2 v36 + v37 + v39 + v40 + 2 v41 + 2 v42 + v44 + 3 v45 + v46 + 2 v47 + 2 v48 + v49 + v51 + v52 + v53 + v54 + v56 + v57 + 5 v59 + v60 + v62 + v65 + v66 + 3 v67 + 2 v69 + v70 + v72 + v73 + 4 v74 + v77 + v78 + v79 + 2 v80 + 2 v85 + 3 v87 + 2 v88 + v90 + 2 v91 + v92 + 3 v94 + v95 + 3 v96 + v98 + v99 + v102 + v103 + 2 v105 + v106 + v107 + v108 + 3 v109 + v110 + v112 + v113 >= 57
C65: 2 v2 + v3 + 2 v4 + 2 v5 + v6 + v7 + v8 + v10 + v12 + v14 + v15 + v16 + 2 v17 + v18 + 3 v19 + v20 + 3 v21 + 3 v24 + v26 + 3 v27 + 2 v28 + v30 + v32 + 2 v35 + 2 v36 + v37 + v38 + 3 v39 + v40 + v42 + 2 v43 + 2 v44 + v45 + v46 + 3 v47 + 2 v48 + v49 + v50 + v51 + 3 v53 + v54 + 2 v55 + v57 + v58 + v59 + 3 v60 + 3 v62 + 2 v64 + 2 v65 + v66 + v69 + v70 + v73 + v74 + v75 + v76 + v80 + 3 v81 + v82 + v83 + v84 + v86 + 2 v87 + v89 + v90 + 4 v91 + 2 v92 + v93 + v95 + v96 + 2 v97 + v101 + 4 v104 + 3 v105 + 3 v106 + v107 + v108 + 4 v110 + v112 + v113 <= 72
D65: 2 v2 + v3 + 2 v4 + 2 v5 + v6 + v7 + v8 + v10 + v12 + v14 + v15 + v16 + 2 v17 + v18 + 3 v19 + v20 + 3 v21 + 3 v24 + v26 + 3 v27 + 2 v28 + v30 + v32 + 2 v35 + 2 v36 + v37 + v38 + 3 v39 + v40 + v42 + 2 v43 + 2 v44 + v45 + v46 + 3 v47 + 2 v48 + v49 + v50 + v51 + 3 v53 + v54 + 2 v55 + v57 + v58 + v59 + 3 v60 + 3 v62 + 2 v64 + 2 v65 + v66 + v69 + v70 + v73 + v74 + v75 + v76 + v80 + 3 v81 + v82 + v83 + v84 + v86 + 2 v87 + v89 + v90 + 4 v91 + 2 v92 + v93 + v95 + v96 + 2 v97 + v101 + 4 v104 + 3 v105 + 3 v106 + v107 + v108 + 4 v110 + v112 + v113 >= 57
C66: 3 v3 + v4 + v6 + v7 + 4 v11 + 2 v13 + 2 v14 + 2 v15 + v16 + 2 v17 + 3 v18 + 2 v20 + v22 + 4 v25 + v29 + v31 + v33 + v35 + v36 + v38 + 4 v39 + 3 v40 + v42 + v43 + 4 v45 + v46 + v48 + v49 + v50 + v51 + v52 + 2 v53 + v55 + v58 + 3 v60 + v61 + v62 + v63 + 2 v64 + 2 v65 + 3 v66 + v67 + v68 + 2 v69 + v70 + 2 v72 + v73 + v74 + 2 v76 + 3 v77 + v79 + 2 v80 + 2 v82 + v83 + v84 + 2 v85 + 2 v86 + v88 + v89 + v90 + v91 + v92 + v93 + 2 v94 + 3 v96 + v97 + v98 + 2 v99 + 2 v100 + 2 v101 + v102 + 2 v104 + v105 + 2 v106 + 3 v107 + v108 + v109 + 2 v112 + v113 <= 72
D66: 3 v3 + v4 + v6 + v7 + 4 v11 + 2 v13 + 2 v14 + 2 v15 + v16 + 2 v17 + 3 v18 + 2 v20 + v22 + 4 v25 + v29 + v31 + v33 + v35 + v36 + v38 + 4 v39 + 3 v40 + v42 + v43 + 4 v45 + v46 + v48 + v49 + v50 + v51 + v52 + 2 v53 + v55 + v58 + 3 v60 + v61 + v62 + v63 + 2 v64 + 2 v65 + 3 v66 + v67 + v68 + 2 v69 + v70 + 2 v72 + v73 + v74 + 2 v76 + 3 v77 + v79 + 2 v80 + 2 v82 + v83 + v84 + 2 v85 + 2 v86 + v88 + v89 + v90 + v91 + v92 + v93 + 2 v94 + 3 v96 + v97 + v98 + 2 v99 + 2 v100 + 2 v101 + v102 + 2 v104 + v105 + 2 v106 + 3 v107 + v108 + v109 + 2 v112 + v113 >= 57
C67: 3 v1 + 2 v2 + v3 + 2 v4 + 2 v5 + v6 + v7 + 2 v8 + 2 v9 + 2 v11 + v12 + 2 v13 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + 2 v22 + 2 v23 + 2 v25 + 3 v26 + v28 + 2 v29 + 2 v34 + v36 + v37 + v39 + 5 v40 + 2 v43 + v45 + 2 v46 + 3 v47 + v48 + v51 + v52 + v53 + v54 + v55 + 3 v57 + 3 v58 + v59 + v60 + v61 + v62 + v63 + v64 + 3 v65 + v67 + v69 + 2 v71 + v72 + v75 + v76 + v77 + v78 + v80 + v82 + 2 v84 + v85 + 2 v87 + 4 v88 + 2 v89 + v91 + 2 v92 + 2 v95 + v97 + 2 v99 + 4 v101 + 3 v103 + v105 + 4 v106 + v107 + v109 + 2 v110 + 2 v111 + 2 v113 <= 72
D67: 3 v1 + 2 v2 + v3 + 2 v4 + 2 v5 + v6 + v7 + 2 v8 + 2 v9 + 2 v11 + v12 + 2 v13 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + 2 v22 + 2 v23 + 2 v25 + 3 v26 + v28 + 2 v29 + 2 v34 + v36 + v37 + v39 + 5 v40 + 2 v43 + v45 + 2 v46 + 3 v47 + v48 + v51 + v52 + v53 + v54 + v55 + 3 v57 + 3 v58 + v59 + v60 + v61 + v62 + v63 + v64 + 3 v65 + v67 + v69 + 2 v71 + v72 + v75 + v76 + v77 + v78 + v80 + v82 + 2 v84 + v85 + 2 v87 + 4 v88 + 2 v89 + v91 + 2 v92 + 2 v95 + v97 + 2 v99 + 4 v101 + 3 v103 + v105 + 4 v106 + v107 + v109 + 2 v110 + 2 v111 + 2 v113 >= 57
C68: v1 + v2 + v3 + v5 + v6 + v7 + v8 + v9 + 2 v10 + v11 + v12 + 3 v13 + 2 v14 + v15 + v16 + 2 v19 + 2 v20 + v21 + v22 + 2 v25 + v29 + v30 + v31 + v33 + v34 + v35 + v37 + v38 + 3 v39 + 2 v40 + v41 + v42 + v44 + 2 v46 + v48 + 2 v54 + 2 v55 + v56 + v57 + 2 v58 + 4 v59 + v61 + v62 + 3 v63 + v65 + v66 + 3 v68 + v69 + 4 v70 + v71 + v75 + 4 v76 + v78 + 3 v79 + v80 + v81 + v82 + v84 + 2 v85 + 3 v87 + v89 + v90 + v91 + 3 v92 + 3 v94 + 4 v95 + 2 v96 + v97 + v98 + v102 + v103 + 3 v104 + v105 + v106 + v107 + v108 + v109 + 3 v110 + v111 + 2 v112 + 3 v113 + v114 <= 72
D68: v1 + v2 + v3 + v5 + v6 + v7 + v8 + v9 + 2 v10 + v11 + v12 + 3 v13 + 2 v14 + v15 + v16 + 2 v19 + 2 v20 + v21 + v22 + 2 v25 + v29 + v30 + v31 + v33 + v34 + v35 + v37 + v38 + 3 v39 + 2 v40 + v41 + v42 + v44 + 2 v46 + v48 + 2 v54 + 2 v55 + v56 + v57 + 2 v58 + 4 v59 + v61 + v62 + 3 v63 + v65 + v66 + 3 v68 + v69 + 4 v70 + v71 + v75 + 4 v76 + v78 + 3 v79 + v80 + v81 + v82 + v84 + 2 v85 + 3 v87 + v89 + v90 + v91 + 3 v92 + 3 v94 + 4 v95 + 2 v96 + v97 + v98 + v102 + v103 + 3 v104 + v105 + v106 + v107 + v108 + v109 + 3 v110 + v111 + 2 v112 + 3 v113 + v114 >= 57
C69: 2 v1 + v3 + v6 + 2 v7 + v8 + 2 v9 + 3 v10 + 2 v11 + 2 v12 + v14 + 3 v15 + v16 + 2 v18 + 4 v19 + v20 + v22 + v24 + 2 v26 + 2 v28 + v29 + 2 v30 + 2 v31 + 2 v32 + 2 v33 + v34 + 2 v35 + v36 + 3 v37 + 2 v38 + 2 v39 + v40 + 3 v42 + 3 v43 + 3 v44 + v45 + v47 + 2 v48 + 2 v51 + 2 v52 + 2 v53 + 2 v54 + v56 + 2 v57 + 2 v58 + v59 + 2 v60 + v61 + v65 + 3 v67 + 2 v69 + 2 v70 + v74 + 4 v76 + v79 + v80 + v81 + v88 + 2 v89 + 2 v90 + v95 + v96 + 2 v98 + v99 + 2 v100 + 4 v101 + v102 + v104 + v105 + 3 v107 + v108 + 2 v109 + v110 + 2 v113 <= 72
D69: 2 v1 + v3 + v6 + 2 v7 + v8 + 2 v9 + 3 v10 + 2 v11 + 2 v12 + v14 + 3 v15 + v16 + 2 v18 + 4 v19 + v20 + v22 + v24 + 2 v26 + 2 v28 + v29 + 2 v30 + 2 v31 + 2 v32 + 2 v33 + v34 + 2 v35 + v36 + 3 v37 + 2 v38 + 2 v39 + v40 + 3 v42 + 3 v43 + 3 v44 + v45 + v47 + 2 v48 + 2 v51 + 2 v52 + 2 v53 + 2 v54 + v56 + 2 v57 + 2 v58 + v59 + 2 v60 + v61 + v65 + 3 v67 + 2 v69 + 2 v70 + v74 + 4 v76 + v79 + v80 + v81 + v88 + 2 v89 + 2 v90 + v95 + v96 + 2 v98 + v99 + 2 v100 + 4 v101 + v102 + v104 + v105 + 3 v107 + v108 + 2 v109 + v110 + 2 v113 >= 57
C70: v1 + v2 + v3 + v6 + v7 + 5 v9 + v10 + 5 v13 + v14 + 2 v15 + 2 v16 + v18 + v20 + v23 + 2 v24 + v26 + 2 v27 + v28 + v29 + v30 + v31 + 2 v32 + 3 v36 + 3 v37 + v38 + v39 + 2 v41 + v42 + 2 v43 + 2 v44 + 3 v45 + 2 v47 + 2 v48 + 2 v49 + 2 v50 + v52 + v53 + v55 + v56 + 2 v57 + v58 + v60 + v61 + v62 + 2 v63 + v64 + 2 v65 + v66 + v67 + 2 v68 + v70 + v71 + v74 + 2 v75 + 2 v76 + v77 + 2 v78 + v80 + v81 + v82 + 3 v83 + v84 + v85 + v87 + v91 + 2 v92 + 3 v94 + v95 + 2 v98 + 3 v99 + 2 v102 + v103 + v104 + 2 v105 + 4 v106 + 3 v107 + 3 v109 + v110 + v112 <= 72
D70: v1 + v2 + v3 + v6 + v7 + 5 v9 + v10 + 5 v13 + v14 + 2 v15 + 2 v16 + v18 + v20 + v23 + 2 v24 + v26 + 2 v27 + v28 + v29 + v30 + v31 + 2 v32 + 3 v36 + 3 v37 + v38 + v39 + 2 v41 + v42 + 2 v43 + 2 v44 + 3 v45 + 2 v47 + 2 v48 + 2 v49 + 2 v50 + v52 + v53 + v55 + v56 + 2 v57 + v58 + v60 + v61 + v62 + 2 v63 + v64 + 2 v65 + v66 + v67 + 2 v68 + v70 + v71 + v74 + 2 v75 + 2 v76 + v77 + 2 v78 + v80 + v81 + v82 + 3 v83 + v84 + v85 + v87 + v91 + 2 v92 + 3 v94 + v95 + 2 v98 + 3 v99 + 2 v102 + v103 + v104 + 2 v105 + 4 v106 + 3 v107 + 3 v109 + v110 + v112 >= 57
C71: v1 + 2 v2 + v5 + v6 + v9 + 2 v10 + 2 v11 + 2 v12 + 2 v13 + 2 v14 + 2 v17 + v18 + 4 v20 + v21 + v22 + 2 v23 + v26 + 3 v27 + v28 + 2 v29 + v30 + 2 v31 + v32 + v33 + 2 v34 + 2 v35 + 2 v36 + 3 v38 + v39 + v41 + 3 v43 + 4 v44 + 2 v46 + v49 + v52 + v53 + v55 + v56 + v57 + v58 + 3 v60 + v62 + v63 + v64 + v65 + 4 v67 + 2 v68 + v69 + 2 v70 + v71 + 2 v73 + v74 + v75 + 3 v77 + 2 v78 + v80 + v84 + 2 v86 + 4 v87 + 2 v88 + v89 + v92 + v93 + v94 + v95 + v96 + v97 + v98 + 2 v99 + v100 + v101 + v103 + 2 v104 + 2 v106 + v107 + 3 v108 + v109 + 2 v111 + 2 v113 + v114 <= 72
D71: v1 + 2 v2 + v5 + v6 + v9 + 2 v10 + 2 v11 + 2 v12 + 2 v13 + 2 v14 + 2 v17 + v18 + 4 v20 + v21 + v22 + 2 v23 + v26 + 3 v27 + v28 + 2 v29 + v30 + 2 v31 + v32 + v33 + 2 v34 + 2 v35 + 2 v36 + 3 v38 + v39 + v41 + 3 v43 + 4 v44 + 2 v46 + v49 + v52 + v53 + v55 + v56 + v57 + v58 + 3 v60 + v62 + v63 + v64 + v65 + 4 v67 + 2 v68 + v69 + 2 v70 + v71 + 2 v73 + v74 + v75 + 3 v77 + 2 v78 + v80 + v84 + 2 v86 + 4 v87 + 2 v88 + v89 + v92 + v93 + v94 + v95 + v96 + v97 + v98 + 2 v99 + v100 + v101 + v103 + 2 v104 + 2 v106 + v107 + 3 v108 + v109 + 2 v111 + 2 v113 + v114 >= 57
C72: v1 + v3 + v4 + v5 + 2 v6 + v7 + 4 v8 + v9 + 2 v10 + v11 + v13 + 3 v15 + v16 + 3 v17 + 2 v18 + 5 v20 + v22 + v25 + v26 + v27 + 2 v28 + v29 + v31 + v32 + v33 + 2 v34 + v35 + 2 v36 + v40 + v41 + v42 + v43 + v44 + v45 + v46 + v47 + v49 + 2 v50 + v51 + v52 + v53 + 5 v54 + v55 + v56 + v58 + 3 v59 + 2 v60 + 2 v66 + v67 + v69 + v70 + 4 v71 + v73 + v74 + 4 v75 + 2 v76 + 3 v77 + 2 v78 + 2 v79 + 2 v81 + v82 + 2 v83 + 2 v86 + v87 + v90 + v91 + 2 v92 + v96 + v97 + 2 v99 + v100 + 2 v101 + v102 + 2 v103 + 2 v104 + 2 v105 + v106 + v107 + 2 v109 + 2 v110 + v112 <= 72
D72: v1 + v3 + v4 + v5 + 2 v6 + v7 + 4 v8 + v9 + 2 v10 + v11 + v13 + 3 v15 + v16 + 3 v17 + 2 v18 + 5 v20 + v22 + v25 + v26 + v27 + 2 v28 + v29 + v31 + v32 + v33 + 2 v34 + v35 + 2 v36 + v40 + v41 + v42 + v43 + v44 + v45 + v46 + v47 + v49 + 2 v50 + v51 + v52 + v53 + 5 v54 + v55 + v56 + v58 + 3 v59 + 2 v60 + 2 v66 + v67 + v69 + v70 + 4 v71 + v73 + v74 + 4 v75 + 2 v76 + 3 v77 + 2 v78 + 2 v79 + 2 v81 + v82 + 2 v83 + 2 v86 + v87 + v90 + v91 + 2 v92 + v96 + v97 + 2 v99 + v100 + 2 v101 + v102 + 2 v103 + 2 v104 + 2 v105 + v106 + v107 + 2 v109 + 2 v110 + v112 >= 57
C73: 2 v1 + v2 + 2 v3 + v4 + v5 + 3 v6 + 2 v7 + 2 v8 + v9 + v10 + v12 + 2 v13 + v14 + v15 + v16 + 3 v18 + v20 + 2 v21 + v23 + 2 v24 + 3 v25 + 3 v26 + 3 v32 + 5 v33 + v34 + v35 + v36 + 3 v37 + 2 v38 + v39 + 2 v44 + v46 + v48 + v49 + v50 + 2 v52 + v53 + 2 v54 + 2 v55 + 3 v60 + v61 + v62 + v63 + 2 v65 + v66 + 2 v72 + v73 + v76 + v77 + 2 v79 + 2 v80 + 3 v81 + 2 v82 + v84 + v86 + 3 v87 + v88 + 2 v89 + 2 v90 + 3 v92 + v94 + v96 + v97 + v98 + 2 v99 + v102 + 2 v103 + v104 + 3 v105 + v106 + v107 + 2 v108 + 2 v109 + 4 v111 + v112 + 2 v113 <= 72
D73: 2 v1 + v2 + 2 v3 + v4 + v5 + 3 v6 + 2 v7 + 2 v8 + v9 + v10 + v12 + 2 v13 + v14 + v15 + v16 + 3 v18 + v20 + 2 v21 + v23 + 2 v24 + 3 v25 + 3 v26 + 3 v32 + 5 v33 + v34 + v35 + v36 + 3 v37 + 2 v38 + v39 + 2 v44 + v46 + v48 + v49 + v50 + 2 v52 + v53 + 2 v54 + 2 v55 + 3 v60 + v61 + v62 + v63 + 2 v65 + v66 + 2 v72 + v73 + v76 + v77 + 2 v79 + 2 v80 + 3 v81 + 2 v82 + v84 + v86 + 3 v87 + v88 + 2 v89 + 2 v90 + 3 v92 + v94 + v96 + v97 + v98 + 2 v99 + v102 + 2 v103 + v104 + 3 v105 + v106 + v107 + 2 v108 + 2 v109 + 4 v111 + v112 + 2 v113 >= 57
C74: 3 v1 + 2 v4 + v5 + v6 + 2 v7 + 2 v10 + v11 + v12 + 2 v13 + 3 v14 + v15 + 4 v16 + v17 + v18 + v19 + 2 v20 + v21 + 3 v23 + v24 + 2 v25 + 3 v26 + 2 v28 + v33 + 3 v36 + v37 + v38 + v39 + v40 + 2 v42 + 2 v43 + 2 v44 + 2 v46 + v47 + 2 v48 + v49 + 2 v50 + v51 + v52 + v55 + v56 + v57 + v58 + v61 + 3 v62 + v63 + v64 + v65 + 2 v70 + v71 + v72 + 4 v73 + 5 v74 + 2 v75 + 3 v76 + 2 v78 + 2 v79 + v82 + 2 v84 + v85 + 3 v86 + v87 + v88 + v89 + v90 + v91 + 3 v92 + v95 + 2 v96 + v98 + v99 + 2 v100 + 2 v101 + 2 v102 + 2 v104 + v106 + v111 + 2 v112 <= 72
D74: 3 v1 + 2 v4 + v5 + v6 + 2 v7 + 2 v10 + v11 + v12 + 2 v13 + 3 v14 + v15 + 4 v16 + v17 + v18 + v19 + 2 v20 + v21 + 3 v23 + v24 + 2 v25 + 3 v26 + 2 v28 + v33 + 3 v36 + v37 + v38 + v39 + v40 + 2 v42 + 2 v43 + 2 v44 + 2 v46 + v47 + 2 v48 + v49 + 2 v50 + v51 + v52 + v55 + v56 + v57 + v58 + v61 + 3 v62 + v63 + v64 + v65 + 2 v70 + v71 + v72 + 4 v73 + 5 v74 + 2 v75 + 3 v76 + 2 v78 + 2 v79 + v82 + 2 v84 + v85 + 3 v86 + v87 + v88 + v89 + v90 + v91 + 3 v92 + v95 + 2 v96 + v98 + v99 + 2 v100 + 2 v101 + 2 v102 + 2 v104 + v106 + v111 + 2 v112 >= 57
C75: v1 + v3 + v6 + v7 + v8 + 2 v10 + v11 + 2 v12 + v14 + 2 v17 + v20 + v21 + 2 v23 + v24 + 2 v25 + v26 + 2 v27 + 2 v29 + 3 v30 + v31 + v32 + v33 + v34 + v36 + v37 + 2 v38 + v39 + 3 v40 + 2 v41 + v42 + 2 v43 + 2 v45 + v46 + 2 v47 + v48 + 2 v50 + v51 + 3 v53 + v54 + v55 + v58 + v59 + 2 v62 + 4 v63 + v64 + v65 + v68 + v69 + v70 + v71 + 5 v73 + 2 v75 + 2 v76 + v80 + 2 v81 + v82 + v83 + v85 + 2 v86 + v87 + v88 + v90 + v92 + v95 + 2 v97 + v98 + v99 + 4 v100 + v101 + 2 v102 + v103 + 2 v105 + v106 + 3 v107 + 2 v108 + 5 v109 + 3 v110 + 3 v111 + v112 + 2 v113 <= 72
D75: v1 + v3 + v6 + v7 + v8 + 2 v10 + v11 + 2 v12 + v14 + 2 v17 + v20 + v21 + 2 v23 + v24 + 2 v25 + v26 + 2 v27 + 2 v29 + 3 v30 + v31 + v32 + v33 + v34 + v36 + v37 + 2 v38 + v39 + 3 v40 + 2 v41 + v42 + 2 v43 + 2 v45 + v46 + 2 v47 + v48 + 2 v50 + v51 + 3 v53 + v54 + v55 + v58 + v59 + 2 v62 + 4 v63 + v64 + v65 + v68 + v69 + v70 + v71 + 5 v73 + 2 v75 + 2 v76 + v80 + 2 v81 + v82 + v83 + v85 + 2 v86 + v87 + v88 + v90 + v92 + v95 + 2 v97 + v98 + v99 + 4 v100 + v101 + 2 v102 + v103 + 2 v105 + v106 + 3 v107 + 2 v108 + 5 v109 + 3 v110 + 3 v111 + v112 + 2 v113 >= 57
C76: v1 + 4 v2 + v3 + 3 v6 + 2 v7 + v9 + v12 + 2 v13 + 2 v15 + 2 v16 + v17 + 2 v18 + v19 + v21 + 2 v22 + v24 + v25 + v26 + 2 v27 + v29 + 2 v30 + v31 + v33 + v34 + v35 + v36 + v37 + 2 v38 + v39 + v41 + 2 v46 + v47 + 2 v48 + v49 + 3 v50 + 2 v51 + 3 v53 + v54 + v55 + v56 + v58 + 2 v59 + 2 v60 + 2 v61 + v64 + v66 + v67 + 2 v69 + v70 + 4 v71 + 2 v73 + 2 v74 + 2 v76 + v79 + v81 + v82 + v84 + 4 v85 + 2 v86 + 2 v88 + 3 v90 + 2 v91 + v92 + v95 + v96 + v97 + 3 v98 + 4 v99 + 2 v101 + 2 v102 + v104 + 3 v106 + 3 v108 + v109 + v110 + v111 + 2 v113 + v114 <= 72
D76: v1 + 4 v2 + v3 + 3 v6 + 2 v7 + v9 + v12 + 2 v13 + 2 v15 + 2 v16 + v17 + 2 v18 + v19 + v21 + 2 v22 + v24 + v25 + v26 + 2 v27 + v29 + 2 v30 + v31 + v33 + v34 + v35 + v36 + v37 + 2 v38 + v39 + v41 + 2 v46 + v47 + 2 v48 + v49 + 3 v50 + 2 v51 + 3 v53 + v54 + v55 + v56 + v58 + 2 v59 + 2 v60 + 2 v61 + v64 + v66 + v67 + 2 v69 + v70 + 4 v71 + 2 v73 + 2 v74 + 2 v76 + v79 + v81 + v82 + v84 + 4 v85 + 2 v86 + 2 v88 + 3 v90 + 2 v91 + v92 + v95 + v96 + v97 + 3 v98 + 4 v99 + 2 v101 + 2 v102 + v104 + 3 v106 + 3 v108 + v109 + v110 + v111 + 2 v113 + v114 >= 57
C77: v2 + v3 + v5 + 2 v6 + v7 + v8 + v9 + v11 + v12 + v13 + v17 + v18 + 2 v19 + v21 + 2 v22 + v23 + v28 + 2 v29 + v30 + v31 + v32 + 3 v33 + v35 + 2 v38 + 2 v39 + v40 + 3 v42 + v43 + 2 v44 + v45 + 2 v47 + 3 v48 + v49 + v53 + 2 v54 + v56 + v57 + 2 v58 + 2 v59 + v61 + v64 + 2 v65 + v66 + 4 v67 + 4 v68 + 2 v69 + 2 v71 + v72 + 3 v73 + 2 v74 + 2 v75 + v77 + v78 + v80 + v81 + 2 v82 + v83 + 4 v84 + 3 v86 + v89 + v90 + 2 v91 + 5 v92 + v94 + v95 + v96 + v98 + v99 + 2 v100 + v101 + 2 v102 + 2 v103 + 4 v105 + 2 v106 + v107 + v108 + v111 + 2 v112 + 2 v113 <= 72
D77: v2 + v3 + v5 + 2 v6 + v7 + v8 + v9 + v11 + v12 + v13 + v17 + v18 + 2 v19 + v21 + 2 v22 + v23 + v28 + 2 v29 + v30 + v31 + v32 + 3 v33 + v35 + 2 v38 + 2 v39 + v40 + 3 v42 + v43 + 2 v44 + v45 + 2 v47 + 3 v48 + v49 + v53 + 2 v54 + v56 + v57 + 2 v58 + 2 v59 + v61 + v64 + 2 v65 + v66 + 4 v67 + 4 v68 + 2 v69 + 2 v71 + v72 + 3 v73 + 2 v74 + 2 v75 + v77 + v78 + v80 + v81 + 2 v82 + v83 + 4 v84 + 3 v86 + v89 + v90 + 2 v91 + 5 v92 + v94 + v95 + v96 + v98 + v99 + 2 v100 + v101 + 2 v102 + 2 v103 + 4 v105 + 2 v106 + v107 + v108 + v111 + 2 v112 + 2 v113 >= 57
C78: v1 + v3 + 2 v4 + 3 v5 + 2 v8 + v9 + v10 + v12 + v14 + 2 v16 + v17 + v18 + v21 + v22 + 2 v23 + 2 v25 + v28 + v30 + 2 v31 + v32 + v34 + 4 v35 + 2 v37 + 3 v38 + 2 v40 + 2 v41 + 3 v42 + 2 v43 + 2 v44 + v45 + 3 v46 + v47 + v49 + v52 + v53 + 2 v54 + 2 v56 + 3 v60 + v61 + v62 + v63 + 3 v65 + v66 + v69 + 3 v70 + 3 v71 + v72 + v76 + v78 + 2 v79 + 2 v83 + 4 v84 + v85 + 3 v86 + v87 + v88 + v89 + 3 v90 + 3 v91 + 2 v94 + v95 + 2 v98 + v99 + v100 + v101 + v102 + v103 + v104 + v105 + 3 v106 + 2 v107 + 2 v108 + 3 v109 + v110 + v111 + 3 v112 <= 72
D78: v1 + v3 + 2 v4 + 3 v5 + 2 v8 + v9 + v10 + v12 + v14 + 2 v16 + v17 + v18 + v21 + v22 + 2 v23 + 2 v25 + v28 + v30 + 2 v31 + v32 + v34 + 4 v35 + 2 v37 + 3 v38 + 2 v40 + 2 v41 + 3 v42 + 2 v43 + 2 v44 + v45 + 3 v46 + v47 + v49 + v52 + v53 + 2 v54 + 2 v56 + 3 v60 + v61 + v62 + v63 + 3 v65 + v66 + v69 + 3 v70 + 3 v71 + v72 + v76 + v78 + 2 v79 + 2 v83 + 4 v84 + v85 + 3 v86 + v87 + v88 + v89 + 3 v90 + 3 v91 + 2 v94 + v95 + 2 v98 + v99 + v100 + v101 + v102 + v103 + v104 + v105 + 3 v106 + 2 v107 + 2 v108 + 3 v109 + v110 + v111 + 3 v112 >= 57
C79: 3 v1 + 2 v2 + 3 v4 + 3 v5 + v6 + v10 + 2 v11 + v12 + 3 v13 + v14 + 2 v15 + v16 + 2 v17 + v19 + v20 + v22 + v24 + v27 + 2 v28 + v30 + v31 + 3 v32 + 2 v33 + v35 + v36 + v38 + v39 + v40 + 3 v41 + v43 + v44 + v45 + 2 v46 + v47 + v48 + v49 + v50 + v51 + 4 v52 + v55 + 2 v57 + 2 v59 + 2 v60 + v63 + v66 + v67 + 2 v69 + 2 v70 + 2 v71 + 2 v73 + v76 + v77 + 2 v78 + 3 v80 + 3 v82 + v83 + 2 v84 + v88 + 2 v90 + v91 + 2 v92 + 2 v95 + v96 + 5 v97 + 2 v98 + v100 + 2 v101 + 4 v102 + v104 + 2 v105 + v106 + 3 v107 + v108 + v110 + 2 v111 + 2 v112 + v113 <= 72
D79: 3 v1 + 2 v2 + 3 v4 + 3 v5 + v6 + v10 + 2 v11 + v12 + 3 v13 + v14 + 2 v15 + v16 + 2 v17 + v19 + v20 + v22 + v24 + v27 + 2 v28 + v30 + v31 + 3 v32 + 2 v33 + v35 + v36 + v38 + v39 + v40 + 3 v41 + v43 + v44 + v45 + 2 v46 + v47 + v48 + v49 + v50 + v51 + 4 v52 + v55 + 2 v57 + 2 v59 + 2 v60 + v63 + v66 + v67 + 2 v69 + 2 v70 + 2 v71 + 2 v73 + v76 + v77 + 2 v78 + 3 v80 + 3 v82 + v83 + 2 v84 + v88 + 2 v90 + v91 + 2 v92 + 2 v95 + v96 + 5 v97 + 2 v98 + v100 + 2 v101 + 4 v102 + v104 + 2 v105 + v106 + 3 v107 + v108 + v110 + 2 v111 + 2 v112 + v113 >= 57
C80: 2 v2 + 4 v3 + v4 + v5 + v8 + 4 v10 + 2 v11 + v12 + v13 + v14 + v15 + 2 v16 + v18 + 2 v19 + v20 + 3 v21 + 2 v22 + v24 + v25 + 2 v26 + v31 + 2 v34 + 3 v36 + v37 + v38 + v39 + v40 + 4 v42 + 2 v43 + 2 v44 + 3 v45 + 3 v46 + 2 v48 + v49 + 4 v50 + 2 v51 + v52 + v54 + 2 v57 + v58 + 2 v59 + v61 + v63 + v65 + 3 v67 + v68 + 2 v71 + 2 v72 + 2 v73 + v75 + 2 v77 + 2 v81 + v82 + v83 + 2 v84 + 2 v85 + 2 v87 + v89 + 2 v90 + v91 + 3 v94 + v95 + 3 v97 + v99 + v101 + 2 v102 + v103 + 2 v104 + v105 + v106 + v107 + 2 v108 + v109 + v110 + 3 v111 + v112 <= 72
D80: 2 v2 + 4 v3 + v4 + v5 + v8 + 4 v10 + 2 v11 + v12 + v13 + v14 + v15 + 2 v16 + v18 + 2 v19 + v20 + 3 v21 + 2 v22 + v24 + v25 + 2 v26 + v31 + 2 v34 + 3 v36 + v37 + v38 + v39 + v40 + 4 v42 + 2 v43 + 2 v44 + 3 v45 + 3 v46 + 2 v48 + v49 + 4 v50 + 2 v51 + v52 + v54 + 2 v57 + v58 + 2 v59 + v61 + v63 + v65 + 3 v67 + v68 + 2 v71 + 2 v72 + 2 v73 + v75 + 2 v77 + 2 v81 + v82 + v83 + 2 v84 + 2 v85 + 2 v87 + v89 + 2 v90 + v91 + 3 v94 + v95 + 3 v97 + v99 + v101 + 2 v102 + v103 + 2 v104 + v105 + v106 + v107 + 2 v108 + v109 + v110 + 3 v111 + v112 >= 57
C81: 2 v1 + v2 + v4 + v5 + 2 v7 + 3 v10 + v11 + 2 v13 + v14 + 3 v15 + 2 v17 + 4 v18 + 3 v20 + v21 + 2 v23 + v26 + v27 + v30 + 2 v31 + 2 v32 + v33 + 3 v34 + 2 v35 + v36 + v37 + v38 + 3 v39 + v40 + 2 v41 + v42 + v44 + 2 v45 + v46 + 4 v47 + 3 v48 + v50 + 2 v51 + v54 + 2 v55 + 2 v56 + v58 + v62 + 2 v63 + v64 + 2 v65 + v66 + v67 + v68 + v69 + v70 + 2 v72 + v74 + v76 + 3 v78 + 4 v81 + v82 + v83 + 3 v84 + 2 v85 + v86 + v88 + 2 v89 + 2 v90 + 2 v91 + v92 + v94 + 3 v97 + v98 + 2 v100 + v101 + v102 + 3 v103 + v106 + v108 + v109 + v112 + 2 v113 + v114 <= 72
D81: 2 v1 + v2 + v4 + v5 + 2 v7 + 3 v10 + v11 + 2 v13 + v14 + 3 v15 + 2 v17 + 4 v18 + 3 v20 + v21 + 2 v23 + v26 + v27 + v30 + 2 v31 + 2 v32 + v33 + 3 v34 + 2 v35 + v36 + v37 + v38 + 3 v39 + v40 + 2 v41 + v42 + v44 + 2 v45 + v46 + 4 v47 + 3 v48 + v50 + 2 v51 + v54 + 2 v55 + 2 v56 + v58 + v62 + 2 v63 + v64 + 2 v65 + v66 + v67 + v68 + v69 + v70 + 2 v72 + v74 + v76 + 3 v78 + 4 v81 + v82 + v83 + 3 v84 + 2 v85 + v86 + v88 + 2 v89 + 2 v90 + 2 v91 + v92 + v94 + 3 v97 + v98 + 2 v100 + v101 + v102 + 3 v103 + v106 + v108 + v109 + v112 + 2 v113 + v114 >= 57
C82: v1 + v5 + v7 + 3 v8 + v10 + 2 v13 + 3 v14 + 2 v17 + v18 + 2 v19 + 3 v20 + 3 v21 + v23 + v25 + v26 + 2 v29 + v31 + v32 + 2 v33 + 3 v35 + v36 + 3 v37 + 3 v38 + v41 + v42 + v44 + 2 v45 + v46 + 2 v47 + 2 v48 + 2 v49 + 2 v50 + v51 + v52 + 2 v53 + 2 v54 + 2 v57 + 3 v58 + v59 + 2 v61 + v62 + 3 v64 + v67 + v68 + v69 + 2 v71 + 3 v72 + 2 v74 + v75 + v76 + 2 v79 + 4 v80 + v82 + 2 v83 + 2 v86 + v87 + 2 v88 + 2 v89 + v91 + v94 + 2 v95 + 2 v96 + 3 v97 + v99 + v100 + v101 + 3 v102 + 3 v106 + 2 v107 + v108 + v109 + 2 v110 + v111 + v112 + v114 <= 72
D82: v1 + v5 + v7 + 3 v8 + v10 + 2 v13 + 3 v14 + 2 v17 + v18 + 2 v19 + 3 v20 + 3 v21 + v23 + v25 + v26 + 2 v29 + v31 + v32 + 2 v33 + 3 v35 + v36 + 3 v37 + 3 v38 + v41 + v42 + v44 + 2 v45 + v46 + 2 v47 + 2 v48 + 2 v49 + 2 v50 + v51 + v52 + 2 v53 + 2 v54 + 2 v57 + 3 v58 + v59 + 2 v61 + v62 + 3 v64 + v67 + v68 + v69 + 2 v71 + 3 v72 + 2 v74 + v75 + v76 + 2 v79 + 4 v80 + v82 + 2 v83 + 2 v86 + v87 + 2 v88 + 2 v89 + v91 + v94 + 2 v95 + 2 v96 + 3 v97 + v99 + v100 + v101 + 3 v102 + 3 v106 + 2 v107 + v108 + v109 + 2 v110 + v111 + v112 + v114 >= 57
C83: v2 + v4 + v5 + v6 + v8 + 2 v9 + v10 + 4 v11 + v12 + v15 + v16 + 2 v18 + v19 + 2 v20 + 2 v21 + 2 v22 + v24 + v25 + v26 + 3 v27 + 2 v28 + 2 v29 + 4 v31 + v32 + 2 v34 + v36 + 2 v37 + 4 v38 + 2 v41 + v42 + v46 + v48 + v49 + 2 v50 + v53 + v56 + v57 + v58 + v61 + 3 v62 + v64 + 2 v65 + v66 + v67 + v69 + v71 + 2 v72 + v73 + v74 + v75 + 2 v76 + 3 v78 + v79 + v80 + v81 + 4 v82 + 2 v84 + v85 + v87 + v88 + v89 + 3 v90 + v92 + v94 + 2 v95 + 5 v96 + v97 + v98 + v100 + 2 v101 + v102 + 2 v103 + 2 v104 + 3 v105 + 2 v106 + 3 v109 + 2 v110 + v111 + v112 + v113 <= 72
D83: v2 + v4 + v5 + v6 + v8 + 2 v9 + v10 + 4 v11 + v12 + v15 + v16 + 2 v18 + v19 + 2 v20 + 2 v21 + 2 v22 + v24 + v25 + v26 + 3 v27 + 2 v28 + 2 v29 + 4 v31 + v32 + 2 v34 + v36 + 2 v37 + 4 v38 + 2 v41 + v42 + v46 + v48 + v49 + 2 v50 + v53 + v56 + v57 + v58 + v61 + 3 v62 + v64 + 2 v65 + v66 + v67 + v69 + v71 + 2 v72 + v73 + v74 + v75 + 2 v76 + 3 v78 + v79 + v80 + v81 + 4 v82 + 2 v84 + v85 + v87 + v88 + v89 + 3 v90 + v92 + v94 + 2 v95 + 5 v96 + v97 + v98 + v100 + 2 v101 + v102 + 2 v103 + 2 v104 + 3 v105 + 2 v106 + 3 v109 + 2 v110 + v111 + v112 + v113 >= 57
C84: 3 v2 + v4 + v6 + v7 + v8 + 2 v9 + 3 v10 + 3 v11 + v12 + v13 + 3 v14 + v16 + v17 + 2 v18 + 2 v19 + v21 + v22 + 2 v23 + 4 v24 + v26 + v27 + v28 + v30 + v31 + v32 + 3 v33 + 2 v34 + 3 v35 + v36 + 3 v40 + v41 + v42 + 2 v43 + v44 + v47 + 4 v49 + v51 + v54 + v55 + v59 + 2 v61 + v62 + v64 + v65 + 3 v69 + 2 v71 + v74 + v76 + 2 v77 + v78 + v79 + v80 + 2 v81 + 2 v85 + 2 v86 + 2 v88 + v89 + 2 v92 + 3 v94 + 2 v95 + v96 + 2 v97 + 2 v99 + 3 v100 + v101 + 3 v102 + 3 v103 + 3 v104 + v105 + 2 v106 + v107 + v108 + 2 v109 + v110 + 3 v112 + v113 <= 72
D84: 3 v2 + v4 + v6 + v7 + v8 + 2 v9 + 3 v10 + 3 v11 + v12 + v13 + 3 v14 + v16 + v17 + 2 v18 + 2 v19 + v21 + v22 + 2 v23 + 4 v24 + v26 + v27 + v28 + v30 + v31 + v32 + 3 v33 + 2 v34 + 3 v35 + v36 + 3 v40 + v41 + v42 + 2 v43 + v44 + v47 + 4 v49 + v51 + v54 + v55 + v59 + 2 v61 + v62 + v64 + v65 + 3 v69 + 2 v71 + v74 + v76 + 2 v77 + v78 + v79 + v80 + 2 v81 + 2 v85 + 2 v86 + 2 v88 + v89 + 2 v92 + 3 v94 + 2 v95 + v96 + 2 v97 + 2 v99 + 3 v100 + v101 + 3 v102 + 3 v103 + 3 v104 + v105 + 2 v106 + v107 + v108 + 2 v109 + v110 + 3 v112 + v113 >= 57
C85: v1 + v2 + v3 + v4 + v6 + 2 v7 + 5 v9 + v12 + v14 + v15 + 5 v17 + 2 v19 + v20 + 2 v21 + 2 v24 + v26 + v27 + v31 + 2 v33 + v34 + 2 v35 + v36 + v38 + v40 + v41 + 3 v42 + v43 + 2 v44 + 2 v45 + 3 v46 + 3 v47 + v48 + 2 v50 + 2 v52 + v53 + 2 v55 + 2 v56 + v58 + 2 v59 + v60 + v61 + 2 v62 + v64 + v65 + 2 v66 + v67 + v69 + v70 + v72 + 2 v73 + v75 + 4 v76 + 4 v77 + 2 v78 + 2 v79 + 3 v80 + 2 v82 + 2 v84 + 2 v85 + v86 + v88 + 2 v89 + v90 + v91 + v92 + 2 v94 + v95 + v96 + v98 + v100 + v101 + v102 + 2 v103 + v106 + 2 v108 + v109 + 2 v110 + 3 v111 + v113 <= 72
D85: v1 + v2 + v3 + v4 + v6 + 2 v7 + 5 v9 + v12 + v14 + v15 + 5 v17 + 2 v19 + v20 + 2 v21 + 2 v24 + v26 + v27 + v31 + 2 v33 + v34 + 2 v35 + v36 + v38 + v40 + v41 + 3 v42 + v43 + 2 v44 + 2 v45 + 3 v46 + 3 v47 + v48 + 2 v50 + 2 v52 + v53 + 2 v55 + 2 v56 + v58 + 2 v59 + v60 + v61 + 2 v62 + v64 + v65 + 2 v66 + v67 + v69 + v70 + v72 + 2 v73 + v75 + 4 v76 + 4 v77 + 2 v78 + 2 v79 + 3 v80 + 2 v82 + 2 v84 + 2 v85 + v86 + v88 + 2 v89 + v90 + v91 + v92 + 2 v94 + v95 + v96 + v98 + v100 + v101 + v102 + 2 v103 + v106 + 2 v108 + v109 + 2 v110 + 3 v111 + v113 >= 57
C86: v2 + 3 v3 + 3 v5 + 2 v6 + 4 v7 + v8 + 2 v9 + 2 v10 + 3 v12 + 2 v13 + v14 + 2 v17 + v23 + v24 + 2 v25 + v26 + v28 + 2 v30 + 2 v31 + 2 v32 + 2 v33 + 4 v34 + v35 + v36 + v37 + v38 + 2 v39 + 2 v42 + v43 + v47 + v48 + 2 v49 + 2 v50 + v52 + v55 + v56 + 3 v57 + v59 + v60 + v62 + 2 v63 + 2 v65 + v66 + 2 v67 + v69 + v73 + v74 + 4 v75 + v77 + 2 v79 + 2 v80 + v82 + 2 v83 + 2 v84 + 2 v85 + v86 + v87 + 2 v88 + v89 + v90 + v91 + 3 v96 + 2 v97 + 2 v98 + v99 + 2 v100 + 3 v101 + v103 + 2 v104 + v105 + 2 v106 + v107 + v108 + 3 v110 + 3 v112 + v114 <= 72
D86: v2 + 3 v3 + 3 v5 + 2 v6 + 4 v7 + v8 + 2 v9 + 2 v10 + 3 v12 + 2 v13 + v14 + 2 v17 + v23 + v24 + 2 v25 + v26 + v28 + 2 v30 + 2 v31 + 2 v32 + 2 v33 + 4 v34 + v35 + v36 + v37 + v38 + 2 v39 + 2 v42 + v43 + v47 + v48 + 2 v49 + 2 v50 + v52 + v55 + v56 + 3 v57 + v59 + v60 + v62 + 2 v63 + 2 v65 + v66 + 2 v67 + v69 + v73 + v74 + 4 v75 + v77 + 2 v79 + 2 v80 + v82 + 2 v83 + 2 v84 + 2 v85 + v86 + v87 + 2 v88 + v89 + v90 + v91 + 3 v96 + 2 v97 + 2 v98 + v99 + 2 v100 + 3 v101 + v103 + 2 v104 + v105 + 2 v106 + v107 + v108 + 3 v110 + 3 v112 + v114 >= 57
C87: v1 + v2 + v3 + 3 v4 + 2 v5 + 2 v6 + 3 v7 + v10 + 2 v11 + v13 + v14 + v15 + 2 v17 + 2 v19 + v20 + 2 v21 + v22 + v24 + v25 + v26 + v27 + 2 v28 + 3 v29 + 2 v30 + 5 v31 + 2 v32 + v34 + 3 v37 + 2 v39 + v43 + 2 v46 + v47 + v48 + 2 v49 + v50 + 2 v54 + v55 + v56 + v57 + v60 + 3 v61 + v64 + 2 v65 + 2 v70 + 2 v71 + v72 + 3 v73 + 2 v74 + 2 v75 + 3 v76 + 3 v77 + v80 + 2 v81 + 2 v83 + v84 + v85 + 2 v87 + 2 v88 + 2 v89 + v90 + 3 v91 + 2 v92 + 3 v94 + v95 + v96 + v97 + v99 + 2 v100 + v102 + 2 v103 + v106 + 4 v107 + 2 v108 + v111 + v113 <= 72
D87: v1 + v2 + v3 + 3 v4 + 2 v5 + 2 v6 + 3 v7 + v10 + 2 v11 + v13 + v14 + v15 + 2 v17 + 2 v19 + v20 + 2 v21 + v22 + v24 + v25 + v26 + v27 + 2 v28 + 3 v29 + 2 v30 + 5 v31 + 2 v32 + v34 + 3 v37 + 2 v39 + v43 + 2 v46 + v47 + v48 + 2 v49 + v50 + 2 v54 + v55 + v56 + v57 + v60 + 3 v61 + v64 + 2 v65 + 2 v70 + 2 v71 + v72 + 3 v73 + 2 v74 + 2 v75 + 3 v76 + 3 v77 + v80 + 2 v81 + 2 v83 + v84 + v85 + 2 v87 + 2 v88 + 2 v89 + v90 + 3 v91 + 2 v92 + 3 v94 + v95 + v96 + v97 + v99 + 2 v100 + v102 + 2 v103 + v106 + 4 v107 + 2 v108 + v111 + v113 >= 57
C88: 2 v1 + v3 + v4 + v7 + v8 + v9 + v10 + v12 + v13 + 2 v14 + v15 + v16 + v17 + v18 + 2 v19 + v20 + v22 + v23 + 2 v24 + 2 v25 + 3 v27 + 3 v28 + v29 + 3 v31 + 2 v32 + 3 v33 + 2 v34 + v36 + 2 v39 + v41 + v42 + 2 v43 + 2 v45 + v46 + 2 v47 + 2 v49 + v50 + v51 + v52 + 2 v54 + 3 v57 + 3 v59 + 2 v61 + 3 v62 + 3 v63 + 2 v64 + 2 v66 + 3 v67 + v69 + 4 v70 + v71 + 3 v72 + v73 + v74 + v77 + 2 v79 + v81 + v82 + v85 + 2 v86 + v89 + 2 v90 + 2 v91 + v96 + v99 + v101 + v102 + 2 v103 + v104 + v105 + 5 v106 + v107 + v108 + v109 + 3 v111 + v112 + 3 v113 <= 72
D88: 2 v1 + v3 + v4 + v7 + v8 + v9 + v10 + v12 + v13 + 2 v14 + v15 + v16 + v17 + v18 + 2 v19 + v20 + v22 + v23 + 2 v24 + 2 v25 + 3 v27 + 3 v28 + v29 + 3 v31 + 2 v32 + 3 v33 + 2 v34 + v36 + 2 v39 + v41 + v42 + 2 v43 + 2 v45 + v46 + 2 v47 + 2 v49 + v50 + v51 + v52 + 2 v54 + 3 v57 + 3 v59 + 2 v61 + 3 v62 + 3 v63 + 2 v64 + 2 v66 + 3 v67 + v69 + 4 v70 + v71 + 3 v72 + v73 + v74 + v77 + 2 v79 + v81 + v82 + v85 + 2 v86 + v89 + 2 v90 + 2 v91 + v96 + v99 + v101 + v102 + 2 v103 + v104 + v105 + 5 v106 + v107 + v108 + v109 + 3 v111 + v112 + 3 v113 >= 57
C89: v1 + v2 + 2 v7 + v8 + v9 + v10 + v14 + 2 v15 + v16 + v17 + v18 + 2 v19 + 2 v20 + 3 v21 + 4 v22 + v23 + v24 + 2 v25 + 2 v26 + 2 v28 + v29 + 3 v30 + v33 + 2 v34 + v36 + 3 v38 + v39 + v41 + 2 v42 + v44 + v46 + 2 v47 + v48 + 2 v49 + v51 + 5 v52 + 2 v53 + v54 + v55 + 2 v56 + v57 + v58 + 2 v63 + v65 + 4 v66 + v68 + 2 v70 + v72 + v73 + v74 + 2 v75 + v77 + v78 + v80 + 2 v81 + v82 + 2 v83 + v84 + 2 v85 + 2 v86 + 4 v88 + v90 + 2 v92 + 2 v94 + 2 v95 + v96 + v97 + v100 + v101 + v102 + v103 + 4 v104 + v105 + 3 v106 + 3 v107 + 2 v108 + v109 + v111 + v113 <= 72
D89: v1 + v2 + 2 v7 + v8 + v9 + v10 + v14 + 2 v15 + v16 + v17 + v18 + 2 v19 + 2 v20 + 3 v21 + 4 v22 + v23 + v24 + 2 v25 + 2 v26 + 2 v28 + v29 + 3 v30 + v33 + 2 v34 + v36 + 3 v38 + v39 + v41 + 2 v42 + v44 + v46 + 2 v47 + v48 + 2 v49 + v51 + 5 v52 + 2 v53 + v54 + v55 + 2 v56 + v57 + v58 + 2 v63 + v65 + 4 v66 + v68 + 2 v70 + v72 + v73 + v74 + 2 v75 + v77 + v78 + v80 + 2 v81 + v82 + 2 v83 + v84 + 2 v85 + 2 v86 + 4 v88 + v90 + 2 v92 + 2 v94 + 2 v95 + v96 + v97 + v100 + v101 + v102 + v103 + 4 v104 + v105 + 3 v106 + 3 v107 + 2 v108 + v109 + v111 + v113 >= 57
C90: v1 + v2 + v3 + v4 + 2 v5 + 2 v6 + 4 v8 + v9 + v11 + v12 + 2 v13 + 2 v15 + 3 v16 + v17 + v18 + 2 v19 + v20 + 3 v23 + 2 v24 + v27 + v28 + 4 v30 + v31 + v33 + v34 + v35 + 5 v36 + v38 + v41 + v43 + 2 v45 + v46 + v47 + v49 + v50 + v51 + v56 + 2 v58 + v59 + v60 + 2 v61 + v62 + v64 + v65 + 2 v66 + v67 + 2 v68 + v70 + 2 v72 + v73 + v76 + v77 + v79 + 2 v80 + 2 v81 + v82 + v83 + 2 v84 + v85 + 2 v86 + v87 + 2 v89 + 2 v90 + 2 v91 + v92 + v94 + 3 v95 + 2 v96 + v98 + v99 + 3 v100 + 3 v101 + 3 v103 + 2 v104 + v105 + 4 v107 + v108 + v110 + 3 v111 + v113 + v114 <= 72
D90: v1 + v2 + v3 + v4 + 2 v5 + 2 v6 + 4 v8 + v9 + v11 + v12 + 2 v13 + 2 v15 + 3 v16 + v17 + v18 + 2 v19 + v20 + 3 v23 + 2 v24 + v27 + v28 + 4 v30 + v31 + v33 + v34 + v35 + 5 v36 + v38 + v41 + v43 + 2 v45 + v46 + v47 + v49 + v50 + v51 + v56 + 2 v58 + v59 + v60 + 2 v61 + v62 + v64 + v65 + 2 v66 + v67 + 2 v68 + v70 + 2 v72 + v73 + v76 + v77 + v79 + 2 v80 + 2 v81 + v82 + v83 + 2 v84 + v85 + 2 v86 + v87 + 2 v89 + 2 v90 + 2 v91 + v92 + v94 + 3 v95 + 2 v96 + v98 + v99 + 3 v100 + 3 v101 + 3 v103 + 2 v104 + v105 + 4 v107 + v108 + v110 + 3 v111 + v113 + v114 >= 57
C91: v1 + 2 v2 + 2 v3 + v4 + 2 v5 + 2 v9 + 3 v10 + v11 + 2 v12 + 4 v14 + 3 v15 + v16 + v17 + 3 v18 + v22 + v25 + v27 + 3 v28 + 6 v30 + v34 + 2 v35 + v36 + 2 v37 + v38 + 2 v39 + v40 + v43 + v44 + v45 + v46 + v47 + v50 + v51 + 2 v52 + 2 v53 + 3 v54 + v55 + v58 + 3 v61 + 2 v62 + v63 + v64 + v65 + v67 + 2 v68 + v71 + 2 v72 + v73 + v74 + 3 v75 + v76 + 3 v77 + 2 v78 + 2 v79 + 2 v80 + 3 v82 + v84 + v85 + v86 + 2 v87 + v88 + 2 v89 + 2 v90 + v91 + v92 + 2 v95 + v97 + v98 + v99 + v100 + 2 v102 + v103 + 2 v105 + 3 v106 + v108 + v110 + v111 + v112 + v113 <= 72
D91: v1 + 2 v2 + 2 v3 + v4 + 2 v5 + 2 v9 + 3 v10 + v11 + 2 v12 + 4 v14 + 3 v15 + v16 + v17 + 3 v18 + v22 + v25 + v27 + 3 v28 + 6 v30 + v34 + 2 v35 + v36 + 2 v37 + v38 + 2 v39 + v40 + v43 + v44 + v45 + v46 + v47 + v50 + v51 + 2 v52 + 2 v53 + 3 v54 + v55 + v58 + 3 v61 + 2 v62 + v63 + v64 + v65 + v67 + 2 v68 + v71 + 2 v72 + v73 + v74 + 3 v75 + v76 + 3 v77 + 2 v78 + 2 v79 + 2 v80 + 3 v82 + v84 + v85 + v86 + 2 v87 + v88 + 2 v89 + 2 v90 + v91 + v92 + 2 v95 + v97 + v98 + v99 + v100 + 2 v102 + v103 + 2 v105 + 3 v106 + v108 + v110 + v111 + v112 + v113 >= 57
C92: 2 v1 + 2 v2 + v3 + 2 v4 + v6 + v7 + v12 + v14 + 4 v15 + v16 + 2 v18 + v19 + v20 + v21 + 2 v22 + 5 v23 + v24 + 2 v25 + v27 + v30 + 3 v31 + v32 + v33 + v34 + v35 + v36 + 2 v37 + v39 + 2 v42 + v43 + v44 + v45 + 2 v46 + v48 + 2 v49 + 3 v53 + 5 v56 + 3 v57 + v58 + 2 v59 + v60 + 2 v63 + 4 v64 + v65 + v66 + v67 + v69 + v71 + v73 + 2 v75 + 2 v76 + 3 v77 + v78 + v79 + 2 v80 + v81 + v84 + v85 + 3 v86 + 2 v87 + 2 v89 + v90 + v92 + v94 + 2 v95 + v96 + 3 v97 + v98 + v99 + v101 + 2 v102 + v103 + v104 + 3 v105 + v106 + v107 + v109 + 2 v110 + v111 + v112 + v113 <= 72
D92: 2 v1 + 2 v2 + v3 + 2 v4 + v6 + v7 + v12 + v14 + 4 v15 + v16 + 2 v18 + v19 + v20 + v21 + 2 v22 + 5 v23 + v24 + 2 v25 + v27 + v30 + 3 v31 + v32 + v33 + v34 + v35 + v36 + 2 v37 + v39 + 2 v42 + v43 + v44 + v45 + 2 v46 + v48 + 2 v49 + 3 v53 + 5 v56 + 3 v57 + v58 + 2 v59 + v60 + 2 v63 + 4 v64 + v65 + v66 + v67 + v69 + v71 + v73 + 2 v75 + 2 v76 + 3 v77 + v78 + v79 + 2 v80 + v81 + v84 + v85 + 3 v86 + 2 v87 + 2 v89 + v90 + v92 + v94 + 2 v95 + v96 + 3 v97 + v98 + v99 + v101 + 2 v102 + v103 + v104 + 3 v105 + v106 + v107 + v109 + 2 v110 + v111 + v112 + v113 >= 57
C93: v1 + 2 v2 + 2 v3 + 2 v6 + v7 + 4 v8 + v9 + v11 + 2 v12 + v13 + 2 v14 + 2 v16 + v17 + v18 + v20 + 2 v21 + 2 v22 + v23 + v24 + v25 + 2 v27 + 3 v30 + 3 v32 + 2 v34 + 3 v35 + v36 + 2 v37 + 3 v39 + v40 + 2 v41 + v42 + v44 + v46 + v50 + 3 v51 + v52 + v55 + 4 v57 + v58 + 2 v60 + v62 + v63 + 2 v64 + v65 + 2 v66 + 3 v67 + 2 v69 + v70 + 2 v71 + 3 v72 + 3 v73 + v74 + v75 + 5 v76 + 2 v78 + v80 + v82 + 2 v83 + v84 + 2 v86 + 2 v88 + v89 + v90 + v91 + 2 v92 + 3 v94 + v97 + v100 + v102 + 2 v103 + 2 v104 + v105 + v106 + v109 + v110 + v111 + v113 <= 72
D93: v1 + 2 v2 + 2 v3 + 2 v6 + v7 + 4 v8 + v9 + v11 + 2 v12 + v13 + 2 v14 + 2 v16 + v17 + v18 + v20 + 2 v21 + 2 v22 + v23 + v24 + v25 + 2 v27 + 3 v30 + 3 v32 + 2 v34 + 3 v35 + v36 + 2 v37 + 3 v39 + v40 + 2 v41 + v42 + v44 + v46 + v50 + 3 v51 + v52 + v55 + 4 v57 + v58 + 2 v60 + v62 + v63 + 2 v64 + v65 + 2 v66 + 3 v67 + 2 v69 + v70 + 2 v71 + 3 v72 + 3 v73 + v74 + v75 + 5 v76 + 2 v78 + v80 + v82 + 2 v83 + v84 + 2 v86 + 2 v88 + v89 + v90 + v91 + 2 v92 + 3 v94 + v97 + v100 + v102 + 2 v103 + 2 v104 + v105 + v106 + v109 + v110 + v111 + v113 >= 57
C94: 7 v1 + 7 v11 + 14 v12 + 7 v16 + 7 v17 + 7 v48 + 7 v49 + 7 v50 + 7 v52 + 7 v53 + 7 v54 + 7 v64 + 7 v65 + 7 v70 + 7 v94 + 7 v103 + 7 v105 + 3 v114 <= 72
D94: 7 v1 + 7 v11 + 14 v12 + 7 v16 + 7 v17 + 7 v48 + 7 v49 + 7 v50 + 7 v52 + 7 v53 + 7 v54 + 7 v64 + 7 v65 + 7 v70 + 7 v94 + 7 v103 + 7 v105 + 3 v114 >= 57
C95: v1 + v2 + 2 v3 + 3 v4 + v6 + v7 + 2 v8 + 2 v9 + v10 + v11 + 2 v14 + 2 v16 + v24 + v25 + v26 + 2 v27 + 2 v29 + 2 v30 + 3 v31 + v34 + 3 v36 + 2 v37 + v38 + v39 + v41 + 2 v44 + 3 v46 + 2 v47 + 4 v48 + v49 + 2 v51 + 3 v52 + 2 v53 + 2 v54 + v55 + v56 + v58 + 2 v59 + 2 v61 + v62 + 3 v63 + 2 v65 + 3 v67 + 3 v69 + v70 + v72 + v76 + 2 v77 + 3 v79 + v80 + v81 + v82 + 3 v83 + 2 v84 + 3 v86 + 2 v88 + v89 + v91 + 3 v92 + v93 + v95 + 2 v96 + 3 v97 + v98 + 2 v99 + v100 + v101 + v102 + 2 v103 + 2 v104 + 2 v109 + v110 + v111 + v112 + v113 <= 72
D95: v1 + v2 + 2 v3 + 3 v4 + v6 + v7 + 2 v8 + 2 v9 + v10 + v11 + 2 v14 + 2 v16 + v24 + v25 + v26 + 2 v27 + 2 v29 + 2 v30 + 3 v31 + v34 + 3 v36 + 2 v37 + v38 + v39 + v41 + 2 v44 + 3 v46 + 2 v47 + 4 v48 + v49 + 2 v51 + 3 v52 + 2 v53 + 2 v54 + v55 + v56 + v58 + 2 v59 + 2 v61 + v62 + 3 v63 + 2 v65 + 3 v67 + 3 v69 + v70 + v72 + v76 + 2 v77 + 3 v79 + v80 + v81 + v82 + 3 v83 + 2 v84 + 3 v86 + 2 v88 + v89 + v91 + 3 v92 + v93 + v95 + 2 v96 + 3 v97 + v98 + 2 v99 + v100 + v101 + v102 + 2 v103 + 2 v104 + 2 v109 + v110 + v111 + v112 + v113 >= 57
C96: v1 + 4 v4 + 2 v6 + 2 v7 + 2 v8 + v9 + v10 + v11 + 2 v12 + 4 v13 + v15 + v17 + 2 v18 + 2 v21 + v22 + 4 v25 + v26 + 3 v27 + 2 v30 + v35 + 2 v37 + v38 + 2 v40 + v41 + 2 v42 + 2 v43 + 3 v44 + v45 + v47 + 4 v49 + 2 v50 + 2 v53 + 2 v54 + 2 v55 + v56 + v57 + v59 + 2 v62 + v63 + v64 + 2 v66 + 4 v67 + v68 + v69 + v70 + v73 + v74 + v75 + v76 + v77 + 2 v78 + v79 + 2 v81 + 2 v82 + 2 v83 + v84 + v86 + 2 v88 + 3 v89 + 2 v90 + 2 v91 + v94 + 4 v95 + v96 + v97 + v99 + v100 + 2 v101 + 2 v102 + v103 + v104 + v107 + 2 v108 + v110 + v111 + v112 + 2 v113 <= 72
D96: v1 + 4 v4 + 2 v6 + 2 v7 + 2 v8 + v9 + v10 + v11 + 2 v12 + 4 v13 + v15 + v17 + 2 v18 + 2 v21 + v22 + 4 v25 + v26 + 3 v27 + 2 v30 + v35 + 2 v37 + v38 + 2 v40 + v41 + 2 v42 + 2 v43 + 3 v44 + v45 + v47 + 4 v49 + 2 v50 + 2 v53 + 2 v54 + 2 v55 + v56 + v57 + v59 + 2 v62 + v63 + v64 + 2 v66 + 4 v67 + v68 + v69 + v70 + v73 + v74 + v75 + v76 + v77 + 2 v78 + v79 + 2 v81 + 2 v82 + 2 v83 + v84 + v86 + 2 v88 + 3 v89 + 2 v90 + 2 v91 + v94 + 4 v95 + v96 + v97 + v99 + v100 + 2 v101 + 2 v102 + v103 + v104 + v107 + 2 v108 + v110 + v111 + v112 + 2 v113 >= 57
C97: v2 + 3 v4 + 2 v6 + 3 v7 + v9 + v10 + v11 + v12 + 2 v14 + 2 v16 + v17 + v18 + v19 + 3 v20 + v21 + v23 + 2 v26 + v27 + 2 v28 + 3 v29 + v30 + v33 + 5 v35 + 2 v36 + v37 + v38 + v39 + v41 + 2 v45 + v48 + 2 v49 + 2 v51 + 2 v52 + v54 + v55 + 3 v56 + 2 v57 + 3 v59 + 2 v60 + 2 v61 + 3 v63 + v64 + 3 v65 + 2 v67 + v68 + v70 + v71 + v72 + 2 v73 + v75 + v76 + v78 + 2 v81 + 5 v82 + v83 + v84 + 3 v85 + v86 + v87 + v88 + 2 v89 + v91 + 2 v94 + v95 + 2 v99 + v100 + 3 v101 + v102 + v104 + 2 v105 + v106 + v107 + v108 + v109 + 2 v110 + 2 v111 + 2 v112 + v113 <= 72
D97: v2 + 3 v4 + 2 v6 + 3 v7 + v9 + v10 + v11 + v12 + 2 v14 + 2 v16 + v17 + v18 + v19 + 3 v20 + v21 + v23 + 2 v26 + v27 + 2 v28 + 3 v29 + v30 + v33 + 5 v35 + 2 v36 + v37 + v38 + v39 + v41 + 2 v45 + v48 + 2 v49 + 2 v51 + 2 v52 + v54 + v55 + 3 v56 + 2 v57 + 3 v59 + 2 v60 + 2 v61 + 3 v63 + v64 + 3 v65 + 2 v67 + v68 + v70 + v71 + v72 + 2 v73 + v75 + v76 + v78 + 2 v81 + 5 v82 + v83 + v84 + 3 v85 + v86 + v87 + v88 + 2 v89 + v91 + 2 v94 + v95 + 2 v99 + v100 + 3 v101 + v102 + v104 + 2 v105 + v106 + v107 + v108 + v109 + 2 v110 + 2 v111 + 2 v112 + v113 >= 57
C98: v1 + 2 v2 + 2 v3 + 4 v6 + v8 + v10 + 2 v11 + 3 v14 + v17 + v19 + v20 + 2 v25 + v26 + v27 + v28 + v29 + v30 + v31 + v33 + 3 v34 + 2 v36 + v37 + 2 v38 + 2 v39 + v40 + 4 v43 + v44 + 2 v46 + 2 v47 + v48 + 2 v49 + 2 v51 + v52 + 2 v53 + v54 + v55 + 2 v56 + 2 v57 + 2 v58 + v59 + v60 + v62 + 2 v64 + v65 + v66 + v67 + v70 + v71 + v72 + 2 v74 + v75 + 5 v78 + 3 v79 + 3 v80 + 3 v81 + v82 + 2 v83 + 2 v85 + v86 + v88 + v90 + 3 v91 + v92 + 3 v94 + v95 + 3 v98 + 2 v101 + 2 v102 + v103 + 2 v105 + 2 v107 + v108 + v109 + v110 + 3 v111 + 2 v112 + v113 <= 72
D98: v1 + 2 v2 + 2 v3 + 4 v6 + v8 + v10 + 2 v11 + 3 v14 + v17 + v19 + v20 + 2 v25 + v26 + v27 + v28 + v29 + v30 + v31 + v33 + 3 v34 + 2 v36 + v37 + 2 v38 + 2 v39 + v40 + 4 v43 + v44 + 2 v46 + 2 v47 + v48 + 2 v49 + 2 v51 + v52 + 2 v53 + v54 + v55 + 2 v56 + 2 v57 + 2 v58 + v59 + v60 + v62 + 2 v64 + v65 + v66 + v67 + v70 + v71 + v72 + 2 v74 + v75 + 5 v78 + 3 v79 + 3 v80 + 3 v81 + v82 + 2 v83 + 2 v85 + v86 + v88 + v90 + 3 v91 + v92 + 3 v94 + v95 + 3 v98 + 2 v101 + 2 v102 + v103 + 2 v105 + 2 v107 + v108 + v109 + v110 + 3 v111 + 2 v112 + v113 >= 57
C99: 3 v1 + 2 v2 + v7 + 4 v8 + v9 + v11 + v13 + 2 v16 + v17 + v18 + 2 v19 + v20 + v23 + v24 + 5 v25 + 2 v26 + 2 v27 + 2 v28 + 2 v29 + v30 + 2 v31 + v32 + 2 v34 + 3 v35 + v36 + v39 + v40 + v42 + 3 v44 + v46 + 2 v47 + 2 v48 + 2 v49 + 3 v50 + v51 + v52 + v55 + 2 v56 + 3 v58 + 2 v60 + 4 v61 + v62 + v63 + v65 + v67 + 2 v68 + 2 v69 + v70 + v72 + v73 + v74 + 3 v75 + v76 + 2 v77 + 2 v78 + v80 + v82 + v84 + 2 v85 + v89 + v90 + v91 + v94 + 3 v97 + 2 v98 + v100 + v102 + 2 v104 + 3 v105 + v106 + 2 v107 + 2 v108 + v109 + v110 + v111 + 2 v112 + 3 v113 <= 72
D99: 3 v1 + 2 v2 + v7 + 4 v8 + v9 + v11 + v13 + 2 v16 + v17 + v18 + 2 v19 + v20 + v23 + v24 + 5 v25 + 2 v26 + 2 v27 + 2 v28 + 2 v29 + v30 + 2 v31 + v32 + 2 v34 + 3 v35 + v36 + v39 + v40 + v42 + 3 v44 + v46 + 2 v47 + 2 v48 + 2 v49 + 3 v50 + v51 + v52 + v55 + 2 v56 + 3 v58 + 2 v60 + 4 v61 + v62 + v63 + v65 + v67 + 2 v68 + 2 v69 + v70 + v72 + v73 + v74 + 3 v75 + v76 + 2 v77 + 2 v78 + v80 + v82 + v84 + 2 v85 + v89 + v90 + v91 + v94 + 3 v97 + 2 v98 + v100 + v102 + 2 v104 + 3 v105 + v106 + 2 v107 + 2 v108 + v109 + v110 + v111 + 2 v112 + 3 v113 >= 57
C100: 6 v2 + v3 + v4 + v5 + 2 v7 + v8 + v9 + v10 + 2 v11 + v12 + 2 v13 + v14 + v15 + v16 + v19 + v20 + v21 + v22 + 2 v23 + v25 + 2 v26 + 2 v27 + v28 + v31 + 2 v32 + 2 v33 + v35 + v36 + 2 v37 + v38 + 3 v39 + 3 v41 + 3 v44 + 3 v45 + 2 v46 + 2 v47 + v49 + 2 v52 + 3 v53 + 2 v54 + v56 + 2 v58 + v61 + 2 v62 + v63 + 2 v65 + 2 v66 + v68 + 3 v69 + 2 v70 + 2 v71 + 2 v72 + v73 + v74 + 4 v75 + v76 + v77 + v79 + v81 + 2 v83 + v85 + v86 + v87 + v89 + v90 + v91 + 2 v94 + v95 + 2 v96 + 2 v100 + 4 v101 + v102 + v103 + v105 + v108 + v110 + 3 v111 + 2 v112 + v113 <= 72
D100: 6 v2 + v3 + v4 + v5 + 2 v7 + v8 + v9 + v10 + 2 v11 + v12 + 2 v13 + v14 + v15 + v16 + v19 + v20 + v21 + v22 + 2 v23 + v25 + 2 v26 + 2 v27 + v28 + v31 + 2 v32 + 2 v33 + v35 + v36 + 2 v37 + v38 + 3 v39 + 3 v41 + 3 v44 + 3 v45 + 2 v46 + 2 v47 + v49 + 2 v52 + 3 v53 + 2 v54 + v56 + 2 v58 + v61 + 2 v62 + v63 + 2 v65 + 2 v66 + v68 + 3 v69 + 2 v70 + 2 v71 + 2 v72 + v73 + v74 + 4 v75 + v76 + v77 + v79 + v81 + 2 v83 + v85 + v86 + v87 + v89 + v90 + v91 + 2 v94 + v95 + 2 v96 + 2 v100 + 4 v101 + v102 + v103 + v105 + v108 + v110 + 3 v111 + 2 v112 + v113 >= 57
C101: v2 + 3 v3 + v4 + 3 v5 + 2 v6 + v8 + 2 v10 + v11 + 2 v12 + v13 + v15 + v17 + 3 v18 + 2 v19 + v20 + 2 v23 + v24 + v25 + 3 v27 + 3 v31 + 2 v32 + v35 + v36 + v38 + 2 v40 + v44 + 2 v45 + 2 v47 + v49 + v50 + v51 + 5 v52 + v53 + 2 v54 + v55 + 2 v56 + 3 v57 + 3 v58 + v59 + v61 + v62 + 2 v65 + 2 v68 + v70 + v71 + 2 v73 + 4 v74 + 2 v76 + v77 + v78 + 2 v80 + v81 + v82 + 3 v83 + v84 + 2 v85 + 2 v86 + v88 + 3 v89 + v90 + v92 + v94 + v95 + v96 + v98 + 2 v99 + v102 + v103 + 3 v104 + v106 + 2 v108 + 2 v109 + 2 v110 + 2 v111 + 2 v112 + 3 v113 <= 72
D101: v2 + 3 v3 + v4 + 3 v5 + 2 v6 + v8 + 2 v10 + v11 + 2 v12 + v13 + v15 + v17 + 3 v18 + 2 v19 + v20 + 2 v23 + v24 + v25 + 3 v27 + 3 v31 + 2 v32 + v35 + v36 + v38 + 2 v40 + v44 + 2 v45 + 2 v47 + v49 + v50 + v51 + 5 v52 + v53 + 2 v54 + v55 + 2 v56 + 3 v57 + 3 v58 + v59 + v61 + v62 + 2 v65 + 2 v68 + v70 + v71 + 2 v73 + 4 v74 + 2 v76 + v77 + v78 + 2 v80 + v81 + v82 + 3 v83 + v84 + 2 v85 + 2 v86 + v88 + 3 v89 + v90 + v92 + v94 + v95 + v96 + v98 + 2 v99 + v102 + v103 + 3 v104 + v106 + 2 v108 + 2 v109 + 2 v110 + 2 v111 + 2 v112 + 3 v113 >= 57
C102: 3 v1 + v2 + v3 + 2 v4 + v8 + v11 + 2 v12 + v14 + v17 + v18 + v19 + v21 + v23 + v24 + v27 + v28 + v29 + v30 + 3 v32 + 2 v33 + 3 v34 + v35 + 2 v36 + v37 + v39 + 2 v42 + 3 v44 + 3 v46 + v47 + 2 v48 + 3 v51 + 2 v53 + 2 v54 + v55 + 2 v57 + v59 + v60 + v61 + 3 v62 + v64 + 2 v65 + 4 v66 + 4 v68 + v70 + 2 v71 + 2 v73 + v74 + 2 v75 + v76 + v77 + 2 v78 + v79 + v80 + v81 + 2 v82 + v83 + v84 + 3 v85 + v87 + v88 + 3 v89 + v91 + v94 + 2 v95 + 3 v96 + 2 v97 + 4 v99 + 2 v101 + v102 + v103 + v104 + v106 + 3 v107 + v108 + 3 v109 + 2 v112 + v113 <= 72
D102: 3 v1 + v2 + v3 + 2 v4 + v8 + v11 + 2 v12 + v14 + v17 + v18 + v19 + v21 + v23 + v24 + v27 + v28 + v29 + v30 + 3 v32 + 2 v33 + 3 v34 + v35 + 2 v36 + v37 + v39 + 2 v42 + 3 v44 + 3 v46 + v47 + 2 v48 + 3 v51 + 2 v53 + 2 v54 + v55 + 2 v57 + v59 + v60 + v61 + 3 v62 + v64 + 2 v65 + 4 v66 + 4 v68 + v70 + 2 v71 + 2 v73 + v74 + 2 v75 + v76 + v77 + 2 v78 + v79 + v80 + v81 + 2 v82 + v83 + v84 + 3 v85 + v87 + v88 + 3 v89 + v91 + v94 + 2 v95 + 3 v96 + 2 v97 + 4 v99 + 2 v101 + v102 + v103 + v104 + v106 + 3 v107 + v108 + 3 v109 + 2 v112 + v113 >= 57
C103: v1 + v3 + 3 v4 + v7 + v9 + v10 + v11 + 2 v16 + v17 + v18 + v19 + v20 + 3 v22 + v23 + 4 v24 + 2 v25 + v26 + 2 v28 + 2 v29 + v30 + v32 + 2 v33 + v34 + v35 + v37 + v39 + v40 + v42 + v43 + 2 v44 + 4 v45 + v46 + 2 v52 + 3 v53 + 3 v57 + v58 + v59 + 2 v60 + 3 v61 + v62 + v63 + v65 + v67 + v68 + 2 v69 + v71 + v72 + 2 v73 + 2 v74 + 2 v75 + 2 v76 + v77 + 4 v78 + 2 v79 + v80 + 3 v81 + v82 + 3 v83 + v84 + v86 + v87 + v88 + 2 v90 + 2 v91 + v92 + v94 + 2 v95 + v96 + 2 v97 + v98 + v99 + v100 + v101 + 2 v103 + v104 + v105 + v106 + 2 v108 + 2 v109 + v110 + v111 + v112 + v113 + 2 v114 <= 72
D103: v1 + v3 + 3 v4 + v7 + v9 + v10 + v11 + 2 v16 + v17 + v18 + v19 + v20 + 3 v22 + v23 + 4 v24 + 2 v25 + v26 + 2 v28 + 2 v29 + v30 + v32 + 2 v33 + v34 + v35 + v37 + v39 + v40 + v42 + v43 + 2 v44 + 4 v45 + v46 + 2 v52 + 3 v53 + 3 v57 + v58 + v59 + 2 v60 + 3 v61 + v62 + v63 + v65 + v67 + v68 + 2 v69 + v71 + v72 + 2 v73 + 2 v74 + 2 v75 + 2 v76 + v77 + 4 v78 + 2 v79 + v80 + 3 v81 + v82 + 3 v83 + v84 + v86 + v87 + v88 + 2 v90 + 2 v91 + v92 + v94 + 2 v95 + v96 + 2 v97 + v98 + v99 + v100 + v101 + 2 v103 + v104 + v105 + v106 + 2 v108 + 2 v109 + v110 + v111 + v112 + v113 + 2 v114 >= 57
C104: v2 + v3 + v6 + v7 + v11 + 2 v12 + v14 + 2 v15 + v16 + v19 + v20 + v21 + v23 + v25 + 4 v26 + 2 v27 + 5 v28 + v29 + v30 + 4 v32 + 2 v34 + v36 + v37 + v38 + 3 v40 + v41 + v42 + 2 v43 + 2 v44 + v45 + v47 + v48 + 3 v50 + v51 + 2 v53 + v55 + 3 v56 + 2 v59 + 2 v61 + v63 + 3 v66 + v67 + v69 + v70 + 2 v71 + 2 v72 + v74 + 2 v76 + v77 + v79 + 3 v80 + 2 v82 + 3 v83 + 2 v84 + v85 + 2 v86 + 2 v87 + v88 + 3 v89 + v90 + v91 + 2 v92 + v93 + 2 v94 + v95 + v97 + v99 + v100 + v101 + 2 v102 + 2 v103 + v104 + v105 + v106 + v107 + v108 + v109 + v110 + v111 + 3 v112 + 2 v113 + v114 <= 72
D104: v2 + v3 + v6 + v7 + v11 + 2 v12 + v14 + 2 v15 + v16 + v19 + v20 + v21 + v23 + v25 + 4 v26 + 2 v27 + 5 v28 + v29 + v30 + 4 v32 + 2 v34 + v36 + v37 + v38 + 3 v40 + v41 + v42 + 2 v43 + 2 v44 + v45 + v47 + v48 + 3 v50 + v51 + 2 v53 + v55 + 3 v56 + 2 v59 + 2 v61 + v63 + 3 v66 + v67 + v69 + v70 + 2 v71 + 2 v72 + v74 + 2 v76 + v77 + v79 + 3 v80 + 2 v82 + 3 v83 + 2 v84 + v85 + 2 v86 + 2 v87 + v88 + 3 v89 + v90 + v91 + 2 v92 + v93 + 2 v94 + v95 + v97 + v99 + v100 + v101 + 2 v102 + 2 v103 + v104 + v105 + v106 + v107 + v108 + v109 + v110 + v111 + 3 v112 + 2 v113 + v114 >= 57
C105: v2 + v4 + 2 v5 + v8 + 2 v10 + v12 + 2 v13 + v14 + 5 v15 + 2 v16 + v17 + 2 v19 + v20 + v21 + v23 + 3 v24 + 3 v25 + v26 + 2 v27 + v29 + 2 v32 + v33 + 2 v34 + 2 v36 + 3 v38 + v39 + 2 v42 + v44 + v45 + 2 v46 + 2 v47 + v51 + v52 + v53 + v54 + 2 v55 + v57 + v59 + 2 v60 + 3 v61 + 4 v64 + 2 v65 + 3 v67 + v68 + v69 + 2 v70 + 2 v71 + v72 + 2 v73 + v75 + v77 + v78 + 2 v79 + 2 v82 + 3 v83 + 2 v85 + v87 + 4 v88 + 2 v89 + v91 + 2 v92 + 2 v94 + v95 + v96 + 2 v98 + 3 v100 + v101 + v102 + v103 + 2 v105 + v108 + 2 v109 + 2 v110 + 2 v112 + 2 v113 <= 72
D105: v2 + v4 + 2 v5 + v8 + 2 v10 + v12 + 2 v13 + v14 + 5 v15 + 2 v16 + v17 + 2 v19 + v20 + v21 + v23 + 3 v24 + 3 v25 + v26 + 2 v27 + v29 + 2 v32 + v33 + 2 v34 + 2 v36 + 3 v38 + v39 + 2 v42 + v44 + v45 + 2 v46 + 2 v47 + v51 + v52 + v53 + v54 + 2 v55 + v57 + v59 + 2 v60 + 3 v61 + 4 v64 + 2 v65 + 3 v67 + v68 + v69 + 2 v70 + 2 v71 + v72 + 2 v73 + v75 + v77 + v78 + 2 v79 + 2 v82 + 3 v83 + 2 v85 + v87 + 4 v88 + 2 v89 + v91 + 2 v92 + 2 v94 + v95 + v96 + 2 v98 + 3 v100 + v101 + v102 + v103 + 2 v105 + v108 + 2 v109 + 2 v110 + 2 v112 + 2 v113 >= 57
C106: v2 + 2 v3 + v4 + v5 + 3 v7 + v9 + 2 v10 + v11 + 3 v12 + 2 v13 + v15 + v17 + v19 + v21 + 3 v22 + 4 v23 + v24 + v25 + 2 v26 + v28 + 2 v29 + v30 + v32 + 2 v34 + 2 v35 + 2 v36 + v38 + v43 + 2 v44 + v45 + v46 + 3 v47 + 2 v49 + v52 + 3 v54 + v55 + 2 v58 + 2 v59 + v62 + 2 v63 + 3 v64 + v65 + v66 + v67 + v68 + 2 v69 + 2 v71 + 3 v72 + 2 v74 + 4 v76 + v77 + 2 v78 + v79 + 3 v82 + v83 + v85 + v87 + v88 + v89 + 2 v90 + 3 v91 + v92 + v93 + 2 v96 + 2 v97 + 3 v98 + v99 + v102 + v103 + 2 v104 + 2 v105 + 3 v107 + 2 v108 + 2 v109 + 2 v111 + v112 <= 72
D106: v2 + 2 v3 + v4 + v5 + 3 v7 + v9 + 2 v10 + v11 + 3 v12 + 2 v13 + v15 + v17 + v19 + v21 + 3 v22 + 4 v23 + v24 + v25 + 2 v26 + v28 + 2 v29 + v30 + v32 + 2 v34 + 2 v35 + 2 v36 + v38 + v43 + 2 v44 + v45 + v46 + 3 v47 + 2 v49 + v52 + 3 v54 + v55 + 2 v58 + 2 v59 + v62 + 2 v63 + 3 v64 + v65 + v66 + v67 + v68 + 2 v69 + 2 v71 + 3 v72 + 2 v74 + 4 v76 + v77 + 2 v78 + v79 + 3 v82 + v83 + v85 + v87 + v88 + v89 + 2 v90 + 3 v91 + v92 + v93 + 2 v96 + 2 v97 + 3 v98 + v99 + v102 + v103 + 2 v104 + 2 v105 + 3 v107 + 2 v108 + 2 v109 + 2 v111 + v112 >= 57
C107: v1 + v2 + v4 + v5 + 2 v8 + v9 + v10 + v12 + 2 v13 + v14 + v16 + 3 v18 + 2 v19 + v21 + v23 + v24 + v27 + 2 v28 + v29 + v30 + v31 + v33 + 2 v35 + v36 + v37 + v38 + v40 + 3 v43 + v45 + v46 + 4 v48 + v49 + 2 v50 + v51 + 2 v52 + v55 + 2 v57 + 2 v58 + v59 + v63 + 3 v64 + 2 v65 + 4 v66 + v67 + 4 v69 + 2 v70 + v71 + v72 + v73 + v74 + 3 v75 + 2 v76 + 3 v77 + v78 + v79 + v80 + 3 v81 + 2 v82 + 2 v83 + v84 + 2 v85 + v86 + 5 v87 + 3 v88 + 3 v90 + v91 + v92 + v96 + v98 + v100 + v101 + v102 + v103 + v107 + 2 v108 + 2 v109 + v110 + v111 + 3 v112 + 2 v113 <= 72
D107: v1 + v2 + v4 + v5 + 2 v8 + v9 + v10 + v12 + 2 v13 + v14 + v16 + 3 v18 + 2 v19 + v21 + v23 + v24 + v27 + 2 v28 + v29 + v30 + v31 + v33 + 2 v35 + v36 + v37 + v38 + v40 + 3 v43 + v45 + v46 + 4 v48 + v49 + 2 v50 + v51 + 2 v52 + v55 + 2 v57 + 2 v58 + v59 + v63 + 3 v64 + 2 v65 + 4 v66 + v67 + 4 v69 + 2 v70 + v71 + v72 + v73 + v74 + 3 v75 + 2 v76 + 3 v77 + v78 + v79 + v80 + 3 v81 + 2 v82 + 2 v83 + v84 + 2 v85 + v86 + 5 v87 + 3 v88 + 3 v90 + v91 + v92 + v96 + v98 + v100 + v101 + v102 + v103 + v107 + 2 v108 + 2 v109 + v110 + v111 + 3 v112 + 2 v113 >= 57
C108: v3 + 2 v5 + v6 + v7 + 2 v9 + 2 v10 + v12 + v13 + 2 v14 + 2 v16 + v17 + v18 + v19 + 2 v20 + 2 v21 + 3 v22 + 2 v24 + v25 + v26 + 2 v27 + v30 + 2 v32 + v33 + v37 + 2 v39 + v40 + 2 v41 + v43 + v44 + 2 v46 + v48 + 4 v50 + v51 + v52 + v54 + 2 v56 + 2 v59 + v60 + 2 v61 + v62 + v63 + v64 + 3 v65 + v66 + v67 + 3 v68 + 3 v69 + v70 + v71 + v72 + 3 v74 + v76 + 2 v77 + 3 v78 + v79 + 2 v81 + v83 + v85 + 4 v86 + v87 + 3 v88 + 4 v89 + v91 + v95 + v96 + 2 v97 + 2 v98 + 3 v101 + v103 + 3 v105 + v106 + 4 v107 + v109 + 2 v110 + 2 v111 + v112 + v113 <= 72
D108: v3 + 2 v5 + v6 + v7 + 2 v9 + 2 v10 + v12 + v13 + 2 v14 + 2 v16 + v17 + v18 + v19 + 2 v20 + 2 v21 + 3 v22 + 2 v24 + v25 + v26 + 2 v27 + v30 + 2 v32 + v33 + v37 + 2 v39 + v40 + 2 v41 + v43 + v44 + 2 v46 + v48 + 4 v50 + v51 + v52 + v54 + 2 v56 + 2 v59 + v60 + 2 v61 + v62 + v63 + v64 + 3 v65 + v66 + v67 + 3 v68 + 3 v69 + v70 + v71 + v72 + 3 v74 + v76 + 2 v77 + 3 v78 + v79 + 2 v81 + v83 + v85 + 4 v86 + v87 + 3 v88 + 4 v89 + v91 + v95 + v96 + 2 v97 + 2 v98 + 3 v101 + v103 + 3 v105 + v106 + 4 v107 + v109 + 2 v110 + 2 v111 + v112 + v113 >= 57
C109: v1 + v2 + v4 + 4 v6 + v11 + 2 v12 + 2 v13 + v18 + 3 v19 + 2 v21 + 3 v22 + 2 v24 + 2 v25 + v26 + v28 + 2 v29 + v30 + 2 v31 + 4 v32 + 2 v34 + 4 v35 + 4 v36 + v38 + v39 + 2 v40 + v41 + v43 + v44 + 4 v45 + 2 v46 + 2 v48 + v50 + v51 + v52 + v53 + 2 v54 + 4 v55 + v56 + v59 + v62 + v63 + v64 + v65 + v67 + v68 + 3 v70 + 2 v72 + 2 v74 + 3 v75 + v76 + 2 v77 + v78 + 2 v79 + v80 + v81 + v83 + 2 v84 + v85 + 2 v86 + v87 + 2 v88 + v89 + v90 + 2 v95 + v96 + v97 + 2 v98 + v99 + 2 v100 + v101 + 2 v102 + v103 + v104 + 2 v105 + 2 v106 + v109 + v110 + v111 <= 72
D109: v1 + v2 + v4 + 4 v6 + v11 + 2 v12 + 2 v13 + v18 + 3 v19 + 2 v21 + 3 v22 + 2 v24 + 2 v25 + v26 + v28 + 2 v29 + v30 + 2 v31 + 4 v32 + 2 v34 + 4 v35 + 4 v36 + v38 + v39 + 2 v40 + v41 + v43 + v44 + 4 v45 + 2 v46 + 2 v48 + v50 + v51 + v52 + v53 + 2 v54 + 4 v55 + v56 + v59 + v62 + v63 + v64 + v65 + v67 + v68 + 3 v70 + 2 v72 + 2 v74 + 3 v75 + v76 + 2 v77 + v78 + 2 v79 + v80 + v81 + v83 + 2 v84 + v85 + 2 v86 + v87 + 2 v88 + v89 + v90 + 2 v95 + v96 + v97 + 2 v98 + v99 + 2 v100 + v101 + 2 v102 + v103 + v104 + 2 v105 + 2 v106 + v109 + v110 + v111 >= 57
C110: 2 v1 + v2 + v3 + v5 + v6 + v7 + v8 + v10 + v11 + v12 + 3 v15 + v17 + v18 + 2 v19 + v21 + v23 + v24 + 2 v27 + v29 + v30 + v34 + v35 + v36 + 4 v37 + 2 v40 + v41 + 3 v42 + v43 + 2 v46 + v48 + 2 v49 + v51 + v52 + v54 + 4 v55 + 2 v56 + v57 + v58 + v59 + 3 v60 + v61 + 3 v62 + 3 v63 + v65 + v66 + v67 + 2 v68 + 3 v69 + v70 + 2 v71 + 2 v72 + 5 v74 + v75 + 3 v77 + v79 + v80 + v81 + 3 v82 + 2 v83 + v84 + v87 + v88 + v91 + v92 + 2 v94 + v96 + v97 + v98 + 2 v100 + 3 v101 + 2 v102 + v103 + 2 v104 + 2 v105 + 2 v106 + v107 + v108 + 2 v109 + 3 v111 + v113 + v114 <= 72
D110: 2 v1 + v2 + v3 + v5 + v6 + v7 + v8 + v10 + v11 + v12 + 3 v15 + v17 + v18 + 2 v19 + v21 + v23 + v24 + 2 v27 + v29 + v30 + v34 + v35 + v36 + 4 v37 + 2 v40 + v41 + 3 v42 + v43 + 2 v46 + v48 + 2 v49 + v51 + v52 + v54 + 4 v55 + 2 v56 + v57 + v58 + v59 + 3 v60 + v61 + 3 v62 + 3 v63 + v65 + v66 + v67 + 2 v68 + 3 v69 + v70 + 2 v71 + 2 v72 + 5 v74 + v75 + 3 v77 + v79 + v80 + v81 + 3 v82 + 2 v83 + v84 + v87 + v88 + v91 + v92 + 2 v94 + v96 + v97 + v98 + 2 v100 + 3 v101 + 2 v102 + v103 + 2 v104 + 2 v105 + 2 v106 + v107 + v108 + 2 v109 + 3 v111 + v113 + v114 >= 57
C111: v1 + v5 + v8 + 2 v9 + v10 + v12 + v14 + v15 + 4 v16 + v17 + v18 + v20 + v21 + v22 + v23 + 3 v26 + v28 + 2 v29 + 2 v30 + 4 v31 + 2 v32 + 3 v33 + v34 + v35 + v36 + 2 v37 + 2 v39 + 4 v40 + v41 + 3 v44 + v45 + 2 v46 + v49 + v50 + 2 v52 + 2 v53 + v54 + 3 v55 + v57 + v58 + v60 + v63 + 4 v64 + 2 v66 + 3 v67 + v68 + v69 + 2 v71 + 3 v74 + v75 + v77 + v78 + v79 + 2 v81 + 2 v82 + v83 + 2 v84 + 3 v85 + v89 + v90 + 2 v91 + v92 + v94 + v95 + 2 v96 + v97 + v98 + v99 + 2 v100 + v102 + v103 + 2 v104 + v106 + 2 v107 + v108 + 4 v110 + 3 v111 + v112 + v113 <= 72
D111: v1 + v5 + v8 + 2 v9 + v10 + v12 + v14 + v15 + 4 v16 + v17 + v18 + v20 + v21 + v22 + v23 + 3 v26 + v28 + 2 v29 + 2 v30 + 4 v31 + 2 v32 + 3 v33 + v34 + v35 + v36 + 2 v37 + 2 v39 + 4 v40 + v41 + 3 v44 + v45 + 2 v46 + v49 + v50 + 2 v52 + 2 v53 + v54 + 3 v55 + v57 + v58 + v60 + v63 + 4 v64 + 2 v66 + 3 v67 + v68 + v69 + 2 v71 + 3 v74 + v75 + v77 + v78 + v79 + 2 v81 + 2 v82 + v83 + 2 v84 + 3 v85 + v89 + v90 + 2 v91 + v92 + v94 + v95 + 2 v96 + v97 + v98 + v99 + 2 v100 + v102 + v103 + 2 v104 + v106 + 2 v107 + v108 + 4 v110 + 3 v111 + v112 + v113 >= 57
C112 : v1 + 4 v2 + 2 v3 + v4 + v5 + 2 v7 + 2 v8 + v9 + 2 v10 + v12 + v13 + v15 + 3 v16 + 2 v17 + v19 + v20 + v22 + v27 + 3 v29 + v32 + v33 + v35 + v36 + v38 + 2 v39 + v40 + v41 + 2 v42 + 3 v43 + v45 + v47 + 3 v49 + 2 v51 + 2 v52 + 2 v53 + 2 v55 + 2 v56 + v57 + v61 + 2 v66 + v67 + 2 v70 + 4 v72 + v73 + 3 v74 + v75 + v76 + v77 + 2 v78 + 3 v79 + v81 + v82 + 3 v84 + v86 + 3 v87 + v88 + 3 v89 + v90 + v91 + v92 + v94 + v95 + 2 v96 + 3 v97 + v98 + 3 v99 + 2 v100 + v102 + v103 + 2 v105 + v106 + 2 v107 + v108 + 3 v109 + 3 v110 + 3 v113 <= 72
D112 : v1 + 4 v2 + 2 v3 + v4 + v5 + 2 v7 + 2 v8 + v9 + 2 v10 + v12 + v13 + v15 + 3 v16 + 2 v17 + v19 + v20 + v22 + v27 + 3 v29 + v32 + v33 + v35 + v36 + v38 + 2 v39 + v40 + v41 + 2 v42 + 3 v43 + v45 + v47 + 3 v49 + 2 v51 + 2 v52 + 2 v53 + 2 v55 + 2 v56 + v57 + v61 + 2 v66 + v67 + 2 v70 + 4 v72 + v73 + 3 v74 + v75 + v76 + v77 + 2 v78 + 3 v79 + v81 + v82 + 3 v84 + v86 + 3 v87 + v88 + 3 v89 + v90 + v91 + v92 + v94 + v95 + 2 v96 + 3 v97 + v98 + 3 v99 + 2 v100 + v102 + v103 + 2 v105 + v106 + 2 v107 + v108 + 3 v109 + 3 v110 + 3 v113 >= 57
C113 : v0 + 3 v1 + 2 v3 + 2 v5 + v6 + 2 v7 + 2 v8 + v10 + v11 + v12 + v13 + v14 + v15 + 2 v16 + 5 v21 + v23 + v24 + v25 + v27 + 2 v28 + v29 + v30 + v32 + 2 v33 + v35 + 2 v38 + v39 + 2 v41 + 3 v43 + 2 v44 + 2 v45 + v46 + v48 + v51 + v52 + v53 + 2 v54 + 2 v55 + 3 v56 + 2 v58 + v59 + v61 + v62 + v63 + v64 + 2 v65 + 2 v67 + v69 + v71 + v72 + 2 v73 + v74 + 2 v76 + 3 v77 + 2 v78 + v79 + v80 + v81 + v82 + 3 v83 + 3 v85 + v87 + v90 + v91 + v94 + v95 + 2 v96 + 2 v97 + 2 v98 + 2 v99 + 2 v100 + 2 v101 + v102 + 3 v103 + 2 v104 + v105 +
3 v106 + v107 + v110 + v112 + 3 v113 <= 72
D113 : v0 + 3 v1 + 2 v3 + 2 v5 + v6 + 2 v7 + 2 v8 + v10 + v11 + v12 + v13 + v14 + v15 + 2 v16 + 5 v21 + v23 + v24 + v25 + v27 + 2 v28 + v29 + v30 + v32 + 2 v33 + v35 + 2 v38 + v39 + 2 v41 + 3 v43 + 2 v44 + 2 v45 + v46 + v48 + v51 + v52 + v53 + 2 v54 + 2 v55 + 3 v56 + 2 v58 + v59 + v61 + v62 + v63 + v64 + 2 v65 + 2 v67 + v69 + v71 + v72 + 2 v73 + v74 + 2 v76 + 3 v77 + 2 v78 + v79 + v80 + v81 + v82 + 3 v83 + 3 v85 + v87 + v90 + v91 + v94 + v95 + 2 v96 + 2 v97 + 2 v98 + 2 v99 + 2 v100 + 2 v101 + v102 + 3 v103 + 2 v104 + v105 + 3 v106 + v107 + v110 + v112 + 3 v113 >= 57
C114 : v0 + v1 + 2 v2 + 3 v4 + v6 + v7 + v9 + v10 + v11 + v14 + v15 + 2 v18 + v20 + v23 + 4 v24 + 2 v26 + 2 v29 + v30 + v31 + v32 + v34 + v35 + v38 + 2 v39 + v40 + v41 + 2 v42 + 2 v46 + 2 v47 + 2 v49 + 4 v50 + 2 v51 + v52 + 2 v53 + 3 v54 + v56 + v57 + 2 v58 + v59 + 3 v60 + v63 + v64 + v65 + 2 v66 + 3 v67 + 2 v68 + 2 v70 + 2 v72 + 2 v74 + 2 v75 + 2 v76 + v78 + 2 v80 + v82 + v83 + v84 + v86 + 3 v87 + v88 + v89 + v90 + v91 + v92 + v94 + 2 v95 + v96 + v97 + 3 v98 + v99 + 3 v100 + v101 + v102 + 2 v103 + 2 v104 + 2 v106 + v107 + v109 + v110 + 3 v111 + 3 v112 + v113 <= 72
D114 : v0 + v1 + 2 v2 + 3 v4 + v6 + v7 + v9 + v10 + v11 + v14 + v15 + 2 v18 + v20 + v23 + 4 v24 + 2 v26 + 2 v29 + v30 + v31 + v32 + v34 + v35 + v38 + 2 v39 + v40 + v41 + 2 v42 + 2 v46 + 2 v47 + 2 v49 + 4 v50 + 2 v51 + v52 + 2 v53 + 3 v54 + v56 + v57 + 2 v58 + v59 + 3 v60 + v63 + v64 + v65 + 2 v66 + 3 v67 + 2 v68 + 2 v70 + 2 v72 + 2 v74 + 2 v75 + 2 v76 + v78 + 2 v80 + v82 + v83 + v84 + v86 + 3 v87 + v88 + v89 + v90 + v91 + v92 + v94 + 2 v95 + v96 + v97 + 3 v98 + v99 + 3 v100 + v101 + v102 + 2 v103 + 2 v104 + 2 v106 + v107 + v109 + v110 + 3 v111 + 3 v112 + v113 >= 57
C115 : 7 v5 + 7 v7 + 7 v16 + 7 v22 + 7 v58 + 7 v60 + 7 v62 + 7 v67 + 7 v70 + 7 v75 + 7 v80 + 7 v81 + 7 v85 + 7 v89 + 3 v93 + 14 v102 + 7 v103 + 7 v109 <= 70
D115 : 7 v5 + 7 v7 + 7 v16 + 7 v22 + 7 v58 + 7 v60 + 7 v62 + 7 v67 + 7 v70 + 7 v75 + 7 v80 + 7 v81 + 7 v85 + 7 v89 + 3 v93 + 14 v102 + 7 v103 + 7 v109 >= 59
F: v0 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 + v32 + v33 + v34 + v35 + v36 + v37 + v38 + v39 + v40 + v41 + v42 + v43 + v44 + v45 + v46 + v47 + v48 + v49 + v50 + v51 + v52 + v53 + v54 + v55 + v56 + v57 + v58 + v59 + v60 + v61 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + v69 + v70 + v71 + v72 + v73 + v74 + v75 + v76 + v77 + v78 + v79 + v80 + v81 + v82 + v83 + v84 + v85 + v86 + v87 + v88 + v89 + v90 + v91 + v92 + v94 + v95 + v96 + v97 + v98 + v99 + v100 + v101 + v102 + v103 + v104 + v105 + v106 + v107 + v108 + v109 + v110 + v111 + v112 + v113 + v114 = 57
Binaries
v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34 v35 v36 v37 v38 v39 v40 v41 v42 v43 v44 v45 v46 v47 v48 v49 v50 v51 v52 v53 v54 v55 v56 v57 v58 v59 v60 v61 v62 v63 v64 v65 v66 v67 v68 v69 v70 v71 v72 v73 v74 v75 v76 v77 v78 v79 v80 v81 v82 v83 v84 v85 v86 v87 v88 v89 v90 v91 v92 v93 v94 v95 v96 v97 v98 v99 v100 v101 v102 v103 v104 v105 v106 v107 v108 v109 v110 v111 v112 v113 v114
EndBest regards,
Santanu
0 -
Hi Santanu,
What exactly do you mean by being not able to solve but the problem becomes faster?
Do you have the possibility to provide a good starting point, e.g., you know that \(v_1\) should be 0 for some reason etc. You could then provide this partial starting point as an initial point.
The constraints look as if they could be linearly dependent or almost linearly dependent. Do you have any information on how the constraints are generated and if they could indeed be linearly dependent?
Best regards,
Jaromił0 -
Dear Jaromił
Thanks a lot.
What exactly do you mean by being not able to solve but the problem becomes faster?
Really sorry for not writing clearly.
If we remove constraints C1, D1 and C2, we can solve. Now if we introduce
v0 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13
+ v14 + v15 + v16 + v17 + v18 + v19 + v20+ v21 + v22 + v23 + v24 + v25
+ v26 + v27 + v28 + v29 + v30 + v31 + v32 + v33 + v34 + v35 + v36
+ v37 + v38 + v39 + v40 + v41 + v42 + v43 + v44 + v45 + v46 + v47
+ v48 + v49 + v50 + v51 + v52 + v53 + v54 + v55 + v56 + v57 + v58
+ v59 + v60 + v61 + v62 + v63 + v64 + v65 + v66 + v67 + v68 + v69
+ v70 + v71 + v72 + v73 + v74 + v75 + v76 + v77 + v78 + v79 + v80
+ v81 + v82 + v83 + v84 + v85 + v86 + v87 + v88 + v89 + v90 + v91
+ v92 + v94 + v95 + v96 + v97 + v98 + v99 + v100 + v101 + v102
+ v103 + v104 + v105 + v106 + v107 + v108 + v109 + v110 + v111
+ v112 + v113 + v114 = 57we get solution faster. However if we include again C1, D1 and C2, I am not getting solution.
Do you have any information on how the constraints are generated and if they could indeed be linearly dependent?
It seems they are not linearly dependent.
I am trying to implement the paper "Patterson-Wiedemann Type Functions on 21 Variables With Nonlinearity Greater Than Bent Concatenation Bound"
published in IEEE Trans. Inf. Theory. In this paper, authors used C programming to get 4 solutions. I am trying to find a solution using Gurobi.Thanks again for your help.
Best regards,
Santanu
0 -
Dear Santanu,
There may be several reasons for Gurobi being able to solve the problem faster without constraints C1, D1 and C2. It can be that the equality you introduced provides some specific structure or variable information to the problem which allows Gurobi to detect and/or eliminate large parts of the search space. The authors of the paper you mentioned, say that over a month was needed to find the 4 solutions they report using a specialized heuristic. This is a clear indicator that this problem is extremely hard and will most likely not be solved within a few hours using MIP technology.
Two other things I would like to note:
1. In the paper the authors state that the bounds of all constraints have to be \(57 \leq \dots \leq 72\) but the bounds for C1 and D1 in your problem are \(63 \leq \dots \leq 66\). Is this desired?
2. The authors also state that removing specific constraints provides a symmetrical coefficient matrix. Maybe, you can use this information to construct a heuristic yourself which breaks the symmetry or computes a feasible solution to this symmetrical problem fast which can be re-used for the whole problem.
Best regards,
Jaromił0 -
Dear Jaromił,
Thanks a lot for your help. Authors of that paper used C programming language with a heuristics to find solutions. They got 4 solutions using 6 cores within 1 month. I tried to solve using Gurobi. I have 48 cores. It was running for 7 days without giving any solution.
1. For binary values of v's, 57<= 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 <=72 actually
gives 63<= 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 <=66. That is 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 can not be 57,58,...,62 for binary values of v.
2. I tried to use symmetry but so far I do not get any good heuristic.
Best regards,
Santanu
0 -
Dear Santanu,
1. OK, this is correct.
2. You could try contacting the authors for more input.
Please note that the authors of the paper used different heuristics, which are specialized for this kind of problem and are currently not part of Gurobi. The authors are flipping bits of specific variable values to finally end up with a feasible solution. Thus, given the drastic complexity of the problem, we cannot expect to find feasible solutions even with the increased core number and a runtime of 7 days.
This does not mean that it is impossible to find feasible solutions to this problem with Gurobi or any MIP solver. It just means that it will most likely not work out of the box.
My knowledge on cryptography and boolean functions is only limited. You could try to contact people in the corresponding community for more input.
Best regards,
Jaromił0
Please sign in to leave a comment.
Comments
10 comments