0.00/0.00 YES 0.00/0.00 0.00/0.00 0.00/0.00 Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.trs". 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x n t h m pid store) 0.00/0.00 (RULES 0.00/0.00 fstsplit(0,x) -> nil 0.00/0.00 fstsplit(s(n),nil) -> nil 0.00/0.00 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.00 sndsplit(0,x) -> x 0.00/0.00 sndsplit(s(n),nil) -> nil 0.00/0.00 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.00 empty(nil) -> true 0.00/0.00 empty(cons(h,t)) -> false 0.00/0.00 leq(0,m) -> true 0.00/0.00 leq(s(n),0) -> false 0.00/0.00 leq(s(n),s(m)) -> leq(n,m) 0.00/0.00 length(nil) -> 0 0.00/0.00 length(cons(h,t)) -> s(length(t)) 0.00/0.00 app(nil,x) -> x 0.00/0.00 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.00 map_f(pid,nil) -> nil 0.00/0.00 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.00 process(store,m) -> process(app(map_f(self,nil),sndsplit(m,store)),m) | leq(m,length(store)) == true, empty(fstsplit(m,store)) == false 0.00/0.00 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.00/0.00 ) 0.00/0.00 (COMMENT doi:10.1007/s002000100063 [50] p. 42-43 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 No "->="-rules. 0.00/0.00 0.00/0.00 Decomposed conditions if possible. 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x n t h m pid store) 0.00/0.00 (RULES 0.00/0.00 fstsplit(0,x) -> nil 0.00/0.00 fstsplit(s(n),nil) -> nil 0.00/0.00 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.00 sndsplit(0,x) -> x 0.00/0.00 sndsplit(s(n),nil) -> nil 0.00/0.00 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.00 empty(nil) -> true 0.00/0.00 empty(cons(h,t)) -> false 0.00/0.00 leq(0,m) -> true 0.00/0.00 leq(s(n),0) -> false 0.00/0.00 leq(s(n),s(m)) -> leq(n,m) 0.00/0.00 length(nil) -> 0 0.00/0.00 length(cons(h,t)) -> s(length(t)) 0.00/0.00 app(nil,x) -> x 0.00/0.00 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.00 map_f(pid,nil) -> nil 0.00/0.00 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.00 process(store,m) -> process(app(map_f(self,nil),sndsplit(m,store)),m) | leq(m,length(store)) == true, empty(fstsplit(m,store)) == false 0.00/0.00 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.00/0.00 ) 0.00/0.00 (COMMENT doi:10.1007/s002000100063 [50] p. 42-43 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 Removed infeasible rules as much as possible. 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x n t h m pid store) 0.00/0.00 (RULES 0.00/0.00 fstsplit(0,x) -> nil 0.00/0.00 fstsplit(s(n),nil) -> nil 0.00/0.00 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.00 sndsplit(0,x) -> x 0.00/0.00 sndsplit(s(n),nil) -> nil 0.00/0.00 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.00 empty(nil) -> true 0.00/0.00 empty(cons(h,t)) -> false 0.00/0.00 leq(0,m) -> true 0.00/0.00 leq(s(n),0) -> false 0.00/0.00 leq(s(n),s(m)) -> leq(n,m) 0.00/0.00 length(nil) -> 0 0.00/0.00 length(cons(h,t)) -> s(length(t)) 0.00/0.00 app(nil,x) -> x 0.00/0.00 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.00 map_f(pid,nil) -> nil 0.00/0.00 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.00 process(store,m) -> process(app(map_f(self,nil),sndsplit(m,store)),m) | leq(m,length(store)) == true, empty(fstsplit(m,store)) == false 0.00/0.00 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.00/0.00 ) 0.00/0.00 (COMMENT doi:10.1007/s002000100063 [50] p. 42-43 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 Try to disprove confluence of the following (C)TRS: 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x n t h m pid store) 0.00/0.00 (RULES 0.00/0.00 fstsplit(0,x) -> nil 0.00/0.00 fstsplit(s(n),nil) -> nil 0.00/0.00 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.00 sndsplit(0,x) -> x 0.00/0.00 sndsplit(s(n),nil) -> nil 0.00/0.00 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.00 empty(nil) -> true 0.00/0.00 empty(cons(h,t)) -> false 0.00/0.00 leq(0,m) -> true 0.00/0.00 leq(s(n),0) -> false 0.00/0.00 leq(s(n),s(m)) -> leq(n,m) 0.00/0.00 length(nil) -> 0 0.00/0.00 length(cons(h,t)) -> s(length(t)) 0.00/0.00 app(nil,x) -> x 0.00/0.00 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.00 map_f(pid,nil) -> nil 0.00/0.00 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.00 process(store,m) -> process(app(map_f(self,nil),sndsplit(m,store)),m) | leq(m,length(store)) == true, empty(fstsplit(m,store)) == false 0.00/0.00 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.00/0.00 ) 0.00/0.00 (COMMENT doi:10.1007/s002000100063 [50] p. 42-43 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs. 0.00/0.00 0.00/0.00 Try to apply SR and U for 3DCTRSs to the above CTRS. 0.00/0.00 0.00/0.00 Succeeded in applying U for 3DCTRSs to the above CTRS. 0.00/0.00 U(R) = 0.00/0.00 (VAR x1 x3 x2) 0.00/0.00 (RULES 0.00/0.00 fstsplit(0,x1) -> nil 0.00/0.00 fstsplit(s(x1),nil) -> nil 0.00/0.00 fstsplit(s(x1),cons(x2,x3)) -> cons(x2,fstsplit(x1,x3)) 0.00/0.00 sndsplit(0,x1) -> x1 0.00/0.00 sndsplit(s(x1),nil) -> nil 0.00/0.00 sndsplit(s(x1),cons(x2,x3)) -> sndsplit(x1,x3) 0.00/0.00 empty(nil) -> true 0.00/0.00 empty(cons(x1,x2)) -> false 0.00/0.00 leq(0,x1) -> true 0.00/0.00 leq(s(x1),0) -> false 0.00/0.00 leq(s(x1),s(x2)) -> leq(x1,x2) 0.00/0.00 length(nil) -> 0 0.00/0.00 length(cons(x1,x2)) -> s(length(x2)) 0.00/0.00 app(nil,x1) -> x1 0.00/0.00 app(cons(x1,x2),x3) -> cons(x1,app(x2,x3)) 0.00/0.00 map_f(x1,nil) -> nil 0.00/0.00 map_f(x1,cons(x2,x3)) -> app(f(x1,x2),map_f(x1,x3)) 0.00/0.00 process(x1,x2) -> u1(leq(x2,length(x1)),x1,x2) 0.00/0.00 u1(true,x1,x2) -> u3(empty(fstsplit(x2,x1)),x1,x2) 0.00/0.00 u3(false,x1,x2) -> process(app(map_f(self,nil),sndsplit(x2,x1)),x2) 0.00/0.00 u1(false,x1,x2) -> u2(empty(fstsplit(x2,app(map_f(self,nil),x1))),x1,x2) 0.00/0.00 u2(false,x1,x2) -> process(sndsplit(x2,app(map_f(self,nil),x1)),x2) 0.00/0.00 ) 0.00/0.00 0.00/0.00 U for 3DCTRSs is sound for the above CTRS. 0.00/0.00 0.00/0.00 U(R) is confluent. 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF