Refutation found. Thanks to Tanya!
=========== Refutation ==========
*********** [63, input] ***********
(? X123)const_eaFrom(X123) & (! X124 X125)(~const_eaFrom(X125) \/ ~const_eaFrom(X124) \/ X125=X124) & (? X126)const_epr(X126) & (! X127 X128)(~const_epr(X128) \/ ~const_epr(X127) \/ X128=X127) & (? X129)const_epv(X129) & (! X130 X131)(~const_epv(X131) \/ ~const_epv(X130) \/ X131=X130) & (? X132)const_epa(X132) & (! X133 X134)(~const_epa(X134) \/ ~const_epa(X133) \/ X134=X133)
*********** [63->137, rectify] ***********
  (? X123)const_eaFrom(X123) & (! X124 X125)(~const_eaFrom(X125) \/ ~const_eaFrom(X124) \/ X125=X124) & (? X126)const_epr(X126) & (! X127 X128)(~const_epr(X128) \/ ~const_epr(X127) \/ X128=X127) & (? X129)const_epv(X129) & (! X130 X131)(~const_epv(X131) \/ ~const_epv(X130) \/ X131=X130) & (? X132)const_epa(X132) & (! X133 X134)(~const_epa(X134) \/ ~const_epa(X133) \/ X134=X133)
-----------------------------
  (? X0)const_eaFrom(X0) & (! X1 X2)(~const_eaFrom(X2) \/ ~const_eaFrom(X1) \/ X2=X1) & (? X3)const_epr(X3) & (! X4 X5)(~const_epr(X5) \/ ~const_epr(X4) \/ X5=X4) & (? X6)const_epv(X6) & (! X7 X8)(~const_epv(X8) \/ ~const_epv(X7) \/ X8=X7) & (? X9)const_epa(X9) & (! X10 X11)(~const_epa(X11) \/ ~const_epa(X10) \/ X11=X10)
*********** [137->382, skolemization] ***********
  (? X0)const_eaFrom(X0) & (! X1 X2)(~const_eaFrom(X2) \/ ~const_eaFrom(X1) \/ X2=X1) & (? X3)const_epr(X3) & (! X4 X5)(~const_epr(X5) \/ ~const_epr(X4) \/ X5=X4) & (? X6)const_epv(X6) & (! X7 X8)(~const_epv(X8) \/ ~const_epv(X7) \/ X8=X7) & (? X9)const_epa(X9) & (! X10 X11)(~const_epa(X11) \/ ~const_epa(X10) \/ X11=X10)
-----------------------------
  const_eaFrom($s10) & (~const_eaFrom(X2) \/ ~const_eaFrom(X1) \/ X2=X1) & const_epr($s11) & (~const_epr(X5) \/ ~const_epr(X4) \/ X5=X4) & const_epv($s12) & (~const_epv(X8) \/ ~const_epv(X7) \/ X8=X7) & const_epa($s13) & (~const_epa(X11) \/ ~const_epa(X10) \/ X11=X10)
*********** [382->832, cnf transformation] ***********
  const_eaFrom($s10) & (~const_eaFrom(X2) \/ ~const_eaFrom(X1) \/ X2=X1) & const_epr($s11) & (~const_epr(X5) \/ ~const_epr(X4) \/ X5=X4) & const_epv($s12) & (~const_epv(X8) \/ ~const_epv(X7) \/ X8=X7) & const_epa($s13) & (~const_epa(X11) \/ ~const_epa(X10) \/ X11=X10)
-----------------------------
  const_epa($s13)
*********** [64, input] ***********
(! X135)(~const_epa(X135) \/ const_STATUS(X135))
*********** [64->138, rectify] ***********
  (! X135)(~const_epa(X135) \/ const_STATUS(X135))
-----------------------------
  (! X0)(~const_epa(X0) \/ const_STATUS(X0))
*********** [138->383, skolemization] ***********
  (! X0)(~const_epa(X0) \/ const_STATUS(X0))
-----------------------------
  ~const_epa(X0) \/ const_STATUS(X0)
*********** [383->834, cnf transformation] ***********
  ~const_epa(X0) \/ const_STATUS(X0)
-----------------------------
  const_STATUS(X0) \/ ~const_epa(X0)
*********** [24, input] ***********
(! X48)((~const_MESSAGE(X48) & ~const_STATUS(X48) & ~const_ConState(X48)) \/ ~const_SEQNO(X48))
*********** [24->98, rectify] ***********
  (! X48)((~const_MESSAGE(X48) & ~const_STATUS(X48) & ~const_ConState(X48)) \/ ~const_SEQNO(X48))
-----------------------------
  (! X0)((~const_MESSAGE(X0) & ~const_STATUS(X0) & ~const_ConState(X0)) \/ ~const_SEQNO(X0))
*********** [98->343, skolemization] ***********
  (! X0)((~const_MESSAGE(X0) & ~const_STATUS(X0) & ~const_ConState(X0)) \/ ~const_SEQNO(X0))
-----------------------------
  (~const_MESSAGE(X0) & ~const_STATUS(X0) & ~const_ConState(X0)) \/ ~const_SEQNO(X0)
*********** [343->766, cnf transformation] ***********
  (~const_MESSAGE(X0) & ~const_STATUS(X0) & ~const_ConState(X0)) \/ ~const_SEQNO(X0)
-----------------------------
  ~const_SEQNO(X0) \/ ~const_STATUS(X0)
*********** [5, input] ***********
(! X7 X8)(~const_seqord(X8,X7) \/ (const_SEQNO(X7) & const_SEQNO(X8)))
*********** [5->79, rectify] ***********
  (! X7 X8)(~const_seqord(X8,X7) \/ (const_SEQNO(X7) & const_SEQNO(X8)))
