Math AI Documentation

Source

Github repository of the code https://github.com/infinity390/mathai

Philosophy

I think it is a big realization in computer science and programming to realize that computers can solve mathematics.
This understanding should be made mainstream. It can help transform education, mathematical research, and computation of mathematical equations for work.

Societal Implications Of Such A Computer Program And The Author's Comment On Universities Of India

I think mathematics is valued by society because of education. Schools and universities teach them.
So this kind of software, if made mainstream, could bring real change.

The Summary Of How Computer "Solves" Math

Math equations are a tree data structure (TreeNode class).
We can manipulate the math equations using various algorithms (functions provided by the mathai library).
We first parse the math equation strings to get the tree data structure (parse function in mathai).

The Library

Import the library by doing:

from mathai import *

str_form

It is the string representation of a TreeNode math equation.

Example

(cos(x)^2)+(sin(x)^2)

Is represented internally as:

f_add
 f_pow
  f_cos
   v_0
  d_2
 f_pow
  f_sin
   v_0
  d_2

Leaf Nodes

Variables (start with a v_ prefix):

• v_0 -> x
• v_1 -> y
• v_2 -> z
• v_3 -> a

Numbers (start with d_ prefix; only integers):

• d_-1 -> -1
• d_0 -> 0
• d_1 -> 1
• d_2 -> 2

Branch Nodes

• f_add -> addition
• f_mul -> multiplication
• f_pow -> power

parse

Takes a math equation string and outputs a TreeNode object.

from mathai import *

equation = parse("sin(x)^2+cos(x)^2")
print(equation)

Output

(cos(x)^2)+(sin(x)^2)

simplify

It simplifies and cleans up a given math equation.

from mathai import *

equation = simplify(parse("(x+x+x+x-1-1-1-1)*(4*x-4)*sin(sin(x+x+x)*sin(3*x))"))
printeq(equation)

Output

((-4+(4*x))^2)*sin((sin((3*x))^2))

Incomplete Documentation, Will be updated and completed later on

Demonstrations

