--------------------------------------------------------------------------- WATCH: 0.00 CPU 0.01 WC SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p SZS output start CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p fof(transitivity, axiom, (! [X, Y, Z] : ((r1(X, Y) & r1(Y, Z)) => r1(X, Z)))). fof(main, conjecture, (~ ? [X] : ~ (~ (! [Y] : (~ r1(X, Y) | (((~ ! [X] : (~ (~ p15(X) & ~ p115(X) & p114(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p15(X) & p114(X) & ~ p115(X)) | ~ r1(Y, X))) | ~ (p113(Y) & ~ p114(Y))) & ((~ ! [X] : (~ (p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X))) | ~ (p111(Y) & ~ p112(Y))) & (~ (~ p106(Y) & p105(Y)) | (~ ! [X] : (~ (~ p107(X) & p106(X) & p7(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p107(X) & p106(X) & ~ p7(X))))) & ((~ ! [X] : (~ (~ p105(X) & p104(X) & ~ p5(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p104(X) & ~ p105(X) & p5(X)))) | ~ (p103(Y) & ~ p104(Y))) & (~ (~ p103(Y) & p102(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p4(X) & ~ p104(X) & p103(X))) & ~ ! [X] : (~ (~ p4(X) & ~ p104(X) & p103(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p3(X) & ~ p103(X) & p102(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p102(X) & ~ p103(X) & p3(X)))) | ~ (~ p102(Y) & p101(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p2(X) & p101(X) & ~ p102(X))) & ~ ! [X] : (~ (p2(X) & p101(X) & ~ p102(X)) | ~ r1(Y, X))) | ~ (p100(Y) & ~ p101(Y))) & (((! [X] : (~ p16(X) | ~ p115(X) | ~ r1(Y, X)) | p16(Y)) & (! [X] : (~ p115(X) | p16(X) | ~ r1(Y, X)) | ~ p16(Y))) | ~ p115(Y)) & (~ p114(Y) | ((p15(Y) | ! [X] : (~ r1(Y, X) | ~ p15(X) | ~ p114(X))) & (~ p15(Y) | ! [X] : (~ r1(Y, X) | p15(X) | ~ p114(X))))) & (~ p113(Y) | ((p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))) & (~ p14(Y) | ! [X] : (~ p113(X) | p14(X) | ~ r1(Y, X))))) & (((~ p13(Y) | ! [X] : (~ r1(Y, X) | p13(X) | ~ p112(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X)))) | ~ p112(Y)) & (((! [X] : (~ r1(Y, X) | ~ p100(X) | ~ p1(X)) | p1(Y)) & (~ p1(Y) | ! [X] : (~ r1(Y, X) | p1(X) | ~ p100(X)))) | ~ p100(Y)) & (p113(Y) | ~ p114(Y)) & (p111(Y) | ~ p112(Y)) & (p110(Y) | ~ p111(Y)) & (p109(Y) | ~ p110(Y)) & (p108(Y) | ~ p109(Y)) & (~ p108(Y) | p107(Y)) & (p106(Y) | ~ p107(Y)) & (p104(Y) | ~ p105(Y)) & (~ p103(Y) | p102(Y)) & (p100(Y) | ~ p101(Y)) & (p101(Y) | ~ p102(Y)) & (p103(Y) | ~ p104(Y)) & (p105(Y) | ~ p106(Y)) & (~ p113(Y) | p112(Y)) & (p114(Y) | ~ p115(Y)) & (p115(Y) | ~ p116(Y)) & (((~ p2(Y) | ! [X] : (~ p101(X) | p2(X) | ~ r1(Y, X))) & (p2(Y) | ! [X] : (~ r1(Y, X) | ~ p2(X) | ~ p101(X)))) | ~ p101(Y)) & (((! [X] : (p3(X) | ~ p102(X) | ~ r1(Y, X)) | ~ p3(Y)) & (! [X] : (~ p3(X) | ~ p102(X) | ~ r1(Y, X)) | p3(Y))) | ~ p102(Y)) & (~ p103(Y) | ((p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | p4(X) | ~ p103(X)) | ~ p4(Y)))) & (((! [X] : (p5(X) | ~ p104(X) | ~ r1(Y, X)) | ~ p5(Y)) & (p5(Y) | ! [X] : (~ r1(Y, X) | ~ p104(X) | ~ p5(X)))) | ~ p104(Y)) & (((~ p6(Y) | ! [X] : (~ p105(X) | p6(X) | ~ r1(Y, X))) & (! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X)) | p6(Y))) | ~ p105(Y)) & (~ p106(Y) | ((! [X] : (~ r1(Y, X) | ~ p7(X) | ~ p106(X)) | p7(Y)) & (! [X] : (~ r1(Y, X) | ~ p106(X) | p7(X)) | ~ p7(Y)))) & (((p8(Y) | ! [X] : (~ p8(X) | ~ p107(X) | ~ r1(Y, X))) & (~ p8(Y) | ! [X] : (~ r1(Y, X) | ~ p107(X) | p8(X)))) | ~ p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | p9(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | ~ p108(X) | ~ p9(X)) | p9(Y)))) & (((p10(Y) | ! [X] : (~ p109(X) | ~ p10(X) | ~ r1(Y, X))) & (~ p10(Y) | ! [X] : (~ r1(Y, X) | ~ p109(X) | p10(X)))) | ~ p109(Y)) & (~ p110(Y) | ((! [X] : (~ r1(Y, X) | p11(X) | ~ p110(X)) | ~ p11(Y)) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | ((p12(Y) | ! [X] : (~ p12(X) | ~ p111(X) | ~ r1(Y, X))) & (~ p12(Y) | ! [X] : (p12(X) | ~ p111(X) | ~ r1(Y, X))))) & ((~ ! [X] : (~ (~ p6(X) & p105(X) & ~ p106(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p6(X) & p105(X) & ~ p106(X)))) | ~ (~ p105(Y) & p104(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p8(X) & ~ p108(X) & p107(X))) & ~ ! [X] : (~ r1(Y, X) | ~ (p8(X) & ~ p108(X) & p107(X)))) | ~ (~ p107(Y) & p106(Y))) & (~ (p107(Y) & ~ p108(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (~ p109(X) & p108(X) & p9(X))) & ~ ! [X] : (~ (p108(X) & ~ p109(X) & ~ p9(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (p109(X) & ~ p110(X) & ~ p10(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p109(X) & ~ p110(X) & p10(X)) | ~ r1(Y, X))) | ~ (~ p109(Y) & p108(Y))) & ((~ ! [X] : (~ (p11(X) & ~ p111(X) & p110(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p111(X) & p110(X) & ~ p11(X)))) | ~ (~ p110(Y) & p109(Y))) & (~ (p110(Y) & ~ p111(Y)) | (~ ! [X] : (~ (~ p112(X) & p111(X) & p12(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p112(X) & p111(X) & ~ p12(X)) | ~ r1(Y, X)))) & (~ (~ p113(Y) & p112(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p113(X) & ~ p114(X) & p14(X))) & ~ ! [X] : (~ (p113(X) & ~ p114(X) & ~ p14(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p116(X) & p115(X) & ~ p16(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p116(X) & p115(X) & p16(X)))) | ~ (~ p115(Y) & p114(Y))))) & p100(X) & ~ p101(X)) | ~ ! [Y] : (~ r1(X, Y) | p7(Y))))). fof(reflexivity, axiom, (! [X] : r1(X, X))). fof(subgoal_0, plain, (! [X] : (~ ~ (! [Y] : (~ r1(X, Y) | (((~ ! [X] : (~ (~ p15(X) & ~ p115(X) & p114(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p15(X) & p114(X) & ~ p115(X)) | ~ r1(Y, X))) | ~ (p113(Y) & ~ p114(Y))) & ((~ ! [X] : (~ (p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X))) | ~ (p111(Y) & ~ p112(Y))) & (~ (~ p106(Y) & p105(Y)) | (~ ! [X] : (~ (~ p107(X) & p106(X) & p7(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p107(X) & p106(X) & ~ p7(X))))) & ((~ ! [X] : (~ (~ p105(X) & p104(X) & ~ p5(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p104(X) & ~ p105(X) & p5(X)))) | ~ (p103(Y) & ~ p104(Y))) & (~ (~ p103(Y) & p102(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p4(X) & ~ p104(X) & p103(X))) & ~ ! [X] : (~ (~ p4(X) & ~ p104(X) & p103(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p3(X) & ~ p103(X) & p102(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p102(X) & ~ p103(X) & p3(X)))) | ~ (~ p102(Y) & p101(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p2(X) & p101(X) & ~ p102(X))) & ~ ! [X] : (~ (p2(X) & p101(X) & ~ p102(X)) | ~ r1(Y, X))) | ~ (p100(Y) & ~ p101(Y))) & (((! [X] : (~ p16(X) | ~ p115(X) | ~ r1(Y, X)) | p16(Y)) & (! [X] : (~ p115(X) | p16(X) | ~ r1(Y, X)) | ~ p16(Y))) | ~ p115(Y)) & (~ p114(Y) | ((p15(Y) | ! [X] : (~ r1(Y, X) | ~ p15(X) | ~ p114(X))) & (~ p15(Y) | ! [X] : (~ r1(Y, X) | p15(X) | ~ p114(X))))) & (~ p113(Y) | ((p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))) & (~ p14(Y) | ! [X] : (~ p113(X) | p14(X) | ~ r1(Y, X))))) & (((~ p13(Y) | ! [X] : (~ r1(Y, X) | p13(X) | ~ p112(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X)))) | ~ p112(Y)) & (((! [X] : (~ r1(Y, X) | ~ p100(X) | ~ p1(X)) | p1(Y)) & (~ p1(Y) | ! [X] : (~ r1(Y, X) | p1(X) | ~ p100(X)))) | ~ p100(Y)) & (p113(Y) | ~ p114(Y)) & (p111(Y) | ~ p112(Y)) & (p110(Y) | ~ p111(Y)) & (p109(Y) | ~ p110(Y)) & (p108(Y) | ~ p109(Y)) & (~ p108(Y) | p107(Y)) & (p106(Y) | ~ p107(Y)) & (p104(Y) | ~ p105(Y)) & (~ p103(Y) | p102(Y)) & (p100(Y) | ~ p101(Y)) & (p101(Y) | ~ p102(Y)) & (p103(Y) | ~ p104(Y)) & (p105(Y) | ~ p106(Y)) & (~ p113(Y) | p112(Y)) & (p114(Y) | ~ p115(Y)) & (p115(Y) | ~ p116(Y)) & (((~ p2(Y) | ! [X] : (~ p101(X) | p2(X) | ~ r1(Y, X))) & (p2(Y) | ! [X] : (~ r1(Y, X) | ~ p2(X) | ~ p101(X)))) | ~ p101(Y)) & (((! [X] : (p3(X) | ~ p102(X) | ~ r1(Y, X)) | ~ p3(Y)) & (! [X] : (~ p3(X) | ~ p102(X) | ~ r1(Y, X)) | p3(Y))) | ~ p102(Y)) & (~ p103(Y) | ((p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | p4(X) | ~ p103(X)) | ~ p4(Y)))) & (((! [X] : (p5(X) | ~ p104(X) | ~ r1(Y, X)) | ~ p5(Y)) & (p5(Y) | ! [X] : (~ r1(Y, X) | ~ p104(X) | ~ p5(X)))) | ~ p104(Y)) & (((~ p6(Y) | ! [X] : (~ p105(X) | p6(X) | ~ r1(Y, X))) & (! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X)) | p6(Y))) | ~ p105(Y)) & (~ p106(Y) | ((! [X] : (~ r1(Y, X) | ~ p7(X) | ~ p106(X)) | p7(Y)) & (! [X] : (~ r1(Y, X) | ~ p106(X) | p7(X)) | ~ p7(Y)))) & (((p8(Y) | ! [X] : (~ p8(X) | ~ p107(X) | ~ r1(Y, X))) & (~ p8(Y) | ! [X] : (~ r1(Y, X) | ~ p107(X) | p8(X)))) | ~ p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | p9(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | ~ p108(X) | ~ p9(X)) | p9(Y)))) & (((p10(Y) | ! [X] : (~ p109(X) | ~ p10(X) | ~ r1(Y, X))) & (~ p10(Y) | ! [X] : (~ r1(Y, X) | ~ p109(X) | p10(X)))) | ~ p109(Y)) & (~ p110(Y) | ((! [X] : (~ r1(Y, X) | p11(X) | ~ p110(X)) | ~ p11(Y)) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | ((p12(Y) | ! [X] : (~ p12(X) | ~ p111(X) | ~ r1(Y, X))) & (~ p12(Y) | ! [X] : (p12(X) | ~ p111(X) | ~ r1(Y, X))))) & ((~ ! [X] : (~ (~ p6(X) & p105(X) & ~ p106(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p6(X) & p105(X) & ~ p106(X)))) | ~ (~ p105(Y) & p104(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p8(X) & ~ p108(X) & p107(X))) & ~ ! [X] : (~ r1(Y, X) | ~ (p8(X) & ~ p108(X) & p107(X)))) | ~ (~ p107(Y) & p106(Y))) & (~ (p107(Y) & ~ p108(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (~ p109(X) & p108(X) & p9(X))) & ~ ! [X] : (~ (p108(X) & ~ p109(X) & ~ p9(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (p109(X) & ~ p110(X) & ~ p10(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p109(X) & ~ p110(X) & p10(X)) | ~ r1(Y, X))) | ~ (~ p109(Y) & p108(Y))) & ((~ ! [X] : (~ (p11(X) & ~ p111(X) & p110(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p111(X) & p110(X) & ~ p11(X)))) | ~ (~ p110(Y) & p109(Y))) & (~ (p110(Y) & ~ p111(Y)) | (~ ! [X] : (~ (~ p112(X) & p111(X) & p12(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p112(X) & p111(X) & ~ p12(X)) | ~ r1(Y, X)))) & (~ (~ p113(Y) & p112(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p113(X) & ~ p114(X) & p14(X))) & ~ ! [X] : (~ (p113(X) & ~ p114(X) & ~ p14(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p116(X) & p115(X) & ~ p16(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p116(X) & p115(X) & p16(X)))) | ~ (~ p115(Y) & p114(Y))))) & p100(X) & ~ p101(X)) => ~ ! [Y] : (~ r1(X, Y) | p7(Y)))), inference(strip, [], [main])). fof(negate_0_0, plain, (~ ! [X] : (~ ~ (! [Y] : (~ r1(X, Y) | (((~ ! [X] : (~ (~ p15(X) & ~ p115(X) & p114(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p15(X) & p114(X) & ~ p115(X)) | ~ r1(Y, X))) | ~ (p113(Y) & ~ p114(Y))) & ((~ ! [X] : (~ (p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p13(X) & ~ p113(X) & p112(X)) | ~ r1(Y, X))) | ~ (p111(Y) & ~ p112(Y))) & (~ (~ p106(Y) & p105(Y)) | (~ ! [X] : (~ (~ p107(X) & p106(X) & p7(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p107(X) & p106(X) & ~ p7(X))))) & ((~ ! [X] : (~ (~ p105(X) & p104(X) & ~ p5(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p104(X) & ~ p105(X) & p5(X)))) | ~ (p103(Y) & ~ p104(Y))) & (~ (~ p103(Y) & p102(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p4(X) & ~ p104(X) & p103(X))) & ~ ! [X] : (~ (~ p4(X) & ~ p104(X) & p103(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p3(X) & ~ p103(X) & p102(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p102(X) & ~ p103(X) & p3(X)))) | ~ (~ p102(Y) & p101(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p2(X) & p101(X) & ~ p102(X))) & ~ ! [X] : (~ (p2(X) & p101(X) & ~ p102(X)) | ~ r1(Y, X))) | ~ (p100(Y) & ~ p101(Y))) & (((! [X] : (~ p16(X) | ~ p115(X) | ~ r1(Y, X)) | p16(Y)) & (! [X] : (~ p115(X) | p16(X) | ~ r1(Y, X)) | ~ p16(Y))) | ~ p115(Y)) & (~ p114(Y) | ((p15(Y) | ! [X] : (~ r1(Y, X) | ~ p15(X) | ~ p114(X))) & (~ p15(Y) | ! [X] : (~ r1(Y, X) | p15(X) | ~ p114(X))))) & (~ p113(Y) | ((p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))) & (~ p14(Y) | ! [X] : (~ p113(X) | p14(X) | ~ r1(Y, X))))) & (((~ p13(Y) | ! [X] : (~ r1(Y, X) | p13(X) | ~ p112(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X)))) | ~ p112(Y)) & (((! [X] : (~ r1(Y, X) | ~ p100(X) | ~ p1(X)) | p1(Y)) & (~ p1(Y) | ! [X] : (~ r1(Y, X) | p1(X) | ~ p100(X)))) | ~ p100(Y)) & (p113(Y) | ~ p114(Y)) & (p111(Y) | ~ p112(Y)) & (p110(Y) | ~ p111(Y)) & (p109(Y) | ~ p110(Y)) & (p108(Y) | ~ p109(Y)) & (~ p108(Y) | p107(Y)) & (p106(Y) | ~ p107(Y)) & (p104(Y) | ~ p105(Y)) & (~ p103(Y) | p102(Y)) & (p100(Y) | ~ p101(Y)) & (p101(Y) | ~ p102(Y)) & (p103(Y) | ~ p104(Y)) & (p105(Y) | ~ p106(Y)) & (~ p113(Y) | p112(Y)) & (p114(Y) | ~ p115(Y)) & (p115(Y) | ~ p116(Y)) & (((~ p2(Y) | ! [X] : (~ p101(X) | p2(X) | ~ r1(Y, X))) & (p2(Y) | ! [X] : (~ r1(Y, X) | ~ p2(X) | ~ p101(X)))) | ~ p101(Y)) & (((! [X] : (p3(X) | ~ p102(X) | ~ r1(Y, X)) | ~ p3(Y)) & (! [X] : (~ p3(X) | ~ p102(X) | ~ r1(Y, X)) | p3(Y))) | ~ p102(Y)) & (~ p103(Y) | ((p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | p4(X) | ~ p103(X)) | ~ p4(Y)))) & (((! [X] : (p5(X) | ~ p104(X) | ~ r1(Y, X)) | ~ p5(Y)) & (p5(Y) | ! [X] : (~ r1(Y, X) | ~ p104(X) | ~ p5(X)))) | ~ p104(Y)) & (((~ p6(Y) | ! [X] : (~ p105(X) | p6(X) | ~ r1(Y, X))) & (! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X)) | p6(Y))) | ~ p105(Y)) & (~ p106(Y) | ((! [X] : (~ r1(Y, X) | ~ p7(X) | ~ p106(X)) | p7(Y)) & (! [X] : (~ r1(Y, X) | ~ p106(X) | p7(X)) | ~ p7(Y)))) & (((p8(Y) | ! [X] : (~ p8(X) | ~ p107(X) | ~ r1(Y, X))) & (~ p8(Y) | ! [X] : (~ r1(Y, X) | ~ p107(X) | p8(X)))) | ~ p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | p9(X) | ~ r1(Y, X))) & (! [X] : (~ r1(Y, X) | ~ p108(X) | ~ p9(X)) | p9(Y)))) & (((p10(Y) | ! [X] : (~ p109(X) | ~ p10(X) | ~ r1(Y, X))) & (~ p10(Y) | ! [X] : (~ r1(Y, X) | ~ p109(X) | p10(X)))) | ~ p109(Y)) & (~ p110(Y) | ((! [X] : (~ r1(Y, X) | p11(X) | ~ p110(X)) | ~ p11(Y)) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | ((p12(Y) | ! [X] : (~ p12(X) | ~ p111(X) | ~ r1(Y, X))) & (~ p12(Y) | ! [X] : (p12(X) | ~ p111(X) | ~ r1(Y, X))))) & ((~ ! [X] : (~ (~ p6(X) & p105(X) & ~ p106(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (p6(X) & p105(X) & ~ p106(X)))) | ~ (~ p105(Y) & p104(Y))) & ((~ ! [X] : (~ r1(Y, X) | ~ (~ p8(X) & ~ p108(X) & p107(X))) & ~ ! [X] : (~ r1(Y, X) | ~ (p8(X) & ~ p108(X) & p107(X)))) | ~ (~ p107(Y) & p106(Y))) & (~ (p107(Y) & ~ p108(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (~ p109(X) & p108(X) & p9(X))) & ~ ! [X] : (~ (p108(X) & ~ p109(X) & ~ p9(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (p109(X) & ~ p110(X) & ~ p10(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (p109(X) & ~ p110(X) & p10(X)) | ~ r1(Y, X))) | ~ (~ p109(Y) & p108(Y))) & ((~ ! [X] : (~ (p11(X) & ~ p111(X) & p110(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p111(X) & p110(X) & ~ p11(X)))) | ~ (~ p110(Y) & p109(Y))) & (~ (p110(Y) & ~ p111(Y)) | (~ ! [X] : (~ (~ p112(X) & p111(X) & p12(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ (~ p112(X) & p111(X) & ~ p12(X)) | ~ r1(Y, X)))) & (~ (~ p113(Y) & p112(Y)) | (~ ! [X] : (~ r1(Y, X) | ~ (p113(X) & ~ p114(X) & p14(X))) & ~ ! [X] : (~ (p113(X) & ~ p114(X) & ~ p14(X)) | ~ r1(Y, X)))) & ((~ ! [X] : (~ (~ p116(X) & p115(X) & ~ p16(X)) | ~ r1(Y, X)) & ~ ! [X] : (~ r1(Y, X) | ~ (~ p116(X) & p115(X) & p16(X)))) | ~ (~ p115(Y) & p114(Y))))) & p100(X) & ~ p101(X)) => ~ ! [Y] : (~ r1(X, Y) | p7(Y)))), inference(negate, [], [subgoal_0])). fof(normalize_0_0, plain, (? [X] : (~ p101(X) & p100(X) & ! [Y] : (~ r1(X, Y) | p7(Y)) & ! [Y] : (~ r1(X, Y) | ((~ p100(Y) | ((~ p1(Y) | ! [X] : (~ p100(X) | ~ r1(Y, X) | p1(X))) & (p1(Y) | ! [X] : (~ p1(X) | ~ p100(X) | ~ r1(Y, X))))) & (~ p101(Y) | p100(Y)) & (~ p101(Y) | ((~ p2(Y) | ! [X] : (~ p101(X) | ~ r1(Y, X) | p2(X))) & (p2(Y) | ! [X] : (~ p101(X) | ~ p2(X) | ~ r1(Y, X))))) & (~ p102(Y) | p101(Y)) & (~ p102(Y) | ((~ p3(Y) | ! [X] : (~ p102(X) | ~ r1(Y, X) | p3(X))) & (p3(Y) | ! [X] : (~ p102(X) | ~ p3(X) | ~ r1(Y, X))))) & (~ p103(Y) | p102(Y)) & (~ p103(Y) | ((~ p4(Y) | ! [X] : (~ p103(X) | ~ r1(Y, X) | p4(X))) & (p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))))) & (~ p104(Y) | p103(Y)) & (~ p104(Y) | ((~ p5(Y) | ! [X] : (~ p104(X) | ~ r1(Y, X) | p5(X))) & (p5(Y) | ! [X] : (~ p104(X) | ~ p5(X) | ~ r1(Y, X))))) & (~ p105(Y) | p104(Y)) & (~ p105(Y) | ((~ p6(Y) | ! [X] : (~ p105(X) | ~ r1(Y, X) | p6(X))) & (p6(Y) | ! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X))))) & (~ p106(Y) | p105(Y)) & (~ p106(Y) | ((~ p7(Y) | ! [X] : (~ p106(X) | ~ r1(Y, X) | p7(X))) & (p7(Y) | ! [X] : (~ p106(X) | ~ p7(X) | ~ r1(Y, X))))) & (~ p107(Y) | p106(Y)) & (~ p107(Y) | ((~ p8(Y) | ! [X] : (~ p107(X) | ~ r1(Y, X) | p8(X))) & (p8(Y) | ! [X] : (~ p107(X) | ~ p8(X) | ~ r1(Y, X))))) & (~ p108(Y) | p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | ~ r1(Y, X) | p9(X))) & (p9(Y) | ! [X] : (~ p108(X) | ~ p9(X) | ~ r1(Y, X))))) & (~ p109(Y) | p108(Y)) & (~ p109(Y) | ((~ p10(Y) | ! [X] : (~ p109(X) | ~ r1(Y, X) | p10(X))) & (p10(Y) | ! [X] : (~ p10(X) | ~ p109(X) | ~ r1(Y, X))))) & (~ p110(Y) | p109(Y)) & (~ p110(Y) | ((~ p11(Y) | ! [X] : (~ p110(X) | ~ r1(Y, X) | p11(X))) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | p110(Y)) & (~ p111(Y) | ((~ p12(Y) | ! [X] : (~ p111(X) | ~ r1(Y, X) | p12(X))) & (p12(Y) | ! [X] : (~ p111(X) | ~ p12(X) | ~ r1(Y, X))))) & (~ p112(Y) | p111(Y)) & (~ p112(Y) | ((~ p13(Y) | ! [X] : (~ p112(X) | ~ r1(Y, X) | p13(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X))))) & (~ p113(Y) | p112(Y)) & (~ p113(Y) | ((~ p14(Y) | ! [X] : (~ p113(X) | ~ r1(Y, X) | p14(X))) & (p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))))) & (~ p114(Y) | p113(Y)) & (~ p114(Y) | ((~ p15(Y) | ! [X] : (~ p114(X) | ~ r1(Y, X) | p15(X))) & (p15(Y) | ! [X] : (~ p114(X) | ~ p15(X) | ~ r1(Y, X))))) & (~ p115(Y) | p114(Y)) & (~ p115(Y) | ((~ p16(Y) | ! [X] : (~ p115(X) | ~ r1(Y, X) | p16(X))) & (p16(Y) | ! [X] : (~ p115(X) | ~ p16(X) | ~ r1(Y, X))))) & (~ p116(Y) | p115(Y)) & (~ p100(Y) | p101(Y) | (? [X] : (~ p102(X) & ~ p2(X) & p101(X) & r1(Y, X)) & ? [X] : (~ p102(X) & p101(X) & p2(X) & r1(Y, X)))) & (~ p101(Y) | p102(Y) | (? [X] : (~ p103(X) & ~ p3(X) & p102(X) & r1(Y, X)) & ? [X] : (~ p103(X) & p102(X) & p3(X) & r1(Y, X)))) & (~ p102(Y) | p103(Y) | (? [X] : (~ p104(X) & ~ p4(X) & p103(X) & r1(Y, X)) & ? [X] : (~ p104(X) & p103(X) & p4(X) & r1(Y, X)))) & (~ p103(Y) | p104(Y) | (? [X] : (~ p105(X) & ~ p5(X) & p104(X) & r1(Y, X)) & ? [X] : (~ p105(X) & p104(X) & p5(X) & r1(Y, X)))) & (~ p104(Y) | p105(Y) | (? [X] : (~ p106(X) & ~ p6(X) & p105(X) & r1(Y, X)) & ? [X] : (~ p106(X) & p105(X) & p6(X) & r1(Y, X)))) & (~ p105(Y) | p106(Y) | (? [X] : (~ p107(X) & ~ p7(X) & p106(X) & r1(Y, X)) & ? [X] : (~ p107(X) & p106(X) & p7(X) & r1(Y, X)))) & (~ p106(Y) | p107(Y) | (? [X] : (~ p108(X) & ~ p8(X) & p107(X) & r1(Y, X)) & ? [X] : (~ p108(X) & p107(X) & p8(X) & r1(Y, X)))) & (~ p107(Y) | p108(Y) | (? [X] : (~ p109(X) & ~ p9(X) & p108(X) & r1(Y, X)) & ? [X] : (~ p109(X) & p108(X) & p9(X) & r1(Y, X)))) & (~ p108(Y) | p109(Y) | (? [X] : (~ p10(X) & ~ p110(X) & p109(X) & r1(Y, X)) & ? [X] : (~ p110(X) & p10(X) & p109(X) & r1(Y, X)))) & (~ p109(Y) | p110(Y) | (? [X] : (~ p11(X) & ~ p111(X) & p110(X) & r1(Y, X)) & ? [X] : (~ p111(X) & p11(X) & p110(X) & r1(Y, X)))) & (~ p110(Y) | p111(Y) | (? [X] : (~ p112(X) & ~ p12(X) & p111(X) & r1(Y, X)) & ? [X] : (~ p112(X) & p111(X) & p12(X) & r1(Y, X)))) & (~ p111(Y) | p112(Y) | (? [X] : (~ p113(X) & ~ p13(X) & p112(X) & r1(Y, X)) & ? [X] : (~ p113(X) & p112(X) & p13(X) & r1(Y, X)))) & (~ p112(Y) | p113(Y) | (? [X] : (~ p114(X) & ~ p14(X) & p113(X) & r1(Y, X)) & ? [X] : (~ p114(X) & p113(X) & p14(X) & r1(Y, X)))) & (~ p113(Y) | p114(Y) | (? [X] : (~ p115(X) & ~ p15(X) & p114(X) & r1(Y, X)) & ? [X] : (~ p115(X) & p114(X) & p15(X) & r1(Y, X)))) & (~ p114(Y) | p115(Y) | (? [X] : (~ p116(X) & ~ p16(X) & p115(X) & r1(Y, X)) & ? [X] : (~ p116(X) & p115(X) & p16(X) & r1(Y, X)))))))), inference(canonicalize, [], [negate_0_0])). fof(normalize_0_1, plain, (~ p101(skolemFOFtoCNF_X) & p100(skolemFOFtoCNF_X) & ! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | p7(Y)) & ! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | ((~ p100(Y) | ((~ p1(Y) | ! [X] : (~ p100(X) | ~ r1(Y, X) | p1(X))) & (p1(Y) | ! [X] : (~ p1(X) | ~ p100(X) | ~ r1(Y, X))))) & (~ p101(Y) | p100(Y)) & (~ p101(Y) | ((~ p2(Y) | ! [X] : (~ p101(X) | ~ r1(Y, X) | p2(X))) & (p2(Y) | ! [X] : (~ p101(X) | ~ p2(X) | ~ r1(Y, X))))) & (~ p102(Y) | p101(Y)) & (~ p102(Y) | ((~ p3(Y) | ! [X] : (~ p102(X) | ~ r1(Y, X) | p3(X))) & (p3(Y) | ! [X] : (~ p102(X) | ~ p3(X) | ~ r1(Y, X))))) & (~ p103(Y) | p102(Y)) & (~ p103(Y) | ((~ p4(Y) | ! [X] : (~ p103(X) | ~ r1(Y, X) | p4(X))) & (p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))))) & (~ p104(Y) | p103(Y)) & (~ p104(Y) | ((~ p5(Y) | ! [X] : (~ p104(X) | ~ r1(Y, X) | p5(X))) & (p5(Y) | ! [X] : (~ p104(X) | ~ p5(X) | ~ r1(Y, X))))) & (~ p105(Y) | p104(Y)) & (~ p105(Y) | ((~ p6(Y) | ! [X] : (~ p105(X) | ~ r1(Y, X) | p6(X))) & (p6(Y) | ! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X))))) & (~ p106(Y) | p105(Y)) & (~ p106(Y) | ((~ p7(Y) | ! [X] : (~ p106(X) | ~ r1(Y, X) | p7(X))) & (p7(Y) | ! [X] : (~ p106(X) | ~ p7(X) | ~ r1(Y, X))))) & (~ p107(Y) | p106(Y)) & (~ p107(Y) | ((~ p8(Y) | ! [X] : (~ p107(X) | ~ r1(Y, X) | p8(X))) & (p8(Y) | ! [X] : (~ p107(X) | ~ p8(X) | ~ r1(Y, X))))) & (~ p108(Y) | p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | ~ r1(Y, X) | p9(X))) & (p9(Y) | ! [X] : (~ p108(X) | ~ p9(X) | ~ r1(Y, X))))) & (~ p109(Y) | p108(Y)) & (~ p109(Y) | ((~ p10(Y) | ! [X] : (~ p109(X) | ~ r1(Y, X) | p10(X))) & (p10(Y) | ! [X] : (~ p10(X) | ~ p109(X) | ~ r1(Y, X))))) & (~ p110(Y) | p109(Y)) & (~ p110(Y) | ((~ p11(Y) | ! [X] : (~ p110(X) | ~ r1(Y, X) | p11(X))) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | p110(Y)) & (~ p111(Y) | ((~ p12(Y) | ! [X] : (~ p111(X) | ~ r1(Y, X) | p12(X))) & (p12(Y) | ! [X] : (~ p111(X) | ~ p12(X) | ~ r1(Y, X))))) & (~ p112(Y) | p111(Y)) & (~ p112(Y) | ((~ p13(Y) | ! [X] : (~ p112(X) | ~ r1(Y, X) | p13(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X))))) & (~ p113(Y) | p112(Y)) & (~ p113(Y) | ((~ p14(Y) | ! [X] : (~ p113(X) | ~ r1(Y, X) | p14(X))) & (p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))))) & (~ p114(Y) | p113(Y)) & (~ p114(Y) | ((~ p15(Y) | ! [X] : (~ p114(X) | ~ r1(Y, X) | p15(X))) & (p15(Y) | ! [X] : (~ p114(X) | ~ p15(X) | ~ r1(Y, X))))) & (~ p115(Y) | p114(Y)) & (~ p115(Y) | ((~ p16(Y) | ! [X] : (~ p115(X) | ~ r1(Y, X) | p16(X))) & (p16(Y) | ! [X] : (~ p115(X) | ~ p16(X) | ~ r1(Y, X))))) & (~ p116(Y) | p115(Y)) & (~ p100(Y) | p101(Y) | (? [X] : (~ p102(X) & ~ p2(X) & p101(X) & r1(Y, X)) & ? [X] : (~ p102(X) & p101(X) & p2(X) & r1(Y, X)))) & (~ p101(Y) | p102(Y) | (? [X] : (~ p103(X) & ~ p3(X) & p102(X) & r1(Y, X)) & ? [X] : (~ p103(X) & p102(X) & p3(X) & r1(Y, X)))) & (~ p102(Y) | p103(Y) | (? [X] : (~ p104(X) & ~ p4(X) & p103(X) & r1(Y, X)) & ? [X] : (~ p104(X) & p103(X) & p4(X) & r1(Y, X)))) & (~ p103(Y) | p104(Y) | (? [X] : (~ p105(X) & ~ p5(X) & p104(X) & r1(Y, X)) & ? [X] : (~ p105(X) & p104(X) & p5(X) & r1(Y, X)))) & (~ p104(Y) | p105(Y) | (? [X] : (~ p106(X) & ~ p6(X) & p105(X) & r1(Y, X)) & ? [X] : (~ p106(X) & p105(X) & p6(X) & r1(Y, X)))) & (~ p105(Y) | p106(Y) | (? [X] : (~ p107(X) & ~ p7(X) & p106(X) & r1(Y, X)) & ? [X] : (~ p107(X) & p106(X) & p7(X) & r1(Y, X)))) & (~ p106(Y) | p107(Y) | (? [X] : (~ p108(X) & ~ p8(X) & p107(X) & r1(Y, X)) & ? [X] : (~ p108(X) & p107(X) & p8(X) & r1(Y, X)))) & (~ p107(Y) | p108(Y) | (? [X] : (~ p109(X) & ~ p9(X) & p108(X) & r1(Y, X)) & ? [X] : (~ p109(X) & p108(X) & p9(X) & r1(Y, X)))) & (~ p108(Y) | p109(Y) | (? [X] : (~ p10(X) & ~ p110(X) & p109(X) & r1(Y, X)) & ? [X] : (~ p110(X) & p10(X) & p109(X) & r1(Y, X)))) & (~ p109(Y) | p110(Y) | (? [X] : (~ p11(X) & ~ p111(X) & p110(X) & r1(Y, X)) & ? [X] : (~ p111(X) & p11(X) & p110(X) & r1(Y, X)))) & (~ p110(Y) | p111(Y) | (? [X] : (~ p112(X) & ~ p12(X) & p111(X) & r1(Y, X)) & ? [X] : (~ p112(X) & p111(X) & p12(X) & r1(Y, X)))) & (~ p111(Y) | p112(Y) | (? [X] : (~ p113(X) & ~ p13(X) & p112(X) & r1(Y, X)) & ? [X] : (~ p113(X) & p112(X) & p13(X) & r1(Y, X)))) & (~ p112(Y) | p113(Y) | (? [X] : (~ p114(X) & ~ p14(X) & p113(X) & r1(Y, X)) & ? [X] : (~ p114(X) & p113(X) & p14(X) & r1(Y, X)))) & (~ p113(Y) | p114(Y) | (? [X] : (~ p115(X) & ~ p15(X) & p114(X) & r1(Y, X)) & ? [X] : (~ p115(X) & p114(X) & p15(X) & r1(Y, X)))) & (~ p114(Y) | p115(Y) | (? [X] : (~ p116(X) & ~ p16(X) & p115(X) & r1(Y, X)) & ? [X] : (~ p116(X) & p115(X) & p16(X) & r1(Y, X))))))), inference(skolemize, [], [normalize_0_0])). fof(normalize_0_2, plain, (! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | p7(Y))), inference(conjunct, [], [normalize_0_1])). fof(normalize_0_3, plain, (! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | p7(Y))), inference(specialize, [], [normalize_0_2])). fof(normalize_0_4, plain, (! [X] : r1(X, X)), inference(canonicalize, [], [reflexivity])). fof(normalize_0_5, plain, (! [X] : r1(X, X)), inference(specialize, [], [normalize_0_4])). fof(normalize_0_6, plain, (! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | ((~ p100(Y) | ((~ p1(Y) | ! [X] : (~ p100(X) | ~ r1(Y, X) | p1(X))) & (p1(Y) | ! [X] : (~ p1(X) | ~ p100(X) | ~ r1(Y, X))))) & (~ p101(Y) | p100(Y)) & (~ p101(Y) | ((~ p2(Y) | ! [X] : (~ p101(X) | ~ r1(Y, X) | p2(X))) & (p2(Y) | ! [X] : (~ p101(X) | ~ p2(X) | ~ r1(Y, X))))) & (~ p102(Y) | p101(Y)) & (~ p102(Y) | ((~ p3(Y) | ! [X] : (~ p102(X) | ~ r1(Y, X) | p3(X))) & (p3(Y) | ! [X] : (~ p102(X) | ~ p3(X) | ~ r1(Y, X))))) & (~ p103(Y) | p102(Y)) & (~ p103(Y) | ((~ p4(Y) | ! [X] : (~ p103(X) | ~ r1(Y, X) | p4(X))) & (p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))))) & (~ p104(Y) | p103(Y)) & (~ p104(Y) | ((~ p5(Y) | ! [X] : (~ p104(X) | ~ r1(Y, X) | p5(X))) & (p5(Y) | ! [X] : (~ p104(X) | ~ p5(X) | ~ r1(Y, X))))) & (~ p105(Y) | p104(Y)) & (~ p105(Y) | ((~ p6(Y) | ! [X] : (~ p105(X) | ~ r1(Y, X) | p6(X))) & (p6(Y) | ! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X))))) & (~ p106(Y) | p105(Y)) & (~ p106(Y) | ((~ p7(Y) | ! [X] : (~ p106(X) | ~ r1(Y, X) | p7(X))) & (p7(Y) | ! [X] : (~ p106(X) | ~ p7(X) | ~ r1(Y, X))))) & (~ p107(Y) | p106(Y)) & (~ p107(Y) | ((~ p8(Y) | ! [X] : (~ p107(X) | ~ r1(Y, X) | p8(X))) & (p8(Y) | ! [X] : (~ p107(X) | ~ p8(X) | ~ r1(Y, X))))) & (~ p108(Y) | p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | ~ r1(Y, X) | p9(X))) & (p9(Y) | ! [X] : (~ p108(X) | ~ p9(X) | ~ r1(Y, X))))) & (~ p109(Y) | p108(Y)) & (~ p109(Y) | ((~ p10(Y) | ! [X] : (~ p109(X) | ~ r1(Y, X) | p10(X))) & (p10(Y) | ! [X] : (~ p10(X) | ~ p109(X) | ~ r1(Y, X))))) & (~ p110(Y) | p109(Y)) & (~ p110(Y) | ((~ p11(Y) | ! [X] : (~ p110(X) | ~ r1(Y, X) | p11(X))) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | p110(Y)) & (~ p111(Y) | ((~ p12(Y) | ! [X] : (~ p111(X) | ~ r1(Y, X) | p12(X))) & (p12(Y) | ! [X] : (~ p111(X) | ~ p12(X) | ~ r1(Y, X))))) & (~ p112(Y) | p111(Y)) & (~ p112(Y) | ((~ p13(Y) | ! [X] : (~ p112(X) | ~ r1(Y, X) | p13(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X))))) & (~ p113(Y) | p112(Y)) & (~ p113(Y) | ((~ p14(Y) | ! [X] : (~ p113(X) | ~ r1(Y, X) | p14(X))) & (p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))))) & (~ p114(Y) | p113(Y)) & (~ p114(Y) | ((~ p15(Y) | ! [X] : (~ p114(X) | ~ r1(Y, X) | p15(X))) & (p15(Y) | ! [X] : (~ p114(X) | ~ p15(X) | ~ r1(Y, X))))) & (~ p115(Y) | p114(Y)) & (~ p115(Y) | ((~ p16(Y) | ! [X] : (~ p115(X) | ~ r1(Y, X) | p16(X))) & (p16(Y) | ! [X] : (~ p115(X) | ~ p16(X) | ~ r1(Y, X))))) & (~ p116(Y) | p115(Y)) & (~ p100(Y) | p101(Y) | (? [X] : (~ p102(X) & ~ p2(X) & p101(X) & r1(Y, X)) & ? [X] : (~ p102(X) & p101(X) & p2(X) & r1(Y, X)))) & (~ p101(Y) | p102(Y) | (? [X] : (~ p103(X) & ~ p3(X) & p102(X) & r1(Y, X)) & ? [X] : (~ p103(X) & p102(X) & p3(X) & r1(Y, X)))) & (~ p102(Y) | p103(Y) | (? [X] : (~ p104(X) & ~ p4(X) & p103(X) & r1(Y, X)) & ? [X] : (~ p104(X) & p103(X) & p4(X) & r1(Y, X)))) & (~ p103(Y) | p104(Y) | (? [X] : (~ p105(X) & ~ p5(X) & p104(X) & r1(Y, X)) & ? [X] : (~ p105(X) & p104(X) & p5(X) & r1(Y, X)))) & (~ p104(Y) | p105(Y) | (? [X] : (~ p106(X) & ~ p6(X) & p105(X) & r1(Y, X)) & ? [X] : (~ p106(X) & p105(X) & p6(X) & r1(Y, X)))) & (~ p105(Y) | p106(Y) | (? [X] : (~ p107(X) & ~ p7(X) & p106(X) & r1(Y, X)) & ? [X] : (~ p107(X) & p106(X) & p7(X) & r1(Y, X)))) & (~ p106(Y) | p107(Y) | (? [X] : (~ p108(X) & ~ p8(X) & p107(X) & r1(Y, X)) & ? [X] : (~ p108(X) & p107(X) & p8(X) & r1(Y, X)))) & (~ p107(Y) | p108(Y) | (? [X] : (~ p109(X) & ~ p9(X) & p108(X) & r1(Y, X)) & ? [X] : (~ p109(X) & p108(X) & p9(X) & r1(Y, X)))) & (~ p108(Y) | p109(Y) | (? [X] : (~ p10(X) & ~ p110(X) & p109(X) & r1(Y, X)) & ? [X] : (~ p110(X) & p10(X) & p109(X) & r1(Y, X)))) & (~ p109(Y) | p110(Y) | (? [X] : (~ p11(X) & ~ p111(X) & p110(X) & r1(Y, X)) & ? [X] : (~ p111(X) & p11(X) & p110(X) & r1(Y, X)))) & (~ p110(Y) | p111(Y) | (? [X] : (~ p112(X) & ~ p12(X) & p111(X) & r1(Y, X)) & ? [X] : (~ p112(X) & p111(X) & p12(X) & r1(Y, X)))) & (~ p111(Y) | p112(Y) | (? [X] : (~ p113(X) & ~ p13(X) & p112(X) & r1(Y, X)) & ? [X] : (~ p113(X) & p112(X) & p13(X) & r1(Y, X)))) & (~ p112(Y) | p113(Y) | (? [X] : (~ p114(X) & ~ p14(X) & p113(X) & r1(Y, X)) & ? [X] : (~ p114(X) & p113(X) & p14(X) & r1(Y, X)))) & (~ p113(Y) | p114(Y) | (? [X] : (~ p115(X) & ~ p15(X) & p114(X) & r1(Y, X)) & ? [X] : (~ p115(X) & p114(X) & p15(X) & r1(Y, X)))) & (~ p114(Y) | p115(Y) | (? [X] : (~ p116(X) & ~ p16(X) & p115(X) & r1(Y, X)) & ? [X] : (~ p116(X) & p115(X) & p16(X) & r1(Y, X))))))), inference(conjunct, [], [normalize_0_1])). fof(normalize_0_7, plain, (! [Y] : (~ r1(skolemFOFtoCNF_X, Y) | ((~ p100(Y) | ((~ p1(Y) | ! [X] : (~ p100(X) | ~ r1(Y, X) | p1(X))) & (p1(Y) | ! [X] : (~ p1(X) | ~ p100(X) | ~ r1(Y, X))))) & (~ p101(Y) | p100(Y)) & (~ p101(Y) | ((~ p2(Y) | ! [X] : (~ p101(X) | ~ r1(Y, X) | p2(X))) & (p2(Y) | ! [X] : (~ p101(X) | ~ p2(X) | ~ r1(Y, X))))) & (~ p102(Y) | p101(Y)) & (~ p102(Y) | ((~ p3(Y) | ! [X] : (~ p102(X) | ~ r1(Y, X) | p3(X))) & (p3(Y) | ! [X] : (~ p102(X) | ~ p3(X) | ~ r1(Y, X))))) & (~ p103(Y) | p102(Y)) & (~ p103(Y) | ((~ p4(Y) | ! [X] : (~ p103(X) | ~ r1(Y, X) | p4(X))) & (p4(Y) | ! [X] : (~ p103(X) | ~ p4(X) | ~ r1(Y, X))))) & (~ p104(Y) | p103(Y)) & (~ p104(Y) | ((~ p5(Y) | ! [X] : (~ p104(X) | ~ r1(Y, X) | p5(X))) & (p5(Y) | ! [X] : (~ p104(X) | ~ p5(X) | ~ r1(Y, X))))) & (~ p105(Y) | p104(Y)) & (~ p105(Y) | ((~ p6(Y) | ! [X] : (~ p105(X) | ~ r1(Y, X) | p6(X))) & (p6(Y) | ! [X] : (~ p105(X) | ~ p6(X) | ~ r1(Y, X))))) & (~ p106(Y) | p105(Y)) & (~ p106(Y) | ((~ p7(Y) | ! [X] : (~ p106(X) | ~ r1(Y, X) | p7(X))) & (p7(Y) | ! [X] : (~ p106(X) | ~ p7(X) | ~ r1(Y, X))))) & (~ p107(Y) | p106(Y)) & (~ p107(Y) | ((~ p8(Y) | ! [X] : (~ p107(X) | ~ r1(Y, X) | p8(X))) & (p8(Y) | ! [X] : (~ p107(X) | ~ p8(X) | ~ r1(Y, X))))) & (~ p108(Y) | p107(Y)) & (~ p108(Y) | ((~ p9(Y) | ! [X] : (~ p108(X) | ~ r1(Y, X) | p9(X))) & (p9(Y) | ! [X] : (~ p108(X) | ~ p9(X) | ~ r1(Y, X))))) & (~ p109(Y) | p108(Y)) & (~ p109(Y) | ((~ p10(Y) | ! [X] : (~ p109(X) | ~ r1(Y, X) | p10(X))) & (p10(Y) | ! [X] : (~ p10(X) | ~ p109(X) | ~ r1(Y, X))))) & (~ p110(Y) | p109(Y)) & (~ p110(Y) | ((~ p11(Y) | ! [X] : (~ p110(X) | ~ r1(Y, X) | p11(X))) & (p11(Y) | ! [X] : (~ p11(X) | ~ p110(X) | ~ r1(Y, X))))) & (~ p111(Y) | p110(Y)) & (~ p111(Y) | ((~ p12(Y) | ! [X] : (~ p111(X) | ~ r1(Y, X) | p12(X))) & (p12(Y) | ! [X] : (~ p111(X) | ~ p12(X) | ~ r1(Y, X))))) & (~ p112(Y) | p111(Y)) & (~ p112(Y) | ((~ p13(Y) | ! [X] : (~ p112(X) | ~ r1(Y, X) | p13(X))) & (p13(Y) | ! [X] : (~ p112(X) | ~ p13(X) | ~ r1(Y, X))))) & (~ p113(Y) | p112(Y)) & (~ p113(Y) | ((~ p14(Y) | ! [X] : (~ p113(X) | ~ r1(Y, X) | p14(X))) & (p14(Y) | ! [X] : (~ p113(X) | ~ p14(X) | ~ r1(Y, X))))) & (~ p114(Y) | p113(Y)) & (~ p114(Y) | ((~ p15(Y) | ! [X] : (~ p114(X) | ~ r1(Y, X) | p15(X))) & (p15(Y) | ! [X] : (~ p114(X) | ~ p15(X) | ~ r1(Y, X))))) & (~ p115(Y) | p114(Y)) & (~ p115(Y) | ((~ p16(Y) | ! [X] : (~ p115(X) | ~ r1(Y, X) | p16(X))) & (p16(Y) | ! [X] : (~ p115(X) | ~ p16(X) | ~ r1(Y, X))))) & (~ p116(Y) | p115(Y)) & (~ p100(Y) | p101(Y) | (? [X] : (~ p102(X) & ~ p2(X) & p101(X) & r1(Y, X)) & ? [X] : (~ p102(X) & p101(X) & p2(X) & r1(Y, X)))) & (~ p101(Y) | p102(Y) | (? [X] : (~ p103(X) & ~ p3(X) & p102(X) & r1(Y, X)) & ? [X] : (~ p103(X) & p102(X) & p3(X) & r1(Y, X)))) & (~ p102(Y) | p103(Y) | (? [X] : (~ p104(X) & ~ p4(X) & p103(X) & r1(Y, X)) & ? [X] : (~ p104(X) & p103(X) & p4(X) & r1(Y, X)))) & (~ p103(Y) | p104(Y) | (? [X] : (~ p105(X) & ~ p5(X) & p104(X) & r1(Y, X)) & ? [X] : (~ p105(X) & p104(X) & p5(X) & r1(Y, X)))) & (~ p104(Y) | p105(Y) | (? [X] : (~ p106(X) & ~ p6(X) & p105(X) & r1(Y, X)) & ? [X] : (~ p106(X) & p105(X) & p6(X) & r1(Y, X)))) & (~ p105(Y) | p106(Y) | (? [X] : (~ p107(X) & ~ p7(X) & p106(X) & r1(Y, X)) & ? [X] : (~ p107(X) & p106(X) & p7(X) & r1(Y, X)))) & (~ p106(Y) | p107(Y) | (? [X] : (~ p108(X) & ~ p8(X) & p107(X) & r1(Y, X)) & ? [X] : (~ p108(X) & p107(X) & p8(X) & r1(Y, X)))) & (~ p107(Y) | p108(Y) | (? [X] : (~ p109(X) & ~ p9(X) & p108(X) & r1(Y, X)) & ? [X] : (~ p109(X) & p108(X) & p9(X) & r1(Y, X)))) & (~ p108(Y) | p109(Y) | (? [X] : (~ p10(X) & ~ p110(X) & p109(X) & r1(Y, X)) & ? [X] : (~ p110(X) & p10(X) & p109(X) & r1(Y, X)))) & (~ p109(Y) | p110(Y) | (? [X] : (~ p11(X) & ~ p111(X) & p110(X) & r1(Y, X)) & ? [X] : (~ p111(X) & p11(X) & p110(X) & r1(Y, X)))) & (~ p110(Y) | p111(Y) | (? [X] : (~ p112(X) & ~ p12(X) & p111(X) & r1(Y, X)) & ? [X] : (~ p112(X) & p111(X) & p12(X) & r1(Y, X)))) & (~ p111(Y) | p112(Y) | (? [X] : (~ p113(X) & ~ p13(X) & p112(X) & r1(Y, X)) & ? [X] : (~ p113(X) & p112(X) & p13(X) & r1(Y, X)))) & (~ p112(Y) | p113(Y) | (? [X] : (~ p114(X) & ~ p14(X) & p113(X) & r1(Y, X)) & ? [X] : (~ p114(X) & p113(X) & p14(X) & r1(Y, X)))) & (~ p113(Y) | p114(Y) | (? [X] : (~ p115(X) & ~ p15(X) & p114(X) & r1(Y, X)) & ? [X] : (~ p115(X) & p114(X) & p15(X) & r1(Y, X)))) & (~ p114(Y) | p115(Y) | (? [X] : (~ p116(X) & ~ p16(X) & p115(X) & r1(Y, X)) & ? [X] : (~ p116(X) & p115(X) & p16(X) & r1(Y, X))))))), inference(specialize, [], [normalize_0_6])). fof(normalize_0_8, plain, (! [X, Y] : ((~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p100(Y)) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y)) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y)) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y)) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y)) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y)) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y)) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y)) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y)) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y)) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y)) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y)) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y)) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y)) & (~ p115(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y)) & (~ p116(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y)) & (~ p10(skolemFOFtoCNF_X_14(Y)) | ~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y)) & (~ p100(Y) | ~ p102(skolemFOFtoCNF_X_29(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y)) & (~ p100(Y) | ~ p102(skolemFOFtoCNF_X_30(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y)) & (~ p100(Y) | ~ p2(skolemFOFtoCNF_X_30(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y)) & (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | p101(skolemFOFtoCNF_X_29(Y))) & (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | p101(skolemFOFtoCNF_X_30(Y))) & (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | p2(skolemFOFtoCNF_X_29(Y))) & (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | r1(Y, skolemFOFtoCNF_X_29(Y))) & (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | r1(Y, skolemFOFtoCNF_X_30(Y))) & (~ p101(Y) | ~ p103(skolemFOFtoCNF_X_27(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y)) & (~ p101(Y) | ~ p103(skolemFOFtoCNF_X_28(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y)) & (~ p101(Y) | ~ p3(skolemFOFtoCNF_X_28(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y)) & (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | p102(skolemFOFtoCNF_X_27(Y))) & (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | p102(skolemFOFtoCNF_X_28(Y))) & (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | p3(skolemFOFtoCNF_X_27(Y))) & (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | r1(Y, skolemFOFtoCNF_X_27(Y))) & (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | r1(Y, skolemFOFtoCNF_X_28(Y))) & (~ p102(Y) | ~ p104(skolemFOFtoCNF_X_25(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y)) & (~ p102(Y) | ~ p104(skolemFOFtoCNF_X_26(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y)) & (~ p102(Y) | ~ p4(skolemFOFtoCNF_X_26(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y)) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | p103(skolemFOFtoCNF_X_25(Y))) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | p103(skolemFOFtoCNF_X_26(Y))) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | p4(skolemFOFtoCNF_X_25(Y))) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | r1(Y, skolemFOFtoCNF_X_25(Y))) & (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | r1(Y, skolemFOFtoCNF_X_26(Y))) & (~ p103(Y) | ~ p105(skolemFOFtoCNF_X_23(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y)) & (~ p103(Y) | ~ p105(skolemFOFtoCNF_X_24(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y)) & (~ p103(Y) | ~ p5(skolemFOFtoCNF_X_24(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y)) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | p104(skolemFOFtoCNF_X_23(Y))) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | p104(skolemFOFtoCNF_X_24(Y))) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | p5(skolemFOFtoCNF_X_23(Y))) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | r1(Y, skolemFOFtoCNF_X_23(Y))) & (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | r1(Y, skolemFOFtoCNF_X_24(Y))) & (~ p104(Y) | ~ p106(skolemFOFtoCNF_X_21(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y)) & (~ p104(Y) | ~ p106(skolemFOFtoCNF_X_22(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y)) & (~ p104(Y) | ~ p6(skolemFOFtoCNF_X_22(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y)) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | p105(skolemFOFtoCNF_X_21(Y))) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | p105(skolemFOFtoCNF_X_22(Y))) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | p6(skolemFOFtoCNF_X_21(Y))) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | r1(Y, skolemFOFtoCNF_X_21(Y))) & (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | r1(Y, skolemFOFtoCNF_X_22(Y))) & (~ p105(Y) | ~ p107(skolemFOFtoCNF_X_19(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y)) & (~ p105(Y) | ~ p107(skolemFOFtoCNF_X_20(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y)) & (~ p105(Y) | ~ p7(skolemFOFtoCNF_X_20(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y)) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | p106(skolemFOFtoCNF_X_19(Y))) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | p106(skolemFOFtoCNF_X_20(Y))) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | p7(skolemFOFtoCNF_X_19(Y))) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | r1(Y, skolemFOFtoCNF_X_19(Y))) & (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | r1(Y, skolemFOFtoCNF_X_20(Y))) & (~ p106(Y) | ~ p108(skolemFOFtoCNF_X_17(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y)) & (~ p106(Y) | ~ p108(skolemFOFtoCNF_X_18(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y)) & (~ p106(Y) | ~ p8(skolemFOFtoCNF_X_18(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y)) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y) | p107(skolemFOFtoCNF_X_17(Y))) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y) | p107(skolemFOFtoCNF_X_18(Y))) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y) | p8(skolemFOFtoCNF_X_17(Y))) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y) | r1(Y, skolemFOFtoCNF_X_17(Y))) & (~ p106(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p107(Y) | r1(Y, skolemFOFtoCNF_X_18(Y))) & (~ p107(Y) | ~ p109(skolemFOFtoCNF_X_15(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y)) & (~ p107(Y) | ~ p109(skolemFOFtoCNF_X_16(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y)) & (~ p107(Y) | ~ p9(skolemFOFtoCNF_X_16(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y)) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y) | p108(skolemFOFtoCNF_X_15(Y))) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y) | p108(skolemFOFtoCNF_X_16(Y))) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y) | p9(skolemFOFtoCNF_X_15(Y))) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y) | r1(Y, skolemFOFtoCNF_X_15(Y))) & (~ p107(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p108(Y) | r1(Y, skolemFOFtoCNF_X_16(Y))) & (~ p108(Y) | ~ p110(skolemFOFtoCNF_X_13(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y)) & (~ p108(Y) | ~ p110(skolemFOFtoCNF_X_14(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y)) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p10(skolemFOFtoCNF_X_13(Y)) | p109(Y)) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y) | p109(skolemFOFtoCNF_X_13(Y))) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y) | p109(skolemFOFtoCNF_X_14(Y))) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y) | r1(Y, skolemFOFtoCNF_X_13(Y))) & (~ p108(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p109(Y) | r1(Y, skolemFOFtoCNF_X_14(Y))) & (~ p109(Y) | ~ p11(skolemFOFtoCNF_X_12(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y)) & (~ p109(Y) | ~ p111(skolemFOFtoCNF_X_11(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y)) & (~ p109(Y) | ~ p111(skolemFOFtoCNF_X_12(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y)) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p11(skolemFOFtoCNF_X_11(Y)) | p110(Y)) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y) | p110(skolemFOFtoCNF_X_11(Y))) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y) | p110(skolemFOFtoCNF_X_12(Y))) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y) | r1(Y, skolemFOFtoCNF_X_11(Y))) & (~ p109(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p110(Y) | r1(Y, skolemFOFtoCNF_X_12(Y))) & (~ p110(Y) | ~ p112(skolemFOFtoCNF_X_10(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y)) & (~ p110(Y) | ~ p112(skolemFOFtoCNF_X_9(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y)) & (~ p110(Y) | ~ p12(skolemFOFtoCNF_X_10(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y)) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y) | p111(skolemFOFtoCNF_X_10(Y))) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y) | p111(skolemFOFtoCNF_X_9(Y))) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y) | p12(skolemFOFtoCNF_X_9(Y))) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y) | r1(Y, skolemFOFtoCNF_X_10(Y))) & (~ p110(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p111(Y) | r1(Y, skolemFOFtoCNF_X_9(Y))) & (~ p111(Y) | ~ p113(skolemFOFtoCNF_X_7(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y)) & (~ p111(Y) | ~ p113(skolemFOFtoCNF_X_8(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y)) & (~ p111(Y) | ~ p13(skolemFOFtoCNF_X_8(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y)) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y) | p112(skolemFOFtoCNF_X_7(Y))) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y) | p112(skolemFOFtoCNF_X_8(Y))) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y) | p13(skolemFOFtoCNF_X_7(Y))) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y) | r1(Y, skolemFOFtoCNF_X_7(Y))) & (~ p111(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p112(Y) | r1(Y, skolemFOFtoCNF_X_8(Y))) & (~ p112(Y) | ~ p114(skolemFOFtoCNF_X_5(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y)) & (~ p112(Y) | ~ p114(skolemFOFtoCNF_X_6(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y)) & (~ p112(Y) | ~ p14(skolemFOFtoCNF_X_6(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y)) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y) | p113(skolemFOFtoCNF_X_5(Y))) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y) | p113(skolemFOFtoCNF_X_6(Y))) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y) | p14(skolemFOFtoCNF_X_5(Y))) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y) | r1(Y, skolemFOFtoCNF_X_5(Y))) & (~ p112(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p113(Y) | r1(Y, skolemFOFtoCNF_X_6(Y))) & (~ p113(Y) | ~ p115(skolemFOFtoCNF_X_3(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y)) & (~ p113(Y) | ~ p115(skolemFOFtoCNF_X_4(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y)) & (~ p113(Y) | ~ p15(skolemFOFtoCNF_X_4(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y)) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y) | p114(skolemFOFtoCNF_X_3(Y))) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y) | p114(skolemFOFtoCNF_X_4(Y))) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y) | p15(skolemFOFtoCNF_X_3(Y))) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y) | r1(Y, skolemFOFtoCNF_X_3(Y))) & (~ p113(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p114(Y) | r1(Y, skolemFOFtoCNF_X_4(Y))) & (~ p114(Y) | ~ p116(skolemFOFtoCNF_X_1(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y)) & (~ p114(Y) | ~ p116(skolemFOFtoCNF_X_2(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y)) & (~ p114(Y) | ~ p16(skolemFOFtoCNF_X_2(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y)) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y) | p115(skolemFOFtoCNF_X_1(Y))) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y) | p115(skolemFOFtoCNF_X_2(Y))) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y) | p16(skolemFOFtoCNF_X_1(Y))) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y) | r1(Y, skolemFOFtoCNF_X_1(Y))) & (~ p114(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p115(Y) | r1(Y, skolemFOFtoCNF_X_2(Y))) & (~ p1(X) | ~ p100(X) | ~ p100(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p1(Y)) & (~ p1(Y) | ~ p100(X) | ~ p100(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p1(X)) & (~ p10(X) | ~ p109(X) | ~ p109(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p10(Y)) & (~ p10(Y) | ~ p109(X) | ~ p109(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p10(X)) & (~ p101(X) | ~ p101(Y) | ~ p2(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p2(Y)) & (~ p101(X) | ~ p101(Y) | ~ p2(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p2(X)) & (~ p102(X) | ~ p102(Y) | ~ p3(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p3(Y)) & (~ p102(X) | ~ p102(Y) | ~ p3(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p3(X)) & (~ p103(X) | ~ p103(Y) | ~ p4(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p4(Y)) & (~ p103(X) | ~ p103(Y) | ~ p4(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p4(X)) & (~ p104(X) | ~ p104(Y) | ~ p5(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p5(Y)) & (~ p104(X) | ~ p104(Y) | ~ p5(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p5(X)) & (~ p105(X) | ~ p105(Y) | ~ p6(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p6(Y)) & (~ p105(X) | ~ p105(Y) | ~ p6(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p6(X)) & (~ p106(X) | ~ p106(Y) | ~ p7(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p7(Y)) & (~ p106(X) | ~ p106(Y) | ~ p7(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p7(X)) & (~ p107(X) | ~ p107(Y) | ~ p8(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p8(Y)) & (~ p107(X) | ~ p107(Y) | ~ p8(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p8(X)) & (~ p108(X) | ~ p108(Y) | ~ p9(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p9(Y)) & (~ p108(X) | ~ p108(Y) | ~ p9(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p9(X)) & (~ p11(X) | ~ p110(X) | ~ p110(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p11(Y)) & (~ p11(Y) | ~ p110(X) | ~ p110(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p11(X)) & (~ p111(X) | ~ p111(Y) | ~ p12(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p12(Y)) & (~ p111(X) | ~ p111(Y) | ~ p12(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p12(X)) & (~ p112(X) | ~ p112(Y) | ~ p13(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p13(Y)) & (~ p112(X) | ~ p112(Y) | ~ p13(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p13(X)) & (~ p113(X) | ~ p113(Y) | ~ p14(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p14(Y)) & (~ p113(X) | ~ p113(Y) | ~ p14(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p14(X)) & (~ p114(X) | ~ p114(Y) | ~ p15(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p15(Y)) & (~ p114(X) | ~ p114(Y) | ~ p15(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p15(X)) & (~ p115(X) | ~ p115(Y) | ~ p16(X) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p16(Y)) & (~ p115(X) | ~ p115(Y) | ~ p16(Y) | ~ r1(Y, X) | ~ r1(skolemFOFtoCNF_X, Y) | p16(X)))), inference(clausify, [], [normalize_0_7])). fof(normalize_0_9, plain, (! [Y] : (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | r1(Y, skolemFOFtoCNF_X_29(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_10, plain, (p100(skolemFOFtoCNF_X)), inference(conjunct, [], [normalize_0_1])). fof(normalize_0_11, plain, (~ p101(skolemFOFtoCNF_X)), inference(conjunct, [], [normalize_0_1])). fof(normalize_0_12, plain, (! [Y] : (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | r1(Y, skolemFOFtoCNF_X_27(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_13, plain, (! [Y] : (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | p101(skolemFOFtoCNF_X_29(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_14, plain, (! [Y] : (~ p100(Y) | ~ p102(skolemFOFtoCNF_X_29(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_15, plain, (! [X, Y, Z] : (~ r1(X, Y) | ~ r1(Y, Z) | r1(X, Z))), inference(canonicalize, [], [transitivity])). fof(normalize_0_16, plain, (! [X, Y, Z] : (~ r1(X, Y) | ~ r1(Y, Z) | r1(X, Z))), inference(specialize, [], [normalize_0_15])). fof(normalize_0_17, plain, (! [Y] : (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | r1(Y, skolemFOFtoCNF_X_20(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_18, plain, (! [Y] : (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | r1(Y, skolemFOFtoCNF_X_22(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_19, plain, (! [Y] : (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | r1(Y, skolemFOFtoCNF_X_24(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_20, plain, (! [Y] : (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | r1(Y, skolemFOFtoCNF_X_26(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_21, plain, (! [Y] : (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | p102(skolemFOFtoCNF_X_27(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_22, plain, (! [Y] : (~ p101(Y) | ~ p103(skolemFOFtoCNF_X_27(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_23, plain, (! [Y] : (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | p103(skolemFOFtoCNF_X_26(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_24, plain, (! [Y] : (~ p102(Y) | ~ p104(skolemFOFtoCNF_X_26(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_25, plain, (! [Y] : (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | p104(skolemFOFtoCNF_X_24(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_26, plain, (! [Y] : (~ p103(Y) | ~ p105(skolemFOFtoCNF_X_24(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_27, plain, (! [Y] : (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | p105(skolemFOFtoCNF_X_22(Y)))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_28, plain, (! [Y] : (~ p104(Y) | ~ p106(skolemFOFtoCNF_X_22(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y))), inference(conjunct, [], [normalize_0_8])). fof(normalize_0_29, plain, (! [Y] : (~ p105(Y) | ~ p7(skolemFOFtoCNF_X_20(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y))), inference(conjunct, [], [normalize_0_8])). cnf(refute_0_0, plain, (~ r1(skolemFOFtoCNF_X, Y) | p7(Y)), inference(canonicalize, [], [normalize_0_3])). cnf(refute_0_1, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(subst, [], [refute_0_0 : [bind(Y, $fot(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))]])). cnf(refute_0_2, plain, (r1(X, X)), inference(canonicalize, [], [normalize_0_5])). cnf(refute_0_3, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X)), inference(subst, [], [refute_0_2 : [bind(X, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_4, plain, (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | r1(Y, skolemFOFtoCNF_X_29(Y))), inference(canonicalize, [], [normalize_0_9])). cnf(refute_0_5, plain, (~ p100(skolemFOFtoCNF_X) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(subst, [], [refute_0_4 : [bind(Y, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_6, plain, (~ p100(skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X))], [refute_0_3, refute_0_5])). cnf(refute_0_7, plain, (p100(skolemFOFtoCNF_X)), inference(canonicalize, [], [normalize_0_10])). cnf(refute_0_8, plain, (p101(skolemFOFtoCNF_X) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p100(skolemFOFtoCNF_X))], [refute_0_7, refute_0_6])). cnf(refute_0_9, plain, (~ p101(skolemFOFtoCNF_X)), inference(canonicalize, [], [normalize_0_11])). cnf(refute_0_10, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X))], [refute_0_8, refute_0_9])). cnf(refute_0_11, plain, (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | r1(Y, skolemFOFtoCNF_X_27(Y))), inference(canonicalize, [], [normalize_0_12])). cnf(refute_0_12, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(subst, [], [refute_0_11 : [bind(Y, $fot(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))]])). cnf(refute_0_13, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_10, refute_0_12])). cnf(refute_0_14, plain, (~ p100(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y) | p101(skolemFOFtoCNF_X_29(Y))), inference(canonicalize, [], [normalize_0_13])). cnf(refute_0_15, plain, (~ p100(skolemFOFtoCNF_X) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(subst, [], [refute_0_14 : [bind(Y, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_16, plain, (~ p100(skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X))], [refute_0_3, refute_0_15])). cnf(refute_0_17, plain, (p101(skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p100(skolemFOFtoCNF_X))], [refute_0_7, refute_0_16])). cnf(refute_0_18, plain, (p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X))], [refute_0_17, refute_0_9])). cnf(refute_0_19, plain, (p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_18, refute_0_13])). cnf(refute_0_20, plain, (~ p100(Y) | ~ p102(skolemFOFtoCNF_X_29(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p101(Y)), inference(canonicalize, [], [normalize_0_14])). cnf(refute_0_21, plain, (~ p100(skolemFOFtoCNF_X) | ~ p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X) | p101(skolemFOFtoCNF_X)), inference(subst, [], [refute_0_20 : [bind(Y, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_22, plain, (~ p100(skolemFOFtoCNF_X) | ~ p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p101(skolemFOFtoCNF_X)), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X))], [refute_0_3, refute_0_21])). cnf(refute_0_23, plain, (~ p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p101(skolemFOFtoCNF_X)), inference(resolve, [$cnf(p100(skolemFOFtoCNF_X))], [refute_0_7, refute_0_22])). cnf(refute_0_24, plain, (~ p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X))], [refute_0_23, refute_0_9])). cnf(refute_0_25, plain, (r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_19, refute_0_24])). cnf(refute_0_26, plain, (~ r1(X, Y) | ~ r1(Y, Z) | r1(X, Z)), inference(canonicalize, [], [normalize_0_16])). cnf(refute_0_27, plain, (~ r1(X_138, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(X_138, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(subst, [], [refute_0_26 : [bind(X, $fot(X_138)), bind(Y, $fot(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), bind(Z, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))]])). cnf(refute_0_28, plain, (~ r1(X_138, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | r1(X_138, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X), skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_25, refute_0_27])). cnf(refute_0_29, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(subst, [], [refute_0_28 : [bind(X_138, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_30, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_10, refute_0_29])). cnf(refute_0_31, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | r1(X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(subst, [], [refute_0_26 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Z, $fot(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))]])). cnf(refute_0_32, plain, (~ p105(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y) | r1(Y, skolemFOFtoCNF_X_20(Y))), inference(canonicalize, [], [normalize_0_17])). cnf(refute_0_33, plain, (~ p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(subst, [], [refute_0_32 : [bind(Y, $fot(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))]])). cnf(refute_0_34, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(subst, [], [refute_0_26 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Z, $fot(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))]])). cnf(refute_0_35, plain, (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | r1(Y, skolemFOFtoCNF_X_22(Y))), inference(canonicalize, [], [normalize_0_18])). cnf(refute_0_36, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(subst, [], [refute_0_35 : [bind(Y, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_37, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_26 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Z, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_38, plain, (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | r1(Y, skolemFOFtoCNF_X_24(Y))), inference(canonicalize, [], [normalize_0_19])). cnf(refute_0_39, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_38 : [bind(Y, $fot(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))]])). cnf(refute_0_40, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | r1(X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(subst, [], [refute_0_26 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Z, $fot(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))]])). cnf(refute_0_41, plain, (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | r1(Y, skolemFOFtoCNF_X_26(Y))), inference(canonicalize, [], [normalize_0_20])). cnf(refute_0_42, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(subst, [], [refute_0_41 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))]])). cnf(refute_0_43, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_42])). cnf(refute_0_44, plain, (~ p101(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y) | p102(skolemFOFtoCNF_X_27(Y))), inference(canonicalize, [], [normalize_0_21])). cnf(refute_0_45, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(subst, [], [refute_0_44 : [bind(Y, $fot(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))]])). cnf(refute_0_46, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_10, refute_0_45])). cnf(refute_0_47, plain, (p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_18, refute_0_46])). cnf(refute_0_48, plain, (p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_47, refute_0_24])). cnf(refute_0_49, plain, (p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_48, refute_0_43])). cnf(refute_0_50, plain, (~ p101(Y) | ~ p103(skolemFOFtoCNF_X_27(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p102(Y)), inference(canonicalize, [], [normalize_0_22])). cnf(refute_0_51, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(subst, [], [refute_0_50 : [bind(Y, $fot(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))]])). cnf(refute_0_52, plain, (~ p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)) | ~ p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_10, refute_0_51])). cnf(refute_0_53, plain, (~ p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), inference(resolve, [$cnf(p101(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_18, refute_0_52])). cnf(refute_0_54, plain, (~ p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))], [refute_0_53, refute_0_24])). cnf(refute_0_55, plain, (r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_49, refute_0_54])). cnf(refute_0_56, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_55, refute_0_40])). cnf(refute_0_57, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(subst, [], [refute_0_56 : [bind(X, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_58, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_57])). cnf(refute_0_59, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_58, refute_0_39])). cnf(refute_0_60, plain, (~ p102(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y) | p103(skolemFOFtoCNF_X_26(Y))), inference(canonicalize, [], [normalize_0_23])). cnf(refute_0_61, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(subst, [], [refute_0_60 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))]])). cnf(refute_0_62, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_61])). cnf(refute_0_63, plain, (p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_48, refute_0_62])). cnf(refute_0_64, plain, (p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_63, refute_0_54])). cnf(refute_0_65, plain, (p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_64, refute_0_59])). cnf(refute_0_66, plain, (~ p102(Y) | ~ p104(skolemFOFtoCNF_X_26(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p103(Y)), inference(canonicalize, [], [normalize_0_24])). cnf(refute_0_67, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(subst, [], [refute_0_66 : [bind(Y, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))]])). cnf(refute_0_68, plain, (~ p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | ~ p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_67])). cnf(refute_0_69, plain, (~ p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), inference(resolve, [$cnf(p102(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_48, refute_0_68])). cnf(refute_0_70, plain, (~ p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_69, refute_0_54])). cnf(refute_0_71, plain, (r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_65, refute_0_70])). cnf(refute_0_72, plain, (~ r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), Z) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(subst, [], [refute_0_26 : [bind(X, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Y, $fot(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))]])). cnf(refute_0_73, plain, (~ r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), Z) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_55, refute_0_72])). cnf(refute_0_74, plain, (~ r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_73 : [bind(Z, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_75, plain, (r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_71, refute_0_74])). cnf(refute_0_76, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_75, refute_0_37])). cnf(refute_0_77, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_76 : [bind(X, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_78, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_77])). cnf(refute_0_79, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_78, refute_0_36])). cnf(refute_0_80, plain, (~ p103(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y) | p104(skolemFOFtoCNF_X_24(Y))), inference(canonicalize, [], [normalize_0_25])). cnf(refute_0_81, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(subst, [], [refute_0_80 : [bind(Y, $fot(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))]])). cnf(refute_0_82, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_58, refute_0_81])). cnf(refute_0_83, plain, (p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_64, refute_0_82])). cnf(refute_0_84, plain, (p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_83, refute_0_70])). cnf(refute_0_85, plain, (p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_84, refute_0_79])). cnf(refute_0_86, plain, (~ p103(Y) | ~ p105(skolemFOFtoCNF_X_24(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p104(Y)), inference(canonicalize, [], [normalize_0_26])). cnf(refute_0_87, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | ~ p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(subst, [], [refute_0_86 : [bind(Y, $fot(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))]])). cnf(refute_0_88, plain, (~ p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))) | ~ p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_58, refute_0_87])). cnf(refute_0_89, plain, (~ p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), inference(resolve, [$cnf(p103(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_64, refute_0_88])). cnf(refute_0_90, plain, (~ p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))], [refute_0_89, refute_0_70])). cnf(refute_0_91, plain, (r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_85, refute_0_90])). cnf(refute_0_92, plain, (~ r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), Z) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(subst, [], [refute_0_26 : [bind(X, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Y, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_93, plain, (~ r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), Z) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_75, refute_0_92])). cnf(refute_0_94, plain, (~ r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(subst, [], [refute_0_93 : [bind(Z, $fot(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))]])). cnf(refute_0_95, plain, (r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_91, refute_0_94])). cnf(refute_0_96, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_95, refute_0_34])). cnf(refute_0_97, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(subst, [], [refute_0_96 : [bind(X, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_98, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_97])). cnf(refute_0_99, plain, (~ p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_98, refute_0_33])). cnf(refute_0_100, plain, (~ p104(Y) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y) | p105(skolemFOFtoCNF_X_22(Y))), inference(canonicalize, [], [normalize_0_27])). cnf(refute_0_101, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_100 : [bind(Y, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_102, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_78, refute_0_101])). cnf(refute_0_103, plain, (p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_84, refute_0_102])). cnf(refute_0_104, plain, (p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_103, refute_0_90])). cnf(refute_0_105, plain, (p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_104, refute_0_99])). cnf(refute_0_106, plain, (~ p104(Y) | ~ p106(skolemFOFtoCNF_X_22(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p105(Y)), inference(canonicalize, [], [normalize_0_28])). cnf(refute_0_107, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | ~ p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(subst, [], [refute_0_106 : [bind(Y, $fot(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))]])). cnf(refute_0_108, plain, (~ p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))) | ~ p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_78, refute_0_107])). cnf(refute_0_109, plain, (~ p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))), inference(resolve, [$cnf(p104(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_84, refute_0_108])). cnf(refute_0_110, plain, (~ p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(p105(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))], [refute_0_109, refute_0_90])). cnf(refute_0_111, plain, (r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_105, refute_0_110])). cnf(refute_0_112, plain, (~ r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), Z) | ~ r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(subst, [], [refute_0_26 : [bind(X, $fot(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))), bind(Y, $fot(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))]])). cnf(refute_0_113, plain, (~ r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), Z) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), Z)), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_95, refute_0_112])). cnf(refute_0_114, plain, (~ r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(subst, [], [refute_0_113 : [bind(Z, $fot(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))]])). cnf(refute_0_115, plain, (r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))], [refute_0_111, refute_0_114])). cnf(refute_0_116, plain, (~ r1(X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)), skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))], [refute_0_115, refute_0_31])). cnf(refute_0_117, plain, (~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))) | r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(subst, [], [refute_0_116 : [bind(X, $fot(skolemFOFtoCNF_X))]])). cnf(refute_0_118, plain, (r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))], [refute_0_30, refute_0_117])). cnf(refute_0_119, plain, (p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))], [refute_0_118, refute_0_1])). cnf(refute_0_120, plain, (~ p105(Y) | ~ p7(skolemFOFtoCNF_X_20(Y)) | ~ r1(skolemFOFtoCNF_X, Y) | p106(Y)), inference(canonicalize, [], [normalize_0_29])). cnf(refute_0_121, plain, (~ p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | ~ p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | ~ r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(subst, [], [refute_0_120 : [bind(Y, $fot(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))]])). cnf(refute_0_122, plain, (~ p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))) | ~ p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(r1(skolemFOFtoCNF_X, skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_98, refute_0_121])). cnf(refute_0_123, plain, (~ p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))) | p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))), inference(resolve, [$cnf(p105(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_104, refute_0_122])). cnf(refute_0_124, plain, (~ p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))), inference(resolve, [$cnf(p106(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X)))))))], [refute_0_123, refute_0_110])). cnf(refute_0_125, plain, ($false), inference(resolve, [$cnf(p7(skolemFOFtoCNF_X_20(skolemFOFtoCNF_X_22(skolemFOFtoCNF_X_24(skolemFOFtoCNF_X_26(skolemFOFtoCNF_X_27(skolemFOFtoCNF_X_29(skolemFOFtoCNF_X))))))))], [refute_0_119, refute_0_124])). SZS output end CNFRefutation for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p WATCH: 0.89 CPU 0.93 WC FINAL WATCH: 0.89 CPU 0.93 WC