TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60138 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (156ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (88ms), PolynomialLinearRange4iUR (2367ms), DependencyGraph (85ms), PolynomialLinearRange8NegiUR (6752ms), DependencyGraph (73ms), ReductionPairSAT (50464ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

app^#(app(mult, app(s, x)), y)	→	app^#(app(mult, x), y)		app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(rec, f), x)
app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(app(rec, f), x), y)		app^#(app(add, app(s, x)), y)	→	app^#(add, x)
app^#(app(add, app(s, x)), y)	→	app^#(s, app(app(add, x), y))		app^#(app(add, app(s, x)), y)	→	app^#(app(add, x), y)
app^#(app(mult, app(s, x)), y)	→	app^#(add, app(app(mult, x), y))		app^#(app(mult, app(s, x)), y)	→	app^#(mult, x)
app^#(app(app(rec, f), x), app(s, y))	→	app^#(rec, f)		app^#(app(mult, app(s, x)), y)	→	app^#(app(add, app(app(mult, x), y)), y)
app^#(app(app(rec, f), x), app(s, y))	→	app^#(s, y)		app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(f, app(s, y)), app(app(app(rec, f), x), y))
app^#(app(app(rec, f), x), app(s, y))	→	app^#(f, app(s, y))

Rewrite Rules

app(app(add, 0), y)	→	y		app(app(add, app(s, x)), y)	→	app(s, app(app(add, x), y))
app(app(mult, 0), y)	→	0		app(app(mult, app(s, x)), y)	→	app(app(add, app(app(mult, x), y)), y)
app(app(app(rec, f), x), 0)	→	x		app(app(app(rec, f), x), app(s, y))	→	app(app(f, app(s, y)), app(app(app(rec, f), x), y))
fact	→	app(app(rec, mult), app(s, 0))

Original Signature

Termination of terms over the following signature is verified: app, rec, mult, fact, 0, s, add

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

app^#(app(mult, app(s, x)), y)	→	app^#(app(mult, x), y)		fact^#	→	app^#(s, 0)
fact^#	→	app^#(app(rec, mult), app(s, 0))		app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(rec, f), x)
app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(app(rec, f), x), y)		app^#(app(add, app(s, x)), y)	→	app^#(add, x)
fact^#	→	app^#(rec, mult)		app^#(app(add, app(s, x)), y)	→	app^#(s, app(app(add, x), y))
app^#(app(add, app(s, x)), y)	→	app^#(app(add, x), y)		app^#(app(mult, app(s, x)), y)	→	app^#(add, app(app(mult, x), y))
app^#(app(mult, app(s, x)), y)	→	app^#(mult, x)		app^#(app(app(rec, f), x), app(s, y))	→	app^#(rec, f)
app^#(app(mult, app(s, x)), y)	→	app^#(app(add, app(app(mult, x), y)), y)		app^#(app(app(rec, f), x), app(s, y))	→	app^#(s, y)
app^#(app(app(rec, f), x), app(s, y))	→	app^#(f, app(s, y))		app^#(app(app(rec, f), x), app(s, y))	→	app^#(app(f, app(s, y)), app(app(app(rec, f), x), y))

Rewrite Rules

app(app(add, 0), y)	→	y		app(app(add, app(s, x)), y)	→	app(s, app(app(add, x), y))
app(app(mult, 0), y)	→	0		app(app(mult, app(s, x)), y)	→	app(app(add, app(app(mult, x), y)), y)
app(app(app(rec, f), x), 0)	→	x		app(app(app(rec, f), x), app(s, y))	→	app(app(f, app(s, y)), app(app(app(rec, f), x), y))
fact	→	app(app(rec, mult), app(s, 0))

Original Signature

Termination of terms over the following signature is verified: app, mult, rec, 0, fact, s, add

Strategy

The following SCCs where found

app^#(app(mult, app(s, x)), y) → app^#(app(mult, x), y)	app^#(app(app(rec, f), x), app(s, y)) → app^#(app(rec, f), x)
app^#(app(app(rec, f), x), app(s, y)) → app^#(app(app(rec, f), x), y)	app^#(app(add, app(s, x)), y) → app^#(add, x)
app^#(app(add, app(s, x)), y) → app^#(s, app(app(add, x), y))	app^#(app(mult, app(s, x)), y) → app^#(mult, x)
app^#(app(mult, app(s, x)), y) → app^#(add, app(app(mult, x), y))	app^#(app(add, app(s, x)), y) → app^#(app(add, x), y)
app^#(app(app(rec, f), x), app(s, y)) → app^#(rec, f)	app^#(app(mult, app(s, x)), y) → app^#(app(add, app(app(mult, x), y)), y)
app^#(app(app(rec, f), x), app(s, y)) → app^#(s, y)	app^#(app(app(rec, f), x), app(s, y)) → app^#(f, app(s, y))
app^#(app(app(rec, f), x), app(s, y)) → app^#(app(f, app(s, y)), app(app(app(rec, f), x), y))