Example Demonstration 1 (derivation of hydrogen and helium atom's ground state energy in electron volts using the variational principle in quantum physics)

from mathai import *
print("ground state energy of hydrogen atom using quantum physics variational principle")
print(f"{hydrogen_gse()} eV")
print()
print("ground state energy of helium atom using quantum physics variational principle")
print(f"{helium_gse()} eV")

Output

ground state energy of hydrogen atom using quantum physics variational principle
-13.605693122882869 eV

ground state energy of helium atom using quantum physics variational principle
-77.48867420464012 eV

Example Demonstration 2 (boolean algebra)

from mathai import *
eq = parse("(A-B)|(B-A)")
eq = set_sub(eq)
eq = solve_logically(eq)
print(eq)
eq = parse("(A|B)-(A&B)")
eq = set_sub(eq)
eq = solve_logically(eq)
print(eq)

Output

(~A&B)|(~B&A)
(~A&B)|(~B&A)

Example Demonstration 3 (limits approaching to a constant value)

from mathai import *
limits = ["(e^(tan(x)) - 1 - tan(x)) / x^2", "sin(x)/x", "(1-cos(x))/x^2", "(sin(x)-x)/sin(x)^3"]
for q in limits:
    q = fraction(simplify(TreeNode("f_limit",[parse(q),parse("x")])))
    q = limit1(q)
    print(q)

Output

1/2
1
1/2
-(1/6)

Example Demonstration 4 (limits approaching to infinity)

from mathai import *
eq= parse("limitpinf((3*x^2+x)/(2*x^2+5),x)")
eq = simplify(eq)
eq = limit4(eq)
eq = simplify(eq)
eq = limit3(eq)
eq = simplify(eq)
print(eq)

Output

3/2

Example Demonstration 5 (linear equations) (general solution of linear equations in two variables)

from mathai import *
eq= parse("a*x+b*y+c = 0 & d*x+f*y+g = 0")
eq = simplify(eq)
eq = linear_solve(eq, [parse(item) for item in "a b c d f g".split(" ")])
eq = factor1(eq)
eq = simplify(eq)
for item in eq.children:
  print(item)

Output

((((c*f)-(b*g))/((a*f)-(b*d)))+x)=0
((((a*g)-(c*d))/((a*f)-(b*d)))+y)=0

Example Demonstration 6 (expectation algebra)

from mathai import *
eq = simplify(parse("covariance(A+B,C+D)=covariance(B,C)+covariance(B,D)+covariance(A,D)+covariance(A,C)"))
eq = logic0(simplify(expect(simplify(expand(expect(eq))))))
print(eq)

Output

true

Example Demonstration 7 (neural networks, older version)

from mathai import NeuralNetwork, NeuralNetworkScalar

for gm in [NeuralNetwork, NeuralNetworkScalar]:
    nn = gm([2,4,4,2], [0,1]).model("dense")
    train_x = [[0.0,0.0],[1.0,0.0],[0.0,1.0],[1.0,1.0]]
    train_y = [[0.0,0.0],[0.0,1.0],[0.0,1.0],[0.0,1.0]]
    nn.train(train_x, train_y, 12, 1000)
    for item in train_x:
        print(nn.predict(item))
    print()

    nn = gm([1,2,6,2], [0,1]).model("rnn_vanilla")
    a_x = [[0.0,1.0]]
    b_x = [[1.0,0.0]]
    c_x = [[1.0,1.0]]
    d_x = [[0.0,0.0]]
    a_y = [[0.0,1.0],[0.0,1.0]]
    b_y = [[0.0,1.0],[0.0,1.0]]
    c_y = [[0.0,1.0],[0.0,1.0]]
    d_y = [[0.0,1.0],[0.0,1.0]]
    train_x = [a_x, b_x, c_x, d_x]
    train_y = [a_y, b_y, c_y, d_y]
    nn.train(train_x, train_y, 12, 100)
    for item in train_x:
        print(nn.predict(item))
    print()

Output

epoches done 1/1000
epoches done 101/1000
epoches done 201/1000
epoches done 301/1000
epoches done 401/1000
epoches done 501/1000
epoches done 601/1000
epoches done 701/1000
epoches done 801/1000
epoches done 901/1000
training done.

[0.0007942662363688463, 0.005414380331103362]
[0.0016579305600058485, 0.9962974002063962]
[0.0017653993828768018, 0.9949707119204272]
[0.0015291756602401642, 0.9971824076135734]

epoches done 1/100
epoches done 11/100
epoches done 21/100
epoches done 31/100
epoches done 41/100
epoches done 51/100
epoches done 61/100
epoches done 71/100
epoches done 81/100
epoches done 91/100
training done.

[[0.012780402811390697, 0.9953976654923926], [0.012713336573813388, 0.9958645028043224]]
[[0.012940077354919177, 0.9908435224431728], [0.012917464946137311, 0.9907321735711152]]
[[0.012940077354919177, 0.9954273843100733], [0.012917464946137311, 0.9958893170859691]]
[[0.012780402811390697, 0.9907654434473478], [0.012713336573813388, 0.9906558567914048]]

epoches done 1/1000
epoches done 101/1000
epoches done 201/1000
epoches done 301/1000
epoches done 401/1000
epoches done 501/1000
epoches done 601/1000
epoches done 701/1000
epoches done 801/1000
epoches done 901/1000
training done.

[0.0032011064862924195, 0.007049572299207291]
[0.0017352861303737029, 0.9959594709440822]
[0.0017576985243942566, 0.9948662186565006]
[0.0018004028889592447, 0.9970687301136343]

epoches done 1/100
epoches done 11/100
epoches done 21/100
epoches done 31/100
epoches done 41/100
epoches done 51/100
epoches done 61/100
epoches done 71/100
epoches done 81/100
epoches done 91/100
training done.

[[0.008834236758389541, 0.9946853486239138], [0.008739967675337235, 0.9948032325721593]]
[[0.008823477410072706, 0.9940402125295567], [0.008727620121273713, 0.9941452266604042]]
[[0.008823477410072706, 0.9947036204624601], [0.008727620121273713, 0.99482101905113]]
[[0.008834236758389541, 0.9940178289678866], [0.008739967675337235, 0.9941232242029681]]

Example Demonstration 8 (neural networks)

from mathai import NeuralNetwork, parse
import random
def binary_random(*shape):
    if len(shape) == 0:
        return random.choice([0,1])
    return [binary_random(*shape[1:]) for _ in range(shape[0])]
activation_function = parse("sigmoid(Z)")
detail = []
detail.append({"dim":[6,6,3]})
detail.append({"dim":[2,2,3], "type":"convolution", "activation":activation_function})
detail.append({"dim":[2], "type":"dense", "activation":activation_function})
nn = NeuralNetwork(detail).model("image")
train_x = binary_random(3, 6, 6, 3)
train_y = binary_random(3, 2)
nn.train(train_x, train_y, 12, 10000, 1)
for item in train_x:
    print(nn.predict(item))
    print(train_y.pop(0))
    print()
print()

Output

matrix calculus formulas compiled
gradients calculated
calculated the equation of every weight in the network
epoch 0/10000
epoch 1000/10000
epoch 2000/10000
epoch 3000/10000
epoch 4000/10000
epoch 5000/10000
epoch 6000/10000
epoch 7000/10000
epoch 8000/10000
epoch 9000/10000

[0.9919816718627309, 0.9985494959144323]
[1, 1]

[0.9862372758368634, 0.9960769568908187]
[1, 1]

[0.015725442209655396, 0.9936864875975912]
[0, 1]

Example Demonstration 9 (automatic testing)

from mathai import *
test(10)

Output

problems generated
1. (-1+x)/y
2. 0
3. 0
4. 2*(y/-1)*(y/1)*y
5. -(2*(x^2))^4
6. -2/-2
7. 1
8. -5+x+y
9. -(2/2)
10. 1

answer
(1)
((x*y)-y)/(y^2)

(2,3)
0
0

(4)
-(2*(y^3))

(5)
16*(x^8)

(6,7,10)
1
1
1

(8)
-5+x+y

(9)
-1

Example Demonstration 10 (equivalent resistance)

from mathai import *
load_formula_from_file()
wire_1 = Edge((0, 1))
ohm_5 = Edge((1, 2), "resistor", TreeNode("d_5"))
ohm_10 = Edge((2, 3), "resistor", TreeNode("d_10"))
ohm_11 = Edge((3, 4), "resistor", TreeNode("d_11"))
ohm_8 = Edge((2, 5), "resistor", TreeNode("d_8"))
ohm_7 = Edge((5, 4), "resistor", TreeNode("d_7"))
ohm_6 = Edge((1, 6), "resistor", TreeNode("d_6"))
ohm_8_2 = Edge((1, 7), "resistor", TreeNode("d_8"))
wire_2 = Edge((6, 8))
wire_3 = Edge((7, 8))
ohm_20 = Edge((8, 4), "resistor", TreeNode("d_20"))
wire_4 = Edge((4, 9))
edge_list = [wire_1, wire_2, wire_3, wire_4,ohm_5, ohm_6, ohm_7, ohm_8, ohm_8_2, ohm_10, ohm_11, ohm_20]
graph = CircuitGraph(10, edge_list, {})
print(compute(find_resistance(graph, 0, 9)))
draw_circuit(graph, start=0, end=9, scale=3.0, grid_size=30)

Output

loading formulas from file...
done

8.66474543707973

Example Demonstration 11 (engineering graphics)

from mathai import *
# (z,y) is dash, a'b' is front view
# (z,-x) is no dash, ab is top view

# A line AB 60 mm long has its end A 20 mm above HP and 30 mm infront of VP. The line is inclined at 40 degrees to HP and is parallel to VP. Draw the projection
solve_graphics_string("30 20 0 None None None None None None 0 40*pi/180 None None 60")
print()

# Engineering Graphics for DEGREE P.I. Varghese
solve_graphics_string("20 25 0 None None None None None None 30*pi/180 0 60 None None") # 11.14
print()
solve_graphics_string("15 25 0 None None None None None None 30*pi/180 0 50 None None") # 11.15
print()
solve_graphics_string("0 -25 0 None None None None None None None 0 55 None 75") # 11.17
print()
solve_graphics_string("25 50 0 -30 None None None None None None 0 50 None 80") # 11.19

Output

Ax : 30
Ay : 20
Az : 0
Bx : 30
By : 20+(60*sin(((2*pi)/9)))
Bz : 60*abs(cos(((2*pi)/9)))
Bx-Ax : 0
By-Ay : 60*sin(((2*pi)/9))
Bz-Az : 60*abs(cos(((2*pi)/9)))
inclination_with_VP : 0
inclination_with_HP : (2*pi)/9
front_view_length : 60
top_view_length : 60*abs(cos(((2*pi)/9)))
line_length : 60

Ax : 20
Ay : 25
Az : 0
Bx : 20+(60/(3^-(-1/2)))
By : 25
Bz : 60
Bx-Ax : 60/(3^-(-1/2))
By-Ay : 0
Bz-Az : 60
inclination_with_VP : pi/6
inclination_with_HP : 0
front_view_length : 60
top_view_length : sqrt(4800)
line_length : 120/(3^-(-1/2))

Ax : 15
Ay : 25
Az : 0
Bx : 15+(50/(3^-(-1/2)))
By : 25
Bz : 50
Bx-Ax : 50/(3^-(-1/2))
By-Ay : 0
Bz-Az : 50
inclination_with_VP : pi/6
inclination_with_HP : 0
front_view_length : 50
top_view_length : 100/(3^-(-1/2))
line_length : 100/(3^-(-1/2))

Ax : 0
Ay : -25
Az : 0
Bx : 75*sin(arccos((11/15)))
By : -25
Bz : 55
Bx-Ax : 75*sin(arccos((11/15)))
By-Ay : 0
Bz-Az : 55
inclination_with_VP : arccos((11/15))
inclination_with_HP : 0
front_view_length : 55
top_view_length : sqrt((3025+(5625*(sin(arccos((11/15)))^2))))
line_length : 75

Ax : 25
Ay : 50
Az : 0
Bx : -30
By : 50
Bz : 80*abs(cos(arcsin((-11/16))))
Bx-Ax : -55
By-Ay : 0
Bz-Az : 80*abs(cos(arcsin((-11/16))))
inclination_with_VP : arcsin((-11/16))
inclination_with_HP : 0
front_view_length : 50
top_view_length : sqrt((3025+(6400*(cos(arcsin((-11/16)))^2))))
line_length : 80

Questions solved using god() function

Code

from mathai import *
question_list = """integrate(tan(x)/(sec(x)+tan(x)),x)
integrate(sec(x)/(sec(x)+tan(x)),x)
integrate(e^arctan(x)/(1+x^2),x)
integrate(sin(x)^2/(1+cos(x)),x)
integrate(tan(x)^3,x)
integrate(cos(x)/(1+cos(x)),x)
integrate(1/(1+sin(x)),x)
integrate(cos(x)/(1+sin(x))^2,x)
(x-1)^2 = x^2 - 1
(sin(x)+cosec(x))^2+(cos(x)+sec(x))^2=7+tan(x)^2+cot(x)^2
2*x/(2*x^2+5*x+2)>1/(x+1)
(5*x-1)<(x+1)^2&(x+1)^2<7*x-3
abs(x+5)*x+2*abs(x+7)-2=0
x*abs(x)-5*abs(x+2)+6=0
abs(3*x-5)+abs(8-x)=abs(3+2*x)
abs(x^2+5*x+9)<abs(x^2+2*x+2)+abs(3*x+7)
(A-B)|(B-A) <-> (A|B)-(A&B)
(cosec(x)-cot(x))^2=(1-cos(x))/(1+cos(x))
x^2 = 4 & x+y^2 = 1
x + y*x = 5 & y + z=5 & z = 4
integrate(abs(x+1),x,-4,10)
integrate(abs(sin(x)),x,-pi,pi/6)
x^(2*x)=1
-i*(i+1)^5
sqrt(x) = x-2
integrate(sin(x+a)/sin(x),x)
integrate(sqrt(sin(2*x))*cos(2*x),x)
x = y & y = z & x+y+z=180
sec(x)^2*tan(y)+sec(y)^2*tan(x)*dif(y,x)=0
x + y = 10 & x*y = 24
(x+y)*dif(y,x)=1
abs(abs(x-2)-3)<=2
abs(x)>=0
dif(y,x)=arcsin(x)
integrate(sin(x)^6+cos(x)^6+3*sin(x)^2*cos(x)^2,x)
integrate((x^4+x^2+1)/(x^2-x+1),x)
integrate(1/(sin(x)^2*cos(x)^2),x)
integrate(x/sqrt(x+4),x)
integrate(sin(x)^4,x)
integrate(2*x/(1+x^2),x)
integrate(sin(2*x+5)^2,x)
integrate(sqrt(a*x+b),x)
integrate(x*sqrt(x),x)
integrate(x*sqrt(1+2*x^2),x)
integrate(e^(2*x+3),x)
integrate(x/e^(x^2),x)
integrate(sin(x)*sin(cos(x)),x)
integrate(sin(3*x)*cos(4*x),x)
integrate(cos(2*x)*cos(4*x)*cos(6*x),x)
integrate(sin(2*x+1)^3,x)
integrate(sin(x)^3*cos(x)^3,x)
integrate(sin(x)*sin(2*x)*sin(3*x),x)
integrate(sin(4*x)*sin(8*x),x)
integrate(cos(2*x)^4,x)
integrate(x/((x+1)*(x+2)),x)
integrate(1/(x^2-9),x)
integrate((3*x-1)/((x-1)*(x-2)*(x-3)),x)
integrate(x/((x-1)*(x-2)*(x-3)),x)
integrate(2*x/(x^2+3*x+2),x)
integrate((1-x^2)/(x*(1-2*x)),x)
integrate(x/((x-1)^2*(x+2)),x)
integrate((2*x-3)/((x^2-1)*(2*x+3)),x)
integrate(5*x/((x+1)*(x^2-4)),x)
(x+2)*(x+3)/((x-2)*(x-3))<=1
cos(x)/(1+sin(x))+(1+sin(x))/cos(x)=2*sec(x)
tan(x)/(1-cot(x))+cot(x)/(1-tan(x))=1+sec(x)*cosec(x)
(1+sec(x))/sec(x)=sin(x)^2/(1-cos(x))
(cos(x)-sin(x)+1)/(cos(x)+sin(x)-1)=cosec(x)+cot(x)
integrate(x/((x-1)*(x^2+1)),x)
(sin(x)-2*sin(x)^3)/(2*cos(x)^3-cos(x))=tan(x)
(cosec(x)-sin(x))*(sec(x)-cos(x))=1/(tan(x)+cot(x))
integrate(2/((1-x)*(1+x^2)),x)
x^2-abs(x+2)+x>0
limit(sin(x)/x,x)
limit((x^2 - 1)/(x-1),x,1)
dif(y,x)=sqrt(4-y^2)
dif(y,x)+y=1
x^5*dif(y,x)=-y^5
dif(y,x)=(1+x^2)*(1+y^2)
x*(x^2-1)*dif(y,x)=1
(x^2+x*y)*dif(y,x)=(x^2+y^2)
dif(y,x)=(x+y)/x
(x-y)*dif(y,x)-(x+y)=0
(x^2-y^2)+2*x*y*dif(y,x)=0
x*dif(y,x)-y+x*sin(y/x)=0
(a+b)^2 = a^2 + b^2 + 2*a*b
(x-1)*(x+1) = x^2 - 1
integrate((7^(7^(7^x)))*(7^(7^x))*(7^x),x)"""
for item in question_list.split("\n"):
  god(item)

Output

? integrate(tan(x)/(sec(x)+tan(x)),x)
thinking...
integrate(((cos(x)*sin(x))/(cos(x)+(cos(x)*sin(x)))),x)
integrate((sin((2*x))/(2*(cos(x)+(sin((2*x))/2)))),x)
integrate((sin((2*x))/(cos(x)+(sin((2*x))/2))),x)/2
integrate((sin(x)/(1+sin(x))),x)
integrate((sin(x)/(1+sin(x))),x)
integrate(((((-1+(cos(x)^2))*(cos(x)^2))+((cos(x)^2)*sin(x)))/(cos(x)^4)),x)
integrate((1+(-1/(cos(x)^2))+(sin(x)/(cos(x)^2))),x)
integrate((sin(x)/(cos(x)^2)),x)-tan(x)+x
-tan(x)+try(subs(integrate((y/(1/((1-(y^2))^(-3/2)))),y),y,sin(x)),subs(integrate((-1/(y^2)),y),y,cos(x)),subs(integrate((cos((y^(-1/2)))/2),y),y,(1/(cos(x)^2))))+x
-tan(x)+try(subs(integrate((y/(1/(((1-y)*(1+y))^(-3/2)))),y),y,sin(x)),subs((1/y),y,cos(x)),subs((integrate(cos((y^(-1/2))),y)/2),y,(1/(cos(x)^2))))+x
=> (1/cos(x))+(-sin(x)/cos(x))+x

? integrate(sec(x)/(sec(x)+tan(x)),x)
thinking...
integrate((cos(x)/(cos(x)+(cos(x)*sin(x)))),x)
integrate((cos(x)/(cos(x)+(sin((2*x))/2))),x)
integrate((1/(1+sin(x))),x)
integrate((1/(1+sin(x))),x)
integrate(((-((cos(x)^2)*sin(x))+(cos(x)^2))/(cos(x)^4)),x)
integrate(((1/(cos(x)^2))+(-sin(x)/(cos(x)^2))),x)
-integrate((sin(x)/(cos(x)^2)),x)+tan(x)
-try(subs(integrate((y/(1/((1-(y^2))^(-3/2)))),y),y,sin(x)),subs(integrate((-1/(y^2)),y),y,cos(x)),subs(integrate((cos((y^(-1/2)))/2),y),y,(1/(cos(x)^2))))+tan(x)
-try(subs(integrate((y/(1/(((1-y)*(1+y))^(-3/2)))),y),y,sin(x)),subs((1/y),y,cos(x)),subs((integrate(cos((y^(-1/2))),y)/2),y,(1/(cos(x)^2))))+tan(x)
=> (-1/cos(x))+(sin(x)/cos(x))

? integrate(e^arctan(x)/(1+x^2),x)
thinking...
integrate((1/((1+(x^2))*(e^-arctan(x)))),x)
integrate((1/((1+(x^2))*(e^-arctan(x)))),x)
integrate((1/((1+(x^2))*(e^-arcsin((x/(1/((1+(x^2))^(-1/2)))))))),x)
integrate((1/((1+(x^2))*(e^-arcsin((x/(1/((1+(x^2))^(-1/2)))))))),x)
try(subs(integrate((-1/(2*(1/((-1+(1/y))^(-1/2)))*(e^-arcsin((sqrt((-1+(1/y)))*sqrt(y))))*y)),y),y,(1/(1+(x^2)))),subs(integrate((1/(2*(1+y)*(1/(y^(-1/2)))*(e^-arcsin((sqrt(y)/(1/((1+y)^(-1/2)))))))),y),y,(x^2)),subs(integrate((-1/(abs(y)*(1/((-1+(1/(y^2)))^(-1/2)))*(e^-arcsin((abs(y)*sqrt((-1+(1/(y^2))))))))),y),y,((1+(x^2))^(-1/2))))
try(subs((-integrate((1/((1/((1-y)^(-1/2)))*(1/(y^(-1/2)))*(e^-arcsin(sqrt((1-y)))))),y)/2),y,(1/(1+(x^2)))),subs((integrate((1/((1+y)*(1/(y^(-1/2)))*(e^-arcsin((sqrt(y)/(1/((1+y)^(-1/2)))))))),y)/2),y,(x^2)),subs(-integrate((1/((1/((1-(y^2))^(-1/2)))*(e^-arcsin(sqrt((1-(y^2))))))),y),y,((1+(x^2))^(-1/2))))
try(subs((-integrate((1/((1/((1-y)^(-1/2)))*(1/(y^(-1/2)))*(e^-arcsin(sqrt((1-y)))))),y)/2),y,(1/(1+(x^2)))),subs((integrate((1/((1+y)*(1/(y^(-1/2)))*(e^-arcsin((sqrt(y)/(1/((1+y)^(-1/2)))))))),y)/2),y,(x^2)),subs(-integrate((1/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*(e^-arcsin((sqrt((1-y))*sqrt((1+y))))))),y),y,((1+(x^2))^(-1/2))))
try(subs((-integrate((1/((1/((1-y)^(-1/2)))*(1/(y^(-1/2)))*(e^-arcsin(sqrt((1-y)))))),y)/2),y,(1/(1+(x^2)))),subs((integrate((1/((1+y)*(1/(y^(-1/2)))*(e^-arcsin((sqrt(y)/(1/((1+y)^(-1/2)))))))),y)/2),y,(x^2)),subs(-integrate((1/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*(e^-arcsin((sqrt((1-y))*sqrt((1+y))))))),y),y,((1+(x^2))^(-1/2))))
try(subs(integrate(1,y),y,(e^arctan(x))),subs(integrate((1/(2*(1+y)*(1/(y^(-1/2)))*(e^-arctan(sqrt(y))))),y),y,(x^2)),subs(integrate((-1/(2*(1/((-1+(1/y))^(-1/2)))*(e^-arctan(sqrt((-1+(1/y)))))*y)),y),y,(1/(1+(x^2)))))
try(subs(y,y,(e^arctan(x))),subs((integrate((1/((1+y)*(1/(y^(-1/2)))*(e^-arctan(sqrt(y))))),y)/2),y,(x^2)),subs((-integrate((1/((1/((-1+(1/y))^(-1/2)))*(e^-arctan(sqrt((-1+(1/y)))))*y)),y)/2),y,(1/(1+(x^2)))))
=> e^arctan(x)

