:bug: simpl_num

[hiwane]

vars(a,b):
F = a-1>=0 && b+4==0 || a-1>=0 && a*b+a^2+3==0 || a-1>0 && b+4>0 && a*b+a^2+3>0 && b+4>0 && (a^2-2*a+1)*b^3+(4*a^2-8*a+4)*b^2+(-12*a^2+24*a-12)*b-48*a^2+96*a-48>=0 && (a+1)*b+2*a+6<0 || a-1>0 && b+4>0 && a*b+a^2+3>0 && b+4<0 || b+4==0 && a-1>0 && b+4>0 && a*b+a^2+3>0 && (a+1)*b+2*a+6<0 || a-1>0 && b+4<0 && a*b+a^2+3<0 && b+4<0 && (a^2-2*a+1)*b^3+(4*a^2-8*a+4)*b^2+(-12*a^2+24*a-12)*b-48*a^2+96*a-48<=0 && (a+1)*b+2*a+6>0 || a-1>0 && b+4<0 && a*b+a^2+3<0 && b+4>0 || b+4==0 && a-1>0 && b+4<0 && a*b+a^2+3<0 && (a+1)*b+2*a+6>0 || a-1>0 && b+4>0 && a*b+a^2+3<0 || a-1>0 && b+4<0 && a*b+a^2+3>0:
G = a*b+a^2+3>=0 && b+4<=0 && a-1>=0 || b<=0 && a^2-3>=0 && b^2-12>=0 && b+4>=0 && a-1>=0 || a*b+a^2+3<=0 && b+4>=0 && a-1>=0:
cad(equiv(F, G));  # true
qe(all([a,b],equiv(F, G)));  # false

[hiwane]

[88,1]       simple:  38: simplFof() step@5: all([b], b^2-12<0 || (b+4!=0 && (b+4<0 || b+2>=0 || (b^2-12<=0 && b+2>=0))) || (b^2-12<=0 && b+4==0) || (b+2<=0 && b+4>=0))
[89,1]       simple:  38: simplFof() step@6: all([b], b^2-12<0 || (b+4!=0 && b+4<0) || (b+2<=0 && b+4>=0))

[hiwane]

F = (b^2-12<0 || (b+4!=0 && (b+4<0 || b+2>=0 || (b^2-12<=0 && b+2>=0))));
G = simplnum(F);
cad(F);  # b+4<0 || b^2-12<0 || b+2>=0
cad(G);  # b+4<0 || b^2-12<0

[hiwane]

F = (b^2-12<0 || (a!=0 && (b+2>=0 || (b^2-12<=0 && b+2>=0))));
cad(F);  # b^2-12<0 || (b+2>=0 && a!=0)
simplnum(F);  # b^2-12<0