MAYBE Time: 0.007723 TRS: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} DP: DP: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} TRS: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} UR: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} STATUS: arrows: 0.000000 SCCS (1): Scc: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} SCC (5): Strict: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} Weak: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} Open