? integrate(sin(x)^2/(1+cos(x)),x)
thinking...
integrate(((sin(x)^2)/(1+cos(x))),x)
integrate(((1/(2*(1+cos(x))))+(-cos((2*x))/(2*(1+cos(x))))),x)
(integrate((1/(1+cos(x))),x)/2)+(-integrate((cos((2*x))/(1+cos(x))),x)/2)
integrate((1-cos(x)),x)
-sin(x)+x
=> -sin(x)+x

? integrate(tan(x)^3,x)
thinking...
integrate(((sin(x)/cos(x))^3),x)
integrate((((3*sin(x))/(4*(cos(x)^3)))+(-sin((3*x))/(4*(cos(x)^3)))),x)
((3*integrate((sin(x)/(cos(x)^3)),x))/4)+(-integrate((sin((3*x))/(cos(x)^3)),x)/4)
integrate(((sin(x)^3)/(cos(x)^3)),x)
integrate(((sin(x)^3)/(cos(x)^3)),x)
try(subs(integrate(((y^3)/((1-(y^2))^2)),y),y,sin(x)),subs(integrate(((-1+(y^2))/(y^3)),y),y,cos(x)),subs(integrate((sin((y^(1/3)))/(3*(cos((y^(1/3)))^4))),y),y,(sin(x)^3)))
try(subs(integrate(((y^3)/(((1-y)^2)*((1+y)^2))),y),y,sin(x)),subs(integrate((((-1+y)*(1+y))/(y^3)),y),y,cos(x)),subs((integrate((sin((y^(1/3)))/(cos((y^(1/3)))^4)),y)/3),y,(sin(x)^3)))
try(subs(integrate(((-1/(2*(1+y)))+(-1/(4*((1-y)^2)))+(1/(2*(1-y)))+(1/(4*((1+y)^2)))),y),y,sin(x)),subs(integrate((((-1+y)*(1+y))/(y^3)),y),y,cos(x)),subs((integrate((sin((y^(1/3)))/(cos((y^(1/3)))^4)),y)/3),y,(sin(x)^3)))
try(subs(((-1/(4*(1-y)))+(-1/(4*(1+y)))+(-log(abs((1-y)))/2)+(-log(abs((1+y)))/2)),y,sin(x)),subs(integrate((((-1+y)*(1+y))/(y^3)),y),y,cos(x)),subs((integrate((sin((y^(1/3)))/(cos((y^(1/3)))^4)),y)/3),y,(sin(x)^3)))
=> (-1/(2*(1-sin(x))*(1+sin(x))))+((log(abs((1-sin(x))))*(sin(x)^2))/(2*(1-sin(x))*(1+sin(x))))+((log(abs((1+sin(x))))*(sin(x)^2))/(2*(1-sin(x))*(1+sin(x))))+(-log(abs((1-sin(x))))/(2*(1-sin(x))*(1+sin(x))))+(-log(abs((1+sin(x))))/(2*(1-sin(x))*(1+sin(x))))

? integrate(cos(x)/(1+cos(x)),x)
thinking...
integrate((cos(x)/(1+cos(x))),x)
integrate(((((-1+(sin(x)^2))*(sin(x)^2))+(cos(x)*(sin(x)^2)))/(sin(x)^4)),x)
integrate((1+(-1/(sin(x)^2))+(cos(x)/(sin(x)^2))),x)
cot(x)+integrate((cos(x)/(sin(x)^2)),x)+x
cot(x)+try(subs(integrate((-sin((y^(-1/2)))/2),y),y,(1/(sin(x)^2))),subs(integrate((1/(y^2)),y),y,sin(x)),subs(integrate((-y/(1/((1-(y^2))^(-3/2)))),y),y,cos(x)))+x
cot(x)+try(subs((-integrate(sin((y^(-1/2))),y)/2),y,(1/(sin(x)^2))),subs((-1/y),y,sin(x)),subs(-integrate((y/(1/(((1-y)*(1+y))^(-3/2)))),y),y,cos(x)))+x
=> (-1/sin(x))+(cos(x)/sin(x))+x

? integrate(1/(1+sin(x)),x)
thinking...
integrate((1/(1+sin(x))),x)
integrate(((-((cos(x)^2)*sin(x))+(cos(x)^2))/(cos(x)^4)),x)
integrate(((1/(cos(x)^2))+(-sin(x)/(cos(x)^2))),x)
-integrate((sin(x)/(cos(x)^2)),x)+tan(x)
-try(subs(integrate((y/(1/((1-(y^2))^(-3/2)))),y),y,sin(x)),subs(integrate((-1/(y^2)),y),y,cos(x)),subs(integrate((cos((y^(-1/2)))/2),y),y,(1/(cos(x)^2))))+tan(x)
-try(subs(integrate((y/(1/(((1-y)*(1+y))^(-3/2)))),y),y,sin(x)),subs((1/y),y,cos(x)),subs((integrate(cos((y^(-1/2))),y)/2),y,(1/(cos(x)^2))))+tan(x)
=> (-1/cos(x))+(sin(x)/cos(x))

