No optimization function

Ongoing

Comments

10 comments

  • Jaromił Najman

    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
    Comment actions Permalink
  • Santanu Sarkar

    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
    Comment actions Permalink
  • Jaromił Najman

    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
    Comment actions Permalink
  • 0
    Comment actions Permalink
  • Santanu Sarkar

    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

    End

    Best regards,

    Santanu

     

    0
    Comment actions Permalink
  • Jaromił Najman

    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
    Comment actions Permalink
  • Santanu Sarkar

    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 = 57

    we 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
    Comment actions Permalink
  • Jaromił Najman

    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
    Comment actions Permalink
  • Santanu Sarkar

    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
    Comment actions Permalink
  • Jaromił Najman

    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
    Comment actions Permalink

Please sign in to leave a comment.

Powered by Zendesk