MAYBE
(ignored inputs)COMMENT from Example 3 of \cite{OO03}
Rewrite Rules:
   [ if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     -(s(?x),s(?y)) -> -(?x,?y),
     -(?x,0) -> ?x,
     -(0,?x) -> 0,
     <(s(?x),s(?y)) -> <(?x,?y),
     <(0,s(?x)) -> true,
     <(?x,0) -> false,
     mod(0,?y) -> 0,
     mod(?x,s(?y)) -> if(<(?x,s(?y)),?x,mod(-(?x,s(?y)),s(?y))),
     mod(?x,0) -> ?x,
     gcd(?x,?y) -> gcd(?y,mod(?x,?y)),
     gcd(?x,0) -> ?x,
     gcd(0,?x) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ 0 = 0,
     0 = if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))),
     0 = 0,
     gcd(0,mod(?x_11,0)) = ?x_11,
     gcd(?y_11,mod(0,?y_11)) = ?y_11,
     0 = 0 ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ 0 = 0,
     if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))) = 0,
     0 = if(<(0,s(?y)),0,mod(-(0,s(?y)),s(?y))),
     ?x = gcd(0,mod(?x,0)),
     ?y = gcd(?y,mod(0,?y)),
     gcd(0,mod(?x,0)) = ?x,
     gcd(?x,mod(0,?x)) = ?x ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <0, 0> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))), 0> by Rules <9, 8> preceded by []
 joinable by a reduction of rules <[([(if,1)],6),([],0)], []>
Critical Pair <0, 0> by Rules <10, 8> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <?x_12, gcd(0,mod(?x_12,0))> by Rules <12, 11> preceded by []
 joinable by a reduction of rules <[], [([(gcd,2)],10),([],13)]>
 joinable by a reduction of rules <[], [([],13),([],10)]>
Critical Pair <?x_13, gcd(?x_13,mod(0,?x_13))> by Rules <13, 11> preceded by []
 joinable by a reduction of rules <[], [([(gcd,2)],8),([],12)]>
Critical Pair <0, 0> by Rules <13, 12> preceded by []
 joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
   [ if(true,?x,?y) -> ?x,
     if(false,?x_1,?y_1) -> ?y_1,
     -(s(?x_2),s(?y_2)) -> -(?x_2,?y_2),
     -(?x_3,0) -> ?x_3,
     -(0,?x_4) -> 0,
     <(s(?x_5),s(?y_5)) -> <(?x_5,?y_5),
     <(0,s(?x_6)) -> true,
     <(?x_7,0) -> false,
     mod(0,?y_8) -> 0,
     mod(?x_9,s(?y_9)) -> if(<(?x_9,s(?y_9)),?x_9,mod(-(?x_9,s(?y_9)),s(?y_9))),
     mod(?x_10,0) -> ?x_10,
     gcd(?x_11,?y_11) -> gcd(?y_11,mod(?x_11,?y_11)),
     gcd(?x_12,0) -> ?x_12,
     gcd(0,?x_13) -> ?x_13 ]
Sort Assignment:
 - : 42*42=>42
 0 : =>42
 < : 42*42=>48
 s : 42=>42
 if : 48*42*42=>42
 gcd : 42*42=>42
 mod : 42*42=>42
 true : =>48
 false : =>48
non-linear variables: {?x_9,?y_9,?y_11}
non-linear types: {42}
types leq non-linear types: {42}
rules applicable to terms of non-linear types:
   [ if(true,?x,?y) -> ?x,
     if(false,?x_1,?y_1) -> ?y_1,
     -(s(?x_2),s(?y_2)) -> -(?x_2,?y_2),
     -(?x_3,0) -> ?x_3,
     -(0,?x_4) -> 0,
     <(s(?x_5),s(?y_5)) -> <(?x_5,?y_5),
     <(0,s(?x_6)) -> true,
     <(?x_7,0) -> false,
     mod(0,?y_8) -> 0,
     mod(?x_9,s(?y_9)) -> if(<(?x_9,s(?y_9)),?x_9,mod(-(?x_9,s(?y_9)),s(?y_9))),
     mod(?x_10,0) -> ?x_10,
     gcd(?x_11,?y_11) -> gcd(?y_11,mod(?x_11,?y_11)),
     gcd(?x_12,0) -> ?x_12,
     gcd(0,?x_13) -> ?x_13 ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {}
9: {0,1,2,3,4,5,6,7,8,9,10,11,12,13}
10: {}
11: {0,1,2,3,4,5,6,7,8,9,10,11,12,13}
12: {}
13: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ if(true,?x,?y) -> ?x,
     if(false,?x_1,?y_1) -> ?y_1,
     -(s(?x_2),s(?y_2)) -> -(?x_2,?y_2),
     -(?x_3,0) -> ?x_3,
     -(0,?x_4) -> 0,
     <(s(?x_5),s(?y_5)) -> <(?x_5,?y_5),
     <(0,s(?x_6)) -> true,
     <(?x_7,0) -> false,
     mod(0,?y_8) -> 0,
     mod(?x_9,s(?y_9)) -> if(<(?x_9,s(?y_9)),?x_9,mod(-(?x_9,s(?y_9)),s(?y_9))),
     mod(?x_10,0) -> ?x_10,
     gcd(?x_11,?y_11) -> gcd(?y_11,mod(?x_11,?y_11)),
     gcd(?x_12,0) -> ?x_12,
     gcd(0,?x_13) -> ?x_13 ]
