• Gurobi Staff

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ł

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

• Gurobi Staff

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ł

• Gurobi Staff

This is a cross-post from https://stackoverflow.com/questions/63764318/no-optimization-function

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 ToC1: 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 <= 66D1: 3 v0 + 21 v17 + 21 v22 + 21 v36 + 21 v37 + 21 v112 + 21 v113 >= 63C2: 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 <= 72D2: 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 >= 57C3: 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 <= 72D3: 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 >= 57C4: 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 <= 72D4: 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 >= 57C5: 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 <= 72D5: 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 >= 57C6: 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 <= 72D6: 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 >= 57C7: 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 <= 72D7: 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 >= 57C8: 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 <= 72D8: 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 >= 57C9: 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 <= 72D9: 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 >= 57C10: 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 <= 72D10: 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 >= 57C11: 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 <= 72D11: 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 >= 57C12: 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 <= 72D12: 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 >= 57C13: 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 <= 72D13: 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 >= 57C14: 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 <= 72D14: 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 >= 57C15: 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 <= 72D15: 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 >= 57C16: 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 <= 72D16: 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 >= 57C17: 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 <= 72D17: 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 >= 57C18: 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 <= 72D18: 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 >= 57C19: 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 <= 72D19: 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 >= 57C20: 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 <= 72D20: 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 >= 57C21: 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 <= 72D21: 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 >= 57C22: 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 <= 72D22: 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 >= 57C23: 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 <= 72D23: 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 >= 57C24: 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 <= 72D24: 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 >= 57C25: 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 <= 72D25: 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 >= 57C26: 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 <= 72D26: 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 >= 57C27: 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 <= 72D27: 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 >= 57C28: 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 <= 72D28: 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 >= 57C29: 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 <= 72D29: 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 >= 57C30: 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 <= 72D30: 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 >= 57C31: 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 <= 72D31: 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 >= 57C32: 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 <= 72D32: 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 >= 57C33: 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 <= 72D33: 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 >= 57C34: 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 <= 72D34: 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 >= 57C35: 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 <= 72D35: 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 >= 57C36: 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 <= 72D36: 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 >= 57C37: 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 <= 72D37: 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 >= 57C38: 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 <= 72D38: 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 >= 57C39: 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 <= 72D39: 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 >= 57C40: 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 <= 72D40: 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 >= 57C41: 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 <= 72D41: 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 >= 57C42: 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 <= 72D42: 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 >= 57C43: 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 <= 72D43: 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 >= 57C44: 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 <= 72D44: 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 >= 57C45: 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 <= 72D45: 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 >= 57C46: 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 <= 72D46: 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 >= 57C47: 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 <= 72D47: 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 >= 57C48: 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 <= 72D48: 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 >= 57C49: 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 <= 72D49: 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 >= 57C50: 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 <= 72D50: 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 >= 57C51: 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 <= 72D51: 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 >= 57C52: 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 <= 72D52: 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 >= 57C53: 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 <= 72D53: 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 >= 57C54: 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 <= 72D54: 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 >= 57C55: 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 <= 72D55: 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 >= 57C56: 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 <= 72D56: 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 >= 57C57: 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 <= 72D57: 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 >= 57C58: 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 <= 72D58: 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 >= 57C59: 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 <= 72D59: 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 >= 57C60: 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 <= 72D60: 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 >= 57C61: 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 <= 72D61: 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 >= 57C62: 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 <= 72D62: 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 >= 57C63: 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 <= 72D63: 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 >= 57C64: 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 <= 72D64: 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 >= 57C65: 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 <= 72D65: 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 >= 57C66: 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 <= 72D66: 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 >= 57C67: 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 <= 72D67: 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 >= 57C68: 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 <= 72D68: 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 >= 57C69: 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 <= 72D69: 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 >= 57C70: 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 <= 72D70: 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 >= 57C71: 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 <= 72D71: 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 >= 57C72: 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 <= 72D72: 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 >= 57C73: 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 <= 72D73: 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 >= 57C74: 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 <= 72D74: 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 >= 57C75: 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 <= 72D75: 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 >= 57C76: 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 <= 72D76: 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 >= 57C77: 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 <= 72D77: 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 >= 57C78: 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 <= 72D78: 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 >= 57C79: 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 <= 72D79: 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 >= 57C80: 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 <= 72D80: 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 >= 57C81: 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 <= 72D81: 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 >= 57C82: 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 <= 72D82: 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 >= 57C83: 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 <= 72D83: 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 >= 57C84: 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 <= 72D84: 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 >= 57C85: 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 <= 72D85: 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 >= 57C86: 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 <= 72D86: 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 >= 57C87: 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 <= 72D87: 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 >= 57C88: 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 <= 72D88: 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 >= 57C89: 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 <= 72D89: 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 >= 57C90: 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 <= 72D90: 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 >= 57C91: 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 <= 72D91: 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 >= 57C92: 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 <= 72D92: 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 >= 57C93: 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 <= 72D93: 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 >= 57C94: 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 <= 72D94: 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 >= 57C95: 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 <= 72D95: 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 >= 57C96: 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 <= 72D96: 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 >= 57C97: 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 <= 72D97: 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 >= 57C98: 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 <= 72D98: 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 >= 57C99: 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 <= 72D99: 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 >= 57C100: 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 <= 72D100: 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 >= 57C101: 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 <= 72D101: 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 >= 57C102: 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 <= 72D102: 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 >= 57C103: 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 <= 72D103: 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 >= 57C104: 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 <= 72D104: 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 >= 57C105: 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 <= 72D105: 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 >= 57C106: 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 <= 72D106: 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 >= 57C107: 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 <= 72D107: 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 >= 57C108: 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 <= 72D108: 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 >= 57C109: 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 <= 72D109: 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 >= 57C110: 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 <= 72D110: 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 >= 57C111: 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 <= 72D111: 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 >= 57C112 : 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 <= 72D112 : 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 >= 57C113 : 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 <= 72D113 : 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 >= 57C114 : 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 <= 72D114 : 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 >= 57C115 : 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 <= 70D115 : 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 >= 59F: 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 = 57Binariesv0 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 v114End

Best regards,

Santanu

• Gurobi Staff

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ł

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.

Best regards,

Santanu

• Gurobi Staff

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ł

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

• Gurobi Staff

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ł