Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( x , y , z ) → g#( <=( x , y ) , x , y , z )
g#( false , x , y , z ) → f#( f( p( x ) , y , z ) , f( p( y ) , z , x ) , f( p( z ) , x , y ) )
g#( false , x , y , z ) → f#( p( x ) , y , z )
g#( false , x , y , z ) → p#( x )
g#( false , x , y , z ) → f#( p( y ) , z , x )
g#( false , x , y , z ) → p#( y )
g#( false , x , y , z ) → f#( p( z ) , x , y )
g#( false , x , y , z ) → p#( z )

1.1: dependency graph processor

The dependency pairs are split into 0 component(s).