Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!
% remaining time: 3000 next slice time: 185
dis-1002_3_bs=off:bsr=unit_only:gsp=input_only:gs=on:lcm=reverse:nwc=3:ptb=off:ssec=off:sac=on:sgo=on:sio=off:spo=on:swb=on:sp=occurrence:urr=on:updr=off_168 on FNE045
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE045
% SZS output start Proof for FNE045
64. $false (2:0) [unit resulting resolution 7,8,34,6]
6. ~a_truth(implies(X0,X1)) | a_truth(X1) | ~a_truth(X0) (0:8) [cnf transformation 5]
5. ! [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))))[skolemisation 4]
4. ! [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))))[flattening 3]
3. ~~(! [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)))))[rectify 2]
2. ~~(! [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)))))[negated conjecture 1]
1. ~(! [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)))))[input]
34. a_truth(implies(implies(X0,X1),implies(X0,X0))) (1:8) [unit resulting resolution 7,10,6]
10. a_truth(implies(implies(X7,implies(X8,X9)),implies(implies(X7,X8),implies(X7,X9)))) (0:14) [cnf transformation 5]
8. ~a_truth(implies(sK0,sK0)) (0:4) [cnf transformation 5]
7. a_truth(implies(X2,implies(X3,X2))) (0:6) [cnf transformation 5]
% SZS output end Proof for FNE045
------------------------------
Version: Vampire 1.8 (revision 1280)
Termination reason: Refutation

Active clauses: 11
Passive clauses: 43
Generated clauses: 60
Final active clauses: 11
Final passive clauses: 30
Input formulas: 1
Initial clauses: 5

Simple tautologies: 1
Forward subsumptions: 10

Binary resolution: 8
Unit resulting resolution: 58

SAT solver clauses: 54
SAT solver unit clauses: 48
SAT solver binary clauses: 4

Memory used [KB]: 255
Time elapsed: 0.0000 s
------------------------------

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

WATCH: 0.00 CPU 0.03 WC

FINAL WATCH: 0.00 CPU 0.03 WC