fof(pel24_1,axiom,
    ~ ? [X] :
        ( s(X)
        & q(X) ),
    file('Pell24Simplified.p',pel24_1) ).

fof(pel24_2,axiom,
    ! [X] :
      ( p(X)
     => ( q(X)
        | r(X) ) ),
    file('Pell24Simplified.p',pel24_2) ).

fof(pel24_3a,axiom,
    ? [X] : p(X),
    file('Pell24Simplified.p',pel24_3a) ).

fof(pel24_4a,axiom,
    ! [X] :
      ( q(X)
     => s(X) ),
    file('Pell24Simplified.p',pel24_4a) ).

fof(pel24,conjecture,
    ? [X] :
      ( p(X)
      & r(X) ),
    file('Pell24Simplified.p',pel24) ).

fof(f1,negated_conjecture,
    ~ ? [X] :
        ( p(X)
        & r(X) ),
    inference(negate,[status(cth)],[pel24]) ).

cnf(c1,plain,
    ( ~ p(X)
    | ~ r(X) ),
    inference(clausify,[status(thm)],[f1]) ).

cnf(c2,plain,
    ( ~ s(X)
    | ~ q(X) ),
    inference(clausify,[status(thm)],[pel24_1]) ).

cnf(c3,plain,
    p(a),
    inference(clausify,[status(esa),new_symbols(skolem,[a]),skolemized(X)],[pel24_3a]) ).

cnf(c4,plain,
    ( ~ q(X)
    | s(X) ),
    inference(clausify,[status(thm)],[pel24_4a]) ).

cnf(c5,plain,
    ( ~ p(X)
    | q(X)
    | r(X) ),
    inference(clausify,[status(thm)],[pel24_2]) ).

cnf(t1,plain,
    ( ~ p(a)
    | ~ r(a) ),
    inference(start,[status(thm),path([])],[c1]) ).

cnf(t2,plain,
    p(a),
    inference(extension,[status(thm),path([t1:1])],[c3]) ).

cnf(t3,plain,
    $false,
    inference(reduction,[status(thm),path([t2:1,t1:1])],[t2:1,t1:1]) ).

cnf(t4,plain,
    ( ~ p(a)
    | q(a)
    | r(a) ),
    inference(extension,[status(thm),path([t1:2])],[c5]) ).

cnf(t5,plain,
    $false,
    inference(reduction,[status(thm),path([t4:3,t1:2])],[t4:1,t1:2]) ).

cnf(t6,plain,
    p(a),
    inference(extension,[status(thm),path([t4:1,t1:2])],[c3]) ).

cnf(t7,plain,
    $false,
    inference(reduction,[status(thm),path([t6:1,t4:1,t1:2])],[t6:1,t4:1]) ).

cnf(t8,plain,
    ( ~ s(a)
    | ~ q(a) ),
    inference(extension,[status(thm),path([t4:2,t1:2])],[c2]) ).

cnf(t9,plain,
    $false,
    inference(reduction,[status(thm),path([t8:2,t4:2,t1:2])],[t8:2,t4:2]) ).

cnf(t10,plain,
    ( ~ q(a)
    | s(a) ),
    inference(extension,[status(thm),path([t8:1,t4:2,t1:2])],[c4]) ).

cnf(t11,plain,
    $false,
    inference(reduction,[status(thm),path([t10:2,t8:1,t4:2,t1:2])],[t10:2,t8:1]) ).

cnf(t12,plain,
    $false,
    inference(reduction,[status(thm),path([t10:1,t8:1,t4:2,t1:2])],[t10:1,t4:2]) ).