int_rules_8_8 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 8.8*Polylogarithm*function =#
    #= Antiderivative(PolyLog(2,(~a')*((~b')*(~x)^(~p'))^(~q')),~x) :=  x*PolyLog(2,a*(b*x^p)^q) + p*q*Antiderivative(log(1-a*(b*x^p)^q),x) <--  FreeQ([a,b,p,q],x) =#
    @apply_utils Antiderivative(PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => ~x * PolyLog(~n, ~a * (~b * (~x) ^ ~p) ^ ~q) - ~p * ~q * Antiderivative(PolyLog(~n - 1, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~p, ~q], ~x) && GtQ(~n, 0)
    @apply_utils Antiderivative(PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => (~x * PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q)) / (~p * ~q) - (1 / (~p * ~q)) * Antiderivative(PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~p, ~q], ~x) && LtQ(~n, -1)
    @apply_utils Antiderivative(PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => Unintegrable(PolyLog(~n, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~n, ~p, ~q], ~x)
    @apply_utils Antiderivative(PolyLog(~n, ~(c') * (~(a') + ~(b') * ~x) ^ ~(p')) / (~(d') + ~(e') * ~x), ~x) => PolyLog(~n + 1, ~c * (~a + ~b * ~x) ^ ~p) / (~e * ~p) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~n, ~p], ~x) && EqQ(~b * ~d, ~a * ~e)
    @apply_utils Antiderivative(PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')) / ~x, ~x) => PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q) / (~p * ~q) <-- FreeQ([~a, ~b, ~n, ~p, ~q], ~x)
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => ((~d * ~x) ^ (~m + 1) * PolyLog(~n, ~a * (~b * (~x) ^ ~p) ^ ~q)) / (~d * (~m + 1)) - ((~p * ~q) / (~m + 1)) * Antiderivative((~d * ~x) ^ ~m * PolyLog(~n - 1, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~d, ~m, ~p, ~q], ~x) && (NeQ(~m, -1) && GtQ(~n, 0))
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => ((~d * ~x) ^ (~m + 1) * PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q)) / (~d * ~p * ~q) - ((~m + 1) / (~p * ~q)) * Antiderivative((~d * ~x) ^ ~m * PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~d, ~m, ~p, ~q], ~x) && (NeQ(~m, -1) && LtQ(~n, -1))
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q')), ~x) => Unintegrable((~d * ~x) ^ ~m * PolyLog(~n, ~a * (~b * (~x) ^ ~p) ^ ~q), ~x) <-- FreeQ([~a, ~b, ~d, ~m, ~n, ~p, ~q], ~x)
    @apply_utils Antiderivative((log(~(c') * (~x) ^ ~(m')) ^ ~(r') * PolyLog(~n, ~(a') * (~(b') * (~x) ^ ~(p')) ^ ~(q'))) / ~x, ~x) => (log(~c * (~x) ^ ~m) ^ ~r * PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q)) / (~p * ~q) - ((~m * ~r) / (~p * ~q)) * Antiderivative((log(~c * (~x) ^ ~m) ^ (~r - 1) * PolyLog(~n + 1, ~a * (~b * (~x) ^ ~p) ^ ~q)) / ~x, ~x) <-- FreeQ([~a, ~b, ~c, ~m, ~n, ~q, ~r], ~x) && GtQ(~r, 0)
    @apply_utils Antiderivative(PolyLog(~n, ~(c') * (~(a') + ~(b') * ~x) ^ ~(p')), ~x) => (~x * PolyLog(~n, ~c * (~a + ~b * ~x) ^ ~p) - ~p * Antiderivative(PolyLog(~n - 1, ~c * (~a + ~b * ~x) ^ ~p), ~x)) + ~a * ~p * Antiderivative(PolyLog(~n - 1, ~c * (~a + ~b * ~x) ^ ~p) / (~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~p], ~x) && GtQ(~n, 0)
    @apply_utils Antiderivative(PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)) / (~(d') + ~(e') * ~x), ~x) => (log((1 - ~a * ~c) - ~b * ~c * ~x) * PolyLog(2, ~c * (~a + ~b * ~x))) / ~e + (~b / ~e) * Antiderivative(log((1 - ~a * ~c) - ~b * ~c * ~x) ^ 2 / (~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e], ~x) && EqQ(~c * (~b * ~d - ~a * ~e) + ~e, 0)
    @apply_utils Antiderivative(PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)) / (~(d') + ~(e') * ~x), ~x) => (log(~d + ~e * ~x) * PolyLog(2, ~c * (~a + ~b * ~x))) / ~e + (~b / ~e) * Antiderivative((log(~d + ~e * ~x) * log((1 - ~a * ~c) - ~b * ~c * ~x)) / (~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e], ~x) && NeQ(~c * (~b * ~d - ~a * ~e) + ~e, 0)
    @apply_utils Antiderivative((~(d') + ~(e') * ~x) ^ ~(m') * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => ((~d + ~e * ~x) ^ (~m + 1) * PolyLog(2, ~c * (~a + ~b * ~x))) / (~e * (~m + 1)) + (~b / (~e * (~m + 1))) * Antiderivative(((~d + ~e * ~x) ^ (~m + 1) * log((1 - ~a * ~c) - ~b * ~c * ~x)) / (~a + ~b * ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~m], ~x) && NeQ(~m, -1)
    #= Antiderivative(((~d')+(~e')*(~x))^(~m')*PolyLog((~n),(~c')*((~a')+(~b')*(~x))^(~p')),~x) :=   (d+e*x)^(m+1)*PolyLog(n,c*(a+b*x)^p)/(e*(m+1)) - b*p/(e*(m+1))*Antiderivative((d+e*x)^(m+1)*PolyLog(n-1,c*(a+b*x)^p)/(a+b*x),x)  <-- FreeQ([a,b,c,d,e,m,p],x) && GtQ(n,0) && IGtQ(m,0) =#
    @apply_utils Antiderivative((~x) ^ ~(m') * PolyLog(~n, ~(c') * (~(a') + ~(b') * ~x) ^ ~(p')), ~x) => (-(((~a) ^ (~m + 1) - (~b) ^ (~m + 1) * (~x) ^ (~m + 1))) * PolyLog(~n, ~c * (~a + ~b * ~x) ^ ~p)) / ((~m + 1) * (~b) ^ (~m + 1)) + (~p / ((~m + 1) * (~b) ^ ~m)) * Antiderivative(ExpandIntegrand(PolyLog(~n - 1, ~c * (~a + ~b * ~x) ^ ~p), ((~a) ^ (~m + 1) - (~b) ^ (~m + 1) * (~x) ^ (~m + 1)) / (~a + ~b * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~p], ~x) && (GtQ(~n, 0) && (IntegerQ(~m) && NeQ(~m, -1)))
    @apply_utils Antiderivative((~(g') + ~(h') * log(~(f') * (~(d') + ~(e') * ~x) ^ ~(n'))) * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => (~x * (~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * PolyLog(2, ~c * (~a + ~b * ~x)) + ~b * Antiderivative((~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * log((1 - ~a * ~c) - ~b * ~c * ~x) * ExpandIntegrand(~x / (~a + ~b * ~x), ~x), ~x)) - ~e * ~h * ~n * Antiderivative(PolyLog(2, ~c * (~a + ~b * ~x)) * ExpandIntegrand(~x / (~d + ~e * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~f, ~g, ~h, ~n], ~x)
    @apply_utils Antiderivative((log(1 + ~(e') * ~x) * PolyLog(2, ~(c') * ~x)) / ~x, ~x) => -(PolyLog(2, ~c * ~x) ^ 2) / 2 <-- FreeQ([~c, ~e], ~x) && EqQ(~c + ~e, 0)
    @apply_utils Antiderivative(((~g + ~(h') * log(1 + ~(e') * ~x)) * PolyLog(2, ~(c') * ~x)) / ~x, ~x) => ~g * Antiderivative(PolyLog(2, ~c * ~x) / ~x, ~x) + ~h * Antiderivative((log(1 + ~e * ~x) * PolyLog(2, ~c * ~x)) / ~x, ~x) <-- FreeQ([~c, ~e, ~g, ~h], ~x) && EqQ(~c + ~e, 0)
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(g') + ~(h') * log(~(f') * (~(d') + ~(e') * ~x) ^ ~(n'))) * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => (((~x) ^ (~m + 1) * (~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * PolyLog(2, ~c * (~a + ~b * ~x))) / (~m + 1) + (~b / (~m + 1)) * Antiderivative(ExpandIntegrand((~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * log((1 - ~a * ~c) - ~b * ~c * ~x), (~x) ^ (~m + 1) / (~a + ~b * ~x), ~x), ~x)) - ((~e * ~h * ~n) / (~m + 1)) * Antiderivative(ExpandIntegrand(PolyLog(2, ~c * (~a + ~b * ~x)), (~x) ^ (~m + 1) / (~d + ~e * ~x), ~x), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~f, ~g, ~h, ~n], ~x) && (IntegerQ(~m) && NeQ(~m, -1))
    @apply_utils Antiderivative(~Px * (~(g') + ~(h') * log(~(f') * (~(d') + ~(e') * ~x) ^ ~(n'))) * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => With([u = IntHide(~Px, ~x)], (u * (~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * PolyLog(2, ~c * (~a + ~b * ~x)) + ~b * Antiderivative(ExpandIntegrand((~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * log((1 - ~a * ~c) - ~b * ~c * ~x), u / (~a + ~b * ~x), ~x), ~x)) - ~e * ~h * ~n * Antiderivative(ExpandIntegrand(PolyLog(2, ~c * (~a + ~b * ~x)), u / (~d + ~e * ~x), ~x), ~x)) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~f, ~g, ~h, ~n], ~x) && PolyQ(~Px, ~x)
    @apply_utils Antiderivative((~x) ^ ~m * ~Px * (~(g') + ~(h') * log(1 + ~(e') * ~x)) * PolyLog(2, ~(c') * ~x), ~x) => Coeff(~Px, ~x, -(~m) - 1) * Antiderivative(((~g + ~h * log(1 + ~e * ~x)) * PolyLog(2, ~c * ~x)) / ~x, ~x) + Antiderivative((~x) ^ ~m * (~Px - Coeff(~Px, ~x, -(~m) - 1) * (~x) ^ (-(~m) - 1)) * (~g + ~h * log(1 + ~e * ~x)) * PolyLog(2, ~c * ~x), ~x) <-- FreeQ([~c, ~e, ~g, ~h], ~x) && (PolyQ(~Px, ~x) && (ILtQ(~m, 0) && (EqQ(~c + ~e, 0) && NeQ(Coeff(~Px, ~x, -(~m) - 1), 0))))
    @apply_utils Antiderivative((~x) ^ ~(m') * ~Px * (~(g') + ~(h') * log(~(f') * (~(d') + ~(e') * ~x) ^ ~(n'))) * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => With([u = IntHide((~x) ^ ~m * ~Px, ~x)], (u * (~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * PolyLog(2, ~c * (~a + ~b * ~x)) + ~b * Antiderivative(ExpandIntegrand((~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * log((1 - ~a * ~c) - ~b * ~c * ~x), u / (~a + ~b * ~x), ~x), ~x)) - ~e * ~h * ~n * Antiderivative(ExpandIntegrand(PolyLog(2, ~c * (~a + ~b * ~x)), u / (~d + ~e * ~x), ~x), ~x)) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~f, ~g, ~h, ~n], ~x) && (PolyQ(~Px, ~x) && IntegerQ(~m))
    @apply_utils Antiderivative((~x) ^ ~m * ~(Px') * (~(g') + ~(h') * log(~(f') * (~(d') + ~(e') * ~x) ^ ~(n'))) * PolyLog(2, ~(c') * (~(a') + ~(b') * ~x)), ~x) => Unintegrable((~x) ^ ~m * ~Px * (~g + ~h * log(~f * (~d + ~e * ~x) ^ ~n)) * PolyLog(2, ~c * (~a + ~b * ~x)), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~e, ~f, ~g, ~h, ~m, ~n], ~x) && PolyQ(~Px, ~x)
    @apply_utils Antiderivative(PolyLog(~n, ~(d') * ((~F) ^ (~(c') * (~(a') + ~(b') * ~x))) ^ ~(p')), ~x) => PolyLog(~n + 1, ~d * ((~F) ^ (~c * (~a + ~b * ~x))) ^ ~p) / (~b * ~c * ~p * log(~F)) <-- FreeQ([~F, ~a, ~b, ~c, ~d, ~n, ~p], ~x)
    @apply_utils Antiderivative((~(e') + ~(f') * ~x) ^ ~(m') * PolyLog(~n, ~(d') * ((~F) ^ (~(c') * (~(a') + ~(b') * ~x))) ^ ~(p')), ~x) => ((~e + ~f * ~x) ^ ~m * PolyLog(~n + 1, ~d * ((~F) ^ (~c * (~a + ~b * ~x))) ^ ~p)) / (~b * ~c * ~p * log(~F)) - ((~f * ~m) / (~b * ~c * ~p * log(~F))) * Antiderivative((~e + ~f * ~x) ^ (~m - 1) * PolyLog(~n + 1, ~d * ((~F) ^ (~c * (~a + ~b * ~x))) ^ ~p), ~x) <-- FreeQ([~F, ~a, ~b, ~c, ~d, ~e, ~f, ~n, ~p], ~x) && GtQ(~m, 0)
    @apply_utils Antiderivative(~u * PolyLog(~n, ~v), ~x) => With([w = DerivativeDivides(~v, ~u * ~v, ~x)], w * PolyLog(~n + 1, ~v) <-- Not(FalseQ(w))) <-- FreeQ(~n, ~x)
    @apply_utils Antiderivative(~u * log(~w) * PolyLog(~n, ~v), ~x) => With([z = DerivativeDivides(~v, ~u * ~v, ~x)], z * log(~w) * PolyLog(~n + 1, ~v) - Antiderivative(SimplifyIntegrand((z * D(~w, ~x) * PolyLog(~n + 1, ~v)) / ~w, ~x), ~x) <-- Not(FalseQ(z))) <-- FreeQ(~n, ~x) && InverseFunctionFreeQ(~w, ~x)
end
