MAYBE
TRS:
 { function(iszero(), 0(), dummy, dummy2) -> true(),
  function(iszero(), s(x), dummy, dummy2) -> false(),
        function(p(), 0(), dummy, dummy2) -> 0(),
     function(p(), s(0()), dummy, dummy2) -> 0(),
    function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)),
             function(if(), true(), x, y) -> y,
            function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
            function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y),
               function(third(), x, y, z) -> z}
 DP:
  Strict:
   {function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x),
            function#(if(), false(), x, y) -> function#(p(), x, x, y),
            function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
            function#(if(), false(), x, y) -> function#(third(), x, y, y),
            function#(plus(), dummy, x, y) -> function#(iszero(), x, x, x),
            function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y)}
  Weak:
  { function(iszero(), 0(), dummy, dummy2) -> true(),
   function(iszero(), s(x), dummy, dummy2) -> false(),
         function(p(), 0(), dummy, dummy2) -> 0(),
      function(p(), s(0()), dummy, dummy2) -> 0(),
     function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)),
              function(if(), true(), x, y) -> y,
             function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
             function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y),
                function(third(), x, y, z) -> z}
  EDG:
   {(function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x), function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x))
    (function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)), function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y))
    (function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)), function#(plus(), dummy, x, y) -> function#(iszero(), x, x, x))
    (function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y), function#(if(), false(), x, y) -> function#(p(), x, x, y))
    (function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y), function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)))
    (function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y), function#(if(), false(), x, y) -> function#(third(), x, y, y))
    (function#(if(), false(), x, y) -> function#(p(), x, x, y), function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x))}
   SCCS:
    Scc:
     {function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
      function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y)}
    Scc:
     {function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x)}
    SCC:
     Strict:
      {function#(if(), false(), x, y) -> function#(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
       function#(plus(), dummy, x, y) -> function#(if(), function(iszero(), x, x, x), x, y)}
     Weak:
     { function(iszero(), 0(), dummy, dummy2) -> true(),
      function(iszero(), s(x), dummy, dummy2) -> false(),
            function(p(), 0(), dummy, dummy2) -> 0(),
         function(p(), s(0()), dummy, dummy2) -> 0(),
        function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)),
                 function(if(), true(), x, y) -> y,
                function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
                function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y),
                   function(third(), x, y, z) -> z}
     Fail
    SCC:
     Strict:
      {function#(p(), s(s(x)), dummy, dummy2) -> function#(p(), s(x), x, x)}
     Weak:
     { function(iszero(), 0(), dummy, dummy2) -> true(),
      function(iszero(), s(x), dummy, dummy2) -> false(),
            function(p(), 0(), dummy, dummy2) -> 0(),
         function(p(), s(0()), dummy, dummy2) -> 0(),
        function(p(), s(s(x)), dummy, dummy2) -> s(function(p(), s(x), x, x)),
                 function(if(), true(), x, y) -> y,
                function(if(), false(), x, y) -> function(plus(), function(third(), x, y, y), function(p(), x, x, y), s(y)),
                function(plus(), dummy, x, y) -> function(if(), function(iszero(), x, x, x), x, y),
                   function(third(), x, y, z) -> z}
     SPSC:
      Simple Projection:
       pi(function#) = 1
      Strict:
       {}
      Qed