Sort Assignment:
 - : 42*42=>42
 0 : =>42
 < : 42*42=>48
 s : 42=>42
 if : 48*42*42=>42
 gcd : 42*42=>42
 mod : 42*42=>42
 true : =>48
 false : =>48
non-linear variables: {?x_9,?y_9,?y_11}
non-linear types: {42}
types leq non-linear types: {42}
rules applicable to terms of non-linear types:
   [ if(true,?x,?y) -> ?x,
     if(false,?x_1,?y_1) -> ?y_1,
     -(s(?x_2),s(?y_2)) -> -(?x_2,?y_2),
     -(?x_3,0) -> ?x_3,
     -(0,?x_4) -> 0,
     <(s(?x_5),s(?y_5)) -> <(?x_5,?y_5),
     <(0,s(?x_6)) -> true,
     <(?x_7,0) -> false,
     mod(0,?y_8) -> 0,
     mod(?x_9,s(?y_9)) -> if(<(?x_9,s(?y_9)),?x_9,mod(-(?x_9,s(?y_9)),s(?y_9))),
     mod(?x_10,0) -> ?x_10,
     gcd(?x_11,?y_11) -> gcd(?y_11,mod(?x_11,?y_11)),
     gcd(?x_12,0) -> ?x_12,
     gcd(0,?x_13) -> ?x_13 ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 24 rules by 3 steps unfolding
strenghten gcd(?x_13,mod(0,?x_13)) and ?x_13
strenghten gcd(0,mod(?x_12,0)) and ?x_12
strenghten gcd(0,mod(0,0)) and 0
strenghten if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))) and 0
obtain 31 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     -(s(?x),s(?y)) -> -(?x,?y),
     -(?x,0) -> ?x,
     -(0,?x) -> 0,
     <(s(?x),s(?y)) -> <(?x,?y),
     <(0,s(?x)) -> true,
     <(?x,0) -> false,
     mod(0,?y) -> 0,
     mod(?x,s(?y)) -> if(<(?x,s(?y)),?x,mod(-(?x,s(?y)),s(?y))),
     mod(?x,0) -> ?x,
     gcd(?x,?y) -> gcd(?y,mod(?x,?y)),
     gcd(?x,0) -> ?x,
     gcd(0,?x) -> ?x ]
Sort Assignment:
 - : 42*42=>42
 0 : =>42
 < : 42*42=>48
 s : 42=>42
 if : 48*42*42=>42
 gcd : 42*42=>42
 mod : 42*42=>42
 true : =>48
 false : =>48
maximal types: {42,48}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     -(s(?x),s(?y)) -> -(?x,?y),
     -(?x,0) -> ?x,
     -(0,?x) -> 0,
     <(s(?x),s(?y)) -> <(?x,?y),
     <(0,s(?x)) -> true,
     <(?x,0) -> false,
     mod(0,?y) -> 0,
     mod(?x,s(?y)) -> if(<(?x,s(?y)),?x,mod(-(?x,s(?y)),s(?y))),
     mod(?x,0) -> ?x,
     gcd(?x,?y) -> gcd(?y,mod(?x,?y)),
     gcd(?x,0) -> ?x,
     gcd(0,?x) -> ?x ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     -(s(?x),s(?y)) -> -(?x,?y),
     -(?x,0) -> ?x,
     -(0,?x) -> 0,
     <(s(?x),s(?y)) -> <(?x,?y),
     <(0,s(?x)) -> true,
     <(?x,0) -> false,
     mod(0,?y) -> 0,
     mod(?x,s(?y)) -> if(<(?x,s(?y)),?x,mod(-(?x,s(?y)),s(?y))),
     mod(?x,0) -> ?x,
     gcd(?x,?y) -> gcd(?y,mod(?x,?y)),
     gcd(?x,0) -> ?x,
     gcd(0,?x) -> ?x ]
