script test(){
    impRight;
    andLeft;
    notLeft;
    repeat { andLeft; }
    exLeft;
    andLeft;
    eqSymm formula = `agatha = butler`;
    nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;

}

script SolveAgathaRiddle_1() {
    impRight;
    andLeft;
    notLeft;
    repeat { andLeft; }
    exLeft;
    andLeft;
    eqSymm formula = `agatha = butler`;
    auto;
}

script SolveAgathaRiddle_2() {
    impRight;
    andLeft;
    notLeft;

    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;
    andLeft;

    exLeft;
    andLeft;
    eqSymm formula = `agatha = butler`;
    nnf_imp2or formula=`\forall S w6;(hates(agatha,w6) -> hates(butler,w6))`;
    auto;
}