Output of Waldmeister Run
Generated Specification
NAME WWW-Specification
MODE PROOF
SORTS S
SIGNATURE A: S -> S
F: S -> S
G: S -> S
e: S S -> S # guessed
sk: S S -> S # guessed
f: S S -> S # guessed
i: S S -> S # guessed
ORDERING LPO
i > f > e > sk
VARIABLES x : S
EQUATIONS A(A(x))=A(x)
A(F(A(F(x))))=A(F(x))
G(A(F(G(x))))=A(F(G(x)))
G(A(F(A(G(x)))))=A(F(A(G(x))))
CONCLUSION A(F(G(A(F(G(x))))))=A(F(A(G(A(F(A(G(x))))))))
Start of Waldmeister
changed to KBO
********************************************************************************
* W A L D M E I S T E R \| \ / \|/ *
* |/ | \/ | *
* (C) 1994-2009 A. Buch and Th. Hillenbrand, \ / \ / *
* A. Jaeger and B. Loechner | | *
* <waldmeister@informatik.uni-kl.de> | *
********************************************************************************
Initial equations:
------------------
( 1) A(x1) = A(A(x1))
( 2) A(F(x1)) = A(F(A(F(x1))))
( 3) A(F(A(G(x1)))) = G(A(F(A(G(x1)))))
( 4) A(F(G(x1))) = G(A(F(G(x1))))
( 5) eq(x1,x1) = true
( 6) eq(A(F(A(G(A(F(A(G(x1)))))))),A(F(G(A(F(G(x1))))))) = false
Goals:
------
( 1) true ?= false
using narrowing to prove A(F(A(G(A(F(A(G(x1)))))))) ?= A(F(G(A(F(G(x1))))))
Detected structure: Orkus
********************************************************************************
****************************** COMPLETION - PROOF ******************************
********************************************************************************
new rule: 1 A(A(x1)) -> A(x1)
new rule: 2 A(F(A(F(x1)))) -> A(F(x1))
new rule: 3 G(A(F(A(G(x1))))) -> A(F(A(G(x1))))
new rule: 4 G(A(F(G(x1)))) -> A(F(G(x1)))
new rule: 5 eq(x1,x1) -> true
new rule: 6 A(F(A(G(x1)))) ? A(F(G(x1)))
new rule: 7 true -> false
simplify goal: 1 false =? false
joined goal: 1 A(F(A(G(A(F(A(G(x1)))))))) ?= A(F(G(A(F(G(x1)))))) to false
+--------------------------+
| this proves the goal |
+--------------------------+
Proved Goals:
No. 1: true ?= false, current false ?= false
using narrowing to prove A(F(A(G(A(F(A(G(x1)))))))) ?= A(F(G(A(F(G(x1))))))
1 goal was specified, which was proved.
Waldmeister states: Goal proved.
Statistics:
-----------
Rules 7
Equations 0
Critical pairs 17
Process size 8659000
Search time [s] 0.0
Proof
Calling proof presentation program...
********************************************************************************
* P R O O F *
* *
* (C) 1992 by Stephan Schulz <schulz@informatik.tu-muenchen.de> *
********************************************************************************
Consider the following set of axioms:
Axiom 1: A(X1) = A(A(X1))
Axiom 2: A(F(X1)) = A(F(A(F(X1))))
Axiom 3: A(F(A(G(X1)))) = G(A(F(A(G(X1)))))
Axiom 4: A(F(G(X1))) = G(A(F(G(X1))))
Axiom 5: eq(X1,X1) = true
Axiom 6: eq(A(F(A(G(A(F(A(G(X1)))))))),A(F(G(A(F(G(X1))))))) = false
This theorem holds true:
Theorem 1: true = false
Proof:
Lemma 1: eq(A(F(A(G(X1)))),A(F(G(X1)))) = false
eq(A(F(A(G(X1)))),A(F(G(X1))))
= by Axiom 2 LR
eq(A(F(A(G(X1)))),A(F(A(F(G(X1))))))
= by Axiom 4 LR
eq(A(F(A(G(X1)))),A(F(G(A(F(G(X1)))))))
= by Axiom 2 LR
eq(A(F(A(F(A(G(X1)))))),A(F(G(A(F(G(X1)))))))
= by Axiom 1 LR
eq(A(F(A(A(F(A(G(X1))))))),A(F(G(A(F(G(X1)))))))
= by Axiom 3 LR
eq(A(F(A(G(A(F(A(G(X1)))))))),A(F(G(A(F(G(X1)))))))
= by Axiom 6 LR
false
Lemma 2: false = eq(A(F(A(G(X1)))),A(F(A(G(X1)))))
false
= by Lemma 1 RL
eq(A(F(A(G(A(F(A(G(X1)))))))),A(F(G(A(F(A(G(X1))))))))
= by Axiom 3 RL
eq(A(F(A(A(F(A(G(X1))))))),A(F(G(A(F(A(G(X1))))))))
= by Axiom 1 RL
eq(A(F(A(F(A(G(X1)))))),A(F(G(A(F(A(G(X1))))))))
= by Axiom 2 RL
eq(A(F(A(G(X1)))),A(F(G(A(F(A(G(X1))))))))
= by Axiom 3 RL
eq(A(F(A(G(X1)))),A(F(A(F(A(G(X1)))))))
= by Axiom 2 RL
eq(A(F(A(G(X1)))),A(F(A(G(X1)))))
Theorem 1: true = false
true
= by Axiom 5 RL
eq(A(F(A(G(X1)))),A(F(A(G(X1)))))
= by Lemma 2 RL
false
Waldmeister stopped.