? integrate(cos(x)/(1+sin(x))^2,x)
thinking...
integrate((cos(x)/((1+sin(x))^2)),x)
integrate((cos(x)/((3/2)+(-cos((2*x))/2)+(2*sin(x)))),x)
integrate(((((cos(x)^6)*(sin(x)^2))-(2*(cos(x)^6)*sin(x))+(cos(x)^6))/(cos(x)^9)),x)
integrate(((1/(cos(x)^3))+(-(2*sin(x))/(cos(x)^3))+((sin(x)^2)/(cos(x)^3))),x)
integrate((1/(cos(x)^3)),x)+integrate(((sin(x)^2)/(cos(x)^3)),x)-(2*integrate((sin(x)/(cos(x)^3)),x))
-(2*try(subs(integrate((-1/(y^3)),y),y,cos(x)),subs(integrate((y/((1-(y^2))^2)),y),y,sin(x)),subs(integrate((cos((y^(-1/3)))/3),y),y,(1/(cos(x)^3)))))+try(subs(integrate((cos((y^(-1/3)))/(3*sin((y^(-1/3))))),y),y,(1/(cos(x)^3))),subs(integrate((-1/((1/((1-(y^2))^(-1/2)))*(y^3))),y),y,cos(x)),subs(integrate(sqrt((1+(y^2))),y),y,(sin(x)/cos(x))))+try(subs(integrate((-sqrt((1-(y^2)))/(y^3)),y),y,cos(x)),subs(integrate(((y^2)/((1-(y^2))^2)),y),y,sin(x)),subs(integrate((sin(sqrt(y))/(2*(cos(sqrt(y))^4))),y),y,(sin(x)^2)))
-(2*try(subs((1/(2*(y^2))),y,cos(x)),subs(integrate((y/(((1-y)^2)*((1+y)^2))),y),y,sin(x)),subs((integrate(cos((y^(-1/3))),y)/3),y,(1/(cos(x)^3)))))+try(subs((integrate((cos((y^(-1/3)))/sin((y^(-1/3)))),y)/3),y,(1/(cos(x)^3))),subs(-integrate((1/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*(y^3))),y),y,cos(x)),subs(integrate(sqrt((1+(y^2))),y),y,(sin(x)/cos(x))))+try(subs(-integrate(((sqrt((1-y))*sqrt((1+y)))/(y^3)),y),y,cos(x)),subs(integrate(((y^2)/(((1-y)^2)*((1+y)^2))),y),y,sin(x)),subs((integrate((sin(sqrt(y))/(cos(sqrt(y))^4)),y)/2),y,(sin(x)^2)))
-(2*try(subs((1/(2*(y^2))),y,cos(x)),subs(integrate(((-1/(4*((1-y)^2)))+(1/(4*((1+y)^2)))),y),y,sin(x)),subs((integrate(cos((y^(-1/3))),y)/3),y,(1/(cos(x)^3)))))+try(subs((integrate((cos((y^(-1/3)))/sin((y^(-1/3)))),y)/3),y,(1/(cos(x)^3))),subs(-integrate((1/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*(y^3))),y),y,cos(x)),subs(integrate(sqrt((1+(y^2))),y),y,(sin(x)/cos(x))))+try(subs(-integrate(((sqrt((1-y))*sqrt((1+y)))/(y^3)),y),y,cos(x)),subs(integrate(((-1/(4*((1-y)^2)))+(-1/(4*((1+y)^2)))+(1/(4*(1-y)))+(1/(4*(1+y)))),y),y,sin(x)),subs((integrate((sin(sqrt(y))/(cos(sqrt(y))^4)),y)/2),y,(sin(x)^2)))
-(2*try(subs((1/(2*(y^2))),y,cos(x)),subs(((-1/(4*(1-y)))+(-1/(4*(1+y)))),y,sin(x)),subs((integrate(cos((y^(-1/3))),y)/3),y,(1/(cos(x)^3)))))+try(subs((integrate((cos((y^(-1/3)))/sin((y^(-1/3)))),y)/3),y,(1/(cos(x)^3))),subs(-integrate((1/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*(y^3))),y),y,cos(x)),subs(integrate(sqrt((1+(y^2))),y),y,(sin(x)/cos(x))))+try(subs(-integrate(((sqrt((1-y))*sqrt((1+y)))/(y^3)),y),y,cos(x)),subs(((-1/(4*(1-y)))+(1/(4*(1+y)))+(log(abs((1+y)))/4)+(-log(abs((1-y)))/4)),y,sin(x)),subs((integrate((sin(sqrt(y))/(cos(sqrt(y))^4)),y)/2),y,(sin(x)^2)))
try(subs(integrate((1/(y^2)),y),y,(1+sin(x))),subs(integrate((1/((1+y)^2)),y),y,sin(x)),subs(integrate((-y/((1/((1-(y^2))^(-1/2)))*((1+sqrt((1-(y^2))))^2))),y),y,cos(x)))
try(subs((-1/y),y,(1+sin(x))),subs((-1/(1+y)),y,sin(x)),subs(-integrate((y/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2)))*((1+(sqrt((1-y))*sqrt((1+y))))^2))),y),y,cos(x)))
=> -1/(1+sin(x))

? (x-1)^2 = x^2 - 1
thinking...
(1-(x^2)+((-1+x)^2))=0
(2-(2*x))=0
x∈{1}
=> x∈{1}

? (sin(x)+cosec(x))^2+(cos(x)+sec(x))^2=7+tan(x)^2+cot(x)^2
thinking...
(-7-(cot(x)^2)-(tan(x)^2)+((cos(x)+sec(x))^2)+((cosec(x)+sin(x))^2))=0
(-7-((cos(x)/sin(x))^2)-((sin(x)/cos(x))^2)+((cos(x)+(1/cos(x)))^2)+(((1/sin(x))+sin(x))^2))=0
0=0
true
=> true

? 2*x/(2*x^2+5*x+2)>1/(x+1)
thinking...
((-1/(1+x))+((2*x)/(2+(2*(x^2))+(5*x))))>0
~((((-1/(1+x))+((2*x)/(2+(2*(x^2))+(5*x))))=0)|(((-1/(1+x))+((2*x)/(2+(2*(x^2))+(5*x))))<0))
~(((-2-(3*x))=0)|(((-2-(3*x))/((1+x)*(2+(2*(x^2))+(5*x))))<0))
x∈(-2,-1)U(-2/3,-1/2)
=> x∈(-2,-1)U(-2/3,-1/2)

? (5*x-1)<(x+1)^2&(x+1)^2<7*x-3
thinking...
((-1+(5*x)+((-1-x)*(1+x)))<0)&((3-(7*x)+((1+x)^2))<0)
((-2+(3*x)-(x^2))<0)&((4-(5*x)+(x^2))<0)
x∈(2,4)
=> x∈(2,4)

? abs(x+5)*x+2*abs(x+7)-2=0
thinking...
(-2+(2*abs((7+x)))+(abs((5+x))*x))=0
(((5+x)<0)&((((-2+(2*(-7-x))+((-5-x)*x))=0)&((7+x)<0))|(((-2+(2*(7+x))+((-5-x)*x))=0)&(((7+x)=0)|~(((7+x)=0)|((7+x)<0))))))|(((((-2+(2*(-7-x))+((5+x)*x))=0)&((7+x)<0))|(((-2+(2*(7+x))+((5+x)*x))=0)&(((7+x)=0)|~(((7+x)=0)|((7+x)<0)))))&(((5+x)=0)|~(((5+x)=0)|((5+x)<0))))
(((5+x)<0)&((((-16-(7*x)-(x^2))=0)&((7+x)<0))|(((12-(3*x)-(x^2))=0)&(((7+x)=0)|~(((7+x)=0)|((7+x)<0))))))|(((((-16+(3*x)+(x^2))=0)&((7+x)<0))|(((12+(7*x)+(x^2))=0)&(((7+x)=0)|~(((7+x)=0)|((7+x)<0)))))&(((5+x)=0)|~(((5+x)=0)|((5+x)<0))))
x∈{-4,(-3/2)+(-sqrt(57)/2),-3}
x∈{-4,(-6-(2*sqrt(57)))/4,-3}
=> x∈{-4,(-6-(2*sqrt(57)))/4,-3}

? x*abs(x)-5*abs(x+2)+6=0
thinking...
(6+(abs(x)*x)-(5*abs((2+x))))=0
((x<0)&((((6+(5*(-2-x))-(x^2))=0)&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))|(((6+(5*(2+x))-(x^2))=0)&((2+x)<0))))|(((((6+(5*(-2-x))+(x^2))=0)&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))|(((6+(5*(2+x))+(x^2))=0)&((2+x)<0)))&((x=0)|~((x=0)|(x<0))))
((x<0)&((((-4-(5*x)-(x^2))=0)&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))|(((16+(5*x)-(x^2))=0)&((2+x)<0))))|(((((-4-(5*x)+(x^2))=0)&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))|(((16+(5*x)+(x^2))=0)&((2+x)<0)))&((x=0)|~((x=0)|(x<0))))
x∈{-1,(5/2)+(-sqrt(89)/2),(5/2)+(sqrt(41)/2)}
x∈{-1,(10-(2*sqrt(89)))/4,(10+(2*sqrt(41)))/4}
=> x∈{-1,(10-(2*sqrt(89)))/4,(10+(2*sqrt(41)))/4}

? abs(3*x-5)+abs(8-x)=abs(3+2*x)
thinking...
(abs((-5+(3*x)))+abs((8-x))-abs((3+(2*x))))=0
(((3+(2*x))<0)&((((8-x)<0)&(((0=0)&((-5+(3*x))<0))|(((-10+(6*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))))|(((((16-(2*x))=0)&((-5+(3*x))<0))|(((6+(4*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0)))))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0))))))|(((((8-x)<0)&((((-16+(2*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|(((-6-(4*x))=0)&((-5+(3*x))<0))))|((((0=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|(((10-(6*x))=0)&((-5+(3*x))<0)))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0)))))&(((3+(2*x))=0)|~(((3+(2*x))=0)|((3+(2*x))<0))))
(((3+(2*x))<0)&((((8-x)<0)&(((0=0)&((-5+(3*x))<0))|(((-10+(6*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))))|(((((16-(2*x))=0)&((-5+(3*x))<0))|(((6+(4*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0)))))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0))))))|(((((8-x)<0)&((((-16+(2*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|(((-6-(4*x))=0)&((-5+(3*x))<0))))|((((0=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|(((10-(6*x))=0)&((-5+(3*x))<0)))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0)))))&(((3+(2*x))=0)|~(((3+(2*x))=0)|((3+(2*x))<0))))
(((3+(2*x))<0)&((((8-x)<0)&((((-10+(6*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|((-5+(3*x))<0)))|(((((16-(2*x))=0)&((-5+(3*x))<0))|(((6+(4*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0)))))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0))))))|(((((8-x)<0)&((((-16+(2*x))=0)&(((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0))))|(((-6-(4*x))=0)&((-5+(3*x))<0))))|(((((10-(6*x))=0)&((-5+(3*x))<0))|((-5+(3*x))=0)|~(((-5+(3*x))=0)|((-5+(3*x))<0)))&(((8-x)=0)|~(((8-x)=0)|((8-x)<0)))))&(((3+(2*x))=0)|~(((3+(2*x))=0)|((3+(2*x))<0))))
x∈(5/3,8)U{8,5/3}
=> x∈(5/3,8)U{8,5/3}

? abs(x^2+5*x+9)<abs(x^2+2*x+2)+abs(3*x+7)
thinking...
(abs((9+(5*x)+(x^2)))-abs((2+(2*x)+(x^2)))-abs((7+(3*x))))<0
(((7+(3*x))<0)&((((2+(2*x)+(x^2))<0)&(((0<0)&((9+(5*x)+(x^2))<0))|(((18+(10*x)+(2*(x^2)))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))))|(((((-4-(2*(x^2))-(4*x))<0)&((9+(5*x)+(x^2))<0))|(((14+(6*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0)))))&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0))))))|(((((2+(2*x)+(x^2))<0)&((((-14-(6*x))<0)&((9+(5*x)+(x^2))<0))|(((4+(2*(x^2))+(4*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))))|((((0<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))|(((-18-(10*x)-(2*(x^2)))<0)&((9+(5*x)+(x^2))<0)))&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0)))))&(((7+(3*x))=0)|~(((7+(3*x))=0)|((7+(3*x))<0))))
(((7+(3*x))<0)&((((2+(2*x)+(x^2))<0)&(((0<0)&((9+(5*x)+(x^2))<0))|(((18+(10*x)+(2*(x^2)))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))))|(((((-4-(2*(x^2))-(4*x))<0)&((9+(5*x)+(x^2))<0))|(((14+(6*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0)))))&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0))))))|(((((2+(2*x)+(x^2))<0)&((((-14-(6*x))<0)&((9+(5*x)+(x^2))<0))|(((4+(2*(x^2))+(4*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))))|((((0<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))|(((-18-(10*x)-(2*(x^2)))<0)&((9+(5*x)+(x^2))<0)))&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0)))))&(((7+(3*x))=0)|~(((7+(3*x))=0)|((7+(3*x))<0))))
(((7+(3*x))<0)&((((18+(10*x)+(2*(x^2)))<0)&((2+(2*x)+(x^2))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0))))|(((((-4-(2*(x^2))-(4*x))<0)&((9+(5*x)+(x^2))<0))|(((14+(6*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0)))))&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0))))))|(((((-18-(10*x)-(2*(x^2)))<0)&((9+(5*x)+(x^2))<0)&(((2+(2*x)+(x^2))=0)|~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0))))|(((2+(2*x)+(x^2))<0)&((((-14-(6*x))<0)&((9+(5*x)+(x^2))<0))|(((4+(2*(x^2))+(4*x))<0)&(((9+(5*x)+(x^2))=0)|~(((9+(5*x)+(x^2))=0)|((9+(5*x)+(x^2))<0)))))))&(((7+(3*x))=0)|~(((7+(3*x))=0)|((7+(3*x))<0))))
x∈(-inf,-7/3)
=> x∈(-inf,-7/3)