-----------------------------
  (! X0 X1)(~const_seqord(X1,X0) \/ (const_SEQNO(X0) & const_SEQNO(X1)))
*********** [79->324, skolemization] ***********
  (! X0 X1)(~const_seqord(X1,X0) \/ (const_SEQNO(X0) & const_SEQNO(X1)))
-----------------------------
  ~const_seqord(X1,X0) \/ (const_SEQNO(X0) & const_SEQNO(X1))
*********** [324->717, cnf transformation] ***********
  ~const_seqord(X1,X0) \/ (const_SEQNO(X0) & const_SEQNO(X1))
-----------------------------
  const_SEQNO(X0) \/ ~const_seqord(X1,X0)
*********** [71, input] ***********
(! X150 X151)(X150!=X151 \/ const_seqord(X150,X151)) & (! X152 X153)(~const_seqord(X153,X152) \/ ~const_seqord(X152,X153) \/ X152=X153) & (! X154 X155)((! X156)(~const_seqord(X154,X156) \/ ~const_seqord(X156,X155)) \/ const_seqord(X154,X155)) & (! X157 X158)(~const_SEQNO(X157) \/ ~const_SEQNO(X158) \/ const_seqord(X157,X158) \/ const_seqord(X158,X157))
*********** [71->145, rectify] ***********
  (! X150 X151)(X150!=X151 \/ const_seqord(X150,X151)) & (! X152 X153)(~const_seqord(X153,X152) \/ ~const_seqord(X152,X153) \/ X152=X153) & (! X154 X155)((! X156)(~const_seqord(X154,X156) \/ ~const_seqord(X156,X155)) \/ const_seqord(X154,X155)) & (! X157 X158)(~const_SEQNO(X157) \/ ~const_SEQNO(X158) \/ const_seqord(X157,X158) \/ const_seqord(X158,X157))
-----------------------------
  (! X0 X1)(X0!=X1 \/ const_seqord(X0,X1)) & (! X2 X3)(~const_seqord(X3,X2) \/ ~const_seqord(X2,X3) \/ X2=X3) & (! X4 X5)((! X6)(~const_seqord(X4,X6) \/ ~const_seqord(X6,X5)) \/ const_seqord(X4,X5)) & (! X7 X8)(~const_SEQNO(X7) \/ ~const_SEQNO(X8) \/ const_seqord(X7,X8) \/ const_seqord(X8,X7))
*********** [145->390, skolemization] ***********
  (! X0 X1)(X0!=X1 \/ const_seqord(X0,X1)) & (! X2 X3)(~const_seqord(X3,X2) \/ ~const_seqord(X2,X3) \/ X2=X3) & (! X4 X5)((! X6)(~const_seqord(X4,X6) \/ ~const_seqord(X6,X5)) \/ const_seqord(X4,X5)) & (! X7 X8)(~const_SEQNO(X7) \/ ~const_SEQNO(X8) \/ const_seqord(X7,X8) \/ const_seqord(X8,X7))
-----------------------------
  (X0!=X1 \/ const_seqord(X0,X1)) & (~const_seqord(X3,X2) \/ ~const_seqord(X2,X3) \/ X2=X3) & ((~const_seqord(X4,X6) \/ ~const_seqord(X6,X5)) \/ const_seqord(X4,X5)) & (~const_SEQNO(X7) \/ ~const_SEQNO(X8) \/ const_seqord(X7,X8) \/ const_seqord(X8,X7))
*********** [390->843, cnf transformation] ***********
  (X0!=X1 \/ const_seqord(X0,X1)) & (~const_seqord(X3,X2) \/ ~const_seqord(X2,X3) \/ X2=X3) & ((~const_seqord(X4,X6) \/ ~const_seqord(X6,X5)) \/ const_seqord(X4,X5)) & (~const_SEQNO(X7) \/ ~const_SEQNO(X8) \/ const_seqord(X7,X8) \/ const_seqord(X8,X7))
-----------------------------
  const_seqord(X0,X1) \/ X0!=X1
*********** [843->3939, equality resolution] ***********
  const_seqord(X0,X1) \/ X0!=X1
-----------------------------
  const_seqord(X1,X1)
*********** [717,3939->5271, resolution] ***********
  const_SEQNO(X0) \/ ~const_seqord(X1,X0)
  const_seqord(X1,X1)
-----------------------------
  const_SEQNO(X1)
*********** [766,5271->5273, resolution] ***********
  ~const_SEQNO(X0) \/ ~const_STATUS(X0)
  const_SEQNO(X1)
-----------------------------
  ~const_STATUS(X1)
*********** [834,5273->5280, resolution] ***********
  const_STATUS(X0) \/ ~const_epa(X0)
  ~const_STATUS(X1)
-----------------------------
  ~const_epa(X1)
*********** [832,5280->5309, resolution] ***********
  const_epa($s13)
  ~const_epa(X1)
-----------------------------
  #
======= End of refutation =======
=========== Statistics ==========
version: 7.45 Civatateo (v7.44 + more ASSERT's in LPO + several bug fixes in LPO)
=== General:
time: 0.2s
memory: 19.4Mb
termination reason: refutation found
=== Generating inferences:
resolution: 2359
equality_resolution: 1
=== Simplifying inferences:
propositional_tautology: 42
equational_tautology: 1
forward_subsumption: 285
forward_subsumption_resolution: 316
backward_subsumption: 1017
=== Generated clauses:
total: 4784
discarded_as_redundant: 328
=== Retained clauses:
total: 3244
selected: 1253
currently_active: 938
currently_passive: 1288
======= End of statistics =======