// This code checks the solutions of the inequations of Theorem 2 of
// "How far away must forced letters be so that squares are still avoidable?"
// It requires gmp to be installed and should be compiled with c++11 or higher and optimization O3 wich gives:
//      g++ check_solution.cpp -O3 -lgmp -lgmpxx -o <executable_name>

#include <iostream>
#include <vector>
#include <gmpxx.h>

using namespace std;

int main(){
  int n, p, sA;  //we start by reading the inputs
  cout<<"Enter |{|w|: w in W}|, p and |A| (where A is the alphabet)"<<endl;
  cout<<"Then enter the n pairs that describe f in the following format: |u| f(|u|) ... |v| f(|v|)." <<endl;
  cout<<"Finally give the x_|u| in the same order."<<endl;
  cout<<"For instance to check the inequations for the case d({0,1,2})<=19 you can enter:"<<endl;
  cout<<"10 61 3   9 4 19 19 20 22 21 28 22 36 23 50 24 63 25 88 26 118 27 148   27/100  7/100  13/200  11/200  9/200  1/25  3/100  1/40  1/40  1/50 "<<endl;
  int k=0;
  cin>> n>>p>>sA;
  vector<int> l(n);
  vector<int> f(n);
  for(int i=0;i<n;i++){
    cin >>l[i]>>f[i];
    if(l[i]>k) k=l[i];
  }
  vector<mpq_class> x(n);
  for(int i=0;i<n;i++) cin>>x[i]; 
  
  vector<mpz_class> powSA(k+1,1);
  for(int i=1; i<=k; i++) powSA[i]=(sA-1)*powSA[i-1];
  
  vector<vector<mpz_class> > alpha(n, vector<mpz_class>(n,0));//we compute alpha by applying the formula
  for(int u=0;u<n;u++){
    for(int v=0;v<n;v++){
      for(int m=1; m<=l[u];m++)
        for(int j=0;j<=(l[v]-1)/m;j++)
          if(powSA[l[v]-1-j*m]<f[v]) alpha[u][v] += powSA[l[v]-1-j*m];
          else  alpha[u][v] +=f[v];
    }
  }
  
  vector<vector<mpz_class> > alphaBis(k+1, vector<mpz_class>(n,0));//we compute alpha' by applying the formula
  for(int i=1; i<=k; i++){
    for(int v=0;v<n;v++){
      for(int m=0; m<i; m++)
        if(powSA[m]<f[v]) alphaBis[i][v] += powSA[m];
        else  alphaBis[i][v] +=f[v];
    }
  }
  
  vector<mpq_class> beta(p+1,0);//we compute beta by dynamic programmic
  beta[0]=1;
  for(int i=1; i<=p;i++)
    for(int j=0; j<n; j++)
      if(i>=l[j] && beta[i-l[j]]*x[j]>beta[i]) 
        beta[i]=beta[i-l[j]]*x[j];
  
  bool ok = true;//we check all the inequations
  for(int w=0; w<n; w++){
    for(int u=0; u<n; u++){
      for(int v=0; v<n; v++){
        for(int r=1; r<=l[v];r++){
          if(f[w]-beta[r+p-l[w]-l[v]]*(alphaBis[r][w]+ x[v]*alpha[u][w]/(1-x[u]))<1/x[w]) ok = false;          
        }
      }
    }
  }
  //we can conclude
  if(ok) cout<<" This is a solution."<<endl; 
  else cout<< "This is not a solution."<<endl;
  return 0;
}