162.60/29.79	MAYBE
162.60/29.79	(UNSUPPORTED)
162.60/29.79	ConCon could not decide confluence of the system.
162.60/29.79	\cite{ALS94}, Theorem 4.1 does not apply.
162.60/29.79	This system is of type 3 or smaller.
162.60/29.79	This system is absolutely deterministic.
162.60/29.79	The external tool could not decide termination of the system.
162.60/29.79	Call external tool:
162.60/29.79	./ttt2.sh
162.60/29.79	Input:
162.60/29.79	(VAR x t store pid n h m)
162.60/29.79	(RULES
162.60/29.79	  fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
162.60/29.79	  map_f(pid, nil) -> nil
162.60/29.79	  leq(s(n), s(m)) -> leq(n, m)
162.60/29.79	  app(cons(h, t), x) -> cons(h, app(t, x))
162.60/29.79	  sndsplit(s(n), nil) -> nil
162.60/29.79	  process(store, m) -> U1(leq(m, length(store)), store, m)
162.60/29.79	  U1(false, store, m) -> U3(empty(fstsplit(m, app(map_f(self, nil), store))), store, m)
162.60/29.79	  U3(false, store, m) -> process(sndsplit(m, app(map_f(self, nil), store)), m)
162.60/29.79	  fstsplit(s(n), nil) -> nil
162.60/29.79	  sndsplit(0, x) -> x
162.60/29.79	  empty(nil) -> true
162.60/29.79	  length(cons(h, t)) -> s(length(t))
162.60/29.79	  process(store, m) -> U1(leq(m, length(store)), store, m)
162.60/29.79	  U1(true, store, m) -> U2(empty(fstsplit(m, store)), store, m)
162.60/29.79	  U2(false, store, m) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
162.60/29.79	  leq(0, m) -> true
162.60/29.79	  map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
162.60/29.79	  empty(cons(h, t)) -> false
162.60/29.79	  fstsplit(0, x) -> nil
162.60/29.79	  app(nil, x) -> x
162.60/29.79	  sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
162.60/29.79	  leq(s(n), 0) -> false
162.60/29.79	  length(nil) -> 0
162.60/29.79	)
162.60/29.79	
162.60/29.79	EOF