\settings {
"#Proof-Settings-Config-File
#Mon Apr 17 13:56:57 CEST 2006
[General]SoundNotification=true
[View]FontIndex=2
[SimultaneousUpdateSimplifier]DeleteEffectLessLocations=true
[General]SuggestiveVarNames=false
[View]ShowWholeTaclet=true
[General]ProofAssistant=true
[View]MaxTooltipLines=0
[SimultaneousUpdateSimplifier]EagerSimplification=false
[General]StupidMode=true
[Strategy]MaximumNumberOfAutomaticApplications=1000
[Libraries]Default=stringRules.key-false, deprecatedRules.key-false
[Choice]DefaultChoices=transactions-transactions\:transactionsOn , programRules-programRules\:Java , initialisation-initialisation\:disableStaticInitialisation , transactionAbort-transactionAbort\:abortOn , throughout-throughout\:toutOn , intRules-intRules\:javaSemantics , nullPointerPolicy-nullPointerPolicy\:nullCheck
[OCLRef]Null=false
[OCLRef]ExcThrown=false
[Model]Source=1
[Choice]Choices=transactions-transactions\:transactionsOff-transactions\:transactionsOn , programRules-programRules\:ODL-programRules\:Java , throughout-throughout\:toutOff-throughout\:toutOn , initialisation-initialisation\:disableStaticInitialisation-initialisation\:enableStaticInitialisation , transactionAbort-transactionAbort\:abortOff-transactionAbort\:abortOn , intRules-intRules\:arithmeticSemanticsCheckingOF-intRules\:javaSemantics-intRules\:arithmeticSemanticsIgnoringOF , nullPointerPolicy-nullPointerPolicy\:noNullCheck-nullPointerPolicy\:nullCheck
[OCLRef]Array=false
[DecisionProcedure]=SIMPLIFY
[General]OuterRenaming=true
[Strategy]ActiveStrategy=Simple JavaCardDL
"
}

\predicates {
        p;
        q;
}
\problem {
p & q -> q & p

}

\proof {
(keyLog "0" (keyUser "ahrendt" ) (keyVersion "0.2041"))

(branch "dummy ID"
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andRight" (formula "3"))
(branch " Case 1"
   (rule "close" (formula "3") (ifseqformula "2"))
)
(branch " Case 2"
   (rule "close" (formula "3") (ifseqformula "1"))
)
)

}