? (A-B)|(B-A) <-> (A|B)-(A&B)
thinking...
=> true

? (cosec(x)-cot(x))^2=(1-cos(x))/(1+cos(x))
thinking...
(((-1+cos(x))/(1+cos(x)))+((cosec(x)-cot(x))^2))=0
(((-1+cos(x))/(1+cos(x)))+(((1/sin(x))+(-cos(x)/sin(x)))^2))=0
0=0
true
=> true

? x^2 = 4 & x+y^2 = 1
thinking...
((-1+(y^2)+x)=0)&((-4+(x^2))=0)
(((-2+x)=0)&((1+(y^2))=0))|(((2+x)=0)&((-sqrt(3)+y)=0))
(x∈{-2}&y∈{sqrt(12)/2})|x∈{}
=> (x∈{-2}&y∈{sqrt(12)/2})|x∈{}

? x + y*x = 5 & y + z=5 & z = 4
thinking...
((-4+z)=0)&((-5+(x*y)+x)=0)&((-5+y+z)=0)
((-1+y)=0)&((-4+z)=0)&((-5+(x*y)+x)=0)
((-1+y)=0)&((-5+(2*x))=0)&z∈{4}
x∈{5/2}&y∈{1}&z∈{4}
=> x∈{5/2}&y∈{1}&z∈{4}

? integrate(abs(x+1),x,-4,10)
thinking...
-subs((((2*x)+(x^2))/2),x,-1)-subs(((-(2*x)-(x^2))/2),x,-4)+subs((((2*x)+(x^2))/2),x,10)+subs(((-(2*x)-(x^2))/2),x,-1)
=> 65

? integrate(abs(sin(x)),x,-pi,pi/6)
thinking...
-subs(cos(x),x,-pi)-subs(-cos(x),x,0)+subs(cos(x),x,0)+subs(-cos(x),x,(pi/6))
=> 3+(-sqrt(3)/2)

? x^(2*x)=1
thinking...
(-1+(x^(2*x)))=0
(((1+x)=0)&(((2*x)%2)=0))|((x=0)&~(x=0))|((-1+x)=0)
(((1+x)=0)&(((2*x)%2)=0))|((x=0)&~(x=0))|((-1+x)=0)
((1+x)=0)|x∈{1}
x∈{-1,1}
=> x∈{-1,1}

? -i*(i+1)^5
thinking...
=> -4+(4*i)

? sqrt(x) = x-2
thinking...
(2-x+sqrt(x))=0
x∈{4}
=> x∈{4}

? integrate(sin(x+a)/sin(x),x)
thinking...
integrate((((cos(x)*sin(a))+(cos(a)*sin(x)))/sin(x)),x)
integrate(((sin((-x+a))/(2*sin(x)))+(sin((-a+x))/(2*sin(x)))+(sin((x+a))/sin(x))),x)
(integrate((((cos(-x)*sin(a))+(cos(a)*sin(-x)))/sin(x)),x)/2)+(integrate((((cos(-a)*sin(x))+(cos(x)*sin(-a)))/sin(x)),x)/2)+integrate((((cos(x)*sin(a))+(cos(a)*sin(x)))/sin(x)),x)
integrate((cos(a)+((cos(x)*sin(a))/sin(x))),x)
(cos(a)*x)+(integrate((cos(x)/sin(x)),x)*sin(a))
(cos(a)*x)+(sin(a)*try(subs(integrate((-y/(1-(y^2))),y),y,cos(x)),subs(integrate((1/y),y),y,sin(x)),subs(integrate(-sin((1/y)),y),y,(1/sin(x)))))
(cos(a)*x)+(sin(a)*try(subs((log(abs((-1+(y^2))))/2),y,cos(x)),subs(log(abs(y)),y,sin(x)),subs(-integrate(sin((1/y)),y),y,(1/sin(x)))))
=> ((log(abs((-1+(cos(x)^2))))*sin(a))/2)+(cos(a)*x)

? integrate(sqrt(sin(2*x))*cos(2*x),x)
thinking...
integrate((cos((2*x))*sqrt(sin((2*x)))),x)
integrate((((2*sqrt(2)*sqrt(sin(x)))/(1/(cos(x)^(5/2))))-(sqrt(2)*sqrt(cos(x))*sqrt(sin(x)))),x)
(2*integrate((sqrt(sin(x))/(1/(cos(x)^(5/2)))),x)*sqrt(2))-(integrate((sqrt(cos(x))*sqrt(sin(x))),x)*sqrt(2))
(2*sqrt(2)*try(subs(integrate((sqrt(y)/(1/((1-(y^2))^(3/4)))),y),y,sin(x)),subs(integrate((-1/((1/((1-(y^2))^(-1/4)))*(1/(y^(5/2))))),y),y,cos(x)),subs(integrate(((2*sin((y^2)))/(1/(cos((y^2))^(3/2)))),y),y,sqrt(sin(x)))))-(sqrt(2)*try(subs(integrate((-sqrt(y)/(1/((1-(y^2))^(-1/4)))),y),y,cos(x)),subs(integrate((sqrt(y)/(1/((1-(y^2))^(-1/4)))),y),y,sin(x)),subs(integrate(((2*sin((y^2)))/(1/(cos((y^2))^(-1/2)))),y),y,sqrt(sin(x)))))
(2*sqrt(2)*try(subs(integrate((sqrt(y)/(1/(((1-y)*(1+y))^(3/4)))),y),y,sin(x)),subs(-integrate((1/((1/(((1-y)*(1+y))^(-1/4)))*(1/(y^(5/2))))),y),y,cos(x)),subs((2*integrate((sin((y^2))/(1/(cos((y^2))^(3/2)))),y)),y,sqrt(sin(x)))))-(sqrt(2)*try(subs(-integrate((sqrt(y)/(1/(((1-y)*(1+y))^(-1/4)))),y),y,cos(x)),subs(integrate((sqrt(y)/(1/(((1-y)*(1+y))^(-1/4)))),y),y,sin(x)),subs((2*integrate((sin((y^2))/(1/(cos((y^2))^(-1/2)))),y)),y,sqrt(sin(x)))))
(2*sqrt(2)*try(subs(integrate((sqrt(y)/(1/(((1-y)*(1+y))^(3/4)))),y),y,sin(x)),subs(-integrate((1/((1/(((1-y)*(1+y))^(-1/4)))*(1/(y^(5/2))))),y),y,cos(x)),subs((2*integrate((sin((y^2))/(1/(cos((y^2))^(3/2)))),y)),y,sqrt(sin(x)))))-(sqrt(2)*try(subs(-integrate((sqrt(y)/(1/(((1-y)*(1+y))^(-1/4)))),y),y,cos(x)),subs(integrate((sqrt(y)/(1/(((1-y)*(1+y))^(-1/4)))),y),y,sin(x)),subs((2*integrate((sin((y^2))/(1/(cos((y^2))^(-1/2)))),y)),y,sqrt(sin(x)))))
try(subs(integrate((sqrt(y)/2),y),y,sin((2*x))),subs(integrate(((cos(y)*sqrt(sin(y)))/2),y),y,(2*x)),subs(integrate((-y/(2*(1/((1-(y^2))^(-1/4))))),y),y,cos((2*x))))
try(subs((1/(3*(1/(y^(3/2))))),y,sin((2*x))),subs((integrate((cos(y)*sqrt(sin(y))),y)/2),y,(2*x)),subs((-integrate((y/(1/(((1-y)*(1+y))^(-1/4)))),y)/2),y,cos((2*x))))
=> 1/(3*(1/(sin((2*x))^(3/2))))

? x = y & y = z & x+y+z=180
thinking...
((-180+x+y+z)=0)&((-y+x)=0)&((-z+y)=0)
((-60+x)=0)&((-60+y)=0)&((-60+z)=0)
x∈{60}&y∈{60}&z∈{60}
=> x∈{60}&y∈{60}&z∈{60}

? sec(x)^2*tan(y)+sec(y)^2*tan(x)*dif(y,x)=0
thinking...
(-integrate((1/(cos(x)*sin(x))),x)-integrate((1/(cos(y)*sin(y))),y)+c1)=0
(-integrate((2/sin((2*x))),x)-integrate((2/sin((2*y))),y)+c1)=0
(-log(abs(tan(x)))-log(abs(tan(y)))+c1)=0
=> (-log(abs((sin(x)/cos(x))))-log(abs((sin(y)/cos(y))))+c1)=0

? x + y = 10 & x*y = 24
thinking...
((-10+x+y)=0)&((-24+(x*y))=0)
(((-10+x+y)=0)&((-4+x)=0))|(((-10+x+y)=0)&((-4+x)=0)&((-4+y)=0))|(((-10+x+y)=0)&((-4+x)=0)&((-4+y)=0)&((6-x)=0))|(((-10+x+y)=0)&((-4+x)=0)&((-4+y)=0)&((6-y)=0))|(((-10+x+y)=0)&((-4+x)=0)&((6-x)=0))|(((-10+x+y)=0)&((-4+x)=0)&((6-x)=0)&((6-y)=0))|(((-10+x+y)=0)&((-4+x)=0)&((6-y)=0))|(((-10+x+y)=0)&((-4+y)=0))|(((-10+x+y)=0)&((-4+y)=0)&((6-x)=0))|(((-10+x+y)=0)&((-4+y)=0)&((6-x)=0)&((6-y)=0))|(((-10+x+y)=0)&((-4+y)=0)&((6-y)=0))|(((-10+x+y)=0)&((6-x)=0))|(((-10+x+y)=0)&((6-x)=0)&((6-y)=0))|(((-10+x+y)=0)&((6-y)=0))
(((-10+x+y)=0)&x∈{})|(((-10+x+y)=0)&y∈{})|(((-4+x)=0)&((-6+y)=0))|(((-4+x)=0)&((-6+y)=0)&x∈{4})|(((-4+x)=0)&((-6+y)=0)&x∈{6})|(((-4+x)=0)&((-6+y)=0)&x∈{})|(((-4+x)=0)&((-6+y)=0)&y∈{})|(((-4+y)=0)&((-6+x)=0))|(((-4+y)=0)&((-6+x)=0)&x∈{4})|(((-4+y)=0)&((-6+x)=0)&x∈{6})|(((-4+y)=0)&((-6+x)=0)&x∈{})|(((-4+y)=0)&((-6+x)=0)&y∈{})
(x∈{4}&y∈{6})|(x∈{6}&y∈{4})|(x∈{}&y∈{4})|(x∈{}&y∈{6})|x∈{}
(x∈{4}&y∈{6})|(x∈{6}&y∈{4})|x∈{}
=> (x∈{4}&y∈{6})|(x∈{6}&y∈{4})|x∈{}

