/
rk4.out
12 lines (12 loc) · 12 KB
/
rk4.out
1
2
3
4
5
6
7
8
9
10
11
12
1:[[0,2,4,7],[0,2,4,6],[0,1,4,5],[0,2,4,5],[1,2,4,7],[3,5,6,7],[0,1,4,7],[1,2,4,6],[0,1,4,6],[1,2,4,5],[1,4,5,7],[1,4,5,6],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[0,3,4,7],[0,3,4,6],[1,3,5,7],[0,3,4,5],[1,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[0,2,5,7],[0,1,5,7],[0,2,5,6],[1,2,3,6],[0,1,5,6],[0,5,6,7],[0,3,6,7],[0,1,3,7],[0,1,3,6],[0,1,3,5],[0,1,3,4],[3,4,6,7],[2,4,5,7],[2,4,5,6],[0,4,5,7],[3,4,5,7],[0,4,5,6],[3,4,5,6],[1,3,4,7],[1,3,4,6],[1,3,6,7],[1,3,4,5],[1,2,5,7],[1,2,5,6],[0,3,5,7],[0,3,5,6],[2,5,6,7],[0,2,6,7],[1,4,6,7],[2,3,6,7],[1,5,6,7],[0,1,6,7],[0,1,2,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[0,4,6,7],[2,3,5,7],[2,3,5,6],[2,3,4,5],[2,3,4,7],[2,3,4,6],[2,4,6,7],[1,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[7]-x[8],x[9]-1,x[10]-x[14],x[13]-1]:7:[x[6]*x[8]*x[12]*x[14]-x[6]*x[8]*x[12]*x[15]+x[6]*x[8]*x[14]*x[15]-x[6]*x[8]*x[14]-x[6]*x[12]*x[14]*x[15]+x[6]*x[12]*x[15]-x[8]^2*x[14]^2+x[8]^2*x[14]+x[8]*x[12]*x[14]*x[15]-x[8]*x[12]*x[14]+x[8]*x[14]^2-x[8]*x[14]*x[15],x[6]*x[11]*x[12]*x[15]-x[6]*x[11]*x[12]*x[16]-x[6]*x[11]*x[15]*x[16]+x[6]*x[11]*x[16]+x[6]*x[12]*x[15]*x[16]-x[6]*x[12]*x[15]+x[8]*x[11]*x[16]^2-x[8]*x[11]*x[16]-x[8]*x[12]*x[14]*x[15]+x[8]*x[12]*x[14]*x[16]-x[8]*x[12]*x[15]*x[16]+x[8]*x[12]*x[15]+x[8]*x[14]*x[15]*x[16]-x[8]*x[14]*x[16]^2+x[11]*x[12]*x[15]*x[16]-x[11]*x[12]*x[15]-x[11]*x[12]*x[16]^2+x[11]*x[12]*x[16]+x[11]*x[14]*x[16]^2-x[11]*x[14]*x[16]-x[11]*x[15]*x[16]^2+x[11]*x[15]*x[16]-x[12]*x[14]*x[15]*x[16]+x[12]*x[14]*x[15]+x[12]*x[15]*x[16]^2-x[12]*x[15]*x[16],x[8]*x[11]*x[14]-x[8]*x[11]*x[16]-x[8]*x[12]*x[14]+x[8]*x[12]*x[15]-x[8]*x[14]*x[15]+x[8]*x[14]*x[16]-x[11]*x[12]*x[15]+x[11]*x[12]*x[16]-x[11]*x[14]*x[16]+x[11]*x[15]*x[16]+x[12]*x[14]*x[15]-x[12]*x[15]*x[16],x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[7]-x[8],x[9]-1,x[10]-x[14],x[13]-1]:5:false:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,x[6],x[8],x[8]],[0,0,1,0,1,x[14],x[11],x[12]],[0,0,0,1,1,x[14],x[15],x[16]]]
2:[[0,1,4,5],[0,1,4,7],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[1,3,5,6],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[2,3,4,6],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,3,4,6],[0,4,6,7],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]*x[12]-x[6]-x[8]*x[14]+x[8]-x[12]+x[14],x[7]-x[8],x[9]-1,x[10]-x[14],x[13]-1,x[15]]:5:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]*x[12]-x[6]-x[8]*x[14]+x[8]-x[12]+x[14],x[7]-x[8],x[8]*x[11]*x[14]-x[8]*x[11]*x[16]-x[8]*x[12]*x[14]+x[8]*x[14]*x[16]+x[11]*x[12]*x[16]-x[11]*x[14]*x[16],x[9]-1,x[10]-x[14],x[13]-1,x[15]]:4:false:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,x[6],x[8],x[8]],[0,0,1,0,1,x[14],x[11],x[12]],[0,0,0,1,1,x[14],0,x[16]]]
3:[[0,1,4,5],[0,1,4,7],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[2,3,4,6],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]*x[12]-x[6]-x[12]-x[14]*x[16]+x[14]+x[16],x[7]-x[16],x[8]-x[16],x[9]-1,x[10]-x[14],x[11]-x[14],x[13]-1,x[15]]:3:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]*x[12]-x[6]-x[12]-x[14]*x[16]+x[14]+x[16],x[7]-x[16],x[8]-x[16],x[9]-1,x[10]-x[14],x[11]-x[14],x[13]-1,x[15]]:3:true:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,x[6],x[16],x[16]],[0,0,1,0,1,x[14],x[14],x[12]],[0,0,0,1,1,x[14],0,x[16]]]
4:[[0,1,4,5],[0,1,4,7],[0,1,4,6],[3,4,6,7],[1,5,6,7],[0,1,3,7],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[1,3,6,7],[4,5,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,6],[2,3,5,7],[1,3,5,6],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[2,3,4,6],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[0,1,2,3],[1,2,4,7],[1,4,6,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,5],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[15],x[7]-x[15],x[8]-1,x[9]-1,x[10]-x[16],x[11]-1,x[12]-x[16],x[13]-1,x[14]-x[15]*x[16]]:2:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[15],x[7]-x[15],x[8]-1,x[9]-1,x[10]-x[16],x[11]-1,x[12]-x[16],x[13]-1,x[14]-x[15]*x[16]]:2:true:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,x[15],x[15],1],[0,0,1,0,1,x[16],1,x[16]],[0,0,0,1,1,x[15]*x[16],x[15],x[16]]]
5:[[0,1,4,5],[0,1,4,7],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[1,3,5,6],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]+x[8]*x[14]-x[8]-x[14],x[7]-x[8],x[9]-1,x[10]-x[14],x[12],x[13]-1,x[15]]:4:[x[6]*x[11]*x[14]-x[6]*x[11]*x[16]+x[6]*x[14]*x[16]+x[11]*x[14]^2*x[16]-x[11]*x[14]^2-x[14]^2*x[16],x[6]*x[11]+x[6]*x[16]+x[8]*x[11]*x[16]-x[8]*x[11]-x[8]*x[16]+x[11]*x[14]*x[16]-x[11]*x[14]-x[14]*x[16],x[6]+x[8]*x[14]-x[8]-x[14],x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[7]-x[8],x[9]-1,x[10]-x[14],x[12],x[13]-1,x[15]]:3:false:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,-x[8]*x[14]+x[8]+x[14],x[8],x[8]],[0,0,1,0,1,x[14],x[11],0],[0,0,0,1,1,x[14],0,x[16]]]
6:[[0,1,4,5],[0,1,4,7],[0,1,4,6],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[2,5,6,7],[3,4,5,7],[4,5,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[2,3,5,7],[1,3,5,6],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,6],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[0,1,2,3],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,6],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4],x[5],x[6]-1,x[7]-1,x[8]-1,x[9]-1,x[10]+x[15]-x[16]-1,x[11],x[12]-x[16],x[13]-1,x[14]-x[16]-1]:2:[x[1]-1,x[2]-1,x[3]-1,x[4],x[5],x[6]-1,x[7]-1,x[8]-1,x[9]-1,x[10]+x[15]-x[16]-1,x[11],x[12]-x[16],x[13]-1,x[14]-x[16]-1]:2:true:[[1,0,0,0,1,1,1,0],[0,1,0,0,0,1,1,1],[0,0,1,0,1,-x[15]+x[16]+1,0,x[16]],[0,0,0,1,1,x[16]+1,x[15],x[16]]]
7:[[0,1,4,5],[0,1,4,7],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[3,5,6,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,2,6,7],[0,1,6,7]]:[x[1],x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[14]-x[16],x[7]-x[16],x[8]-x[16],x[9]-1,x[10]-x[14],x[11]-x[14],x[12],x[13]-1,x[15]]:2:[x[1],x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[14]-x[16],x[7]-x[16],x[8]-x[16],x[9]-1,x[10]-x[14],x[11]-x[14],x[12],x[13]-1,x[15]]:2:true:[[1,0,0,0,0,1,1,1],[0,1,0,0,1,x[14]+x[16],x[16],x[16]],[0,0,1,0,1,x[14],x[14],0],[0,0,0,1,1,x[14],0,x[16]]]
8:[[0,1,4,5],[0,1,4,6],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[4,5,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[2,3,5,7],[1,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,6],[0,5,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[0,1,2,3],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,5,7],[0,3,5,6],[0,2,6,7],[0,1,6,7]]:[x[1],x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6],x[7]-x[15],x[8]+x[15],x[9]-1,x[10]+x[15],x[11],x[12]+x[15],x[13]-1,x[14]-x[15],x[16]]:1:[x[1],x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6],x[7]-x[15],x[8]+x[15],x[9]-1,x[10]+x[15],x[11],x[12]+x[15],x[13]-1,x[14]-x[15],x[16]]:1:true:[[1,0,0,0,0,1,1,1],[0,1,0,0,1,0,x[15],-x[15]],[0,0,1,0,1,-x[15],0,-x[15]],[0,0,0,1,1,x[15],x[15],0]]
9:[[0,1,4,5],[0,1,4,7],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,6],[0,2,5,7],[1,3,4,5],[2,4,5,7],[2,4,5,6],[1,3,5,7],[2,3,5,6],[1,2,3,5],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[0,5,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[3,5,6,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,5,7],[0,3,5,6],[0,2,6,7],[0,1,6,7]]:[1]:-9:[1]:-9:true:[[0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0]]
10:[[0,1,4,5],[3,4,6,7],[1,5,6,7],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,3,4],[0,1,5,6],[2,5,6,7],[3,4,5,7],[3,4,5,6],[1,3,6,7],[4,5,6,7],[0,2,3,4],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[1,3,5,6],[1,2,3,4],[1,2,3,7],[1,2,3,6],[2,3,4,7],[2,3,4,6],[0,5,6,7],[1,2,6,7],[0,4,5,7],[0,4,5,6],[0,1,2,7],[2,4,6,7],[0,1,2,6],[0,1,2,5],[0,1,2,4],[1,2,5,7],[0,1,2,3],[1,2,5,6],[1,2,4,7],[1,2,4,6],[1,2,4,5],[3,5,6,7],[0,2,4,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-1,x[9]-1,x[10]-1,x[13]-1,x[15],x[16]]:5:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-1,x[7]*x[8]*x[11]-x[7]*x[8]*x[12]-x[7]*x[11]*x[12]+x[7]*x[12]+x[8]*x[11]*x[12]-x[8]*x[11],x[9]-1,x[10]-1,x[13]-1,x[15],x[16]]:4:false:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,1,x[7],x[8]],[0,0,1,0,1,1,x[11],x[12]],[0,0,0,1,1,x[14],0,0]]
11:[[0,1,4,5],[0,1,4,7],[0,1,4,6],[0,1,3,7],[0,1,3,6],[1,4,5,7],[0,1,3,5],[1,4,5,6],[0,1,5,7],[0,1,5,6],[1,3,6,7],[0,2,3,5],[0,2,3,7],[0,2,3,6],[1,3,4,7],[1,3,4,6],[0,2,5,7],[1,3,4,5],[0,2,5,6],[2,4,5,7],[2,4,5,6],[1,3,5,7],[2,3,5,7],[1,3,5,6],[2,3,5,6],[1,2,3,5],[1,2,3,7],[1,2,3,6],[2,3,4,5],[2,3,4,7],[2,3,4,6],[1,2,6,7],[0,4,5,7],[0,4,5,6],[2,4,6,7],[1,2,5,7],[1,2,5,6],[1,4,6,7],[1,2,4,7],[1,2,4,6],[1,2,4,5],[0,2,4,7],[2,3,6,7],[0,2,4,6],[0,2,4,5],[0,3,4,7],[0,4,6,7],[0,3,4,6],[0,3,4,5],[0,3,5,7],[0,3,5,6],[0,3,6,7],[0,1,6,7],[0,2,6,7]]:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[8],x[7]-x[8],x[9],x[10]-1,x[11]-x[12],x[13],x[14],x[15]-1]:3:[x[1]-1,x[2]-1,x[3]-1,x[4]-1,x[5]-1,x[6]-x[8],x[7]-x[8],x[9],x[10]-1,x[11]-x[12],x[13],x[14],x[15]-1]:3:true:[[1,0,0,0,1,1,1,1],[0,1,0,0,1,x[8],x[8],x[8]],[0,0,1,0,0,1,x[12],x[12]],[0,0,0,1,0,0,1,x[16]]]
12:[[3,4,5,7],[3,4,5,6],[0,2,3,5],[0,2,3,4],[2,3,4,5],[0,4,6,7],[0,1,3,7],[0,1,3,6],[0,5,6,7],[4,5,6,7],[0,3,5,7],[0,3,5,6],[1,2,5,7],[1,2,5,6],[0,1,2,7],[1,5,6,7],[0,1,2,6],[0,1,2,3],[1,3,4,7],[1,3,4,6],[1,3,5,7],[1,3,5,6],[0,3,4,7],[0,3,4,6],[0,2,4,7],[1,2,4,7],[0,2,4,6],[1,2,4,6],[1,4,6,7],[0,1,6,7],[2,4,5,7],[2,4,5,6],[1,2,3,5],[1,2,3,4],[0,2,5,7],[0,2,5,6]]:[x[1],x[2],x[3]-1,x[4]-1,x[5]-1,x[6]-1,x[7],x[8],x[9]-1,x[11],x[12],x[13],x[14],x[15]-1]:2:[x[1],x[2],x[3]-1,x[4]-1,x[5]-1,x[6]-1,x[7],x[8],x[9]-1,x[11],x[12],x[13],x[14],x[15]-1]:2:true:[[1,0,0,0,0,0,1,1],[0,1,0,0,1,1,0,0],[0,0,1,0,1,x[10],0,0],[0,0,0,1,0,0,1,x[16]]]