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 FNE056 WATCH: 0.00 CPU 0.01 WC WATCH: 2.99 CPU 3.02 WC WATCH: 6.01 CPU 6.03 WC WATCH: 9.02 CPU 9.04 WC WATCH: 12.03 CPU 12.05 WC WATCH: 15.04 CPU 15.06 WC WATCH: 18.05 CPU 18.07 WC Time limit reached! ------------------------------ Version: Vampire 1.8 (revision 1280) Termination reason: Time limit Active clauses: 9148 Passive clauses: 138450 Generated clauses: 360383 Final active clauses: 9135 Final passive clauses: 111736 Input formulas: 3 Initial clauses: 205 Duplicate literals: 24558 Fw subsumption resolutions: 6850 Bw subsumption resolutions: 13 Global subsumptions: 800 Simple tautologies: 943 Forward subsumptions: 224827 Binary resolution: 32674 Unit resulting resolution: 312967 Factoring: 3954 SAT solver clauses: 149881 SAT solver unit clauses: 127981 SAT solver binary clauses: 1220 SAT solver learnt clauses: 800 SAT solver learnt literals: 2650 Memory used [KB]: 118846 Time elapsed: 18.622 s ------------------------------ % remaining time: 2813 next slice time: 20 dis+1011_128_bsr=on:bms=on:cond=on:fsr=off:lcm=reverse:nwc=4:nicw=on:sswn=on:sswsr=on:sac=on:sio=off:sp=occurrence:updr=off_18 on FNE056 Time limit reached! ------------------------------ Version: Vampire 1.8 (revision 1280) Termination reason: Time limit Active clauses: 19169 Passive clauses: 40252 Generated clauses: 43203 Final active clauses: 15179 Final passive clauses: 5820 Input formulas: 3 Initial clauses: 205 Reactivated clauses: 6857 Duplicate literals: 278 Bw subsumption resolutions: 2004 Condensations: 4 Simple tautologies: 39 Forward subsumptions: 1209 Backward subsumptions: 6834 Subsumed by BDD marking: 205 Binary resolution: 28029 Split clauses: 8437 Split components: 21373 Unique components: 15279 Introduced splitting names: 6646 BDD propositional clauses: 1386 SAT solver clauses: 15102 SAT solver unit clauses: 20 SAT solver binary clauses: 159 SAT solver learnt clauses: 23 SAT solver learnt literals: 86 Memory used by BDDs [KB]: 1151 Memory used [KB]: 43624 Time elapsed: 2.102 s ------------------------------ % remaining time: 2792 next slice time: 6 dis+4_128_bs=off:cond=fast:gs=on:lcm=predicate:nwc=5:ptb=off:ssec=off:sos=on:sac=on:sgo=on:sio=off:spo=on:swb=on:sp=occurrence:updr=off_4 on FNE056 WATCH: 21.02 CPU 21.08 WC Time limit reached! ------------------------------ Version: Vampire 1.8 (revision 1280) Termination reason: Time limit Active clauses: 3179 Passive clauses: 8192 Generated clauses: 12355 Final active clauses: 3179 Final passive clauses: 3608 Input formulas: 3 Initial clauses: 205 Duplicate literals: 1011 Fw subsumption resolutions: 1440 Condensations: 9 Global subsumptions: 620 Simple tautologies: 31 Forward subsumptions: 2468 Binary resolution: 8880 Split clauses: 210 Split components: 420 Introduced splitting names: 202 SAT solver clauses: 13240 SAT solver unit clauses: 1442 SAT solver binary clauses: 2575 SAT solver learnt clauses: 620 SAT solver learnt literals: 946 Memory used [KB]: 10106 Time elapsed: 0.721 s ------------------------------ % remaining time: 2784 next slice time: 6 dis+10_128_bs=off:cond=fast:gsp=input_only:gs=on:lcm=predicate:nwc=1.1:ptb=off:ssec=off:spo=on:swb=on:sp=reverse_arity:urr=on_4 on FNE056 Refutation found. Thanks to Tanya! % SZS status Theorem for FNE056 % SZS output start Proof for FNE056 35169_1. $false (24:0) [global subsumption 35136,34720] 34720. r1(sK14(sK22(sK20(sK18(sK16(sK30))))),sK25(sK14(sK22(sK20(sK18(sK16(sK30))))))) (22:14) [unit resulting resolution 5162,5163,34613,302] 302. ~sP2(X0) | ~p105(X0) | p106(X0) | r1(X0,sK25(X0)) (0:10) [cnf transformation 117] 117. ! [X0] : (~sP2(X0) | p106(X0) | ~p105(X0) | ((~p107(sK24(X0)) & p106(sK24(X0)) & p7(sK24(X0)) & r1(X0,sK24(X0))) & (r1(X0,sK25(X0)) & ~p107(sK25(X0)) & p106(sK25(X0)) & ~p7(sK25(X0)))))[skolemisation 116] 116. ! [X0] : (~sP2(X0) | p106(X0) | ~p105(X0) | (? [X1] : (~p107(X1) & p106(X1) & p7(X1) & r1(X0,X1)) & ? [X2] : (r1(X0,X2) & ~p107(X2) & p106(X2) & ~p7(X2))))[rectify 115] 115. ! [X1] : (~sP2(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))))[nnf transformation 14] 14. ! [X1] : (~sP2(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))))[predicate definition introduction] 34613. sP2(sK14(sK22(sK20(sK18(sK16(sK30)))))) (21:7) [unit resulting resolution 34555,128] 128. ~sP31(X0) | sP2(X0) (0:4) [cnf transformation 46] 46. ! [X0] : (~sP31(X0) | (sP0(X0) & sP1(X0) & sP2(X0) & sP3(X0) & sP4(X0) & sP5(X0) & sP6(X0) & sP15(X0) & sP16(X0) & sP17(X0) & sP18(X0) & sP19(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)) & sP20(X0) & sP21(X0) & sP22(X0) & sP23(X0) & sP24(X0) & sP25(X0) & sP26(X0) & sP27(X0) & sP28(X0) & sP29(X0) & sP30(X0) & sP7(X0) & sP8(X0) & sP9(X0) & sP10(X0) & sP11(X0) & sP12(X0) & sP13(X0) & sP14(X0)))[rectify 45] 45. ! [X1] : (~sP31(X1) | (sP0(X1) & sP1(X1) & sP2(X1) & sP3(X1) & sP4(X1) & sP5(X1) & sP6(X1) & sP15(X1) & sP16(X1) & sP17(X1) & sP18(X1) & sP19(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)) & sP20(X1) & sP21(X1) & sP22(X1) & sP23(X1) & sP24(X1) & sP25(X1) & sP26(X1) & sP27(X1) & sP28(X1) & sP29(X1) & sP30(X1) & sP7(X1) & sP8(X1) & sP9(X1) & sP10(X1) & sP11(X1) & sP12(X1) & sP13(X1) & sP14(X1)))[nnf transformation 43] 43. ! [X1] : (~sP31(X1) | (sP0(X1) & sP1(X1) & sP2(X1) & sP3(X1) & sP4(X1) & sP5(X1) & sP6(X1) & sP15(X1) & sP16(X1) & sP17(X1) & sP18(X1) & sP19(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)) & sP20(X1) & sP21(X1) & sP22(X1) & sP23(X1) & sP24(X1) & sP25(X1) & sP26(X1) & sP27(X1) & sP28(X1) & sP29(X1) & sP30(X1) & sP7(X1) & sP8(X1) & sP9(X1) & sP10(X1) & sP11(X1) & sP12(X1) & sP13(X1) & sP14(X1)))[predicate definition introduction] 34555. sP31(sK14(sK22(sK20(sK18(sK16(sK30)))))) (20:7) [unit resulting resolution 34456,322] 322. ~r1(sK30,X1) | sP31(X1) (0:5) [cnf transformation 125] 125. ! [X1] : (~r1(sK30,X1) | sP31(X1)) & p100(sK30) & ~p101(sK30) & ! [X2] : (~r1(sK30,X2) | p7(X2))[skolemisation 124] 124. ? [X0] : (! [X1] : (~r1(X0,X1) | sP31(X1)) & p100(X0) & ~p101(X0) & ! [X2] : (~r1(X0,X2) | p7(X2)))[rectify 44] 44. ? [X0] : (! [X1] : (~r1(X0,X1) | sP31(X1)) & p100(X0) & ~p101(X0) & ! [X64] : (~r1(X0,X64) | p7(X64)))[definition folding 9,43,42,41,40,39,38,37,36,35,34,33,32,31,30,29,28,27,26,25,24,23,22,21,20,19,18,17,16,15,14,13,12] 12. ! [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))[predicate definition introduction] 13. ! [X1] : (~sP1(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))[predicate definition introduction] 15. ! [X1] : (~sP3(X1) | (? [X8] : (~p105(X8) & p104(X8) & ~p5(X8) & r1(X1,X8)) & ? [X9] : (r1(X1,X9) & p104(X9) & ~p105(X9) & p5(X9))) | ~p103(X1) | p104(X1))[predicate definition introduction] 16. ! [X1] : (~sP4(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))))[predicate definition introduction] 17. ! [X1] : (~sP5(X1) | (? [X12] : (~p3(X12) & ~p103(X12) & p102(X12) & r1(X1,X12)) & ? [X13] : (r1(X1,X13) & p102(X13) & ~p103(X13) & p3(X13))) | p102(X1) | ~p101(X1))[predicate definition introduction] 18. ! [X1] : (~sP6(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))[predicate definition introduction] 19. ! [X1] : (~sP7(X1) | (? [X48] : (~p6(X48) & p105(X48) & ~p106(X48) & r1(X1,X48)) & ? [X49] : (r1(X1,X49) & p6(X49) & p105(X49) & ~p106(X49))) | p105(X1) | ~p104(X1))[predicate definition introduction] 20. ! [X1] : (~sP8(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))[predicate definition introduction] 21. ! [X1] : (~sP9(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))))[predicate definition introduction] 22. ! [X1] : (~sP10(X1) | (? [X54] : (p109(X54) & ~p110(X54) & ~p10(X54) & r1(X1,X54)) & ? [X55] : (p109(X55) & ~p110(X55) & p10(X55) & r1(X1,X55))) | p109(X1) | ~p108(X1))[predicate definition introduction] 23. ! [X1] : (~sP11(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))[predicate definition introduction] 24. ! [X1] : (~sP12(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))))[predicate definition introduction] 25. ! [X1] : (~sP13(X1) | p113(X1) | ~p112(X1) | (? [X60] : (r1(X1,X60) & p113(X60) & ~p114(X60) & p14(X60)) & ? [X61] : (p113(X61) & ~p114(X61) & ~p14(X61) & r1(X1,X61))))[predicate definition introduction] 26. ! [X1] : (~sP14(X1) | (? [X62] : (p115(X62) & ~p16(X62) & r1(X1,X62)) & ? [X63] : (r1(X1,X63) & p115(X63) & p16(X63))) | p115(X1) | ~p114(X1))[predicate definition introduction] 27. ! [X1] : (~sP15(X1) | ((! [X16] : (~p16(X16) | ~p115(X16) | ~r1(X1,X16)) | p16(X1)) & (! [X17] : (~p115(X17) | p16(X17) | ~r1(X1,X17)) | ~p16(X1))) | ~p115(X1))[predicate definition introduction] 28. ! [X1] : (~sP16(X1) | ~p114(X1) | ((p15(X1) | ! [X18] : (~r1(X1,X18) | ~p15(X18) | ~p114(X18))) & (~p15(X1) | ! [X19] : (~r1(X1,X19) | p15(X19) | ~p114(X19)))))[predicate definition introduction] 29. ! [X1] : (~sP17(X1) | ~p113(X1) | ((p14(X1) | ! [X20] : (~p113(X20) | ~p14(X20) | ~r1(X1,X20))) & (~p14(X1) | ! [X21] : (~p113(X21) | p14(X21) | ~r1(X1,X21)))))[predicate definition introduction] 30. ! [X1] : (~sP18(X1) | ((~p13(X1) | ! [X22] : (~r1(X1,X22) | p13(X22) | ~p112(X22))) & (p13(X1) | ! [X23] : (~p112(X23) | ~p13(X23) | ~r1(X1,X23)))) | ~p112(X1))[predicate definition introduction] 31. ! [X1] : (~sP19(X1) | ((! [X24] : (~r1(X1,X24) | ~p100(X24) | ~p1(X24)) | p1(X1)) & (~p1(X1) | ! [X25] : (~r1(X1,X25) | p1(X25) | ~p100(X25)))) | ~p100(X1))[predicate definition introduction] 32. ! [X1] : (~sP20(X1) | ((~p2(X1) | ! [X26] : (~p101(X26) | p2(X26) | ~r1(X1,X26))) & (p2(X1) | ! [X27] : (~r1(X1,X27) | ~p2(X27) | ~p101(X27)))) | ~p101(X1))[predicate definition introduction] 33. ! [X1] : (~sP21(X1) | ((! [X28] : (p3(X28) | ~p102(X28) | ~r1(X1,X28)) | ~p3(X1)) & (! [X29] : (~p3(X29) | ~p102(X29) | ~r1(X1,X29)) | p3(X1))) | ~p102(X1))[predicate definition introduction] 34. ! [X1] : (~sP22(X1) | ~p103(X1) | ((p4(X1) | ! [X30] : (~p103(X30) | ~p4(X30) | ~r1(X1,X30))) & (! [X31] : (~r1(X1,X31) | p4(X31) | ~p103(X31)) | ~p4(X1))))[predicate definition introduction] 35. ! [X1] : (~sP23(X1) | ((! [X32] : (p5(X32) | ~p104(X32) | ~r1(X1,X32)) | ~p5(X1)) & (p5(X1) | ! [X33] : (~r1(X1,X33) | ~p104(X33) | ~p5(X33)))) | ~p104(X1))[predicate definition introduction] 36. ! [X1] : (~sP24(X1) | ((~p6(X1) | ! [X34] : (~p105(X34) | p6(X34) | ~r1(X1,X34))) & (! [X35] : (~p105(X35) | ~p6(X35) | ~r1(X1,X35)) | p6(X1))) | ~p105(X1))[predicate definition introduction] 37. ! [X1] : (~sP25(X1) | ~p106(X1) | ((! [X36] : (~r1(X1,X36) | ~p7(X36) | ~p106(X36)) | p7(X1)) & (! [X37] : (~r1(X1,X37) | ~p106(X37) | p7(X37)) | ~p7(X1))))[predicate definition introduction] 38. ! [X1] : (~sP26(X1) | ((p8(X1) | ! [X38] : (~p8(X38) | ~p107(X38) | ~r1(X1,X38))) & (~p8(X1) | ! [X39] : (~r1(X1,X39) | ~p107(X39) | p8(X39)))) | ~p107(X1))[predicate definition introduction] 39. ! [X1] : (~sP27(X1) | ~p108(X1) | ((~p9(X1) | ! [X40] : (~p108(X40) | p9(X40) | ~r1(X1,X40))) & (! [X41] : (~r1(X1,X41) | ~p108(X41) | ~p9(X41)) | p9(X1))))[predicate definition introduction] 40. ! [X1] : (~sP28(X1) | ((p10(X1) | ! [X42] : (~p109(X42) | ~p10(X42) | ~r1(X1,X42))) & (~p10(X1) | ! [X43] : (~r1(X1,X43) | ~p109(X43) | p10(X43)))) | ~p109(X1))[predicate definition introduction] 41. ! [X1] : (~sP29(X1) | ~p110(X1) | ((! [X44] : (~r1(X1,X44) | p11(X44) | ~p110(X44)) | ~p11(X1)) & (p11(X1) | ! [X45] : (~p11(X45) | ~p110(X45) | ~r1(X1,X45)))))[predicate definition introduction] 42. ! [X1] : (~sP30(X1) | ~p111(X1) | ((p12(X1) | ! [X46] : (~p12(X46) | ~p111(X46) | ~r1(X1,X46))) & (~p12(X1) | ! [X47] : (p12(X47) | ~p111(X47) | ~r1(X1,X47)))))[predicate definition introduction] 9. ? [X0] : (! [X1] : (~r1(X0,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)))) & p100(X0) & ~p101(X0) & ! [X64] : (~r1(X0,X64) | p7(X64)))[flattening 8] 8. ? [X0] : ((! [X1] : (~r1(X0,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))))) & p100(X0) & ~p101(X0)) & ! [X64] : (~r1(X0,X64) | p7(X64)))[ennf transformation 7] 7. ? [X0] : ~(~(! [X1] : (~r1(X0,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))))) & p100(X0) & ~p101(X0)) | ~! [X64] : (~r1(X0,X64) | p7(X64)))[pure predicate removal 6] 6. ? [X0] : ~(~(! [X1] : (~r1(X0,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)) & (p115(X1) | ~p116(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] : (~(~p116(X62) & p115(X62) & ~p16(X62)) | ~r1(X1,X62)) & ~! [X63] : (~r1(X1,X63) | ~(~p116(X63) & p115(X63) & p16(X63)))) | ~(~p115(X1) & p114(X1))))) & p100(X0) & ~p101(X0)) | ~! [X64] : (~r1(X0,X64) | p7(X64)))[flattening 5] 5. ~~? [X0] : ~(~(! [X1] : (~r1(X0,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)) & (p115(X1) | ~p116(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] : (~(~p116(X62) & p115(X62) & ~p16(X62)) | ~r1(X1,X62)) & ~! [X63] : (~r1(X1,X63) | ~(~p116(X63) & p115(X63) & p16(X63)))) | ~(~p115(X1) & p114(X1))))) & p100(X0) & ~p101(X0)) | ~! [X64] : (~r1(X0,X64) | p7(X64)))[rectify 3] 3. ~~? [X0] : ~(~(! [X1] : (~r1(X0,X1) | (((~! [X0] : (~(~p15(X0) & ~p115(X0) & p114(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(p15(X0) & p114(X0) & ~p115(X0)) | ~r1(X1,X0))) | ~(p113(X1) & ~p114(X1))) & ((~! [X0] : (~(p13(X0) & ~p113(X0) & p112(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(~p13(X0) & ~p113(X0) & p112(X0)) | ~r1(X1,X0))) | ~(p111(X1) & ~p112(X1))) & (~(~p106(X1) & p105(X1)) | (~! [X0] : (~(~p107(X0) & p106(X0) & p7(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p107(X0) & p106(X0) & ~p7(X0))))) & ((~! [X0] : (~(~p105(X0) & p104(X0) & ~p5(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p104(X0) & ~p105(X0) & p5(X0)))) | ~(p103(X1) & ~p104(X1))) & (~(~p103(X1) & p102(X1)) | (~! [X0] : (~r1(X1,X0) | ~(p4(X0) & ~p104(X0) & p103(X0))) & ~! [X0] : (~(~p4(X0) & ~p104(X0) & p103(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(~p3(X0) & ~p103(X0) & p102(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p102(X0) & ~p103(X0) & p3(X0)))) | ~(~p102(X1) & p101(X1))) & ((~! [X0] : (~r1(X1,X0) | ~(~p2(X0) & p101(X0) & ~p102(X0))) & ~! [X0] : (~(p2(X0) & p101(X0) & ~p102(X0)) | ~r1(X1,X0))) | ~(p100(X1) & ~p101(X1))) & (((! [X0] : (~p16(X0) | ~p115(X0) | ~r1(X1,X0)) | p16(X1)) & (! [X0] : (~p115(X0) | p16(X0) | ~r1(X1,X0)) | ~p16(X1))) | ~p115(X1)) & (~p114(X1) | ((p15(X1) | ! [X0] : (~r1(X1,X0) | ~p15(X0) | ~p114(X0))) & (~p15(X1) | ! [X0] : (~r1(X1,X0) | p15(X0) | ~p114(X0))))) & (~p113(X1) | ((p14(X1) | ! [X0] : (~p113(X0) | ~p14(X0) | ~r1(X1,X0))) & (~p14(X1) | ! [X0] : (~p113(X0) | p14(X0) | ~r1(X1,X0))))) & (((~p13(X1) | ! [X0] : (~r1(X1,X0) | p13(X0) | ~p112(X0))) & (p13(X1) | ! [X0] : (~p112(X0) | ~p13(X0) | ~r1(X1,X0)))) | ~p112(X1)) & (((! [X0] : (~r1(X1,X0) | ~p100(X0) | ~p1(X0)) | p1(X1)) & (~p1(X1) | ! [X0] : (~r1(X1,X0) | p1(X0) | ~p100(X0)))) | ~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)) & (p115(X1) | ~p116(X1)) & (((~p2(X1) | ! [X0] : (~p101(X0) | p2(X0) | ~r1(X1,X0))) & (p2(X1) | ! [X0] : (~r1(X1,X0) | ~p2(X0) | ~p101(X0)))) | ~p101(X1)) & (((! [X0] : (p3(X0) | ~p102(X0) | ~r1(X1,X0)) | ~p3(X1)) & (! [X0] : (~p3(X0) | ~p102(X0) | ~r1(X1,X0)) | p3(X1))) | ~p102(X1)) & (~p103(X1) | ((p4(X1) | ! [X0] : (~p103(X0) | ~p4(X0) | ~r1(X1,X0))) & (! [X0] : (~r1(X1,X0) | p4(X0) | ~p103(X0)) | ~p4(X1)))) & (((! [X0] : (p5(X0) | ~p104(X0) | ~r1(X1,X0)) | ~p5(X1)) & (p5(X1) | ! [X0] : (~r1(X1,X0) | ~p104(X0) | ~p5(X0)))) | ~p104(X1)) & (((~p6(X1) | ! [X0] : (~p105(X0) | p6(X0) | ~r1(X1,X0))) & (! [X0] : (~p105(X0) | ~p6(X0) | ~r1(X1,X0)) | p6(X1))) | ~p105(X1)) & (~p106(X1) | ((! [X0] : (~r1(X1,X0) | ~p7(X0) | ~p106(X0)) | p7(X1)) & (! [X0] : (~r1(X1,X0) | ~p106(X0) | p7(X0)) | ~p7(X1)))) & (((p8(X1) | ! [X0] : (~p8(X0) | ~p107(X0) | ~r1(X1,X0))) & (~p8(X1) | ! [X0] : (~r1(X1,X0) | ~p107(X0) | p8(X0)))) | ~p107(X1)) & (~p108(X1) | ((~p9(X1) | ! [X0] : (~p108(X0) | p9(X0) | ~r1(X1,X0))) & (! [X0] : (~r1(X1,X0) | ~p108(X0) | ~p9(X0)) | p9(X1)))) & (((p10(X1) | ! [X0] : (~p109(X0) | ~p10(X0) | ~r1(X1,X0))) & (~p10(X1) | ! [X0] : (~r1(X1,X0) | ~p109(X0) | p10(X0)))) | ~p109(X1)) & (~p110(X1) | ((! [X0] : (~r1(X1,X0) | p11(X0) | ~p110(X0)) | ~p11(X1)) & (p11(X1) | ! [X0] : (~p11(X0) | ~p110(X0) | ~r1(X1,X0))))) & (~p111(X1) | ((p12(X1) | ! [X0] : (~p12(X0) | ~p111(X0) | ~r1(X1,X0))) & (~p12(X1) | ! [X0] : (p12(X0) | ~p111(X0) | ~r1(X1,X0))))) & ((~! [X0] : (~(~p6(X0) & p105(X0) & ~p106(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p6(X0) & p105(X0) & ~p106(X0)))) | ~(~p105(X1) & p104(X1))) & ((~! [X0] : (~r1(X1,X0) | ~(~p8(X0) & ~p108(X0) & p107(X0))) & ~! [X0] : (~r1(X1,X0) | ~(p8(X0) & ~p108(X0) & p107(X0)))) | ~(~p107(X1) & p106(X1))) & (~(p107(X1) & ~p108(X1)) | (~! [X0] : (~r1(X1,X0) | ~(~p109(X0) & p108(X0) & p9(X0))) & ~! [X0] : (~(p108(X0) & ~p109(X0) & ~p9(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(p109(X0) & ~p110(X0) & ~p10(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(p109(X0) & ~p110(X0) & p10(X0)) | ~r1(X1,X0))) | ~(~p109(X1) & p108(X1))) & ((~! [X0] : (~(p11(X0) & ~p111(X0) & p110(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p111(X0) & p110(X0) & ~p11(X0)))) | ~(~p110(X1) & p109(X1))) & (~(p110(X1) & ~p111(X1)) | (~! [X0] : (~(~p112(X0) & p111(X0) & p12(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(~p112(X0) & p111(X0) & ~p12(X0)) | ~r1(X1,X0)))) & (~(~p113(X1) & p112(X1)) | (~! [X0] : (~r1(X1,X0) | ~(p113(X0) & ~p114(X0) & p14(X0))) & ~! [X0] : (~(p113(X0) & ~p114(X0) & ~p14(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(~p116(X0) & p115(X0) & ~p16(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p116(X0) & p115(X0) & p16(X0)))) | ~(~p115(X1) & p114(X1))))) & p100(X0) & ~p101(X0)) | ~! [X1] : (~r1(X0,X1) | p7(X1)))[negated conjecture 2] 2. ~? [X0] : ~(~(! [X1] : (~r1(X0,X1) | (((~! [X0] : (~(~p15(X0) & ~p115(X0) & p114(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(p15(X0) & p114(X0) & ~p115(X0)) | ~r1(X1,X0))) | ~(p113(X1) & ~p114(X1))) & ((~! [X0] : (~(p13(X0) & ~p113(X0) & p112(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(~p13(X0) & ~p113(X0) & p112(X0)) | ~r1(X1,X0))) | ~(p111(X1) & ~p112(X1))) & (~(~p106(X1) & p105(X1)) | (~! [X0] : (~(~p107(X0) & p106(X0) & p7(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p107(X0) & p106(X0) & ~p7(X0))))) & ((~! [X0] : (~(~p105(X0) & p104(X0) & ~p5(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p104(X0) & ~p105(X0) & p5(X0)))) | ~(p103(X1) & ~p104(X1))) & (~(~p103(X1) & p102(X1)) | (~! [X0] : (~r1(X1,X0) | ~(p4(X0) & ~p104(X0) & p103(X0))) & ~! [X0] : (~(~p4(X0) & ~p104(X0) & p103(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(~p3(X0) & ~p103(X0) & p102(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p102(X0) & ~p103(X0) & p3(X0)))) | ~(~p102(X1) & p101(X1))) & ((~! [X0] : (~r1(X1,X0) | ~(~p2(X0) & p101(X0) & ~p102(X0))) & ~! [X0] : (~(p2(X0) & p101(X0) & ~p102(X0)) | ~r1(X1,X0))) | ~(p100(X1) & ~p101(X1))) & (((! [X0] : (~p16(X0) | ~p115(X0) | ~r1(X1,X0)) | p16(X1)) & (! [X0] : (~p115(X0) | p16(X0) | ~r1(X1,X0)) | ~p16(X1))) | ~p115(X1)) & (~p114(X1) | ((p15(X1) | ! [X0] : (~r1(X1,X0) | ~p15(X0) | ~p114(X0))) & (~p15(X1) | ! [X0] : (~r1(X1,X0) | p15(X0) | ~p114(X0))))) & (~p113(X1) | ((p14(X1) | ! [X0] : (~p113(X0) | ~p14(X0) | ~r1(X1,X0))) & (~p14(X1) | ! [X0] : (~p113(X0) | p14(X0) | ~r1(X1,X0))))) & (((~p13(X1) | ! [X0] : (~r1(X1,X0) | p13(X0) | ~p112(X0))) & (p13(X1) | ! [X0] : (~p112(X0) | ~p13(X0) | ~r1(X1,X0)))) | ~p112(X1)) & (((! [X0] : (~r1(X1,X0) | ~p100(X0) | ~p1(X0)) | p1(X1)) & (~p1(X1) | ! [X0] : (~r1(X1,X0) | p1(X0) | ~p100(X0)))) | ~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)) & (p115(X1) | ~p116(X1)) & (((~p2(X1) | ! [X0] : (~p101(X0) | p2(X0) | ~r1(X1,X0))) & (p2(X1) | ! [X0] : (~r1(X1,X0) | ~p2(X0) | ~p101(X0)))) | ~p101(X1)) & (((! [X0] : (p3(X0) | ~p102(X0) | ~r1(X1,X0)) | ~p3(X1)) & (! [X0] : (~p3(X0) | ~p102(X0) | ~r1(X1,X0)) | p3(X1))) | ~p102(X1)) & (~p103(X1) | ((p4(X1) | ! [X0] : (~p103(X0) | ~p4(X0) | ~r1(X1,X0))) & (! [X0] : (~r1(X1,X0) | p4(X0) | ~p103(X0)) | ~p4(X1)))) & (((! [X0] : (p5(X0) | ~p104(X0) | ~r1(X1,X0)) | ~p5(X1)) & (p5(X1) | ! [X0] : (~r1(X1,X0) | ~p104(X0) | ~p5(X0)))) | ~p104(X1)) & (((~p6(X1) | ! [X0] : (~p105(X0) | p6(X0) | ~r1(X1,X0))) & (! [X0] : (~p105(X0) | ~p6(X0) | ~r1(X1,X0)) | p6(X1))) | ~p105(X1)) & (~p106(X1) | ((! [X0] : (~r1(X1,X0) | ~p7(X0) | ~p106(X0)) | p7(X1)) & (! [X0] : (~r1(X1,X0) | ~p106(X0) | p7(X0)) | ~p7(X1)))) & (((p8(X1) | ! [X0] : (~p8(X0) | ~p107(X0) | ~r1(X1,X0))) & (~p8(X1) | ! [X0] : (~r1(X1,X0) | ~p107(X0) | p8(X0)))) | ~p107(X1)) & (~p108(X1) | ((~p9(X1) | ! [X0] : (~p108(X0) | p9(X0) | ~r1(X1,X0))) & (! [X0] : (~r1(X1,X0) | ~p108(X0) | ~p9(X0)) | p9(X1)))) & (((p10(X1) | ! [X0] : (~p109(X0) | ~p10(X0) | ~r1(X1,X0))) & (~p10(X1) | ! [X0] : (~r1(X1,X0) | ~p109(X0) | p10(X0)))) | ~p109(X1)) & (~p110(X1) | ((! [X0] : (~r1(X1,X0) | p11(X0) | ~p110(X0)) | ~p11(X1)) & (p11(X1) | ! [X0] : (~p11(X0) | ~p110(X0) | ~r1(X1,X0))))) & (~p111(X1) | ((p12(X1) | ! [X0] : (~p12(X0) | ~p111(X0) | ~r1(X1,X0))) & (~p12(X1) | ! [X0] : (p12(X0) | ~p111(X0) | ~r1(X1,X0))))) & ((~! [X0] : (~(~p6(X0) & p105(X0) & ~p106(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(p6(X0) & p105(X0) & ~p106(X0)))) | ~(~p105(X1) & p104(X1))) & ((~! [X0] : (~r1(X1,X0) | ~(~p8(X0) & ~p108(X0) & p107(X0))) & ~! [X0] : (~r1(X1,X0) | ~(p8(X0) & ~p108(X0) & p107(X0)))) | ~(~p107(X1) & p106(X1))) & (~(p107(X1) & ~p108(X1)) | (~! [X0] : (~r1(X1,X0) | ~(~p109(X0) & p108(X0) & p9(X0))) & ~! [X0] : (~(p108(X0) & ~p109(X0) & ~p9(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(p109(X0) & ~p110(X0) & ~p10(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(p109(X0) & ~p110(X0) & p10(X0)) | ~r1(X1,X0))) | ~(~p109(X1) & p108(X1))) & ((~! [X0] : (~(p11(X0) & ~p111(X0) & p110(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p111(X0) & p110(X0) & ~p11(X0)))) | ~(~p110(X1) & p109(X1))) & (~(p110(X1) & ~p111(X1)) | (~! [X0] : (~(~p112(X0) & p111(X0) & p12(X0)) | ~r1(X1,X0)) & ~! [X0] : (~(~p112(X0) & p111(X0) & ~p12(X0)) | ~r1(X1,X0)))) & (~(~p113(X1) & p112(X1)) | (~! [X0] : (~r1(X1,X0) | ~(p113(X0) & ~p114(X0) & p14(X0))) & ~! [X0] : (~(p113(X0) & ~p114(X0) & ~p14(X0)) | ~r1(X1,X0)))) & ((~! [X0] : (~(~p116(X0) & p115(X0) & ~p16(X0)) | ~r1(X1,X0)) & ~! [X0] : (~r1(X1,X0) | ~(~p116(X0) & p115(X0) & p16(X0)))) | ~(~p115(X1) & p114(X1))))) & p100(X0) & ~p101(X0)) | ~! [X1] : (~r1(X0,X1) | p7(X1)))[input] 34456. r1(sK30,sK14(sK22(sK20(sK18(sK16(sK30)))))) (19:8) [unit resulting resolution 4987,5164,327] 327. ~r1(X1,X2) | r1(X0,X2) | ~r1(X0,X1) (0:9) [cnf transformation 11] 11. ! [X0,X1,X2] : (~r1(X0,X1) | ~r1(X1,X2) | r1(X0,X2))[flattening 10] 10. ! [X0,X1,X2] : ((~r1(X0,X1) | ~r1(X1,X2)) | r1(X0,X2))[ennf transformation 1] 1. ! [X0,X1,X2] : ((r1(X0,X1) & r1(X1,X2)) => r1(X0,X2))[input] 5164. r1(sK22(sK20(sK18(sK16(sK30)))),sK14(sK22(sK20(sK18(sK16(sK30)))))) (18:12) [unit resulting resolution 2282,2281,5033,261] 261. ~sP7(X0) | p105(X0) | r1(X0,sK14(X0)) | ~p104(X0) (0:10) [cnf transformation 102] 102. ! [X0] : (~sP7(X0) | ((~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))[skolemisation 101] 101. ! [X0] : (~sP7(X0) | (? [X1] : (~p6(X1) & p105(X1) & ~p106(X1) & r1(X0,X1)) & ? [X2] : (r1(X0,X2) & p6(X2) & p105(X2) & ~p106(X2))) | p105(X0) | ~p104(X0))[rectify 100] 100. ! [X1] : (~sP7(X1) | (? [X48] : (~p6(X48) & p105(X48) & ~p106(X48) & r1(X1,X48)) & ? [X49] : (r1(X1,X49) & p6(X49) & p105(X49) & ~p106(X49))) | p105(X1) | ~p104(X1))[nnf transformation 19] 5033. sP7(sK22(sK20(sK18(sK16(sK30))))) (17:6) [unit resulting resolution 4996,164] 164. ~sP31(X0) | sP7(X0) (0:4) [cnf transformation 46] 4996. sP31(sK22(sK20(sK18(sK16(sK30))))) (16:6) [unit resulting resolution 4987,322] 2281. ~p105(sK22(sK20(sK18(sK16(sK30))))) (14:6) [unit resulting resolution 1162,1163,2181,290] 290. ~p105(sK22(X0)) | ~p103(X0) | p104(X0) | ~sP3(X0) (0:9) [cnf transformation 114] 114. ! [X0] : (~sP3(X0) | ((~p105(sK22(X0)) & p104(sK22(X0)) & ~p5(sK22(X0)) & r1(X0,sK22(X0))) & (r1(X0,sK23(X0)) & p104(sK23(X0)) & ~p105(sK23(X0)) & p5(sK23(X0)))) | ~p103(X0) | p104(X0))[skolemisation 113] 113. ! [X0] : (~sP3(X0) | (? [X1] : (~p105(X1) & p104(X1) & ~p5(X1) & r1(X0,X1)) & ? [X2] : (r1(X0,X2) & p104(X2) & ~p105(X2) & p5(X2))) | ~p103(X0) | p104(X0))[rectify 112] 112. ! [X1] : (~sP3(X1) | (? [X8] : (~p105(X8) & p104(X8) & ~p5(X8) & r1(X1,X8)) & ? [X9] : (r1(X1,X9) & p104(X9) & ~p105(X9) & p5(X9))) | ~p103(X1) | p104(X1))[nnf transformation 15] 2181. sP3(sK20(sK18(sK16(sK30)))) (13:5) [unit resulting resolution 2172,129] 129. ~sP31(X0) | sP3(X0) (0:4) [cnf transformation 46] 2172. sP31(sK20(sK18(sK16(sK30)))) (12:5) [unit resulting resolution 2169,322] 2169. r1(sK30,sK20(sK18(sK16(sK30)))) (11:6) [unit resulting resolution 1043,1560,327] 1560. r1(sK18(sK16(sK30)),sK20(sK18(sK16(sK30)))) (10:8) [unit resulting resolution 1056,639,638,282] 282. ~sP4(X0) | ~p102(X0) | p103(X0) | r1(X0,sK20(X0)) (0:10) [cnf transformation 111] 111. ! [X0] : (~sP4(X0) | p103(X0) | ~p102(X0) | ((r1(X0,sK20(X0)) & p4(sK20(X0)) & ~p104(sK20(X0)) & p103(sK20(X0))) & (~p4(sK21(X0)) & ~p104(sK21(X0)) & p103(sK21(X0)) & r1(X0,sK21(X0)))))[skolemisation 110] 110. ! [X0] : (~sP4(X0) | p103(X0) | ~p102(X0) | (? [X1] : (r1(X0,X1) & p4(X1) & ~p104(X1) & p103(X1)) & ? [X2] : (~p4(X2) & ~p104(X2) & p103(X2) & r1(X0,X2))))[rectify 109] 109. ! [X1] : (~sP4(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))))[nnf transformation 16] 638. p102(sK18(sK16(sK30))) (6:4) [unit resulting resolution 462,466,528,276] 276. ~sP5(X0) | p102(X0) | p102(sK18(X0)) | ~p101(X0) (0:9) [cnf transformation 108] 108. ! [X0] : (~sP5(X0) | ((~p3(sK18(X0)) & ~p103(sK18(X0)) & p102(sK18(X0)) & r1(X0,sK18(X0))) & (r1(X0,sK19(X0)) & p102(sK19(X0)) & ~p103(sK19(X0)) & p3(sK19(X0)))) | p102(X0) | ~p101(X0))[skolemisation 107] 107. ! [X0] : (~sP5(X0) | (? [X1] : (~p3(X1) & ~p103(X1) & p102(X1) & r1(X0,X1)) & ? [X2] : (r1(X0,X2) & p102(X2) & ~p103(X2) & p3(X2))) | p102(X0) | ~p101(X0))[rectify 106] 106. ! [X1] : (~sP5(X1) | (? [X12] : (~p3(X12) & ~p103(X12) & p102(X12) & r1(X1,X12)) & ? [X13] : (r1(X1,X13) & p102(X13) & ~p103(X13) & p3(X13))) | p102(X1) | ~p101(X1))[nnf transformation 17] 528. sP5(sK16(sK30)) (5:3) [unit resulting resolution 517,131] 131. ~sP31(X0) | sP5(X0) (0:4) [cnf transformation 46] 517. sP31(sK16(sK30)) (4:3) [unit resulting resolution 512,322] 512. r1(sK30,sK16(sK30)) (3:4) [unit resulting resolution 324,336,323,266] 266. ~sP6(X0) | ~p100(X0) | r1(X0,sK16(X0)) | p101(X0) (0:10) [cnf transformation 105] 105. ! [X0] : (~sP6(X0) | ((r1(X0,sK16(X0)) & ~p2(sK16(X0)) & p101(sK16(X0)) & ~p102(sK16(X0))) & (p2(sK17(X0)) & p101(sK17(X0)) & ~p102(sK17(X0)) & r1(X0,sK17(X0)))) | ~p100(X0) | p101(X0))[skolemisation 104] 104. ! [X0] : (~sP6(X0) | (? [X1] : (r1(X0,X1) & ~p2(X1) & p101(X1) & ~p102(X1)) & ? [X2] : (p2(X2) & p101(X2) & ~p102(X2) & r1(X0,X2))) | ~p100(X0) | p101(X0))[rectify 103] 103. ! [X1] : (~sP6(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))[nnf transformation 18] 323. p100(sK30) (0:2) [cnf transformation 125] 336. sP6(sK30) (2:2) [unit resulting resolution 328,132] 132. ~sP31(X0) | sP6(X0) (0:4) [cnf transformation 46] 328. sP31(sK30) (1:2) [unit resulting resolution 326,322] 326. r1(X0,X0) (0:3) [cnf transformation 4] 4. ! [X0] : r1(X0,X0)[input] 324. ~p101(sK30) (0:2) [cnf transformation 125] 466. ~p102(sK16(sK30)) (3:3) [unit resulting resolution 336,324,323,269] 269. ~p102(sK16(X0)) | ~p100(X0) | p101(X0) | ~sP6(X0) (0:9) [cnf transformation 105] 462. p101(sK16(sK30)) (3:3) [unit resulting resolution 324,336,323,268] 268. ~sP6(X0) | ~p100(X0) | p101(sK16(X0)) | p101(X0) (0:9) [cnf transformation 105] 639. ~p103(sK18(sK16(sK30))) (6:4) [unit resulting resolution 466,462,528,275] 275. ~p103(sK18(X0)) | p102(X0) | ~p101(X0) | ~sP5(X0) (0:9) [cnf transformation 108] 1056. sP4(sK18(sK16(sK30))) (9:4) [unit resulting resolution 1046,130] 130. ~sP31(X0) | sP4(X0) (0:4) [cnf transformation 46] 1046. sP31(sK18(sK16(sK30))) (8:4) [unit resulting resolution 1043,322] 1043. r1(sK30,sK18(sK16(sK30))) (7:5) [unit resulting resolution 512,1029,327] 1029. r1(sK16(sK30),sK18(sK16(sK30))) (6:6) [unit resulting resolution 462,528,466,277] 277. ~sP5(X0) | p102(X0) | r1(X0,sK18(X0)) | ~p101(X0) (0:10) [cnf transformation 108] 1163. ~p104(sK20(sK18(sK16(sK30)))) (10:5) [unit resulting resolution 638,639,1056,284] 284. ~p104(sK20(X0)) | ~p102(X0) | p103(X0) | ~sP4(X0) (0:9) [cnf transformation 111] 1162. p103(sK20(sK18(sK16(sK30)))) (10:5) [unit resulting resolution 638,639,1056,285] 285. ~sP4(X0) | ~p102(X0) | p103(X0) | p103(sK20(X0)) (0:9) [cnf transformation 111] 2282. p104(sK22(sK20(sK18(sK16(sK30))))) (14:6) [unit resulting resolution 1163,1162,2181,291] 291. ~sP3(X0) | ~p103(X0) | p104(sK22(X0)) | p104(X0) (0:9) [cnf transformation 114] 4987. r1(sK30,sK22(sK20(sK18(sK16(sK30))))) (15:7) [unit resulting resolution 2169,2284,327] 2284. r1(sK20(sK18(sK16(sK30))),sK22(sK20(sK18(sK16(sK30))))) (14:10) [unit resulting resolution 1163,1162,2181,293] 293. ~sP3(X0) | ~p103(X0) | r1(X0,sK22(X0)) | p104(X0) (0:10) [cnf transformation 114] 5163. ~p106(sK14(sK22(sK20(sK18(sK16(sK30)))))) (18:7) [unit resulting resolution 2281,2282,5033,260] 260. ~p106(sK14(X0)) | p105(X0) | ~p104(X0) | ~sP7(X0) (0:9) [cnf transformation 102] 5162. p105(sK14(sK22(sK20(sK18(sK16(sK30)))))) (18:7) [unit resulting resolution 2282,2281,5033,259] 259. ~sP7(X0) | p105(X0) | p105(sK14(X0)) | ~p104(X0) (0:9) [cnf transformation 102] 35136. ~r1(sK14(sK22(sK20(sK18(sK16(sK30))))),sK25(sK14(sK22(sK20(sK18(sK16(sK30))))))) (24:14) [unit resulting resolution 34456,35038,327] 35038. ~r1(sK30,sK25(sK14(sK22(sK20(sK18(sK16(sK30))))))) (23:9) [unit resulting resolution 34723,325] 325. ~r1(sK30,X2) | p7(X2) (0:5) [cnf transformation 125] 34723. ~p7(sK25(sK14(sK22(sK20(sK18(sK16(sK30))))))) (22:8) [unit resulting resolution 5162,5163,34613,305] 305. ~p7(sK25(X0)) | ~p105(X0) | p106(X0) | ~sP2(X0) (0:9) [cnf transformation 117] % SZS output end Proof for FNE056 ------------------------------ Version: Vampire 1.8 (revision 1280) Termination reason: Refutation Active clauses: 3248 Passive clauses: 9092 Generated clauses: 35043 Final active clauses: 3248 Final passive clauses: 601 Input formulas: 3 Initial clauses: 202 Pure predicates: 1 Duplicate literals: 32 Fw subsumption resolutions: 1925 Global subsumptions: 2661 Simple tautologies: 175 Forward subsumptions: 26401 Binary resolution: 15384 Unit resulting resolution: 14840 SAT solver clauses: 20314 SAT solver unit clauses: 13214 SAT solver binary clauses: 1892 SAT solver learnt clauses: 2661 SAT solver learnt literals: 92 Memory used [KB]: 12281 Time elapsed: 0.436 s ------------------------------ % Success in time 21.97 s WATCH: 21.92 CPU 22.00 WC FINAL WATCH: 21.92 CPU 22.00 WC