NO
LCTRS
  Theories
    Core, Ints
  Signature
    geq: (Int, Int) -> Bool
    geq2: (Int, Int, Int, Int) -> Bool
    p: Int -> Int
    plus: (Int, Int) -> Int
    s: Int -> Int
    sum: Int -> Int
    sum2: (Bool, Int) -> Int
  Rules
    geq(?73, ?74) -> geq2(?73, ?74, 0, 0)
    geq2(?75, ?76, ?77, ?78) -> true [?75 = 0, ?76 = 0, ?78 = 0]
    geq2(?79, ?80, ?81, s(?82)) -> false [?79 = 0, ?80 = 0, ?81 = 0]
    geq2(?83, ?84, s(?85), s(?86)) -> geq2(0, 0, ?85, ?86) [?83 = 0, ?84 = 0]
    geq2(?87, p(?88), ?89, ?90) -> geq2(0, ?88, s(?89), ?90) [?87 = 0]
    geq2(?91, s(?92), ?93, ?94) -> geq2(0, ?92, ?93, s(?94)) [?91 = 0]
    geq2(p(?95), ?96, ?97, ?98) -> geq2(?95, ?96, ?97, s(?98))
    geq2(s(?99), ?100, ?101, ?102) -> geq2(?99, ?100, s(?101), ?102)
    p(s(?103)) -> ?103
    plus(?104, ?105) -> ?105 [?104 = 0]
    plus(p(?106), ?107) -> p(plus(?106, ?107))
    plus(s(?108), ?109) -> s(plus(?108, ?109))
    s(p(?110)) -> ?110
    sum(?111) -> sum2(geq(0, ?111), ?111)
    sum2(?112, ?113) -> 0 [?112 = true]
    sum2(?114, s(?115)) -> plus(s(?115), sum(?115)) [?114 = false]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      s(p(?110')) -> ?110'
    Outer Rule
      geq2(?79", ?80", ?81", s(?82")) -> false [=(?79", 0), =(?80", 0), =(?81", 0)]
    Pair
      geq2(?79", ?80", ?81", ?110') ≈ false [=(?79", 0), =(?80", 0), =(?81", 0)]
  reaches the non-trivial normal form
    geq2(?79", ?80", ?81", ?110') ≈ false [?79" = 0, ?80" = 0, ?81" = 0]
      -> geq2(?79", ?80", ?81", ?110') ≈ ?1082' [?79" = 0, ?80" = 0, ?81" = 0, ?1082' = false]

Elapsed Time: 1240.36 ms