? (x+y)*dif(y,x)=1
thinking...
((x/(e^y))-integrate((y/(e^y)),y)-c1)=0
((x/(e^y))-try(subs(integrate((z/(e^-z)),z),z,-y),subs(integrate(log(z),z),z,(e^-y)))-c1)=0
((x/(e^y))-try(subs(((integrate((e^z),z)*z)-integrate(integrate((e^z),z),z)),z,-y),subs(try(((integrate(1,z)*log(z))-integrate((integrate(1,z)/z),z)),(integrate(log(z),z)-integrate(0,z))),z,(e^-y)))-c1)=0
((x/(e^y))-try(subs(((-1/(e^-z))+(z/(e^-z))),z,-y),subs(try(((log(z)*z)-z),integrate(log(z),z)),z,(e^-y)))-c1)=0
=> ((x/(e^y))+(y/(e^y))-c1+(e^-y))=0

? abs(abs(x-2)-3)<=2
thinking...
(-2+abs((-3+abs((-2+x)))))<=0
(((-2+x)<0)&((((-1-x)<0)&(((-1+x)=0)|((-1+x)<0)))|((((-1-x)=0)|~(((-1-x)=0)|((-1-x)<0)))&(((-3-x)=0)|((-3-x)<0)))))|(((((-5+x)<0)&(((3-x)=0)|((3-x)<0)))|((((-5+x)=0)|~(((-5+x)=0)|((-5+x)<0)))&(((-7+x)=0)|((-7+x)<0))))&(((-2+x)=0)|~(((-2+x)=0)|((-2+x)<0))))
(((-2+x)<0)&((((-1-x)<0)&(((-1+x)=0)|((-1+x)<0)))|((((-1-x)=0)|~(((-1-x)=0)|((-1-x)<0)))&(((-3-x)=0)|((-3-x)<0)))))|(((((-5+x)<0)&(((3-x)=0)|((3-x)<0)))|((((-5+x)=0)|~(((-5+x)=0)|((-5+x)<0)))&(((-7+x)=0)|((-7+x)<0))))&(((-2+x)=0)|~(((-2+x)=0)|((-2+x)<0))))
x∈(-3,1)U(3,7)U{1,7,3,-3}
=> x∈(-3,1)U(3,7)U{1,7,3,-3}

? abs(x)>=0
thinking...
((x<0)&((x=0)|~((x=0)|(x>0))))|(x=0)|~((x=0)|(x<0))
((x<0)&((x=0)|~((x=0)|(x>0))))|(x=0)|~((x=0)|(x<0))
((x<0)&((x=0)|~((x=0)|~(x<=0))))|(x=0)|~((x=0)|(x<0))
true
=> true

? dif(y,x)=arcsin(x)
thinking...
(integrate(arcsin(x),x)-y+c1)=0
(-y+try(((arcsin(x)*integrate(1,x))-integrate((integrate(1,x)/(1/((1-(x^2))^(-1/2)))),x)),(integrate(arcsin(x),x)-integrate(0,x)))+c1)=0
(-y+try(((arcsin(x)*x)+sqrt((1-(x^2)))),integrate(arcsin(x),x))+c1)=0
=> ((arcsin(x)*x)-y+sqrt((1-(x^2)))+c1)=0

? integrate(sin(x)^6+cos(x)^6+3*sin(x)^2*cos(x)^2,x)
thinking...
integrate((cos(x)^6),x)+integrate((sin(x)^6),x)+(3*integrate(((cos(x)^2)*(sin(x)^2)),x))
integrate(((5/16)+(cos((6*x))/32)+((15*cos((2*x)))/32)+((3*cos((4*x)))/16)),x)+integrate(((5/16)+((3*cos((4*x)))/16)+(-cos((6*x))/32)+(-(15*cos((2*x)))/32)),x)+(3*integrate(((1/8)+(-cos((4*x))/8)),x))
((3*sin((4*x)))/32)+((5*x)/8)+(3*((-sin((4*x))/32)+(x/8)))
=> x

? integrate((x^4+x^2+1)/(x^2-x+1),x)
thinking...
integrate(((1+(x^2)+(x^4))/(1-x+(x^2))),x)
integrate((1+(x^2)+x),x)
((2*(x^3))+(3*(x^2))+(6*x))/6
=> ((x^2)/2)+((x^3)/3)+x

? integrate(1/(sin(x)^2*cos(x)^2),x)
thinking...
integrate((1/((cos(x)^2)*(sin(x)^2))),x)
integrate((4/((1+cos((2*x)))*(1-cos((2*x))))),x)
4*integrate((1/((1+cos((2*x)))*(1-cos((2*x))))),x)
integrate(((1/(cos(x)^2))+(1/(sin(x)^2))),x)
-cot(x)+tan(x)
=> (-cos(x)/sin(x))+(sin(x)/cos(x))

? integrate(x/sqrt(x+4),x)
thinking...
integrate((x/(1/((4+x)^(-1/2)))),x)
try(subs(integrate(((-4+y)/(1/(y^(-1/2)))),y),y,(4+x)),subs(integrate(((2*(4+(-1/(y^2))))/(y^2)),y),y,((4+x)^(-1/2))))
try(subs(integrate(((-4+y)/(1/(y^(-1/2)))),y),y,(4+x)),subs((2*integrate(((-1+(4*(y^2)))/(y^4)),y)),y,((4+x)^(-1/2))))
try(subs(integrate(((-4+y)/(1/(y^(-1/2)))),y),y,(4+x)),subs((2*integrate(((4*((-1/2)+y)*((1/2)+y))/(y^4)),y)),y,((4+x)^(-1/2))))
try(subs(integrate(((-4+y)/(1/(y^(-1/2)))),y),y,(4+x)),subs((8*integrate(((((-1/2)+y)*((1/2)+y))/(y^4)),y)),y,((4+x)^(-1/2))))
try(subs(integrate(((-4+y)/(1/(y^(-1/2)))),y),y,(4+x)),subs((2*integrate(((4+(-1/(y^2)))/(y^2)),y)),y,((4+x)^(-1/2))))
try(subs(integrate(((-4/(1/(y^(-1/2))))+sqrt(y)),y),y,(4+x)),subs((2*integrate(((-1/(y^4))+(4/(y^2))),y)),y,((4+x)^(-1/2))))
try(subs(((2*(-(12*sqrt(y))+(y^(3/2))))/3),y,(4+x)),subs((2*integrate(((-1+(4*(y^2)))/(y^4)),y)),y,((4+x)^(-1/2))))
=> (2/(3*(1/((4+x)^(3/2)))))-(8*sqrt((4+x)))

? integrate(sin(x)^4,x)
thinking...
integrate((sin(x)^4),x)
integrate(((3/8)+(cos((4*x))/8)+(-cos((2*x))/2)),x)
((3*x)/8)+(-sin((2*x))/4)+(sin((4*x))/32)
=> ((3*x)/8)+(-sin((2*x))/4)+(sin((4*x))/32)

? integrate(2*x/(1+x^2),x)
thinking...
log(abs((1+(x^2))))
=> log(abs((1+(x^2))))

? integrate(sin(2*x+5)^2,x)
thinking...
integrate((((cos(5)*sin((2*x)))+(cos((2*x))*sin(5)))^2),x)
integrate((((cos(5)*sin((2*x)))+(cos((2*x))*sin(5)))^2),x)
integrate(((1/2)+(cos((-10+(4*x)))/8)+(-cos((10+(4*x)))/2)+(-cos((10-(4*x)))/8)),x)
((((cos(-10)*sin((4*x)))/4)+((cos((4*x))*sin(-10))/4))/8)+((((cos(10)*sin(-(4*x)))/4)+((cos(-(4*x))*sin(10))/4))/8)+(((-(cos(10)*sin((4*x)))/4)+(-(cos((4*x))*sin(10))/4))/2)+(x/2)
=> (-(cos(10)*sin((4*x)))/8)+(-(cos((4*x))*sin(10))/8)+(x/2)

? integrate(sqrt(a*x+b),x)
thinking...
2/(3*(1/(((x*a)+b)^(3/2)))*a)
=> 2/(3*(1/(((x*a)+b)^(3/2)))*a)

? integrate(x*sqrt(x),x)
thinking...
2/(5*(1/(x^(5/2))))
=> 2/(5*(1/(x^(5/2))))

? integrate(x*sqrt(1+2*x^2),x)
thinking...
integrate((sqrt((1+(2*(x^2))))*x),x)
integrate((sqrt((1+(2*(x^2))))*x),x)
try(subs(integrate(((1+(2*((sqrt((-1+(y^2)))/(2^-(-1/2)))^2)))/2),y),y,sqrt((1+(2*(x^2))))),subs(integrate((sqrt((1+(2*y)))/2),y),y,(x^2)))
try(subs(((integrate(((-1+y)*(1+y)),y)+y)/2),y,sqrt((1+(2*(x^2))))),subs((1/(6*(1/((1+(2*y))^(3/2))))),y,(x^2)))
=> 1/(6*(1/((1+(2*(x^2)))^(3/2))))

? integrate(e^(2*x+3),x)
thinking...
1/(2*(e^(-3-(2*x))))
=> 1/(2*(e^(-3-(2*x))))

? integrate(x/e^(x^2),x)
thinking...
integrate((x/(e^(x^2))),x)
integrate((x/(e^(x^2))),x)
try(subs(integrate((1/(2*(e^y))),y),y,(x^2)),subs(integrate((-1/2),y),y,(e^-(x^2))))
try(subs((-1/(2*(e^y))),y,(x^2)),subs((-y/2),y,(e^-(x^2))))
=> -1/(2*(e^(x^2)))

