3.50/3.52	MAYBE
3.50/3.52	(ignored inputs)COMMENT doi:10.4230/LIPIcs.FSCD.2016.10 [91] derived from Figure 1 , with modified conditions in last two rules to conform to Haskell's evaluation strategy; cf. Cops #499 submitted by: Thomas Sternagel
3.50/3.52	Conditional Rewrite Rules:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.52	     mult(0,?y) -> 0,
3.50/3.52	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.52	     lte(0,?y) -> true,
3.50/3.52	     lte(s(?x),0) -> false,
3.50/3.52	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.52	     minus(0,s(?y)) -> 0,
3.50/3.52	     minus(?x,0) -> ?x,
3.50/3.52	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.52	     mod(0,?y) -> 0,
3.50/3.52	     mod(?x,0) -> ?x,
3.50/3.52	     mod(?x,s(?y)) -> mod(minus(?x,s(?y)),s(?y)) | lte(s(?y),?x) == true,
3.50/3.52	     mod(?x,s(?y)) -> ?x | lte(s(?y),?x) == false,
3.50/3.52	     div(0,s(?x)) -> 0,
3.50/3.52	     div(s(?x),s(?y)) -> 0 | lte(s(?x),?y) == true,
3.50/3.52	     div(s(?x),s(?y)) -> s(?q) | lte(s(?x),?y) == false,div(minus(?x,?y),s(?y)) == ?q,
3.50/3.52	     power(?x,0) -> s(0),
3.50/3.52	     power(?x,?n) -> mult(mult(?y,?y),s(0)) | ?n == s(?n'),mod(?n,s(s(0))) == 0,power(?x,div(?n,s(s(0)))) == ?y,
3.50/3.52	     power(?x,?n) -> mult(mult(?y,?y),?x) | ?n == s(?n'),mod(?n,s(s(0))) == s(?z),power(?x,div(?n,s(s(0)))) == ?y ]
3.50/3.52	Check whether all rules are type 3
3.50/3.52	OK
3.50/3.52	Check whether the input is deterministic
3.50/3.52	OK
3.50/3.52	Result of unraveling:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.52	     mult(0,?y) -> 0,
3.50/3.52	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.52	     lte(0,?y) -> true,
3.50/3.52	     lte(s(?x),0) -> false,
3.50/3.52	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.52	     minus(0,s(?y)) -> 0,
3.50/3.52	     minus(?x,0) -> ?x,
3.50/3.52	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.52	     mod(0,?y) -> 0,
3.50/3.52	     mod(?x,0) -> ?x,
3.50/3.52	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.52	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.52	     U1(false,?x,?y) -> ?x,
3.50/3.52	     div(0,s(?x)) -> 0,
3.50/3.52	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.52	     U3(true,?x,?y) -> 0,
3.50/3.52	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.52	     U4(?q,?x,?y) -> s(?q),
3.50/3.52	     power(?x,0) -> s(0),
3.50/3.52	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.52	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.52	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.52	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.52	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.52	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.52	Check whether U(R) is terminating
3.50/3.52	failed to show termination
3.50/3.52	Check whether the input is weakly left-linear
3.50/3.52	OK
3.50/3.52	Conditional critical pairs (CCPs):
3.50/3.52	   [ 0 = 0,
3.50/3.52	     mod(minus(0,s(?y_12)),s(?y_12)) = 0 | lte(s(?y_12),0) == true,
3.50/3.52	     0 = 0 | lte(s(?y_13),0) == false,
3.50/3.52	     0 = 0,
3.50/3.52	     0 = mod(minus(0,s(?y_12)),s(?y_12)) | lte(s(?y_12),0) == true,
3.50/3.52	     ?x_13 = mod(minus(?x_13,s(?y_13)),s(?y_13)) | lte(s(?y_13),?x_13) == false,lte(s(?y_13),?x_13) == true,
3.50/3.52	     0 = 0 | lte(s(?y_13),0) == false,
3.50/3.52	     mod(minus(?x_12,s(?y_12)),s(?y_12)) = ?x_12 | lte(s(?y_12),?x_12) == true,lte(s(?y_12),?x_12) == false,
3.50/3.52	     s(?q_16) = 0 | lte(s(?x_16),?y_16) == false,div(minus(?x_16,?y_16),s(?y_16)) == ?q_16,lte(s(?x_16),?y_16) == true,
3.50/3.52	     0 = s(?q_16) | lte(s(?x_15),?y_15) == true,lte(s(?x_15),?y_15) == false,div(minus(?x_15,?y_15),s(?y_15)) == ?q_16,
3.50/3.52	     mult(mult(?y_18,?y_18),s(0)) = s(0) | 0 == s(?n'_18),mod(0,s(s(0))) == 0,power(?x_18,div(0,s(s(0)))) == ?y_18,
3.50/3.52	     mult(mult(?y_19,?y_19),?x_19) = s(0) | 0 == s(?n'_19),mod(0,s(s(0))) == s(?z_19),power(?x_19,div(0,s(s(0)))) == ?y_19,
3.50/3.52	     s(0) = mult(mult(?y_18,?y_18),s(0)) | 0 == s(?n'_18),mod(0,s(s(0))) == 0,power(?x_17,div(0,s(s(0)))) == ?y_18,
3.50/3.52	     mult(mult(?y_19,?y_19),?x_19) = mult(mult(?y_18,?y_18),s(0)) | ?n_19 == s(?n'_19),mod(?n_19,s(s(0))) == s(?z_19),power(?x_19,div(?n_19,s(s(0)))) == ?y_19,?n_19 == s(?n'_18),mod(?n_19,s(s(0))) == 0,power(?x_19,div(?n_19,s(s(0)))) == ?y_18,
3.50/3.52	     s(0) = mult(mult(?y_19,?y_19),?x_17) | 0 == s(?n'_19),mod(0,s(s(0))) == s(?z_19),power(?x_17,div(0,s(s(0)))) == ?y_19,
3.50/3.52	     mult(mult(?y_18,?y_18),s(0)) = mult(mult(?y_19,?y_19),?x_18) | ?n_18 == s(?n'_18),mod(?n_18,s(s(0))) == 0,power(?x_18,div(?n_18,s(s(0)))) == ?y_18,?n_18 == s(?n'_19),mod(?n_18,s(s(0))) == s(?z_19),power(?x_18,div(?n_18,s(s(0)))) == ?y_19 ]
3.50/3.52	Check whether the input is almost orthogonale
3.50/3.52	not almost orthogonal
3.50/3.52	OK
3.50/3.52	Check U(R) is confluent
3.50/3.52	Rewrite Rules:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.52	     mult(0,?y) -> 0,
3.50/3.52	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.52	     lte(0,?y) -> true,
3.50/3.52	     lte(s(?x),0) -> false,
3.50/3.52	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.52	     minus(0,s(?y)) -> 0,
3.50/3.52	     minus(?x,0) -> ?x,
3.50/3.52	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.52	     mod(0,?y) -> 0,
3.50/3.52	     mod(?x,0) -> ?x,
3.50/3.52	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.52	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.52	     U1(false,?x,?y) -> ?x,
3.50/3.52	     div(0,s(?x)) -> 0,
3.50/3.52	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.52	     U3(true,?x,?y) -> 0,
3.50/3.52	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.52	     U4(?q,?x,?y) -> s(?q),
3.50/3.52	     power(?x,0) -> s(0),
3.50/3.52	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.52	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.52	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.52	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.52	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.52	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.52	Apply Direct Methods...
3.50/3.52	Inner CPs:
3.50/3.52	   [  ]
3.50/3.52	Outer CPs:
3.50/3.52	   [ 0 = 0,
3.50/3.52	     0 = U1(lte(s(?y_12),0),0,?y_12),
3.50/3.52	     s(0) = U8(0,0,?x_20) ]
3.50/3.52	Overlay, check Innermost Termination...
3.50/3.52	unknown Innermost Terminating
3.50/3.52	unknown Knuth & Bendix
3.50/3.52	Left-Linear, not Right-Linear
3.50/3.52	unknown Development Closed
3.50/3.52	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
3.50/3.52	unknown Upside-Parallel-Closed/Outside-Closed
3.50/3.52	(inner) Parallel CPs: (not computed)
3.50/3.52	unknown Toyama (Parallel CPs)
3.50/3.52	Simultaneous CPs:
3.50/3.52	   [ 0 = 0,
3.50/3.52	     U1(lte(s(?y_12),0),0,?y_12) = 0,
3.50/3.52	     0 = U1(lte(s(?y),0),0,?y),
3.50/3.52	     U8(0,0,?x) = s(0),
3.50/3.52	     s(0) = U8(0,0,?x) ]
3.50/3.52	unknown Okui (Simultaneous CPs)
3.50/3.52	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
3.50/3.52	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
3.50/3.52	check Locally Decreasing Diagrams by Rule Labelling...
3.50/3.52	Critical Pair <0, 0> by Rules <11, 10> preceded by []
3.50/3.52	 joinable by a reduction of rules <[], []>
3.50/3.52	Critical Pair <U1(lte(s(?y_12),0),0,?y_12), 0> by Rules <12, 10> preceded by []
3.50/3.52	 joinable by a reduction of rules <[([(U1,1)],5),([],14)], []>
3.50/3.52	Critical Pair <U8(0,0,?x_21), s(0)> by Rules <21, 20> preceded by []
3.50/3.52	unknown Diagram Decreasing
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x_1),?y_1) -> s(add(?x_1,?y_1)),
3.50/3.52	     mult(0,?y_2) -> 0,
3.50/3.52	     mult(s(?x_3),?y_3) -> add(mult(?x_3,?y_3),?y_3),
3.50/3.52	     lte(0,?y_4) -> true,
3.50/3.52	     lte(s(?x_5),0) -> false,
3.50/3.52	     lte(s(?x_6),s(?y_6)) -> lte(?x_6,?y_6),
3.50/3.52	     minus(0,s(?y_7)) -> 0,
3.50/3.52	     minus(?x_8,0) -> ?x_8,
3.50/3.52	     minus(s(?x_9),s(?y_9)) -> minus(?x_9,?y_9),
3.50/3.52	     mod(0,?y_10) -> 0,
3.50/3.52	     mod(?x_11,0) -> ?x_11,
3.50/3.52	     mod(?x_12,s(?y_12)) -> U1(lte(s(?y_12),?x_12),?x_12,?y_12),
3.50/3.52	     U1(true,?x_13,?y_13) -> mod(minus(?x_13,s(?y_13)),s(?y_13)),
3.50/3.52	     U1(false,?x_14,?y_14) -> ?x_14,
3.50/3.52	     div(0,s(?x_15)) -> 0,
3.50/3.52	     div(s(?x_16),s(?y_16)) -> U3(lte(s(?x_16),?y_16),?x_16,?y_16),
3.50/3.52	     U3(true,?x_17,?y_17) -> 0,
3.50/3.52	     U3(false,?x_18,?y_18) -> U4(div(minus(?x_18,?y_18),s(?y_18)),?x_18,?y_18),
3.50/3.52	     U4(?q_19,?x_19,?y_19) -> s(?q_19),
3.50/3.52	     power(?x_20,0) -> s(0),
3.50/3.52	     power(?x_21,?n_21) -> U8(?n_21,?n_21,?x_21),
3.50/3.52	     U8(s(?n'_22),?n_22,?x_22) -> U9(mod(?n_22,s(s(0))),?n_22,?x_22,?n'_22),
3.50/3.52	     U9(0,?n_23,?x_23,?n'_23) -> U7(power(?x_23,div(?n_23,s(s(0)))),?n_23,?x_23,?n'_23),
3.50/3.52	     U7(?y_24,?n_24,?x_24,?n'_24) -> mult(mult(?y_24,?y_24),s(0)),
3.50/3.52	     U9(s(?z_25),?n_25,?x_25,?n'_25) -> U10(power(?x_25,div(?n_25,s(s(0)))),?n_25,?x_25,?n'_25,?z_25),
3.50/3.52	     U10(?y_26,?n_26,?x_26,?n'_26,?z_26) -> mult(mult(?y_26,?y_26),?x_26) ]
3.50/3.52	Sort Assignment:
3.50/3.52	 0 : =>113
3.50/3.52	 s : 113=>113
3.50/3.52	 U1 : 62*113*113=>113
3.50/3.52	 U3 : 62*113*113=>113
3.50/3.52	 U4 : 113*113*113=>113
3.50/3.52	 U7 : 113*113*113*113=>113
3.50/3.52	 U8 : 113*113*113=>113
3.50/3.52	 U9 : 113*113*113*113=>113
3.50/3.52	 U10 : 113*113*113*113*113=>113
3.50/3.52	 add : 113*113=>113
3.50/3.52	 div : 113*113=>113
3.50/3.52	 lte : 113*113=>62
3.50/3.52	 mod : 113*113=>113
3.50/3.52	 mult : 113*113=>113
3.50/3.52	 true : =>62
3.50/3.52	 false : =>62
3.50/3.52	 minus : 113*113=>113
3.50/3.52	 power : 113*113=>113
3.50/3.52	non-linear variables: {?y_3,?y_12,?x_12,?y_13,?x_16,?y_16,?x_18,?y_18,?n_21,?n_22,?x_23,?n_23,?y_24,?x_25,?n_25,?y_26}
3.50/3.52	non-linear types: {113}
3.50/3.52	types leq non-linear types: {113}
3.50/3.52	rules applicable to terms of non-linear types:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x_1),?y_1) -> s(add(?x_1,?y_1)),
3.50/3.52	     mult(0,?y_2) -> 0,
3.50/3.52	     mult(s(?x_3),?y_3) -> add(mult(?x_3,?y_3),?y_3),
3.50/3.52	     lte(0,?y_4) -> true,
3.50/3.52	     lte(s(?x_5),0) -> false,
3.50/3.52	     lte(s(?x_6),s(?y_6)) -> lte(?x_6,?y_6),
3.50/3.52	     minus(0,s(?y_7)) -> 0,
3.50/3.52	     minus(?x_8,0) -> ?x_8,
3.50/3.52	     minus(s(?x_9),s(?y_9)) -> minus(?x_9,?y_9),
3.50/3.52	     mod(0,?y_10) -> 0,
3.50/3.52	     mod(?x_11,0) -> ?x_11,
3.50/3.52	     mod(?x_12,s(?y_12)) -> U1(lte(s(?y_12),?x_12),?x_12,?y_12),
3.50/3.52	     U1(true,?x_13,?y_13) -> mod(minus(?x_13,s(?y_13)),s(?y_13)),
3.50/3.52	     U1(false,?x_14,?y_14) -> ?x_14,
3.50/3.52	     div(0,s(?x_15)) -> 0,
3.50/3.52	     div(s(?x_16),s(?y_16)) -> U3(lte(s(?x_16),?y_16),?x_16,?y_16),
3.50/3.52	     U3(true,?x_17,?y_17) -> 0,
3.50/3.52	     U3(false,?x_18,?y_18) -> U4(div(minus(?x_18,?y_18),s(?y_18)),?x_18,?y_18),
3.50/3.52	     U4(?q_19,?x_19,?y_19) -> s(?q_19),
3.50/3.52	     power(?x_20,0) -> s(0),
3.50/3.52	     power(?x_21,?n_21) -> U8(?n_21,?n_21,?x_21),
3.50/3.52	     U8(s(?n'_22),?n_22,?x_22) -> U9(mod(?n_22,s(s(0))),?n_22,?x_22,?n'_22),
3.50/3.52	     U9(0,?n_23,?x_23,?n'_23) -> U7(power(?x_23,div(?n_23,s(s(0)))),?n_23,?x_23,?n'_23),
3.50/3.52	     U7(?y_24,?n_24,?x_24,?n'_24) -> mult(mult(?y_24,?y_24),s(0)),
3.50/3.52	     U9(s(?z_25),?n_25,?x_25,?n'_25) -> U10(power(?x_25,div(?n_25,s(s(0)))),?n_25,?x_25,?n'_25,?z_25),
3.50/3.52	     U10(?y_26,?n_26,?x_26,?n'_26,?z_26) -> mult(mult(?y_26,?y_26),?x_26) ]
3.50/3.52	Rnl:
3.50/3.52	0: {}
3.50/3.52	1: {}
3.50/3.52	2: {}
3.50/3.52	3: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	4: {}
3.50/3.52	5: {}
3.50/3.52	6: {}
3.50/3.52	7: {}
3.50/3.52	8: {}
3.50/3.52	9: {}
3.50/3.52	10: {}
3.50/3.52	11: {}
3.50/3.52	12: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	13: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	14: {}
3.50/3.52	15: {}
3.50/3.52	16: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	17: {}
3.50/3.52	18: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	19: {}
3.50/3.52	20: {}
3.50/3.52	21: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	22: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	23: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	24: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	25: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	26: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26}
3.50/3.52	unknown innermost-termination for terms of non-linear types
3.50/3.52	unknown Quasi-Linear & Linearized-Decreasing
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x_1),?y_1) -> s(add(?x_1,?y_1)),
3.50/3.52	     mult(0,?y_2) -> 0,
3.50/3.52	     mult(s(?x_3),?y_3) -> add(mult(?x_3,?y_3),?y_3),
3.50/3.52	     lte(0,?y_4) -> true,
3.50/3.52	     lte(s(?x_5),0) -> false,
3.50/3.52	     lte(s(?x_6),s(?y_6)) -> lte(?x_6,?y_6),
3.50/3.52	     minus(0,s(?y_7)) -> 0,
3.50/3.52	     minus(?x_8,0) -> ?x_8,
3.50/3.52	     minus(s(?x_9),s(?y_9)) -> minus(?x_9,?y_9),
3.50/3.52	     mod(0,?y_10) -> 0,
3.50/3.52	     mod(?x_11,0) -> ?x_11,
3.50/3.52	     mod(?x_12,s(?y_12)) -> U1(lte(s(?y_12),?x_12),?x_12,?y_12),
3.50/3.52	     U1(true,?x_13,?y_13) -> mod(minus(?x_13,s(?y_13)),s(?y_13)),
3.50/3.52	     U1(false,?x_14,?y_14) -> ?x_14,
3.50/3.52	     div(0,s(?x_15)) -> 0,
3.50/3.52	     div(s(?x_16),s(?y_16)) -> U3(lte(s(?x_16),?y_16),?x_16,?y_16),
3.50/3.52	     U3(true,?x_17,?y_17) -> 0,
3.50/3.52	     U3(false,?x_18,?y_18) -> U4(div(minus(?x_18,?y_18),s(?y_18)),?x_18,?y_18),
3.50/3.52	     U4(?q_19,?x_19,?y_19) -> s(?q_19),
3.50/3.52	     power(?x_20,0) -> s(0),
3.50/3.52	     power(?x_21,?n_21) -> U8(?n_21,?n_21,?x_21),
3.50/3.52	     U8(s(?n'_22),?n_22,?x_22) -> U9(mod(?n_22,s(s(0))),?n_22,?x_22,?n'_22),
3.50/3.52	     U9(0,?n_23,?x_23,?n'_23) -> U7(power(?x_23,div(?n_23,s(s(0)))),?n_23,?x_23,?n'_23),
3.50/3.52	     U7(?y_24,?n_24,?x_24,?n'_24) -> mult(mult(?y_24,?y_24),s(0)),
3.50/3.52	     U9(s(?z_25),?n_25,?x_25,?n'_25) -> U10(power(?x_25,div(?n_25,s(s(0)))),?n_25,?x_25,?n'_25,?z_25),
3.50/3.52	     U10(?y_26,?n_26,?x_26,?n'_26,?z_26) -> mult(mult(?y_26,?y_26),?x_26) ]
3.50/3.52	Sort Assignment:
3.50/3.52	 0 : =>113
3.50/3.52	 s : 113=>113
3.50/3.52	 U1 : 62*113*113=>113
3.50/3.52	 U3 : 62*113*113=>113
3.50/3.52	 U4 : 113*113*113=>113
3.50/3.52	 U7 : 113*113*113*113=>113
3.50/3.52	 U8 : 113*113*113=>113
3.50/3.52	 U9 : 113*113*113*113=>113
3.50/3.52	 U10 : 113*113*113*113*113=>113
3.50/3.52	 add : 113*113=>113
3.50/3.52	 div : 113*113=>113
3.50/3.52	 lte : 113*113=>62
3.50/3.52	 mod : 113*113=>113
3.50/3.52	 mult : 113*113=>113
3.50/3.52	 true : =>62
3.50/3.52	 false : =>62
3.50/3.52	 minus : 113*113=>113
3.50/3.52	 power : 113*113=>113
3.50/3.52	non-linear variables: {?y_3,?y_12,?x_12,?y_13,?x_16,?y_16,?x_18,?y_18,?n_21,?n_22,?x_23,?n_23,?y_24,?x_25,?n_25,?y_26}
3.50/3.52	non-linear types: {113}
3.50/3.52	types leq non-linear types: {113}
3.50/3.52	rules applicable to terms of non-linear types:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x_1),?y_1) -> s(add(?x_1,?y_1)),
3.50/3.52	     mult(0,?y_2) -> 0,
3.50/3.52	     mult(s(?x_3),?y_3) -> add(mult(?x_3,?y_3),?y_3),
3.50/3.52	     lte(0,?y_4) -> true,
3.50/3.52	     lte(s(?x_5),0) -> false,
3.50/3.52	     lte(s(?x_6),s(?y_6)) -> lte(?x_6,?y_6),
3.50/3.52	     minus(0,s(?y_7)) -> 0,
3.50/3.52	     minus(?x_8,0) -> ?x_8,
3.50/3.52	     minus(s(?x_9),s(?y_9)) -> minus(?x_9,?y_9),
3.50/3.52	     mod(0,?y_10) -> 0,
3.50/3.52	     mod(?x_11,0) -> ?x_11,
3.50/3.52	     mod(?x_12,s(?y_12)) -> U1(lte(s(?y_12),?x_12),?x_12,?y_12),
3.50/3.52	     U1(true,?x_13,?y_13) -> mod(minus(?x_13,s(?y_13)),s(?y_13)),
3.50/3.52	     U1(false,?x_14,?y_14) -> ?x_14,
3.50/3.52	     div(0,s(?x_15)) -> 0,
3.50/3.52	     div(s(?x_16),s(?y_16)) -> U3(lte(s(?x_16),?y_16),?x_16,?y_16),
3.50/3.52	     U3(true,?x_17,?y_17) -> 0,
3.50/3.52	     U3(false,?x_18,?y_18) -> U4(div(minus(?x_18,?y_18),s(?y_18)),?x_18,?y_18),
3.50/3.52	     U4(?q_19,?x_19,?y_19) -> s(?q_19),
3.50/3.52	     power(?x_20,0) -> s(0),
3.50/3.52	     power(?x_21,?n_21) -> U8(?n_21,?n_21,?x_21),
3.50/3.52	     U8(s(?n'_22),?n_22,?x_22) -> U9(mod(?n_22,s(s(0))),?n_22,?x_22,?n'_22),
3.50/3.52	     U9(0,?n_23,?x_23,?n'_23) -> U7(power(?x_23,div(?n_23,s(s(0)))),?n_23,?x_23,?n'_23),
3.50/3.52	     U7(?y_24,?n_24,?x_24,?n'_24) -> mult(mult(?y_24,?y_24),s(0)),
3.50/3.52	     U9(s(?z_25),?n_25,?x_25,?n'_25) -> U10(power(?x_25,div(?n_25,s(s(0)))),?n_25,?x_25,?n'_25,?z_25),
3.50/3.52	     U10(?y_26,?n_26,?x_26,?n'_26,?z_26) -> mult(mult(?y_26,?y_26),?x_26) ]
3.50/3.52	unknown innermost-termination for terms of non-linear types
3.50/3.52	unknown Strongly Quasi-Linear & Hierarchically Decreasing
3.50/3.52	unknown Huet (modulo AC)
3.50/3.52	check by Reduction-Preserving Completion...
3.50/3.52	failure(empty P)
3.50/3.52	unknown Reduction-Preserving Completion
3.50/3.52	check by Ordered Rewriting...
3.50/3.52	remove redundants rules and split
3.50/3.52	R-part:
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.52	     mult(0,?y) -> 0,
3.50/3.52	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.52	     lte(0,?y) -> true,
3.50/3.52	     lte(s(?x),0) -> false,
3.50/3.52	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.52	     minus(0,s(?y)) -> 0,
3.50/3.52	     minus(?x,0) -> ?x,
3.50/3.52	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.52	     mod(0,?y) -> 0,
3.50/3.52	     mod(?x,0) -> ?x,
3.50/3.52	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.52	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.52	     U1(false,?x,?y) -> ?x,
3.50/3.52	     div(0,s(?x)) -> 0,
3.50/3.52	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.52	     U3(true,?x,?y) -> 0,
3.50/3.52	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.52	     U4(?q,?x,?y) -> s(?q),
3.50/3.52	     power(?x,0) -> s(0),
3.50/3.52	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.52	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.52	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.52	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.52	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.52	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.52	E-part:
3.50/3.52	   [ ]
3.50/3.52	...failed to find a suitable LPO.
3.50/3.52	unknown Confluence by Ordered Rewriting
3.50/3.52	Direct Methods: Can't judge
3.50/3.52	
3.50/3.52	Try Persistent Decomposition for...
3.50/3.52	   [ add(0,?x) -> ?x,
3.50/3.52	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.52	     mult(0,?y) -> 0,
3.50/3.52	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.52	     lte(0,?y) -> true,
3.50/3.52	     lte(s(?x),0) -> false,
3.50/3.52	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.52	     minus(0,s(?y)) -> 0,
3.50/3.52	     minus(?x,0) -> ?x,
3.50/3.52	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.52	     mod(0,?y) -> 0,
3.50/3.52	     mod(?x,0) -> ?x,
3.50/3.52	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.52	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.52	     U1(false,?x,?y) -> ?x,
3.50/3.52	     div(0,s(?x)) -> 0,
3.50/3.52	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.52	     U3(true,?x,?y) -> 0,
3.50/3.52	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.52	     U4(?q,?x,?y) -> s(?q),
3.50/3.52	     power(?x,0) -> s(0),
3.50/3.52	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.52	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.52	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.52	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.52	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.52	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.53	Sort Assignment:
3.50/3.53	 0 : =>113
3.50/3.53	 s : 113=>113
3.50/3.53	 U1 : 62*113*113=>113
3.50/3.53	 U3 : 62*113*113=>113
3.50/3.53	 U4 : 113*113*113=>113
3.50/3.53	 U7 : 113*113*113*113=>113
3.50/3.53	 U8 : 113*113*113=>113
3.50/3.53	 U9 : 113*113*113*113=>113
3.50/3.53	 U10 : 113*113*113*113*113=>113
3.50/3.53	 add : 113*113=>113
3.50/3.53	 div : 113*113=>113
3.50/3.53	 lte : 113*113=>62
3.50/3.53	 mod : 113*113=>113
3.50/3.53	 mult : 113*113=>113
3.50/3.53	 true : =>62
3.50/3.53	 false : =>62
3.50/3.53	 minus : 113*113=>113
3.50/3.53	 power : 113*113=>113
3.50/3.53	maximal types: {62,113}
3.50/3.53	Persistent Decomposition failed: Can't judge
3.50/3.53	
3.50/3.53	Try Layer Preserving Decomposition for...
3.50/3.53	   [ add(0,?x) -> ?x,
3.50/3.53	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.53	     mult(0,?y) -> 0,
3.50/3.53	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.53	     lte(0,?y) -> true,
3.50/3.53	     lte(s(?x),0) -> false,
3.50/3.53	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.53	     minus(0,s(?y)) -> 0,
3.50/3.53	     minus(?x,0) -> ?x,
3.50/3.53	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.53	     mod(0,?y) -> 0,
3.50/3.53	     mod(?x,0) -> ?x,
3.50/3.53	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.53	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.53	     U1(false,?x,?y) -> ?x,
3.50/3.53	     div(0,s(?x)) -> 0,
3.50/3.53	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.53	     U3(true,?x,?y) -> 0,
3.50/3.53	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.53	     U4(?q,?x,?y) -> s(?q),
3.50/3.53	     power(?x,0) -> s(0),
3.50/3.53	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.53	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.53	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.53	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.53	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.53	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.53	Layer Preserving Decomposition failed: Can't judge
3.50/3.53	
3.50/3.53	Try Commutative Decomposition for...
3.50/3.53	   [ add(0,?x) -> ?x,
3.50/3.53	     add(s(?x),?y) -> s(add(?x,?y)),
3.50/3.53	     mult(0,?y) -> 0,
3.50/3.53	     mult(s(?x),?y) -> add(mult(?x,?y),?y),
3.50/3.53	     lte(0,?y) -> true,
3.50/3.53	     lte(s(?x),0) -> false,
3.50/3.53	     lte(s(?x),s(?y)) -> lte(?x,?y),
3.50/3.53	     minus(0,s(?y)) -> 0,
3.50/3.53	     minus(?x,0) -> ?x,
3.50/3.53	     minus(s(?x),s(?y)) -> minus(?x,?y),
3.50/3.53	     mod(0,?y) -> 0,
3.50/3.53	     mod(?x,0) -> ?x,
3.50/3.53	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y),
3.50/3.53	     U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)),
3.50/3.53	     U1(false,?x,?y) -> ?x,
3.50/3.53	     div(0,s(?x)) -> 0,
3.50/3.53	     div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y),
3.50/3.53	     U3(true,?x,?y) -> 0,
3.50/3.53	     U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y),
3.50/3.53	     U4(?q,?x,?y) -> s(?q),
3.50/3.53	     power(?x,0) -> s(0),
3.50/3.53	     power(?x,?n) -> U8(?n,?n,?x),
3.50/3.53	     U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n'),
3.50/3.53	     U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n'),
3.50/3.53	     U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)),
3.50/3.53	     U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z),
3.50/3.53	     U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.53	Outside Critical Pair: <0, 0> by Rules <11, 10>
3.50/3.53	develop reducts from lhs term...
3.50/3.53	<{}, 0>
3.50/3.53	develop reducts from rhs term...
3.50/3.53	<{}, 0>
3.50/3.53	Outside Critical Pair: <U1(lte(s(?y_12),0),0,?y_12), 0> by Rules <12, 10>
3.50/3.53	develop reducts from lhs term...
3.50/3.53	<{5}, U1(false,0,?y_12)>
3.50/3.53	<{}, U1(lte(s(?y_12),0),0,?y_12)>
3.50/3.53	develop reducts from rhs term...
3.50/3.53	<{}, 0>
3.50/3.53	Outside Critical Pair: <U8(0,0,?x_21), s(0)> by Rules <21, 20>
3.50/3.53	develop reducts from lhs term...
3.50/3.53	<{}, U8(0,0,?x_21)>
3.50/3.53	develop reducts from rhs term...
3.50/3.53	<{}, s(0)>
3.50/3.53	Try A Minimal Decomposition {10,12}{20,21}{0}{1}{2}{3}{4}{5}{6}{7}{8}{9}{11}{13}{14}{15}{16}{17}{18}{19}{22}{23}{24}{25}{26}
3.50/3.53	{10,12}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ mod(0,?y) -> 0,
3.50/3.53	     mod(?x,s(?y)) -> U1(lte(s(?y),?x),?x,?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [ 0 = U1(lte(s(?y_1),0),0,?y_1) ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), not WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: not CR
3.50/3.53	{20,21}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ power(?x,0) -> s(0),
3.50/3.53	     power(?x,?n) -> U8(?n,?n,?x) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [ s(0) = U8(0,0,?x) ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), not WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: not CR
3.50/3.53	{0}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ add(0,?x) -> ?x ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{1}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ add(s(?x),?y) -> s(add(?x,?y)) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{2}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ mult(0,?y) -> 0 ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{3}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ mult(s(?x),?y) -> add(mult(?x,?y),?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{4}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ lte(0,?y) -> true ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{5}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ lte(s(?x),0) -> false ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{6}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ lte(s(?x),s(?y)) -> lte(?x,?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{7}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ minus(0,s(?y)) -> 0 ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{8}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ minus(?x,0) -> ?x ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{9}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ minus(s(?x),s(?y)) -> minus(?x,?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{11}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ mod(?x,0) -> ?x ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{13}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U1(true,?x,?y) -> mod(minus(?x,s(?y)),s(?y)) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{14}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U1(false,?x,?y) -> ?x ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{15}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ div(0,s(?x)) -> 0 ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{16}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ div(s(?x),s(?y)) -> U3(lte(s(?x),?y),?x,?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{17}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U3(true,?x,?y) -> 0 ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{18}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U3(false,?x,?y) -> U4(div(minus(?x,?y),s(?y)),?x,?y) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{19}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U4(?q,?x,?y) -> s(?q) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{22}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U8(s(?n'),?n,?x) -> U9(mod(?n,s(s(0))),?n,?x,?n') ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{23}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U9(0,?n,?x,?n') -> U7(power(?x,div(?n,s(s(0)))),?n,?x,?n') ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{24}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U7(?y,?n,?x,?n') -> mult(mult(?y,?y),s(0)) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{25}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U9(s(?z),?n,?x,?n') -> U10(power(?x,div(?n,s(s(0)))),?n,?x,?n',?z) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	{26}
3.50/3.53	(cm)Rewrite Rules:
3.50/3.53	   [ U10(?y,?n,?x,?n',?z) -> mult(mult(?y,?y),?x) ]
3.50/3.53	Apply Direct Methods...
3.50/3.53	Inner CPs:
3.50/3.53	   [  ]
3.50/3.53	Outer CPs:
3.50/3.53	   [  ]
3.50/3.53	Overlay, check Innermost Termination...
3.50/3.53	Innermost Terminating (hence Terminating), WCR
3.50/3.53	Knuth & Bendix
3.50/3.53	Direct Methods: CR
3.50/3.53	Commutative Decomposition failed: Can't judge
3.50/3.53	No further decomposition possible
3.50/3.53	
3.50/3.53	
3.50/3.53	Combined result: Can't judge
3.50/3.53	failed to show confluence of U(R)
3.50/3.53	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
3.50/3.53	(3804 msec.)
3.50/3.53	EOF