== You are given a number of syntactically incorrect formulas. == Your job is to make them syntactically correct by inserting parentheses == (no other visible symbols are permitted) == in such a way that the formulas become not only syntactically correct == but also are accepted by the Mizar checker (without any errors). == That is, all formulas you obtain should be tautologies. environ given a being PERSON; == If you wish, you may understand the abbreviations as follows: == K[a] a is a knight == N[a] a is a knave == S[a] a is short == T[a] a is tall == H[a] a is handsome == You should understand however that the above suggestion is == completely immaterial since tautologies are independent of the == interpretation. begin == Example. For the syntactically incorrect 1: K[a] implies T[a] & T[a] implies H[a] & K[a] implies H[a]; == the solution can be: 1: ((K[a] implies T[a]) & (T[a] implies H[a]) & K[a]) implies H[a]; == End of example 1: K[a] implies S[a] iff S[a] or not K[a]; 2: K[a] implies T[a] implies T[a] implies H[a] implies K[a] implies H[a]; 3: K[a] implies T[a] & T[a] implies H[a] implies K[a] implies H[a]; 4: K[a] implies T[a] implies K[a] implies K[a]; 5: K[a] implies S[a] & N[a] implies T[a] implies K[a] & N[a] implies S[a] & T[a]; 6: K[a] implies S[a] & N[a] implies T[a] & K[a] or N[a] implies S[a] or T[a]; 7: K[a] implies S[a] & N[a] implies T[a] & K[a] or N[a] & not S[a] implies T[a]; 8: K[a] implies S[a] & S[a] implies K[a] iff K[a] iff S[a]; 9: K[a] & S[a] or not S[a] & not K[a] iff K[a] iff S[a];