- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] fstsplit(0,x) -> nil
[2] fstsplit(s(n),nil) -> nil
[3] fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
[4] sndsplit(0,x) -> x
[5] sndsplit(s(n),nil) -> nil
[6] sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
[7] empty(nil) -> true
[8] empty(cons(h,t)) -> false
[9] leq(0,m) -> true
[10] leq(s(n),0) -> false
[11] leq(s(n),s(m)) -> leq(n,m)
[12] length(nil) -> 0
[13] length(cons(h,t)) -> s(length(t))
[14] app(nil,x) -> x
[15] app(cons(h,t),x) -> cons(h,app(t,x))
[16] map_f(pid,nil) -> nil
[17] map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))
[18] head(cons(h,t)) -> h
[19] tail(cons(h,t)) -> t
[20] ring(st_1,in_2,st_2,in_3,st_3,m) ->
 if_1(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_1)))
[21] if_1(st_1,in_2,st_2,in_3,st_3,m,false) ->
 ring(sndsplit(m,st_1),cons(fstsplit(m,st_1),in_2),st_2,in_3,st_3,m)
[22] ring(st_1,in_2,st_2,in_3,st_3,m) ->
 if_2(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_2)))
[23] if_2(st_1,in_2,st_2,in_3,st_3,m,true) ->
 if_3(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_2)))
[24] if_3(st_1,in_2,st_2,in_3,st_3,m,false) ->
 ring(st_1,in_2,sndsplit(m,st_2),cons(fstsplit(m,st_2),in_3),st_3,m)
[25] if_2(st_1,in_2,st_2,in_3,st_3,m,false) ->
 if_4(st_1,in_2,st_2,in_3,st_3,m,
  empty(fstsplit(m,app(map_f(two,head(in_2)),st_2))))
[26] if_4(st_1,in_2,st_2,in_3,st_3,m,false) ->
 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)
[27] ring(st_1,in_2,st_2,in_3,st_3,m) ->
 if_5(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(two,head(in_2))))
[28] if_5(st_1,in_2,st_2,in_3,st_3,m,true) ->
 ring(st_1,tail(in_2),st_2,in_3,st_3,m)
[29] ring(st_1,in_2,st_2,in_3,st_3,m) ->
 if_6(st_1,in_2,st_2,in_3,st_3,m,leq(m,length(st_3)))
[30] if_6(st_1,in_2,st_2,in_3,st_3,m,true) ->
 if_7(st_1,in_2,st_2,in_3,st_3,m,empty(fstsplit(m,st_3)))
[31] if_7(st_1,in_2,st_2,in_3,st_3,m,false) ->
 ring(st_1,in_2,st_2,in_3,sndsplit(m,st_3),m)
[32] if_6(st_1,in_2,st_2,in_3,st_3,m,false) ->
 if_8(st_1,in_2,st_2,in_3,st_3,m,
  empty(fstsplit(m,app(map_f(three,head(in_3)),st_3))))
[33] if_8(st_1,in_2,st_2,in_3,st_3,m,false) ->
 ring(st_1,in_2,st_2,tail(in_3),sndsplit(m,app(map_f(three,head(in_3)),st_3)),
  m)
[34] ring(st_1,in_2,st_2,in_3,st_3,m) ->
 if_9(st_1,in_2,st_2,in_3,st_3,m,empty(map_f(three,head(in_3))))
[35] if_9(st_1,in_2,st_2,in_3,st_3,m,true) ->
 ring(st_1,in_2,st_2,tail(in_3),st_3,m)


Sub problem: 
guided: 

DP termination of:
<Marked_fstsplit(s(n),cons(h,t)) , Marked_fstsplit(n,t)>
<Marked_sndsplit(s(n),cons(h,t)) , Marked_sndsplit(n,t)>
<Marked_leq(s(n),s(m)) , Marked_leq(n,m)>
<Marked_length(cons(h,t)) , Marked_length(t)>
<Marked_app(cons(h,t),x) , Marked_app(t,x)>
<Marked_map_f(pid,cons(h,t)) , Marked_app(f(pid,h),map_f(pid,t))>
<Marked_map_f(pid,cons(h,t)) , Marked_map_f(pid,t)>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,in_2,st_2,
                                            in_3,st_3,m,
                                            empty(fstsplit(m,st_1)))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_empty(fstsplit(m,st_1))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_fstsplit(m,st_1)>
<Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                  cons(fstsplit(m,st_1),in_2),
                                                  st_2,in_3,st_3,m)>
<Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_sndsplit(m,st_1)>
<Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_fstsplit(m,st_1)>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,in_2,st_2,
                                            in_3,st_3,m,leq(m,length(st_2)))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_leq(m,length(st_2))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_length(st_2)>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_3(st_1,in_2,
                                                 st_2,in_3,st_3,m,
                                                 empty(fstsplit(m,st_2)))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_empty(fstsplit(m,st_2))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_fstsplit(m,st_2)>
<Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                  sndsplit(m,st_2),
                                                  cons(fstsplit(m,st_2),in_3),
                                                  st_3,m)>
<Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_sndsplit(m,st_2)>
<Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_fstsplit(m,st_2)>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_4(st_1,in_2,
                                                  st_2,in_3,st_3,m,
                                                  empty(fstsplit(m,
                                                         app(map_f(two,
                                                              head(in_2)),
                                                          st_2))))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_empty(fstsplit(
                                                               m,
                                                               app(map_f(
                                                                    two,
                                                                    head(in_2)),
                                                                st_2)))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_fstsplit(m,
                                                  app(map_f(two,head(in_2)),
                                                   st_2))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_app(map_f(two,
                                                             head(in_2)),
                                                  st_2)>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_map_f(two,head(in_2))>
<Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_head(in_2)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_tail(in_2)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_sndsplit(m,
                                                  app(map_f(two,head(in_2)),
                                                   st_2))>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_app(map_f(two,
                                                             head(in_2)),
                                                  st_2)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_map_f(two,head(in_2))>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_head(in_2)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_fstsplit(m,
                                                  app(map_f(two,head(in_2)),
                                                   st_2))>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_app(map_f(two,
                                                             head(in_2)),
                                                  st_2)>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_map_f(two,head(in_2))>
<Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_head(in_2)>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,in_2,st_2,
                                            in_3,st_3,m,
                                            empty(map_f(two,head(in_2))))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_empty(map_f(two,head(in_2)))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_map_f(two,head(in_2))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_head(in_2)>
<Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                 st_2,in_3,st_3,m)>
<Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_tail(in_2)>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,in_2,st_2,
                                            in_3,st_3,m,leq(m,length(st_3)))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_leq(m,length(st_3))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_length(st_3)>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_7(st_1,in_2,
                                                 st_2,in_3,st_3,m,
                                                 empty(fstsplit(m,st_3)))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_empty(fstsplit(m,st_3))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_fstsplit(m,st_3)>
<Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                  st_2,in_3,sndsplit(m,st_3),
                                                  m)>
<Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_sndsplit(m,st_3)>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_8(st_1,in_2,
                                                  st_2,in_3,st_3,m,
                                                  empty(fstsplit(m,
                                                         app(map_f(three,
                                                              head(in_3)),
                                                          st_3))))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_empty(fstsplit(
                                                               m,
                                                               app(map_f(
                                                                    three,
                                                                    head(in_3)),
                                                                st_3)))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_fstsplit(m,
                                                  app(map_f(three,head(in_3)),
                                                   st_3))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_app(map_f(three,
                                                             head(in_3)),
                                                  st_3)>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_map_f(three,head(in_3))>
<Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_head(in_3)>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                  st_2,tail(in_3),
                                                  sndsplit(m,
                                                   app(map_f(three,head(in_3)),
                                                    st_3)),m)>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_tail(in_3)>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_sndsplit(m,
                                                  app(map_f(three,head(in_3)),
                                                   st_3))>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_app(map_f(three,
                                                             head(in_3)),
                                                  st_3)>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_map_f(three,head(in_3))>
<Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_head(in_3)>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,in_2,st_2,
                                            in_3,st_3,m,
                                            empty(map_f(three,head(in_3))))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_empty(map_f(three,head(in_3)))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_map_f(three,head(in_3))>
<Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_head(in_3)>
<Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                 st_2,tail(in_3),st_3,
                                                 m)>
<Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_tail(in_3)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 7 components:

