0.77/0.88	YES
0.77/0.88	(ignored inputs)COMMENT doi:10.1007/s002000100063 [50] p. 42-43 submitted by: Thomas Sternagel and Aart Middeldorp
0.77/0.88	Conditional Rewrite Rules:
0.77/0.88	   [ fstsplit(0,?x) -> nil,
0.77/0.88	     fstsplit(s(?n),nil) -> nil,
0.77/0.88	     fstsplit(s(?n),cons(?h,?t)) -> cons(?h,fstsplit(?n,?t)),
0.77/0.88	     sndsplit(0,?x) -> ?x,
0.77/0.88	     sndsplit(s(?n),nil) -> nil,
0.77/0.88	     sndsplit(s(?n),cons(?h,?t)) -> sndsplit(?n,?t),
0.77/0.88	     empty(nil) -> true,
0.77/0.88	     empty(cons(?h,?t)) -> false,
0.77/0.88	     leq(0,?m) -> true,
0.77/0.88	     leq(s(?n),0) -> false,
0.77/0.88	     leq(s(?n),s(?m)) -> leq(?n,?m),
0.77/0.88	     length(nil) -> 0,
0.77/0.88	     length(cons(?h,?t)) -> s(length(?t)),
0.77/0.88	     app(nil,?x) -> ?x,
0.77/0.88	     app(cons(?h,?t),?x) -> cons(?h,app(?t,?x)),
0.77/0.88	     map_f(?pid,nil) -> nil,
0.77/0.88	     map_f(?pid,cons(?h,?t)) -> app(f(?pid,?h),map_f(?pid,?t)),
0.77/0.88	     process(?store,?m) -> process(app(map_f(self,nil),sndsplit(?m,?store)),?m) | leq(?m,length(?store)) == true,empty(fstsplit(?m,?store)) == false,
0.77/0.88	     process(?store,?m) -> process(sndsplit(?m,app(map_f(self,nil),?store)),?m) | leq(?m,length(?store)) == false,empty(fstsplit(?m,app(map_f(self,nil),?store))) == false ]
0.77/0.88	Check whether all rules are type 3
0.77/0.88	OK
0.77/0.88	Check whether the input is deterministic
0.77/0.88	OK
0.77/0.88	Result of unraveling:
0.77/0.88	   [ fstsplit(0,?x) -> nil,
0.77/0.88	     fstsplit(s(?n),nil) -> nil,
0.77/0.88	     fstsplit(s(?n),cons(?h,?t)) -> cons(?h,fstsplit(?n,?t)),
0.77/0.88	     sndsplit(0,?x) -> ?x,
0.77/0.88	     sndsplit(s(?n),nil) -> nil,
0.77/0.88	     sndsplit(s(?n),cons(?h,?t)) -> sndsplit(?n,?t),
0.77/0.88	     empty(nil) -> true,
0.77/0.88	     empty(cons(?h,?t)) -> false,
0.77/0.88	     leq(0,?m) -> true,
0.77/0.88	     leq(s(?n),0) -> false,
0.77/0.88	     leq(s(?n),s(?m)) -> leq(?n,?m),
0.77/0.88	     length(nil) -> 0,
0.77/0.88	     length(cons(?h,?t)) -> s(length(?t)),
0.77/0.88	     app(nil,?x) -> ?x,
0.77/0.88	     app(cons(?h,?t),?x) -> cons(?h,app(?t,?x)),
0.77/0.88	     map_f(?pid,nil) -> nil,
0.77/0.88	     map_f(?pid,cons(?h,?t)) -> app(f(?pid,?h),map_f(?pid,?t)),
0.77/0.88	     process(?store,?m) -> U2(leq(?m,length(?store)),?m,?store),
0.77/0.88	     U2(true,?m,?store) -> U1(empty(fstsplit(?m,?store)),?m,?store),
0.77/0.88	     U1(false,?m,?store) -> process(app(map_f(self,nil),sndsplit(?m,?store)),?m),
0.77/0.88	     U2(false,?m,?store) -> U3(empty(fstsplit(?m,app(map_f(self,nil),?store))),?m,?store),
0.77/0.88	     U3(false,?m,?store) -> process(sndsplit(?m,app(map_f(self,nil),?store)),?m) ]
0.77/0.88	Check whether U(R) is terminating
0.77/0.88	failed to show termination
0.77/0.88	Check whether the input is weakly left-linear
0.77/0.88	OK
0.77/0.88	Conditional critical pairs (CCPs):
0.77/0.88	   [ process(sndsplit(?m_16,app(map_f(self,nil),?store_16)),?m_16) = process(app(map_f(self,nil),sndsplit(?m_16,?store_16)),?m_16) | leq(?m_16,length(?store_16)) == false,empty(fstsplit(?m_16,app(map_f(self,nil),?store_16))) == false,leq(?m_16,length(?store_16)) == true,empty(fstsplit(?m_16,?store_16)) == false,
0.77/0.88	     process(app(map_f(self,nil),sndsplit(?m_15,?store_15)),?m_15) = process(sndsplit(?m_15,app(map_f(self,nil),?store_15)),?m_15) | leq(?m_15,length(?store_15)) == true,empty(fstsplit(?m_15,?store_15)) == false,leq(?m_15,length(?store_15)) == false,empty(fstsplit(?m_15,app(map_f(self,nil),?store_15))) == false ]
0.77/0.88	Check whether the input is almost orthogonale
0.77/0.88	not almost orthogonal
0.77/0.88	OK
0.77/0.88	Check U(R) is confluent
0.77/0.88	Rewrite Rules:
0.77/0.88	   [ fstsplit(0,?x) -> nil,
0.77/0.88	     fstsplit(s(?n),nil) -> nil,
0.77/0.88	     fstsplit(s(?n),cons(?h,?t)) -> cons(?h,fstsplit(?n,?t)),
0.77/0.88	     sndsplit(0,?x) -> ?x,
0.77/0.88	     sndsplit(s(?n),nil) -> nil,
0.77/0.88	     sndsplit(s(?n),cons(?h,?t)) -> sndsplit(?n,?t),
0.77/0.88	     empty(nil) -> true,
0.77/0.88	     empty(cons(?h,?t)) -> false,
0.77/0.88	     leq(0,?m) -> true,
0.77/0.88	     leq(s(?n),0) -> false,
0.77/0.88	     leq(s(?n),s(?m)) -> leq(?n,?m),
0.77/0.88	     length(nil) -> 0,
0.77/0.88	     length(cons(?h,?t)) -> s(length(?t)),
0.77/0.88	     app(nil,?x) -> ?x,
0.77/0.88	     app(cons(?h,?t),?x) -> cons(?h,app(?t,?x)),
0.77/0.88	     map_f(?pid,nil) -> nil,
0.77/0.88	     map_f(?pid,cons(?h,?t)) -> app(f(?pid,?h),map_f(?pid,?t)),
0.77/0.88	     process(?store,?m) -> U2(leq(?m,length(?store)),?m,?store),
0.77/0.88	     U2(true,?m,?store) -> U1(empty(fstsplit(?m,?store)),?m,?store),
0.77/0.88	     U1(false,?m,?store) -> process(app(map_f(self,nil),sndsplit(?m,?store)),?m),
0.77/0.88	     U2(false,?m,?store) -> U3(empty(fstsplit(?m,app(map_f(self,nil),?store))),?m,?store),
0.77/0.88	     U3(false,?m,?store) -> process(sndsplit(?m,app(map_f(self,nil),?store)),?m) ]
0.77/0.88	Apply Direct Methods...
0.77/0.88	Inner CPs:
0.77/0.88	   [  ]
0.77/0.88	Outer CPs:
0.77/0.88	   [  ]
0.77/0.88	Overlay, check Innermost Termination...
0.77/0.88	unknown Innermost Terminating
0.77/0.88	unknown Knuth & Bendix
0.77/0.88	Left-Linear, not Right-Linear
0.77/0.88	Development Closed
0.77/0.88	Direct Methods: CR
0.77/0.88	
0.77/0.88	Combined result: CR
0.77/0.88	U(R) is confluent
0.77/0.88	R is deterministic, weakly left-linear and U(R) is confluent
0.77/0.88	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.77/0.88	(700 msec.)
0.77/0.88	EOF