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

WATCH: 0.00 CPU 0.01 WC

WATCH: 2.99 CPU 3.02 WC

WATCH: 6.00 CPU 6.03 WC

WATCH: 9.01 CPU 9.04 WC

WATCH: 12.01 CPU 12.05 WC
SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p

SZS output start CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p
fof(ax2_4328, axiom, (genls(c_tptpcol_16_130924, c_tptpcol_15_130923))).

fof(ax2_4304, axiom, (genls(c_tptpcol_16_130924, c_tptpcol_15_130923))).

fof(query172, conjecture,
    (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),
         c_translation_0_885)) =>
     genls(c_tptpcol_16_130924, c_tptpcol_15_130923))).

fof(subgoal_0, plain,
    (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),
         c_translation_0_885)) =>
     genls(c_tptpcol_16_130924, c_tptpcol_15_130923)),
    inference(strip, [], [query172])).

fof(negate_0_0, plain,
    (~
       (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),
            c_translation_0_885)) =>
        genls(c_tptpcol_16_130924, c_tptpcol_15_130923))),
    inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain,
    (~ genls(c_tptpcol_16_130924, c_tptpcol_15_130923) &
     mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),
         c_translation_0_885))),
    inference(canonicalize, [], [negate_0_0])).

fof(normalize_0_1, plain,
    (genls(c_tptpcol_16_130924, c_tptpcol_15_130923)),
    inference(canonicalize, [], [ax2_4304])).

fof(normalize_0_2, plain, ($false),
    inference(simplify, [], [normalize_0_0, normalize_0_1])).

cnf(refute_0_0, plain, ($false),
    inference(canonicalize, [], [normalize_0_2])).
SZS output end CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p


WATCH: 12.23 CPU 12.28 WC

FINAL WATCH: 12.23 CPU 12.28 WC