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