% 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: 3000 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 FNE045
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE045
% SZS output start Proof for FNE045
fof(f32,plain,(
  $false),
  inference(resolution,[],[f26,f7])).
fof(f7,plain,(
  ~a_truth(implies(sK0,sK0))),
  inference(cnf_transformation,[],[f4])).
fof(f4,plain,(
  ! [X0,X1] : (~a_truth(X0) | a_truth(X1) | ~a_truth(implies(X0,X1))) & ! [X2,X3] : a_truth(implies(X2,implies(X3,X2))) & ~a_truth(implies(sK0,sK0)) & ! [X5,X6] : a_truth(implies(implies(not(X5),not(X6)),implies(X6,X5))) & ! [X7,X8,X9] : a_truth(implies(implies(X7,implies(X8,X9)),implies(implies(X7,X8),implies(X7,X9))))),
  inference(skolemisation,[status(esa)],[f3])).
fof(f3,plain,(
  ! [X0,X1] : (~a_truth(X0) | a_truth(X1) | ~a_truth(implies(X0,X1))) & ! [X2,X3] : a_truth(implies(X2,implies(X3,X2))) & ? [X4] : ~a_truth(implies(X4,X4)) & ! [X5,X6] : a_truth(implies(implies(not(X5),not(X6)),implies(X6,X5))) & ! [X7,X8,X9] : a_truth(implies(implies(X7,implies(X8,X9)),implies(implies(X7,X8),implies(X7,X9))))),
  inference(ennf_transformation,[],[f2])).
fof(f2,plain,(
  ~~(! [X0,X1] : (~a_truth(X0) | a_truth(X1) | ~a_truth(implies(X0,X1))) & ! [X2,X3] : a_truth(implies(X2,implies(X3,X2))) & ? [X4] : ~a_truth(implies(X4,X4)) & ! [X5,X6] : a_truth(implies(implies(not(X5),not(X6)),implies(X6,X5))) & ! [X7,X8,X9] : a_truth(implies(implies(X7,implies(X8,X9)),implies(implies(X7,X8),implies(X7,X9)))))),
  inference(rectify,[],[f1])).
fof(f1,negated_conjecture,(
  ~~(! [X0,X1] : (~a_truth(X0) | a_truth(X1) | ~a_truth(implies(X0,X1))) & ! [X0,X1] : a_truth(implies(X0,implies(X1,X0))) & ? [X2] : ~a_truth(implies(X2,X2)) & ! [X0,X1] : a_truth(implies(implies(not(X0),not(X1)),implies(X1,X0))) & ! [X0,X1,X3] : a_truth(implies(implies(X0,implies(X1,X3)),implies(implies(X0,X1),implies(X0,X3)))))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p',thm147)).
fof(f26,plain,(
  ( ! [X0] : (a_truth(implies(X0,X0))) )),
  inference(resolution,[],[f20,f6])).
fof(f6,plain,(
  ( ! [X2,X3] : (a_truth(implies(X2,implies(X3,X2)))) )),
  inference(cnf_transformation,[],[f4])).
fof(f20,plain,(
  ( ! [X0,X1] : (~a_truth(implies(X0,X1)) | a_truth(implies(X0,X0))) )),
  inference(resolution,[],[f19,f6])).
fof(f19,plain,(
  ( ! [X2,X0,X1] : (~a_truth(implies(X0,implies(X1,X2))) | a_truth(implies(X0,X2)) | ~a_truth(implies(X0,X1))) )),
  inference(resolution,[],[f18,f5])).
fof(f5,plain,(
  ( ! [X0,X1] : (~a_truth(implies(X0,X1)) | a_truth(X1) | ~a_truth(X0)) )),
  inference(cnf_transformation,[],[f4])).
fof(f18,plain,(
  ( ! [X2,X0,X1] : (a_truth(implies(implies(X0,X1),implies(X0,X2))) | ~a_truth(implies(X0,implies(X1,X2)))) )),
  inference(resolution,[],[f9,f5])).
fof(f9,plain,(
  ( ! [X8,X7,X9] : (a_truth(implies(implies(X7,implies(X8,X9)),implies(implies(X7,X8),implies(X7,X9))))) )),
  inference(cnf_transformation,[],[f4])).
% SZS output end Proof for FNE045
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 16
Passive clauses: 24
Generated clauses: 32
Final active clauses: 16
Final passive clauses: 8
Input formulas: 1
Initial clauses: 5

Simple tautologies: 2
Forward subsumptions: 2

Binary resolution: 27

Unique components: 5

Memory used: 127KB
Time elapsed: 0.001 s
------------------------------

WATCH: 0.00 CPU 0.01 WC
% Success in time 0.002 s

WATCH: 0.00 CPU 0.03 WC

FINAL WATCH: 0.00 CPU 0.03 WC