{  <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),st_3,
                                                    m)> 
      --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                      in_2,st_2,in_3,
                                                      st_3,m,
                                                      empty(map_f(three,
                                                             head(in_3))))>
  <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(three,head(in_3))))> 
     --> <Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(
                                                          st_1,in_2,st_2,
                                                          tail(in_3),
                                                          st_3,m)>
  <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_8(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                three,
                                                                head(in_3)),
                                                            st_3))))> 
     --> <Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(
                                                           st_1,in_2,
                                                           st_2,tail(in_3),
                                                           sndsplit(m,
                                                            app(map_f(
                                                                 three,
                                                                 head(in_3)),
                                                             st_3)),m)>
  <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_7(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_3)))> 
     --> <Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(
                                                           st_1,in_2,
                                                           st_2,in_3,
                                                           sndsplit(m,st_3),
                                                           m)>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_3)))> 
     --> <Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_8(
                                                           st_1,in_2,
                                                           st_2,in_3,
                                                           st_3,m,
                                                           empty(fstsplit(
                                                                  m,
                                                                  app(
                                                                   map_f(
                                                                    three,
                                                                    head(in_3)),
                                                                   st_3))))>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_3)))> 
     --> <Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_7(
                                                          st_1,in_2,st_2,
                                                          in_3,st_3,m,
                                                          empty(fstsplit(
                                                                 m,st_3)))>
  <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(two,head(in_2))))> 
     --> <Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_ring(
                                                          st_1,tail(in_2),
                                                          st_2,in_3,st_3,
                                                          m)>
  <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_4(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                two,head(in_2)),
                                                            st_2))))> 
     --> <Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_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)>
  <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_3(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_2)))> 
     --> <Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(
                                                           st_1,in_2,
                                                           sndsplit(m,st_2),
                                                           cons(fstsplit(
                                                                 m,st_2),
                                                            in_3),st_3,
                                                           m)>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_2)))> 
     --> <Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_if_4(
                                                           st_1,in_2,
                                                           st_2,in_3,
                                                           st_3,m,
                                                           empty(fstsplit(
                                                                  m,
                                                                  app(
                                                                   map_f(
                                                                    two,
                                                                    head(in_2)),
                                                                   st_2))))>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_2)))> 
     --> <Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) , Marked_if_3(
                                                          st_1,in_2,st_2,
                                                          in_3,st_3,m,
                                                          empty(fstsplit(
                                                                 m,st_2)))>
  <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_9(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(three,
                                                            head(in_3))))>
  <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_6(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_3)))>
  <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_5(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,
                                                     empty(map_f(two,
                                                            head(in_2))))>
  <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_2(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,leq(m,length(st_2)))>
  <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m)> 
     --> <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,
                                                     in_2,st_2,in_3,st_3,
                                                     m,empty(fstsplit(m,st_1)))>
  <Marked_ring(st_1,in_2,st_2,in_3,st_3,m) , Marked_if_1(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(fstsplit(m,st_1)))> 
     --> <Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) , Marked_ring(
                                                           sndsplit(m,
                                                            st_1),
                                                           cons(fstsplit(
                                                                 m,st_1),
                                                            in_2),st_2,
                                                           in_3,st_3,
                                                           m)>
}

{  <Marked_sndsplit(s(n),cons(h,t)) , Marked_sndsplit(n,t)> 
      --> <Marked_sndsplit(s(n),cons(h,t)) , Marked_sndsplit(n,t)>
}

{  <Marked_fstsplit(s(n),cons(h,t)) , Marked_fstsplit(n,t)> 
      --> <Marked_fstsplit(s(n),cons(h,t)) , Marked_fstsplit(n,t)>
}

{  <Marked_app(cons(h,t),x) , Marked_app(t,x)> 
      --> <Marked_app(cons(h,t),x) , Marked_app(t,x)>
}

{  <Marked_leq(s(n),s(m)) , Marked_leq(n,m)> 
      --> <Marked_leq(s(n),s(m)) , Marked_leq(n,m)>
}

{  <Marked_length(cons(h,t)) , Marked_length(t)> 
      --> <Marked_length(cons(h,t)) , Marked_length(t)>
}

