# This system cannot be solved with the methods available to Reduce [closed]

I get the error message in the Title, which is not very helpful. Situation:

Reduce[ForAll[{x,y,z},Implies[x<=y&&y<=z, x<=z]]]


evaluates to True, but

Reduce[ForAll[{x,y,z,w},Implies[ x>=0&&y>=0&&z>=0&&w>=0&&x+y<= z+w,xyw>=wwz]]]


gives "This system cannot be solved with the methods available to Reduce". Any explanation?

Put spaces or * between your variables xyz and wwz to give:
Reduce[ForAll[{x, y, z, w},

• Duh... okay if I may be permitted to make the question slightly more interesting, I get the same problem with Reduce[ForAll[{x010,x011,x100,x101,x111},Implies[ x001+x101 <=x010+x110&&x010+x110<=x100+x101 && x010>=0&&x011>=0&&x100>=0&&x101>=0&&x111>=0,x010^2 x100>=0]]] – Bjørn Kjos-Hanssen May 25 at 17:34
• For that problem you missed some variables in your ForAll. Try Reduce[ForAll[{x000, x001, x010, x011, x100, x101, x110, x111}, Implies[x001 + x101 <= x010 + x110 && x010 + x110 <= x100 + x101 && x010 >= 0 && x011 >= 0 && x100 >= 0 && x101 >= 0 && x111 >= 0, x010^2 x100 >= 0]]] I get result True – flinty May 25 at 17:37
• @Bjørn, I would interpret it more as Reduce[] not knowing what to do when you suddenly added the new variables xyw and wwz which it was not previously told about. ;) – J. M.'s technical difficulties May 25 at 18:01
• You could create a check function to spot any mistakes check[expr_, vars_] := Block[{b = Complement[Variables[Level[expr, {-1}]], variables]}, If[b != {}, Print["There are bad variables in your expression: " <> ToString[b]]]] – flinty May 25 at 18:09