int_rules_4_5_4_1 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 4.5.4.1*(a+b*sec)^m*(A+B*sec+C*sec^2) =#
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (1 / (~b) ^ 2) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp((~b * ~B - ~a * ~C) + ~b * ~C * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x) && EqQ((~A * (~b) ^ 2 - ~a * ~b * ~B) + (~a) ^ 2 * ~C, 0)
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~C / (~b) ^ 2) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp(-(~a) + ~b * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C, ~m], ~x) && EqQ(~A * (~b) ^ 2 + (~a) ^ 2 * ~C, 0)
    @apply_utils Antiderivative((~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~A + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~A * cot(~e + ~f * ~x) * (~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * ~m) <-- FreeQ([~b, ~e, ~f, ~A, ~C, ~m], ~x) && EqQ(~C * ~m + ~A * (~m + 1), 0)
    @apply_utils Antiderivative(csc(~(e') + ~(f') * ~x) ^ ~(m') * (~A + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => Antiderivative((~C + ~A * sin(~e + ~f * ~x) ^ 2) / sin(~e + ~f * ~x) ^ (~m + 2), ~x) <-- FreeQ([~e, ~f, ~A, ~C], ~x) && (NeQ(~C * ~m + ~A * (~m + 1), 0) && ILtQ((~m + 1) / 2, 0))
    @apply_utils Antiderivative((~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~A + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~A * cot(~e + ~f * ~x) * (~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * ~m) + ((~C * ~m + ~A * (~m + 1)) / ((~b) ^ 2 * ~m)) * Antiderivative((~b * csc(~e + ~f * ~x)) ^ (~m + 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~C], ~x) && (NeQ(~C * ~m + ~A * (~m + 1), 0) && LeQ(~m, -1))
    @apply_utils Antiderivative((~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~A + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~C) * cot(~e + ~f * ~x) * (~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * (~m + 1)) + ((~C * ~m + ~A * (~m + 1)) / (~m + 1)) * Antiderivative((~b * csc(~e + ~f * ~x)) ^ ~m, ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~C, ~m], ~x) && (NeQ(~C * ~m + ~A * (~m + 1), 0) && Not(LeQ(~m, -1)))
    @apply_utils Antiderivative((~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~B / ~b) * Antiderivative((~b * csc(~e + ~f * ~x)) ^ (~m + 1), ~x) + Antiderivative((~b * csc(~e + ~f * ~x)) ^ ~m * (~A + ~C * csc(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x)
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~b) * ~C * csc(~e + ~f * ~x) * cot(~e + ~f * ~x)) / (2 * ~f) + (1 / 2) * Antiderivative(Simp(2 * ~A * ~a + (2 * ~B * ~a + ~b * (2 * ~A + ~C)) * csc(~e + ~f * ~x) + 2 * (~a * ~C + ~B * ~b) * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x)
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~b) * ~C * csc(~e + ~f * ~x) * cot(~e + ~f * ~x)) / (2 * ~f) + (1 / 2) * Antiderivative(Simp(2 * ~A * ~a + ~b * (2 * ~A + ~C) * csc(~e + ~f * ~x) + 2 * ~a * ~C * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x)
    @apply_utils Antiderivative((~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2) / (~a + ~(b') * csc(~(e') + ~(f') * ~x)), ~x) => (~C / ~b) * Antiderivative(csc(~e + ~f * ~x), ~x) + (1 / ~b) * Antiderivative((~A * ~b + (~b * ~B - ~a * ~C) * csc(~e + ~f * ~x)) / (~a + ~b * csc(~e + ~f * ~x)), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x)
    @apply_utils Antiderivative((~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2) / (~a + ~(b') * csc(~(e') + ~(f') * ~x)), ~x) => (~C / ~b) * Antiderivative(csc(~e + ~f * ~x), ~x) + (1 / ~b) * Antiderivative((~A * ~b - ~a * ~C * csc(~e + ~f * ~x)) / (~a + ~b * csc(~e + ~f * ~x)), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x)
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(((~a * ~A - ~b * ~B) + ~a * ~C)) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~a * ~f * (2 * ~m + 1)) + (1 / (~a * ~b * (2 * ~m + 1))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp(~A * ~b * (2 * ~m + 1) + (~b * ~B * (~m + 1) - ~a * (~A * (~m + 1) - ~C * ~m)) * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x) && (EqQ((~a) ^ 2 - (~b) ^ 2, 0) && LtQ(~m, -1 / 2))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~a) * (~A + ~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~a * ~f * (2 * ~m + 1)) + (1 / (~a * ~b * (2 * ~m + 1))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp(~A * ~b * (2 * ~m + 1) - ~a * (~A * (~m + 1) - ~C * ~m) * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x) && (EqQ((~a) ^ 2 - (~b) ^ 2, 0) && LtQ(~m, -1 / 2))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * (~m + 1)) + (1 / (~b * (~m + 1))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ ~m * Simp(~A * ~b * (~m + 1) + (~a * ~C * ~m + ~b * ~B * (~m + 1)) * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x) && (EqQ((~a) ^ 2 - (~b) ^ 2, 0) && Not(LtQ(~m, -1 / 2)))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * (~m + 1)) + (1 / (~b * (~m + 1))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ ~m * Simp(~A * ~b * (~m + 1) + ~a * ~C * ~m * csc(~e + ~f * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C, ~m], ~x) && (EqQ((~a) ^ 2 - (~b) ^ 2, 0) && Not(LtQ(~m, -1 / 2)))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * (~m + 1)) + (1 / (~m + 1)) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m - 1) * Simp(~a * ~A * (~m + 1) + ((~A * ~b + ~a * ~B) * (~m + 1) + ~b * ~C * ~m) * csc(~e + ~f * ~x) + (~b * ~B * (~m + 1) + ~a * ~C * ~m) * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && IGtQ(2 * ~m, 0))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~(m') * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (-(~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ ~m) / (~f * (~m + 1)) + (1 / (~m + 1)) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m - 1) * Simp(~a * ~A * (~m + 1) + (~A * ~b * (~m + 1) + ~b * ~C * ~m) * csc(~e + ~f * ~x) + ~a * ~C * ~m * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && IGtQ(2 * ~m, 0))
    @apply_utils Antiderivative((~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2) / sqrt(~a + ~(b') * csc(~(e') + ~(f') * ~x)), ~x) => Antiderivative((~A + (~B - ~C) * csc(~e + ~f * ~x)) / sqrt(~a + ~b * csc(~e + ~f * ~x)), ~x) + ~C * Antiderivative((csc(~e + ~f * ~x) * (1 + csc(~e + ~f * ~x))) / sqrt(~a + ~b * csc(~e + ~f * ~x)), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x) && NeQ((~a) ^ 2 - (~b) ^ 2, 0)
    @apply_utils Antiderivative((~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2) / sqrt(~a + ~(b') * csc(~(e') + ~(f') * ~x)), ~x) => Antiderivative((~A - ~C * csc(~e + ~f * ~x)) / sqrt(~a + ~b * csc(~e + ~f * ~x)), ~x) + ~C * Antiderivative((csc(~e + ~f * ~x) * (1 + csc(~e + ~f * ~x))) / sqrt(~a + ~b * csc(~e + ~f * ~x)), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x) && NeQ((~a) ^ 2 - (~b) ^ 2, 0)
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (((~A * (~b) ^ 2 - ~a * ~b * ~B) + (~a) ^ 2 * ~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1)) / (~a * ~f * (~m + 1) * ((~a) ^ 2 - (~b) ^ 2)) + (1 / (~a * (~m + 1) * ((~a) ^ 2 - (~b) ^ 2))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp((~A * ((~a) ^ 2 - (~b) ^ 2) * (~m + 1) - ~a * ((~A * ~b - ~a * ~B) + ~b * ~C) * (~m + 1) * csc(~e + ~f * ~x)) + ((~A * (~b) ^ 2 - ~a * ~b * ~B) + (~a) ^ 2 * ~C) * (~m + 2) * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && LtQ(~m, -1))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => ((~A * (~b) ^ 2 + (~a) ^ 2 * ~C) * cot(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1)) / (~a * ~f * (~m + 1) * ((~a) ^ 2 - (~b) ^ 2)) + (1 / (~a * (~m + 1) * ((~a) ^ 2 - (~b) ^ 2))) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1) * Simp((~A * ((~a) ^ 2 - (~b) ^ 2) * (~m + 1) - ~a * ~b * (~A + ~C) * (~m + 1) * csc(~e + ~f * ~x)) + (~A * (~b) ^ 2 + (~a) ^ 2 * ~C) * (~m + 2) * csc(~e + ~f * ~x) ^ 2, ~x), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && (IntegerQ(2 * ~m) && LtQ(~m, -1)))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (1 / ~b) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ ~m * (~A * ~b + (~b * ~B - ~a * ~C) * csc(~e + ~f * ~x)), ~x) + (~C / ~b) * Antiderivative(csc(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && Not(IntegerQ(2 * ~m)))
    @apply_utils Antiderivative((~a + ~(b') * csc(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (1 / ~b) * Antiderivative((~a + ~b * csc(~e + ~f * ~x)) ^ ~m * (~A * ~b - ~a * ~C * csc(~e + ~f * ~x)), ~x) + (~C / ~b) * Antiderivative(csc(~e + ~f * ~x) * (~a + ~b * csc(~e + ~f * ~x)) ^ (~m + 1), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C, ~m], ~x) && (NeQ((~a) ^ 2 - (~b) ^ 2, 0) && Not(IntegerQ(2 * ~m)))
    @apply_utils Antiderivative((~(b') * cos(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(B') * sec(~(e') + ~(f') * ~x) + ~(C') * sec(~(e') + ~(f') * ~x) ^ 2), ~x) => (~b) ^ 2 * Antiderivative((~b * cos(~e + ~f * ~x)) ^ (~m - 2) * (~C + ~B * cos(~e + ~f * ~x) + ~A * cos(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(b') * sin(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~b) ^ 2 * Antiderivative((~b * sin(~e + ~f * ~x)) ^ (~m - 2) * (~C + ~B * sin(~e + ~f * ~x) + ~A * sin(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~B, ~C, ~m], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(b') * cos(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(C') * sec(~(e') + ~(f') * ~x) ^ 2), ~x) => (~b) ^ 2 * Antiderivative((~b * cos(~e + ~f * ~x)) ^ (~m - 2) * (~C + ~A * cos(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~C, ~m], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(b') * sin(~(e') + ~(f') * ~x)) ^ ~m * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (~b) ^ 2 * Antiderivative((~b * sin(~e + ~f * ~x)) ^ (~m - 2) * (~C + ~A * sin(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~b, ~e, ~f, ~A, ~C, ~m], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(a') * (~(b') * sec(~(e') + ~(f') * ~x)) ^ ~p) ^ ~m * (~(A') + ~(B') * sec(~(e') + ~(f') * ~x) + ~(C') * sec(~(e') + ~(f') * ~x) ^ 2), ~x) => (((~a) ^ IntPart(~m) * (~a * (~b * sec(~e + ~f * ~x)) ^ ~p) ^ FracPart(~m)) / (~b * sec(~e + ~f * ~x)) ^ (~p * FracPart(~m))) * Antiderivative((~b * sec(~e + ~f * ~x)) ^ (~m * ~p) * (~A + ~B * sec(~e + ~f * ~x) + ~C * sec(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C, ~m, ~p], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(a') * (~(b') * csc(~(e') + ~(f') * ~x)) ^ ~p) ^ ~m * (~(A') + ~(B') * csc(~(e') + ~(f') * ~x) + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (((~a) ^ IntPart(~m) * (~a * (~b * csc(~e + ~f * ~x)) ^ ~p) ^ FracPart(~m)) / (~b * csc(~e + ~f * ~x)) ^ (~p * FracPart(~m))) * Antiderivative((~b * csc(~e + ~f * ~x)) ^ (~m * ~p) * (~A + ~B * csc(~e + ~f * ~x) + ~C * csc(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~B, ~C, ~m, ~p], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(a') * (~(b') * sec(~(e') + ~(f') * ~x)) ^ ~p) ^ ~m * (~(A') + ~(C') * sec(~(e') + ~(f') * ~x) ^ 2), ~x) => (((~a) ^ IntPart(~m) * (~a * (~b * sec(~e + ~f * ~x)) ^ ~p) ^ FracPart(~m)) / (~b * sec(~e + ~f * ~x)) ^ (~p * FracPart(~m))) * Antiderivative((~b * sec(~e + ~f * ~x)) ^ (~m * ~p) * (~A + ~C * sec(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C, ~m, ~p], ~x) && Not(IntegerQ(~m))
    @apply_utils Antiderivative((~(a') * (~(b') * csc(~(e') + ~(f') * ~x)) ^ ~p) ^ ~m * (~(A') + ~(C') * csc(~(e') + ~(f') * ~x) ^ 2), ~x) => (((~a) ^ IntPart(~m) * (~a * (~b * csc(~e + ~f * ~x)) ^ ~p) ^ FracPart(~m)) / (~b * csc(~e + ~f * ~x)) ^ (~p * FracPart(~m))) * Antiderivative((~b * csc(~e + ~f * ~x)) ^ (~m * ~p) * (~A + ~C * csc(~e + ~f * ~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~e, ~f, ~A, ~C, ~m, ~p], ~x) && Not(IntegerQ(~m))
end
