Evaluate whether a propositional formula is a tautology. The method is already sketched in Hilbert/Ackermann 1928 "Grundzuge der theoretischen Logik". This is an implementation on the AVR butterfly (and thus at 67 mm x 45 mm x 10 mm the smallest implementation of a theorem prover on a gadget known to me). We do a three-pass evaluation: First pass (parseary2, parseary1, parseatom) is a top-down parse by recursive descent. Second pass (shuffletree) is a depth-first substition to create a (relaxed) CNF. (The CNF is relaxed in that double negations are allowed which is easily handled by the third pass.) Third pass (tautology) is a traversal to check whether all clauses are tautologies. Usage: 1) Starting the butterfly: quickly toggle the joystick up. This starts the device and you will now have entered the data entry stage. The display shows "P0VN". 2) Entering data: "P0VN" stands for "Position 0 Value N(ot)". Press 'up'/'down' to swap the values of the letter, press 'left'/'right' to move back/forth (e.g. right will move you to position 1 and initially show "P1VN"). When you move back again you will see what you had entered in position 0. 3) Syntax for formulas: B,C,D,E,F,G,H,I,J,K,L,M,P,Q,R,S,T,U,V,W,X,Y,Z are used as symbols for propositions, A for binary 'and', O for binary 'or', N for unary 'not'. The formula is to be given in Polish notation, e.g. "A->A" is "not A or A" which is "ONAA", hence entered as "P0V0", "P1VN", "P2VA", "P3VA". By the encoding in Polish notation and fixed arities of N/A/O no brackets are needed and the length of a formula is determined by reading starting at the first position (no sign for the end of a formula is needed). Hence in the "A->A" example the value of P4 is irrelevant and will not be evaluated. 4) Checking for tautologies: Press 'enter' (press the joystick down) to load the word into the prover. The last 5 symbols of the formula are displayed, followed by '1' for tautology, or '0' for no tautology. For example, as "A->A" is a tautology, it will show up as "ONAA1". The LED and button functionality reuses released STK 500 code by Atmel Norway with modifications by Martin Thomas. The AVR butterfly board had been obtained in elmicro.de's Munich branch. Soldering support by Christoph Wunder is thanked for.