{  <Marked_map_f(pid,cons(h,t)) , Marked_map_f(pid,t)> 
      --> <Marked_map_f(pid,cons(h,t)) , Marked_map_f(pid,t)>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  fstsplit(0,x) >= nil ;
  fstsplit(s(n),nil) >= nil ;
  fstsplit(s(n),cons(h,t)) >= cons(h,fstsplit(n,t)) ;
  sndsplit(0,x) >= x ;
  sndsplit(s(n),nil) >= nil ;
  sndsplit(s(n),cons(h,t)) >= sndsplit(n,t) ;
  empty(nil) >= true ;
  empty(cons(h,t)) >= false ;
  leq(0,m) >= true ;
  leq(s(n),0) >= false ;
  leq(s(n),s(m)) >= leq(n,m) ;
  length(nil) >= 0 ;
  length(cons(h,t)) >= s(length(t)) ;
  app(nil,x) >= x ;
  app(cons(h,t),x) >= cons(h,app(t,x)) ;
  map_f(pid,nil) >= nil ;
  map_f(pid,cons(h,t)) >= app(f(pid,h),map_f(pid,t)) ;
  head(cons(h,t)) >= h ;
  tail(cons(h,t)) >= t ;
  if_1(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(sndsplit(m,st_1),
                                             cons(fstsplit(m,st_1),in_2),
                                             st_2,in_3,st_3,m) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_1(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(fstsplit(m,st_1))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_2(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_2))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_5(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(two,head(in_2)))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_6(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_3))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_9(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(three,head(in_3)))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= if_3(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_2))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= if_4(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(two,head(in_2)),
                                                     st_2)))) ;
  if_3(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,sndsplit(m,st_2),
                                             cons(fstsplit(m,st_2),in_3),
                                             st_3,m) ;
  if_4(st_1,in_2,st_2,in_3,st_3,m,false) >= 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) ;
  if_5(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,tail(in_2),st_2,
                                            in_3,st_3,m) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= if_7(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_3))) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= if_8(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)))) ;
  if_7(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,in_3,
                                             sndsplit(m,st_3),m) ;
  if_8(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,tail(in_3),
                                             sndsplit(m,
                                              app(map_f(three,head(in_3)),st_3)),
                                             m) ;
  if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,in_2,st_2,tail(in_3),
                                            st_3,m) ;
  Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_9(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(three,head(in_3)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_6(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_3))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_5(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(two,head(in_2)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_2(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_2))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_1(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(fstsplit(m,st_1))) ;
  Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_ring(st_1,in_2,
                                                    st_2,tail(in_3),
                                                    sndsplit(m,
                                                     app(map_f(three,
                                                          head(in_3)),
                                                      st_3)),m) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_7(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_3))) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_8(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                three,
                                                                head(in_3)),
                                                            st_3)))) ;
  Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_ring(st_1,in_2,
                                                    st_2,in_3,sndsplit(m,st_3),
                                                    m) ;
  Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_ring(st_1,tail(in_2),
                                                   st_2,in_3,st_3,m) ;
  Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_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) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_3(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_2))) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_4(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                two,head(in_2)),
                                                            st_2)))) ;
  Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_ring(st_1,in_2,
                                                    sndsplit(m,st_2),
                                                    cons(fstsplit(m,st_2),in_3),
                                                    st_3,m) ;
  Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_ring(sndsplit(m,st_1),
                                                    cons(fstsplit(m,st_1),in_2),
                                                    st_2,in_3,st_3,m) ;
 }
 + Disjunctions:{ 
{
  Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_ring(st_1,in_2,
                                                  st_2,tail(in_3),st_3,
                                                  m) ;
 }
{
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_9(st_1,in_2,st_2,
                                             in_3,st_3,m,
                                             empty(map_f(three,head(in_3)))) ;
 }
{
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_6(st_1,in_2,st_2,
                                             in_3,st_3,m,leq(m,length(st_3))) ;
 }
{
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_5(st_1,in_2,st_2,
                                             in_3,st_3,m,
                                             empty(map_f(two,head(in_2)))) ;
 }
{
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_2(st_1,in_2,st_2,
                                             in_3,st_3,m,leq(m,length(st_2))) ;
 }
{
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_1(st_1,in_2,st_2,
                                             in_3,st_3,m,
                                             empty(fstsplit(m,st_1))) ;
 }
{
  Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),
                                                   sndsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)),m) ;
 }
{
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_if_7(st_1,in_2,
                                                  st_2,in_3,st_3,m,
                                                  empty(fstsplit(m,st_3))) ;
 }
{
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_if_8(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,
                                                          app(map_f(three,
                                                               head(in_3)),
                                                           st_3)))) ;
 }
{
  Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,in_3,sndsplit(m,st_3),
                                                   m) ;
 }
{
  Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_ring(st_1,tail(in_2),
                                                  st_2,in_3,st_3,m) ;
 }
{
  Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_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) ;
 }
{
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_if_3(st_1,in_2,
                                                  st_2,in_3,st_3,m,
                                                  empty(fstsplit(m,st_2))) ;
 }
{
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_if_4(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,
                                                          app(map_f(two,
                                                               head(in_2)),
                                                           st_2)))) ;
 }
{
  Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   sndsplit(m,st_2),
                                                   cons(fstsplit(m,st_2),in_3),
                                                   st_3,m) ;
 }
{
  Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(sndsplit(m,st_1),
                                                   cons(fstsplit(m,st_1),in_2),
                                                   st_2,in_3,st_3,m) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat timeout reached
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (Simple graph)
Found the following constraints:
{
  fstsplit(0,x) >= nil ;
  fstsplit(s(n),nil) >= nil ;
  fstsplit(s(n),cons(h,t)) >= cons(h,fstsplit(n,t)) ;
  sndsplit(0,x) >= x ;
  sndsplit(s(n),nil) >= nil ;
  sndsplit(s(n),cons(h,t)) >= sndsplit(n,t) ;
  empty(nil) >= true ;
  empty(cons(h,t)) >= false ;
  leq(0,m) >= true ;
  leq(s(n),0) >= false ;
  leq(s(n),s(m)) >= leq(n,m) ;
  length(nil) >= 0 ;
  length(cons(h,t)) >= s(length(t)) ;
  app(nil,x) >= x ;
  app(cons(h,t),x) >= cons(h,app(t,x)) ;
  map_f(pid,nil) >= nil ;
  map_f(pid,cons(h,t)) >= app(f(pid,h),map_f(pid,t)) ;
  head(cons(h,t)) >= h ;
  tail(cons(h,t)) >= t ;
  if_1(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(sndsplit(m,st_1),
                                             cons(fstsplit(m,st_1),in_2),
                                             st_2,in_3,st_3,m) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_1(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(fstsplit(m,st_1))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_2(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_2))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_5(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(two,head(in_2)))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_6(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_3))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_9(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(three,head(in_3)))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= if_3(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_2))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= if_4(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(two,head(in_2)),
                                                     st_2)))) ;
  if_3(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,sndsplit(m,st_2),
                                             cons(fstsplit(m,st_2),in_3),
                                             st_3,m) ;
  if_4(st_1,in_2,st_2,in_3,st_3,m,false) >= 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) ;
  if_5(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,tail(in_2),st_2,
                                            in_3,st_3,m) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= if_7(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_3))) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= if_8(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)))) ;
  if_7(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,in_3,
                                             sndsplit(m,st_3),m) ;
  if_8(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,tail(in_3),
                                             sndsplit(m,
                                              app(map_f(three,head(in_3)),st_3)),
                                             m) ;
  if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,in_2,st_2,tail(in_3),
                                            st_3,m) ;
  Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_9(st_1,in_2,st_2,
                                             in_3,st_3,m,
                                             empty(map_f(three,head(in_3)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_6(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_3))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_5(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(two,head(in_2)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_2(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_2))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_1(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(fstsplit(m,st_1))) ;
  Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),
                                                   sndsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)),m) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_7(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_3))) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_8(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                three,
                                                                head(in_3)),
                                                            st_3)))) ;
  Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,in_3,sndsplit(m,st_3),
                                                   m) ;
  Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_ring(st_1,tail(in_2),
                                                  st_2,in_3,st_3,m) ;
  Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_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) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_3(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_2))) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_4(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                two,head(in_2)),
                                                            st_2)))) ;
  Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   sndsplit(m,st_2),
                                                   cons(fstsplit(m,st_2),in_3),
                                                   st_3,m) ;
  Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(sndsplit(m,st_1),
                                                   cons(fstsplit(m,st_1),in_2),
                                                   st_2,in_3,st_3,m) ;
 }

