z3 -smt2 KnuthAAA.smt
z3 -smt2 KnuthAAE.smt
z3 -smt2 KnuthAEA.smt
z3 -smt2 KnuthAEE.smt
z3 -smt2 KnuthEAA.smt
z3 -smt2 KnuthEAE.smt
z3 -smt2 KnuthEEA.smt
z3 -smt2 KnuthEEE.smt