rm printlns
first applicative axiom
applicative axiom 3
simplify applicative axiom 3
comment out un-finished applicative axioms