%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n015.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:27 AM UTC 2026
% Result : Theorem 81.09s 12.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 21:33:13 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.27/0.52 start to proof:theBenchmark.p
% 81.09/12.33 % Version : CSI_E---1.1
% 81.09/12.33 % Problem : theBenchmark.p
% 81.09/12.33 % Proof found!
% 81.09/12.33 % SZS status Theorem for theBenchmark.p
% 81.09/12.33 % SZS output start Proof
% 81.09/12.33 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|p7(X2))))|~(((![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)).
% 81.09/12.33 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity)).
% 81.09/12.33 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 81.09/12.33 fof(c_0_3, 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)).
% 81.09/12.34 fof(c_0_4, 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_3])).
% 81.09/12.34 fof(c_0_5, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|p7(X2))))|~(((![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_3])).
% 81.09/12.34 fof(c_0_6, plain, ![X5, X6, X7]:((~r1(X5,X6)|~r1(X6,X7)|r1(X5,X7))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])])).
% 81.09/12.34 fof(c_0_7, plain, ![X11, X42, X43, X44, X45, X46, X47, X48, X49, X50, X51, X52, X53, X54, X55, X56, X57, X58, X59, X60, X61, X62, X63, X64, X65, X66, X67, X68, X69, X70, X71, X72, X73]:((((((((((((((((((((((((((((((((((((((((((((((((((r1(X11,esk2_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11))&(((~p16(esk2_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11))&(~p116(esk2_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11)))&(p115(esk2_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11))))&((r1(X11,esk3_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11))&(((p16(esk3_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11))&(~p116(esk3_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11)))&(p115(esk3_1(X11))|(p115(X11)|~p114(X11))|~epred1_1(X11)))))&(((r1(X11,esk4_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))&(((~p15(esk4_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))&(~p115(esk4_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11)))&(p114(esk4_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))))&((r1(X11,esk5_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))&(((p15(esk5_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))&(~p115(esk5_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11)))&(p114(esk5_1(X11))|(p114(X11)|~p113(X11))|~epred1_1(X11))))))&(((r1(X11,esk6_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))&(((~p14(esk6_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))&(~p114(esk6_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11)))&(p113(esk6_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))))&((r1(X11,esk7_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))&(((p14(esk7_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))&(~p114(esk7_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11)))&(p113(esk7_1(X11))|(p113(X11)|~p112(X11))|~epred1_1(X11))))))&(((r1(X11,esk8_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))&(((~p13(esk8_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))&(~p113(esk8_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11)))&(p112(esk8_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))))&((r1(X11,esk9_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))&(((p13(esk9_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))&(~p113(esk9_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11)))&(p112(esk9_1(X11))|(p112(X11)|~p111(X11))|~epred1_1(X11))))))&(((r1(X11,esk10_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))&(((~p12(esk10_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))&(~p112(esk10_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11)))&(p111(esk10_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))))&((r1(X11,esk11_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))&(((p12(esk11_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))&(~p112(esk11_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11)))&(p111(esk11_1(X11))|(p111(X11)|~p110(X11))|~epred1_1(X11))))))&(((r1(X11,esk12_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(((~p11(esk12_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(~p111(esk12_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11)))&(p110(esk12_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))))&((r1(X11,esk13_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(((p11(esk13_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))&(~p111(esk13_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11)))&(p110(esk13_1(X11))|(p110(X11)|~p109(X11))|~epred1_1(X11))))))&(((r1(X11,esk14_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(((~p10(esk14_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(~p110(esk14_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11)))&(p109(esk14_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))))&((r1(X11,esk15_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(((p10(esk15_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))&(~p110(esk15_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11)))&(p109(esk15_1(X11))|(p109(X11)|~p108(X11))|~epred1_1(X11))))))&(((r1(X11,esk16_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(((~p9(esk16_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(~p109(esk16_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11)))&(p108(esk16_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))))&((r1(X11,esk17_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(((p9(esk17_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))&(~p109(esk17_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11)))&(p108(esk17_1(X11))|(p108(X11)|~p107(X11))|~epred1_1(X11))))))&(((r1(X11,esk18_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(((~p8(esk18_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(~p108(esk18_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11)))&(p107(esk18_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))))&((r1(X11,esk19_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(((p8(esk19_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))&(~p108(esk19_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11)))&(p107(esk19_1(X11))|(p107(X11)|~p106(X11))|~epred1_1(X11))))))&(((r1(X11,esk20_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(((~p7(esk20_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(~p107(esk20_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11)))&(p106(esk20_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))))&((r1(X11,esk21_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(((p7(esk21_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))&(~p107(esk21_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11)))&(p106(esk21_1(X11))|(p106(X11)|~p105(X11))|~epred1_1(X11))))))&(((r1(X11,esk22_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((~p6(esk22_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk22_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk22_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))))&((r1(X11,esk23_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(((p6(esk23_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))&(~p106(esk23_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11)))&(p105(esk23_1(X11))|(p105(X11)|~p104(X11))|~epred1_1(X11))))))&(((r1(X11,esk24_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((~p5(esk24_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk24_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk24_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))&((r1(X11,esk25_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(((p5(esk25_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))&(~p105(esk25_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11)))&(p104(esk25_1(X11))|(p104(X11)|~p103(X11))|~epred1_1(X11))))))&(((r1(X11,esk26_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((~p4(esk26_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk26_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk26_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))&((r1(X11,esk27_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(((p4(esk27_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))&(~p104(esk27_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11)))&(p103(esk27_1(X11))|(p103(X11)|~p102(X11))|~epred1_1(X11))))))&(((r1(X11,esk28_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((~p3(esk28_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk28_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk28_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))&((r1(X11,esk29_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(((p3(esk29_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))&(~p103(esk29_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11)))&(p102(esk29_1(X11))|(p102(X11)|~p101(X11))|~epred1_1(X11))))))&(((r1(X11,esk30_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((~p2(esk30_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk30_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk30_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))&((r1(X11,esk31_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(((p2(esk31_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))&(~p102(esk31_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11)))&(p101(esk31_1(X11))|(p101(X11)|~p100(X11))|~epred1_1(X11))))))&((~r1(X11,X42)|~p16(X42)|~p115(X42)|p16(X11)|~p115(X11)|~epred1_1(X11))&(~r1(X11,X43)|p16(X43)|~p115(X43)|~p16(X11)|~p115(X11)|~epred1_1(X11))))&((~r1(X11,X44)|~p15(X44)|~p114(X44)|p15(X11)|~p114(X11)|~epred1_1(X11))&(~r1(X11,X45)|p15(X45)|~p114(X45)|~p15(X11)|~p114(X11)|~epred1_1(X11))))&((~r1(X11,X46)|~p14(X46)|~p113(X46)|p14(X11)|~p113(X11)|~epred1_1(X11))&(~r1(X11,X47)|p14(X47)|~p113(X47)|~p14(X11)|~p113(X11)|~epred1_1(X11))))&((~r1(X11,X48)|~p13(X48)|~p112(X48)|p13(X11)|~p112(X11)|~epred1_1(X11))&(~r1(X11,X49)|p13(X49)|~p112(X49)|~p13(X11)|~p112(X11)|~epred1_1(X11))))&((~r1(X11,X50)|~p12(X50)|~p111(X50)|p12(X11)|~p111(X11)|~epred1_1(X11))&(~r1(X11,X51)|p12(X51)|~p111(X51)|~p12(X11)|~p111(X11)|~epred1_1(X11))))&((~r1(X11,X52)|~p11(X52)|~p110(X52)|p11(X11)|~p110(X11)|~epred1_1(X11))&(~r1(X11,X53)|p11(X53)|~p110(X53)|~p11(X11)|~p110(X11)|~epred1_1(X11))))&((~r1(X11,X54)|~p10(X54)|~p109(X54)|p10(X11)|~p109(X11)|~epred1_1(X11))&(~r1(X11,X55)|p10(X55)|~p109(X55)|~p10(X11)|~p109(X11)|~epred1_1(X11))))&((~r1(X11,X56)|~p9(X56)|~p108(X56)|p9(X11)|~p108(X11)|~epred1_1(X11))&(~r1(X11,X57)|p9(X57)|~p108(X57)|~p9(X11)|~p108(X11)|~epred1_1(X11))))&((~r1(X11,X58)|~p8(X58)|~p107(X58)|p8(X11)|~p107(X11)|~epred1_1(X11))&(~r1(X11,X59)|p8(X59)|~p107(X59)|~p8(X11)|~p107(X11)|~epred1_1(X11))))&((~r1(X11,X60)|~p7(X60)|~p106(X60)|p7(X11)|~p106(X11)|~epred1_1(X11))&(~r1(X11,X61)|p7(X61)|~p106(X61)|~p7(X11)|~p106(X11)|~epred1_1(X11))))&((~r1(X11,X62)|~p6(X62)|~p105(X62)|p6(X11)|~p105(X11)|~epred1_1(X11))&(~r1(X11,X63)|p6(X63)|~p105(X63)|~p6(X11)|~p105(X11)|~epred1_1(X11))))&((~r1(X11,X64)|~p5(X64)|~p104(X64)|p5(X11)|~p104(X11)|~epred1_1(X11))&(~r1(X11,X65)|p5(X65)|~p104(X65)|~p5(X11)|~p104(X11)|~epred1_1(X11))))&((~r1(X11,X66)|~p4(X66)|~p103(X66)|p4(X11)|~p103(X11)|~epred1_1(X11))&(~r1(X11,X67)|p4(X67)|~p103(X67)|~p4(X11)|~p103(X11)|~epred1_1(X11))))&((~r1(X11,X68)|~p3(X68)|~p102(X68)|p3(X11)|~p102(X11)|~epred1_1(X11))&(~r1(X11,X69)|p3(X69)|~p102(X69)|~p3(X11)|~p102(X11)|~epred1_1(X11))))&((~r1(X11,X70)|~p2(X70)|~p101(X70)|p2(X11)|~p101(X11)|~epred1_1(X11))&(~r1(X11,X71)|p2(X71)|~p101(X71)|~p2(X11)|~p101(X11)|~epred1_1(X11))))&((~r1(X11,X72)|~p1(X72)|~p100(X72)|p1(X11)|~p100(X11)|~epred1_1(X11))&(~r1(X11,X73)|p1(X73)|~p100(X73)|~p1(X11)|~p100(X11)|~epred1_1(X11))))&(p115(X11)|~p116(X11)|~epred1_1(X11)))&(p114(X11)|~p115(X11)|~epred1_1(X11)))&(p113(X11)|~p114(X11)|~epred1_1(X11)))&(p112(X11)|~p113(X11)|~epred1_1(X11)))&(p111(X11)|~p112(X11)|~epred1_1(X11)))&(p110(X11)|~p111(X11)|~epred1_1(X11)))&(p109(X11)|~p110(X11)|~epred1_1(X11)))&(p108(X11)|~p109(X11)|~epred1_1(X11)))&(p107(X11)|~p108(X11)|~epred1_1(X11)))&(p106(X11)|~p107(X11)|~epred1_1(X11)))&(p105(X11)|~p106(X11)|~epred1_1(X11)))&(p104(X11)|~p105(X11)|~epred1_1(X11)))&(p103(X11)|~p104(X11)|~epred1_1(X11)))&(p102(X11)|~p103(X11)|~epred1_1(X11)))&(p101(X11)|~p102(X11)|~epred1_1(X11)))&(p100(X11)|~p101(X11)|~epred1_1(X11)))), 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_4])])])])])])).
% 81.09/12.34 fof(c_0_8, negated_conjecture, ![X9, X10]:(((~r1(esk1_0,X9)|p7(X9))&(((~r1(esk1_0,X10)|epred1_1(X10))&~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_5])])])])])).
% 81.09/12.34 fof(c_0_9, plain, ![X4]:(r1(X4,X4)), inference(variable_rename,[status(thm)],[reflexivity])).
% 81.09/12.34 cnf(c_0_10, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 81.09/12.34 cnf(c_0_11, plain, (r1(X1,esk29_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_12, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 81.09/12.34 cnf(c_0_13, plain, (r1(X1,esk31_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_14, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 81.09/12.34 cnf(c_0_15, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 81.09/12.34 cnf(c_0_16, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 81.09/12.34 cnf(c_0_17, plain, (p102(X1)|r1(X2,esk29_1(X1))|~epred1_1(X1)|~p101(X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 81.09/12.34 cnf(c_0_18, plain, (p101(esk31_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_19, plain, (p101(X1)|~p102(esk31_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_20, negated_conjecture, (epred1_1(esk31_1(esk1_0))|~epred1_1(esk1_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_21, negated_conjecture, (epred1_1(esk1_0)), inference(spm,[status(thm)],[c_0_12, c_0_16])).
% 81.09/12.34 cnf(c_0_22, plain, (r1(X1,esk27_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_23, plain, (p101(X1)|r1(X1,esk29_1(esk31_1(X1)))|~epred1_1(esk31_1(X1))|~epred1_1(X1)|~p100(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_13]), c_0_18]), c_0_19])).
% 81.09/12.34 cnf(c_0_24, negated_conjecture, (epred1_1(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_21])])).
% 81.09/12.34 cnf(c_0_25, plain, (p103(X1)|r1(X2,esk27_1(X1))|~epred1_1(X1)|~p102(X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_22])).
% 81.09/12.34 cnf(c_0_26, plain, (p102(esk29_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_27, plain, (p102(X1)|~p103(esk29_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_28, negated_conjecture, (r1(esk1_0,esk29_1(esk31_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_23, c_0_24]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_29, plain, (p102(X1)|r1(X1,esk27_1(esk29_1(X1)))|~epred1_1(esk29_1(X1))|~epred1_1(X1)|~p101(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_11]), c_0_26]), c_0_27])).
% 81.09/12.34 cnf(c_0_30, negated_conjecture, (epred1_1(esk29_1(esk31_1(esk1_0)))), inference(spm,[status(thm)],[c_0_12, c_0_28])).
% 81.09/12.34 cnf(c_0_31, negated_conjecture, (p102(esk31_1(esk1_0))|r1(esk31_1(esk1_0),esk27_1(esk29_1(esk31_1(esk1_0))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_24])])).
% 81.09/12.34 cnf(c_0_32, plain, (p102(esk31_1(esk1_0))|r1(esk31_1(esk1_0),esk27_1(esk29_1(esk31_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_31, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_33, plain, (r1(X1,esk24_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_34, plain, (p102(esk31_1(esk1_0))|r1(X1,esk27_1(esk29_1(esk31_1(esk1_0))))|~r1(X1,esk31_1(esk1_0))), inference(spm,[status(thm)],[c_0_10, c_0_32])).
% 81.09/12.34 cnf(c_0_35, plain, (p104(X1)|r1(X2,esk24_1(X1))|~epred1_1(X1)|~p103(X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_33])).
% 81.09/12.34 cnf(c_0_36, plain, (p103(esk27_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_37, plain, (p103(X1)|~p104(esk27_1(X1))|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_38, plain, (p102(esk31_1(esk1_0))|r1(esk1_0,esk27_1(esk29_1(esk31_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_34, c_0_13]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_39, plain, (p103(X1)|r1(X1,esk24_1(esk27_1(X1)))|~epred1_1(esk27_1(X1))|~epred1_1(X1)|~p102(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_22]), c_0_36]), c_0_37])).
% 81.09/12.34 cnf(c_0_40, negated_conjecture, (epred1_1(esk27_1(esk29_1(esk31_1(esk1_0))))|p102(esk31_1(esk1_0))), inference(spm,[status(thm)],[c_0_12, c_0_38])).
% 81.09/12.34 cnf(c_0_41, negated_conjecture, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|r1(esk29_1(esk31_1(esk1_0)),esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_30])])).
% 81.09/12.34 cnf(c_0_42, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|r1(esk29_1(esk31_1(esk1_0)),esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_43, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|r1(esk29_1(esk31_1(esk1_0)),esk24_1(esk27_1(esk29_1(esk31_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_42, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_44, plain, (r1(X1,esk22_1(X1))|p105(X1)|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_45, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|r1(X1,esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~r1(X1,esk29_1(esk31_1(esk1_0)))), inference(spm,[status(thm)],[c_0_10, c_0_43])).
% 81.09/12.34 cnf(c_0_46, plain, (p105(X1)|r1(X2,esk22_1(X1))|~epred1_1(X1)|~p104(X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_44])).
% 81.09/12.34 cnf(c_0_47, plain, (p104(esk24_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_48, plain, (p104(X1)|~p105(esk24_1(X1))|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_49, negated_conjecture, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|r1(esk1_0,esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))), inference(spm,[status(thm)],[c_0_45, c_0_28])).
% 81.09/12.34 cnf(c_0_50, plain, (p104(X1)|r1(X1,esk22_1(esk24_1(X1)))|~epred1_1(esk24_1(X1))|~epred1_1(X1)|~p103(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_33]), c_0_47]), c_0_48])).
% 81.09/12.34 cnf(c_0_51, negated_conjecture, (epred1_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))), inference(spm,[status(thm)],[c_0_12, c_0_49])).
% 81.09/12.34 cnf(c_0_52, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(esk27_1(esk29_1(esk31_1(esk1_0))),esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p103(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_40])).
% 81.09/12.34 cnf(c_0_53, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(esk27_1(esk29_1(esk31_1(esk1_0))),esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_36]), c_0_30])])).
% 81.09/12.34 cnf(c_0_54, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(esk27_1(esk29_1(esk31_1(esk1_0))),esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_55, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(esk27_1(esk29_1(esk31_1(esk1_0))),esk22_1(esk24_1(esk27_1(esk29_1(esk31_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_54, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_56, plain, (r1(X1,esk20_1(X1))|p106(X1)|~p105(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_57, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(X1,esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~r1(X1,esk27_1(esk29_1(esk31_1(esk1_0))))), inference(spm,[status(thm)],[c_0_10, c_0_55])).
% 81.09/12.34 cnf(c_0_58, plain, (p106(X1)|r1(X2,esk20_1(X1))|~epred1_1(X1)|~p105(X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_10, c_0_56])).
% 81.09/12.34 cnf(c_0_59, plain, (p105(esk22_1(X1))|p105(X1)|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_60, plain, (p105(X1)|~p106(esk22_1(X1))|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_61, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|r1(esk1_0,esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))), inference(spm,[status(thm)],[c_0_57, c_0_38])).
% 81.09/12.34 cnf(c_0_62, plain, (p105(X1)|r1(X1,esk20_1(esk22_1(X1)))|~epred1_1(esk22_1(X1))|~epred1_1(X1)|~p104(X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_44]), c_0_59]), c_0_60])).
% 81.09/12.34 cnf(c_0_63, negated_conjecture, (epred1_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(spm,[status(thm)],[c_0_12, c_0_61])).
% 81.09/12.34 cnf(c_0_64, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))),esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))|~p104(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_51])).
% 81.09/12.34 cnf(c_0_65, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))),esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))|~p103(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_47]), c_0_40])).
% 81.09/12.34 cnf(c_0_66, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))),esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_36]), c_0_30])])).
% 81.09/12.34 cnf(c_0_67, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))),esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_68, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))),esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_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_67, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_69, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(X1,esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))|~r1(X1,esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))), inference(spm,[status(thm)],[c_0_10, c_0_68])).
% 81.09/12.34 cnf(c_0_70, negated_conjecture, (p7(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 81.09/12.34 cnf(c_0_71, negated_conjecture, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|r1(esk1_0,esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))), inference(spm,[status(thm)],[c_0_69, c_0_49])).
% 81.09/12.34 cnf(c_0_72, plain, (p106(X1)|~p7(esk20_1(X1))|~p105(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 81.09/12.34 cnf(c_0_73, negated_conjecture, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p7(esk20_1(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))))), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 81.09/12.34 cnf(c_0_74, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p105(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_63])).
% 81.09/12.34 cnf(c_0_75, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p104(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_59]), c_0_51])).
% 81.09/12.34 cnf(c_0_76, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p103(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_47]), c_0_40])).
% 81.09/12.34 cnf(c_0_77, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_36]), c_0_30])])).
% 81.09/12.34 cnf(c_0_78, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0))))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_79, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|p106(esk22_1(esk24_1(esk27_1(esk29_1(esk31_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_78, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_80, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p104(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_79]), c_0_51])).
% 81.09/12.34 cnf(c_0_81, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p103(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_47]), c_0_40])).
% 81.09/12.34 cnf(c_0_82, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_36]), c_0_30])])).
% 81.09/12.34 cnf(c_0_83, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_1(esk1_0)))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_84, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|p105(esk24_1(esk27_1(esk29_1(esk31_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_83, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_85, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|~p103(esk27_1(esk29_1(esk31_1(esk1_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_84]), c_0_40])).
% 81.09/12.34 cnf(c_0_86, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_36]), c_0_30])])).
% 81.09/12.34 cnf(c_0_87, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_1(esk1_0))))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_88, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|p104(esk27_1(esk29_1(esk31_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_87, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_89, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|~p102(esk29_1(esk31_1(esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_88]), c_0_30])])).
% 81.09/12.34 cnf(c_0_90, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_1(esk1_0)))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_26]), c_0_24])])).
% 81.09/12.34 cnf(c_0_91, plain, (p102(esk31_1(esk1_0))|p103(esk29_1(esk31_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_90, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_92, plain, (p102(esk31_1(esk1_0))|~p101(esk31_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_91]), c_0_24])])).
% 81.09/12.34 cnf(c_0_93, plain, (p102(esk31_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_92, c_0_18]), c_0_21]), c_0_14])]), c_0_15])).
% 81.09/12.34 cnf(c_0_94, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_93]), c_0_21]), c_0_14])]), c_0_15]), ['proof']).
% 81.09/12.34 % SZS output end Proof
% 81.09/12.34 % User time : 11.420 s
% 81.09/12.34 % System time : 0.039 s
% 81.09/12.34 % Total time : 11.459 s
% 81.09/12.34 % User time : 57.204 s
% 81.09/12.34 % System time : 0.105 s
% 81.09/12.34 % Total time : 57.310 s
% 81.09/12.34
%------------------------------------------------------------------------------