---------------------------------------------------------------------------

WATCH: 0.00 CPU 0.01 WC
SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p

SZS output start CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p
fof(thm147, conjecture,
    (~
       (! [P, Q] : (~ a_truth(P) | a_truth(Q) | ~ a_truth(implies(P, Q))) &
        ! [P, Q] : a_truth(implies(P, implies(Q, P))) &
        ? [A] : ~ a_truth(implies(A, A)) &
        ! [P, Q] :
          a_truth(implies(implies(not(P), not(Q)), implies(Q, P))) &
        ! [P, Q, R] :
          a_truth(implies(implies(P, implies(Q, R)),
              implies(implies(P, Q), implies(P, R))))))).

fof(subgoal_0, plain,
    ((! [P, Q] : (~ a_truth(P) | a_truth(Q) | ~ a_truth(implies(P, Q))) &
      ! [P, Q] : a_truth(implies(P, implies(Q, P))) &
      ? [A] : ~ a_truth(implies(A, A)) &
      ! [P, Q] :
        a_truth(implies(implies(not(P), not(Q)), implies(Q, P)))) =>
     ~
       ! [P, Q, R] :
         a_truth(implies(implies(P, implies(Q, R)),
             implies(implies(P, Q), implies(P, R))))),
    inference(strip, [], [thm147])).

fof(negate_0_0, plain,
    (~
       ((! [P, Q] :
           (~ a_truth(P) | a_truth(Q) | ~ a_truth(implies(P, Q))) &
         ! [P, Q] : a_truth(implies(P, implies(Q, P))) &
         ? [A] : ~ a_truth(implies(A, A)) &
         ! [P, Q] :
           a_truth(implies(implies(not(P), not(Q)), implies(Q, P)))) =>
        ~
          ! [P, Q, R] :
            a_truth(implies(implies(P, implies(Q, R)),
                implies(implies(P, Q), implies(P, R)))))),
    inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain,
    (? [A] : ~ a_truth(implies(A, A)) &
     ! [P, Q] : a_truth(implies(P, implies(Q, P))) &
     ! [P, Q] : a_truth(implies(implies(not(P), not(Q)), implies(Q, P))) &
     ! [P, Q] : (~ a_truth(P) | ~ a_truth(implies(P, Q)) | a_truth(Q)) &
     ! [P, Q, R] :
       a_truth(implies(implies(P, implies(Q, R)),
           implies(implies(P, Q), implies(P, R))))),
    inference(canonicalize, [], [negate_0_0])).

fof(normalize_0_1, plain, (? [A] : ~ a_truth(implies(A, A))),
    inference(conjunct, [], [normalize_0_0])).

fof(normalize_0_2, plain,
    (~ a_truth(implies(skolemFOFtoCNF_A, skolemFOFtoCNF_A))),
    inference(skolemize, [], [normalize_0_1])).

fof(normalize_0_3, plain,
    (! [P, Q] : a_truth(implies(implies(not(P), not(Q)), implies(Q, P)))),
    inference(conjunct, [], [normalize_0_0])).

fof(normalize_0_4, plain,
    (! [P, Q] : a_truth(implies(implies(not(P), not(Q)), implies(Q, P)))),
    inference(specialize, [], [normalize_0_3])).

fof(normalize_0_5, plain, (! [P, Q] : a_truth(implies(P, implies(Q, P)))),
    inference(conjunct, [], [normalize_0_0])).

fof(normalize_0_6, plain, (! [P, Q] : a_truth(implies(P, implies(Q, P)))),
    inference(specialize, [], [normalize_0_5])).

fof(normalize_0_7, plain,
    (! [P, Q] : (~ a_truth(P) | ~ a_truth(implies(P, Q)) | a_truth(Q))),
    inference(conjunct, [], [normalize_0_0])).

fof(normalize_0_8, plain,
    (! [P, Q] : (~ a_truth(P) | ~ a_truth(implies(P, Q)) | a_truth(Q))),
    inference(specialize, [], [normalize_0_7])).

fof(normalize_0_9, plain,
    (! [P, Q, R] :
       a_truth(implies(implies(P, implies(Q, R)),
           implies(implies(P, Q), implies(P, R))))),
    inference(conjunct, [], [normalize_0_0])).

fof(normalize_0_10, plain,
    (! [P, Q, R] :
       a_truth(implies(implies(P, implies(Q, R)),
           implies(implies(P, Q), implies(P, R))))),
    inference(specialize, [], [normalize_0_9])).

cnf(refute_0_0, plain,
    (~ a_truth(implies(skolemFOFtoCNF_A, skolemFOFtoCNF_A))),
    inference(canonicalize, [], [normalize_0_2])).

cnf(refute_0_1, plain,
    (a_truth(implies(implies(not(P), not(Q)), implies(Q, P)))),
    inference(canonicalize, [], [normalize_0_4])).

cnf(refute_0_2, plain, (a_truth(implies(P, implies(Q, P)))),
    inference(canonicalize, [], [normalize_0_6])).

cnf(refute_0_3, plain, (a_truth(implies(X_7, implies(Q, X_7)))),
    inference(subst, [], [refute_0_2 : [bind(P, $fot(X_7))]])).

cnf(refute_0_4, plain,
    (~ a_truth(P) | ~ a_truth(implies(P, Q)) | a_truth(Q)),
    inference(canonicalize, [], [normalize_0_8])).

cnf(refute_0_5, plain,
    (~ a_truth(X_7) | ~ a_truth(implies(X_7, implies(Q, X_7))) |
     a_truth(implies(Q, X_7))),
    inference(subst, [],
              [refute_0_4 :
               [bind(P, $fot(X_7)), bind(Q, $fot(implies(Q, X_7)))]])).

