Platform claims not to support CPU time, falling back to wall time.
proof of /home/fs5/ayamada/tpdb/relative/Relative_05/rt1-3.trs
# AProVE Commit ID: 2b684c7cda508b1711f707cb42f127e64fe1df88 ffrohn 20140415 dirty


Termination of the given RelTRS could be proven:

(0) RelTRS
(1) RelTRStoQDPProof [SOUND, 0 ms]
(2) QDP
(3) DependencyGraphProof [EQUIVALENT, 0 ms]
(4) TRUE


----------------------------------------

(0)
Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:

   t(f(x), g(y), f(z)) -> t(z, g(x), g(y))
   t(g(x), g(y), f(z)) -> t(f(y), f(z), x)

The relative TRS consists of the following S rules:

   f(g(x)) -> g(f(x))
   g(f(x)) -> f(g(x))
   f(f(x)) -> g(g(x))
   g(g(x)) -> f(f(x))


----------------------------------------

(1) RelTRStoQDPProof (SOUND)
The relative termination problem is root-restricted. We can therefore treat it as a dependency pair problem.
----------------------------------------

(2)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   t(f(x), g(y), f(z)) -> t(z, g(x), g(y))
   t(g(x), g(y), f(z)) -> t(f(y), f(z), x)

The TRS R consists of the following rules:

   f(g(x)) -> g(f(x))
   g(f(x)) -> f(g(x))
   f(f(x)) -> g(g(x))
   g(g(x)) -> f(f(x))

Q is empty.
We have to consider all (P,Q,R)-chains.
----------------------------------------

(3) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
----------------------------------------

(4)
TRUE