[System]
ss

[Parameter]
p1 (enum): v1, v2, v3
p2 (enum): v1, v2, v3, v4
p3 (enum): v1, v2, v3
p4 (enum): v1, v2, v3
p5 (enum): v1, v2, v3

[Constraint]
C1: (p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p1 != "v1")
C2: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
C3: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1")
C4: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v1" || p2 != "v2")
C5: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3")
C6: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2")
C7: (p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p1 != "v1")
C8: (p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3" || p1 != "v1")
C9: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1")
C10: (p5 != "v1" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
C11: (p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p1 != "v1")
C12: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3")
C13: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
C14: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3")
C15: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1")
C16: (p1 != "v3" || p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
C17: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3")
C18: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v3" || p2 != "v2")
C19: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
C20: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4")
C21: (p4 != "v1" || p3 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
C22: (p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p1 != "v1")
C23: (p1 != "v3" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3")
C24: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3")
C25: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3")
C26: (p5 != "v1" || p4 != "v1" || p3 != "v1" || p1 != "v1" || p2 != "v2")
C27: (p1 != "v3" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3")
C28: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3")
C29: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1")
C30: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p1 != "v1")
C31: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3")
C32: (p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3" || p1 != "v1")
C33: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3")
C34: (p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1" || p5 != "v3")
C35: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1")
C36: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1")
C37: (p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p5 != "v3")
C38: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3")
C39: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4")
C40: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v1" || p2 != "v2")
C41: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3")
C42: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3")
C43: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1" || p1 != "v1")
C44: (p1 != "v3" || p5 != "v1" || p4 != "v3" || p3 != "v1" || p2 != "v2")
C45: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1")
C46: (p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p5 != "v3")
C47: (p4 != "v3" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
C48: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1")
C49: (p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3" || p1 != "v1")
C50: (p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p1 != "v1")
C51: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1")
C52: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3")
C53: (p1 != "v3" || p3 != "v3" || p4 != "v3" || p5 != "v3" || p2 != "v2")
C54: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
C55: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p5 != "v3")
C56: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p1 != "v1")
C57: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2")
C58: (p1 != "v3" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3")
C59: (p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
C60: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p1 != "v1")
C61: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3" || p1 != "v1")
C62: (p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1")
C63: (p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1" || p1 != "v1")
C64: (p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p1 != "v1")
C65: (p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3" || p1 != "v1")
C66: (p1 != "v3" || p4 != "v1" || p3 != "v3" || p5 != "v3" || p2 != "v2")
C67: (p1 != "v3" || p4 != "v1" || p3 != "v1" || p5 != "v3" || p2 != "v2")
C68: (p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
C69: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3" || p5 != "v3")
C70: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1")
C71: (p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p1 != "v1")
C72: (p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3" || p1 != "v1")
C73: (p4 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
C74: (p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1" || p1 != "v1")
C75: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p1 != "v1")
C76: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3")
C77: (p1 != "v3" || p4 != "v3" || p3 != "v1" || p5 != "v3" || p2 != "v2")
C78: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1")
C79: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3" || p1 != "v1")
C80: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3")
C81: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
C82: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
C83: (p1 != "v3" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
C84: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
C85: (p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
C86: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3")
C87: (p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
C88: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p1 != "v1")
C89: (p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3" || p1 != "v1")
C90: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3")
C91: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1")
C92: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
C93: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1")
C94: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v3" || p2 != "v2")
C95: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1" || p5 != "v3")
C96: (p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3" || p1 != "v1")
C97: (p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
C98: (p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3" || p1 != "v1")
C99: (p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p5 != "v3")
C100: (p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p5 != "v3")
C101: (p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p1 != "v1")
C102: (p1 != "v3" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
C103: (p3 != "v3" || p4 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
C104: (p5 != "v1" || p3 != "v3" || p4 != "v3" || p1 != "v1" || p2 != "v2")
C105: (p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3" || p1 != "v1")
C106: (p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p1 != "v1")
C107: (p1 != "v3" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3")
C108: (p5 != "v1" || p4 != "v3" || p3 != "v1" || p1 != "v1" || p2 != "v2")
C109: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p1 != "v1")
C110: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4" || p1 != "v1")
C111: (p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
C112: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1" || p1 != "v1")