0.00/0.08 MAYBE 0.00/0.08 0.00/0.08 0.00/0.08 Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs". 0.00/0.08 (CONDITIONTYPE ORIENTED) 0.00/0.08 (VAR x n t h m pid st_3 in_3 st_2 in_2 st_1) 0.00/0.08 (RULES 0.00/0.08 fstsplit(0,x) -> nil 0.00/0.08 fstsplit(s(n),nil) -> nil 0.00/0.08 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.08 sndsplit(0,x) -> x 0.00/0.08 sndsplit(s(n),nil) -> nil 0.00/0.08 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.08 empty(nil) -> true 0.00/0.08 empty(cons(h,t)) -> false 0.00/0.08 leq(0,m) -> true 0.00/0.08 leq(s(n),0) -> false 0.00/0.08 leq(s(n),s(m)) -> leq(n,m) 0.00/0.08 length(nil) -> 0 0.00/0.08 length(cons(h,t)) -> s(length(t)) 0.00/0.08 app(nil,x) -> x 0.00/0.08 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.08 map_f(pid,nil) -> nil 0.00/0.08 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.08 head(cons(h,t)) -> h 0.00/0.08 tail(cons(h,t)) -> t 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) | empty(fstsplit(m,st_1)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) | leq(m,length(st_2)) == true, empty(fstsplit(m,st_2)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two,head(in_2)),st_2)),cons(fstsplit(m,app(map_f(two,head(in_2)),st_2)),in_3),st_3,m) | leq(m,length(st_2)) == false, empty(fstsplit(m,app(map_f(two,head(in_2)),st_2))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),st_2,in_3,st_3,m) | empty(map_f(two,head(in_2))) == true 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) | leq(m,length(st_3)) == true, empty(fstsplit(m,st_3)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three,head(in_3)),st_3)),m) | leq(m,length(st_3)) == false, empty(fstsplit(m,app(map_f(three,head(in_3)),st_3))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),st_3,m) | empty(map_f(three,head(in_3))) == true 0.00/0.08 ) 0.00/0.08 (COMMENT doi:10.1007/s002000100063 [50] p. 61 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.08 0.00/0.08 No "->="-rules. 0.00/0.08 0.00/0.08 Decomposed conditions if possible. 0.00/0.08 (CONDITIONTYPE ORIENTED) 0.00/0.08 (VAR x n t h m pid st_3 in_3 st_2 in_2 st_1) 0.00/0.08 (RULES 0.00/0.08 fstsplit(0,x) -> nil 0.00/0.08 fstsplit(s(n),nil) -> nil 0.00/0.08 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.08 sndsplit(0,x) -> x 0.00/0.08 sndsplit(s(n),nil) -> nil 0.00/0.08 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.08 empty(nil) -> true 0.00/0.08 empty(cons(h,t)) -> false 0.00/0.08 leq(0,m) -> true 0.00/0.08 leq(s(n),0) -> false 0.00/0.08 leq(s(n),s(m)) -> leq(n,m) 0.00/0.08 length(nil) -> 0 0.00/0.08 length(cons(h,t)) -> s(length(t)) 0.00/0.08 app(nil,x) -> x 0.00/0.08 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.08 map_f(pid,nil) -> nil 0.00/0.08 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.08 head(cons(h,t)) -> h 0.00/0.08 tail(cons(h,t)) -> t 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) | empty(fstsplit(m,st_1)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) | leq(m,length(st_2)) == true, empty(fstsplit(m,st_2)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two,head(in_2)),st_2)),cons(fstsplit(m,app(map_f(two,head(in_2)),st_2)),in_3),st_3,m) | leq(m,length(st_2)) == false, empty(fstsplit(m,app(map_f(two,head(in_2)),st_2))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),st_2,in_3,st_3,m) | empty(map_f(two,head(in_2))) == true 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) | leq(m,length(st_3)) == true, empty(fstsplit(m,st_3)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three,head(in_3)),st_3)),m) | leq(m,length(st_3)) == false, empty(fstsplit(m,app(map_f(three,head(in_3)),st_3))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),st_3,m) | empty(map_f(three,head(in_3))) == true 0.00/0.08 ) 0.00/0.08 (COMMENT doi:10.1007/s002000100063 [50] p. 61 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.08 0.00/0.08 Removed infeasible rules as much as possible. 0.00/0.08 (CONDITIONTYPE ORIENTED) 0.00/0.08 (VAR x n t h m pid st_3 in_3 st_2 in_2 st_1) 0.00/0.08 (RULES 0.00/0.08 fstsplit(0,x) -> nil 0.00/0.08 fstsplit(s(n),nil) -> nil 0.00/0.08 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.08 sndsplit(0,x) -> x 0.00/0.08 sndsplit(s(n),nil) -> nil 0.00/0.08 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.08 empty(nil) -> true 0.00/0.08 empty(cons(h,t)) -> false 0.00/0.08 leq(0,m) -> true 0.00/0.08 leq(s(n),0) -> false 0.00/0.08 leq(s(n),s(m)) -> leq(n,m) 0.00/0.08 length(nil) -> 0 0.00/0.08 length(cons(h,t)) -> s(length(t)) 0.00/0.08 app(nil,x) -> x 0.00/0.08 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.08 map_f(pid,nil) -> nil 0.00/0.08 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.08 head(cons(h,t)) -> h 0.00/0.08 tail(cons(h,t)) -> t 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) | empty(fstsplit(m,st_1)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) | leq(m,length(st_2)) == true, empty(fstsplit(m,st_2)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two,head(in_2)),st_2)),cons(fstsplit(m,app(map_f(two,head(in_2)),st_2)),in_3),st_3,m) | leq(m,length(st_2)) == false, empty(fstsplit(m,app(map_f(two,head(in_2)),st_2))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),st_2,in_3,st_3,m) | empty(map_f(two,head(in_2))) == true 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) | leq(m,length(st_3)) == true, empty(fstsplit(m,st_3)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three,head(in_3)),st_3)),m) | leq(m,length(st_3)) == false, empty(fstsplit(m,app(map_f(three,head(in_3)),st_3))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),st_3,m) | empty(map_f(three,head(in_3))) == true 0.00/0.08 ) 0.00/0.08 (COMMENT doi:10.1007/s002000100063 [50] p. 61 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.08 0.00/0.08 Try to disprove confluence of the following (C)TRS: 0.00/0.08 (CONDITIONTYPE ORIENTED) 0.00/0.08 (VAR x n t h m pid st_3 in_3 st_2 in_2 st_1) 0.00/0.08 (RULES 0.00/0.08 fstsplit(0,x) -> nil 0.00/0.08 fstsplit(s(n),nil) -> nil 0.00/0.08 fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t)) 0.00/0.08 sndsplit(0,x) -> x 0.00/0.08 sndsplit(s(n),nil) -> nil 0.00/0.08 sndsplit(s(n),cons(h,t)) -> sndsplit(n,t) 0.00/0.08 empty(nil) -> true 0.00/0.08 empty(cons(h,t)) -> false 0.00/0.08 leq(0,m) -> true 0.00/0.08 leq(s(n),0) -> false 0.00/0.08 leq(s(n),s(m)) -> leq(n,m) 0.00/0.08 length(nil) -> 0 0.00/0.08 length(cons(h,t)) -> s(length(t)) 0.00/0.08 app(nil,x) -> x 0.00/0.08 app(cons(h,t),x) -> cons(h,app(t,x)) 0.00/0.08 map_f(pid,nil) -> nil 0.00/0.08 map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t)) 0.00/0.08 head(cons(h,t)) -> h 0.00/0.08 tail(cons(h,t)) -> t 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m) | empty(fstsplit(m,st_1)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m) | leq(m,length(st_2)) == true, empty(fstsplit(m,st_2)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),sndsplit(m,app(map_f(two,head(in_2)),st_2)),cons(fstsplit(m,app(map_f(two,head(in_2)),st_2)),in_3),st_3,m) | leq(m,length(st_2)) == false, empty(fstsplit(m,app(map_f(two,head(in_2)),st_2))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,tail(in_2),st_2,in_3,st_3,m) | empty(map_f(two,head(in_2))) == true 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m) | leq(m,length(st_3)) == true, empty(fstsplit(m,st_3)) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three,head(in_3)),st_3)),m) | leq(m,length(st_3)) == false, empty(fstsplit(m,app(map_f(three,head(in_3)),st_3))) == false 0.00/0.08 ring(st_1,in_2,st_2,in_3,st_3,m) -> ring(st_1,in_2,st_2,tail(in_3),st_3,m) | empty(map_f(three,head(in_3))) == true 0.00/0.08 ) 0.00/0.08 (COMMENT doi:10.1007/s002000100063 [50] p. 61 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.08 0.00/0.08 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.08 0.00/0.08 Try to apply SR and U for 3DCTRSs to the above CTRS. 0.00/0.08 0.00/0.08 Succeeded in applying U for 3DCTRSs to the above CTRS. 0.00/0.08 U(R) = 0.00/0.08 (VAR x1 x3 x2 x6 x5 x4) 0.00/0.08 (RULES 0.00/0.08 fstsplit(0,x1) -> nil 0.00/0.08 fstsplit(s(x1),nil) -> nil 0.00/0.08 fstsplit(s(x1),cons(x2,x3)) -> cons(x2,fstsplit(x1,x3)) 0.00/0.08 sndsplit(0,x1) -> x1 0.00/0.08 sndsplit(s(x1),nil) -> nil 0.00/0.08 sndsplit(s(x1),cons(x2,x3)) -> sndsplit(x1,x3) 0.00/0.08 empty(nil) -> true 0.00/0.08 empty(cons(x1,x2)) -> false 0.00/0.08 leq(0,x1) -> true 0.00/0.08 leq(s(x1),0) -> false 0.00/0.08 leq(s(x1),s(x2)) -> leq(x1,x2) 0.00/0.08 length(nil) -> 0 0.00/0.08 length(cons(x1,x2)) -> s(length(x2)) 0.00/0.08 app(nil,x1) -> x1 0.00/0.08 app(cons(x1,x2),x3) -> cons(x1,app(x2,x3)) 0.00/0.08 map_f(x1,nil) -> nil 0.00/0.08 map_f(x1,cons(x2,x3)) -> app(f(x1,x2),map_f(x1,x3)) 0.00/0.08 head(cons(x1,x2)) -> x1 0.00/0.08 tail(cons(x1,x2)) -> x2 0.00/0.08 ring(x1,x2,x3,x4,x5,x6) -> u1(empty(fstsplit(x6,x1)),x1,x2,x3,x4,x5,x6) 0.00/0.08 u1(false,x1,x2,x3,x4,x5,x6) -> ring(sndsplit(x6,x1),cons(fstsplit(x6,x1),x2),x3,x4,x5,x6) 0.00/0.08 ring(x1,x2,x3,x4,x5,x6) -> u2(leq(x6,length(x3)),x1,x2,x3,x4,x5,x6) 0.00/0.08 u2(true,x1,x2,x3,x4,x5,x6) -> u9(empty(fstsplit(x6,x3)),x1,x2,x3,x4,x5,x6) 0.00/0.08 u9(false,x1,x2,x3,x4,x5,x6) -> ring(x1,x2,sndsplit(x6,x3),cons(fstsplit(x6,x3),x4),x5,x6) 0.00/0.08 u2(false,x1,x2,x3,x4,x5,x6) -> u8(empty(fstsplit(x6,app(map_f(two,head(x2)),x3))),x1,x2,x3,x4,x5,x6) 0.00/0.08 u8(false,x1,x2,x3,x4,x5,x6) -> ring(x1,tail(x2),sndsplit(x6,app(map_f(two,head(x2)),x3)),cons(fstsplit(x6,app(map_f(two,head(x2)),x3)),x4),x5,x6) 0.00/0.08 ring(x1,x2,x3,x4,x5,x6) -> u3(empty(map_f(two,head(x2))),x1,x2,x3,x4,x5,x6) 0.00/0.08 u3(true,x1,x2,x3,x4,x5,x6) -> ring(x1,tail(x2),x3,x4,x5,x6) 0.00/0.08 ring(x1,x2,x3,x4,x5,x6) -> u4(leq(x6,length(x5)),x1,x2,x3,x4,x5,x6) 0.00/0.08 u4(true,x1,x2,x3,x4,x5,x6) -> u7(empty(fstsplit(x6,x5)),x1,x2,x3,x4,x5,x6) 0.00/0.08 u7(false,x1,x2,x3,x4,x5,x6) -> ring(x1,x2,x3,x4,sndsplit(x6,x5),x6) 0.00/0.08 u4(false,x1,x2,x3,x4,x5,x6) -> u6(empty(fstsplit(x6,app(map_f(three,head(x4)),x5))),x1,x2,x3,x4,x5,x6) 0.00/0.08 u6(false,x1,x2,x3,x4,x5,x6) -> ring(x1,x2,x3,tail(x4),sndsplit(x6,app(map_f(three,head(x4)),x5)),x6) 0.00/0.08 ring(x1,x2,x3,x4,x5,x6) -> u5(empty(map_f(three,head(x4))),x1,x2,x3,x4,x5,x6) 0.00/0.08 u5(true,x1,x2,x3,x4,x5,x6) -> ring(x1,x2,x3,tail(x4),x5,x6) 0.00/0.08 ) 0.00/0.08 0.00/0.08 U for 3DCTRSs is sound for the above CTRS. 0.00/0.08 0.00/0.08 Failed to prove confluence of U(R). 0.00/0.08 0.00/0.08 Try to prove operational termination of R, i.e., termination of U(R). 0.00/0.08 0.00/0.08 Failed to prove operational termination of R. 0.00/0.08 0.00/0.08 MAYBE 0.00/0.08 EOF