? integrate(sin(x)*sin(cos(x)),x)
thinking...
integrate((sin(cos(x))*sin(x)),x)
integrate(((cos((cos(x)-x))/2)+(-cos((cos(x)+x))/2)),x)
((integrate((cos(cos(x))*cos(-x)),x)-integrate((sin(cos(x))*sin(-x)),x))/2)+((integrate((sin(cos(x))*sin(x)),x)-integrate((cos(cos(x))*cos(x)),x))/2)
try(subs(integrate((-sin(sqrt((1-(y^2))))/cos(sqrt((1-(y^2))))),y),y,sin(cos(x))),subs(integrate(((sin(sqrt((1-(y^2))))*y)/(1/((1-(y^2))^(-1/2)))),y),y,sin(x)),subs(integrate(-sin(y),y),y,cos(x)))
try(subs(-integrate((sin((sqrt((1-y))*sqrt((1+y))))/cos((sqrt((1-y))*sqrt((1+y))))),y),y,sin(cos(x))),subs(integrate(((sin((sqrt((1-y))*sqrt((1+y))))*y)/((1/((1-y)^(-1/2)))*(1/((1+y)^(-1/2))))),y),y,sin(x)),subs(cos(y),y,cos(x)))
=> cos(cos(x))

? integrate(sin(3*x)*cos(4*x),x)
thinking...
integrate((cos((4*x))*sin((3*x))),x)
integrate(((-sin(x)/2)+(sin((7*x))/2)),x)
(cos(x)/2)+(-cos((7*x))/14)
=> (cos(x)/2)+(-cos((7*x))/14)

? integrate(cos(2*x)*cos(4*x)*cos(6*x),x)
thinking...
integrate((cos((2*x))*cos((4*x))*cos((6*x))),x)
integrate(((1/4)+(cos((12*x))/4)+(cos((4*x))/4)+(cos((8*x))/4)),x)
(sin((12*x))/48)+(sin((4*x))/16)+(sin((8*x))/32)+(x/4)
=> (sin((12*x))/48)+(sin((4*x))/16)+(sin((8*x))/32)+(x/4)

? integrate(sin(2*x+1)^3,x)
thinking...
integrate((((cos(1)*sin((2*x)))+(cos((2*x))*sin(1)))^3),x)
integrate((((cos(1)*sin((2*x)))+(cos((2*x))*sin(1)))^3),x)
integrate((((25*sin((-1+(2*x))))/32)+((25*sin((1-(2*x))))/32)+((3*sin((-1+(6*x))))/16)+((3*sin((1-(6*x))))/16)+(-(3*sin((-1-(6*x))))/8)+(-(3*sin((-3+(2*x))))/16)+(-(3*sin((-3-(2*x))))/8)+(-(3*sin((1+(6*x))))/8)+(-(3*sin((3+(2*x))))/8)+(-(3*sin((3-(2*x))))/16)+(-sin((-1-(2*x)))/4)+(-sin((-3+(6*x)))/32)+(-sin((3+(6*x)))/4)+(-sin((3-(6*x)))/32)+(sin((1+(2*x)))/2)),x)
((((cos(-3)*cos((6*x)))/6)+(-(sin(-3)*sin((6*x)))/6))/32)+((((cos(3)*cos((6*x)))/6)+(-(sin(3)*sin((6*x)))/6))/4)+((((sin(-1)*sin(-(2*x)))/2)+(-(cos(-1)*cos(-(2*x)))/2))/4)+((((sin(1)*sin((2*x)))/2)+(-(cos(1)*cos((2*x)))/2))/2)+((((sin(3)*sin(-(6*x)))/6)+(-(cos(3)*cos(-(6*x)))/6))/32)+((25*(((cos(1)*cos(-(2*x)))/2)+(-(sin(1)*sin(-(2*x)))/2)))/32)+((25*(((sin(-1)*sin((2*x)))/2)+(-(cos(-1)*cos((2*x)))/2)))/32)+((3*(((cos(-3)*cos((2*x)))/2)+(-(sin(-3)*sin((2*x)))/2)))/16)+((3*(((cos(1)*cos((6*x)))/6)+(-(sin(1)*sin((6*x)))/6)))/8)+((3*(((cos(1)*cos(-(6*x)))/6)+(-(sin(1)*sin(-(6*x)))/6)))/16)+((3*(((cos(3)*cos((2*x)))/2)+(-(sin(3)*sin((2*x)))/2)))/8)+((3*(((sin(-1)*sin((6*x)))/6)+(-(cos(-1)*cos((6*x)))/6)))/16)+((3*(((sin(-1)*sin(-(6*x)))/6)+(-(cos(-1)*cos(-(6*x)))/6)))/8)+((3*(((sin(-3)*sin(-(2*x)))/2)+(-(cos(-3)*cos(-(2*x)))/2)))/8)+((3*(((sin(3)*sin(-(2*x)))/2)+(-(cos(3)*cos(-(2*x)))/2)))/16)
=> ((3*sin(1)*sin((2*x)))/8)+((cos(3)*cos((6*x)))/24)+(-(3*cos(1)*cos((2*x)))/8)+(-(sin(3)*sin((6*x)))/24)

? integrate(sin(x)^3*cos(x)^3,x)
thinking...
integrate(((cos(x)^3)*(sin(x)^3)),x)
integrate((((3*sin((2*x)))/32)+(-sin((6*x))/32)),x)
(cos((6*x))/192)+(-(3*cos((2*x)))/64)
=> (cos((6*x))/192)+(-(3*cos((2*x)))/64)

? integrate(sin(x)*sin(2*x)*sin(3*x),x)
thinking...
integrate((sin((2*x))*sin((3*x))*sin(x)),x)
integrate(((-sin((6*x))/4)+(sin((2*x))/4)+(sin((4*x))/4)),x)
(cos((6*x))/24)+(-cos((2*x))/8)+(-cos((4*x))/16)
=> (cos((6*x))/24)+(-cos((2*x))/8)+(-cos((4*x))/16)

? integrate(sin(4*x)*sin(8*x),x)
thinking...
integrate((sin((4*x))*sin((8*x))),x)
integrate(((cos((4*x))/2)+(-cos((12*x))/2)),x)
(-sin((12*x))/24)+(sin((4*x))/8)
=> (-sin((12*x))/24)+(sin((4*x))/8)

? integrate(cos(2*x)^4,x)
thinking...
integrate((cos((2*x))^4),x)
integrate(((3/8)+(cos((4*x))/2)+(cos((8*x))/8)),x)
((3*x)/8)+(sin((4*x))/8)+(sin((8*x))/64)
=> ((3*x)/8)+(sin((4*x))/8)+(sin((8*x))/64)

? integrate(x/((x+1)*(x+2)),x)
thinking...
(log(abs((2+(3*x)+(x^2))))/2)+(-(3*integrate((1/(2+(3*x)+(x^2))),x))/2)
(log(abs(((1+x)*(2+x))))/2)+(-(3*integrate((1/((1+x)*(2+x))),x))/2)
(log(abs(((1+x)*(2+x))))/2)+(-(3*integrate(((-1/(1+x))+(1/(2+x))),x))/2)
(log(abs(((1+x)*(2+x))))/2)+((3*(log(abs((1+x)))-log(abs((2+x)))))/2)
=> (log(abs((2+(3*x)+(x^2))))/2)+((3*log(abs((1+x))))/2)+(-(3*log(abs((2+x))))/2)

? integrate(1/(x^2-9),x)
thinking...
integrate((1/((-3+x)*(3+x))),x)
integrate(((-1/(6*(-3+x)))+(1/(6*(3+x)))),x)
(log(abs((3+x)))/6)+(-log(abs((-3+x)))/6)
=> (log(abs((3+x)))/6)+(-log(abs((-3+x)))/6)

? integrate((3*x-1)/((x-1)*(x-2)*(x-3)),x)
thinking...
integrate(((-1+(3*x))/((-1+x)*(-2+x)*(-3+x))),x)
integrate(((-1/(-1+x))+(-4/(-3+x))+(5/(-2+x))),x)
(5*log(abs((-2+x))))-log(abs((-1+x)))-(4*log(abs((-3+x))))
=> (5*log(abs((-2+x))))-log(abs((-1+x)))-(4*log(abs((-3+x))))

? integrate(x/((x-1)*(x-2)*(x-3)),x)
thinking...
integrate((x/((-1+x)*(-2+x)*(-3+x))),x)
integrate(((-1/(2*(-1+x)))+(-3/(2*(-3+x)))+(2/(-2+x))),x)
(-log(abs((-1+x)))/2)+(-(3*log(abs((-3+x))))/2)+(2*log(abs((-2+x))))
=> (-log(abs((-1+x)))/2)+(-(3*log(abs((-3+x))))/2)+(2*log(abs((-2+x))))

? integrate(2*x/(x^2+3*x+2),x)
thinking...
2*((log(abs((2+(3*x)+(x^2))))/2)+(-(3*integrate((1/(2+(3*x)+(x^2))),x))/2))
2*((log(abs(((1+x)*(2+x))))/2)+(-(3*integrate((1/((1+x)*(2+x))),x))/2))
2*((log(abs(((1+x)*(2+x))))/2)+(-(3*integrate(((-1/(1+x))+(1/(2+x))),x))/2))
2*((log(abs(((1+x)*(2+x))))/2)+((3*(log(abs((1+x)))-log(abs((2+x)))))/2))
=> log(abs((2+(3*x)+(x^2))))+(3*log(abs((1+x))))-(3*log(abs((2+x))))

? integrate((1-x^2)/(x*(1-2*x)),x)
thinking...
integrate((((1-x)*(1+x))/((1-(2*x))*x)),x)
integrate(((-1/x)+(-2/(1-(2*x)))),x)
log(abs((1-(2*x))))-log(abs(x))
=> log(abs((1-(2*x))))-log(abs(x))

? integrate(x/((x-1)^2*(x+2)),x)
thinking...
integrate((x/((2+x)*((-1+x)^2))),x)
integrate(((-1/(3*((-1+x)^2)))+(-2/(9*(-1+x)))+(2/(9*(2+x)))),x)
(1/(3*(-1+x)))+((2*log(abs((2+x))))/9)+(-(2*log(abs((-1+x))))/9)
=> (1/(3*(-1+x)))+((2*log(abs((-1+x))))/(9*(-1+x)))+((2*log(abs((2+x)))*x)/(9*(-1+x)))+(-(2*log(abs((-1+x)))*x)/(9*(-1+x)))+(-(2*log(abs((2+x))))/(9*(-1+x)))

? integrate((2*x-3)/((x^2-1)*(2*x+3)),x)
thinking...
integrate(((-3+(2*x))/((-1+x)*(1+x)*(3+(2*x)))),x)
integrate(((-5/(2*(1+x)))+(1/(10*(-1+x)))+(24/(5*(3+(2*x))))),x)
(log(abs((-1+x)))/10)+((12*log(abs((3+(2*x)))))/5)+(-(5*log(abs((1+x))))/2)
=> (log(abs((-1+x)))/10)+((12*log(abs((3+(2*x)))))/5)+(-(5*log(abs((1+x))))/2)