Outside Critical Pair: <0, 0> by Rules <4, 3>
develop reducts from lhs term...
<{}, 0>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))), 0> by Rules <9, 8>
develop reducts from lhs term...
<{4,6,9}, if(true,0,if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))))>
<{6,9}, if(true,0,if(<(-(0,s(?y_9)),s(?y_9)),-(0,s(?y_9)),mod(-(-(0,s(?y_9)),s(?y_9)),s(?y_9))))>
<{4,6}, if(true,0,mod(0,s(?y_9)))>
<{6}, if(true,0,mod(-(0,s(?y_9)),s(?y_9)))>
<{4,9}, if(<(0,s(?y_9)),0,if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9))))>
<{9}, if(<(0,s(?y_9)),0,if(<(-(0,s(?y_9)),s(?y_9)),-(0,s(?y_9)),mod(-(-(0,s(?y_9)),s(?y_9)),s(?y_9))))>
<{4}, if(<(0,s(?y_9)),0,mod(0,s(?y_9)))>
<{}, if(<(0,s(?y_9)),0,mod(-(0,s(?y_9)),s(?y_9)))>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <0, 0> by Rules <10, 8>
develop reducts from lhs term...
<{}, 0>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <?x_12, gcd(0,mod(?x_12,0))> by Rules <12, 11>
develop reducts from lhs term...
<{}, ?x_12>
develop reducts from rhs term...
<{10,13}, ?x_12>
<{13}, mod(?x_12,0)>
<{10,11}, gcd(?x_12,mod(0,?x_12))>
<{11}, gcd(mod(?x_12,0),mod(0,mod(?x_12,0)))>
<{10}, gcd(0,?x_12)>
<{}, gcd(0,mod(?x_12,0))>
Outside Critical Pair: <?x_13, gcd(?x_13,mod(0,?x_13))> by Rules <13, 11>
develop reducts from lhs term...
<{}, ?x_13>
develop reducts from rhs term...
<{8,11}, gcd(0,mod(?x_13,0))>
<{11}, gcd(mod(0,?x_13),mod(?x_13,mod(0,?x_13)))>
<{8}, gcd(?x_13,0)>
<{}, gcd(?x_13,mod(0,?x_13))>
Outside Critical Pair: <0, 0> by Rules <13, 12>
develop reducts from lhs term...
<{}, 0>
develop reducts from rhs term...
<{}, 0>
Try A Minimal Decomposition {8,9}{13,11,12}{0}{1}{2}{3}{4}{5}{6}{7}{10}
{8,9}
(cm)Rewrite Rules:
   [ mod(0,?y) -> 0,
     mod(?x,s(?y)) -> if(<(?x,s(?y)),?x,mod(-(?x,s(?y)),s(?y))) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ 0 = if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))) = 0,
     0 = if(<(0,s(?y)),0,mod(-(0,s(?y)),s(?y))) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))), 0> by Rules <1, 0> preceded by []
unknown Diagram Decreasing
   [ mod(0,?y) -> 0,
     mod(?x_1,s(?y_1)) -> if(<(?x_1,s(?y_1)),?x_1,mod(-(?x_1,s(?y_1)),s(?y_1))) ]
Sort Assignment:
 - : 4*5=>4
 0 : =>4
 < : 4*5=>13
 s : 11=>5
 if : 13*4*4=>4
 mod : 4*5=>4
non-linear variables: {?x_1,?y_1}
non-linear types: {4,11}
types leq non-linear types: {4,11}
rules applicable to terms of non-linear types:
   [ mod(0,?y) -> 0,
     mod(?x_1,s(?y_1)) -> if(<(?x_1,s(?y_1)),?x_1,mod(-(?x_1,s(?y_1)),s(?y_1))) ]
NLR:
0: {}
1: {0,1}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ mod(0,?y) -> 0,
     mod(?x_1,s(?y_1)) -> if(<(?x_1,s(?y_1)),?x_1,mod(-(?x_1,s(?y_1)),s(?y_1))) ]
Sort Assignment:
 - : 4*5=>4
 0 : =>4
 < : 4*5=>13
 s : 11=>5
 if : 13*4*4=>4
 mod : 4*5=>4
non-linear variables: {?x_1,?y_1}
non-linear types: {4,11}
types leq non-linear types: {4,11}
rules applicable to terms of non-linear types:
   [ mod(0,?y) -> 0,
     mod(?x_1,s(?y_1)) -> if(<(?x_1,s(?y_1)),?x_1,mod(-(?x_1,s(?y_1)),s(?y_1))) ]
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
strenghten mod(0,?y_5) and 0
strenghten mod(0,0) and 0
strenghten mod(0,mod(0,?y_3)) and 0
strenghten mod(0,mod(0,0)) and 0
strenghten if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))) and 0
strenghten mod(0,if(<(?x_1,s(?y_1)),?x_1,mod(-(?x_1,s(?y_1)),s(?y_1)))) and 0
strenghten mod(0,if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1)))) and 0
strenghten mod(if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))),?y_5) and 0
strenghten mod(0,mod(0,if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))))) and 0
strenghten mod(0,mod(if(<(0,s(?y_1)),0,mod(-(0,s(?y_1)),s(?y_1))),?y_23)) and 0
strenghten if(<(mod(0,?y_4),s(?y_1)),mod(0,?y_4),mod(-(mod(0,?y_4),s(?y_1)),s(?y_1))) and 0
strenghten mod(0,if(<(mod(0,?y_22),s(?y_1)),mod(0,?y_22),mod(-(mod(0,?y_22),s(?y_1)),s(?y_1)))) and 0
obtain 45 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <if(<(0,s(c_1)),0,mod(-(0,s(c_1)),s(c_1))), 0>
Direct Methods: not CR
{13,11,12}
(cm)Rewrite Rules:
   [ gcd(0,?x) -> ?x,
     gcd(?x,?y) -> gcd(?y,mod(?x,?y)),
     gcd(?x,0) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ ?x = gcd(?x,mod(0,?x)),
     0 = 0,
     gcd(0,mod(?x_1,0)) = ?x_1 ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ gcd(?x,mod(0,?x)) = ?x,
     0 = 0,
     ?y = gcd(?y,mod(0,?y)),
     ?x = gcd(0,mod(?x,0)),
     gcd(0,mod(?x,0)) = ?x ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <gcd(?y_1,mod(0,?y_1)), ?y_1> by Rules <1, 0> preceded by []
unknown Diagram Decreasing
   [ gcd(0,?x) -> ?x,
     gcd(?x_1,?y_1) -> gcd(?y_1,mod(?x_1,?y_1)),
     gcd(?x_2,0) -> ?x_2 ]
Sort Assignment:
 0 : =>12
 gcd : 12*12=>12
 mod : 12*12=>12
non-linear variables: {?y_1}
non-linear types: {12}
types leq non-linear types: {12}
rules applicable to terms of non-linear types:
   [ gcd(0,?x) -> ?x,
     gcd(?x_1,?y_1) -> gcd(?y_1,mod(?x_1,?y_1)),
     gcd(?x_2,0) -> ?x_2 ]
NLR:
0: {}
1: {0,1,2}
2: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ gcd(0,?x) -> ?x,
     gcd(?x_1,?y_1) -> gcd(?y_1,mod(?x_1,?y_1)),
     gcd(?x_2,0) -> ?x_2 ]
Sort Assignment:
 0 : =>12
 gcd : 12*12=>12
 mod : 12*12=>12
non-linear variables: {?y_1}
non-linear types: {12}
types leq non-linear types: {12}
rules applicable to terms of non-linear types:
   [ gcd(0,?x) -> ?x,
     gcd(?x_1,?y_1) -> gcd(?y_1,mod(?x_1,?y_1)),
     gcd(?x_2,0) -> ?x_2 ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 13 rules by 3 steps unfolding
strenghten gcd(?x_8,0) and ?x_8
strenghten gcd(0,?x_2) and ?x_2
strenghten gcd(0,0) and 0
strenghten mod(?x_5,0) and ?x_5
strenghten mod(0,0) and 0
strenghten gcd(?x_4,mod(0,?x_4)) and ?x_4
strenghten gcd(?x_8,mod(0,0)) and ?x_8
strenghten gcd(0,mod(?x_2,0)) and ?x_2
strenghten gcd(0,mod(?x_5,0)) and mod(?x_5,0)
strenghten gcd(?x_8,gcd(0,mod(0,0))) and ?x_8
strenghten gcd(0,gcd(0,mod(?x_1,0))) and ?x_1
strenghten gcd(gcd(?x_12,0),mod(0,gcd(?x_12,0))) and ?x_12
strenghten gcd(gcd(0,0),mod(?x_8,gcd(0,0))) and ?x_8
obtain 52 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <mod(0,0), 0>
Direct Methods: not CR
{0}
(cm)Rewrite Rules:
   [ if(true,?x,?y) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{1}
(cm)Rewrite Rules:
   [ if(false,?x,?y) -> ?y ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{2}
(cm)Rewrite Rules:
   [ -(s(?x),s(?y)) -> -(?x,?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{3}
(cm)Rewrite Rules:
   [ -(?x,0) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{4}
(cm)Rewrite Rules:
   [ -(0,?x) -> 0 ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{5}
(cm)Rewrite Rules:
   [ <(s(?x),s(?y)) -> <(?x,?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{6}
(cm)Rewrite Rules:
   [ <(0,s(?x)) -> true ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{7}
(cm)Rewrite Rules:
   [ <(?x,0) -> false ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
{10}
(cm)Rewrite Rules:
   [ mod(?x,0) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
62.trs: Failure(unknown)
(6360 msec.)