MAYBE
Rewrite Rules:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))),
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ ?z_3 = ?z_3,
     ?z_4 = ?z_4 ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
not Left-Linear, not Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
Sort Assignment:
 0 : =>31
 s : 31=>31
 if : 15*31*31=>31
 tl : 34=>34
 nil : =>34
 cons : 22*34=>34
 null : 34=>15
 true : =>15
 count : 34=>31
 false : =>15
non-linear variables: {?y_5}
non-linear types: {31}
types leq non-linear types: {31}
rules applicable to terms of non-linear types:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
unknown innermost-termination for terms of non-linear types
unknown Quasi-Left-Linear & Parallel-Closed
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
Sort Assignment:
 0 : =>31
 s : 31=>31
 if : 15*31*31=>31
 tl : 34=>34
 nil : =>34
 cons : 22*34=>34
 null : 34=>15
 true : =>15
 count : 34=>31
 false : =>15
non-linear variables: {?xs_1,?y_5}
non-linear types: {34,31}
types leq non-linear types: {34,31}
rules applicable to terms of non-linear types:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
Rnl:
0: {}
1: {}
2: {3,4}
3: {}
4: {}
5: {}
6: {}
7: {0,1,2,3,4,5,6,7}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
Sort Assignment:
 0 : =>31
 s : 31=>31
 if : 15*31*31=>31
 tl : 34=>34
 nil : =>34
 cons : 22*34=>34
 null : 34=>15
 true : =>15
 count : 34=>31
 false : =>15
non-linear variables: {?xs_1,?y_5}
non-linear types: {34,31}
types leq non-linear types: {34,31}
rules applicable to terms of non-linear types:
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs_1) -> if(null(?xs_1),0,s(count(tl(?xs_1)))),
     tl(nil) -> nil,
     tl(cons(?x_2,?ys_2)) -> ?ys_2,
     if(true,?y_3,?z_3) -> ?y_3,
     if(false,?y_4,?z_4) -> ?z_4,
     if(?x_5,?y_5,?y_5) -> ?y_5 ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 12 rules by 3 steps unfolding
obtain 4 candidates for checking non-joinability
check by TCAP-Approximation   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
 (failure)
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
 (failure)
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
 (failure)
check by Interpretation(mod2)   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
check by Descendants-Approximation, check by Ordering(poly)   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?ys:List)) -> false,
     count(?xs:List) -> if(null(?xs:List),0,s(count(tl(?xs:List)))),
     tl(nil) -> nil,
     tl(cons(?x:Nat,?ys:List)) -> ?ys:List,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat ]
 (failure)
unknown Non-Confluence
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))),
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y ]
Sort Assignment:
 0 : =>31
 s : 31=>31
 if : 15*31*31=>31
 tl : 34=>34
 nil : =>34
 cons : 22*34=>34
 null : 34=>15
 true : =>15
 count : 34=>31
 false : =>15
maximal types: {15,22,31,34}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))),
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ null(nil) -> true,
     null(cons(?x,?ys)) -> false,
     count(?xs) -> if(null(?xs),0,s(count(tl(?xs)))),
     tl(nil) -> nil,
     tl(cons(?x,?ys)) -> ?ys,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y ]
Commutative Decomposition failed (not left-linear): Can't judge
No further decomposition possible


Final result: Can't judge
new/if7.trs: Failure(unknown)
(311 msec.)