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.