? integrate(5*x/((x+1)*(x^2-4)),x)
thinking...
5*integrate((x/((-2+x)*(1+x)*(2+x))),x)
5*integrate(((-1/(3*(1+x)))+(-1/(6*(-2+x)))+(1/(2*(2+x)))),x)
5*((log(abs((2+x)))/2)+(-log(abs((-2+x)))/6)+(-log(abs((1+x)))/3))
=> ((5*log(abs((2+x))))/2)+(-(5*log(abs((-2+x))))/6)+(-(5*log(abs((1+x))))/3)

? (x+2)*(x+3)/((x-2)*(x-3))<=1
thinking...
(-1+(((2+x)*(3+x))/((-2+x)*(-3+x))))<=0
((-1+(((2+x)*(3+x))/((-2+x)*(-3+x))))=0)|((-1+(((2+x)*(3+x))/((-2+x)*(-3+x))))<0)
((-1+(6/((-2+x)*(-3+x)))+((5*x)/((-2+x)*(-3+x)))+((x^2)/((-2+x)*(-3+x))))=0)|((-1+(6/((-2+x)*(-3+x)))+((5*x)/((-2+x)*(-3+x)))+((x^2)/((-2+x)*(-3+x))))<0)
(((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))=0)|((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))/(((-2+x)^3)*((-3+x)^3)))<0)
((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))=0)|((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))/(((-2+x)^3)*((-3+x)^3)))<0))&x∈(-inf,+inf)-{2,3}
((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))=0)|((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))/(((-2+x)^3)*((-3+x)^3)))<0))&x∈(-inf,+inf)-{3,2}
=> ((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))=0)|((((10*(x^5))+(360*x)+(370*(x^3))-(100*(x^4))-(600*(x^2)))/(((-2+x)^3)*((-3+x)^3)))<0))&x∈(-inf,+inf)-{3,2}

? cos(x)/(1+sin(x))+(1+sin(x))/cos(x)=2*sec(x)
thinking...
(((1+sin(x))/cos(x))+(cos(x)/(1+sin(x)))-(2*sec(x)))=0
((-2/cos(x))+((1+sin(x))/cos(x))+(cos(x)/(1+sin(x))))=0
0=0
true
=> true

? tan(x)/(1-cot(x))+cot(x)/(1-tan(x))=1+sec(x)*cosec(x)
thinking...
(-1+(cot(x)/(1-tan(x)))+(tan(x)/(1-cot(x)))-(cosec(x)*sec(x)))=0
(-1+(-1/(cos(x)*sin(x)))+(cos(x)/((1+(-sin(x)/cos(x)))*sin(x)))+(sin(x)/((1+(-cos(x)/sin(x)))*cos(x))))=0
0=0
true
=> true

? (1+sec(x))/sec(x)=sin(x)^2/(1-cos(x))
thinking...
(((1+sec(x))/sec(x))+(-(sin(x)^2)/(1-cos(x))))=0
((-(sin(x)^2)/(1-cos(x)))+((1+(1/cos(x)))*cos(x)))=0
0=0
true
=> true

? (cos(x)-sin(x)+1)/(cos(x)+sin(x)-1)=cosec(x)+cot(x)
thinking...
(((1+cos(x)-sin(x))/(-1+cos(x)+sin(x)))-cosec(x)-cot(x))=0
((-1/sin(x))+((1+cos(x)-sin(x))/(-1+cos(x)+sin(x)))+(-cos(x)/sin(x)))=0
0=0
true
=> true

? integrate(x/((x-1)*(x^2+1)),x)
thinking...
integrate((x/((-1+x)*(1+(x^2)))),x)
integrate(((-1/(2*(-1+x)))+(((-1/2)+(x/2))/(1+(x^2)))),x)
(log(abs((1+(x^2))))/4)+(-arctan(x)/2)+(-log(abs((-1+x)))/2)
=> (log(abs((1+(x^2))))/4)+(-arctan(x)/2)+(-log(abs((-1+x)))/2)

? (sin(x)-2*sin(x)^3)/(2*cos(x)^3-cos(x))=tan(x)
thinking...
(((-(2*(sin(x)^3))+sin(x))/((2*(cos(x)^3))-cos(x)))-tan(x))=0
(((-(2*(sin(x)^3))+sin(x))/((2*(cos(x)^3))-cos(x)))+(-sin(x)/cos(x)))=0
0=0
true
=> true

? (cosec(x)-sin(x))*(sec(x)-cos(x))=1/(tan(x)+cot(x))
thinking...
((-1/(cot(x)+tan(x)))+((cosec(x)-sin(x))*(-cos(x)+sec(x))))=0
((-1/((cos(x)/sin(x))+(sin(x)/cos(x))))+(((1/cos(x))-cos(x))*((1/sin(x))-sin(x))))=0
0=0
true
=> true

? integrate(2/((1-x)*(1+x^2)),x)
thinking...
2*integrate((1/((1-x)*(1+(x^2)))),x)
2*integrate(((-1/(2*(1-x)))+(((-1/2)+(-x/2))/(1+(x^2)))),x)
2*((log(abs((1-x)))/2)+(-arctan(x)/2)+(-log(abs((1+(x^2))))/4))
=> (-log(abs((1+(x^2))))/2)+log(abs((1-x)))-arctan(x)

? x^2-abs(x+2)+x>0
thinking...
(-abs((2+x))+(x^2)+x)>0
(((2+x)<0)&~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0)))|(~(((-2+(x^2))=0)|((-2+(x^2))<0))&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))
(((2+x)<0)&~(((2+(2*x)+(x^2))=0)|((2+(2*x)+(x^2))<0)))|(~(((-2+(x^2))=0)|((-2+(x^2))<0))&(((2+x)=0)|~(((2+x)=0)|((2+x)<0))))
x∈(-inf,-sqrt(8)/2)U(sqrt(8)/2,+inf)
=> x∈(-inf,-sqrt(8)/2)U(sqrt(8)/2,+inf)

? limit(sin(x)/x,x)
thinking...
=> 1

? limit((x^2 - 1)/(x-1),x,1)
thinking...
=> 2

? dif(y,x)=sqrt(4-y^2)
thinking...
(-arcsin((y/2))+x+c1)=0
=> (-arcsin((y/2))+x+c1)=0

? dif(y,x)+y=1
thinking...
(log(abs((1-y)))+x+c1)=0
=> (log(abs((1-y)))+x+c1)=0

? x^5*dif(y,x)=-y^5
thinking...
((4*(x^4)*(y^4)*c1)+(x^4)+(y^4))=0
=> ((4*(x^4)*(y^4)*c1)+(x^4)+(y^4))=0

? dif(y,x)=(1+x^2)*(1+y^2)
thinking...
((3*x)+(3*c1)-(3*arctan(y))+(x^3))=0
=> ((3*x)+(3*c1)-(3*arctan(y))+(x^3))=0

? x*(x^2-1)*dif(y,x)=1
thinking...
(integrate((1/((-1+x)*(1+x)*x)),x)-y+c1)=0
(integrate(((-1/(2*(-1+x)))+(-1/(2*(1+x)))+(1/x)),x)-y+c1)=0
((-log(abs((-1+x)))/2)+(-log(abs((1+x)))/2)+log(abs(x))-y+c1)=0
=> ((4*log(abs(x)))+(4*c1)-(2*log(abs((-1+x))))-(2*log(abs((1+x))))-(4*y))=0

? (x^2+x*y)*dif(y,x)=(x^2+y^2)
thinking...
try(subs((integrate(((1+z)/(-1+z)),z)+log(abs(x))+c1),z,(y/x)))=0
try(subs((integrate(((1/(-1+z))+(z/(-1+z))),z)+log(abs(x))+c1),z,(y/x)))=0
try(subs((integrate((z/(-1+z)),z)+log(abs((-1+z)))+log(abs(x))+c1),z,(y/x)))=0
try(subs((integrate(((-1+(z^2))/((-1+z)^2)),z)+log(abs(x))+c1),z,(y/x)))=0
try(subs((integrate(((1/(-1+z))+(z/(-1+z))),z)+log(abs(x))+c1),z,(y/x)))=0
try(subs((log(abs((-1+z)))+log(abs(x))+try(subs(integrate(((-1+(-1/a))/a),a),a,(1/(-1+z))),subs(integrate(((1+a)/a),a),a,(-1+z)))+c1),z,(y/x)))=0
try(subs((log(abs((-1+z)))+log(abs(x))+try(subs(((-log(abs((a^2)))/2)-integrate((1/(a^2)),a)),a,(1/(-1+z))),subs(integrate(((1+a)/a),a),a,(-1+z)))+c1),z,(y/x)))=0
try(subs((log(abs((-1+z)))+log(abs(x))+try(subs(((1/a)+(-log(abs((a^2)))/2)),a,(1/(-1+z))),subs(integrate(((1+a)/a),a),a,(-1+z)))+c1),z,(y/x)))=0
=> ((2*log(abs((-1+(y/x))))*x)+(2*log(abs(x))*x)+(2*x*c1)+(2*y)-(2*x)-(log(abs((1/((-1+(y/x))^2))))*x))=0

? dif(y,x)=(x+y)/x
thinking...
try(subs((log(abs(x))-z+c1),z,(y/x)))=0
=> ((log(abs(x))*x)+(x*c1)-y)=0

? (x-y)*dif(y,x)-(x+y)=0
thinking...
try(subs(((log(abs((-1-(z^2))))/2)+log(abs(x))-arctan(z)+c1),z,(y/x)))=0
=> (log(abs((-1+(-(y^2)/(x^2)))))+(2*log(abs(x)))+(2*c1)-(2*arctan((y/x))))=0

? (x^2-y^2)+2*x*y*dif(y,x)=0
thinking...
try(subs((((2*c1)-log(abs((1+(z^2))))-log(abs(x)))/2),z,(y/x)))=0
=> ((2*c1)-log(abs((1+((y^2)/(x^2)))))-log(abs(x)))=0

? x*dif(y,x)-y+x*sin(y/x)=0
thinking...
try(subs((-log(abs(tan((z/2))))-log(abs(x))+c1),z,(y/x)))=0
=> (-log(abs((sin((y/(2*x)))/cos((y/(2*x))))))-log(abs(x))+c1)=0

? (a+b)^2 = a^2 + b^2 + 2*a*b
thinking...
(-(2*a*b)-(a^2)-(b^2)+((a+b)^2))=0
0=0
true
=> true

? (x-1)*(x+1) = x^2 - 1
thinking...
(1+((-1+x)*(1+x))-(x^2))=0
0=0
true
=> true

? integrate((7^(7^(7^x)))*(7^(7^x))*(7^x),x)
thinking...
integrate((7^((7^(7^x))+(7^x)+x)),x)
subs(integrate((1/((7^-y)*(log(7)^2))),y),y,(7^(7^x)))
subs((1/((7^-y)*(log(7)^3))),y,(7^(7^x)))
=> 1/((7^-(7^(7^x)))*(log(7)^3))