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