% 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 FNE056

WATCH: 0.00 CPU 0.01 WC
Refutation found. Thanks to Tanya!
% SZS status Theorem for FNE056
% SZS output start Proof for FNE056
fof(f6546,plain,(
  $false),
  inference(subsumption_resolution,[],[f6545,f189])).
fof(f189,plain,(
  sP0(sK30)),
  inference(resolution,[],[f186,f182])).
fof(f182,plain,(
  ( ! [X1] : (~r1(sK30,X1) | sP0(X1)) )),
  inference(cnf_transformation,[],[f16])).
fof(f16,plain,(
  ! [X1] : (~r1(sK30,X1) | sP0(X1)) & p100(sK30) & ~p101(sK30) & ! [X2] : (~r1(sK30,X2) | p7(X2))),
  inference(skolemisation,[status(esa)],[f15])).
fof(f15,plain,(
  ? [X0] : (! [X1] : (~r1(X0,X1) | sP0(X1)) & p100(X0) & ~p101(X0) & ! [X2] : (~r1(X0,X2) | p7(X2)))),
  inference(rectify,[],[f11])).
fof(f11,plain,(
  ? [X0] : (! [X1] : (~r1(X0,X1) | sP0(X1)) & p100(X0) & ~p101(X0) & ! [X64] : (~r1(X0,X64) | p7(X64)))),
  inference(definition_folding,[],[f10])).
fof(f10,plain,(
  ! [X1] : (~sP0(X1) | (((? [X2] : (~p15(X2) & ~p115(X2) & p114(X2) & r1(X1,X2)) & ? [X3] : (p15(X3) & p114(X3) & ~p115(X3) & r1(X1,X3))) | ~p113(X1) | p114(X1)) & ((? [X4] : (p13(X4) & ~p113(X4) & p112(X4) & r1(X1,X4)) & ? [X5] : (~p13(X5) & ~p113(X5) & p112(X5) & r1(X1,X5))) | ~p111(X1) | p112(X1)) & (p106(X1) | ~p105(X1) | (? [X6] : (~p107(X6) & p106(X6) & p7(X6) & r1(X1,X6)) & ? [X7] : (r1(X1,X7) & ~p107(X7) & p106(X7) & ~p7(X7)))) & ((? [X8] : (~p105(X8) & p104(X8) & ~p5(X8) & r1(X1,X8)) & ? [X9] : (r1(X1,X9) & p104(X9) & ~p105(X9) & p5(X9))) | ~p103(X1) | p104(X1)) & (p103(X1) | ~p102(X1) | (? [X10] : (r1(X1,X10) & p4(X10) & ~p104(X10) & p103(X10)) & ? [X11] : (~p4(X11) & ~p104(X11) & p103(X11) & r1(X1,X11)))) & ((? [X12] : (~p3(X12) & ~p103(X12) & p102(X12) & r1(X1,X12)) & ? [X13] : (r1(X1,X13) & p102(X13) & ~p103(X13) & p3(X13))) | p102(X1) | ~p101(X1)) & ((? [X14] : (r1(X1,X14) & ~p2(X14) & p101(X14) & ~p102(X14)) & ? [X15] : (p2(X15) & p101(X15) & ~p102(X15) & r1(X1,X15))) | ~p100(X1) | p101(X1)) & (((! [X16] : (~p16(X16) | ~p115(X16) | ~r1(X1,X16)) | p16(X1)) & (! [X17] : (~p115(X17) | p16(X17) | ~r1(X1,X17)) | ~p16(X1))) | ~p115(X1)) & (~p114(X1) | ((p15(X1) | ! [X18] : (~r1(X1,X18) | ~p15(X18) | ~p114(X18))) & (~p15(X1) | ! [X19] : (~r1(X1,X19) | p15(X19) | ~p114(X19))))) & (~p113(X1) | ((p14(X1) | ! [X20] : (~p113(X20) | ~p14(X20) | ~r1(X1,X20))) & (~p14(X1) | ! [X21] : (~p113(X21) | p14(X21) | ~r1(X1,X21))))) & (((~p13(X1) | ! [X22] : (~r1(X1,X22) | p13(X22) | ~p112(X22))) & (p13(X1) | ! [X23] : (~p112(X23) | ~p13(X23) | ~r1(X1,X23)))) | ~p112(X1)) & (((! [X24] : (~r1(X1,X24) | ~p100(X24) | ~p1(X24)) | p1(X1)) & (~p1(X1) | ! [X25] : (~r1(X1,X25) | p1(X25) | ~p100(X25)))) | ~p100(X1)) & (p113(X1) | ~p114(X1)) & (p111(X1) | ~p112(X1)) & (p110(X1) | ~p111(X1)) & (p109(X1) | ~p110(X1)) & (p108(X1) | ~p109(X1)) & (~p108(X1) | p107(X1)) & (p106(X1) | ~p107(X1)) & (p104(X1) | ~p105(X1)) & (~p103(X1) | p102(X1)) & (p100(X1) | ~p101(X1)) & (p101(X1) | ~p102(X1)) & (p103(X1) | ~p104(X1)) & (p105(X1) | ~p106(X1)) & (~p113(X1) | p112(X1)) & (p114(X1) | ~p115(X1)) & (((~p2(X1) | ! [X26] : (~p101(X26) | p2(X26) | ~r1(X1,X26))) & (p2(X1) | ! [X27] : (~r1(X1,X27) | ~p2(X27) | ~p101(X27)))) | ~p101(X1)) & (((! [X28] : (p3(X28) | ~p102(X28) | ~r1(X1,X28)) | ~p3(X1)) & (! [X29] : (~p3(X29) | ~p102(X29) | ~r1(X1,X29)) | p3(X1))) | ~p102(X1)) & (~p103(X1) | ((p4(X1) | ! [X30] : (~p103(X30) | ~p4(X30) | ~r1(X1,X30))) & (! [X31] : (~r1(X1,X31) | p4(X31) | ~p103(X31)) | ~p4(X1)))) & (((! [X32] : (p5(X32) | ~p104(X32) | ~r1(X1,X32)) | ~p5(X1)) & (p5(X1) | ! [X33] : (~r1(X1,X33) | ~p104(X33) | ~p5(X33)))) | ~p104(X1)) & (((~p6(X1) | ! [X34] : (~p105(X34) | p6(X34) | ~r1(X1,X34))) & (! [X35] : (~p105(X35) | ~p6(X35) | ~r1(X1,X35)) | p6(X1))) | ~p105(X1)) & (~p106(X1) | ((! [X36] : (~r1(X1,X36) | ~p7(X36) | ~p106(X36)) | p7(X1)) & (! [X37] : (~r1(X1,X37) | ~p106(X37) | p7(X37)) | ~p7(X1)))) & (((p8(X1) | ! [X38] : (~p8(X38) | ~p107(X38) | ~r1(X1,X38))) & (~p8(X1) | ! [X39] : (~r1(X1,X39) | ~p107(X39) | p8(X39)))) | ~p107(X1)) & (~p108(X1) | ((~p9(X1) | ! [X40] : (~p108(X40) | p9(X40) | ~r1(X1,X40))) & (! [X41] : (~r1(X1,X41) | ~p108(X41) | ~p9(X41)) | p9(X1)))) & (((p10(X1) | ! [X42] : (~p109(X42) | ~p10(X42) | ~r1(X1,X42))) & (~p10(X1) | ! [X43] : (~r1(X1,X43) | ~p109(X43) | p10(X43)))) | ~p109(X1)) & (~p110(X1) | ((! [X44] : (~r1(X1,X44) | p11(X44) | ~p110(X44)) | ~p11(X1)) & (p11(X1) | ! [X45] : (~p11(X45) | ~p110(X45) | ~r1(X1,X45))))) & (~p111(X1) | ((p12(X1) | ! [X46] : (~p12(X46) | ~p111(X46) | ~r1(X1,X46))) & (~p12(X1) | ! [X47] : (p12(X47) | ~p111(X47) | ~r1(X1,X47))))) & ((? [X48] : (~p6(X48) & p105(X48) & ~p106(X48) & r1(X1,X48)) & ? [X49] : (r1(X1,X49) & p6(X49) & p105(X49) & ~p106(X49))) | p105(X1) | ~p104(X1)) & ((? [X50] : (r1(X1,X50) & ~p8(X50) & ~p108(X50) & p107(X50)) & ? [X51] : (r1(X1,X51) & p8(X51) & ~p108(X51) & p107(X51))) | p107(X1) | ~p106(X1)) & (~p107(X1) | p108(X1) | (? [X52] : (r1(X1,X52) & ~p109(X52) & p108(X52) & p9(X52)) & ? [X53] : (p108(X53) & ~p109(X53) & ~p9(X53) & r1(X1,X53)))) & ((? [X54] : (p109(X54) & ~p110(X54) & ~p10(X54) & r1(X1,X54)) & ? [X55] : (p109(X55) & ~p110(X55) & p10(X55) & r1(X1,X55))) | p109(X1) | ~p108(X1)) & ((? [X56] : (p11(X56) & ~p111(X56) & p110(X56) & r1(X1,X56)) & ? [X57] : (r1(X1,X57) & ~p111(X57) & p110(X57) & ~p11(X57))) | p110(X1) | ~p109(X1)) & (~p110(X1) | p111(X1) | (? [X58] : (~p112(X58) & p111(X58) & p12(X58) & r1(X1,X58)) & ? [X59] : (~p112(X59) & p111(X59) & ~p12(X59) & r1(X1,X59)))) & (p113(X1) | ~p112(X1) | (? [X60] : (r1(X1,X60) & p113(X60) & ~p114(X60) & p14(X60)) & ? [X61] : (p113(X61) & ~p114(X61) & ~p14(X61) & r1(X1,X61)))) & ((? [X62] : (p115(X62) & ~p16(X62) & r1(X1,X62)) & ? [X63] : (r1(X1,X63) & p115(X63) & p16(X63))) | p115(X1) | ~p114(X1))))),
  introduced(predicate_definition_introduction,[])).
