#include <math.h>

$input double a;
$assume(a > 0);

void main() {
  double b = sqrt(a);
  double c = sqrt(b);
  double d = sqrt(c);

  $assert(a == d*d*d*d*d*d*d*d);
}