13.72/12.46 MAYBE
13.72/12.46 (ignored inputs)COMMENT doi:10.4230/LIPIcs.FSCD.2016.33 [36] Example 25 submitted by: Takahito Aoto and Yoshihito Toyama
13.72/12.46 Rewrite Rules:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Apply Direct Methods...
13.72/12.46 Inner CPs:
13.72/12.46 [ -(0) = 0,
13.72/12.46 -(+(-(?x_3),-(?y_3))) = +(?x_3,?y_3),
13.72/12.46 -(?x) = +(-(0),-(?x)),
13.72/12.46 -(?x_1) = +(-(?x_1),-(0)),
13.72/12.46 -(0) = +(-(1),-(-(1))),
13.72/12.46 -(0) = +(-(-(1)),-(1)),
13.72/12.46 -(+(?x_4,+(?y_4,?z_4))) = +(-(+(?x_4,?y_4)),-(?z_4)),
13.72/12.46 -(+(?y_5,?x_5)) = +(-(?x_5),-(?y_5)),
13.72/12.46 +(?x,?z_4) = +(0,+(?x,?z_4)),
13.72/12.46 +(?x_1,?z_4) = +(?x_1,+(0,?z_4)),
13.72/12.46 +(0,?z_4) = +(1,+(-(1),?z_4)),
13.72/12.46 +(0,?z_4) = +(-(1),+(1,?z_4)),
13.72/12.46 +(+(?y_5,?x_5),?z_4) = +(?x_5,+(?y_5,?z_4)),
13.72/12.46 -(?x) = -(?x),
13.72/12.46 +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
13.72/12.46 Outer CPs:
13.72/12.46 [ 0 = 0,
13.72/12.46 ?x = +(?x,0),
13.72/12.46 +(?x_4,?y_4) = +(?x_4,+(?y_4,0)),
13.72/12.46 ?x_1 = +(0,?x_1),
13.72/12.46 0 = +(-(1),1),
13.72/12.46 0 = +(1,-(1)),
13.72/12.46 +(?x_4,+(?y_4,?z_4)) = +(?z_4,+(?x_4,?y_4)) ]
13.72/12.46 not Overlay, check Termination...
13.72/12.46 unknown/not Terminating
13.72/12.46 unknown Knuth & Bendix
13.72/12.46 Linear
13.72/12.46 unknown Development Closed
13.72/12.46 unknown Strongly Closed
13.72/12.46 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
13.72/12.46 unknown Upside-Parallel-Closed/Outside-Closed
13.72/12.46 (inner) Parallel CPs: (not computed)
13.72/12.46 unknown Toyama (Parallel CPs)
13.72/12.46 Simultaneous CPs:
13.72/12.46 [ 0 = 0,
13.72/12.46 +(?x,0) = ?x,
13.72/12.46 +(-(0),-(?x)) = -(?x),
13.72/12.46 +(0,+(?x,?z_5)) = +(?x,?z_5),
13.72/12.46 +(?x_4,+(?y_4,0)) = +(?x_4,?y_4),
13.72/12.46 +(0,?x) = ?x,
13.72/12.46 +(-(?x),-(0)) = -(?x),
13.72/12.46 +(?x,+(0,?z_5)) = +(?x,?z_5),
13.72/12.46 +(-(1),1) = 0,
13.72/12.46 +(-(1),-(-(1))) = -(0),
13.72/12.46 +(1,+(-(1),?z_4)) = +(0,?z_4),
13.72/12.46 +(1,-(1)) = 0,
13.72/12.46 +(-(-(1)),-(1)) = -(0),
13.72/12.46 +(-(1),+(1,?z_4)) = +(0,?z_4),
13.72/12.46 0 = -(0),
13.72/12.46 -(?x_1) = -(?x_1),
13.72/12.46 -(0) = 0,
13.72/12.46 -(+(-(?x_4),-(?y_4))) = +(?x_4,?y_4),
13.72/12.46 ?x_1 = -(-(?x_1)),
13.72/12.46 +(-(?x_4),-(?y_4)) = -(+(?x_4,?y_4)),
13.72/12.46 -(?y) = +(-(0),-(?y)),
13.72/12.46 -(?x) = +(-(?x),-(0)),
13.72/12.46 -(0) = +(-(1),-(-(1))),
13.72/12.46 -(0) = +(-(-(1)),-(1)),
13.72/12.46 -(+(?x_5,+(?y_5,?y))) = +(-(+(?x_5,?y_5)),-(?y)),
13.72/12.46 -(+(?y,?x)) = +(-(?x),-(?y)),
13.72/12.46 ?y = -(+(-(0),-(?y))),
13.72/12.46 ?x = -(+(-(?x),-(0))),
13.72/12.46 0 = -(+(-(1),-(-(1)))),
13.72/12.46 0 = -(+(-(-(1)),-(1))),
13.72/12.46 +(?x_5,+(?y_5,?y)) = -(+(-(+(?x_5,?y_5)),-(?y))),
13.72/12.46 +(?y,?x) = -(+(-(?x),-(?y))),
13.72/12.46 +(?x,?y) = -(+(-(?x),-(?y))),
13.72/12.46 +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
13.72/12.46 ?y = +(0,+(?y,0)),
13.72/12.46 ?x = +(?x,+(0,0)),
13.72/12.46 0 = +(1,+(-(1),0)),
13.72/12.46 0 = +(-(1),+(1,0)),
13.72/12.46 +(?y,?x) = +(?x,+(?y,0)),
13.72/12.46 +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
13.72/12.46 +(?z,?y) = +(0,+(?y,?z)),
13.72/12.46 +(?z,?x) = +(?x,+(0,?z)),
13.72/12.46 +(?z,0) = +(1,+(-(1),?z)),
13.72/12.46 +(?z,0) = +(-(1),+(1,?z)),
13.72/12.46 +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) = +(?x,+(?y,0)),
13.72/12.46 +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
13.72/12.46 +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
13.72/12.46 +(?y,?z) = +(0,+(?y,?z)),
13.72/12.46 +(?x,?z) = +(?x,+(0,?z)),
13.72/12.46 +(0,?z) = +(1,+(-(1),?z)),
13.72/12.46 +(0,?z) = +(-(1),+(1,?z)),
13.72/12.46 +(+(?y,?x),?z) = +(?x,+(?y,?z)),
13.72/12.46 +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
13.72/12.46 +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
13.72/12.46 +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1),
13.72/12.46 +(0,+(?z,?z_1)) = +(+(1,+(-(1),?z)),?z_1),
13.72/12.46 +(0,+(?z,?z_1)) = +(+(-(1),+(1,?z)),?z_1),
13.72/12.46 +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
13.72/12.46 +(-(+(?x_1,+(?y_1,?y))),-(?z)) = -(+(+(?x_1,?y_1),+(?y,?z))),
13.72/12.46 +(-(?y),-(?z)) = -(+(0,+(?y,?z))),
13.72/12.46 +(-(?x),-(?z)) = -(+(?x,+(0,?z))),
13.72/12.46 +(-(0),-(?z)) = -(+(1,+(-(1),?z))),
13.72/12.46 +(-(0),-(?z)) = -(+(-(1),+(1,?z))),
13.72/12.46 +(-(+(?y,?x)),-(?z)) = -(+(?x,+(?y,?z))),
13.72/12.46 +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
13.72/12.46 +(-(+(?x,?y)),-(?z)) = -(+(?x,+(?y,?z))),
13.72/12.46 ?y = +(?y,0),
13.72/12.46 ?x = +(0,?x),
13.72/12.46 0 = +(-(1),1),
13.72/12.46 0 = +(1,-(1)),
13.72/12.46 +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)),
13.72/12.46 +(-(?x),-(?y)) = -(+(?y,?x)),
13.72/12.46 +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6) ]
13.72/12.46 unknown Okui (Simultaneous CPs)
13.72/12.46 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
13.72/12.46 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
13.72/12.46 check Locally Decreasing Diagrams by Rule Labelling...
13.72/12.46 Critical Pair <-(0), 0> by Rules <4, 5> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],4)], []>
13.72/12.46 Critical Pair <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],6),([(+,2)],5),([(+,1)],5)], []>
13.72/12.46 joinable by a reduction of rules <[([],6),([(+,1)],5),([(+,2)],5)], []>
13.72/12.46 Critical Pair <-(?x), +(-(0),-(?x))> by Rules <0, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[], [([(+,1)],4),([],0)]>
13.72/12.46 Critical Pair <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[], [([(+,2)],4),([],1)]>
13.72/12.46 Critical Pair <-(0), +(-(1),-(-(1)))> by Rules <2, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],4)], [([(+,2)],5),([],3)]>
13.72/12.46 Critical Pair <-(0), +(-(-(1)),-(1))> by Rules <3, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],4)], [([(+,1)],5),([],2)]>
13.72/12.46 Critical Pair <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],6),([(+,2)],6)], [([(+,1)],6),([],7)]>
13.72/12.46 Critical Pair <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[([],6)], [([],8)]>
13.72/12.46 Critical Pair <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[], [([],0)]>
13.72/12.46 Critical Pair <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[], [([(+,2)],0)]>
13.72/12.46 Critical Pair <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],3)]>
13.72/12.46 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],3)]>
13.72/12.46 Critical Pair <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],2)]>
13.72/12.46 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],2)]>
13.72/12.46 Critical Pair <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[([(+,1)],8),([],7)], []>
13.72/12.46 joinable by a reduction of rules <[([],7),([(+,2)],8)], [([],8),([],7)]>
13.72/12.46 Critical Pair <-(?x), -(?x)> by Rules <5, 5> preceded by [(-,1)]
13.72/12.46 joinable by a reduction of rules <[], []>
13.72/12.46 Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <7, 7> preceded by [(+,1)]
13.72/12.46 joinable by a reduction of rules <[([],7),([(+,2)],7)], [([],7)]>
13.72/12.46 Critical Pair <0, 0> by Rules <1, 0> preceded by []
13.72/12.46 joinable by a reduction of rules <[], []>
13.72/12.46 Critical Pair <+(?y_5,0), ?y_5> by Rules <8, 0> preceded by []
13.72/12.46 joinable by a reduction of rules <[([],1)], []>
13.72/12.46 Critical Pair <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1> preceded by []
13.72/12.46 joinable by a reduction of rules <[([(+,2)],1)], []>
13.72/12.46 Critical Pair <+(0,?x_5), ?x_5> by Rules <8, 1> preceded by []
13.72/12.46 joinable by a reduction of rules <[([],0)], []>
13.72/12.46 Critical Pair <+(-(1),1), 0> by Rules <8, 2> preceded by []
13.72/12.46 joinable by a reduction of rules <[([],3)], []>
13.72/12.46 Critical Pair <+(1,-(1)), 0> by Rules <8, 3> preceded by []
13.72/12.46 joinable by a reduction of rules <[([],2)], []>
13.72/12.46 Critical Pair <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7> preceded by []
13.72/12.46 joinable by a reduction of rules <[([],8),([],7)], []>
13.72/12.46 unknown Diagram Decreasing
13.72/12.46 check Non-Confluence...
13.72/12.46 obtain 11 rules by 3 steps unfolding
13.72/12.46 obtain 100 candidates for checking non-joinability
13.72/12.46 check by TCAP-Approximation (failure)
13.72/12.46 check by Ordering(rpo), check by Tree-Automata Approximation (failure)
13.72/12.46 check by Interpretation(mod2) (failure)
13.72/12.46 check by Descendants-Approximation, check by Ordering(poly) (failure)
13.72/12.46 unknown Non-Confluence
13.72/12.46 Check relative termination:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Polynomial Interpretation:
13.72/12.46 +:= (2)+(1)*x1+(1)*x2
13.72/12.46 -:= (2)*x1+(2)*x1*x1
13.72/12.46 0:= 0
13.72/12.46 1:= 0
13.72/12.46 retract +(0,?x) -> ?x
13.72/12.46 retract +(?x,0) -> ?x
13.72/12.46 retract +(1,-(1)) -> 0
13.72/12.46 retract +(-(1),1) -> 0
13.72/12.46 retract -(+(?x,?y)) -> +(-(?x),-(?y))
13.72/12.46 Polynomial Interpretation:
13.72/12.46 +:= (2)+(1)*x1+(1)*x2
13.72/12.46 -:= (1)+(2)*x1+(2)*x1*x1
13.72/12.46 0:= 0
13.72/12.46 1:= 0
13.72/12.46 relatively terminating
13.72/12.46 unknown Huet (modulo AC)
13.72/12.46 check by Reduction-Preserving Completion...
13.72/12.46 STEP: 1 (parallel)
13.72/12.46 S:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46 P:
13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 S: terminating
13.72/12.46 CP(S,S):
13.72/12.46 <0, 0> --> <0, 0> => yes
13.72/12.46 <0, 0> --> <0, 0> => yes
13.72/12.46 <-(0), 0> --> <0, 0> => yes
13.72/12.46 <-(?x), -(?x)> --> <-(?x), -(?x)> => yes
13.72/12.46 <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes
13.72/12.46 <-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
13.72/12.46 <-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes
13.72/12.46 <-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
13.72/12.46 <-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
13.72/12.46 PCP_in(symP,S):
13.72/12.46 <-(+(?x_3,?y_3)), +(-(?y_3),-(?x_3))> --> <+(-(?x_3),-(?y_3)), +(-(?y_3),-(?x_3))> => yes
13.72/12.46 <-(+(+(?x_2,?y_2),?z_2)), +(-(?x_2),-(+(?y_2,?z_2)))> --> <+(+(-(?x_2),-(?y_2)),-(?z_2)), +(-(?x_2),+(-(?y_2),-(?z_2)))> => yes
13.72/12.46 <-(+(?x_1,+(?y_1,?z_1))), +(-(+(?x_1,?y_1)),-(?z_1))> --> <+(-(?x_1),+(-(?y_1),-(?z_1))), +(+(-(?x_1),-(?y_1)),-(?z_1))> => yes
13.72/12.46 CP(S,symP):
13.72/12.46 <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46 <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
13.72/12.46 <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46 --> => yes
13.72/12.46 <+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
13.72/12.46 <+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46 <+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46 --> => yes
13.72/12.46 <+(0,?z), +(1,+(-(1),?z))> --> => no
13.72/12.46 <+(?x,0), +(+(?x,1),-(1))> --> => no
13.72/12.46 <0, +(-(1),1)> --> <0, 0> => yes
13.72/12.46 <+(0,?z), +(-(1),+(1,?z))> --> => no
13.72/12.46 <+(?x,0), +(+(?x,-(1)),1)> --> => no
13.72/12.46 <0, +(1,-(1))> --> <0, 0> => yes
13.72/12.46 check joinability condition:
13.72/12.46 check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
13.72/12.46 check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
13.72/12.46 check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
13.72/12.46 check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
13.72/12.46 failed
13.72/12.46 failure(Step 1)
13.72/12.46 [ ]
13.72/12.46 Added S-Rules:
13.72/12.46 [ ]
13.72/12.46 Added P-Rules:
13.72/12.46 [ ]
13.72/12.46 STEP: 2 (linear)
13.72/12.46 S:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46 P:
13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 S: terminating
13.72/12.46 CP(S,S):
13.72/12.46 <0, 0> --> <0, 0> => yes
13.72/12.46 <0, 0> --> <0, 0> => yes
13.72/12.46 <-(0), 0> --> <0, 0> => yes
13.72/12.46 <-(?x), -(?x)> --> <-(?x), -(?x)> => yes
13.72/12.46 <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes
13.72/12.46 <-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
13.72/12.46 <-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes
13.72/12.46 <-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
13.72/12.46 <-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
13.72/12.46 CP_in(symP,S):
13.72/12.46 <-(+(?x,+(?y,?z))), +(-(+(?x,?y)),-(?z))> --> <+(-(?x),+(-(?y),-(?z))), +(+(-(?x),-(?y)),-(?z))> => yes
13.72/12.46 <-(+(+(?x,?y),?z)), +(-(?x),-(+(?y,?z)))> --> <+(+(-(?x),-(?y)),-(?z)), +(-(?x),+(-(?y),-(?z)))> => yes
13.72/12.46 <-(+(?x,?y)), +(-(?y),-(?x))> --> <+(-(?x),-(?y)), +(-(?y),-(?x))> => yes
13.72/12.46 CP(S,symP):
13.72/12.46 <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46 <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
13.72/12.46 <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46 --> => yes
13.72/12.46 <+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
13.72/12.46 <+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46 <+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46 --> => yes
13.72/12.46 <+(0,?z), +(1,+(-(1),?z))> --> => no
13.72/12.46 <+(?x,0), +(+(?x,1),-(1))> --> => no
13.72/12.46 <0, +(-(1),1)> --> <0, 0> => yes
13.72/12.46 <+(0,?z), +(-(1),+(1,?z))> --> => no
13.72/12.46 <+(?x,0), +(+(?x,-(1)),1)> --> => no
13.72/12.46 <0, +(1,-(1))> --> <0, 0> => yes
13.72/12.46 check joinability condition:
13.72/12.46 check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
13.72/12.46 check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
13.72/12.46 check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
13.72/12.46 check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
13.72/12.46 failed
13.72/12.46 failure(Step 2)
13.72/12.46 [ ]
13.72/12.46 Added S-Rules:
13.72/12.46 [ ]
13.72/12.46 Added P-Rules:
13.72/12.46 [ ]
13.72/12.46 STEP: 3 (relative)
13.72/12.46 S:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46 P:
13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Check relative termination:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Polynomial Interpretation:
13.72/12.46 +:= (2)+(1)*x1+(1)*x2
13.72/12.46 -:= (2)*x1+(2)*x1*x1
13.72/12.46 0:= 0
13.72/12.46 1:= 0
13.72/12.46 retract +(0,?x) -> ?x
13.72/12.46 retract +(?x,0) -> ?x
13.72/12.46 retract +(1,-(1)) -> 0
13.72/12.46 retract +(-(1),1) -> 0
13.72/12.46 retract -(+(?x,?y)) -> +(-(?x),-(?y))
13.72/12.46 Polynomial Interpretation:
13.72/12.46 +:= (2)+(1)*x1+(1)*x2
13.72/12.46 -:= (1)+(2)*x1+(2)*x1*x1
13.72/12.46 0:= 0
13.72/12.46 1:= 0
13.72/12.46 relatively terminating
13.72/12.46 S/P: relatively terminating
13.72/12.46 check CP condition:
13.72/12.46 failed
13.72/12.46 failure(Step 3)
13.72/12.46 failure(no possibility remains)
13.72/12.46 unknown Reduction-Preserving Completion
13.72/12.46 check by Ordered Rewriting...
13.72/12.46 remove redundants rules and split
13.72/12.46 R-part:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
13.72/12.46 E-part:
13.72/12.46 [ +(?x,?y) -> +(?y,?x),
13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46 Perform abstraction and check...
13.72/12.46 Increase tree depth and check...
13.72/12.46 Apply reduction-preserving transformation...
13.72/12.46 Rules to add:
13.72/12.46 [ +(1,+(?x_6,-(1))) -> ?x_6 ]
13.72/12.46 remove redundants rules and split
13.72/12.46 R-part:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6 ]
13.72/12.46 E-part:
13.72/12.46 [ +(?x,?y) -> +(?y,?x),
13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46 Perform abstraction and check...
13.72/12.46 Increase tree depth and check...
13.72/12.46 Apply reduction-preserving transformation...
13.72/12.46 Rules to add:
13.72/12.46 [ +(1,+(-(1),?x_6)) -> ?x_6 ]
13.72/12.46 remove redundants rules and split
13.72/12.46 R-part:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6 ]
13.72/12.46 E-part:
13.72/12.46 [ +(?x,?y) -> +(?y,?x),
13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46 Perform abstraction and check...
13.72/12.46 Increase tree depth and check...
13.72/12.46 Apply reduction-preserving transformation...
13.72/12.46 Rules to add:
13.72/12.46 [ +(-(1),+(?x_8,1)) -> ?x_8 ]
13.72/12.46 remove redundants rules and split
13.72/12.46 R-part:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6,
13.72/12.46 +(-(1),+(?x_8,1)) -> ?x_8 ]
13.72/12.46 E-part:
13.72/12.46 [ +(?x,?y) -> +(?y,?x),
13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46 Perform abstraction and check...
13.72/12.46 Increase tree depth and check...
13.72/12.46 Apply reduction-preserving transformation...
13.72/12.46 Rules to add:
13.72/12.46 [ +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ]
13.72/12.46 remove redundants rules and split
13.72/12.46 R-part:
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6,
13.72/12.46 +(-(1),+(?x_8,1)) -> ?x_8,
13.72/12.46 +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ]
13.72/12.46 E-part:
13.72/12.46 [ +(?x,?y) -> +(?y,?x),
13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46 Perform abstraction and check...
13.72/12.46 Increase tree depth and check...
13.72/12.46 unknown Confluence by Ordered Rewriting
13.72/12.46 Direct Methods: Can't judge
13.72/12.46
13.72/12.46 Try Persistent Decomposition for...
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Sort Assignment:
13.72/12.46 + : 18*18=>18
13.72/12.46 - : 18=>18
13.72/12.46 0 : =>18
13.72/12.46 1 : =>18
13.72/12.46 maximal types: {18}
13.72/12.46 Persistent Decomposition failed: Can't judge
13.72/12.46
13.72/12.46 Try Layer Preserving Decomposition for...
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Layer Preserving Decomposition failed: Can't judge
13.72/12.46
13.72/12.46 Try Commutative Decomposition for...
13.72/12.46 [ +(0,?x) -> ?x,
13.72/12.46 +(?x,0) -> ?x,
13.72/12.46 +(1,-(1)) -> 0,
13.72/12.46 +(-(1),1) -> 0,
13.72/12.46 -(0) -> 0,
13.72/12.46 -(-(?x)) -> ?x,
13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46 +(?x,?y) -> +(?y,?x) ]
13.72/12.46 Outside Critical Pair: <0, 0> by Rules <1, 0>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{}, 0>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, 0>
13.72/12.46 Outside Critical Pair: <+(?y_5,0), ?y_5> by Rules <8, 0>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(0,?y_5)>
13.72/12.46 <{1}, ?y_5>
13.72/12.46 <{}, +(?y_5,0)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, ?y_5>
13.72/12.46 Outside Critical Pair: <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(+(0,?y_4),?x_4)>
13.72/12.46 <{1,8}, +(?y_4,?x_4)>
13.72/12.46 <{8}, +(+(?y_4,0),?x_4)>
13.72/12.46 <{8}, +(?x_4,+(0,?y_4))>
13.72/12.46 <{1}, +(?x_4,?y_4)>
13.72/12.46 <{}, +(?x_4,+(?y_4,0))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(?y_4,?x_4)>
13.72/12.46 <{}, +(?x_4,?y_4)>
13.72/12.46 Outside Critical Pair: <+(0,?x_5), ?x_5> by Rules <8, 1>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?x_5,0)>
13.72/12.46 <{0}, ?x_5>
13.72/12.46 <{}, +(0,?x_5)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, ?x_5>
13.72/12.46 Outside Critical Pair: <+(-(1),1), 0> by Rules <8, 2>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(1,-(1))>
13.72/12.46 <{3}, 0>
13.72/12.46 <{}, +(-(1),1)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, 0>
13.72/12.46 Outside Critical Pair: <+(1,-(1)), 0> by Rules <8, 3>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(-(1),1)>
13.72/12.46 <{2}, 0>
13.72/12.46 <{}, +(1,-(1))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, 0>
13.72/12.46 Outside Critical Pair: <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(+(?y_4,?x_4),?y_5)>
13.72/12.46 <{8}, +(+(?x_4,?y_4),?y_5)>
13.72/12.46 <{8}, +(?y_5,+(?y_4,?x_4))>
13.72/12.46 <{}, +(?y_5,+(?x_4,?y_4))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?y_5,?y_4),?x_4)>
13.72/12.46 <{8}, +(+(?y_4,?y_5),?x_4)>
13.72/12.46 <{8}, +(?x_4,+(?y_5,?y_4))>
13.72/12.46 <{}, +(?x_4,+(?y_4,?y_5))>
13.72/12.46 Inside Critical Pair: <-(0), 0> by Rules <4, 5>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{4}, 0>
13.72/12.46 <{}, -(0)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{}, 0>
13.72/12.46 Inside Critical Pair: <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{6}, +(-(-(?x_3)),-(-(?y_3)))>
13.72/12.46 <{8}, -(+(-(?y_3),-(?x_3)))>
13.72/12.46 <{}, -(+(-(?x_3),-(?y_3)))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(?y_3,?x_3)>
13.72/12.46 <{}, +(?x_3,?y_3)>
13.72/12.46 Inside Critical Pair: <-(?x), +(-(0),-(?x))> by Rules <0, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{}, -(?x)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{4,8}, +(-(?x),0)>
13.72/12.46 <{8}, +(-(?x),-(0))>
13.72/12.46 <{4}, +(0,-(?x))>
13.72/12.46 <{}, +(-(0),-(?x))>
13.72/12.46 Inside Critical Pair: <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{}, -(?x_1)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{4,8}, +(0,-(?x_1))>
13.72/12.46 <{8}, +(-(0),-(?x_1))>
13.72/12.46 <{4}, +(-(?x_1),0)>
13.72/12.46 <{}, +(-(?x_1),-(0))>
13.72/12.46 Inside Critical Pair: <-(0), +(-(1),-(-(1)))> by Rules <2, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{4}, 0>
13.72/12.46 <{}, -(0)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{5,8}, +(1,-(1))>
13.72/12.46 <{8}, +(-(-(1)),-(1))>
13.72/12.46 <{5}, +(-(1),1)>
13.72/12.46 <{}, +(-(1),-(-(1)))>
13.72/12.46 Inside Critical Pair: <-(0), +(-(-(1)),-(1))> by Rules <3, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{4}, 0>
13.72/12.46 <{}, -(0)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{5,8}, +(-(1),1)>
13.72/12.46 <{8}, +(-(1),-(-(1)))>
13.72/12.46 <{5}, +(1,-(1))>
13.72/12.46 <{}, +(-(-(1)),-(1))>
13.72/12.46 Inside Critical Pair: <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{6,8}, +(-(?x_4),-(+(?z_4,?y_4)))>
13.72/12.46 <{6}, +(-(?x_4),-(+(?y_4,?z_4)))>
13.72/12.46 <{8}, -(+(+(?z_4,?y_4),?x_4))>
13.72/12.46 <{8}, -(+(+(?y_4,?z_4),?x_4))>
13.72/12.46 <{8}, -(+(?x_4,+(?z_4,?y_4)))>
13.72/12.46 <{}, -(+(?x_4,+(?y_4,?z_4)))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{6,8}, +(-(?z_4),+(-(?x_4),-(?y_4)))>
13.72/12.46 <{8}, +(-(?z_4),-(+(?y_4,?x_4)))>
13.72/12.46 <{8}, +(-(?z_4),-(+(?x_4,?y_4)))>
13.72/12.46 <{6}, +(+(-(?x_4),-(?y_4)),-(?z_4))>
13.72/12.46 <{8}, +(-(+(?y_4,?x_4)),-(?z_4))>
13.72/12.46 <{}, +(-(+(?x_4,?y_4)),-(?z_4))>
13.72/12.46 Inside Critical Pair: <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{6}, +(-(?y_5),-(?x_5))>
13.72/12.46 <{8}, -(+(?x_5,?y_5))>
13.72/12.46 <{}, -(+(?y_5,?x_5))>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(-(?y_5),-(?x_5))>
13.72/12.46 <{}, +(-(?x_5),-(?y_5))>
13.72/12.46 Inside Critical Pair: <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?z_4,?x)>
13.72/12.46 <{}, +(?x,?z_4)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?z_4,?x),0)>
13.72/12.46 <{8}, +(+(?x,?z_4),0)>
13.72/12.46 <{0,8}, +(?z_4,?x)>
13.72/12.46 <{0}, +(?x,?z_4)>
13.72/12.46 <{8}, +(0,+(?z_4,?x))>
13.72/12.46 <{}, +(0,+(?x,?z_4))>
13.72/12.46 Inside Critical Pair: <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?z_4,?x_1)>
13.72/12.46 <{}, +(?x_1,?z_4)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?z_4,0),?x_1)>
13.72/12.46 <{0,8}, +(?z_4,?x_1)>
13.72/12.46 <{8}, +(+(0,?z_4),?x_1)>
13.72/12.46 <{8}, +(?x_1,+(?z_4,0))>
13.72/12.46 <{0}, +(?x_1,?z_4)>
13.72/12.46 <{}, +(?x_1,+(0,?z_4))>
13.72/12.46 Inside Critical Pair: <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?z_4,0)>
13.72/12.46 <{0}, ?z_4>
13.72/12.46 <{}, +(0,?z_4)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?z_4,-(1)),1)>
13.72/12.46 <{8}, +(+(-(1),?z_4),1)>
13.72/12.46 <{8}, +(1,+(?z_4,-(1)))>
13.72/12.46 <{}, +(1,+(-(1),?z_4))>
13.72/12.46 Inside Critical Pair: <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?z_4,0)>
13.72/12.46 <{0}, ?z_4>
13.72/12.46 <{}, +(0,?z_4)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?z_4,1),-(1))>
13.72/12.46 <{8}, +(+(1,?z_4),-(1))>
13.72/12.46 <{8}, +(-(1),+(?z_4,1))>
13.72/12.46 <{}, +(-(1),+(1,?z_4))>
13.72/12.46 Inside Critical Pair: <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7>
13.72/12.46 develop reducts from lhs term...
13.72/12.46 <{8}, +(?z_4,+(?x_5,?y_5))>
13.72/12.46 <{8}, +(?z_4,+(?y_5,?x_5))>
13.72/12.46 <{7}, +(?y_5,+(?x_5,?z_4))>
13.72/12.46 <{8}, +(+(?x_5,?y_5),?z_4)>
13.72/12.46 <{}, +(+(?y_5,?x_5),?z_4)>
13.72/12.46 develop reducts from rhs term...
13.72/12.46 <{8}, +(+(?z_4,?y_5),?x_5)>
13.72/12.46 <{8}, +(+(?y_5,?z_4),?x_5)>
13.72/12.46 <{8}, +(?x_5,+(?z_4,?y_5))>
13.72/12.46 <{}, +(?x_5,+(?y_5,?z_4))>
13.72/12.46 Commutative Decomposition failed: Can't judge
13.72/12.46 No further decomposition possible
13.72/12.46
13.72/12.46
13.72/12.46 Combined result: Can't judge
13.72/12.46 /export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
13.72/12.46 (5152 msec.)
13.72/12.46 EOF