fof(f186,plain,(
  ( ! [X0] : (r1(X0,X0)) )),
  inference(cnf_transformation,[],[f3])).
fof(f3,axiom,(
  ! [X0] : r1(X0,X0)),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p',reflexivity)).
fof(f6545,plain,(
  ~sP0(sK30)),
  inference(subsumption_resolution,[],[f6544,f184])).
fof(f184,plain,(
  ~p101(sK30)),
  inference(cnf_transformation,[],[f16])).
fof(f6544,plain,(
  p101(sK30) | ~sP0(sK30)),
  inference(subsumption_resolution,[],[f6543,f183])).
fof(f183,plain,(
  p100(sK30)),
  inference(cnf_transformation,[],[f16])).
fof(f6543,plain,(
  ~p100(sK30) | p101(sK30) | ~sP0(sK30)),
  inference(subsumption_resolution,[],[f6542,f67])).
fof(f67,plain,(
  ( ! [X0] : (p101(sK12(X0)) | ~p100(X0) | p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f14,plain,(
  ! [X0] : (~sP0(X0) | ((((~p15(sK0(X0)) & ~p115(sK0(X0)) & p114(sK0(X0)) & r1(X0,sK0(X0))) & (p15(sK1(X0)) & p114(sK1(X0)) & ~p115(sK1(X0)) & r1(X0,sK1(X0)))) | ~p113(X0) | p114(X0)) & (((p13(sK2(X0)) & ~p113(sK2(X0)) & p112(sK2(X0)) & r1(X0,sK2(X0))) & (~p13(sK3(X0)) & ~p113(sK3(X0)) & p112(sK3(X0)) & r1(X0,sK3(X0)))) | ~p111(X0) | p112(X0)) & (p106(X0) | ~p105(X0) | ((~p107(sK4(X0)) & p106(sK4(X0)) & p7(sK4(X0)) & r1(X0,sK4(X0))) & (r1(X0,sK5(X0)) & ~p107(sK5(X0)) & p106(sK5(X0)) & ~p7(sK5(X0))))) & (((~p105(sK6(X0)) & p104(sK6(X0)) & ~p5(sK6(X0)) & r1(X0,sK6(X0))) & (r1(X0,sK7(X0)) & p104(sK7(X0)) & ~p105(sK7(X0)) & p5(sK7(X0)))) | ~p103(X0) | p104(X0)) & (p103(X0) | ~p102(X0) | ((r1(X0,sK8(X0)) & p4(sK8(X0)) & ~p104(sK8(X0)) & p103(sK8(X0))) & (~p4(sK9(X0)) & ~p104(sK9(X0)) & p103(sK9(X0)) & r1(X0,sK9(X0))))) & (((~p3(sK10(X0)) & ~p103(sK10(X0)) & p102(sK10(X0)) & r1(X0,sK10(X0))) & (r1(X0,sK11(X0)) & p102(sK11(X0)) & ~p103(sK11(X0)) & p3(sK11(X0)))) | p102(X0) | ~p101(X0)) & (((r1(X0,sK12(X0)) & ~p2(sK12(X0)) & p101(sK12(X0)) & ~p102(sK12(X0))) & (p2(sK13(X0)) & p101(sK13(X0)) & ~p102(sK13(X0)) & r1(X0,sK13(X0)))) | ~p100(X0) | p101(X0)) & (((! [X15] : (~p16(X15) | ~p115(X15) | ~r1(X0,X15)) | p16(X0)) & (! [X16] : (~p115(X16) | p16(X16) | ~r1(X0,X16)) | ~p16(X0))) | ~p115(X0)) & (~p114(X0) | ((p15(X0) | ! [X17] : (~r1(X0,X17) | ~p15(X17) | ~p114(X17))) & (~p15(X0) | ! [X18] : (~r1(X0,X18) | p15(X18) | ~p114(X18))))) & (~p113(X0) | ((p14(X0) | ! [X19] : (~p113(X19) | ~p14(X19) | ~r1(X0,X19))) & (~p14(X0) | ! [X20] : (~p113(X20) | p14(X20) | ~r1(X0,X20))))) & (((~p13(X0) | ! [X21] : (~r1(X0,X21) | p13(X21) | ~p112(X21))) & (p13(X0) | ! [X22] : (~p112(X22) | ~p13(X22) | ~r1(X0,X22)))) | ~p112(X0)) & (((! [X23] : (~r1(X0,X23) | ~p100(X23) | ~p1(X23)) | p1(X0)) & (~p1(X0) | ! [X24] : (~r1(X0,X24) | p1(X24) | ~p100(X24)))) | ~p100(X0)) & (p113(X0) | ~p114(X0)) & (p111(X0) | ~p112(X0)) & (p110(X0) | ~p111(X0)) & (p109(X0) | ~p110(X0)) & (p108(X0) | ~p109(X0)) & (~p108(X0) | p107(X0)) & (p106(X0) | ~p107(X0)) & (p104(X0) | ~p105(X0)) & (~p103(X0) | p102(X0)) & (p100(X0) | ~p101(X0)) & (p101(X0) | ~p102(X0)) & (p103(X0) | ~p104(X0)) & (p105(X0) | ~p106(X0)) & (~p113(X0) | p112(X0)) & (p114(X0) | ~p115(X0)) & (((~p2(X0) | ! [X25] : (~p101(X25) | p2(X25) | ~r1(X0,X25))) & (p2(X0) | ! [X26] : (~r1(X0,X26) | ~p2(X26) | ~p101(X26)))) | ~p101(X0)) & (((! [X27] : (p3(X27) | ~p102(X27) | ~r1(X0,X27)) | ~p3(X0)) & (! [X28] : (~p3(X28) | ~p102(X28) | ~r1(X0,X28)) | p3(X0))) | ~p102(X0)) & (~p103(X0) | ((p4(X0) | ! [X29] : (~p103(X29) | ~p4(X29) | ~r1(X0,X29))) & (! [X30] : (~r1(X0,X30) | p4(X30) | ~p103(X30)) | ~p4(X0)))) & (((! [X31] : (p5(X31) | ~p104(X31) | ~r1(X0,X31)) | ~p5(X0)) & (p5(X0) | ! [X32] : (~r1(X0,X32) | ~p104(X32) | ~p5(X32)))) | ~p104(X0)) & (((~p6(X0) | ! [X33] : (~p105(X33) | p6(X33) | ~r1(X0,X33))) & (! [X34] : (~p105(X34) | ~p6(X34) | ~r1(X0,X34)) | p6(X0))) | ~p105(X0)) & (~p106(X0) | ((! [X35] : (~r1(X0,X35) | ~p7(X35) | ~p106(X35)) | p7(X0)) & (! [X36] : (~r1(X0,X36) | ~p106(X36) | p7(X36)) | ~p7(X0)))) & (((p8(X0) | ! [X37] : (~p8(X37) | ~p107(X37) | ~r1(X0,X37))) & (~p8(X0) | ! [X38] : (~r1(X0,X38) | ~p107(X38) | p8(X38)))) | ~p107(X0)) & (~p108(X0) | ((~p9(X0) | ! [X39] : (~p108(X39) | p9(X39) | ~r1(X0,X39))) & (! [X40] : (~r1(X0,X40) | ~p108(X40) | ~p9(X40)) | p9(X0)))) & (((p10(X0) | ! [X41] : (~p109(X41) | ~p10(X41) | ~r1(X0,X41))) & (~p10(X0) | ! [X42] : (~r1(X0,X42) | ~p109(X42) | p10(X42)))) | ~p109(X0)) & (~p110(X0) | ((! [X43] : (~r1(X0,X43) | p11(X43) | ~p110(X43)) | ~p11(X0)) & (p11(X0) | ! [X44] : (~p11(X44) | ~p110(X44) | ~r1(X0,X44))))) & (~p111(X0) | ((p12(X0) | ! [X45] : (~p12(X45) | ~p111(X45) | ~r1(X0,X45))) & (~p12(X0) | ! [X46] : (p12(X46) | ~p111(X46) | ~r1(X0,X46))))) & (((~p6(sK14(X0)) & p105(sK14(X0)) & ~p106(sK14(X0)) & r1(X0,sK14(X0))) & (r1(X0,sK15(X0)) & p6(sK15(X0)) & p105(sK15(X0)) & ~p106(sK15(X0)))) | p105(X0) | ~p104(X0)) & (((r1(X0,sK16(X0)) & ~p8(sK16(X0)) & ~p108(sK16(X0)) & p107(sK16(X0))) & (r1(X0,sK17(X0)) & p8(sK17(X0)) & ~p108(sK17(X0)) & p107(sK17(X0)))) | p107(X0) | ~p106(X0)) & (~p107(X0) | p108(X0) | ((r1(X0,sK18(X0)) & ~p109(sK18(X0)) & p108(sK18(X0)) & p9(sK18(X0))) & (p108(sK19(X0)) & ~p109(sK19(X0)) & ~p9(sK19(X0)) & r1(X0,sK19(X0))))) & (((p109(sK20(X0)) & ~p110(sK20(X0)) & ~p10(sK20(X0)) & r1(X0,sK20(X0))) & (p109(sK21(X0)) & ~p110(sK21(X0)) & p10(sK21(X0)) & r1(X0,sK21(X0)))) | p109(X0) | ~p108(X0)) & (((p11(sK22(X0)) & ~p111(sK22(X0)) & p110(sK22(X0)) & r1(X0,sK22(X0))) & (r1(X0,sK23(X0)) & ~p111(sK23(X0)) & p110(sK23(X0)) & ~p11(sK23(X0)))) | p110(X0) | ~p109(X0)) & (~p110(X0) | p111(X0) | ((~p112(sK24(X0)) & p111(sK24(X0)) & p12(sK24(X0)) & r1(X0,sK24(X0))) & (~p112(sK25(X0)) & p111(sK25(X0)) & ~p12(sK25(X0)) & r1(X0,sK25(X0))))) & (p113(X0) | ~p112(X0) | ((r1(X0,sK26(X0)) & p113(sK26(X0)) & ~p114(sK26(X0)) & p14(sK26(X0))) & (p113(sK27(X0)) & ~p114(sK27(X0)) & ~p14(sK27(X0)) & r1(X0,sK27(X0))))) & (((p115(sK28(X0)) & ~p16(sK28(X0)) & r1(X0,sK28(X0))) & (r1(X0,sK29(X0)) & p115(sK29(X0)) & p16(sK29(X0)))) | p115(X0) | ~p114(X0))))),
  inference(skolemisation,[status(esa)],[f13])).
fof(f13,plain,(
  ! [X0] : (~sP0(X0) | (((? [X1] : (~p15(X1) & ~p115(X1) & p114(X1) & r1(X0,X1)) & ? [X2] : (p15(X2) & p114(X2) & ~p115(X2) & r1(X0,X2))) | ~p113(X0) | p114(X0)) & ((? [X3] : (p13(X3) & ~p113(X3) & p112(X3) & r1(X0,X3)) & ? [X4] : (~p13(X4) & ~p113(X4) & p112(X4) & r1(X0,X4))) | ~p111(X0) | p112(X0)) & (p106(X0) | ~p105(X0) | (? [X5] : (~p107(X5) & p106(X5) & p7(X5) & r1(X0,X5)) & ? [X6] : (r1(X0,X6) & ~p107(X6) & p106(X6) & ~p7(X6)))) & ((? [X7] : (~p105(X7) & p104(X7) & ~p5(X7) & r1(X0,X7)) & ? [X8] : (r1(X0,X8) & p104(X8) & ~p105(X8) & p5(X8))) | ~p103(X0) | p104(X0)) & (p103(X0) | ~p102(X0) | (? [X9] : (r1(X0,X9) & p4(X9) & ~p104(X9) & p103(X9)) & ? [X10] : (~p4(X10) & ~p104(X10) & p103(X10) & r1(X0,X10)))) & ((? [X11] : (~p3(X11) & ~p103(X11) & p102(X11) & r1(X0,X11)) & ? [X12] : (r1(X0,X12) & p102(X12) & ~p103(X12) & p3(X12))) | p102(X0) | ~p101(X0)) & ((? [X13] : (r1(X0,X13) & ~p2(X13) & p101(X13) & ~p102(X13)) & ? [X14] : (p2(X14) & p101(X14) & ~p102(X14) & r1(X0,X14))) | ~p100(X0) | p101(X0)) & (((! [X15] : (~p16(X15) | ~p115(X15) | ~r1(X0,X15)) | p16(X0)) & (! [X16] : (~p115(X16) | p16(X16) | ~r1(X0,X16)) | ~p16(X0))) | ~p115(X0)) & (~p114(X0) | ((p15(X0) | ! [X17] : (~r1(X0,X17) | ~p15(X17) | ~p114(X17))) & (~p15(X0) | ! [X18] : (~r1(X0,X18) | p15(X18) | ~p114(X18))))) & (~p113(X0) | ((p14(X0) | ! [X19] : (~p113(X19) | ~p14(X19) | ~r1(X0,X19))) & (~p14(X0) | ! [X20] : (~p113(X20) | p14(X20) | ~r1(X0,X20))))) & (((~p13(X0) | ! [X21] : (~r1(X0,X21) | p13(X21) | ~p112(X21))) & (p13(X0) | ! [X22] : (~p112(X22) | ~p13(X22) | ~r1(X0,X22)))) | ~p112(X0)) & (((! [X23] : (~r1(X0,X23) | ~p100(X23) | ~p1(X23)) | p1(X0)) & (~p1(X0) | ! [X24] : (~r1(X0,X24) | p1(X24) | ~p100(X24)))) | ~p100(X0)) & (p113(X0) | ~p114(X0)) & (p111(X0) | ~p112(X0)) & (p110(X0) | ~p111(X0)) & (p109(X0) | ~p110(X0)) & (p108(X0) | ~p109(X0)) & (~p108(X0) | p107(X0)) & (p106(X0) | ~p107(X0)) & (p104(X0) | ~p105(X0)) & (~p103(X0) | p102(X0)) & (p100(X0) | ~p101(X0)) & (p101(X0) | ~p102(X0)) & (p103(X0) | ~p104(X0)) & (p105(X0) | ~p106(X0)) & (~p113(X0) | p112(X0)) & (p114(X0) | ~p115(X0)) & (((~p2(X0) | ! [X25] : (~p101(X25) | p2(X25) | ~r1(X0,X25))) & (p2(X0) | ! [X26] : (~r1(X0,X26) | ~p2(X26) | ~p101(X26)))) | ~p101(X0)) & (((! [X27] : (p3(X27) | ~p102(X27) | ~r1(X0,X27)) | ~p3(X0)) & (! [X28] : (~p3(X28) | ~p102(X28) | ~r1(X0,X28)) | p3(X0))) | ~p102(X0)) & (~p103(X0) | ((p4(X0) | ! [X29] : (~p103(X29) | ~p4(X29) | ~r1(X0,X29))) & (! [X30] : (~r1(X0,X30) | p4(X30) | ~p103(X30)) | ~p4(X0)))) & (((! [X31] : (p5(X31) | ~p104(X31) | ~r1(X0,X31)) | ~p5(X0)) & (p5(X0) | ! [X32] : (~r1(X0,X32) | ~p104(X32) | ~p5(X32)))) | ~p104(X0)) & (((~p6(X0) | ! [X33] : (~p105(X33) | p6(X33) | ~r1(X0,X33))) & (! [X34] : (~p105(X34) | ~p6(X34) | ~r1(X0,X34)) | p6(X0))) | ~p105(X0)) & (~p106(X0) | ((! [X35] : (~r1(X0,X35) | ~p7(X35) | ~p106(X35)) | p7(X0)) & (! [X36] : (~r1(X0,X36) | ~p106(X36) | p7(X36)) | ~p7(X0)))) & (((p8(X0) | ! [X37] : (~p8(X37) | ~p107(X37) | ~r1(X0,X37))) & (~p8(X0) | ! [X38] : (~r1(X0,X38) | ~p107(X38) | p8(X38)))) | ~p107(X0)) & (~p108(X0) | ((~p9(X0) | ! [X39] : (~p108(X39) | p9(X39) | ~r1(X0,X39))) & (! [X40] : (~r1(X0,X40) | ~p108(X40) | ~p9(X40)) | p9(X0)))) & (((p10(X0) | ! [X41] : (~p109(X41) | ~p10(X41) | ~r1(X0,X41))) & (~p10(X0) | ! [X42] : (~r1(X0,X42) | ~p109(X42) | p10(X42)))) | ~p109(X0)) & (~p110(X0) | ((! [X43] : (~r1(X0,X43) | p11(X43) | ~p110(X43)) | ~p11(X0)) & (p11(X0) | ! [X44] : (~p11(X44) | ~p110(X44) | ~r1(X0,X44))))) & (~p111(X0) | ((p12(X0) | ! [X45] : (~p12(X45) | ~p111(X45) | ~r1(X0,X45))) & (~p12(X0) | ! [X46] : (p12(X46) | ~p111(X46) | ~r1(X0,X46))))) & ((? [X47] : (~p6(X47) & p105(X47) & ~p106(X47) & r1(X0,X47)) & ? [X48] : (r1(X0,X48) & p6(X48) & p105(X48) & ~p106(X48))) | p105(X0) | ~p104(X0)) & ((? [X49] : (r1(X0,X49) & ~p8(X49) & ~p108(X49) & p107(X49)) & ? [X50] : (r1(X0,X50) & p8(X50) & ~p108(X50) & p107(X50))) | p107(X0) | ~p106(X0)) & (~p107(X0) | p108(X0) | (? [X51] : (r1(X0,X51) & ~p109(X51) & p108(X51) & p9(X51)) & ? [X52] : (p108(X52) & ~p109(X52) & ~p9(X52) & r1(X0,X52)))) & ((? [X53] : (p109(X53) & ~p110(X53) & ~p10(X53) & r1(X0,X53)) & ? [X54] : (p109(X54) & ~p110(X54) & p10(X54) & r1(X0,X54))) | p109(X0) | ~p108(X0)) & ((? [X55] : (p11(X55) & ~p111(X55) & p110(X55) & r1(X0,X55)) & ? [X56] : (r1(X0,X56) & ~p111(X56) & p110(X56) & ~p11(X56))) | p110(X0) | ~p109(X0)) & (~p110(X0) | p111(X0) | (? [X57] : (~p112(X57) & p111(X57) & p12(X57) & r1(X0,X57)) & ? [X58] : (~p112(X58) & p111(X58) & ~p12(X58) & r1(X0,X58)))) & (p113(X0) | ~p112(X0) | (? [X59] : (r1(X0,X59) & p113(X59) & ~p114(X59) & p14(X59)) & ? [X60] : (p113(X60) & ~p114(X60) & ~p14(X60) & r1(X0,X60)))) & ((? [X61] : (p115(X61) & ~p16(X61) & r1(X0,X61)) & ? [X62] : (r1(X0,X62) & p115(X62) & p16(X62))) | p115(X0) | ~p114(X0))))),
  inference(rectify,[],[f12])).
fof(f12,plain,(
  ! [X1] : (~sP0(X1) | (((? [X2] : (~p15(X2) & ~p115(X2) & p114(X2) & r1(X1,X2)) & ? [X3] : (p15(X3) & p114(X3) & ~p115(X3) & r1(X1,X3))) | ~p113(X1) | p114(X1)) & ((? [X4] : (p13(X4) & ~p113(X4) & p112(X4) & r1(X1,X4)) & ? [X5] : (~p13(X5) & ~p113(X5) & p112(X5) & r1(X1,X5))) | ~p111(X1) | p112(X1)) & (p106(X1) | ~p105(X1) | (? [X6] : (~p107(X6) & p106(X6) & p7(X6) & r1(X1,X6)) & ? [X7] : (r1(X1,X7) & ~p107(X7) & p106(X7) & ~p7(X7)))) & ((? [X8] : (~p105(X8) & p104(X8) & ~p5(X8) & r1(X1,X8)) & ? [X9] : (r1(X1,X9) & p104(X9) & ~p105(X9) & p5(X9))) | ~p103(X1) | p104(X1)) & (p103(X1) | ~p102(X1) | (? [X10] : (r1(X1,X10) & p4(X10) & ~p104(X10) & p103(X10)) & ? [X11] : (~p4(X11) & ~p104(X11) & p103(X11) & r1(X1,X11)))) & ((? [X12] : (~p3(X12) & ~p103(X12) & p102(X12) & r1(X1,X12)) & ? [X13] : (r1(X1,X13) & p102(X13) & ~p103(X13) & p3(X13))) | p102(X1) | ~p101(X1)) & ((? [X14] : (r1(X1,X14) & ~p2(X14) & p101(X14) & ~p102(X14)) & ? [X15] : (p2(X15) & p101(X15) & ~p102(X15) & r1(X1,X15))) | ~p100(X1) | p101(X1)) & (((! [X16] : (~p16(X16) | ~p115(X16) | ~r1(X1,X16)) | p16(X1)) & (! [X17] : (~p115(X17) | p16(X17) | ~r1(X1,X17)) | ~p16(X1))) | ~p115(X1)) & (~p114(X1) | ((p15(X1) | ! [X18] : (~r1(X1,X18) | ~p15(X18) | ~p114(X18))) & (~p15(X1) | ! [X19] : (~r1(X1,X19) | p15(X19) | ~p114(X19))))) & (~p113(X1) | ((p14(X1) | ! [X20] : (~p113(X20) | ~p14(X20) | ~r1(X1,X20))) & (~p14(X1) | ! [X21] : (~p113(X21) | p14(X21) | ~r1(X1,X21))))) & (((~p13(X1) | ! [X22] : (~r1(X1,X22) | p13(X22) | ~p112(X22))) & (p13(X1) | ! [X23] : (~p112(X23) | ~p13(X23) | ~r1(X1,X23)))) | ~p112(X1)) & (((! [X24] : (~r1(X1,X24) | ~p100(X24) | ~p1(X24)) | p1(X1)) & (~p1(X1) | ! [X25] : (~r1(X1,X25) | p1(X25) | ~p100(X25)))) | ~p100(X1)) & (p113(X1) | ~p114(X1)) & (p111(X1) | ~p112(X1)) & (p110(X1) | ~p111(X1)) & (p109(X1) | ~p110(X1)) & (p108(X1) | ~p109(X1)) & (~p108(X1) | p107(X1)) & (p106(X1) | ~p107(X1)) & (p104(X1) | ~p105(X1)) & (~p103(X1) | p102(X1)) & (p100(X1) | ~p101(X1)) & (p101(X1) | ~p102(X1)) & (p103(X1) | ~p104(X1)) & (p105(X1) | ~p106(X1)) & (~p113(X1) | p112(X1)) & (p114(X1) | ~p115(X1)) & (((~p2(X1) | ! [X26] : (~p101(X26) | p2(X26) | ~r1(X1,X26))) & (p2(X1) | ! [X27] : (~r1(X1,X27) | ~p2(X27) | ~p101(X27)))) | ~p101(X1)) & (((! [X28] : (p3(X28) | ~p102(X28) | ~r1(X1,X28)) | ~p3(X1)) & (! [X29] : (~p3(X29) | ~p102(X29) | ~r1(X1,X29)) | p3(X1))) | ~p102(X1)) & (~p103(X1) | ((p4(X1) | ! [X30] : (~p103(X30) | ~p4(X30) | ~r1(X1,X30))) & (! [X31] : (~r1(X1,X31) | p4(X31) | ~p103(X31)) | ~p4(X1)))) & (((! [X32] : (p5(X32) | ~p104(X32) | ~r1(X1,X32)) | ~p5(X1)) & (p5(X1) | ! [X33] : (~r1(X1,X33) | ~p104(X33) | ~p5(X33)))) | ~p104(X1)) & (((~p6(X1) | ! [X34] : (~p105(X34) | p6(X34) | ~r1(X1,X34))) & (! [X35] : (~p105(X35) | ~p6(X35) | ~r1(X1,X35)) | p6(X1))) | ~p105(X1)) & (~p106(X1) | ((! [X36] : (~r1(X1,X36) | ~p7(X36) | ~p106(X36)) | p7(X1)) & (! [X37] : (~r1(X1,X37) | ~p106(X37) | p7(X37)) | ~p7(X1)))) & (((p8(X1) | ! [X38] : (~p8(X38) | ~p107(X38) | ~r1(X1,X38))) & (~p8(X1) | ! [X39] : (~r1(X1,X39) | ~p107(X39) | p8(X39)))) | ~p107(X1)) & (~p108(X1) | ((~p9(X1) | ! [X40] : (~p108(X40) | p9(X40) | ~r1(X1,X40))) & (! [X41] : (~r1(X1,X41) | ~p108(X41) | ~p9(X41)) | p9(X1)))) & (((p10(X1) | ! [X42] : (~p109(X42) | ~p10(X42) | ~r1(X1,X42))) & (~p10(X1) | ! [X43] : (~r1(X1,X43) | ~p109(X43) | p10(X43)))) | ~p109(X1)) & (~p110(X1) | ((! [X44] : (~r1(X1,X44) | p11(X44) | ~p110(X44)) | ~p11(X1)) & (p11(X1) | ! [X45] : (~p11(X45) | ~p110(X45) | ~r1(X1,X45))))) & (~p111(X1) | ((p12(X1) | ! [X46] : (~p12(X46) | ~p111(X46) | ~r1(X1,X46))) & (~p12(X1) | ! [X47] : (p12(X47) | ~p111(X47) | ~r1(X1,X47))))) & ((? [X48] : (~p6(X48) & p105(X48) & ~p106(X48) & r1(X1,X48)) & ? [X49] : (r1(X1,X49) & p6(X49) & p105(X49) & ~p106(X49))) | p105(X1) | ~p104(X1)) & ((? [X50] : (r1(X1,X50) & ~p8(X50) & ~p108(X50) & p107(X50)) & ? [X51] : (r1(X1,X51) & p8(X51) & ~p108(X51) & p107(X51))) | p107(X1) | ~p106(X1)) & (~p107(X1) | p108(X1) | (? [X52] : (r1(X1,X52) & ~p109(X52) & p108(X52) & p9(X52)) & ? [X53] : (p108(X53) & ~p109(X53) & ~p9(X53) & r1(X1,X53)))) & ((? [X54] : (p109(X54) & ~p110(X54) & ~p10(X54) & r1(X1,X54)) & ? [X55] : (p109(X55) & ~p110(X55) & p10(X55) & r1(X1,X55))) | p109(X1) | ~p108(X1)) & ((? [X56] : (p11(X56) & ~p111(X56) & p110(X56) & r1(X1,X56)) & ? [X57] : (r1(X1,X57) & ~p111(X57) & p110(X57) & ~p11(X57))) | p110(X1) | ~p109(X1)) & (~p110(X1) | p111(X1) | (? [X58] : (~p112(X58) & p111(X58) & p12(X58) & r1(X1,X58)) & ? [X59] : (~p112(X59) & p111(X59) & ~p12(X59) & r1(X1,X59)))) & (p113(X1) | ~p112(X1) | (? [X60] : (r1(X1,X60) & p113(X60) & ~p114(X60) & p14(X60)) & ? [X61] : (p113(X61) & ~p114(X61) & ~p14(X61) & r1(X1,X61)))) & ((? [X62] : (p115(X62) & ~p16(X62) & r1(X1,X62)) & ? [X63] : (r1(X1,X63) & p115(X63) & p16(X63))) | p115(X1) | ~p114(X1))))),
  inference(nnf_transformation,[],[f10])).
fof(f6542,plain,(
  ~p101(sK12(sK30)) | ~p100(sK30) | p101(sK30) | ~sP0(sK30)),
  inference(subsumption_resolution,[],[f6516,f68])).
fof(f68,plain,(
  ( ! [X0] : (~p102(sK12(X0)) | ~p100(X0) | p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6516,plain,(
  p102(sK12(sK30)) | ~p101(sK12(sK30)) | ~p100(sK30) | p101(sK30) | ~sP0(sK30)),
  inference(resolution,[],[f6408,f65])).
fof(f65,plain,(
  ( ! [X0] : (r1(X0,sK12(X0)) | ~p100(X0) | p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6408,plain,(
  ( ! [X10] : (~r1(sK30,X10) | p102(X10) | ~p101(X10)) )),
  inference(subsumption_resolution,[],[f6407,f182])).
fof(f6407,plain,(
  ( ! [X10] : (~p101(X10) | ~sP0(X10) | p102(X10) | ~r1(sK30,X10)) )),
  inference(subsumption_resolution,[],[f6406,f58])).
fof(f58,plain,(
  ( ! [X0] : (~p103(sK10(X0)) | p102(X0) | ~p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6406,plain,(
  ( ! [X10] : (p103(sK10(X10)) | ~p101(X10) | ~sP0(X10) | p102(X10) | ~r1(sK30,X10)) )),
  inference(subsumption_resolution,[],[f6376,f59])).
fof(f59,plain,(
  ( ! [X0] : (p102(sK10(X0)) | p102(X0) | ~p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6376,plain,(
  ( ! [X10] : (~p102(sK10(X10)) | p103(sK10(X10)) | ~p101(X10) | ~sP0(X10) | p102(X10) | ~r1(sK30,X10)) )),
  inference(resolution,[],[f6334,f447])).
fof(f447,plain,(
  ( ! [X0,X1] : (r1(X1,sK10(X0)) | ~p101(X0) | ~sP0(X0) | p102(X0) | ~r1(X1,X0)) )),
  inference(resolution,[],[f60,f187])).
fof(f187,plain,(
  ( ! [X2,X0,X1] : (~r1(X1,X2) | r1(X0,X2) | ~r1(X0,X1)) )),
  inference(cnf_transformation,[],[f9])).
fof(f9,plain,(
  ! [X0,X1,X2] : (~r1(X0,X1) | ~r1(X1,X2) | r1(X0,X2))),
  inference(flattening,[],[f8])).
fof(f8,plain,(
  ! [X0,X1,X2] : ((~r1(X0,X1) | ~r1(X1,X2)) | r1(X0,X2))),
  inference(ennf_transformation,[],[f1])).
fof(f1,axiom,(
  ! [X0,X1,X2] : ((r1(X0,X1) & r1(X1,X2)) => r1(X0,X2))),
  file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p',transitivity)).
fof(f60,plain,(
  ( ! [X0] : (r1(X0,sK10(X0)) | p102(X0) | ~p101(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6334,plain,(
  ( ! [X8] : (~r1(sK30,X8) | ~p102(X8) | p103(X8)) )),
  inference(subsumption_resolution,[],[f6333,f182])).
fof(f6333,plain,(
  ( ! [X8] : (p103(X8) | ~sP0(X8) | ~p102(X8) | ~r1(sK30,X8)) )),
  inference(subsumption_resolution,[],[f6332,f51])).
fof(f51,plain,(
  ( ! [X0] : (~p104(sK8(X0)) | ~p102(X0) | p103(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6332,plain,(
  ( ! [X8] : (p104(sK8(X8)) | p103(X8) | ~sP0(X8) | ~p102(X8) | ~r1(sK30,X8)) )),
  inference(subsumption_resolution,[],[f6300,f52])).
fof(f52,plain,(
  ( ! [X0] : (p103(sK8(X0)) | ~p102(X0) | p103(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6300,plain,(
  ( ! [X8] : (~p103(sK8(X8)) | p104(sK8(X8)) | p103(X8) | ~sP0(X8) | ~p102(X8) | ~r1(sK30,X8)) )),
  inference(resolution,[],[f6265,f429])).
fof(f429,plain,(
  ( ! [X0,X1] : (r1(X1,sK8(X0)) | p103(X0) | ~sP0(X0) | ~p102(X0) | ~r1(X1,X0)) )),
  inference(resolution,[],[f49,f187])).
fof(f49,plain,(
  ( ! [X0] : (r1(X0,sK8(X0)) | ~p102(X0) | p103(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6265,plain,(
  ( ! [X6] : (~r1(sK30,X6) | ~p103(X6) | p104(X6)) )),
  inference(subsumption_resolution,[],[f6264,f182])).
fof(f6264,plain,(
  ( ! [X6] : (p104(X6) | ~sP0(X6) | ~p103(X6) | ~r1(sK30,X6)) )),
  inference(subsumption_resolution,[],[f6263,f42])).
fof(f42,plain,(
  ( ! [X0] : (p104(sK6(X0)) | ~p103(X0) | p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6263,plain,(
  ( ! [X6] : (~p104(sK6(X6)) | p104(X6) | ~sP0(X6) | ~p103(X6) | ~r1(sK30,X6)) )),
  inference(subsumption_resolution,[],[f6224,f41])).
fof(f41,plain,(
  ( ! [X0] : (~p105(sK6(X0)) | ~p103(X0) | p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6224,plain,(
  ( ! [X6] : (p105(sK6(X6)) | ~p104(sK6(X6)) | p104(X6) | ~sP0(X6) | ~p103(X6) | ~r1(sK30,X6)) )),
  inference(resolution,[],[f6192,f358])).
fof(f358,plain,(
  ( ! [X0,X1] : (r1(X1,sK6(X0)) | p104(X0) | ~sP0(X0) | ~p103(X0) | ~r1(X1,X0)) )),
  inference(resolution,[],[f44,f187])).
fof(f44,plain,(
  ( ! [X0] : (r1(X0,sK6(X0)) | ~p103(X0) | p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6192,plain,(
  ( ! [X11] : (~r1(sK30,X11) | p105(X11) | ~p104(X11)) )),
  inference(subsumption_resolution,[],[f6191,f182])).
fof(f6191,plain,(
  ( ! [X11] : (~p104(X11) | ~sP0(X11) | p105(X11) | ~r1(sK30,X11)) )),
  inference(subsumption_resolution,[],[f6190,f122])).
fof(f122,plain,(
  ( ! [X0] : (~p106(sK14(X0)) | p105(X0) | ~p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6190,plain,(
  ( ! [X11] : (~p104(X11) | ~sP0(X11) | p105(X11) | ~r1(sK30,X11) | p106(sK14(X11))) )),
  inference(subsumption_resolution,[],[f6128,f121])).
fof(f121,plain,(
  ( ! [X0] : (p105(sK14(X0)) | p105(X0) | ~p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f6128,plain,(
  ( ! [X11] : (~p104(X11) | ~sP0(X11) | p105(X11) | ~r1(sK30,X11) | ~p105(sK14(X11)) | p106(sK14(X11))) )),
  inference(resolution,[],[f521,f4296])).
fof(f4296,plain,(
  ( ! [X1] : (~r1(sK30,X1) | ~p105(X1) | p106(X1)) )),
  inference(subsumption_resolution,[],[f4295,f182])).
fof(f4295,plain,(
  ( ! [X1] : (p106(X1) | ~sP0(X1) | ~p105(X1) | ~r1(sK30,X1)) )),
  inference(subsumption_resolution,[],[f4251,f40])).
fof(f40,plain,(
  ( ! [X0] : (~p7(sK5(X0)) | ~p105(X0) | p106(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f4251,plain,(
  ( ! [X1] : (p106(X1) | ~sP0(X1) | ~p105(X1) | ~r1(sK30,X1) | p7(sK5(X1))) )),
  inference(resolution,[],[f351,f185])).
fof(f185,plain,(
  ( ! [X2] : (~r1(sK30,X2) | p7(X2)) )),
  inference(cnf_transformation,[],[f16])).
fof(f351,plain,(
  ( ! [X0,X1] : (r1(X1,sK5(X0)) | p106(X0) | ~sP0(X0) | ~p105(X0) | ~r1(X1,X0)) )),
  inference(resolution,[],[f37,f187])).
fof(f37,plain,(
  ( ! [X0] : (r1(X0,sK5(X0)) | ~p105(X0) | p106(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
fof(f521,plain,(
  ( ! [X0,X1] : (r1(X1,sK14(X0)) | ~p104(X0) | ~sP0(X0) | p105(X0) | ~r1(X1,X0)) )),
  inference(resolution,[],[f123,f187])).
fof(f123,plain,(
  ( ! [X0] : (r1(X0,sK14(X0)) | p105(X0) | ~p104(X0) | ~sP0(X0)) )),
  inference(cnf_transformation,[],[f14])).
% SZS output end Proof for FNE056
------------------------------
Version: Vampire 1.0 (revision 700)
Termination reason: Refutation

Active clauses: 901
Passive clauses: 3355
Generated clauses: 6530
Final active clauses: 901
Final passive clauses: 2383
Input formulas: 3
Initial clauses: 171

Pure predicates: 1

Duplicate literals: 1316
Fw subsumption resolutions: 1103

Simple tautologies: 93
Forward subsumptions: 904

Binary resolution: 4132

Unique components: 4

Memory used: 2814KB
Time elapsed: 0.075 s
------------------------------
% Success in time 0.1 s

WATCH: 0.07 CPU 0.12 WC

FINAL WATCH: 0.07 CPU 0.12 WC