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


Termination of the given RelTRS could be disproven:

(0) RelTRS
(1) RelTRSLoopFinderProof [COMPLETE, 94 ms]
(2) NO


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

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

   min(x, 0) -> 0
   min(0, y) -> 0
   min(s(x), s(y)) -> s(min(x, y))
   max(x, 0) -> x
   max(0, y) -> y
   max(s(x), s(y)) -> s(max(x, y))
   -(x, 0) -> x
   -(s(x), s(y)) -> -(x, y)
   gcd(nil) -> 0
   gcd(cons(x, nil)) -> x
   gcd(cons(0, y)) -> gcd(y)
   gcd(cons(x, cons(y, z))) -> gcd(cons(-(x, y), cons(y, z)))

The relative TRS consists of the following S rules:

   gcd(cons(x, cons(y, z))) -> gcd(cons(max(x, y), cons(min(x, y), z)))


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

(1) RelTRSLoopFinderProof (COMPLETE)
The following loop was found:

---------- Loop: ----------

gcd(cons(x, cons(y, z))) -> gcd(cons(-(x, y), cons(y, z))) with rule gcd(cons(x', cons(y', z))) -> gcd(cons(-(x', y'), cons(y', z))) at position [] and matcher [x' / x, y' / y]

Now an instance of the first term with Matcher [x / -(x, y)] occurs in the last term at position [].

Context: []

Therefore, the relative TRS problem does not terminate.
----------------------------------------

(2)
NO