def METHOD_NAME(n, f, asproof=True):
    print("(set-logic QF_UFLIA)", file=f)
    print("(declare-sort Proof 0)", file=f)
    if not asproof:
        print("(declare-fun assume (Bool) Proof)", file=f)
        print("(declare-fun res (Bool Proof Proof) Proof)", file=f)
        print("(declare-fun check (Proof) Bool)", file=f)
        print("(declare-fun or+ (Int Bool Bool) Proof)", file=f)
        print("(declare-fun or- (Bool Bool) Proof)", file=f)
        print("(declare-fun and+ (Bool Bool) Proof)", file=f)
        print("(declare-fun and- (Int Bool Bool) Proof)", file=f)
    for i in range(0, n+1):
        for k in range(1, n+1):
            print(f"(declare-fun p_{n}_{i}_{k} () Bool)", file=f)
    if asproof:
        declare_input_clauses(n, file=f)
        print("(check-proof")
        pigeon_hole(n, f, assertcmd="assume")
        print(")", file=f)
    else:
        print("(assert (check", file=f)
        pigeon_hole(n, f, assertcmd="assume")
        print("))", file=f)