\settings {
"#Proof-Settings-Config-File
#Thu May 18 17:52:55 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\:transactionsOn-transactions\:transactionsOff , 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
"
}

\sorts {
	s;
}

\functions {
        s f(s);
        s a;
}

\problem {
\forall s x;  f(f(x)) = f(x) -> f(a) = f(f(f(a)))

}

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

(branch "dummy ID"
(rule "eqSymm" (formula "1") (term "1"))
(rule "impRight" (formula "1"))
(rule "allLeft" (formula "1") (inst "_NAME_MV_t=X_0"))
(rule "applyEq" (formula "3") (term "0,0") (ifseqformula "1"))
(rule "close" (formula "3") (ifseqformula "1"))
)

}