WATCH: 0.00 CPU 0.01 WC
% Vampire version 0.6 licenced to run at CASC-J5
% Any licence to use Vampire shall only be obtained
% as described on Vampire's home page http://www.vprover.org.
Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 2999 next slice time: 84
dis+10_10_bs=off:gsp=input_only:lcm=reverse:nwc=10.0:nicw=on:sswn=on:sgo=on_62 on FNE044
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE044
% SZS output start Proof for FNE044
fof(f23008,plain,(
  $false),
  inference(subsumption_resolution,[],[f16391,f15721])).
fof(f15721,plain,(
  ~genls(c_tptpcol_16_130924,c_tptpcol_15_130923)),
  inference(cnf_transformation,[],[f11016])).
fof(f11016,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(ennf_transformation,[],[f8006])).
fof(f8006,negated_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))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p',query172)).
fof(f16391,plain,(
  genls(c_tptpcol_16_130924,c_tptpcol_15_130923)),
  inference(cnf_transformation,[],[f4847])).
fof(f4847,axiom,(
  genls(c_tptpcol_16_130924,c_tptpcol_15_130923)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE044.p',ax2_4304)).
% SZS output end Proof for FNE044
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 606
Passive clauses: 7288
Generated clauses: 7289
Final active clauses: 606
Final passive clauses: 6615
Input formulas: 8006
Initial clauses: 7288

Pure predicates: 217

Fw subsumption resolutions: 1

Forward subsumptions: 66

Unique components: 2

Memory used: 8315KB
Time elapsed: 0.095 s
------------------------------
% Success in time 0.13 s

WATCH: 0.12 CPU 0.16 WC

FINAL WATCH: 0.12 CPU 0.16 WC