WATCH: 0.00 CPU 0.01 WC

WATCH: 2.93 CPU 3.02 WC
# Preprocessing time       : 0.010 s
# Problem is unsatisfiable (or provable), constructing proof object
# SZS status Theorem
# SZS output start CNFRefutation.
fof(1, axiom,![X1]:![X2]:![X3]:((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3)),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p', transitivity)).
fof(2, conjecture,~(?[X1]:~((~(((![X2]:(~(r1(X1,X2))|((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:(~(((~(p15(X1))&~(p115(X1)))&p114(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((p15(X1)&p114(X1))&~(p115(X1))))|~(r1(X2,X1)))))|~((p113(X2)&~(p114(X2)))))&((~(![X1]:(~(((p13(X1)&~(p113(X1)))&p112(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p13(X1))&~(p113(X1)))&p112(X1)))|~(r1(X2,X1)))))|~((p111(X2)&~(p112(X2))))))&(~((~(p106(X2))&p105(X2)))|(~(![X1]:(~(((~(p107(X1))&p106(X1))&p7(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p107(X1))&p106(X1))&~(p7(X1)))))))))&((~(![X1]:(~(((~(p105(X1))&p104(X1))&~(p5(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p104(X1)&~(p105(X1)))&p5(X1))))))|~((p103(X2)&~(p104(X2))))))&(~((~(p103(X2))&p102(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(((~(p4(X1))&~(p104(X1)))&p103(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p3(X1))&~(p103(X1)))&p102(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p102(X1)&~(p103(X1)))&p3(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&p101(X1))&~(p102(X1))))))&~(![X1]:(~(((p2(X1)&p101(X1))&~(p102(X1))))|~(r1(X2,X1)))))|~((p100(X2)&~(p101(X2))))))&(((![X1]:((~(p16(X1))|~(p115(X1)))|~(r1(X2,X1)))|p16(X2))&(![X1]:((~(p115(X1))|p16(X1))|~(r1(X2,X1)))|~(p16(X2))))|~(p115(X2))))&(~(p114(X2))|((p15(X2)|![X1]:((~(r1(X2,X1))|~(p15(X1)))|~(p114(X1))))&(~(p15(X2))|![X1]:((~(r1(X2,X1))|p15(X1))|~(p114(X1)))))))&(~(p113(X2))|((p14(X2)|![X1]:((~(p113(X1))|~(p14(X1)))|~(r1(X2,X1))))&(~(p14(X2))|![X1]:((~(p113(X1))|p14(X1))|~(r1(X2,X1)))))))&(((~(p13(X2))|![X1]:((~(r1(X2,X1))|p13(X1))|~(p112(X1))))&(p13(X2)|![X1]:((~(p112(X1))|~(p13(X1)))|~(r1(X2,X1)))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p100(X1)))|~(p1(X1)))|p1(X2))&(~(p1(X2))|![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))))|~(p100(X2))))&(p113(X2)|~(p114(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(~(p108(X2))|p107(X2)))&(p106(X2)|~(p107(X2))))&(p104(X2)|~(p105(X2))))&(~(p103(X2))|p102(X2)))&(p100(X2)|~(p101(X2))))&(p101(X2)|~(p102(X2))))&(p103(X2)|~(p104(X2))))&(p105(X2)|~(p106(X2))))&(~(p113(X2))|p112(X2)))&(p114(X2)|~(p115(X2))))&(p115(X2)|~(p116(X2))))&(((~(p2(X2))|![X1]:((~(p101(X1))|p2(X1))|~(r1(X2,X1))))&(p2(X2)|![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))))|~(p101(X2))))&(((![X1]:((p3(X1)|~(p102(X1)))|~(r1(X2,X1)))|~(p3(X2)))&(![X1]:((~(p3(X1))|~(p102(X1)))|~(r1(X2,X1)))|p3(X2)))|~(p102(X2))))&(~(p103(X2))|((p4(X2)|![X1]:((~(p103(X1))|~(p4(X1)))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))))&(((![X1]:((p5(X1)|~(p104(X1)))|~(r1(X2,X1)))|~(p5(X2)))&(p5(X2)|![X1]:((~(r1(X2,X1))|~(p104(X1)))|~(p5(X1)))))|~(p104(X2))))&(((~(p6(X2))|![X1]:((~(p105(X1))|p6(X1))|~(r1(X2,X1))))&(![X1]:((~(p105(X1))|~(p6(X1)))|~(r1(X2,X1)))|p6(X2)))|~(p105(X2))))&(~(p106(X2))|((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|~(p106(X1)))|p7(X1))|~(p7(X2))))))&(((p8(X2)|![X1]:((~(p8(X1))|~(p107(X1)))|~(r1(X2,X1))))&(~(p8(X2))|![X1]:((~(r1(X2,X1))|~(p107(X1)))|p8(X1))))|~(p107(X2))))&(~(p108(X2))|((~(p9(X2))|![X1]:((~(p108(X1))|p9(X1))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|~(p108(X1)))|~(p9(X1)))|p9(X2)))))&(((p10(X2)|![X1]:((~(p109(X1))|~(p10(X1)))|~(r1(X2,X1))))&(~(p10(X2))|![X1]:((~(r1(X2,X1))|~(p109(X1)))|p10(X1))))|~(p109(X2))))&(~(p110(X2))|((![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2)))&(p11(X2)|![X1]:((~(p11(X1))|~(p110(X1)))|~(r1(X2,X1)))))))&(~(p111(X2))|((p12(X2)|![X1]:((~(p12(X1))|~(p111(X1)))|~(r1(X2,X1))))&(~(p12(X2))|![X1]:((p12(X1)|~(p111(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p6(X1))&p105(X1))&~(p106(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&p105(X1))&~(p106(X1)))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&(~((p107(X2)&~(p108(X2))))|(~(![X1]:(~(r1(X2,X1))|~(((~(p109(X1))&p108(X1))&p9(X1)))))&~(![X1]:(~(((p108(X1)&~(p109(X1)))&~(p9(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((p109(X1)&~(p110(X1)))&~(p10(X1))))|~(r1(X2,X1))))&~(![X1]:(~(((p109(X1)&~(p110(X1)))&p10(X1)))|~(r1(X2,X1)))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(((p11(X1)&~(p111(X1)))&p110(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p111(X1))&p110(X1))&~(p11(X1)))))))|~((~(p110(X2))&p109(X2)))))&(~((p110(X2)&~(p111(X2))))|(~(![X1]:(~(((~(p112(X1))&p111(X1))&p12(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p112(X1))&p111(X1))&~(p12(X1))))|~(r1(X2,X1)))))))&(~((~(p113(X2))&p112(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p113(X1)&~(p114(X1)))&p14(X1)))))&~(![X1]:(~(((p113(X1)&~(p114(X1)))&~(p14(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p116(X1))&p115(X1))&~(p16(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p116(X1))&p115(X1))&p16(X1))))))|~((~(p115(X2))&p114(X2))))))&p100(X1))&~(p101(X1))))|~(![X2]:(~(r1(X1,X2))|p7(X2)))))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p', main)).
fof(3, axiom,![X1]:r1(X1,X1),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p', reflexivity)).
fof(4, negated_conjecture,~(~(?[X1]:~((~(((![X2]:(~(r1(X1,X2))|((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:(~(((~(p15(X1))&~(p115(X1)))&p114(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((p15(X1)&p114(X1))&~(p115(X1))))|~(r1(X2,X1)))))|~((p113(X2)&~(p114(X2)))))&((~(![X1]:(~(((p13(X1)&~(p113(X1)))&p112(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p13(X1))&~(p113(X1)))&p112(X1)))|~(r1(X2,X1)))))|~((p111(X2)&~(p112(X2))))))&(~((~(p106(X2))&p105(X2)))|(~(![X1]:(~(((~(p107(X1))&p106(X1))&p7(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p107(X1))&p106(X1))&~(p7(X1)))))))))&((~(![X1]:(~(((~(p105(X1))&p104(X1))&~(p5(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p104(X1)&~(p105(X1)))&p5(X1))))))|~((p103(X2)&~(p104(X2))))))&(~((~(p103(X2))&p102(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(((~(p4(X1))&~(p104(X1)))&p103(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p3(X1))&~(p103(X1)))&p102(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p102(X1)&~(p103(X1)))&p3(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&p101(X1))&~(p102(X1))))))&~(![X1]:(~(((p2(X1)&p101(X1))&~(p102(X1))))|~(r1(X2,X1)))))|~((p100(X2)&~(p101(X2))))))&(((![X1]:((~(p16(X1))|~(p115(X1)))|~(r1(X2,X1)))|p16(X2))&(![X1]:((~(p115(X1))|p16(X1))|~(r1(X2,X1)))|~(p16(X2))))|~(p115(X2))))&(~(p114(X2))|((p15(X2)|![X1]:((~(r1(X2,X1))|~(p15(X1)))|~(p114(X1))))&(~(p15(X2))|![X1]:((~(r1(X2,X1))|p15(X1))|~(p114(X1)))))))&(~(p113(X2))|((p14(X2)|![X1]:((~(p113(X1))|~(p14(X1)))|~(r1(X2,X1))))&(~(p14(X2))|![X1]:((~(p113(X1))|p14(X1))|~(r1(X2,X1)))))))&(((~(p13(X2))|![X1]:((~(r1(X2,X1))|p13(X1))|~(p112(X1))))&(p13(X2)|![X1]:((~(p112(X1))|~(p13(X1)))|~(r1(X2,X1)))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p100(X1)))|~(p1(X1)))|p1(X2))&(~(p1(X2))|![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))))|~(p100(X2))))&(p113(X2)|~(p114(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(~(p108(X2))|p107(X2)))&(p106(X2)|~(p107(X2))))&(p104(X2)|~(p105(X2))))&(~(p103(X2))|p102(X2)))&(p100(X2)|~(p101(X2))))&(p101(X2)|~(p102(X2))))&(p103(X2)|~(p104(X2))))&(p105(X2)|~(p106(X2))))&(~(p113(X2))|p112(X2)))&(p114(X2)|~(p115(X2))))&(p115(X2)|~(p116(X2))))&(((~(p2(X2))|![X1]:((~(p101(X1))|p2(X1))|~(r1(X2,X1))))&(p2(X2)|![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))))|~(p101(X2))))&(((![X1]:((p3(X1)|~(p102(X1)))|~(r1(X2,X1)))|~(p3(X2)))&(![X1]:((~(p3(X1))|~(p102(X1)))|~(r1(X2,X1)))|p3(X2)))|~(p102(X2))))&(~(p103(X2))|((p4(X2)|![X1]:((~(p103(X1))|~(p4(X1)))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))))&(((![X1]:((p5(X1)|~(p104(X1)))|~(r1(X2,X1)))|~(p5(X2)))&(p5(X2)|![X1]:((~(r1(X2,X1))|~(p104(X1)))|~(p5(X1)))))|~(p104(X2))))&(((~(p6(X2))|![X1]:((~(p105(X1))|p6(X1))|~(r1(X2,X1))))&(![X1]:((~(p105(X1))|~(p6(X1)))|~(r1(X2,X1)))|p6(X2)))|~(p105(X2))))&(~(p106(X2))|((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|~(p106(X1)))|p7(X1))|~(p7(X2))))))&(((p8(X2)|![X1]:((~(p8(X1))|~(p107(X1)))|~(r1(X2,X1))))&(~(p8(X2))|![X1]:((~(r1(X2,X1))|~(p107(X1)))|p8(X1))))|~(p107(X2))))&(~(p108(X2))|((~(p9(X2))|![X1]:((~(p108(X1))|p9(X1))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|~(p108(X1)))|~(p9(X1)))|p9(X2)))))&(((p10(X2)|![X1]:((~(p109(X1))|~(p10(X1)))|~(r1(X2,X1))))&(~(p10(X2))|![X1]:((~(r1(X2,X1))|~(p109(X1)))|p10(X1))))|~(p109(X2))))&(~(p110(X2))|((![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2)))&(p11(X2)|![X1]:((~(p11(X1))|~(p110(X1)))|~(r1(X2,X1)))))))&(~(p111(X2))|((p12(X2)|![X1]:((~(p12(X1))|~(p111(X1)))|~(r1(X2,X1))))&(~(p12(X2))|![X1]:((p12(X1)|~(p111(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p6(X1))&p105(X1))&~(p106(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&p105(X1))&~(p106(X1)))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&(~((p107(X2)&~(p108(X2))))|(~(![X1]:(~(r1(X2,X1))|~(((~(p109(X1))&p108(X1))&p9(X1)))))&~(![X1]:(~(((p108(X1)&~(p109(X1)))&~(p9(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((p109(X1)&~(p110(X1)))&~(p10(X1))))|~(r1(X2,X1))))&~(![X1]:(~(((p109(X1)&~(p110(X1)))&p10(X1)))|~(r1(X2,X1)))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(((p11(X1)&~(p111(X1)))&p110(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p111(X1))&p110(X1))&~(p11(X1)))))))|~((~(p110(X2))&p109(X2)))))&(~((p110(X2)&~(p111(X2))))|(~(![X1]:(~(((~(p112(X1))&p111(X1))&p12(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p112(X1))&p111(X1))&~(p12(X1))))|~(r1(X2,X1)))))))&(~((~(p113(X2))&p112(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p113(X1)&~(p114(X1)))&p14(X1)))))&~(![X1]:(~(((p113(X1)&~(p114(X1)))&~(p14(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p116(X1))&p115(X1))&~(p16(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p116(X1))&p115(X1))&p16(X1))))))|~((~(p115(X2))&p114(X2))))))&p100(X1))&~(p101(X1))))|~(![X2]:(~(r1(X1,X2))|p7(X2))))))),inference(assume_negation,[status(cth)],[2])).
fof(5, negated_conjecture,~(~(?[X1]:~((~(((![X2]:(~(r1(X1,X2))|((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:(~(((~(p15(X1))&~(p115(X1)))&p114(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((p15(X1)&p114(X1))&~(p115(X1))))|~(r1(X2,X1)))))|~((p113(X2)&~(p114(X2)))))&((~(![X1]:(~(((p13(X1)&~(p113(X1)))&p112(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p13(X1))&~(p113(X1)))&p112(X1)))|~(r1(X2,X1)))))|~((p111(X2)&~(p112(X2))))))&(~((~(p106(X2))&p105(X2)))|(~(![X1]:(~(((~(p107(X1))&p106(X1))&p7(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p107(X1))&p106(X1))&~(p7(X1)))))))))&((~(![X1]:(~(((~(p105(X1))&p104(X1))&~(p5(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p104(X1)&~(p105(X1)))&p5(X1))))))|~((p103(X2)&~(p104(X2))))))&(~((~(p103(X2))&p102(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(((~(p4(X1))&~(p104(X1)))&p103(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p3(X1))&~(p103(X1)))&p102(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p102(X1)&~(p103(X1)))&p3(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&p101(X1))&~(p102(X1))))))&~(![X1]:(~(((p2(X1)&p101(X1))&~(p102(X1))))|~(r1(X2,X1)))))|~((p100(X2)&~(p101(X2))))))&(((![X1]:((~(p16(X1))|~(p115(X1)))|~(r1(X2,X1)))|p16(X2))&(![X1]:((~(p115(X1))|p16(X1))|~(r1(X2,X1)))|~(p16(X2))))|~(p115(X2))))&(~(p114(X2))|((p15(X2)|![X1]:((~(r1(X2,X1))|~(p15(X1)))|~(p114(X1))))&(~(p15(X2))|![X1]:((~(r1(X2,X1))|p15(X1))|~(p114(X1)))))))&(~(p113(X2))|((p14(X2)|![X1]:((~(p113(X1))|~(p14(X1)))|~(r1(X2,X1))))&(~(p14(X2))|![X1]:((~(p113(X1))|p14(X1))|~(r1(X2,X1)))))))&(((~(p13(X2))|![X1]:((~(r1(X2,X1))|p13(X1))|~(p112(X1))))&(p13(X2)|![X1]:((~(p112(X1))|~(p13(X1)))|~(r1(X2,X1)))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p100(X1)))|~(p1(X1)))|p1(X2))&(~(p1(X2))|![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))))|~(p100(X2))))&(p113(X2)|~(p114(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(~(p108(X2))|p107(X2)))&(p106(X2)|~(p107(X2))))&(p104(X2)|~(p105(X2))))&(~(p103(X2))|p102(X2)))&(p100(X2)|~(p101(X2))))&(p101(X2)|~(p102(X2))))&(p103(X2)|~(p104(X2))))&(p105(X2)|~(p106(X2))))&(~(p113(X2))|p112(X2)))&(p114(X2)|~(p115(X2))))&(p115(X2)|~(p116(X2))))&(((~(p2(X2))|![X1]:((~(p101(X1))|p2(X1))|~(r1(X2,X1))))&(p2(X2)|![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))))|~(p101(X2))))&(((![X1]:((p3(X1)|~(p102(X1)))|~(r1(X2,X1)))|~(p3(X2)))&(![X1]:((~(p3(X1))|~(p102(X1)))|~(r1(X2,X1)))|p3(X2)))|~(p102(X2))))&(~(p103(X2))|((p4(X2)|![X1]:((~(p103(X1))|~(p4(X1)))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))))&(((![X1]:((p5(X1)|~(p104(X1)))|~(r1(X2,X1)))|~(p5(X2)))&(p5(X2)|![X1]:((~(r1(X2,X1))|~(p104(X1)))|~(p5(X1)))))|~(p104(X2))))&(((~(p6(X2))|![X1]:((~(p105(X1))|p6(X1))|~(r1(X2,X1))))&(![X1]:((~(p105(X1))|~(p6(X1)))|~(r1(X2,X1)))|p6(X2)))|~(p105(X2))))&(~(p106(X2))|((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|~(p106(X1)))|p7(X1))|~(p7(X2))))))&(((p8(X2)|![X1]:((~(p8(X1))|~(p107(X1)))|~(r1(X2,X1))))&(~(p8(X2))|![X1]:((~(r1(X2,X1))|~(p107(X1)))|p8(X1))))|~(p107(X2))))&(~(p108(X2))|((~(p9(X2))|![X1]:((~(p108(X1))|p9(X1))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|~(p108(X1)))|~(p9(X1)))|p9(X2)))))&(((p10(X2)|![X1]:((~(p109(X1))|~(p10(X1)))|~(r1(X2,X1))))&(~(p10(X2))|![X1]:((~(r1(X2,X1))|~(p109(X1)))|p10(X1))))|~(p109(X2))))&(~(p110(X2))|((![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2)))&(p11(X2)|![X1]:((~(p11(X1))|~(p110(X1)))|~(r1(X2,X1)))))))&(~(p111(X2))|((p12(X2)|![X1]:((~(p12(X1))|~(p111(X1)))|~(r1(X2,X1))))&(~(p12(X2))|![X1]:((p12(X1)|~(p111(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p6(X1))&p105(X1))&~(p106(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&p105(X1))&~(p106(X1)))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&(~((p107(X2)&~(p108(X2))))|(~(![X1]:(~(r1(X2,X1))|~(((~(p109(X1))&p108(X1))&p9(X1)))))&~(![X1]:(~(((p108(X1)&~(p109(X1)))&~(p9(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((p109(X1)&~(p110(X1)))&~(p10(X1))))|~(r1(X2,X1))))&~(![X1]:(~(((p109(X1)&~(p110(X1)))&p10(X1)))|~(r1(X2,X1)))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(((p11(X1)&~(p111(X1)))&p110(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p111(X1))&p110(X1))&~(p11(X1)))))))|~((~(p110(X2))&p109(X2)))))&(~((p110(X2)&~(p111(X2))))|(~(![X1]:(~(((~(p112(X1))&p111(X1))&p12(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p112(X1))&p111(X1))&~(p12(X1))))|~(r1(X2,X1)))))))&(~((~(p113(X2))&p112(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p113(X1)&~(p114(X1)))&p14(X1)))))&~(![X1]:(~(((p113(X1)&~(p114(X1)))&~(p14(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p116(X1))&p115(X1))&~(p16(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p116(X1))&p115(X1))&p16(X1))))))|~((~(p115(X2))&p114(X2))))))&p100(X1))&~(p101(X1))))|~(![X2]:(~(r1(X1,X2))|p7(X2))))))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
fof(6, plain,![X2]:(epred1_1(X2)=>((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:(~(((~(p15(X1))&~(p115(X1)))&p114(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((p15(X1)&p114(X1))&~(p115(X1))))|~(r1(X2,X1)))))|~((p113(X2)&~(p114(X2)))))&((~(![X1]:(~(((p13(X1)&~(p113(X1)))&p112(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p13(X1))&~(p113(X1)))&p112(X1)))|~(r1(X2,X1)))))|~((p111(X2)&~(p112(X2))))))&(~((~(p106(X2))&p105(X2)))|(~(![X1]:(~(((~(p107(X1))&p106(X1))&p7(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p107(X1))&p106(X1))&~(p7(X1)))))))))&((~(![X1]:(~(((~(p105(X1))&p104(X1))&~(p5(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p104(X1)&~(p105(X1)))&p5(X1))))))|~((p103(X2)&~(p104(X2))))))&(~((~(p103(X2))&p102(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(((~(p4(X1))&~(p104(X1)))&p103(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p3(X1))&~(p103(X1)))&p102(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p102(X1)&~(p103(X1)))&p3(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&p101(X1))&~(p102(X1))))))&~(![X1]:(~(((p2(X1)&p101(X1))&~(p102(X1))))|~(r1(X2,X1)))))|~((p100(X2)&~(p101(X2))))))&(((![X1]:((~(p16(X1))|~(p115(X1)))|~(r1(X2,X1)))|p16(X2))&(![X1]:((~(p115(X1))|p16(X1))|~(r1(X2,X1)))|~(p16(X2))))|~(p115(X2))))&(~(p114(X2))|((p15(X2)|![X1]:((~(r1(X2,X1))|~(p15(X1)))|~(p114(X1))))&(~(p15(X2))|![X1]:((~(r1(X2,X1))|p15(X1))|~(p114(X1)))))))&(~(p113(X2))|((p14(X2)|![X1]:((~(p113(X1))|~(p14(X1)))|~(r1(X2,X1))))&(~(p14(X2))|![X1]:((~(p113(X1))|p14(X1))|~(r1(X2,X1)))))))&(((~(p13(X2))|![X1]:((~(r1(X2,X1))|p13(X1))|~(p112(X1))))&(p13(X2)|![X1]:((~(p112(X1))|~(p13(X1)))|~(r1(X2,X1)))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p100(X1)))|~(p1(X1)))|p1(X2))&(~(p1(X2))|![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))))|~(p100(X2))))&(p113(X2)|~(p114(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(~(p108(X2))|p107(X2)))&(p106(X2)|~(p107(X2))))&(p104(X2)|~(p105(X2))))&(~(p103(X2))|p102(X2)))&(p100(X2)|~(p101(X2))))&(p101(X2)|~(p102(X2))))&(p103(X2)|~(p104(X2))))&(p105(X2)|~(p106(X2))))&(~(p113(X2))|p112(X2)))&(p114(X2)|~(p115(X2))))&(p115(X2)|~(p116(X2))))&(((~(p2(X2))|![X1]:((~(p101(X1))|p2(X1))|~(r1(X2,X1))))&(p2(X2)|![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))))|~(p101(X2))))&(((![X1]:((p3(X1)|~(p102(X1)))|~(r1(X2,X1)))|~(p3(X2)))&(![X1]:((~(p3(X1))|~(p102(X1)))|~(r1(X2,X1)))|p3(X2)))|~(p102(X2))))&(~(p103(X2))|((p4(X2)|![X1]:((~(p103(X1))|~(p4(X1)))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))))&(((![X1]:((p5(X1)|~(p104(X1)))|~(r1(X2,X1)))|~(p5(X2)))&(p5(X2)|![X1]:((~(r1(X2,X1))|~(p104(X1)))|~(p5(X1)))))|~(p104(X2))))&(((~(p6(X2))|![X1]:((~(p105(X1))|p6(X1))|~(r1(X2,X1))))&(![X1]:((~(p105(X1))|~(p6(X1)))|~(r1(X2,X1)))|p6(X2)))|~(p105(X2))))&(~(p106(X2))|((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|~(p106(X1)))|p7(X1))|~(p7(X2))))))&(((p8(X2)|![X1]:((~(p8(X1))|~(p107(X1)))|~(r1(X2,X1))))&(~(p8(X2))|![X1]:((~(r1(X2,X1))|~(p107(X1)))|p8(X1))))|~(p107(X2))))&(~(p108(X2))|((~(p9(X2))|![X1]:((~(p108(X1))|p9(X1))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|~(p108(X1)))|~(p9(X1)))|p9(X2)))))&(((p10(X2)|![X1]:((~(p109(X1))|~(p10(X1)))|~(r1(X2,X1))))&(~(p10(X2))|![X1]:((~(r1(X2,X1))|~(p109(X1)))|p10(X1))))|~(p109(X2))))&(~(p110(X2))|((![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2)))&(p11(X2)|![X1]:((~(p11(X1))|~(p110(X1)))|~(r1(X2,X1)))))))&(~(p111(X2))|((p12(X2)|![X1]:((~(p12(X1))|~(p111(X1)))|~(r1(X2,X1))))&(~(p12(X2))|![X1]:((p12(X1)|~(p111(X1)))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p6(X1))&p105(X1))&~(p106(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&p105(X1))&~(p106(X1)))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&(~((p107(X2)&~(p108(X2))))|(~(![X1]:(~(r1(X2,X1))|~(((~(p109(X1))&p108(X1))&p9(X1)))))&~(![X1]:(~(((p108(X1)&~(p109(X1)))&~(p9(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((p109(X1)&~(p110(X1)))&~(p10(X1))))|~(r1(X2,X1))))&~(![X1]:(~(((p109(X1)&~(p110(X1)))&p10(X1)))|~(r1(X2,X1)))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(((p11(X1)&~(p111(X1)))&p110(X1)))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p111(X1))&p110(X1))&~(p11(X1)))))))|~((~(p110(X2))&p109(X2)))))&(~((p110(X2)&~(p111(X2))))|(~(![X1]:(~(((~(p112(X1))&p111(X1))&p12(X1)))|~(r1(X2,X1))))&~(![X1]:(~(((~(p112(X1))&p111(X1))&~(p12(X1))))|~(r1(X2,X1)))))))&(~((~(p113(X2))&p112(X2)))|(~(![X1]:(~(r1(X2,X1))|~(((p113(X1)&~(p114(X1)))&p14(X1)))))&~(![X1]:(~(((p113(X1)&~(p114(X1)))&~(p14(X1))))|~(r1(X2,X1)))))))&((~(![X1]:(~(((~(p116(X1))&p115(X1))&~(p16(X1))))|~(r1(X2,X1))))&~(![X1]:(~(r1(X2,X1))|~(((~(p116(X1))&p115(X1))&p16(X1))))))|~((~(p115(X2))&p114(X2)))))),introduced(definition)).
fof(7, negated_conjecture,~(~(?[X1]:~((~(((![X2]:(~(r1(X1,X2))|epred1_1(X2))&p100(X1))&~(p101(X1))))|~(![X2]:(~(r1(X1,X2))|p7(X2))))))),inference(apply_def,[status(esa)],[5,6,theory(equality)])).
fof(8, plain,![X1]:![X2]:![X3]:((~(r1(X1,X2))|~(r1(X2,X3)))|r1(X1,X3)),inference(fof_nnf,[status(thm)],[1])).
fof(9, plain,![X4]:![X5]:![X6]:((~(r1(X4,X5))|~(r1(X5,X6)))|r1(X4,X6)),inference(variable_rename,[status(thm)],[8])).
cnf(10,plain,(r1(X1,X2)|~r1(X3,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[9])).
fof(11, negated_conjecture,?[X1]:(((![X2]:(~(r1(X1,X2))|epred1_1(X2))&p100(X1))&~(p101(X1)))&![X2]:(~(r1(X1,X2))|p7(X2))),inference(fof_nnf,[status(thm)],[7])).
fof(12, negated_conjecture,?[X3]:(((![X4]:(~(r1(X3,X4))|epred1_1(X4))&p100(X3))&~(p101(X3)))&![X5]:(~(r1(X3,X5))|p7(X5))),inference(variable_rename,[status(thm)],[11])).
fof(13, negated_conjecture,(((![X4]:(~(r1(esk1_0,X4))|epred1_1(X4))&p100(esk1_0))&~(p101(esk1_0)))&![X5]:(~(r1(esk1_0,X5))|p7(X5))),inference(skolemize,[status(esa)],[12])).
fof(14, negated_conjecture,![X4]:![X5]:((((~(r1(esk1_0,X4))|epred1_1(X4))&p100(esk1_0))&~(p101(esk1_0)))&(~(r1(esk1_0,X5))|p7(X5))),inference(shift_quantors,[status(thm)],[13])).
cnf(15,negated_conjecture,(p7(X1)|~r1(esk1_0,X1)),inference(split_conjunct,[status(thm)],[14])).
cnf(16,negated_conjecture,(~p101(esk1_0)),inference(split_conjunct,[status(thm)],[14])).
cnf(17,negated_conjecture,(p100(esk1_0)),inference(split_conjunct,[status(thm)],[14])).
cnf(18,negated_conjecture,(epred1_1(X1)|~r1(esk1_0,X1)),inference(split_conjunct,[status(thm)],[14])).
fof(19, plain,![X2]:r1(X2,X2),inference(variable_rename,[status(thm)],[3])).
cnf(20,plain,(r1(X1,X1)),inference(split_conjunct,[status(thm)],[19])).
fof(21, plain,![X2]:(~(epred1_1(X2))|((((((((((((((((((((((((((((((((((((((((((((((((?[X1]:(((~(p15(X1))&~(p115(X1)))&p114(X1))&r1(X2,X1))&?[X1]:(((p15(X1)&p114(X1))&~(p115(X1)))&r1(X2,X1)))|(~(p113(X2))|p114(X2)))&((?[X1]:(((p13(X1)&~(p113(X1)))&p112(X1))&r1(X2,X1))&?[X1]:(((~(p13(X1))&~(p113(X1)))&p112(X1))&r1(X2,X1)))|(~(p111(X2))|p112(X2))))&((p106(X2)|~(p105(X2)))|(?[X1]:(((~(p107(X1))&p106(X1))&p7(X1))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((~(p107(X1))&p106(X1))&~(p7(X1)))))))&((?[X1]:(((~(p105(X1))&p104(X1))&~(p5(X1)))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((p104(X1)&~(p105(X1)))&p5(X1))))|(~(p103(X2))|p104(X2))))&((p103(X2)|~(p102(X2)))|(?[X1]:(r1(X2,X1)&((p4(X1)&~(p104(X1)))&p103(X1)))&?[X1]:(((~(p4(X1))&~(p104(X1)))&p103(X1))&r1(X2,X1)))))&((?[X1]:(((~(p3(X1))&~(p103(X1)))&p102(X1))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((p102(X1)&~(p103(X1)))&p3(X1))))|(p102(X2)|~(p101(X2)))))&((?[X1]:(r1(X2,X1)&((~(p2(X1))&p101(X1))&~(p102(X1))))&?[X1]:(((p2(X1)&p101(X1))&~(p102(X1)))&r1(X2,X1)))|(~(p100(X2))|p101(X2))))&(((![X1]:((~(p16(X1))|~(p115(X1)))|~(r1(X2,X1)))|p16(X2))&(![X1]:((~(p115(X1))|p16(X1))|~(r1(X2,X1)))|~(p16(X2))))|~(p115(X2))))&(~(p114(X2))|((p15(X2)|![X1]:((~(r1(X2,X1))|~(p15(X1)))|~(p114(X1))))&(~(p15(X2))|![X1]:((~(r1(X2,X1))|p15(X1))|~(p114(X1)))))))&(~(p113(X2))|((p14(X2)|![X1]:((~(p113(X1))|~(p14(X1)))|~(r1(X2,X1))))&(~(p14(X2))|![X1]:((~(p113(X1))|p14(X1))|~(r1(X2,X1)))))))&(((~(p13(X2))|![X1]:((~(r1(X2,X1))|p13(X1))|~(p112(X1))))&(p13(X2)|![X1]:((~(p112(X1))|~(p13(X1)))|~(r1(X2,X1)))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p100(X1)))|~(p1(X1)))|p1(X2))&(~(p1(X2))|![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))))|~(p100(X2))))&(p113(X2)|~(p114(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(~(p108(X2))|p107(X2)))&(p106(X2)|~(p107(X2))))&(p104(X2)|~(p105(X2))))&(~(p103(X2))|p102(X2)))&(p100(X2)|~(p101(X2))))&(p101(X2)|~(p102(X2))))&(p103(X2)|~(p104(X2))))&(p105(X2)|~(p106(X2))))&(~(p113(X2))|p112(X2)))&(p114(X2)|~(p115(X2))))&(p115(X2)|~(p116(X2))))&(((~(p2(X2))|![X1]:((~(p101(X1))|p2(X1))|~(r1(X2,X1))))&(p2(X2)|![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))))|~(p101(X2))))&(((![X1]:((p3(X1)|~(p102(X1)))|~(r1(X2,X1)))|~(p3(X2)))&(![X1]:((~(p3(X1))|~(p102(X1)))|~(r1(X2,X1)))|p3(X2)))|~(p102(X2))))&(~(p103(X2))|((p4(X2)|![X1]:((~(p103(X1))|~(p4(X1)))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))))&(((![X1]:((p5(X1)|~(p104(X1)))|~(r1(X2,X1)))|~(p5(X2)))&(p5(X2)|![X1]:((~(r1(X2,X1))|~(p104(X1)))|~(p5(X1)))))|~(p104(X2))))&(((~(p6(X2))|![X1]:((~(p105(X1))|p6(X1))|~(r1(X2,X1))))&(![X1]:((~(p105(X1))|~(p6(X1)))|~(r1(X2,X1)))|p6(X2)))|~(p105(X2))))&(~(p106(X2))|((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|~(p106(X1)))|p7(X1))|~(p7(X2))))))&(((p8(X2)|![X1]:((~(p8(X1))|~(p107(X1)))|~(r1(X2,X1))))&(~(p8(X2))|![X1]:((~(r1(X2,X1))|~(p107(X1)))|p8(X1))))|~(p107(X2))))&(~(p108(X2))|((~(p9(X2))|![X1]:((~(p108(X1))|p9(X1))|~(r1(X2,X1))))&(![X1]:((~(r1(X2,X1))|~(p108(X1)))|~(p9(X1)))|p9(X2)))))&(((p10(X2)|![X1]:((~(p109(X1))|~(p10(X1)))|~(r1(X2,X1))))&(~(p10(X2))|![X1]:((~(r1(X2,X1))|~(p109(X1)))|p10(X1))))|~(p109(X2))))&(~(p110(X2))|((![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2)))&(p11(X2)|![X1]:((~(p11(X1))|~(p110(X1)))|~(r1(X2,X1)))))))&(~(p111(X2))|((p12(X2)|![X1]:((~(p12(X1))|~(p111(X1)))|~(r1(X2,X1))))&(~(p12(X2))|![X1]:((p12(X1)|~(p111(X1)))|~(r1(X2,X1)))))))&((?[X1]:(((~(p6(X1))&p105(X1))&~(p106(X1)))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((p6(X1)&p105(X1))&~(p106(X1)))))|(p105(X2)|~(p104(X2)))))&((?[X1]:(r1(X2,X1)&((~(p8(X1))&~(p108(X1)))&p107(X1)))&?[X1]:(r1(X2,X1)&((p8(X1)&~(p108(X1)))&p107(X1))))|(p107(X2)|~(p106(X2)))))&((~(p107(X2))|p108(X2))|(?[X1]:(r1(X2,X1)&((~(p109(X1))&p108(X1))&p9(X1)))&?[X1]:(((p108(X1)&~(p109(X1)))&~(p9(X1)))&r1(X2,X1)))))&((?[X1]:(((p109(X1)&~(p110(X1)))&~(p10(X1)))&r1(X2,X1))&?[X1]:(((p109(X1)&~(p110(X1)))&p10(X1))&r1(X2,X1)))|(p109(X2)|~(p108(X2)))))&((?[X1]:(((p11(X1)&~(p111(X1)))&p110(X1))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((~(p111(X1))&p110(X1))&~(p11(X1)))))|(p110(X2)|~(p109(X2)))))&((~(p110(X2))|p111(X2))|(?[X1]:(((~(p112(X1))&p111(X1))&p12(X1))&r1(X2,X1))&?[X1]:(((~(p112(X1))&p111(X1))&~(p12(X1)))&r1(X2,X1)))))&((p113(X2)|~(p112(X2)))|(?[X1]:(r1(X2,X1)&((p113(X1)&~(p114(X1)))&p14(X1)))&?[X1]:(((p113(X1)&~(p114(X1)))&~(p14(X1)))&r1(X2,X1)))))&((?[X1]:(((~(p116(X1))&p115(X1))&~(p16(X1)))&r1(X2,X1))&?[X1]:(r1(X2,X1)&((~(p116(X1))&p115(X1))&p16(X1))))|(p115(X2)|~(p114(X2)))))),inference(fof_nnf,[status(thm)],[6])).
fof(22, plain,![X3]:(~(epred1_1(X3))|((((((((((((((((((((((((((((((((((((((((((((((((?[X4]:(((~(p15(X4))&~(p115(X4)))&p114(X4))&r1(X3,X4))&?[X5]:(((p15(X5)&p114(X5))&~(p115(X5)))&r1(X3,X5)))|(~(p113(X3))|p114(X3)))&((?[X6]:(((p13(X6)&~(p113(X6)))&p112(X6))&r1(X3,X6))&?[X7]:(((~(p13(X7))&~(p113(X7)))&p112(X7))&r1(X3,X7)))|(~(p111(X3))|p112(X3))))&((p106(X3)|~(p105(X3)))|(?[X8]:(((~(p107(X8))&p106(X8))&p7(X8))&r1(X3,X8))&?[X9]:(r1(X3,X9)&((~(p107(X9))&p106(X9))&~(p7(X9)))))))&((?[X10]:(((~(p105(X10))&p104(X10))&~(p5(X10)))&r1(X3,X10))&?[X11]:(r1(X3,X11)&((p104(X11)&~(p105(X11)))&p5(X11))))|(~(p103(X3))|p104(X3))))&((p103(X3)|~(p102(X3)))|(?[X12]:(r1(X3,X12)&((p4(X12)&~(p104(X12)))&p103(X12)))&?[X13]:(((~(p4(X13))&~(p104(X13)))&p103(X13))&r1(X3,X13)))))&((?[X14]:(((~(p3(X14))&~(p103(X14)))&p102(X14))&r1(X3,X14))&?[X15]:(r1(X3,X15)&((p102(X15)&~(p103(X15)))&p3(X15))))|(p102(X3)|~(p101(X3)))))&((?[X16]:(r1(X3,X16)&((~(p2(X16))&p101(X16))&~(p102(X16))))&?[X17]:(((p2(X17)&p101(X17))&~(p102(X17)))&r1(X3,X17)))|(~(p100(X3))|p101(X3))))&(((![X18]:((~(p16(X18))|~(p115(X18)))|~(r1(X3,X18)))|p16(X3))&(![X19]:((~(p115(X19))|p16(X19))|~(r1(X3,X19)))|~(p16(X3))))|~(p115(X3))))&(~(p114(X3))|((p15(X3)|![X20]:((~(r1(X3,X20))|~(p15(X20)))|~(p114(X20))))&(~(p15(X3))|![X21]:((~(r1(X3,X21))|p15(X21))|~(p114(X21)))))))&(~(p113(X3))|((p14(X3)|![X22]:((~(p113(X22))|~(p14(X22)))|~(r1(X3,X22))))&(~(p14(X3))|![X23]:((~(p113(X23))|p14(X23))|~(r1(X3,X23)))))))&(((~(p13(X3))|![X24]:((~(r1(X3,X24))|p13(X24))|~(p112(X24))))&(p13(X3)|![X25]:((~(p112(X25))|~(p13(X25)))|~(r1(X3,X25)))))|~(p112(X3))))&(((![X26]:((~(r1(X3,X26))|~(p100(X26)))|~(p1(X26)))|p1(X3))&(~(p1(X3))|![X27]:((~(r1(X3,X27))|p1(X27))|~(p100(X27)))))|~(p100(X3))))&(p113(X3)|~(p114(X3))))&(p111(X3)|~(p112(X3))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(~(p108(X3))|p107(X3)))&(p106(X3)|~(p107(X3))))&(p104(X3)|~(p105(X3))))&(~(p103(X3))|p102(X3)))&(p100(X3)|~(p101(X3))))&(p101(X3)|~(p102(X3))))&(p103(X3)|~(p104(X3))))&(p105(X3)|~(p106(X3))))&(~(p113(X3))|p112(X3)))&(p114(X3)|~(p115(X3))))&(p115(X3)|~(p116(X3))))&(((~(p2(X3))|![X28]:((~(p101(X28))|p2(X28))|~(r1(X3,X28))))&(p2(X3)|![X29]:((~(r1(X3,X29))|~(p2(X29)))|~(p101(X29)))))|~(p101(X3))))&(((![X30]:((p3(X30)|~(p102(X30)))|~(r1(X3,X30)))|~(p3(X3)))&(![X31]:((~(p3(X31))|~(p102(X31)))|~(r1(X3,X31)))|p3(X3)))|~(p102(X3))))&(~(p103(X3))|((p4(X3)|![X32]:((~(p103(X32))|~(p4(X32)))|~(r1(X3,X32))))&(![X33]:((~(r1(X3,X33))|p4(X33))|~(p103(X33)))|~(p4(X3))))))&(((![X34]:((p5(X34)|~(p104(X34)))|~(r1(X3,X34)))|~(p5(X3)))&(p5(X3)|![X35]:((~(r1(X3,X35))|~(p104(X35)))|~(p5(X35)))))|~(p104(X3))))&(((~(p6(X3))|![X36]:((~(p105(X36))|p6(X36))|~(r1(X3,X36))))&(![X37]:((~(p105(X37))|~(p6(X37)))|~(r1(X3,X37)))|p6(X3)))|~(p105(X3))))&(~(p106(X3))|((![X38]:((~(r1(X3,X38))|~(p7(X38)))|~(p106(X38)))|p7(X3))&(![X39]:((~(r1(X3,X39))|~(p106(X39)))|p7(X39))|~(p7(X3))))))&(((p8(X3)|![X40]:((~(p8(X40))|~(p107(X40)))|~(r1(X3,X40))))&(~(p8(X3))|![X41]:((~(r1(X3,X41))|~(p107(X41)))|p8(X41))))|~(p107(X3))))&(~(p108(X3))|((~(p9(X3))|![X42]:((~(p108(X42))|p9(X42))|~(r1(X3,X42))))&(![X43]:((~(r1(X3,X43))|~(p108(X43)))|~(p9(X43)))|p9(X3)))))&(((p10(X3)|![X44]:((~(p109(X44))|~(p10(X44)))|~(r1(X3,X44))))&(~(p10(X3))|![X45]:((~(r1(X3,X45))|~(p109(X45)))|p10(X45))))|~(p109(X3))))&(~(p110(X3))|((![X46]:((~(r1(X3,X46))|p11(X46))|~(p110(X46)))|~(p11(X3)))&(p11(X3)|![X47]:((~(p11(X47))|~(p110(X47)))|~(r1(X3,X47)))))))&(~(p111(X3))|((p12(X3)|![X48]:((~(p12(X48))|~(p111(X48)))|~(r1(X3,X48))))&(~(p12(X3))|![X49]:((p12(X49)|~(p111(X49)))|~(r1(X3,X49)))))))&((?[X50]:(((~(p6(X50))&p105(X50))&~(p106(X50)))&r1(X3,X50))&?[X51]:(r1(X3,X51)&((p6(X51)&p105(X51))&~(p106(X51)))))|(p105(X3)|~(p104(X3)))))&((?[X52]:(r1(X3,X52)&((~(p8(X52))&~(p108(X52)))&p107(X52)))&?[X53]:(r1(X3,X53)&((p8(X53)&~(p108(X53)))&p107(X53))))|(p107(X3)|~(p106(X3)))))&((~(p107(X3))|p108(X3))|(?[X54]:(r1(X3,X54)&((~(p109(X54))&p108(X54))&p9(X54)))&?[X55]:(((p108(X55)&~(p109(X55)))&~(p9(X55)))&r1(X3,X55)))))&((?[X56]:(((p109(X56)&~(p110(X56)))&~(p10(X56)))&r1(X3,X56))&?[X57]:(((p109(X57)&~(p110(X57)))&p10(X57))&r1(X3,X57)))|(p109(X3)|~(p108(X3)))))&((?[X58]:(((p11(X58)&~(p111(X58)))&p110(X58))&r1(X3,X58))&?[X59]:(r1(X3,X59)&((~(p111(X59))&p110(X59))&~(p11(X59)))))|(p110(X3)|~(p109(X3)))))&((~(p110(X3))|p111(X3))|(?[X60]:(((~(p112(X60))&p111(X60))&p12(X60))&r1(X3,X60))&?[X61]:(((~(p112(X61))&p111(X61))&~(p12(X61)))&r1(X3,X61)))))&((p113(X3)|~(p112(X3)))|(?[X62]:(r1(X3,X62)&((p113(X62)&~(p114(X62)))&p14(X62)))&?[X63]:(((p113(X63)&~(p114(X63)))&~(p14(X63)))&r1(X3,X63)))))&((?[X64]:(((~(p116(X64))&p115(X64))&~(p16(X64)))&r1(X3,X64))&?[X65]:(r1(X3,X65)&((~(p116(X65))&p115(X65))&p16(X65))))|(p115(X3)|~(p114(X3)))))),inference(variable_rename,[status(thm)],[21])).
fof(23, plain,![X3]:(~(epred1_1(X3))|(((((((((((((((((((((((((((((((((((((((((((((((((((~(p15(esk2_1(X3)))&~(p115(esk2_1(X3))))&p114(esk2_1(X3)))&r1(X3,esk2_1(X3)))&(((p15(esk3_1(X3))&p114(esk3_1(X3)))&~(p115(esk3_1(X3))))&r1(X3,esk3_1(X3))))|(~(p113(X3))|p114(X3)))&(((((p13(esk4_1(X3))&~(p113(esk4_1(X3))))&p112(esk4_1(X3)))&r1(X3,esk4_1(X3)))&(((~(p13(esk5_1(X3)))&~(p113(esk5_1(X3))))&p112(esk5_1(X3)))&r1(X3,esk5_1(X3))))|(~(p111(X3))|p112(X3))))&((p106(X3)|~(p105(X3)))|((((~(p107(esk6_1(X3)))&p106(esk6_1(X3)))&p7(esk6_1(X3)))&r1(X3,esk6_1(X3)))&(r1(X3,esk7_1(X3))&((~(p107(esk7_1(X3)))&p106(esk7_1(X3)))&~(p7(esk7_1(X3))))))))&(((((~(p105(esk8_1(X3)))&p104(esk8_1(X3)))&~(p5(esk8_1(X3))))&r1(X3,esk8_1(X3)))&(r1(X3,esk9_1(X3))&((p104(esk9_1(X3))&~(p105(esk9_1(X3))))&p5(esk9_1(X3)))))|(~(p103(X3))|p104(X3))))&((p103(X3)|~(p102(X3)))|((r1(X3,esk10_1(X3))&((p4(esk10_1(X3))&~(p104(esk10_1(X3))))&p103(esk10_1(X3))))&(((~(p4(esk11_1(X3)))&~(p104(esk11_1(X3))))&p103(esk11_1(X3)))&r1(X3,esk11_1(X3))))))&(((((~(p3(esk12_1(X3)))&~(p103(esk12_1(X3))))&p102(esk12_1(X3)))&r1(X3,esk12_1(X3)))&(r1(X3,esk13_1(X3))&((p102(esk13_1(X3))&~(p103(esk13_1(X3))))&p3(esk13_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk14_1(X3))&((~(p2(esk14_1(X3)))&p101(esk14_1(X3)))&~(p102(esk14_1(X3)))))&(((p2(esk15_1(X3))&p101(esk15_1(X3)))&~(p102(esk15_1(X3))))&r1(X3,esk15_1(X3))))|(~(p100(X3))|p101(X3))))&(((![X18]:((~(p16(X18))|~(p115(X18)))|~(r1(X3,X18)))|p16(X3))&(![X19]:((~(p115(X19))|p16(X19))|~(r1(X3,X19)))|~(p16(X3))))|~(p115(X3))))&(~(p114(X3))|((p15(X3)|![X20]:((~(r1(X3,X20))|~(p15(X20)))|~(p114(X20))))&(~(p15(X3))|![X21]:((~(r1(X3,X21))|p15(X21))|~(p114(X21)))))))&(~(p113(X3))|((p14(X3)|![X22]:((~(p113(X22))|~(p14(X22)))|~(r1(X3,X22))))&(~(p14(X3))|![X23]:((~(p113(X23))|p14(X23))|~(r1(X3,X23)))))))&(((~(p13(X3))|![X24]:((~(r1(X3,X24))|p13(X24))|~(p112(X24))))&(p13(X3)|![X25]:((~(p112(X25))|~(p13(X25)))|~(r1(X3,X25)))))|~(p112(X3))))&(((![X26]:((~(r1(X3,X26))|~(p100(X26)))|~(p1(X26)))|p1(X3))&(~(p1(X3))|![X27]:((~(r1(X3,X27))|p1(X27))|~(p100(X27)))))|~(p100(X3))))&(p113(X3)|~(p114(X3))))&(p111(X3)|~(p112(X3))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(~(p108(X3))|p107(X3)))&(p106(X3)|~(p107(X3))))&(p104(X3)|~(p105(X3))))&(~(p103(X3))|p102(X3)))&(p100(X3)|~(p101(X3))))&(p101(X3)|~(p102(X3))))&(p103(X3)|~(p104(X3))))&(p105(X3)|~(p106(X3))))&(~(p113(X3))|p112(X3)))&(p114(X3)|~(p115(X3))))&(p115(X3)|~(p116(X3))))&(((~(p2(X3))|![X28]:((~(p101(X28))|p2(X28))|~(r1(X3,X28))))&(p2(X3)|![X29]:((~(r1(X3,X29))|~(p2(X29)))|~(p101(X29)))))|~(p101(X3))))&(((![X30]:((p3(X30)|~(p102(X30)))|~(r1(X3,X30)))|~(p3(X3)))&(![X31]:((~(p3(X31))|~(p102(X31)))|~(r1(X3,X31)))|p3(X3)))|~(p102(X3))))&(~(p103(X3))|((p4(X3)|![X32]:((~(p103(X32))|~(p4(X32)))|~(r1(X3,X32))))&(![X33]:((~(r1(X3,X33))|p4(X33))|~(p103(X33)))|~(p4(X3))))))&(((![X34]:((p5(X34)|~(p104(X34)))|~(r1(X3,X34)))|~(p5(X3)))&(p5(X3)|![X35]:((~(r1(X3,X35))|~(p104(X35)))|~(p5(X35)))))|~(p104(X3))))&(((~(p6(X3))|![X36]:((~(p105(X36))|p6(X36))|~(r1(X3,X36))))&(![X37]:((~(p105(X37))|~(p6(X37)))|~(r1(X3,X37)))|p6(X3)))|~(p105(X3))))&(~(p106(X3))|((![X38]:((~(r1(X3,X38))|~(p7(X38)))|~(p106(X38)))|p7(X3))&(![X39]:((~(r1(X3,X39))|~(p106(X39)))|p7(X39))|~(p7(X3))))))&(((p8(X3)|![X40]:((~(p8(X40))|~(p107(X40)))|~(r1(X3,X40))))&(~(p8(X3))|![X41]:((~(r1(X3,X41))|~(p107(X41)))|p8(X41))))|~(p107(X3))))&(~(p108(X3))|((~(p9(X3))|![X42]:((~(p108(X42))|p9(X42))|~(r1(X3,X42))))&(![X43]:((~(r1(X3,X43))|~(p108(X43)))|~(p9(X43)))|p9(X3)))))&(((p10(X3)|![X44]:((~(p109(X44))|~(p10(X44)))|~(r1(X3,X44))))&(~(p10(X3))|![X45]:((~(r1(X3,X45))|~(p109(X45)))|p10(X45))))|~(p109(X3))))&(~(p110(X3))|((![X46]:((~(r1(X3,X46))|p11(X46))|~(p110(X46)))|~(p11(X3)))&(p11(X3)|![X47]:((~(p11(X47))|~(p110(X47)))|~(r1(X3,X47)))))))&(~(p111(X3))|((p12(X3)|![X48]:((~(p12(X48))|~(p111(X48)))|~(r1(X3,X48))))&(~(p12(X3))|![X49]:((p12(X49)|~(p111(X49)))|~(r1(X3,X49)))))))&(((((~(p6(esk16_1(X3)))&p105(esk16_1(X3)))&~(p106(esk16_1(X3))))&r1(X3,esk16_1(X3)))&(r1(X3,esk17_1(X3))&((p6(esk17_1(X3))&p105(esk17_1(X3)))&~(p106(esk17_1(X3))))))|(p105(X3)|~(p104(X3)))))&(((r1(X3,esk18_1(X3))&((~(p8(esk18_1(X3)))&~(p108(esk18_1(X3))))&p107(esk18_1(X3))))&(r1(X3,esk19_1(X3))&((p8(esk19_1(X3))&~(p108(esk19_1(X3))))&p107(esk19_1(X3)))))|(p107(X3)|~(p106(X3)))))&((~(p107(X3))|p108(X3))|((r1(X3,esk20_1(X3))&((~(p109(esk20_1(X3)))&p108(esk20_1(X3)))&p9(esk20_1(X3))))&(((p108(esk21_1(X3))&~(p109(esk21_1(X3))))&~(p9(esk21_1(X3))))&r1(X3,esk21_1(X3))))))&(((((p109(esk22_1(X3))&~(p110(esk22_1(X3))))&~(p10(esk22_1(X3))))&r1(X3,esk22_1(X3)))&(((p109(esk23_1(X3))&~(p110(esk23_1(X3))))&p10(esk23_1(X3)))&r1(X3,esk23_1(X3))))|(p109(X3)|~(p108(X3)))))&(((((p11(esk24_1(X3))&~(p111(esk24_1(X3))))&p110(esk24_1(X3)))&r1(X3,esk24_1(X3)))&(r1(X3,esk25_1(X3))&((~(p111(esk25_1(X3)))&p110(esk25_1(X3)))&~(p11(esk25_1(X3))))))|(p110(X3)|~(p109(X3)))))&((~(p110(X3))|p111(X3))|((((~(p112(esk26_1(X3)))&p111(esk26_1(X3)))&p12(esk26_1(X3)))&r1(X3,esk26_1(X3)))&(((~(p112(esk27_1(X3)))&p111(esk27_1(X3)))&~(p12(esk27_1(X3))))&r1(X3,esk27_1(X3))))))&((p113(X3)|~(p112(X3)))|((r1(X3,esk28_1(X3))&((p113(esk28_1(X3))&~(p114(esk28_1(X3))))&p14(esk28_1(X3))))&(((p113(esk29_1(X3))&~(p114(esk29_1(X3))))&~(p14(esk29_1(X3))))&r1(X3,esk29_1(X3))))))&(((((~(p116(esk30_1(X3)))&p115(esk30_1(X3)))&~(p16(esk30_1(X3))))&r1(X3,esk30_1(X3)))&(r1(X3,esk31_1(X3))&((~(p116(esk31_1(X3)))&p115(esk31_1(X3)))&p16(esk31_1(X3)))))|(p115(X3)|~(p114(X3)))))),inference(skolemize,[status(esa)],[22])).
fof(24, plain,![X3]:![X18]:![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:![X26]:![X27]:![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:![X46]:![X47]:![X48]:![X49]:(~(epred1_1(X3))|(((((((((((((((((((((((((((((((((((((((((((((((((((~(p15(esk2_1(X3)))&~(p115(esk2_1(X3))))&p114(esk2_1(X3)))&r1(X3,esk2_1(X3)))&(((p15(esk3_1(X3))&p114(esk3_1(X3)))&~(p115(esk3_1(X3))))&r1(X3,esk3_1(X3))))|(~(p113(X3))|p114(X3)))&(((((p13(esk4_1(X3))&~(p113(esk4_1(X3))))&p112(esk4_1(X3)))&r1(X3,esk4_1(X3)))&(((~(p13(esk5_1(X3)))&~(p113(esk5_1(X3))))&p112(esk5_1(X3)))&r1(X3,esk5_1(X3))))|(~(p111(X3))|p112(X3))))&((p106(X3)|~(p105(X3)))|((((~(p107(esk6_1(X3)))&p106(esk6_1(X3)))&p7(esk6_1(X3)))&r1(X3,esk6_1(X3)))&(r1(X3,esk7_1(X3))&((~(p107(esk7_1(X3)))&p106(esk7_1(X3)))&~(p7(esk7_1(X3))))))))&(((((~(p105(esk8_1(X3)))&p104(esk8_1(X3)))&~(p5(esk8_1(X3))))&r1(X3,esk8_1(X3)))&(r1(X3,esk9_1(X3))&((p104(esk9_1(X3))&~(p105(esk9_1(X3))))&p5(esk9_1(X3)))))|(~(p103(X3))|p104(X3))))&((p103(X3)|~(p102(X3)))|((r1(X3,esk10_1(X3))&((p4(esk10_1(X3))&~(p104(esk10_1(X3))))&p103(esk10_1(X3))))&(((~(p4(esk11_1(X3)))&~(p104(esk11_1(X3))))&p103(esk11_1(X3)))&r1(X3,esk11_1(X3))))))&(((((~(p3(esk12_1(X3)))&~(p103(esk12_1(X3))))&p102(esk12_1(X3)))&r1(X3,esk12_1(X3)))&(r1(X3,esk13_1(X3))&((p102(esk13_1(X3))&~(p103(esk13_1(X3))))&p3(esk13_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk14_1(X3))&((~(p2(esk14_1(X3)))&p101(esk14_1(X3)))&~(p102(esk14_1(X3)))))&(((p2(esk15_1(X3))&p101(esk15_1(X3)))&~(p102(esk15_1(X3))))&r1(X3,esk15_1(X3))))|(~(p100(X3))|p101(X3))))&(((((~(p16(X18))|~(p115(X18)))|~(r1(X3,X18)))|p16(X3))&(((~(p115(X19))|p16(X19))|~(r1(X3,X19)))|~(p16(X3))))|~(p115(X3))))&(~(p114(X3))|((p15(X3)|((~(r1(X3,X20))|~(p15(X20)))|~(p114(X20))))&(~(p15(X3))|((~(r1(X3,X21))|p15(X21))|~(p114(X21)))))))&(~(p113(X3))|((p14(X3)|((~(p113(X22))|~(p14(X22)))|~(r1(X3,X22))))&(~(p14(X3))|((~(p113(X23))|p14(X23))|~(r1(X3,X23)))))))&(((~(p13(X3))|((~(r1(X3,X24))|p13(X24))|~(p112(X24))))&(p13(X3)|((~(p112(X25))|~(p13(X25)))|~(r1(X3,X25)))))|~(p112(X3))))&(((((~(r1(X3,X26))|~(p100(X26)))|~(p1(X26)))|p1(X3))&(~(p1(X3))|((~(r1(X3,X27))|p1(X27))|~(p100(X27)))))|~(p100(X3))))&(p113(X3)|~(p114(X3))))&(p111(X3)|~(p112(X3))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(~(p108(X3))|p107(X3)))&(p106(X3)|~(p107(X3))))&(p104(X3)|~(p105(X3))))&(~(p103(X3))|p102(X3)))&(p100(X3)|~(p101(X3))))&(p101(X3)|~(p102(X3))))&(p103(X3)|~(p104(X3))))&(p105(X3)|~(p106(X3))))&(~(p113(X3))|p112(X3)))&(p114(X3)|~(p115(X3))))&(p115(X3)|~(p116(X3))))&(((~(p2(X3))|((~(p101(X28))|p2(X28))|~(r1(X3,X28))))&(p2(X3)|((~(r1(X3,X29))|~(p2(X29)))|~(p101(X29)))))|~(p101(X3))))&(((((p3(X30)|~(p102(X30)))|~(r1(X3,X30)))|~(p3(X3)))&(((~(p3(X31))|~(p102(X31)))|~(r1(X3,X31)))|p3(X3)))|~(p102(X3))))&(~(p103(X3))|((p4(X3)|((~(p103(X32))|~(p4(X32)))|~(r1(X3,X32))))&(((~(r1(X3,X33))|p4(X33))|~(p103(X33)))|~(p4(X3))))))&(((((p5(X34)|~(p104(X34)))|~(r1(X3,X34)))|~(p5(X3)))&(p5(X3)|((~(r1(X3,X35))|~(p104(X35)))|~(p5(X35)))))|~(p104(X3))))&(((~(p6(X3))|((~(p105(X36))|p6(X36))|~(r1(X3,X36))))&(((~(p105(X37))|~(p6(X37)))|~(r1(X3,X37)))|p6(X3)))|~(p105(X3))))&(~(p106(X3))|((((~(r1(X3,X38))|~(p7(X38)))|~(p106(X38)))|p7(X3))&(((~(r1(X3,X39))|~(p106(X39)))|p7(X39))|~(p7(X3))))))&(((p8(X3)|((~(p8(X40))|~(p107(X40)))|~(r1(X3,X40))))&(~(p8(X3))|((~(r1(X3,X41))|~(p107(X41)))|p8(X41))))|~(p107(X3))))&(~(p108(X3))|((~(p9(X3))|((~(p108(X42))|p9(X42))|~(r1(X3,X42))))&(((~(r1(X3,X43))|~(p108(X43)))|~(p9(X43)))|p9(X3)))))&(((p10(X3)|((~(p109(X44))|~(p10(X44)))|~(r1(X3,X44))))&(~(p10(X3))|((~(r1(X3,X45))|~(p109(X45)))|p10(X45))))|~(p109(X3))))&(~(p110(X3))|((((~(r1(X3,X46))|p11(X46))|~(p110(X46)))|~(p11(X3)))&(p11(X3)|((~(p11(X47))|~(p110(X47)))|~(r1(X3,X47)))))))&(~(p111(X3))|((p12(X3)|((~(p12(X48))|~(p111(X48)))|~(r1(X3,X48))))&(~(p12(X3))|((p12(X49)|~(p111(X49)))|~(r1(X3,X49)))))))&(((((~(p6(esk16_1(X3)))&p105(esk16_1(X3)))&~(p106(esk16_1(X3))))&r1(X3,esk16_1(X3)))&(r1(X3,esk17_1(X3))&((p6(esk17_1(X3))&p105(esk17_1(X3)))&~(p106(esk17_1(X3))))))|(p105(X3)|~(p104(X3)))))&(((r1(X3,esk18_1(X3))&((~(p8(esk18_1(X3)))&~(p108(esk18_1(X3))))&p107(esk18_1(X3))))&(r1(X3,esk19_1(X3))&((p8(esk19_1(X3))&~(p108(esk19_1(X3))))&p107(esk19_1(X3)))))|(p107(X3)|~(p106(X3)))))&((~(p107(X3))|p108(X3))|((r1(X3,esk20_1(X3))&((~(p109(esk20_1(X3)))&p108(esk20_1(X3)))&p9(esk20_1(X3))))&(((p108(esk21_1(X3))&~(p109(esk21_1(X3))))&~(p9(esk21_1(X3))))&r1(X3,esk21_1(X3))))))&(((((p109(esk22_1(X3))&~(p110(esk22_1(X3))))&~(p10(esk22_1(X3))))&r1(X3,esk22_1(X3)))&(((p109(esk23_1(X3))&~(p110(esk23_1(X3))))&p10(esk23_1(X3)))&r1(X3,esk23_1(X3))))|(p109(X3)|~(p108(X3)))))&(((((p11(esk24_1(X3))&~(p111(esk24_1(X3))))&p110(esk24_1(X3)))&r1(X3,esk24_1(X3)))&(r1(X3,esk25_1(X3))&((~(p111(esk25_1(X3)))&p110(esk25_1(X3)))&~(p11(esk25_1(X3))))))|(p110(X3)|~(p109(X3)))))&((~(p110(X3))|p111(X3))|((((~(p112(esk26_1(X3)))&p111(esk26_1(X3)))&p12(esk26_1(X3)))&r1(X3,esk26_1(X3)))&(((~(p112(esk27_1(X3)))&p111(esk27_1(X3)))&~(p12(esk27_1(X3))))&r1(X3,esk27_1(X3))))))&((p113(X3)|~(p112(X3)))|((r1(X3,esk28_1(X3))&((p113(esk28_1(X3))&~(p114(esk28_1(X3))))&p14(esk28_1(X3))))&(((p113(esk29_1(X3))&~(p114(esk29_1(X3))))&~(p14(esk29_1(X3))))&r1(X3,esk29_1(X3))))))&(((((~(p116(esk30_1(X3)))&p115(esk30_1(X3)))&~(p16(esk30_1(X3))))&r1(X3,esk30_1(X3)))&(r1(X3,esk31_1(X3))&((~(p116(esk31_1(X3)))&p115(esk31_1(X3)))&p16(esk31_1(X3)))))|(p115(X3)|~(p114(X3)))))),inference(shift_quantors,[status(thm)],[23])).
fof(25, plain,![X3]:![X18]:![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:![X26]:![X27]:![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:![X46]:![X47]:![X48]:![X49]:((((((((((((((((((((((((((((((((((((((((((((((((((((~(p15(esk2_1(X3)))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3)))&((~(p115(esk2_1(X3)))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3))))&((p114(esk2_1(X3))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3))))&((r1(X3,esk2_1(X3))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3))))&(((((p15(esk3_1(X3))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3)))&((p114(esk3_1(X3))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3))))&((~(p115(esk3_1(X3)))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3))))&((r1(X3,esk3_1(X3))|(~(p113(X3))|p114(X3)))|~(epred1_1(X3)))))&((((((p13(esk4_1(X3))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3)))&((~(p113(esk4_1(X3)))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))&((p112(esk4_1(X3))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))&((r1(X3,esk4_1(X3))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))&(((((~(p13(esk5_1(X3)))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3)))&((~(p113(esk5_1(X3)))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))&((p112(esk5_1(X3))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))&((r1(X3,esk5_1(X3))|(~(p111(X3))|p112(X3)))|~(epred1_1(X3))))))&((((((~(p107(esk6_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((p106(esk6_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&((p7(esk6_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&((r1(X3,esk6_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&(((r1(X3,esk7_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((((~(p107(esk7_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((p106(esk7_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&((~(p7(esk7_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))))))&((((((~(p105(esk8_1(X3)))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3)))&((p104(esk8_1(X3))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3))))&((~(p5(esk8_1(X3)))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3))))&((r1(X3,esk8_1(X3))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3))))&(((r1(X3,esk9_1(X3))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3)))&((((p104(esk9_1(X3))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3)))&((~(p105(esk9_1(X3)))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3))))&((p5(esk9_1(X3))|(~(p103(X3))|p104(X3)))|~(epred1_1(X3)))))))&((((r1(X3,esk10_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((((p4(esk10_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk10_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk10_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))))&(((((~(p4(esk11_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk11_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk11_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((r1(X3,esk11_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))))&((((((~(p3(esk12_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk12_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p102(esk12_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((r1(X3,esk12_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&(((r1(X3,esk13_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((((p102(esk13_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk13_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p3(esk13_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk14_1(X3))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3)))&((((~(p2(esk14_1(X3)))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3)))&((p101(esk14_1(X3))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3))))&((~(p102(esk14_1(X3)))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3)))))&(((((p2(esk15_1(X3))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3)))&((p101(esk15_1(X3))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3))))&((~(p102(esk15_1(X3)))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3))))&((r1(X3,esk15_1(X3))|(~(p100(X3))|p101(X3)))|~(epred1_1(X3))))))&((((((~(p16(X18))|~(p115(X18)))|~(r1(X3,X18)))|p16(X3))|~(p115(X3)))|~(epred1_1(X3)))&(((((~(p115(X19))|p16(X19))|~(r1(X3,X19)))|~(p16(X3)))|~(p115(X3)))|~(epred1_1(X3)))))&((((p15(X3)|((~(r1(X3,X20))|~(p15(X20)))|~(p114(X20))))|~(p114(X3)))|~(epred1_1(X3)))&(((~(p15(X3))|((~(r1(X3,X21))|p15(X21))|~(p114(X21))))|~(p114(X3)))|~(epred1_1(X3)))))&((((p14(X3)|((~(p113(X22))|~(p14(X22)))|~(r1(X3,X22))))|~(p113(X3)))|~(epred1_1(X3)))&(((~(p14(X3))|((~(p113(X23))|p14(X23))|~(r1(X3,X23))))|~(p113(X3)))|~(epred1_1(X3)))))&((((~(p13(X3))|((~(r1(X3,X24))|p13(X24))|~(p112(X24))))|~(p112(X3)))|~(epred1_1(X3)))&(((p13(X3)|((~(p112(X25))|~(p13(X25)))|~(r1(X3,X25))))|~(p112(X3)))|~(epred1_1(X3)))))&((((((~(r1(X3,X26))|~(p100(X26)))|~(p1(X26)))|p1(X3))|~(p100(X3)))|~(epred1_1(X3)))&(((~(p1(X3))|((~(r1(X3,X27))|p1(X27))|~(p100(X27))))|~(p100(X3)))|~(epred1_1(X3)))))&((p113(X3)|~(p114(X3)))|~(epred1_1(X3))))&((p111(X3)|~(p112(X3)))|~(epred1_1(X3))))&((p110(X3)|~(p111(X3)))|~(epred1_1(X3))))&((p109(X3)|~(p110(X3)))|~(epred1_1(X3))))&((p108(X3)|~(p109(X3)))|~(epred1_1(X3))))&((~(p108(X3))|p107(X3))|~(epred1_1(X3))))&((p106(X3)|~(p107(X3)))|~(epred1_1(X3))))&((p104(X3)|~(p105(X3)))|~(epred1_1(X3))))&((~(p103(X3))|p102(X3))|~(epred1_1(X3))))&((p100(X3)|~(p101(X3)))|~(epred1_1(X3))))&((p101(X3)|~(p102(X3)))|~(epred1_1(X3))))&((p103(X3)|~(p104(X3)))|~(epred1_1(X3))))&((p105(X3)|~(p106(X3)))|~(epred1_1(X3))))&((~(p113(X3))|p112(X3))|~(epred1_1(X3))))&((p114(X3)|~(p115(X3)))|~(epred1_1(X3))))&((p115(X3)|~(p116(X3)))|~(epred1_1(X3))))&((((~(p2(X3))|((~(p101(X28))|p2(X28))|~(r1(X3,X28))))|~(p101(X3)))|~(epred1_1(X3)))&(((p2(X3)|((~(r1(X3,X29))|~(p2(X29)))|~(p101(X29))))|~(p101(X3)))|~(epred1_1(X3)))))&((((((p3(X30)|~(p102(X30)))|~(r1(X3,X30)))|~(p3(X3)))|~(p102(X3)))|~(epred1_1(X3)))&(((((~(p3(X31))|~(p102(X31)))|~(r1(X3,X31)))|p3(X3))|~(p102(X3)))|~(epred1_1(X3)))))&((((p4(X3)|((~(p103(X32))|~(p4(X32)))|~(r1(X3,X32))))|~(p103(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X33))|p4(X33))|~(p103(X33)))|~(p4(X3)))|~(p103(X3)))|~(epred1_1(X3)))))&((((((p5(X34)|~(p104(X34)))|~(r1(X3,X34)))|~(p5(X3)))|~(p104(X3)))|~(epred1_1(X3)))&(((p5(X3)|((~(r1(X3,X35))|~(p104(X35)))|~(p5(X35))))|~(p104(X3)))|~(epred1_1(X3)))))&((((~(p6(X3))|((~(p105(X36))|p6(X36))|~(r1(X3,X36))))|~(p105(X3)))|~(epred1_1(X3)))&(((((~(p105(X37))|~(p6(X37)))|~(r1(X3,X37)))|p6(X3))|~(p105(X3)))|~(epred1_1(X3)))))&((((((~(r1(X3,X38))|~(p7(X38)))|~(p106(X38)))|p7(X3))|~(p106(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X39))|~(p106(X39)))|p7(X39))|~(p7(X3)))|~(p106(X3)))|~(epred1_1(X3)))))&((((p8(X3)|((~(p8(X40))|~(p107(X40)))|~(r1(X3,X40))))|~(p107(X3)))|~(epred1_1(X3)))&(((~(p8(X3))|((~(r1(X3,X41))|~(p107(X41)))|p8(X41)))|~(p107(X3)))|~(epred1_1(X3)))))&((((~(p9(X3))|((~(p108(X42))|p9(X42))|~(r1(X3,X42))))|~(p108(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X43))|~(p108(X43)))|~(p9(X43)))|p9(X3))|~(p108(X3)))|~(epred1_1(X3)))))&((((p10(X3)|((~(p109(X44))|~(p10(X44)))|~(r1(X3,X44))))|~(p109(X3)))|~(epred1_1(X3)))&(((~(p10(X3))|((~(r1(X3,X45))|~(p109(X45)))|p10(X45)))|~(p109(X3)))|~(epred1_1(X3)))))&((((((~(r1(X3,X46))|p11(X46))|~(p110(X46)))|~(p11(X3)))|~(p110(X3)))|~(epred1_1(X3)))&(((p11(X3)|((~(p11(X47))|~(p110(X47)))|~(r1(X3,X47))))|~(p110(X3)))|~(epred1_1(X3)))))&((((p12(X3)|((~(p12(X48))|~(p111(X48)))|~(r1(X3,X48))))|~(p111(X3)))|~(epred1_1(X3)))&(((~(p12(X3))|((p12(X49)|~(p111(X49)))|~(r1(X3,X49))))|~(p111(X3)))|~(epred1_1(X3)))))&((((((~(p6(esk16_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((p105(esk16_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((~(p106(esk16_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((r1(X3,esk16_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&(((r1(X3,esk17_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((((p6(esk17_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((p105(esk17_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((~(p106(esk17_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk18_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((((~(p8(esk18_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((~(p108(esk18_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3))))&((p107(esk18_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk19_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((((p8(esk19_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((~(p108(esk19_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3))))&((p107(esk19_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk20_1(X3))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3)))&((((~(p109(esk20_1(X3)))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3)))&((p108(esk20_1(X3))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3))))&((p9(esk20_1(X3))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3)))))&(((((p108(esk21_1(X3))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3)))&((~(p109(esk21_1(X3)))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3))))&((~(p9(esk21_1(X3)))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3))))&((r1(X3,esk21_1(X3))|(~(p107(X3))|p108(X3)))|~(epred1_1(X3))))))&((((((p109(esk22_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((~(p110(esk22_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((~(p10(esk22_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((r1(X3,esk22_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&(((((p109(esk23_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((~(p110(esk23_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((p10(esk23_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((r1(X3,esk23_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))))&((((((p11(esk24_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((~(p111(esk24_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&((p110(esk24_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&((r1(X3,esk24_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&(((r1(X3,esk25_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((((~(p111(esk25_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((p110(esk25_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&((~(p11(esk25_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))))))&((((((~(p112(esk26_1(X3)))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3)))&((p111(esk26_1(X3))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))&((p12(esk26_1(X3))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))&((r1(X3,esk26_1(X3))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))&(((((~(p112(esk27_1(X3)))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3)))&((p111(esk27_1(X3))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))&((~(p12(esk27_1(X3)))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))&((r1(X3,esk27_1(X3))|(~(p110(X3))|p111(X3)))|~(epred1_1(X3))))))&((((r1(X3,esk28_1(X3))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3)))&((((p113(esk28_1(X3))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3)))&((~(p114(esk28_1(X3)))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3))))&((p14(esk28_1(X3))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3)))))&(((((p113(esk29_1(X3))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3)))&((~(p114(esk29_1(X3)))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3))))&((~(p14(esk29_1(X3)))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3))))&((r1(X3,esk29_1(X3))|(p113(X3)|~(p112(X3))))|~(epred1_1(X3))))))&((((((~(p116(esk30_1(X3)))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3)))&((p115(esk30_1(X3))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3))))&((~(p16(esk30_1(X3)))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3))))&((r1(X3,esk30_1(X3))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3))))&(((r1(X3,esk31_1(X3))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3)))&((((~(p116(esk31_1(X3)))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3)))&((p115(esk31_1(X3))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3))))&((p16(esk31_1(X3))|(p115(X3)|~(p114(X3))))|~(epred1_1(X3))))))),inference(distribute,[status(thm)],[24])).
cnf(86,plain,(p105(X1)|r1(X1,esk16_1(X1))|~epred1_1(X1)|~p104(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(87,plain,(p105(X1)|~epred1_1(X1)|~p104(X1)|~p106(esk16_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(88,plain,(p105(X1)|p105(esk16_1(X1))|~epred1_1(X1)|~p104(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(138,plain,(p101(X1)|r1(X1,esk15_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(139,plain,(p101(X1)|~epred1_1(X1)|~p100(X1)|~p102(esk15_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(140,plain,(p101(X1)|p101(esk15_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(147,plain,(p102(X1)|~epred1_1(X1)|~p101(X1)|~p103(esk13_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(148,plain,(p102(X1)|p102(esk13_1(X1))|~epred1_1(X1)|~p101(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(149,plain,(p102(X1)|r1(X1,esk13_1(X1))|~epred1_1(X1)|~p101(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(154,plain,(p103(X1)|r1(X1,esk11_1(X1))|~epred1_1(X1)|~p102(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(155,plain,(p103(X1)|p103(esk11_1(X1))|~epred1_1(X1)|~p102(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(156,plain,(p103(X1)|~epred1_1(X1)|~p102(X1)|~p104(esk11_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(166,plain,(p104(X1)|r1(X1,esk8_1(X1))|~epred1_1(X1)|~p103(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(168,plain,(p104(X1)|p104(esk8_1(X1))|~epred1_1(X1)|~p103(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(169,plain,(p104(X1)|~epred1_1(X1)|~p103(X1)|~p105(esk8_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(170,plain,(p106(X1)|~epred1_1(X1)|~p105(X1)|~p7(esk7_1(X1))),inference(split_conjunct,[status(thm)],[25])).
cnf(173,plain,(p106(X1)|r1(X1,esk7_1(X1))|~epred1_1(X1)|~p105(X1)),inference(split_conjunct,[status(thm)],[25])).
cnf(195,negated_conjecture,(epred1_1(esk1_0)),inference(spm,[status(thm)],[18,20,theory(equality)])).
cnf(207,negated_conjecture,(epred1_1(esk15_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[18,138,theory(equality)])).
cnf(211,negated_conjecture,(epred1_1(esk15_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|$false),inference(rw,[status(thm)],[207,17,theory(equality)])).
cnf(212,negated_conjecture,(epred1_1(esk15_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)),inference(cn,[status(thm)],[211,theory(equality)])).
cnf(213,negated_conjecture,(epred1_1(esk15_1(esk1_0))|~epred1_1(esk1_0)),inference(sr,[status(thm)],[212,16,theory(equality)])).
cnf(226,plain,(r1(X1,esk13_1(X2))|p102(X2)|~r1(X1,X2)|~epred1_1(X2)|~p101(X2)),inference(spm,[status(thm)],[10,149,theory(equality)])).
cnf(264,plain,(r1(X1,esk7_1(X2))|p106(X2)|~r1(X1,X2)|~epred1_1(X2)|~p105(X2)),inference(spm,[status(thm)],[10,173,theory(equality)])).
cnf(267,plain,(r1(X1,esk16_1(X2))|p105(X2)|~r1(X1,X2)|~epred1_1(X2)|~p104(X2)),inference(spm,[status(thm)],[10,86,theory(equality)])).
cnf(279,plain,(r1(X1,esk8_1(X2))|p104(X2)|~r1(X1,X2)|~epred1_1(X2)|~p103(X2)),inference(spm,[status(thm)],[10,166,theory(equality)])).
cnf(288,plain,(r1(X1,esk11_1(X2))|p103(X2)|~r1(X1,X2)|~epred1_1(X2)|~p102(X2)),inference(spm,[status(thm)],[10,154,theory(equality)])).
cnf(1339,negated_conjecture,(epred1_1(esk15_1(esk1_0))|$false),inference(rw,[status(thm)],[213,195,theory(equality)])).
cnf(1340,negated_conjecture,(epred1_1(esk15_1(esk1_0))),inference(cn,[status(thm)],[1339,theory(equality)])).
cnf(1636,plain,(p102(esk15_1(X1))|r1(X1,esk13_1(esk15_1(X1)))|p101(X1)|~epred1_1(esk15_1(X1))|~p101(esk15_1(X1))|~epred1_1(X1)|~p100(X1)),inference(spm,[status(thm)],[226,138,theory(equality)])).
cnf(2092,plain,(p106(esk16_1(X1))|r1(X1,esk7_1(esk16_1(X1)))|p105(X1)|~epred1_1(esk16_1(X1))|~p105(esk16_1(X1))|~epred1_1(X1)|~p104(X1)),inference(spm,[status(thm)],[264,86,theory(equality)])).
cnf(2131,plain,(p105(esk8_1(X1))|r1(X1,esk16_1(esk8_1(X1)))|p104(X1)|~epred1_1(esk8_1(X1))|~p104(esk8_1(X1))|~epred1_1(X1)|~p103(X1)),inference(spm,[status(thm)],[267,166,theory(equality)])).
cnf(2252,plain,(p104(esk11_1(X1))|r1(X1,esk8_1(esk11_1(X1)))|p103(X1)|~epred1_1(esk11_1(X1))|~p103(esk11_1(X1))|~epred1_1(X1)|~p102(X1)),inference(spm,[status(thm)],[279,154,theory(equality)])).
cnf(2343,plain,(p103(esk13_1(X1))|r1(X1,esk11_1(esk13_1(X1)))|p102(X1)|~epred1_1(esk13_1(X1))|~p102(esk13_1(X1))|~epred1_1(X1)|~p101(X1)),inference(spm,[status(thm)],[288,149,theory(equality)])).
cnf(3481,plain,(p101(X1)|p102(esk15_1(X1))|r1(X1,esk13_1(esk15_1(X1)))|~epred1_1(esk15_1(X1))|~epred1_1(X1)|~p100(X1)),inference(csr,[status(thm)],[1636,140])).
cnf(3482,plain,(p101(X1)|r1(X1,esk13_1(esk15_1(X1)))|~epred1_1(esk15_1(X1))|~epred1_1(X1)|~p100(X1)),inference(csr,[status(thm)],[3481,139])).
cnf(3483,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk13_1(esk15_1(esk1_0)))|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[3482,1340,theory(equality)])).
cnf(3484,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk13_1(esk15_1(esk1_0)))|$false|~p100(esk1_0)),inference(rw,[status(thm)],[3483,195,theory(equality)])).
cnf(3485,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk13_1(esk15_1(esk1_0)))|$false|$false),inference(rw,[status(thm)],[3484,17,theory(equality)])).
cnf(3486,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[3485,theory(equality)])).
cnf(3487,negated_conjecture,(r1(esk1_0,esk13_1(esk15_1(esk1_0)))),inference(sr,[status(thm)],[3486,16,theory(equality)])).
cnf(3552,negated_conjecture,(epred1_1(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[18,3487,theory(equality)])).
cnf(12132,plain,(p102(X1)|p103(esk13_1(X1))|r1(X1,esk11_1(esk13_1(X1)))|~epred1_1(esk13_1(X1))|~epred1_1(X1)|~p101(X1)),inference(csr,[status(thm)],[2343,148])).
cnf(12133,plain,(p102(X1)|r1(X1,esk11_1(esk13_1(X1)))|~epred1_1(esk13_1(X1))|~epred1_1(X1)|~p101(X1)),inference(csr,[status(thm)],[12132,147])).
cnf(12134,negated_conjecture,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[12133,3552,theory(equality)])).
cnf(12136,negated_conjecture,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[12134,1340,theory(equality)])).
cnf(12137,negated_conjecture,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[12136,theory(equality)])).
cnf(12141,plain,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[12137,140,theory(equality)])).
cnf(12144,plain,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[12141,195,theory(equality)])).
cnf(12145,plain,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[12144,17,theory(equality)])).
cnf(12146,plain,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[12145,theory(equality)])).
cnf(12147,plain,(p102(esk15_1(esk1_0))|r1(esk15_1(esk1_0),esk11_1(esk13_1(esk15_1(esk1_0))))),inference(sr,[status(thm)],[12146,16,theory(equality)])).
cnf(12172,plain,(r1(X1,esk11_1(esk13_1(esk15_1(esk1_0))))|p102(esk15_1(esk1_0))|~r1(X1,esk15_1(esk1_0))),inference(spm,[status(thm)],[10,12147,theory(equality)])).
cnf(12417,plain,(p102(esk15_1(esk1_0))|r1(esk1_0,esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[12172,138,theory(equality)])).
cnf(12418,plain,(p102(esk15_1(esk1_0))|r1(esk1_0,esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[12417,195,theory(equality)])).
cnf(12419,plain,(p102(esk15_1(esk1_0))|r1(esk1_0,esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[12418,17,theory(equality)])).
cnf(12420,plain,(p102(esk15_1(esk1_0))|r1(esk1_0,esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[12419,theory(equality)])).
cnf(12421,plain,(p102(esk15_1(esk1_0))|r1(esk1_0,esk11_1(esk13_1(esk15_1(esk1_0))))),inference(sr,[status(thm)],[12420,16,theory(equality)])).
cnf(12486,negated_conjecture,(epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|p102(esk15_1(esk1_0))),inference(spm,[status(thm)],[18,12421,theory(equality)])).
cnf(15721,plain,(p105(X1)|p106(esk16_1(X1))|r1(X1,esk7_1(esk16_1(X1)))|~epred1_1(esk16_1(X1))|~epred1_1(X1)|~p104(X1)),inference(csr,[status(thm)],[2092,88])).
cnf(15722,plain,(p105(X1)|r1(X1,esk7_1(esk16_1(X1)))|~epred1_1(esk16_1(X1))|~epred1_1(X1)|~p104(X1)),inference(csr,[status(thm)],[15721,87])).
cnf(15773,plain,(p104(X1)|p105(esk8_1(X1))|r1(X1,esk16_1(esk8_1(X1)))|~epred1_1(esk8_1(X1))|~epred1_1(X1)|~p103(X1)),inference(csr,[status(thm)],[2131,168])).
cnf(15774,plain,(p104(X1)|r1(X1,esk16_1(esk8_1(X1)))|~epred1_1(esk8_1(X1))|~epred1_1(X1)|~p103(X1)),inference(csr,[status(thm)],[15773,169])).
cnf(16026,plain,(p103(X1)|p104(esk11_1(X1))|r1(X1,esk8_1(esk11_1(X1)))|~epred1_1(esk11_1(X1))|~epred1_1(X1)|~p102(X1)),inference(csr,[status(thm)],[2252,155])).
cnf(16027,plain,(p103(X1)|r1(X1,esk8_1(esk11_1(X1)))|~epred1_1(esk11_1(X1))|~epred1_1(X1)|~p102(X1)),inference(csr,[status(thm)],[16026,156])).
cnf(16028,negated_conjecture,(p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[16027,12486,theory(equality)])).
cnf(16032,negated_conjecture,(p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[16028,3552,theory(equality)])).
cnf(16033,negated_conjecture,(p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[16032,theory(equality)])).
cnf(16061,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[16033,148,theory(equality)])).
cnf(16064,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[16061,1340,theory(equality)])).
cnf(16065,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[16064,theory(equality)])).
cnf(16067,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[16065,140,theory(equality)])).
cnf(16070,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[16067,195,theory(equality)])).
cnf(16071,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[16070,17,theory(equality)])).
cnf(16072,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)),inference(cn,[status(thm)],[16071,theory(equality)])).
cnf(16073,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk13_1(esk15_1(esk1_0)),esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(sr,[status(thm)],[16072,16,theory(equality)])).
cnf(16090,plain,(r1(X1,esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|~r1(X1,esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[10,16073,theory(equality)])).
cnf(16203,negated_conjecture,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|r1(esk1_0,esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[16090,3487,theory(equality)])).
cnf(16272,negated_conjecture,(epred1_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[18,16203,theory(equality)])).
cnf(16360,plain,(p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|~epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[15774,16272,theory(equality)])).
cnf(33996,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(csr,[status(thm)],[16360,12486])).
cnf(33998,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[33996,155,theory(equality)])).
cnf(33999,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[33998,3552,theory(equality)])).
cnf(34000,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[33999,theory(equality)])).
cnf(34002,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[34000,148,theory(equality)])).
cnf(34005,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[34002,1340,theory(equality)])).
cnf(34006,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[34005,theory(equality)])).
cnf(34008,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[34006,140,theory(equality)])).
cnf(34011,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[34008,195,theory(equality)])).
cnf(34012,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[34011,17,theory(equality)])).
cnf(34013,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)),inference(cn,[status(thm)],[34012,theory(equality)])).
cnf(34014,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk11_1(esk13_1(esk15_1(esk1_0))),esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))),inference(sr,[status(thm)],[34013,16,theory(equality)])).
cnf(34031,plain,(r1(X1,esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~r1(X1,esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[10,34014,theory(equality)])).
cnf(34079,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|r1(esk1_0,esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))),inference(spm,[status(thm)],[34031,12421,theory(equality)])).
cnf(34148,negated_conjecture,(epred1_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[18,34079,theory(equality)])).
cnf(34236,plain,(p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~epred1_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[15722,34148,theory(equality)])).
cnf(78830,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(csr,[status(thm)],[34236,16272])).
cnf(78832,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[78830,168,theory(equality)])).
cnf(79338,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(csr,[status(thm)],[78832,12486])).
cnf(79340,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[79338,155,theory(equality)])).
cnf(79341,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[79340,3552,theory(equality)])).
cnf(79342,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[79341,theory(equality)])).
cnf(79344,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[79342,148,theory(equality)])).
cnf(79347,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[79344,1340,theory(equality)])).
cnf(79348,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[79347,theory(equality)])).
cnf(79350,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[79348,140,theory(equality)])).
cnf(79353,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[79350,195,theory(equality)])).
cnf(79354,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[79353,17,theory(equality)])).
cnf(79355,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p101(esk1_0)),inference(cn,[status(thm)],[79354,theory(equality)])).
cnf(79356,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))),esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))),inference(sr,[status(thm)],[79355,16,theory(equality)])).
cnf(79373,plain,(r1(X1,esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~r1(X1,esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[10,79356,theory(equality)])).
cnf(79425,negated_conjecture,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|r1(esk1_0,esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))),inference(spm,[status(thm)],[79373,16203,theory(equality)])).
cnf(79491,negated_conjecture,(p7(esk7_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[15,79425,theory(equality)])).
cnf(79562,plain,(p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~epred1_1(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p105(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))),inference(spm,[status(thm)],[170,79491,theory(equality)])).
cnf(79957,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p105(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))),inference(csr,[status(thm)],[79562,34148])).
cnf(79959,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[79957,88,theory(equality)])).
cnf(79965,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(csr,[status(thm)],[79959,16272])).
cnf(79967,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[79965,168,theory(equality)])).
cnf(79968,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(csr,[status(thm)],[79967,12486])).
cnf(79970,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[79968,155,theory(equality)])).
cnf(79971,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[79970,3552,theory(equality)])).
cnf(79972,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[79971,theory(equality)])).
cnf(79974,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[79972,148,theory(equality)])).
cnf(79977,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[79974,1340,theory(equality)])).
cnf(79978,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[79977,theory(equality)])).
cnf(79980,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[79978,140,theory(equality)])).
cnf(79983,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[79980,195,theory(equality)])).
cnf(79984,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[79983,17,theory(equality)])).
cnf(79985,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))|p101(esk1_0)),inference(cn,[status(thm)],[79984,theory(equality)])).
cnf(79986,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p106(esk16_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0))))))),inference(sr,[status(thm)],[79985,16,theory(equality)])).
cnf(79987,plain,(p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~epred1_1(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(spm,[status(thm)],[87,79986,theory(equality)])).
cnf(79994,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p104(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(csr,[status(thm)],[79987,16272])).
cnf(79996,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[79994,168,theory(equality)])).
cnf(80002,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(csr,[status(thm)],[79996,12486])).
cnf(80004,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[80002,155,theory(equality)])).
cnf(80005,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[80004,3552,theory(equality)])).
cnf(80006,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[80005,theory(equality)])).
cnf(80008,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[80006,148,theory(equality)])).
cnf(80011,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[80008,1340,theory(equality)])).
cnf(80012,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[80011,theory(equality)])).
cnf(80014,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[80012,140,theory(equality)])).
cnf(80017,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[80014,195,theory(equality)])).
cnf(80018,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[80017,17,theory(equality)])).
cnf(80019,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))|p101(esk1_0)),inference(cn,[status(thm)],[80018,theory(equality)])).
cnf(80020,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p105(esk8_1(esk11_1(esk13_1(esk15_1(esk1_0)))))),inference(sr,[status(thm)],[80019,16,theory(equality)])).
cnf(80021,plain,(p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|~epred1_1(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(spm,[status(thm)],[169,80020,theory(equality)])).
cnf(80030,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~p103(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(csr,[status(thm)],[80021,12486])).
cnf(80032,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[80030,155,theory(equality)])).
cnf(80033,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[80032,3552,theory(equality)])).
cnf(80034,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[80033,theory(equality)])).
cnf(80036,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[80034,148,theory(equality)])).
cnf(80039,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[80036,1340,theory(equality)])).
cnf(80040,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[80039,theory(equality)])).
cnf(80048,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[80040,140,theory(equality)])).
cnf(80051,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[80048,195,theory(equality)])).
cnf(80052,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[80051,17,theory(equality)])).
cnf(80053,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[80052,theory(equality)])).
cnf(80054,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p104(esk11_1(esk13_1(esk15_1(esk1_0))))),inference(sr,[status(thm)],[80053,16,theory(equality)])).
cnf(80055,plain,(p103(esk13_1(esk15_1(esk1_0)))|p102(esk15_1(esk1_0))|~epred1_1(esk13_1(esk15_1(esk1_0)))|~p102(esk13_1(esk15_1(esk1_0)))),inference(spm,[status(thm)],[156,80054,theory(equality)])).
cnf(80061,plain,(p103(esk13_1(esk15_1(esk1_0)))|p102(esk15_1(esk1_0))|$false|~p102(esk13_1(esk15_1(esk1_0)))),inference(rw,[status(thm)],[80055,3552,theory(equality)])).
cnf(80062,plain,(p103(esk13_1(esk15_1(esk1_0)))|p102(esk15_1(esk1_0))|~p102(esk13_1(esk15_1(esk1_0)))),inference(cn,[status(thm)],[80061,theory(equality)])).
cnf(80064,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[80062,148,theory(equality)])).
cnf(80067,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[80064,1340,theory(equality)])).
cnf(80068,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[80067,theory(equality)])).
cnf(80070,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[80068,140,theory(equality)])).
cnf(80073,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[80070,195,theory(equality)])).
cnf(80074,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[80073,17,theory(equality)])).
cnf(80075,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))|p101(esk1_0)),inference(cn,[status(thm)],[80074,theory(equality)])).
cnf(80076,plain,(p102(esk15_1(esk1_0))|p103(esk13_1(esk15_1(esk1_0)))),inference(sr,[status(thm)],[80075,16,theory(equality)])).
cnf(80077,plain,(p102(esk15_1(esk1_0))|~epred1_1(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(spm,[status(thm)],[147,80076,theory(equality)])).
cnf(80081,plain,(p102(esk15_1(esk1_0))|$false|~p101(esk15_1(esk1_0))),inference(rw,[status(thm)],[80077,1340,theory(equality)])).
cnf(80082,plain,(p102(esk15_1(esk1_0))|~p101(esk15_1(esk1_0))),inference(cn,[status(thm)],[80081,theory(equality)])).
cnf(80084,plain,(p102(esk15_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[80082,140,theory(equality)])).
cnf(80087,plain,(p102(esk15_1(esk1_0))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[80084,195,theory(equality)])).
cnf(80088,plain,(p102(esk15_1(esk1_0))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[80087,17,theory(equality)])).
cnf(80089,plain,(p102(esk15_1(esk1_0))|p101(esk1_0)),inference(cn,[status(thm)],[80088,theory(equality)])).
cnf(80090,plain,(p102(esk15_1(esk1_0))),inference(sr,[status(thm)],[80089,16,theory(equality)])).
cnf(80091,plain,(p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[139,80090,theory(equality)])).
cnf(82548,plain,(p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[80091,195,theory(equality)])).
cnf(82549,plain,(p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[82548,17,theory(equality)])).
cnf(82550,plain,(p101(esk1_0)),inference(cn,[status(thm)],[82549,theory(equality)])).
cnf(82551,plain,($false),inference(sr,[status(thm)],[82550,16,theory(equality)])).
cnf(82552,plain,($false),82551,['proof']).
# SZS output end CNFRefutation
# Initial clauses in saturation        : 174
# Processed clauses                    : 21157
# ...of these trivial                  : 4
# ...subsumed                          : 6393
# ...remaining for further processing  : 14760
# Other redundant clauses eliminated   : 0
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 4965
# Backward-rewritten                   : 2456
# Generated clauses                    : 32392
# ...of the previous two non-trivial   : 27643
# Contextual simplify-reflections      : 17398
# Paramodulations                      : 32392
# Factorizations                       : 0
# Equation resolutions                 : 0
# Current number of processed clauses  : 7165
#    Positive orientable unit clauses  : 21
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 26
#    Non-unit-clauses                  : 7118
# Current number of unprocessed clauses: 2960
# ...number of literals in the above   : 22608
# Clause-clause subsumption calls (NU) : 12983782
# Rec. Clause-clause subsumption calls : 278165
# Unit Clause-clause subsumption calls : 4696
# Rewrite failures with RHS unbound    : 0
# Indexed BW rewrite attempts          : 1
# Indexed BW rewrite successes         : 1
# Unification attempts                 : 35681
# Unification successes                : 17696
# Backwards rewriting index :  4049 leaves,   1.33+/-0.773 terms/leaf
# Paramod-from index        :   205 leaves,   1.38+/-0.839 terms/leaf
# Paramod-into index        :  1070 leaves,   1.27+/-0.702 terms/leaf

# -------------------------------------------------
# User time                : 5.280 s
# System time              : 0.030 s
# Total time               : 5.310 s
# Maximum resident set size: 32920 pages

WATCH: 5.88 CPU 5.98 WC

FINAL WATCH: 5.88 CPU 5.98 WC