- : unit = ()
h : heuristic =
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)
TRS termination of:
[1] D(t) -> 1
[2] D(constant) -> 0
[3] D(+(x,y)) -> +(D(x),D(y))
[4] D( *(x,y)) -> +( *(y,D(x)), *(x,D(y)))
[5] D(-(x,y)) -> -(D(x),D(y))
Sub problem:
guided:
DP termination of:
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:
{ -->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
D(t) >= 1 ;
D(constant) >= 0 ;
D(+(x,y)) >= +(D(x),D(y)) ;
D( *(x,y)) >= +( *(y,D(x)), *(x,D(y))) ;
D(-(x,y)) >= -(D(x),D(y)) ;
Marked_D(+(x,y)) >= Marked_D(x) ;
Marked_D(+(x,y)) >= Marked_D(y) ;
Marked_D( *(x,y)) >= Marked_D(x) ;
Marked_D( *(x,y)) >= Marked_D(y) ;
Marked_D(-(x,y)) >= Marked_D(x) ;
Marked_D(-(x,y)) >= Marked_D(y) ;
}
+ Disjunctions:{
{
Marked_D(+(x,y)) > Marked_D(x) ;
}
{
Marked_D(+(x,y)) > Marked_D(y) ;
}
{
Marked_D( *(x,y)) > Marked_D(x) ;
}
{
Marked_D( *(x,y)) > Marked_D(y) ;
}
{
Marked_D(-(x,y)) > Marked_D(x) ;
}
{
Marked_D(-(x,y)) > Marked_D(y) ;
}
}
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25..
=== STOPING TIMER virtual ===
=== STOPING TIMER virtual ===
constraint: D(t) >= 1
constraint: D(constant) >= 0
constraint: D(+(x,y)) >= +(D(x),D(y))
constraint: D( *(x,y)) >= +( *(y,D(x)), *(x,D(y)))
constraint: D(-(x,y)) >= -(D(x),D(y))
constraint: Marked_D(+(x,y)) >= Marked_D(x)
constraint: Marked_D(+(x,y)) >= Marked_D(y)
constraint: Marked_D( *(x,y)) >= Marked_D(x)
constraint: Marked_D( *(x,y)) >= Marked_D(y)
constraint: Marked_D(-(x,y)) >= Marked_D(x)
constraint: Marked_D(-(x,y)) >= Marked_D(y)
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
TRS termination of:
[1] D(t) -> 1
[2] D(constant) -> 0
[3] D(+(x,y)) -> +(D(x),D(y))
[4] D( *(x,y)) -> +( *(y,D(x)), *(x,D(y)))
[5] D(-(x,y)) -> -(D(x),D(y))
,
CRITERION: MDP
[ {
DP termination of:
,
CRITERION: SG
[ {
DP termination of:
,
CRITERION: ORD
[
Solution found:
RPO with AFS = AFS:
and precedence:
prec (All symbols are Lex.): { 1 < D ; D > 1 ; D > 0 ; D > + ;
D > * ; D > - ; 0 < D ; + < D ;
* < D ; - < D ; }
]}
]}
]}
Cime worked for 0.051151 seconds (real time)
Cime Exit Status: 0