APPLY CRITERIA (SOLVE_ORD)
Trying to solve the following constraints:
{
  fstsplit(0,x) >= nil ;
  fstsplit(s(n),nil) >= nil ;
  fstsplit(s(n),cons(h,t)) >= cons(h,fstsplit(n,t)) ;
  sndsplit(0,x) >= x ;
  sndsplit(s(n),nil) >= nil ;
  sndsplit(s(n),cons(h,t)) >= sndsplit(n,t) ;
  empty(nil) >= true ;
  empty(cons(h,t)) >= false ;
  leq(0,m) >= true ;
  leq(s(n),0) >= false ;
  leq(s(n),s(m)) >= leq(n,m) ;
  length(nil) >= 0 ;
  length(cons(h,t)) >= s(length(t)) ;
  app(nil,x) >= x ;
  app(cons(h,t),x) >= cons(h,app(t,x)) ;
  map_f(pid,nil) >= nil ;
  map_f(pid,cons(h,t)) >= app(f(pid,h),map_f(pid,t)) ;
  head(cons(h,t)) >= h ;
  tail(cons(h,t)) >= t ;
  if_1(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(sndsplit(m,st_1),
                                             cons(fstsplit(m,st_1),in_2),
                                             st_2,in_3,st_3,m) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_1(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(fstsplit(m,st_1))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_2(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_2))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_5(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(two,head(in_2)))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_6(st_1,in_2,st_2,in_3,st_3,m,
                                       leq(m,length(st_3))) ;
  ring(st_1,in_2,st_2,in_3,st_3,m) >= if_9(st_1,in_2,st_2,in_3,st_3,m,
                                       empty(map_f(three,head(in_3)))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= if_3(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_2))) ;
  if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= if_4(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(two,head(in_2)),
                                                     st_2)))) ;
  if_3(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,sndsplit(m,st_2),
                                             cons(fstsplit(m,st_2),in_3),
                                             st_3,m) ;
  if_4(st_1,in_2,st_2,in_3,st_3,m,false) >= 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) ;
  if_5(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,tail(in_2),st_2,
                                            in_3,st_3,m) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= if_7(st_1,in_2,st_2,in_3,st_3,
                                            m,empty(fstsplit(m,st_3))) ;
  if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= if_8(st_1,in_2,st_2,in_3,
                                             st_3,m,
                                             empty(fstsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)))) ;
  if_7(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,in_3,
                                             sndsplit(m,st_3),m) ;
  if_8(st_1,in_2,st_2,in_3,st_3,m,false) >= ring(st_1,in_2,st_2,tail(in_3),
                                             sndsplit(m,
                                              app(map_f(three,head(in_3)),st_3)),
                                             m) ;
  if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= ring(st_1,in_2,st_2,tail(in_3),
                                            st_3,m) ;
  Marked_if_9(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),st_3,
                                                   m) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) > Marked_if_9(st_1,in_2,st_2,
                                             in_3,st_3,m,
                                             empty(map_f(three,head(in_3)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_6(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_3))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_5(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(map_f(two,head(in_2)))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_2(st_1,in_2,st_2,
                                              in_3,st_3,m,leq(m,length(st_2))) ;
  Marked_ring(st_1,in_2,st_2,in_3,st_3,m) >= Marked_if_1(st_1,in_2,st_2,
                                              in_3,st_3,m,
                                              empty(fstsplit(m,st_1))) ;
  Marked_if_8(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,tail(in_3),
                                                   sndsplit(m,
                                                    app(map_f(three,head(in_3)),
                                                     st_3)),m) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_7(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_3))) ;
  Marked_if_6(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_8(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                three,
                                                                head(in_3)),
                                                            st_3)))) ;
  Marked_if_7(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   st_2,in_3,sndsplit(m,st_3),
                                                   m) ;
  Marked_if_5(st_1,in_2,st_2,in_3,st_3,m,true) > Marked_ring(st_1,tail(in_2),
                                                  st_2,in_3,st_3,m) ;
  Marked_if_4(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_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) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,true) >= Marked_if_3(st_1,in_2,
                                                   st_2,in_3,st_3,m,
                                                   empty(fstsplit(m,st_2))) ;
  Marked_if_2(st_1,in_2,st_2,in_3,st_3,m,false) >= Marked_if_4(st_1,in_2,
                                                    st_2,in_3,st_3,m,
                                                    empty(fstsplit(m,
                                                           app(map_f(
                                                                two,head(in_2)),
                                                            st_2)))) ;
  Marked_if_3(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(st_1,in_2,
                                                   sndsplit(m,st_2),
                                                   cons(fstsplit(m,st_2),in_3),
                                                   st_3,m) ;
  Marked_if_1(st_1,in_2,st_2,in_3,st_3,m,false) > Marked_ring(sndsplit(m,st_1),
                                                   cons(fstsplit(m,st_1),in_2),
                                                   st_2,in_3,st_3,m) ;
 }
 + Disjunctions:{ 
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER virtual ===
=== STOPING TIMER real ===

Global timeout: 300.000000