WATCH: 0.00 CPU 0.01 WC
Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 2999 next slice time: 17
dis-1002_5:1_bs=unit_only:bsr=unit_only:flr=on:gsp=input_only:lcm=predicate:nwc=1:nicw=on:ptb=off:ssec=off:sswn=on:sos=on:spo=on:swb=on:sp=occurrence_15 on FNE044
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE044
% SZS output start Proof for FNE044
23011. $false (0:0) [subsumption resolution 15724,16483]
16483. genls(c_tptpcol_16_130924,c_tptpcol_15_130923) (0:3) [cnf transformation 4108]
4108. genls(c_tptpcol_16_130924,c_tptpcol_15_130923)[input]
15724. ~genls(c_tptpcol_16_130924,c_tptpcol_15_130923) (0:3) [cnf transformation 11049]
11049. 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)[ennf transformation 8007]
8007. ~(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))[negated conjecture 8006]
8006. 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)[input]
% SZS output end Proof for FNE044
------------------------------
Version: Vampire 1.8 (revision 1280)
Termination reason: Refutation

Active clauses: 7286
Generated clauses: 3
Final active clauses: 7286
Input formulas: 8006
Initial clauses: 7288

Pure predicates: 217

Fw subsumption resolutions: 1

Memory used [KB]: 12153
Time elapsed: 0.017 s
------------------------------
% Success in time 0.16 s

WATCH: 0.14 CPU 0.17 WC

FINAL WATCH: 0.14 CPU 0.17 WC