YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) f(g(x),g(y)) -> f(p(f(g(x),s(y))),g(s(p(x))))
(2) p(0) -> g(0)
(3) g(s(p(x))) -> p(x)

[2]  Label this TRS using following interpretation that is a quasi-model:
[f(x,y)] = 0
[g(x)] = 1
[s(x)] = 0
[0] = 1
rest default

  thus obtaining new TRS:
(1a) f$11(g$1(x),g$1(y)) -> f$01(p$0(f$10(g$1(x),s$1(y))),g$0(s$1(p$1(x))))
(1b) f$11(g$0(x),g$1(y)) -> f$01(p$0(f$10(g$0(x),s$1(y))),g$0(s$0(p$0(x))))
(1c) f$11(g$1(x),g$0(y)) -> f$01(p$0(f$10(g$1(x),s$0(y))),g$0(s$1(p$1(x))))
(1d) f$11(g$0(x),g$0(y)) -> f$01(p$0(f$10(g$0(x),s$0(y))),g$0(s$0(p$0(x))))
(2a) p$1(0) -> g$1(0)
(3a) g$0(s$1(p$1(x))) -> p$1(x)
(3b) g$0(s$0(p$0(x))) -> p$0(x)
(D1) f$10(x,y) ->= f$00(x,y)
(D2) f$11(x,y) ->= f$01(x,y)
(D3) f$11(x,y) ->= f$10(x,y)
(D4) f$01(x,y) ->= f$00(x,y)
(D5) s$1(x) ->= s$0(x)
(D6) g$1(x) ->= g$0(x)
(D7) p$1(x) ->= p$0(x)

[3]  Use following polynomial interpretation:
[f$11(x,y)] = 7xy
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1a)-(1d), (D2)-(D3)

[4]  Unlabel this TRS to obtain the one consisting of the rules:
(2)-(3)

[5]  Use following polynomial interpretation:
[s(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3)

[6]  Use following polynomial interpretation:
[p(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2)

[7]  Since there are no remaining rules, termination is proved!

../tpdb/TRS/nontermin/cariboo/tricky1.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory