Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Problem 10.3
Als Ausgabe gibt diese Webseite ja ein detailliertes Log zurück.
Wenn man das Problem in FOF formuliert und den Solver damit gefüttert hat, was kann man dann als Ausgabe erwarten?
Ist die Zeile
im Log das Ergebnis oder kann man auch sehen, wo er das Gold/Wumpus/Grube gefunden hat?
Urprünglich war die Aufgabe so formuliert dass man das aus dem log hätte ablesen sollen; leider hat sich das als unrealistisch herausgestellt (die prover ersetzen alles durch skolem-konstanten -.-).
Der Rest hängt leider davon ab, wie dein konkreter Input aussieht - aber „Proof found!“ klingt ja schonmal gut 
Wenn du nur Axiome hast:
proof found = nicht erfuellbar
no proof found = erfuellbar
Wenn du ne Conjecture hast:
proof found = sie folgt aus deinen Axiomen
no proof found = sie folgt nicht (“nicht unbedingt”) aus deinen Axiomen
1 „Gefällt mir“
# Failure: Resource limit exceeded (time)
# SZS status ResourceOut
eprover: CPU time limit exceeded, terminatingÄh, was kann ich dagegen tun? Ich mache meiner Meinung nach nichts Besonderes/Schlimmes, eigentlich nur was halt notwendig ist.
öhm… wow… keine ahnung, ist mir nicht passiert… 
Sicher dass deine situation nicht unterspezifiziert ist?
Wenn ich E2.0 mit einer conjecture laufen lass, sagt es mir no proof found, wenn ich E2.0 mit der conjecture als axiom laufen lass, sagt es mir auch no proof found?
Wenn ich Metis2.3 mit derselben conjecture laufen lass, findet es den proof für die conjecture?
Scheint als wäre Metis dann wohl ein wenig mächtiger in der spezifischen Situation… oder hattest du die selbe Conjecture auch noch als Axiom mit drin?