Left Termination of the query pattern goal_in_1(g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil).
tree(X) :- ','(no(empty(X)), ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R))))).
s2t(0, nil).
s2t(X, node(T, X1, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X2, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(T, X3, nil)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X4, nil)) :- no(zero(X)).
left(nil, nil).
left(node(L, X5, X6), L).
right(nil, nil).
right(node(X7, X8, R), R).
p(0, 0).
p(s(X), X).
empty(nil).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X9).
failure(b).

Queries:

goal(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil).
tree(X) :- ','(no(empty(X)), ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R))))).
s2t(0, nil).
s2t(X, node(T, X1, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X2, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(T, X3, nil)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X4, nil)) :- no(zero(X)).
left(nil, nil).
left(node(L, X5, X6), L).
right(nil, nil).
right(node(X7, X8, R), R).
p(0, 0).
p(s(X), X).
empty(nil).
zero(0).
no(X) :- ','(X, failure(a)).
no(X9).
failure(b).

Queries:

goal(g).