cnf(refute_0_6, plain, (~ a_truth(X_7) | a_truth(implies(Q, X_7))),
    inference(resolve, [$cnf(a_truth(implies(X_7, implies(Q, X_7))))],
              [refute_0_3, refute_0_5])).

cnf(refute_0_7, plain,
    (~ a_truth(implies(implies(not(P), not(Q)), implies(Q, P))) |
     a_truth(implies(X_9,
         implies(implies(not(P), not(Q)), implies(Q, P))))),
    inference(subst, [],
              [refute_0_6 :
               [bind(Q, $fot(X_9)),
                bind(X_7,
                     $fot(implies(implies(not(P), not(Q)),
                            implies(Q, P))))]])).

cnf(refute_0_8, plain,
    (a_truth(implies(X_9,
         implies(implies(not(P), not(Q)), implies(Q, P))))),
    inference(resolve,
              [$cnf(a_truth(implies(implies(not(P), not(Q)),
                        implies(Q, P))))], [refute_0_1, refute_0_7])).

cnf(refute_0_9, plain,
    (a_truth(implies(X_76,
         implies(implies(not(P), not(Q)), implies(Q, P))))),
    inference(subst, [], [refute_0_8 : [bind(X_9, $fot(X_76))]])).

cnf(refute_0_10, plain,
    (~ a_truth(implies(X_42, X_41)) |
     ~ a_truth(implies(implies(X_42, X_41), implies(X_42, X_42))) |
     a_truth(implies(X_42, X_42))),
    inference(subst, [],
              [refute_0_4 :
               [bind(P, $fot(implies(X_42, X_41))),
                bind(Q, $fot(implies(X_42, X_42)))]])).

cnf(refute_0_11, plain, (a_truth(implies(X_40, implies(X_39, X_40)))),
    inference(subst, [],
              [refute_0_2 : [bind(P, $fot(X_40)), bind(Q, $fot(X_39))]])).

cnf(refute_0_12, plain,
    (a_truth(implies(implies(P, implies(Q, R)),
         implies(implies(P, Q), implies(P, R))))),
    inference(canonicalize, [], [normalize_0_10])).

cnf(refute_0_13, plain,
    (~ a_truth(implies(P, implies(Q, R))) |
     ~
       a_truth(implies(implies(P, implies(Q, R)),
           implies(implies(P, Q), implies(P, R)))) |
     a_truth(implies(implies(P, Q), implies(P, R)))),
    inference(subst, [],
              [refute_0_4 :
               [bind(P, $fot(implies(P, implies(Q, R)))),
                bind(Q, $fot(implies(implies(P, Q), implies(P, R))))]])).

cnf(refute_0_14, plain,
    (~ a_truth(implies(P, implies(Q, R))) |
     a_truth(implies(implies(P, Q), implies(P, R)))),
    inference(resolve,
              [$cnf(a_truth(implies(implies(P, implies(Q, R)),
                        implies(implies(P, Q), implies(P, R)))))],
              [refute_0_12, refute_0_13])).

cnf(refute_0_15, plain,
    (~ a_truth(implies(X_40, implies(X_39, X_40))) |
     a_truth(implies(implies(X_40, X_39), implies(X_40, X_40)))),
    inference(subst, [],
              [refute_0_14 :
               [bind(P, $fot(X_40)), bind(Q, $fot(X_39)),
                bind(R, $fot(X_40))]])).

cnf(refute_0_16, plain,
    (a_truth(implies(implies(X_40, X_39), implies(X_40, X_40)))),
    inference(resolve, [$cnf(a_truth(implies(X_40, implies(X_39, X_40))))],
              [refute_0_11, refute_0_15])).

cnf(refute_0_17, plain,
    (a_truth(implies(implies(X_42, X_41), implies(X_42, X_42)))),
    inference(subst, [],
              [refute_0_16 :
               [bind(X_39, $fot(X_41)), bind(X_40, $fot(X_42))]])).

cnf(refute_0_18, plain,
    (~ a_truth(implies(X_42, X_41)) | a_truth(implies(X_42, X_42))),
    inference(resolve,
              [$cnf(a_truth(implies(implies(X_42, X_41),
                        implies(X_42, X_42))))],
              [refute_0_17, refute_0_10])).

cnf(refute_0_19, plain,
    (~
       a_truth(implies(X_76,
           implies(implies(not(P), not(Q)), implies(Q, P)))) |
     a_truth(implies(X_76, X_76))),
    inference(subst, [],
              [refute_0_18 :
               [bind(X_41,
                     $fot(implies(implies(not(P), not(Q)),
                            implies(Q, P)))), bind(X_42, $fot(X_76))]])).

cnf(refute_0_20, plain, (a_truth(implies(X_76, X_76))),
    inference(resolve,
              [$cnf(a_truth(implies(X_76,
                        implies(implies(not(P), not(Q)),
                          implies(Q, P)))))], [refute_0_9, refute_0_19])).

cnf(refute_0_21, plain,
    (a_truth(implies(skolemFOFtoCNF_A, skolemFOFtoCNF_A))),
    inference(subst, [],
              [refute_0_20 : [bind(X_76, $fot(skolemFOFtoCNF_A))]])).

cnf(refute_0_22, plain, ($false),
    inference(resolve,
              [$cnf(a_truth(implies(skolemFOFtoCNF_A, skolemFOFtoCNF_A)))],
              [refute_0_21, refute_0_0])).
SZS output end CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p


WATCH: 0.00 CPU 0.03 WC

FINAL WATCH: 0.00 CPU 0.03 WC