MAYBE Rewrite Rules: [ eq(?n,?xs,?xs) -> T, eq(s(?n),c(?x,?xs),c(?x,?ys)) -> eq(?n,?xs,?ys), nats -> c(0,inc(nats)), inc(c(?x,?xs)) -> c(s(?x),inc(?xs)) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ T = eq(?n_1,?xs_1,?xs_1) ] Overlay, check Innermost Termination... unknown Innermost Terminating not Left-Linear, Right-Linear unknown Ohta&Oyamaguchi&Toyama unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ eq(?n,?xs,?xs) -> T, eq(s(?n),c(?x,?xs),c(?x,?ys)) -> eq(?n,?xs,?ys), nats -> c(0,inc(nats)), inc(c(?x,?xs)) -> c(s(?x),inc(?xs)) ] Sort Assignment: 0 : =>11 T : =>25 c : 11*23=>23 s : 11=>11 eq : 11*23*23=>25 inc : 23=>23 nats : =>23 maximal types: {11,23,25} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ eq(?n,?xs,?xs) -> T, eq(s(?n),c(?x,?xs),c(?x,?ys)) -> eq(?n,?xs,?ys), nats -> c(0,inc(nats)), inc(c(?x,?xs)) -> c(s(?x),inc(?xs)) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ eq(?n,?xs,?xs) -> T, eq(s(?n),c(?x,?xs),c(?x,?ys)) -> eq(?n,?xs,?ys), nats -> c(0,inc(nats)), inc(c(?x,?xs)) -> c(s(?x),inc(?xs)) ] Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge example11.trs: MAYBE (8 msec.)