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