%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL656+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:21 AM UTC 2026
% Result : Theorem 177.70s 23.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL656+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.36 % Computer : n001.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 10:38:16 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.24/0.48 start to proof:theBenchmark.p
% 177.70/23.00 % Version : CSI_E---1.1
% 177.70/23.00 % Problem : theBenchmark.p
% 177.70/23.00 % Proof found!
% 177.70/23.00 % SZS status Theorem for theBenchmark.p
% 177.70/23.00 % SZS output start Proof
% 177.70/23.00 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p7(X2))))))))))))))))))))))))))))))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:((~(r1(X2,X1))|~(((~(p16(X1))&~(p116(X1)))&p115(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p16(X1)&~(p116(X1)))&p115(X1)))))))|~((~(p115(X2))&p114(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p15(X1))&~(p115(X1)))&p114(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p15(X1)&~(p115(X1)))&p114(X1)))))))|~((~(p114(X2))&p113(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p14(X1))&~(p114(X1)))&p113(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p14(X1)&~(p114(X1)))&p113(X1)))))))|~((~(p113(X2))&p112(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p13(X1))&~(p113(X1)))&p112(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p13(X1)&~(p113(X1)))&p112(X1)))))))|~((~(p112(X2))&p111(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p12(X1))&~(p112(X1)))&p111(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p12(X1)&~(p112(X1)))&p111(X1)))))))|~((~(p111(X2))&p110(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1)))))))|~((~(p110(X2))&p109(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1)))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1)))))))|~((~(p108(X2))&p107(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)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1)))))))|~((~(p106(X2))&p105(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1)))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1)))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1)))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1)))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p16(X1))|~(p115(X1))))|p16(X2))&(![X1]:((~(r1(X2,X1))|p16(X1)|~(p115(X1))))|~(p16(X2))))|~(p115(X2))))&(((![X1]:((~(r1(X2,X1))|~(p15(X1))|~(p114(X1))))|p15(X2))&(![X1]:((~(r1(X2,X1))|p15(X1)|~(p114(X1))))|~(p15(X2))))|~(p114(X2))))&(((![X1]:((~(r1(X2,X1))|~(p14(X1))|~(p113(X1))))|p14(X2))&(![X1]:((~(r1(X2,X1))|p14(X1)|~(p113(X1))))|~(p14(X2))))|~(p113(X2))))&(((![X1]:((~(r1(X2,X1))|~(p13(X1))|~(p112(X1))))|p13(X2))&(![X1]:((~(r1(X2,X1))|p13(X1)|~(p112(X1))))|~(p13(X2))))|~(p112(X2))))&(((![X1]:((~(r1(X2,X1))|~(p12(X1))|~(p111(X1))))|p12(X2))&(![X1]:((~(r1(X2,X1))|p12(X1)|~(p111(X1))))|~(p12(X2))))|~(p111(X2))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1))|~(p110(X1))))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1)|~(p110(X1))))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1))|~(p109(X1))))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1)|~(p109(X1))))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1))|~(p108(X1))))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1)|~(p108(X1))))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1))|~(p107(X1))))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1)|~(p107(X1))))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1))|~(p106(X1))))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1)|~(p106(X1))))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1))|~(p105(X1))))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1)|~(p105(X1))))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1))|~(p104(X1))))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1)|~(p104(X1))))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1))|~(p103(X1))))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1)|~(p103(X1))))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1))|~(p102(X1))))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1)|~(p102(X1))))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1))|~(p101(X1))))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1)|~(p101(X1))))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1))|~(p100(X1))))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1)|~(p100(X1))))|~(p1(X2))))|~(p100(X2))))&(p115(X2)|~(p116(X2))))&(p114(X2)|~(p115(X2))))&(p113(X2)|~(p114(X2))))&(p112(X2)|~(p113(X2))))&(p111(X2)|~(p112(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2))))))))))))))))))))))))))))))))))&~(p101(X1)))&p100(X1))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 177.70/23.00 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 177.70/23.00 fof(c_0_2, plain, ![X2]:((epred1_1(X2)<=>((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p16(X1)&~p116(X1))&p115(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p16(X1)&~p116(X1))&p115(X1)))))))|~((~p115(X2)&p114(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p15(X1)&~p115(X1))&p114(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p15(X1)&~p115(X1))&p114(X1)))))))|~((~p114(X2)&p113(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p14(X1)&~p114(X1))&p113(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p14(X1)&~p114(X1))&p113(X1)))))))|~((~p113(X2)&p112(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p113(X1))&p112(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p113(X1))&p112(X1)))))))|~((~p112(X2)&p111(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p112(X1))&p111(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p12(X1)&~p112(X1))&p111(X1)))))))|~((~p111(X2)&p110(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p111(X1))&p110(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p111(X1))&p110(X1)))))))|~((~p110(X2)&p109(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p110(X1))&p109(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p10(X1)&~p110(X1))&p109(X1)))))))|~((~p109(X2)&p108(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p109(X1))&p108(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p109(X1))&p108(X1)))))))|~((~p108(X2)&p107(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)))))&((~(![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p107(X1))&p106(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p107(X1))&p106(X1)))))))|~((~p106(X2)&p105(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p16(X1)|~p115(X1)))|p16(X2))&(![X1]:((~r1(X2,X1)|p16(X1)|~p115(X1)))|~p16(X2)))|~p115(X2)))&(((![X1]:((~r1(X2,X1)|~p15(X1)|~p114(X1)))|p15(X2))&(![X1]:((~r1(X2,X1)|p15(X1)|~p114(X1)))|~p15(X2)))|~p114(X2)))&(((![X1]:((~r1(X2,X1)|~p14(X1)|~p113(X1)))|p14(X2))&(![X1]:((~r1(X2,X1)|p14(X1)|~p113(X1)))|~p14(X2)))|~p113(X2)))&(((![X1]:((~r1(X2,X1)|~p13(X1)|~p112(X1)))|p13(X2))&(![X1]:((~r1(X2,X1)|p13(X1)|~p112(X1)))|~p13(X2)))|~p112(X2)))&(((![X1]:((~r1(X2,X1)|~p12(X1)|~p111(X1)))|p12(X2))&(![X1]:((~r1(X2,X1)|p12(X1)|~p111(X1)))|~p12(X2)))|~p111(X2)))&(((![X1]:((~r1(X2,X1)|~p11(X1)|~p110(X1)))|p11(X2))&(![X1]:((~r1(X2,X1)|p11(X1)|~p110(X1)))|~p11(X2)))|~p110(X2)))&(((![X1]:((~r1(X2,X1)|~p10(X1)|~p109(X1)))|p10(X2))&(![X1]:((~r1(X2,X1)|p10(X1)|~p109(X1)))|~p10(X2)))|~p109(X2)))&(((![X1]:((~r1(X2,X1)|~p9(X1)|~p108(X1)))|p9(X2))&(![X1]:((~r1(X2,X1)|p9(X1)|~p108(X1)))|~p9(X2)))|~p108(X2)))&(((![X1]:((~r1(X2,X1)|~p8(X1)|~p107(X1)))|p8(X2))&(![X1]:((~r1(X2,X1)|p8(X1)|~p107(X1)))|~p8(X2)))|~p107(X2)))&(((![X1]:((~r1(X2,X1)|~p7(X1)|~p106(X1)))|p7(X2))&(![X1]:((~r1(X2,X1)|p7(X1)|~p106(X1)))|~p7(X2)))|~p106(X2)))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p115(X2)|~p116(X2)))&(p114(X2)|~p115(X2)))&(p113(X2)|~p114(X2)))&(p112(X2)|~p113(X2)))&(p111(X2)|~p112(X2)))&(p110(X2)|~p111(X2)))&(p109(X2)|~p110(X2)))&(p108(X2)|~p109(X2)))&(p107(X2)|~p108(X2)))&(p106(X2)|~p107(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), introduced(definition)).
% 177.70/23.00 fof(c_0_3, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p7(X2))))))))))))))))))))))))))))))))|~(((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|epred1_1(X2)))))))))))))))))))))))))))))))&~p101(X1))&p100(X1)))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_2])).
% 177.70/23.00 fof(c_0_4, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28, X29, X30, X31, X32, X33]:(((~r1(esk1_0,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|(~r1(X7,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|(~r1(X17,X18)|p7(X18))))))))))))))))&(((~r1(esk1_0,X19)|(~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|(~r1(X23,X24)|(~r1(X24,X25)|(~r1(X25,X26)|(~r1(X26,X27)|(~r1(X27,X28)|(~r1(X28,X29)|(~r1(X29,X30)|(~r1(X30,X31)|(~r1(X31,X32)|(~r1(X32,X33)|epred1_1(X33))))))))))))))))&~p101(esk1_0))&p100(esk1_0)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])).
% 177.70/23.00 fof(c_0_5, plain, ![X34]:(r1(X34,X34)), inference(variable_rename,[status(thm)],[reflexivity])).
% 177.70/23.00 cnf(c_0_6, negated_conjecture, (epred1_1(X15)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 177.70/23.00 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 177.70/23.00 cnf(c_0_8, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X2,X14)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 177.70/23.00 cnf(c_0_9, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X2,X13)), inference(spm,[status(thm)],[c_0_8, c_0_7])).
% 177.70/23.00 cnf(c_0_10, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X2,X12)), inference(spm,[status(thm)],[c_0_9, c_0_7])).
% 177.70/23.00 cnf(c_0_11, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X2,X11)), inference(spm,[status(thm)],[c_0_10, c_0_7])).
% 177.70/23.00 cnf(c_0_12, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X2,X10)), inference(spm,[status(thm)],[c_0_11, c_0_7])).
% 177.70/23.00 cnf(c_0_13, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X2,X9)), inference(spm,[status(thm)],[c_0_12, c_0_7])).
% 177.70/23.00 cnf(c_0_14, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X2,X8)), inference(spm,[status(thm)],[c_0_13, c_0_7])).
% 177.70/23.00 cnf(c_0_15, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X2,X7)), inference(spm,[status(thm)],[c_0_14, c_0_7])).
% 177.70/23.00 cnf(c_0_16, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X2,X6)), inference(spm,[status(thm)],[c_0_15, c_0_7])).
% 177.70/23.00 cnf(c_0_17, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X2,X5)), inference(spm,[status(thm)],[c_0_16, c_0_7])).
% 177.70/23.00 cnf(c_0_18, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_17, c_0_7])).
% 177.70/23.00 fof(c_0_19, plain, ![X2]:((epred1_1(X2)=>((((((((((((((((((((((((((((((((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p16(X1)&~p116(X1))&p115(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p16(X1)&~p116(X1))&p115(X1)))))))|~((~p115(X2)&p114(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p15(X1)&~p115(X1))&p114(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p15(X1)&~p115(X1))&p114(X1)))))))|~((~p114(X2)&p113(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p14(X1)&~p114(X1))&p113(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p14(X1)&~p114(X1))&p113(X1)))))))|~((~p113(X2)&p112(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p113(X1))&p112(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p113(X1))&p112(X1)))))))|~((~p112(X2)&p111(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p112(X1))&p111(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p12(X1)&~p112(X1))&p111(X1)))))))|~((~p111(X2)&p110(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p111(X1))&p110(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p111(X1))&p110(X1)))))))|~((~p110(X2)&p109(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p110(X1))&p109(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p10(X1)&~p110(X1))&p109(X1)))))))|~((~p109(X2)&p108(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p109(X1))&p108(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p109(X1))&p108(X1)))))))|~((~p108(X2)&p107(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)))))&((~(![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p107(X1))&p106(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p107(X1))&p106(X1)))))))|~((~p106(X2)&p105(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p16(X1)|~p115(X1)))|p16(X2))&(![X1]:((~r1(X2,X1)|p16(X1)|~p115(X1)))|~p16(X2)))|~p115(X2)))&(((![X1]:((~r1(X2,X1)|~p15(X1)|~p114(X1)))|p15(X2))&(![X1]:((~r1(X2,X1)|p15(X1)|~p114(X1)))|~p15(X2)))|~p114(X2)))&(((![X1]:((~r1(X2,X1)|~p14(X1)|~p113(X1)))|p14(X2))&(![X1]:((~r1(X2,X1)|p14(X1)|~p113(X1)))|~p14(X2)))|~p113(X2)))&(((![X1]:((~r1(X2,X1)|~p13(X1)|~p112(X1)))|p13(X2))&(![X1]:((~r1(X2,X1)|p13(X1)|~p112(X1)))|~p13(X2)))|~p112(X2)))&(((![X1]:((~r1(X2,X1)|~p12(X1)|~p111(X1)))|p12(X2))&(![X1]:((~r1(X2,X1)|p12(X1)|~p111(X1)))|~p12(X2)))|~p111(X2)))&(((![X1]:((~r1(X2,X1)|~p11(X1)|~p110(X1)))|p11(X2))&(![X1]:((~r1(X2,X1)|p11(X1)|~p110(X1)))|~p11(X2)))|~p110(X2)))&(((![X1]:((~r1(X2,X1)|~p10(X1)|~p109(X1)))|p10(X2))&(![X1]:((~r1(X2,X1)|p10(X1)|~p109(X1)))|~p10(X2)))|~p109(X2)))&(((![X1]:((~r1(X2,X1)|~p9(X1)|~p108(X1)))|p9(X2))&(![X1]:((~r1(X2,X1)|p9(X1)|~p108(X1)))|~p9(X2)))|~p108(X2)))&(((![X1]:((~r1(X2,X1)|~p8(X1)|~p107(X1)))|p8(X2))&(![X1]:((~r1(X2,X1)|p8(X1)|~p107(X1)))|~p8(X2)))|~p107(X2)))&(((![X1]:((~r1(X2,X1)|~p7(X1)|~p106(X1)))|p7(X2))&(![X1]:((~r1(X2,X1)|p7(X1)|~p106(X1)))|~p7(X2)))|~p106(X2)))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p115(X2)|~p116(X2)))&(p114(X2)|~p115(X2)))&(p113(X2)|~p114(X2)))&(p112(X2)|~p113(X2)))&(p111(X2)|~p112(X2)))&(p110(X2)|~p111(X2)))&(p109(X2)|~p110(X2)))&(p108(X2)|~p109(X2)))&(p107(X2)|~p108(X2)))&(p106(X2)|~p107(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 177.70/23.00 cnf(c_0_20, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_18, c_0_7])).
% 177.70/23.00 fof(c_0_21, plain, ![X35, X66, X67, X68, X69, X70, X71, X72, X73, X74, X75, X76, X77, X78, X79, X80, X81, X82, X83, X84, X85, X86, X87, X88, X89, X90, X91, X92, X93, X94, X95, X96, X97]:((((((((((((((((((((((((((((((((((((((((((((((((((r1(X35,esk2_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35))&(((~p16(esk2_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35))&(~p116(esk2_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35)))&(p115(esk2_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35))))&((r1(X35,esk3_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35))&(((p16(esk3_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35))&(~p116(esk3_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35)))&(p115(esk3_1(X35))|(p115(X35)|~p114(X35))|~epred1_1(X35)))))&(((r1(X35,esk4_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))&(((~p15(esk4_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))&(~p115(esk4_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35)))&(p114(esk4_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))))&((r1(X35,esk5_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))&(((p15(esk5_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))&(~p115(esk5_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35)))&(p114(esk5_1(X35))|(p114(X35)|~p113(X35))|~epred1_1(X35))))))&(((r1(X35,esk6_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))&(((~p14(esk6_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))&(~p114(esk6_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35)))&(p113(esk6_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))))&((r1(X35,esk7_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))&(((p14(esk7_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))&(~p114(esk7_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35)))&(p113(esk7_1(X35))|(p113(X35)|~p112(X35))|~epred1_1(X35))))))&(((r1(X35,esk8_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))&(((~p13(esk8_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))&(~p113(esk8_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35)))&(p112(esk8_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))))&((r1(X35,esk9_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))&(((p13(esk9_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))&(~p113(esk9_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35)))&(p112(esk9_1(X35))|(p112(X35)|~p111(X35))|~epred1_1(X35))))))&(((r1(X35,esk10_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))&(((~p12(esk10_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))&(~p112(esk10_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35)))&(p111(esk10_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))))&((r1(X35,esk11_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))&(((p12(esk11_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))&(~p112(esk11_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35)))&(p111(esk11_1(X35))|(p111(X35)|~p110(X35))|~epred1_1(X35))))))&(((r1(X35,esk12_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))&(((~p11(esk12_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))&(~p111(esk12_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35)))&(p110(esk12_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))))&((r1(X35,esk13_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))&(((p11(esk13_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))&(~p111(esk13_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35)))&(p110(esk13_1(X35))|(p110(X35)|~p109(X35))|~epred1_1(X35))))))&(((r1(X35,esk14_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))&(((~p10(esk14_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))&(~p110(esk14_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35)))&(p109(esk14_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))))&((r1(X35,esk15_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))&(((p10(esk15_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))&(~p110(esk15_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35)))&(p109(esk15_1(X35))|(p109(X35)|~p108(X35))|~epred1_1(X35))))))&(((r1(X35,esk16_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))&(((~p9(esk16_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))&(~p109(esk16_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35)))&(p108(esk16_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))))&((r1(X35,esk17_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))&(((p9(esk17_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))&(~p109(esk17_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35)))&(p108(esk17_1(X35))|(p108(X35)|~p107(X35))|~epred1_1(X35))))))&(((r1(X35,esk18_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))&(((~p8(esk18_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))&(~p108(esk18_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35)))&(p107(esk18_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))))&((r1(X35,esk19_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))&(((p8(esk19_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))&(~p108(esk19_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35)))&(p107(esk19_1(X35))|(p107(X35)|~p106(X35))|~epred1_1(X35))))))&(((r1(X35,esk20_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))&(((~p7(esk20_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))&(~p107(esk20_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35)))&(p106(esk20_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))))&((r1(X35,esk21_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))&(((p7(esk21_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))&(~p107(esk21_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35)))&(p106(esk21_1(X35))|(p106(X35)|~p105(X35))|~epred1_1(X35))))))&(((r1(X35,esk22_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))&(((~p6(esk22_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))&(~p106(esk22_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35)))&(p105(esk22_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))))&((r1(X35,esk23_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))&(((p6(esk23_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))&(~p106(esk23_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35)))&(p105(esk23_1(X35))|(p105(X35)|~p104(X35))|~epred1_1(X35))))))&(((r1(X35,esk24_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))&(((~p5(esk24_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))&(~p105(esk24_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35)))&(p104(esk24_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))))&((r1(X35,esk25_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))&(((p5(esk25_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))&(~p105(esk25_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35)))&(p104(esk25_1(X35))|(p104(X35)|~p103(X35))|~epred1_1(X35))))))&(((r1(X35,esk26_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))&(((~p4(esk26_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))&(~p104(esk26_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35)))&(p103(esk26_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))))&((r1(X35,esk27_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))&(((p4(esk27_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))&(~p104(esk27_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35)))&(p103(esk27_1(X35))|(p103(X35)|~p102(X35))|~epred1_1(X35))))))&(((r1(X35,esk28_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))&(((~p3(esk28_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))&(~p103(esk28_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35)))&(p102(esk28_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))))&((r1(X35,esk29_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))&(((p3(esk29_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))&(~p103(esk29_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35)))&(p102(esk29_1(X35))|(p102(X35)|~p101(X35))|~epred1_1(X35))))))&(((r1(X35,esk30_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))&(((~p2(esk30_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))&(~p102(esk30_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35)))&(p101(esk30_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))))&((r1(X35,esk31_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))&(((p2(esk31_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))&(~p102(esk31_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35)))&(p101(esk31_1(X35))|(p101(X35)|~p100(X35))|~epred1_1(X35))))))&((~r1(X35,X66)|~p16(X66)|~p115(X66)|p16(X35)|~p115(X35)|~epred1_1(X35))&(~r1(X35,X67)|p16(X67)|~p115(X67)|~p16(X35)|~p115(X35)|~epred1_1(X35))))&((~r1(X35,X68)|~p15(X68)|~p114(X68)|p15(X35)|~p114(X35)|~epred1_1(X35))&(~r1(X35,X69)|p15(X69)|~p114(X69)|~p15(X35)|~p114(X35)|~epred1_1(X35))))&((~r1(X35,X70)|~p14(X70)|~p113(X70)|p14(X35)|~p113(X35)|~epred1_1(X35))&(~r1(X35,X71)|p14(X71)|~p113(X71)|~p14(X35)|~p113(X35)|~epred1_1(X35))))&((~r1(X35,X72)|~p13(X72)|~p112(X72)|p13(X35)|~p112(X35)|~epred1_1(X35))&(~r1(X35,X73)|p13(X73)|~p112(X73)|~p13(X35)|~p112(X35)|~epred1_1(X35))))&((~r1(X35,X74)|~p12(X74)|~p111(X74)|p12(X35)|~p111(X35)|~epred1_1(X35))&(~r1(X35,X75)|p12(X75)|~p111(X75)|~p12(X35)|~p111(X35)|~epred1_1(X35))))&((~r1(X35,X76)|~p11(X76)|~p110(X76)|p11(X35)|~p110(X35)|~epred1_1(X35))&(~r1(X35,X77)|p11(X77)|~p110(X77)|~p11(X35)|~p110(X35)|~epred1_1(X35))))&((~r1(X35,X78)|~p10(X78)|~p109(X78)|p10(X35)|~p109(X35)|~epred1_1(X35))&(~r1(X35,X79)|p10(X79)|~p109(X79)|~p10(X35)|~p109(X35)|~epred1_1(X35))))&((~r1(X35,X80)|~p9(X80)|~p108(X80)|p9(X35)|~p108(X35)|~epred1_1(X35))&(~r1(X35,X81)|p9(X81)|~p108(X81)|~p9(X35)|~p108(X35)|~epred1_1(X35))))&((~r1(X35,X82)|~p8(X82)|~p107(X82)|p8(X35)|~p107(X35)|~epred1_1(X35))&(~r1(X35,X83)|p8(X83)|~p107(X83)|~p8(X35)|~p107(X35)|~epred1_1(X35))))&((~r1(X35,X84)|~p7(X84)|~p106(X84)|p7(X35)|~p106(X35)|~epred1_1(X35))&(~r1(X35,X85)|p7(X85)|~p106(X85)|~p7(X35)|~p106(X35)|~epred1_1(X35))))&((~r1(X35,X86)|~p6(X86)|~p105(X86)|p6(X35)|~p105(X35)|~epred1_1(X35))&(~r1(X35,X87)|p6(X87)|~p105(X87)|~p6(X35)|~p105(X35)|~epred1_1(X35))))&((~r1(X35,X88)|~p5(X88)|~p104(X88)|p5(X35)|~p104(X35)|~epred1_1(X35))&(~r1(X35,X89)|p5(X89)|~p104(X89)|~p5(X35)|~p104(X35)|~epred1_1(X35))))&((~r1(X35,X90)|~p4(X90)|~p103(X90)|p4(X35)|~p103(X35)|~epred1_1(X35))&(~r1(X35,X91)|p4(X91)|~p103(X91)|~p4(X35)|~p103(X35)|~epred1_1(X35))))&((~r1(X35,X92)|~p3(X92)|~p102(X92)|p3(X35)|~p102(X35)|~epred1_1(X35))&(~r1(X35,X93)|p3(X93)|~p102(X93)|~p3(X35)|~p102(X35)|~epred1_1(X35))))&((~r1(X35,X94)|~p2(X94)|~p101(X94)|p2(X35)|~p101(X35)|~epred1_1(X35))&(~r1(X35,X95)|p2(X95)|~p101(X95)|~p2(X35)|~p101(X35)|~epred1_1(X35))))&((~r1(X35,X96)|~p1(X96)|~p100(X96)|p1(X35)|~p100(X35)|~epred1_1(X35))&(~r1(X35,X97)|p1(X97)|~p100(X97)|~p1(X35)|~p100(X35)|~epred1_1(X35))))&(p115(X35)|~p116(X35)|~epred1_1(X35)))&(p114(X35)|~p115(X35)|~epred1_1(X35)))&(p113(X35)|~p114(X35)|~epred1_1(X35)))&(p112(X35)|~p113(X35)|~epred1_1(X35)))&(p111(X35)|~p112(X35)|~epred1_1(X35)))&(p110(X35)|~p111(X35)|~epred1_1(X35)))&(p109(X35)|~p110(X35)|~epred1_1(X35)))&(p108(X35)|~p109(X35)|~epred1_1(X35)))&(p107(X35)|~p108(X35)|~epred1_1(X35)))&(p106(X35)|~p107(X35)|~epred1_1(X35)))&(p105(X35)|~p106(X35)|~epred1_1(X35)))&(p104(X35)|~p105(X35)|~epred1_1(X35)))&(p103(X35)|~p104(X35)|~epred1_1(X35)))&(p102(X35)|~p103(X35)|~epred1_1(X35)))&(p101(X35)|~p102(X35)|~epred1_1(X35)))&(p100(X35)|~p101(X35)|~epred1_1(X35)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])])])).
% 177.70/23.00 cnf(c_0_22, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_20, c_0_7])).
% 177.70/23.00 cnf(c_0_23, negated_conjecture, (p7(X15)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 177.70/23.00 cnf(c_0_24, plain, (r1(X1,esk30_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_25, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 177.70/23.00 cnf(c_0_26, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 177.70/23.00 cnf(c_0_27, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_22, c_0_7])).
% 177.70/23.00 cnf(c_0_28, plain, (p7(X1)|~epred1_1(esk1_0)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X2,X14)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_29, negated_conjecture, (epred1_1(esk1_0)), inference(spm,[status(thm)],[c_0_27, c_0_7])).
% 177.70/23.00 cnf(c_0_30, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X2,X14)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 177.70/23.00 cnf(c_0_31, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X2,X13)), inference(spm,[status(thm)],[c_0_30, c_0_7])).
% 177.70/23.00 cnf(c_0_32, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X2,X12)), inference(spm,[status(thm)],[c_0_31, c_0_7])).
% 177.70/23.00 cnf(c_0_33, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X2,X11)), inference(spm,[status(thm)],[c_0_32, c_0_7])).
% 177.70/23.00 cnf(c_0_34, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X2,X10)), inference(spm,[status(thm)],[c_0_33, c_0_7])).
% 177.70/23.00 cnf(c_0_35, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X2,X9)), inference(spm,[status(thm)],[c_0_34, c_0_7])).
% 177.70/23.00 cnf(c_0_36, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X2,X8)), inference(spm,[status(thm)],[c_0_35, c_0_7])).
% 177.70/23.00 cnf(c_0_37, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X2,X7)), inference(spm,[status(thm)],[c_0_36, c_0_7])).
% 177.70/23.00 cnf(c_0_38, plain, (epred1_1(X1)|~epred1_1(esk1_0)|~r1(esk30_1(esk1_0),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_24]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_39, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X2,X6)), inference(spm,[status(thm)],[c_0_37, c_0_7])).
% 177.70/23.00 cnf(c_0_40, plain, (epred1_1(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_29])])).
% 177.70/23.00 cnf(c_0_41, plain, (epred1_1(X1)|~epred1_1(esk1_0)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_24]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_42, plain, (p7(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X2,X5)), inference(spm,[status(thm)],[c_0_39, c_0_7])).
% 177.70/23.00 cnf(c_0_43, plain, (r1(X1,esk29_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_44, plain, (epred1_1(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_24]), c_0_25])]), c_0_26]), c_0_29])])).
% 177.70/23.00 cnf(c_0_45, plain, (epred1_1(X1)|~r1(esk30_1(esk1_0),X1)), inference(spm,[status(thm)],[c_0_40, c_0_7])).
% 177.70/23.00 cnf(c_0_46, plain, (epred1_1(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_29])])).
% 177.70/23.00 cnf(c_0_47, plain, (epred1_1(X1)|~r1(esk30_1(esk1_0),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_24]), c_0_25])]), c_0_26]), c_0_29])])).
% 177.70/23.00 cnf(c_0_48, plain, (p102(esk30_1(esk1_0))|p7(X1)|~p101(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_44])])).
% 177.70/23.00 cnf(c_0_49, plain, (p101(esk30_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_50, plain, (epred1_1(esk29_1(esk30_1(esk1_0)))|p102(esk30_1(esk1_0))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_43]), c_0_44])])).
% 177.70/23.00 cnf(c_0_51, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~p101(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_43]), c_0_44])])).
% 177.70/23.00 cnf(c_0_52, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~p101(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_43]), c_0_44])])).
% 177.70/23.00 cnf(c_0_53, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~p101(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_43]), c_0_44])])).
% 177.70/23.00 cnf(c_0_54, plain, (p102(esk30_1(esk1_0))|p7(X1)|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_55, plain, (r1(X1,esk27_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_56, plain, (epred1_1(esk29_1(esk30_1(esk1_0)))|p102(esk30_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_57, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_58, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_59, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|~r1(esk29_1(esk30_1(esk1_0)),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_60, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p7(X1)|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_56])).
% 177.70/23.00 cnf(c_0_61, plain, (p102(esk29_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_62, plain, (epred1_1(esk27_1(esk29_1(esk30_1(esk1_0))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_55]), c_0_56])).
% 177.70/23.00 cnf(c_0_63, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_55]), c_0_56])).
% 177.70/23.00 cnf(c_0_64, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_55]), c_0_56])).
% 177.70/23.00 cnf(c_0_65, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p7(X1)|~p101(esk30_1(esk1_0))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_66, plain, (epred1_1(esk27_1(esk29_1(esk30_1(esk1_0))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_67, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p101(esk30_1(esk1_0))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_68, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p101(esk30_1(esk1_0))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_69, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p7(X1)|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_70, plain, (r1(X1,esk25_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_71, plain, (epred1_1(esk27_1(esk29_1(esk30_1(esk1_0))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_72, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_73, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~r1(esk27_1(esk29_1(esk30_1(esk1_0))),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_74, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p7(X1)|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_71])).
% 177.70/23.00 cnf(c_0_75, plain, (p103(esk27_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_76, plain, (epred1_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_70]), c_0_71])).
% 177.70/23.00 cnf(c_0_77, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_70]), c_0_71])).
% 177.70/23.00 cnf(c_0_78, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p7(X1)|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_79, plain, (epred1_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_80, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_81, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p7(X1)|~p101(esk30_1(esk1_0))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_82, plain, (epred1_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_83, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p101(esk30_1(esk1_0))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_84, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p7(X1)|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_85, plain, (r1(X1,esk23_1(X1))|p105(X1)|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_86, plain, (epred1_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_87, plain, (epred1_1(X1)|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~r1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_88, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p7(X1)|~p104(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~r1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_85]), c_0_86])).
% 177.70/23.00 cnf(c_0_89, plain, (p104(esk25_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_90, plain, (epred1_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p104(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_85]), c_0_86])).
% 177.70/23.00 cnf(c_0_91, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p7(X1)|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))|~r1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_89]), c_0_71])).
% 177.70/23.00 cnf(c_0_92, plain, (epred1_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_89]), c_0_71])).
% 177.70/23.00 cnf(c_0_93, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p7(X1)|~p102(esk29_1(esk30_1(esk1_0)))|~r1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_94, plain, (epred1_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_95, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p7(X1)|~p101(esk30_1(esk1_0))|~r1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_96, plain, (epred1_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_97, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p7(X1)|~r1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_98, plain, (r1(X1,esk20_1(X1))|p106(X1)|~p105(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_99, plain, (epred1_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_100, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))|~p105(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_98]), c_0_99])).
% 177.70/23.00 cnf(c_0_101, plain, (p105(esk23_1(X1))|p105(X1)|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_102, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))|~p104(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_101]), c_0_86])).
% 177.70/23.00 cnf(c_0_103, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_89]), c_0_71])).
% 177.70/23.00 cnf(c_0_104, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_105, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_106, plain, (p106(X1)|~p7(esk20_1(X1))|~p105(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_107, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|p7(esk20_1(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_108, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|~p105(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_107]), c_0_99])).
% 177.70/23.00 cnf(c_0_109, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|~p104(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_101]), c_0_86])).
% 177.70/23.00 cnf(c_0_110, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_109, c_0_89]), c_0_71])).
% 177.70/23.00 cnf(c_0_111, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_112, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_113, plain, (p105(X1)|~p106(esk23_1(X1))|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_114, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|p106(esk23_1(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0))))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_115, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p104(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_114]), c_0_86])).
% 177.70/23.00 cnf(c_0_116, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_89]), c_0_71])).
% 177.70/23.00 cnf(c_0_117, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_118, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_119, plain, (p104(X1)|~p105(esk25_1(X1))|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_120, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|p105(esk25_1(esk27_1(esk29_1(esk30_1(esk1_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_121, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p103(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_120]), c_0_71])).
% 177.70/23.00 cnf(c_0_122, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_75]), c_0_56])).
% 177.70/23.00 cnf(c_0_123, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_124, plain, (p103(X1)|~p104(esk27_1(X1))|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_125, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|p104(esk27_1(esk29_1(esk30_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_126, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p102(esk29_1(esk30_1(esk1_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_125]), c_0_56])).
% 177.70/23.00 cnf(c_0_127, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_61]), c_0_44])])).
% 177.70/23.00 cnf(c_0_128, plain, (p102(X1)|~p103(esk29_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_129, plain, (p102(esk30_1(esk1_0))|p103(esk29_1(esk30_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_130, plain, (p102(esk30_1(esk1_0))|~p101(esk30_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_44])])).
% 177.70/23.00 cnf(c_0_131, plain, (p101(X1)|~p102(esk30_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 177.70/23.00 cnf(c_0_132, plain, (p102(esk30_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_49]), c_0_29]), c_0_25])]), c_0_26])).
% 177.70/23.00 cnf(c_0_133, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131, c_0_132]), c_0_29]), c_0_25])]), c_0_26]), ['proof']).
% 177.70/23.00 % SZS output end Proof
% 177.70/23.00 % User time : 22.111 s
% 177.70/23.00 % System time : 0.059 s
% 177.70/23.00 % Total time : 22.170 s
% 177.70/23.00 % User time : 22.115 s
% 177.70/23.00 % System time : 0.065 s
% 177.70/23.00 % Total time : 22.180 s
% 177.70/23.00
%------------------------------------------------------------------------------