script empty(){

}

script full(){
  impRight;
  impRight;
  impLeft;
  cases {
	case derivable `p`:
   }
}


script full(){
  impRight;
  impRight;
  impLeft;
  cases {
	case match `!q ==> p`:
		notLeft;
		notRight;
		closeAntec;


	case match `q==>!p`:
		notLeft;
		closeAntec;
   }
}

script autoScript(){
    __STRICT_MODE := true;
    auto;
}


script interactive(){
  impRight;
  impRight;
  impLeft;
//after execution of this script, manual interaction can be performed
}
script interactive_with_match(){
impRight;
impRight;
#save 'test0' force='yes';
impLeft;
cases{
    case match `==> !(?Z), ?Z`:
      notRight;

    default:
      notLeft;

    }

}

script usageOfTryInCases(){
cases{
    try: impLeft; //if this mutator is successful, do this operation otherwise use next case

    default:
        __KEY_MAX_STEPS:= 100;
        impRight;
    }
    auto;
}

script varDecl1(){
    var1 : INT :=  1;
    var2 : INT :=  2;
    var3 : INT :=  3;
}

script varDecl2(){
  var1 : INT :=  1;
  impRight;
  impRight;
  impLeft;
  cases {
	case match `!q ==> p`:
		notLeft;
		var2 : INT :=  2;
		notRight;



	case match `q==>!p`:
		notLeft;
		var3 : INT :=  3;
   }



}