WATCH: 0.00 CPU 0.01 WC

WATCH: 2.55 CPU 3.03 WC

/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p is a Theorem
Start of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p
%-----------------------------------------------------
fof(query172,conjecture,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)),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p',query172)).
fof(ax2_4328,axiom,genls(c_tptpcol_16_130924, c_tptpcol_15_130923),file('/CW/home-0/sutcliff/TPTP/Axioms/CSR002+2.ax',ax2_4328)).

cnf(1, plain, [genls(c_tptpcol_16_130924, c_tptpcol_15_130923)], clausify(query172)).
cnf(2, plain, [-(genls(c_tptpcol_16_130924, c_tptpcol_15_130923))], clausify(ax2_4328)).

cnf('1',plain,[genls(c_tptpcol_16_130924, c_tptpcol_15_130923)],start(1)).
cnf('1.1',plain,[-(genls(c_tptpcol_16_130924, c_tptpcol_15_130923))],extension(2)).
%-----------------------------------------------------
End of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p

WATCH: 2.59 CPU 3.12 WC

FINAL WATCH: 2.59 CPU 3.12 WC