Lean 4 formal verification and explicit counterexample to the support lifting conjecture on H_P^n (n = 7)

Starred Gists，GitHub Gist，即时分享代码、笔记与代码片段。关注
import Mathlib.Data.Fintype.Basic
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
namespace ConjectureCounterexample
def Gmask : Nat := 3733342667197135953300778395388072828175404778592912048662363837771429210514
def edgeOrder : List Nat := [160,206,199,135,15,102,200,105,167,56,248,47,62,214,209,250,6,163,152,155,66,98,205,210,168,185,171,122,74,63,159,68,133,136,12,85,89,188,242,178,181,213,101,104,195,10,198,9,41,95,197,131,39,158,249,231,24,139,25,91,177,2,211,143,112,45,50,93,52,42,140,77,115,162,240,247,82,38,245,170,179,18,241,172,230,130,183,201,125,212,3,123,35,165,190,61,175,80,176,244,28,17,71,192,110,107,111,21,22,108,221,149,81,57,156,30,88,219,243,202,16,5,150,83,216,19,127,70,0,46,20,164,48,76,204,97]
def witnessPerms : List (List Nat) := [
[4,6,0,1,3,2,5],
[4,6,1,0,3,2,5],
[5,2,0,1,3,4,6],
[5,2,1,0,3,4,6],
[5,6,0,1,3,2,4],
[5,6,0,1,3,4,2],
[5,6,1,0,3,2,4],
[5,6,1,0,3,4,2]
]
def targetPerms : List (List Nat) := [
[1,3,2,4,5,6,0],
[5,3,2,4,1,0,6]
]
def lowerPerms : List (List Nat) := [
[0,2,6,4,3,1,5],
[1,2,0,4,3,6,5],
[1,3,6,0,4,2,5],
[3,6,1,0,4,2,5],
[4,2,1,0,3,6,5],
[4,2,6,0,3,1,5],
[5,2,6,0,4,1,3],
[5,3,6,0,4,1,2],
[0,2,6,4,5,1,3],
[3,6,0,4,5,1,2],
[1,2,3,4,5,6,0],
[5,2,3,4,1,0,6]
]
def allPerms : List (List Nat) := [
[0,1,2,3,4,5,6],
[0,1,2,3,4,6,5],
[0,1,2,3,5,4,6],
[0,1,2,3,5,6,4],
[0,1,2,3,6,4,5],
[0,1,2,3,6,5,4],
[0,1,2,4,3,5,6],
[0,1,2,4,3,6,5],
[0,1,2,4,5,3,6],
[0,1,2,4,5,6,3],
[0,1,2,4,6,3,5],
[0,1,2,4,6,5,3],
[0,1,2,5,3,4,6],
[0,1,2,5,3,6,4],
[0,1,2,5,4,3,6],
[0,1,2,5,4,6,3],
[0,1,2,5,6,3,4],
[0,1,2,5,6,4,3],
[0,1,2,6,3,4,5],
[0,1,2,6,3,5,4],
[0,1,2,6,4,3,5],
[0,1,2,6,4,5,3],
[0,1,2,6,5,3,4],
[0,1,2,6,5,4,3],
[0,1,3,2,4,5,6],
[0,1,3,2,4,6,5],
[0,1,3,2,5,4,6],
[0,1,3,2,5,6,4],
[0,1,3,2,6,4,5],
[0,1,3,2,6,5,4],
[0,1,3,4,2,5,6],
[0,1,3,4,2,6,5],
[0,1,3,4,5,2,6],
[0,1,3,4,5,6,2],
[0,1,3,4,6,2,5],
[0,1,3,4,6,5,2],
[0,1,3,5,2,4,6],
[0,1,3,5,2,6,4],
[0,1,3,5,4,2,6],
[0,1,3,5,4,6,2],
[0,1,3,5,6,2,4],
[0,1,3,5,6,4,2],
[0,1,3,6,2,4,5],
[0,1,3,6,2,5,4],
[0,1,3,6,4,2,5],
[0,1,3,6,4,5,2],
[0,1,3,6,5,2,4],
[0,1,3,6,5,4,2],
[0,1,4,2,3,5,6],
[0,1,4,2,3,6,5],
[0,1,4,2,5,3,6],
[0,1,4,2,5,6,3],
[0,1,4,2,6,3,5],
[0,1,4,2,6,5,3],
[0,1,4,3,2,5,6],
[0,1,4,3,2,6,5],
[0,1,4,3,5,2,6],
[0,1,4,3,5,6,2],
[0,1,4,3,6,2,5],
[0,1,4,3,6,5,2],
[0,1,4,5,2,3,6],
[0,1,4,5,2,6,3],
[0,1,4,5,3,2,6],
[0,1,4,5,3,6,2],
[0,1,4,5,6,2,3],
[0,1,4,5,6,3,2],
[0,1,4,6,2,3,5],
[0,1,4,6,2,5,3],
[0,1,4,6,3,2,5],
[0,1,4,6,3,5,2],
[0,1,4,6,5,2,3],
[0,1,4,6,5,3,2],
[0,1,5,2,3,4,6],
[0,1,5,2,3,6,4],
[0,1,5,2,4,3,6],
[0,1,5,2,4,6,3],
[0,1,5,2,6,3,4],
[0,1,5,2,6,4,3],
[0,1,5,3,2,4,6],
[0,1,5,3,2,6,4],
[0,1,5,3,4,2,6],
[0,1,5,3,4,6,2],
[0,1,5,3,6,2,4],
[0,1,5,3,6,4,2],
[0,1,5,4,2,3,6],
[0,1,5,4,2,6,3],
[0,1,5,4,3,2,6],
[0,1,5,4,3,6,2],
[0,1,5,4,6,2,3],
[0,1,5,4,6,3,2],
[0,1,5,6,2,3,4],
[0,1,5,6,2,4,3],
[0,1,5,6,3,2,4],
[0,1,5,6,3,4,2],
[0,1,5,6,4,2,3],
[0,1,5,6,4,3,2],
[0,1,6,2,3,4,5],
[0,1,6,2,3,5,4],
[0,1,6,2,4,3,5],
[0,1,6,2,4,5,3],
[0,1,6,2,5,3,4],
[0,1,6,2,5,4,3],
[0,1,6,3,2,4,5],
[0,1,6,3,2,5,4],
[0,1,6,3,4,2,5],
[0,1,6,3,4,5,2],
[0,1,6,3,5,2,4],
[0,1,6,3,5,4,2],
[0,1,6,4,2,3,5],
[0,1,6,4,2,5,3],
[0,1,6,4,3,2,5],
[0,1,6,4,3,5,2],
[0,1,6,4,5,2,3],
[0,1,6,4,5,3,2],
[0,1,6,5,2,3,4],
[0,1,6,5,2,4,3],
[0,1,6,5,3,2,4],
[0,1,6,5,3,4,2],
[0,1,6,5,4,2,3],
[0,1,6,5,4,3,2],
[0,2,1,3,4,5,6],
[0,2,1,3,4,6,5],
[0,2,1,3,5,4,6],
[0,2,1,3,5,6,4],
[0,2,1,3,6,4,5],
[0,2,1,3,6,5,4],
[0,2,1,4,3,5,6],
[0,2,1,4,3,6,5],
[0,2,1,4,5,3,6],
[0,2,1,4,5,6,3],
[0,2,1,4,6,3,5],
[0,2,1,4,6,5,3],
[0,2,1,5,3,4,6],
[0,2,1,5,3,6,4],
[0,2,1,5,4,3,6],
[0,2,1,5,4,6,3],
[0,2,1,5,6,3,4],
[0,2,1,5,6,4,3],
[0,2,1,6,3,4,5],
[0,2,1,6,3,5,4],
[0,2,1,6,4,3,5],
[0,2,1,6,4,5,3],
[0,2,1,6,5,3,4],
[0,2,1,6,5,4,3],
[0,2,3,1,4,5,6],
[0,2,3,1,4,6,5],
[0,2,3,1,5,4,6],
[0,2,3,1,5,6,4],
[0,2,3,1,6,4,5],
[0,2,3,1,6,5,4],
[0,2,3,4,1,5,6],
[0,2,3,4,1,6,5],
[0,2,3,4,5,1,6],
[0,2,3,4,5,6,1],
[0,2,3,4,6,1,5],
[0,2,3,4,6,5,1],
[0,2,3,5,1,4,6],
[0,2,3,5,1,6,4],
[0,2,3,5,4,1,6],
[0,2,3,5,4,6,1],
[0,2,3,5,6,1,4],
[0,2,3,5,6,4,1],
[0,2,3,6,1,4,5],
[0,2,3,6,1,5,4],
[0,2,3,6,4,1,5],
[0,2,3,6,4,5,1],
[0,2,3,6,5,1,4],
[0,2,3,6,5,4,1],
[0,2,4,1,3,5,6],
[0,2,4,1,3,6,5],
[0,2,4,1,5,3,6],
[0,2,4,1,5,6,3],
[0,2,4,1,6,3,5],
[0,2,4,1,6,5,3],
[0,2,4,3,1,5,6],
[0,2,4,3,1,6,5],
[0,2,4,3,5,1,6],
[0,2,4,3,5,6,1],
[0,2,4,3,6,1,5],
[0,2,4,3,6,5,1],
[0,2,4,5,1,3,6],
[0,2,4,5,1,6,3],
[0,2,4,5,3,1,6],
[0,2,4,5,3,6,1],
[0,2,4,5,6,1,3],
[0,2,4,5,6,3,1],
[0,2,4,6,1,3,5],
[0,2,4,6,1,5,3],
[0,2,4,6,3,1,5],
[0,2,4,6,3,5,1],
[0,2,4,6,5,1,3],
[0,2,4,6,5,3,1],
[0,2,5,1,3,4,6],
[0,2,5,1,3,6,4],
[0,2,5,1,4,3,6],
[0,2,5,1,4,6,3],
[0,2,5,1,6,3,4],
[0,2,5,1,6,4,3],
[0,2,5,3,1,4,6],
[0,2,5,3,1,6,4],
[0,2,5,3,4,1,6],
[0,2,5,3,4,6,1],
[0,2,5,3,6,1,4],
[0,2,5,3,6,4,1],
[0,2,5,4,1,3,6],
[0,2,5,4,1,6,3],
[0,2,5,4,3,1,6],
[0,2,5,4,3,6,1],
[0,2,5,4,6,1,3],
[0,2,5,4,6,3,1],
[0,2,5,6,1,3,4],
[0,2,5,6,1,4,3],
[0,2,5,6,3,1,4],
[0,2,5,6,3,4,1],
[0,2,5,6,4,1,3],
[0,2,5,6,4,3,1],
[0,2,6,1,3,4,5],
[0,2,6,1,3,5,4],
[0,2,6,1,4,3,5],
[0,2,6,1,4,5,3],
[0,2,6,1,5,3,4],
[0,2,6,1,5,4,3],
[0,2,6,3,1,4,5],
[0,2,6,3,1,5,4],
[0,2,6,3,4,1,5],
[0,2,6,3,4,5,1],
[0,2,6,3,5,1,4],
[0,2,6,3,5,4,1],
[0,2,6,4,1,3,5],
[0,2,6,4,1,5,3],
[0,2,6,4,3,1,5],
[0,2,6,4,3,5,1],
[0,2,6,4,5,1,3],
[0,2,6,4,5,3,1],
[0,2,6,5,1,3,4],
[0,2,6,5,1,4,3],
[0,2,6,5,3,1,4],
[0,2,6,5,3,4,1],
[0,2,6,5,4,1,3],
[0,2,6,5,4,3,1],
[0,3,1,2,4,5,6],
[0,3,1,2,4,6,5],
[0,3,1,2,5,4,6],
[0,3,1,2,5,6,4],
[0,3,1,2,6,4,5],
[0,3,1,2,6,5,4],
[0,3,1,4,2,5,6],
[0,3,1,4,2,6,5],
[0,3,1,4,5,2,6],
[0,3,1,4,5,6,2],
[0,3,1,4,6,2,5],
[0,3,1,4,6,5,2],
[0,3,1,5,2,4,6],
[0,3,1,5,2,6,4],
[0,3,1,5,4,2,6],
[0,3,1,5,4,6,2],
[0,3,1,5,6,2,4],
[0,3,1,5,6,4,2],
[0,3,1,6,2,4,5],
[0,3,1,6,2,5,4],
[0,3,1,6,4,2,5],
[0,3,1,6,4,5,2],
[0,3,1,6,5,2,4],
[0,3,1,6,5,4,2],
[0,3,2,1,4,5,6],
[0,3,2,1,4,6,5],
[0,3,2,1,5,4,6],
[0,3,2,1,5,6,4],
[0,3,2,1,6,4,5],
[0,3,2,1,6,5,4],
[0,3,2,4,1,5,6],
[0,3,2,4,1,6,5],
[0,3,2,4,5,1,6],
[0,3,2,4,5,6,1],
[0,3,2,4,6,1,5],
[0,3,2,4,6,5,1],
[0,3,2,5,1,4,6],
[0,3,2,5,1,6,4],
[0,3,2,5,4,1,6],
[0,3,2,5,4,6,1],
[0,3,2,5,6,1,4],
[0,3,2,5,6,4,1],
[0,3,2,6,1,4,5],
[0,3,2,6,1,5,4],
[0,3,2,6,4,1,5],
[0,3,2,6,4,5,1],
[0,3,2,6,5,1,4],
[0,3,2,6,5,4,1],
[0,3,4,1,2,5,6],
[0,3,4,1,2,6,5],
[0,3,4,1,5,2,6],
[0,3,4,1,5,6,2],
[0,3,4,1,6,2,5],
[0,3,4,1,6,5,2],
[0,3,4,2,1,5,6],
[0,3,4,2,1,6,5],
[0,3,4,2,5,1,6],
[0,3,4,2,5,6,1],
[0,3,4,2,6,1,5],
[0,3,4,2,6,5,1],
[0,3,4,5,1,2,6],
[0,3,4,5,1,6,2],
[0,3,4,5,2,1,6],
[0,3,4,5,2,6,1],
[0,3,4,5,6,1,2],
[0,3,4,5,6,2,1],
[0,3,4,6,1,2,5],
[0,3,4,6,1,5,2],
[0,3,4,6,2,1,5],
[0,3,4,6,2,5,1],
[0,3,4,6,5,1,2],
[0,3,4,6,5,2,1],
[0,3,5,1,2,4,6],
[0,3,5,1,2,6,4],
[0,3,5,1,4,2,6],
[0,3,5,1,4,6,2],
[0,3,5,1,6,2,4],
[0,3,5,1,6,4,2],
[0,3,5,2,1,4,6],
[0,3,5,2,1,6,4],
[0,3,5,2,4,1,6],
[0,3,5,2,4,6,1],
[0,3,5,2,6,1,4],
[0,3,5,2,6,4,1],
[0,3,5,4,1,2,6],
[0,3,5,4,1,6,2],
[0,3,5,4,2,1,6],
[0,3,5,4,2,6,1],
[0,3,5,4,6,1,2],
[0,3,5,4,6,2,1],
[0,3,5,6,1,2,4],
[0,3,5,6,1,4,2],
[0,3,5,6,2,1,4],
[0,3,5,6,2,4,1],
[0,3,5,6,4,1,2],
[0,3,5,6,4,2,1],
[0,3,6,1,2,4,5],
[0,3,6,1,2,5,4],
[0,3,6,1,4,2,5],
[0,3,6,1,4,5,2],
[0,3,6,1,5,2,4],
[0,3,6,1,5,4,2],
[0,3,6,2,1,4,5],
[0,3,6,2,1,5,4],
[0,3,6,2,4,1,5],
[0,3,6,2,4,5,1],
[0,3,6,2,5,1,4],
[0,3,6,2,5,4,1],
[0,3,6,4,1,2,5],
[0,3,6,4,1,5,2],
[0,3,6,4,2,1,5],
[0,3,6,4,2,5,1],
[0,3,6,4,5,1,2],
[0,3,6,4,5,2,1],
[0,3,6,5,1,2,4],
[0,3,6,5,1,4,2],
[0,3,6,5,2,1,4],
[0,3,6,5,2,4,1],
[0,3,6,5,4,1,2],
[0,3,6,5,4,2,1],
[0,4,1,2,3,5,6],
[0,4,1,2,3,6,5],
[0,4,1,2,5,3,6],
[0,4,1,2,5,6,3],
[0,4,1,2,6,3,5],
[0,4,1,2,6,5,3],
[0,4,1,3,2,5,6],
[0,4,1,3,2,6,5],
[0,4,1,3,5,2,6],
[0,4,1,3,5,6,2],
[0,4,1,3,6,2,5],
[0,4,1,3,6,5,2],
[0,4,1,5,2,3,6],
[0,4,1,5,2,6,3],
[0,4,1,5,3,2,6],
[0,4,1,5,3,6,2],
[0,4,1,5,6,2,3],
[0,4,1,5,6,3,2],
[0,4,1,6,2,3,5],
[0,4,1,6,2,5,3],
[0,4,1,6,3,2,5],
[0,4,1,6,3,5,2],
[0,4,1,6,5,2,3],
[0,4,1,6,5,3,2],
[0,4,2,1,3,5,6],
[0,4,2,1,3,6,5],
[0,4,2,1,5,3,6],
[0,4,2,1,5,6,3],
[0,4,2,1,6,3,5],
[0,4,2,1,6,5,3],
[0,4,2,3,1,5,6],
[0,4,2,3,1,6,5],
[0,4,2,3,5,1,6],
[0,4,2,3,5,6,1],
[0,4,2,3,6,1,5],
[0,4,2,3,6,5,1],
[0,4,2,5,1,3,6],
[0,4,2,5,1,6,3],
[0,4,2,5,3,1,6],
[0,4,2,5,3,6,1],
[0,4,2,5,6,1,3],
[0,4,2,5,6,3,1],
[0,4,2,6,1,3,5],
[0,4,2,6,1,5,3],
[0,4,2,6,3,1,5],
[0,4,2,6,3,5,1],
[0,4,2,6,5,1,3],
[0,4,2,6,5,3,1],
[0,4,3,1,2,5,6],
[0,4,3,1,2,6,5],
[0,4,3,1,5,2,6],
[0,4,3,1,5,6,2],
[0,4,3,1,6,2,5],
[0,4,3,1,6,5,2],
[0,4,3,2,1,5,6],
[0,4,3,2,1,6,5],
[0,4,3,2,5,1,6],
[0,4,3,2,5,6,1],
[0,4,3,2,6,1,5],
[0,4,3,2,6,5,1],
[0,4,3,5,1,2,6],
[0,4,3,5,1,6,2],
[0,4,3,5,2,1,6],
[0,4,3,5,2,6,1],
[0,4,3,5,6,1,2],
[0,4,3,5,6,2,1],
[0,4,3,6,1,2,5],
[0,4,3,6,1,5,2],
[0,4,3,6,2,1,5],
[0,4,3,6,2,5,1],
[0,4,3,6,5,1,2],
[0,4,3,6,5,2,1],
[0,4,5,1,2,3,6],
[0,4,5,1,2,6,3],
[0,4,5,1,3,2,6],
[0,4,5,1,3,6,2],
[0,4,5,1,6,2,3],
[0,4,5,1,6,3,2],
[0,4,5,2,1,3,6],
[0,4,5,2,1,6,3],
[0,4,5,2,3,1,6],
[0,4,5,2,3,6,1],
[0,4,5,2,6,1,3],
[0,4,5,2,6,3,1],
[0,4,5,3,1,2,6],
[0,4,5,3,1,6,2],
[0,4,5,3,2,1,6],
[0,4,5,3,2,6,1],
[0,4,5,3,6,1,2],
[0,4,5,3,6,2,1],
[0,4,5,6,1,2,3],
[0,4,5,6,1,3,2],
[0,4,5,6,2,1,3],
[0,4,5,6,2,3,1],
[0,4,5,6,3,1,2],
[0,4,5,6,3,2,1],
[0,4,6,1,2,3,5],
[0,4,6,1,2,5,3],
[0,4,6,1,3,2,5],
[0,4,6,1,3,5,2],
[0,4,6,1,5,2,3],
[0,4,6,1,5,3,2],
[0,4,6,2,1,3,5],
[0,4,6,2,1,5,3],
[0,4,6,2,3,1,5],
[0,4,6,2,3,5,1],
[0,4,6,2,5,1,3],
[0,4,6,2,5,3,1],
[0,4,6,3,1,2,5],
[0,4,6,3,1,5,2],
[0,4,6,3,2,1,5],
[0,4,6,3,2,5,1],
[0,4,6,3,5,1,2],
[0,4,6,3,5,2,1],
[0,4,6,5,1,2,3],
[0,4,6,5,1,3,2],
[0,4,6,5,2,1,3],
[0,4,6,5,2,3,1],
[0,4,6,5,3,1,2],
[0,4,6,5,3,2,1],
[0,5,1,2,3,4,6],
[0,5,1,2,3,6,4],
[0,5,1,2,4,3,6],
[0,5,1,2,4,6,3],
[0,5,1,2,6,3,4],
[0,5,1,2,6,4,3],
[0,5,1,3,2,4,6],
[0,5,1,3,2,6,4],
[0,5,1,3,4,2,6],
[0,5,1,3,4,6,2],
[0,5,1,3,6,2,4],
[0,5,1,3,6,4,2],
[0,5,1,4,2,3,6],
[0,5,1,4,2,6,3],
[0,5,1,4,3,2,6],
[0,5,1,4,3,6,2],
[0,5,1,4,6,2,3],
[0,5,1,4,6,3,2],
[0,5,1,6,2,3,4],
[0,5,1,6,2,4,3],
[0,5,1,6,3,2,4],
[0,5,1,6,3,4,2],
[0,5,1,6,4,2,3],
[0,5,1,6,4,3,2],
[0,5,2,1,3,4,6],
[0,5,2,1,3,6,4],
[0,5,2,1,4,3,6],
[0,5,2,1,4,6,3],
[0,5,2,1,6,3,4],
[0,5,2,1,6,4,3],
[0,5,2,3,1,4,6],
[0,5,2,3,1,6,4],
[0,5,2,3,4,1,6],
[0,5,2,3,4,6,1],
[0,5,2,3,6,1,4],
[0,5,2,3,6,4,1],
[0,5,2,4,1,3,6],
[0,5,2,4,1,6,3],
[0,5,2,4,3,1,6],
[0,5,2,4,3,6,1],
[0,5,2,4,6,1,3],
[0,5,2,4,6,3,1],
[0,5,2,6,1,3,4],
[0,5,2,6,1,4,3],
[0,5,2,6,3,1,4],
[0,5,2,6,3,4,1],
[0,5,2,6,4,1,3],
[0,5,2,6,4,3,1],
[0,5,3,1,2,4,6],
[0,5,3,1,2,6,4],
[0,5,3,1,4,2,6],
[0,5,3,1,4,6,2],
[0,5,3,1,6,2,4],
[0,5,3,1,6,4,2],
[0,5,3,2,1,4,6],
[0,5,3,2,1,6,4],
[0,5,3,2,4,1,6],
[0,5,3,2,4,6,1],
[0,5,3,2,6,1,4],
[0,5,3,2,6,4,1],
[0,5,3,4,1,2,6],
[0,5,3,4,1,6,2],
[0,5,3,4,2,1,6],
[0,5,3,4,2,6,1],
[0,5,3,4,6,1,2],
[0,5,3,4,6,2,1],
[0,5,3,6,1,2,4],
[0,5,3,6,1,4,2],
[0,5,3,6,2,1,4],
[0,5,3,6,2,4,1],
[0,5,3,6,4,1,2],
[0,5,3,6,4,2,1],
[0,5,4,1,2,3,6],
[0,5,4,1,2,6,3],
[0,5,4,1,3,2,6],
[0,5,4,1,3,6,2],
[0,5,4,1,6,2,3],
[0,5,4,1,6,3,2],
[0,5,4,2,1,3,6],
[0,5,4,2,1,6,3],
[0,5,4,2,3,1,6],
[0,5,4,2,3,6,1],
[0,5,4,2,6,1,3],
[0,5,4,2,6,3,1],
[0,5,4,3,1,2,6],
[0,5,4,3,1,6,2],
[0,5,4,3,2,1,6],
[0,5,4,3,2,6,1],
[0,5,4,3,6,1,2],
[0,5,4,3,6,2,1],
[0,5,4,6,1,2,3],
[0,5,4,6,1,3,2],
[0,5,4,6,2,1,3],
[0,5,4,6,2,3,1],
[0,5,4,6,3,1,2],
[0,5,4,6,3,2,1],
[0,5,6,1,2,3,4],
[0,5,6,1,2,4,3],
[0,5,6,1,3,2,4],
[0,5,6,1,3,4,2],
[0,5,6,1,4,2,3],
[0,5,6,1,4,3,2],
[0,5,6,2,1,3,4],
[0,5,6,2,1,4,3],
[0,5,6,2,3,1,4],
[0,5,6,2,3,4,1],
[0,5,6,2,4,1,3],
[0,5,6,2,4,3,1],
[0,5,6,3,1,2,4],
[0,5,6,3,1,4,2],
[0,5,6,3,2,1,4],
[0,5,6,3,2,4,1],
[0,5,6,3,4,1,2],
[0,5,6,3,4,2,1],
[0,5,6,4,1,2,3],
[0,5,6,4,1,3,2],
[0,5,6,4,2,1,3],
[0,5,6,4,2,3,1],
[0,5,6,4,3,1,2],
[0,5,6,4,3,2,1],
[0,6,1,2,3,4,5],
[0,6,1,2,3,5,4],
[0,6,1,2,4,3,5],
[0,6,1,2,4,5,3],
[0,6,1,2,5,3,4],
[0,6,1,2,5,4,3],
[0,6,1,3,2,4,5],
[0,6,1,3,2,5,4],
[0,6,1,3,4,2,5],
[0,6,1,3,4,5,2],
[0,6,1,3,5,2,4],
[0,6,1,3,5,4,2],
[0,6,1,4,2,3,5],
[0,6,1,4,2,5,3],
[0,6,1,4,3,2,5],
[0,6,1,4,3,5,2],
[0,6,1,4,5,2,3],
[0,6,1,4,5,3,2],
[0,6,1,5,2,3,4],
[0,6,1,5,2,4,3],
[0,6,1,5,3,2,4],
[0,6,1,5,3,4,2],
[0,6,1,5,4,2,3],
[0,6,1,5,4,3,2],
[0,6,2,1,3,4,5],
[0,6,2,1,3,5,4],
[0,6,2,1,4,3,5],
[0,6,2,1,4,5,3],
[0,6,2,1,5,3,4],
[0,6,2,1,5,4,3],
[0,6,2,3,1,4,5],
[0,6,2,3,1,5,4],
[0,6,2,3,4,1,5],
[0,6,2,3,4,5,1],
[0,6,2,3,5,1,4],
[0,6,2,3,5,4,1],
[0,6,2,4,1,3,5],
[0,6,2,4,1,5,3],
[0,6,2,4,3,1,5],
[0,6,2,4,3,5,1],
[0,6,2,4,5,1,3],
[0,6,2,4,5,3,1],
[0,6,2,5,1,3,4],
[0,6,2,5,1,4,3],
[0,6,2,5,3,1,4],
[0,6,2,5,3,4,1],
[0,6,2,5,4,1,3],
[0,6,2,5,4,3,1],
[0,6,3,1,2,4,5],
[0,6,3,1,2,5,4],
[0,6,3,1,4,2,5],
[0,6,3,1,4,5,2],
[0,6,3,1,5,2,4],
[0,6,3,1,5,4,2],
[0,6,3,2,1,4,5],
[0,6,3,2,1,5,4],
[0,6,3,2,4,1,5],
[0,6,3,2,4,5,1],
[0,6,3,2,5,1,4],
[0,6,3,2,5,4,1],
[0,6,3,4,1,2,5],
[0,6,3,4,1,5,2],
[0,6,3,4,2,1,5],
[0,6,3,4,2,5,1],
[0,6,3,4,5,1,2],
[0,6,3,4,5,2,1],
[0,6,3,5,1,2,4],
[0,6,3,5,1,4,2],
[0,6,3,5,2,1,4],
[0,6,3,5,2,4,1],
[0,6,3,5,4,1,2],
[0,6,3,5,4,2,1],
[0,6,4,1,2,3,5],
[0,6,4,1,2,5,3],
[0,6,4,1,3,2,5],
[0,6,4,1,3,5,2],
[0,6,4,1,5,2,3],
[0,6,4,1,5,3,2],
[0,6,4,2,1,3,5],
[0,6,4,2,1,5,3],
[0,6,4,2,3,1,5],
[0,6,4,2,3,5,1],
[0,6,4,2,5,1,3],
[0,6,4,2,5,3,1],
[0,6,4,3,1,2,5],
[0,6,4,3,1,5,2],
[0,6,4,3,2,1,5],
[0,6,4,3,2,5,1],
[0,6,4,3,5,1,2],
[0,6,4,3,5,2,1],
[0,6,4,5,1,2,3],
[0,6,4,5,1,3,2],
[0,6,4,5,2,1,3],
[0,6,4,5,2,3,1],
[0,6,4,5,3,1,2],
[0,6,4,5,3,2,1],
[0,6,5,1,2,3,4],
[0,6,5,1,2,4,3],
[0,6,5,1,3,2,4],
[0,6,5,1,3,4,2],
[0,6,5,1,4,2,3],
[0,6,5,1,4,3,2],
[0,6,5,2,1,3,4],
[0,6,5,2,1,4,3],
[0,6,5,2,3,1,4],
[0,6,5,2,3,4,1],
[0,6,5,2,4,1,3],
[0,6,5,2,4,3,1],
[0,6,5,3,1,2,4],
[0,6,5,3,1,4,2],
[0,6,5,3,2,1,4],
[0,6,5,3,2,4,1],
[0,6,5,3,4,1,2],
[0,6,5,3,4,2,1],
[0,6,5,4,1,2,3],
[0,6,5,4,1,3,2],
[0,6,5,4,2,1,3],
[0,6,5,4,2,3,1],
[0,6,5,4,3,1,2],
[0,6,5,4,3,2,1],
[1,0,2,3,4,5,6],
[1,0,2,3,4,6,5],
[1,0,2,3,5,4,6],
[1,0,2,3,5,6,4],
[1,0,2,3,6,4,5],
[1,0,2,3,6,5,4],
[1,0,2,4,3,5,6],
[1,0,2,4,3,6,5],
[1,0,2,4,5,3,6],
[1,0,2,4,5,6,3],
[1,0,2,4,6,3,5],
[1,0,2,4,6,5,3],
[1,0,2,5,3,4,6],
[1,0,2,5,3,6,4],
[1,0,2,5,4,3,6],
[1,0,2,5,4,6,3],
[1,0,2,5,6,3,4],
[1,0,2,5,6,4,3],
[1,0,2,6,3,4,5],
[1,0,2,6,3,5,4],
[1,0,2,6,4,3,5],
[1,0,2,6,4,5,3],
[1,0,2,6,5,3,4],
[1,0,2,6,5,4,3],
[1,0,3,2,4,5,6],
[1,0,3,2,4,6,5],
[1,0,3,2,5,4,6],
[1,0,3,2,5,6,4],
[1,0,3,2,6,4,5],
[1,0,3,2,6,5,4],
[1,0,3,4,2,5,6],
[1,0,3,4,2,6,5],
[1,0,3,4,5,2,6],
[1,0,3,4,5,6,2],
[1,0,3,4,6,2,5],
[1,0,3,4,6,5,2],
[1,0,3,5,2,4,6],
[1,0,3,5,2,6,4],
[1,0,3,5,4,2,6],
[1,0,3,5,4,6,2],
[1,0,3,5,6,2,4],
[1,0,3,5,6,4,2],
[1,0,3,6,2,4,5],
[1,0,3,6,2,5,4],
[1,0,3,6,4,2,5],
[1,0,3,6,4,5,2],
[1,0,3,6,5,2,4],
[1,0,3,6,5,4,2],
[1,0,4,2,3,5,6],
[1,0,4,2,3,6,5],
[1,0,4,2,5,3,6],
[1,0,4,2,5,6,3],
[1,0,4,2,6,3,5],
[1,0,4,2,6,5,3],
[1,0,4,3,2,5,6],
[1,0,4,3,2,6,5],
[1,0,4,3,5,2,6],
[1,0,4,3,5,6,2],
[1,0,4,3,6,2,5],
[1,0,4,3,6,5,2],
[1,0,4,5,2,3,6],
[1,0,4,5,2,6,3],
[1,0,4,5,3,2,6],
[1,0,4,5,3,6,2],
[1,0,4,5,6,2,3],
[1,0,4,5,6,3,2],
[1,0,4,6,2,3,5],
[1,0,4,6,2,5,3],
[1,0,4,6,3,2,5],
[1,0,4,6,3,5,2],
[1,0,4,6,5,2,3],
[1,0,4,6,5,3,2],
[1,0,5,2,3,4,6],
[1,0,5,2,3,6,4],
[1,0,5,2,4,3,6],
[1,0,5,2,4,6,3],
[1,0,5,2,6,3,4],
[1,0,5,2,6,4,3],
[1,0,5,3,2,4,6],
[1,0,5,3,2,6,4],
[1,0,5,3,4,2,6],
[1,0,5,3,4,6,2],
[1,0,5,3,6,2,4],
[1,0,5,3,6,4,2],
[1,0,5,4,2,3,6],
[1,0,5,4,2,6,3],
[1,0,5,4,3,2,6],
[1,0,5,4,3,6,2],
[1,0,5,4,6,2,3],
[1,0,5,4,6,3,2],
[1,0,5,6,2,3,4],
[1,0,5,6,2,4,3],
[1,0,5,6,3,2,4],
[1,0,5,6,3,4,2],
[1,0,5,6,4,2,3],
[1,0,5,6,4,3,2],
[1,0,6,2,3,4,5],
[1,0,6,2,3,5,4],
[1,0,6,2,4,3,5],
[1,0,6,2,4,5,3],
[1,0,6,2,5,3,4],
[1,0,6,2,5,4,3],
[1,0,6,3,2,4,5],
[1,0,6,3,2,5,4],
[1,0,6,3,4,2,5],
[1,0,6,3,4,5,2],
[1,0,6,3,5,2,4],
[1,0,6,3,5,4,2],
[1,0,6,4,2,3,5],
[1,0,6,4,2,5,3],
[1,0,6,4,3,2,5],
[1,0,6,4,3,5,2],
[1,0,6,4,5,2,3],
[1,0,6,4,5,3,2],
[1,0,6,5,2,3,4],
[1,0,6,5,2,4,3],
[1,0,6,5,3,2,4],
[1,0,6,5,3,4,2],
[1,0,6,5,4,2,3],
[1,0,6,5,4,3,2],
[1,2,0,3,4,5,6],
[1,2,0,3,4,6,5],
[1,2,0,3,5,4,6],
[1,2,0,3,5,6,4],
[1,2,0,3,6,4,5],
[1,2,0,3,6,5,4],
[1,2,0,4,3,5,6],
[1,2,0,4,3,6,5],
[1,2,0,4,5,3,6],
[1,2,0,4,5,6,3],
[1,2,0,4,6,3,5],
[1,2,0,4,6,5,3],
[1,2,0,5,3,4,6],
[1,2,0,5,3,6,4],
[1,2,0,5,4,3,6],
[1,2,0,5,4,6,3],
[1,2,0,5,6,3,4],
[1,2,0,5,6,4,3],
[1,2,0,6,3,4,5],
[1,2,0,6,3,5,4],
[1,2,0,6,4,3,5],
[1,2,0,6,4,5,3],
[1,2,0,6,5,3,4],
[1,2,0,6,5,4,3],
[1,2,3,0,4,5,6],
[1,2,3,0,4,6,5],
[1,2,3,0,5,4,6],
[1,2,3,0,5,6,4],
[1,2,3,0,6,4,5],
[1,2,3,0,6,5,4],
[1,2,3,4,0,5,6],
[1,2,3,4,0,6,5],
[1,2,3,4,5,0,6],
[1,2,3,4,5,6,0],
[1,2,3,4,6,0,5],
[1,2,3,4,6,5,0],
[1,2,3,5,0,4,6],
[1,2,3,5,0,6,4],
[1,2,3,5,4,0,6],
[1,2,3,5,4,6,0],
[1,2,3,5,6,0,4],
[1,2,3,5,6,4,0],
[1,2,3,6,0,4,5],
[1,2,3,6,0,5,4],
[1,2,3,6,4,0,5],
[1,2,3,6,4,5,0],
[1,2,3,6,5,0,4],
[1,2,3,6,5,4,0],
[1,2,4,0,3,5,6],
[1,2,4,0,3,6,5],
[1,2,4,0,5,3,6],
[1,2,4,0,5,6,3],
[1,2,4,0,6,3,5],
[1,2,4,0,6,5,3],
[1,2,4,3,0,5,6],
[1,2,4,3,0,6,5],
[1,2,4,3,5,0,6],
[1,2,4,3,5,6,0],
[1,2,4,3,6,0,5],
[1,2,4,3,6,5,0],
[1,2,4,5,0,3,6],
[1,2,4,5,0,6,3],
[1,2,4,5,3,0,6],
[1,2,4,5,3,6,0],
[1,2,4,5,6,0,3],
[1,2,4,5,6,3,0],
[1,2,4,6,0,3,5],
[1,2,4,6,0,5,3],
[1,2,4,6,3,0,5],
[1,2,4,6,3,5,0],
[1,2,4,6,5,0,3],
[1,2,4,6,5,3,0],
[1,2,5,0,3,4,6],
[1,2,5,0,3,6,4],
[1,2,5,0,4,3,6],
[1,2,5,0,4,6,3],
[1,2,5,0,6,3,4],
[1,2,5,0,6,4,3],
[1,2,5,3,0,4,6],
[1,2,5,3,0,6,4],
[1,2,5,3,4,0,6],
[1,2,5,3,4,6,0],
[1,2,5,3,6,0,4],
[1,2,5,3,6,4,0],
[1,2,5,4,0,3,6],
[1,2,5,4,0,6,3],
[1,2,5,4,3,0,6],
[1,2,5,4,3,6,0],
[1,2,5,4,6,0,3],
[1,2,5,4,6,3,0],
[1,2,5,6,0,3,4],
[1,2,5,6,0,4,3],
[1,2,5,6,3,0,4],
[1,2,5,6,3,4,0],
[1,2,5,6,4,0,3],
[1,2,5,6,4,3,0],
[1,2,6,0,3,4,5],
[1,2,6,0,3,5,4],
[1,2,6,0,4,3,5],
[1,2,6,0,4,5,3],
[1,2,6,0,5,3,4],
[1,2,6,0,5,4,3],
[1,2,6,3,0,4,5],
[1,2,6,3,0,5,4],
[1,2,6,3,4,0,5],
[1,2,6,3,4,5,0],
[1,2,6,3,5,0,4],
[1,2,6,3,5,4,0],
[1,2,6,4,0,3,5],
[1,2,6,4,0,5,3],
[1,2,6,4,3,0,5],
[1,2,6,4,3,5,0],
[1,2,6,4,5,0,3],
[1,2,6,4,5,3,0],
[1,2,6,5,0,3,4],
[1,2,6,5,0,4,3],
[1,2,6,5,3,0,4],
[1,2,6,5,3,4,0],
[1,2,6,5,4,0,3],
[1,2,6,5,4,3,0],
[1,3,0,2,4,5,6],
[1,3,0,2,4,6,5],
[1,3,0,2,5,4,6],
[1,3,0,2,5,6,4],
[1,3,0,2,6,4,5],
[1,3,0,2,6,5,4],
[1,3,0,4,2,5,6],
[1,3,0,4,2,6,5],
[1,3,0,4,5,2,6],
[1,3,0,4,5,6,2],
[1,3,0,4,6,2,5],
[1,3,0,4,6,5,2],
[1,3,0,5,2,4,6],
[1,3,0,5,2,6,4],
[1,3,0,5,4,2,6],
[1,3,0,5,4,6,2],
[1,3,0,5,6,2,4],
[1,3,0,5,6,4,2],
[1,3,0,6,2,4,5],
[1,3,0,6,2,5,4],
[1,3,0,6,4,2,5],
[1,3,0,6,4,5,2],
[1,3,0,6,5,2,4],
[1,3,0,6,5,4,2],
[1,3,2,0,4,5,6],
[1,3,2,0,4,6,5],
[1,3,2,0,5,4,6],
[1,3,2,0,5,6,4],
[1,3,2,0,6,4,5],
[1,3,2,0,6,5,4],
[1,3,2,4,0,5,6],
[1,3,2,4,0,6,5],
[1,3,2,4,5,0,6],
[1,3,2,4,5,6,0],
[1,3,2,4,6,0,5],
[1,3,2,4,6,5,0],
[1,3,2,5,0,4,6],
[1,3,2,5,0,6,4],
[1,3,2,5,4,0,6],
[1,3,2,5,4,6,0],
[1,3,2,5,6,0,4],
[1,3,2,5,6,4,0],
[1,3,2,6,0,4,5],
[1,3,2,6,0,5,4],
[1,3,2,6,4,0,5],
[1,3,2,6,4,5,0],
[1,3,2,6,5,0,4],
[1,3,2,6,5,4,0],
[1,3,4,0,2,5,6],
[1,3,4,0,2,6,5],
[1,3,4,0,5,2,6],
[1,3,4,0,5,6,2],
[1,3,4,0,6,2,5],
[1,3,4,0,6,5,2],
[1,3,4,2,0,5,6],
[1,3,4,2,0,6,5],
[1,3,4,2,5,0,6],
[1,3,4,2,5,6,0],
[1,3,4,2,6,0,5],
[1,3,4,2,6,5,0],
[1,3,4,5,0,2,6],
[1,3,4,5,0,6,2],
[1,3,4,5,2,0,6],
[1,3,4,5,2,6,0],
[1,3,4,5,6,0,2],
[1,3,4,5,6,2,0],
[1,3,4,6,0,2,5],
[1,3,4,6,0,5,2],
[1,3,4,6,2,0,5],
[1,3,4,6,2,5,0],
[1,3,4,6,5,0,2],
[1,3,4,6,5,2,0],
[1,3,5,0,2,4,6],
[1,3,5,0,2,6,4],
[1,3,5,0,4,2,6],
[1,3,5,0,4,6,2],
[1,3,5,0,6,2,4],
[1,3,5,0,6,4,2],
[1,3,5,2,0,4,6],
[1,3,5,2,0,6,4],
[1,3,5,2,4,0,6],
[1,3,5,2,4,6,0],
[1,3,5,2,6,0,4],
[1,3,5,2,6,4,0],
[1,3,5,4,0,2,6],
[1,3,5,4,0,6,2],
[1,3,5,4,2,0,6],
[1,3,5,4,2,6,0],
[1,3,5,4,6,0,2],
[1,3,5,4,6,2,0],
[1,3,5,6,0,2,4],
[1,3,5,6,0,4,2],
[1,3,5,6,2,0,4],
[1,3,5,6,2,4,0],
[1,3,5,6,4,0,2],
[1,3,5,6,4,2,0],
[1,3,6,0,2,4,5],
[1,3,6,0,2,5,4],
[1,3,6,0,4,2,5],
[1,3,6,0,4,5,2],
[1,3,6,0,5,2,4],
[1,3,6,0,5,4,2],
[1,3,6,2,0,4,5],
[1,3,6,2,0,5,4],
[1,3,6,2,4,0,5],
[1,3,6,2,4,5,0],
[1,3,6,2,5,0,4],
[1,3,6,2,5,4,0],
[1,3,6,4,0,2,5],
[1,3,6,4,0,5,2],
[1,3,6,4,2,0,5],
[1,3,6,4,2,5,0],
[1,3,6,4,5,0,2],
[1,3,6,4,5,2,0],
[1,3,6,5,0,2,4],
[1,3,6,5,0,4,2],
[1,3,6,5,2,0,4],
[1,3,6,5,2,4,0],
[1,3,6,5,4,0,2],
[1,3,6,5,4,2,0],
[1,4,0,2,3,5,6],
[1,4,0,2,3,6,5],
[1,4,0,2,5,3,6],
[1,4,0,2,5,6,3],
[1,4,0,2,6,3,5],
[1,4,0,2,6,5,3],
[1,4,0,3,2,5,6],
[1,4,0,3,2,6,5],
[1,4,0,3,5,2,6],
[1,4,0,3,5,6,2],
[1,4,0,3,6,2,5],
[1,4,0,3,6,5,2],
添加评论
点赞收藏
点踩分享查看原文
评论
?
参与讨论