%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL656+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n016.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 1.10s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL656+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n016.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 5 18:58:15 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark.p
% 1.10/0.59 % Version : CSI_E---1.1
% 1.10/0.59 % Problem : theBenchmark.p
% 1.10/0.59 % Proof found!
% 1.10/0.59 % SZS status Theorem for theBenchmark.p
% 1.10/0.59 % SZS output start Proof
% 1.10/0.59 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))|p5(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))|~(((~(p11(X2))&~(p111(X2)))&p110(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p11(X2)&~(p111(X2)))&p110(X2)))))))|~((~(p110(X1))&p109(X1))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p10(X2))&~(p110(X2)))&p109(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p10(X2)&~(p110(X2)))&p109(X2)))))))|~((~(p109(X1))&p108(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p9(X2))&~(p109(X2)))&p108(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p9(X2)&~(p109(X2)))&p108(X2)))))))|~((~(p108(X1))&p107(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p8(X2))&~(p108(X2)))&p107(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p8(X2)&~(p108(X2)))&p107(X2)))))))|~((~(p107(X1))&p106(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p7(X2))&~(p107(X2)))&p106(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p7(X2)&~(p107(X2)))&p106(X2)))))))|~((~(p106(X1))&p105(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p6(X2))&~(p106(X2)))&p105(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p106(X2)))&p105(X2)))))))|~((~(p105(X1))&p104(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p5(X2))&~(p105(X2)))&p104(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p5(X2)&~(p105(X2)))&p104(X2)))))))|~((~(p104(X1))&p103(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p4(X2))&~(p104(X2)))&p103(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p104(X2)))&p103(X2)))))))|~((~(p103(X1))&p102(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p3(X2))&~(p103(X2)))&p102(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p3(X2)&~(p103(X2)))&p102(X2)))))))|~((~(p102(X1))&p101(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p2(X2))&~(p102(X2)))&p101(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p102(X2)))&p101(X2)))))))|~((~(p101(X1))&p100(X1)))))&(((![X2]:((~(r1(X1,X2))|~(p11(X2))|~(p110(X2))))|p11(X1))&(![X2]:((~(r1(X1,X2))|p11(X2)|~(p110(X2))))|~(p11(X1))))|~(p110(X1))))&(((![X2]:((~(r1(X1,X2))|~(p10(X2))|~(p109(X2))))|p10(X1))&(![X2]:((~(r1(X1,X2))|p10(X2)|~(p109(X2))))|~(p10(X1))))|~(p109(X1))))&(((![X2]:((~(r1(X1,X2))|~(p9(X2))|~(p108(X2))))|p9(X1))&(![X2]:((~(r1(X1,X2))|p9(X2)|~(p108(X2))))|~(p9(X1))))|~(p108(X1))))&(((![X2]:((~(r1(X1,X2))|~(p8(X2))|~(p107(X2))))|p8(X1))&(![X2]:((~(r1(X1,X2))|p8(X2)|~(p107(X2))))|~(p8(X1))))|~(p107(X1))))&(((![X2]:((~(r1(X1,X2))|~(p7(X2))|~(p106(X2))))|p7(X1))&(![X2]:((~(r1(X1,X2))|p7(X2)|~(p106(X2))))|~(p7(X1))))|~(p106(X1))))&(((![X2]:((~(r1(X1,X2))|~(p6(X2))|~(p105(X2))))|p6(X1))&(![X2]:((~(r1(X1,X2))|p6(X2)|~(p105(X2))))|~(p6(X1))))|~(p105(X1))))&(((![X2]:((~(r1(X1,X2))|~(p5(X2))|~(p104(X2))))|p5(X1))&(![X2]:((~(r1(X1,X2))|p5(X2)|~(p104(X2))))|~(p5(X1))))|~(p104(X1))))&(((![X2]:((~(r1(X1,X2))|~(p4(X2))|~(p103(X2))))|p4(X1))&(![X2]:((~(r1(X1,X2))|p4(X2)|~(p103(X2))))|~(p4(X1))))|~(p103(X1))))&(((![X2]:((~(r1(X1,X2))|~(p3(X2))|~(p102(X2))))|p3(X1))&(![X2]:((~(r1(X1,X2))|p3(X2)|~(p102(X2))))|~(p3(X1))))|~(p102(X1))))&(((![X2]:((~(r1(X1,X2))|~(p2(X2))|~(p101(X2))))|p2(X1))&(![X2]:((~(r1(X1,X2))|p2(X2)|~(p101(X2))))|~(p2(X1))))|~(p101(X1))))&(((![X2]:((~(r1(X1,X2))|~(p1(X2))|~(p100(X2))))|p1(X1))&(![X2]:((~(r1(X1,X2))|p1(X2)|~(p100(X2))))|~(p1(X1))))|~(p100(X1))))&(p110(X1)|~(p111(X1))))&(p109(X1)|~(p110(X1))))&(p108(X1)|~(p109(X1))))&(p107(X1)|~(p108(X1))))&(p106(X1)|~(p107(X1))))&(p105(X1)|~(p106(X1))))&(p104(X1)|~(p105(X1))))&(p103(X1)|~(p104(X1))))&(p102(X1)|~(p103(X1))))&(p101(X1)|~(p102(X1))))&(p100(X1)|~(p101(X1))))))))))))))))))))))))&~(p101(X1)))&p100(X1))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 1.10/0.59 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 1.10/0.59 fof(c_0_2, plain, ![X1]:((epred1_1(X1)<=>(((((((((((((((((((((((((((((((((~(![X2]:((~r1(X1,X2)|~(((~p11(X2)&~p111(X2))&p110(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p11(X2)&~p111(X2))&p110(X2)))))))|~((~p110(X1)&p109(X1))))&((~(![X2]:((~r1(X1,X2)|~(((~p10(X2)&~p110(X2))&p109(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p110(X2))&p109(X2)))))))|~((~p109(X1)&p108(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p9(X2)&~p109(X2))&p108(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p9(X2)&~p109(X2))&p108(X2)))))))|~((~p108(X1)&p107(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p8(X2)&~p108(X2))&p107(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p108(X2))&p107(X2)))))))|~((~p107(X1)&p106(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p7(X2)&~p107(X2))&p106(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p7(X2)&~p107(X2))&p106(X2)))))))|~((~p106(X1)&p105(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p6(X2)&~p106(X2))&p105(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p106(X2))&p105(X2)))))))|~((~p105(X1)&p104(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p5(X2)&~p105(X2))&p104(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p5(X2)&~p105(X2))&p104(X2)))))))|~((~p104(X1)&p103(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p4(X2)&~p104(X2))&p103(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p104(X2))&p103(X2)))))))|~((~p103(X1)&p102(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p3(X2)&~p103(X2))&p102(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p3(X2)&~p103(X2))&p102(X2)))))))|~((~p102(X1)&p101(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p2(X2)&~p102(X2))&p101(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p102(X2))&p101(X2)))))))|~((~p101(X1)&p100(X1)))))&(((![X2]:((~r1(X1,X2)|~p11(X2)|~p110(X2)))|p11(X1))&(![X2]:((~r1(X1,X2)|p11(X2)|~p110(X2)))|~p11(X1)))|~p110(X1)))&(((![X2]:((~r1(X1,X2)|~p10(X2)|~p109(X2)))|p10(X1))&(![X2]:((~r1(X1,X2)|p10(X2)|~p109(X2)))|~p10(X1)))|~p109(X1)))&(((![X2]:((~r1(X1,X2)|~p9(X2)|~p108(X2)))|p9(X1))&(![X2]:((~r1(X1,X2)|p9(X2)|~p108(X2)))|~p9(X1)))|~p108(X1)))&(((![X2]:((~r1(X1,X2)|~p8(X2)|~p107(X2)))|p8(X1))&(![X2]:((~r1(X1,X2)|p8(X2)|~p107(X2)))|~p8(X1)))|~p107(X1)))&(((![X2]:((~r1(X1,X2)|~p7(X2)|~p106(X2)))|p7(X1))&(![X2]:((~r1(X1,X2)|p7(X2)|~p106(X2)))|~p7(X1)))|~p106(X1)))&(((![X2]:((~r1(X1,X2)|~p6(X2)|~p105(X2)))|p6(X1))&(![X2]:((~r1(X1,X2)|p6(X2)|~p105(X2)))|~p6(X1)))|~p105(X1)))&(((![X2]:((~r1(X1,X2)|~p5(X2)|~p104(X2)))|p5(X1))&(![X2]:((~r1(X1,X2)|p5(X2)|~p104(X2)))|~p5(X1)))|~p104(X1)))&(((![X2]:((~r1(X1,X2)|~p4(X2)|~p103(X2)))|p4(X1))&(![X2]:((~r1(X1,X2)|p4(X2)|~p103(X2)))|~p4(X1)))|~p103(X1)))&(((![X2]:((~r1(X1,X2)|~p3(X2)|~p102(X2)))|p3(X1))&(![X2]:((~r1(X1,X2)|p3(X2)|~p102(X2)))|~p3(X1)))|~p102(X1)))&(((![X2]:((~r1(X1,X2)|~p2(X2)|~p101(X2)))|p2(X1))&(![X2]:((~r1(X1,X2)|p2(X2)|~p101(X2)))|~p2(X1)))|~p101(X1)))&(((![X2]:((~r1(X1,X2)|~p1(X2)|~p100(X2)))|p1(X1))&(![X2]:((~r1(X1,X2)|p1(X2)|~p100(X2)))|~p1(X1)))|~p100(X1)))&(p110(X1)|~p111(X1)))&(p109(X1)|~p110(X1)))&(p108(X1)|~p109(X1)))&(p107(X1)|~p108(X1)))&(p106(X1)|~p107(X1)))&(p105(X1)|~p106(X1)))&(p104(X1)|~p105(X1)))&(p103(X1)|~p104(X1)))&(p102(X1)|~p103(X1)))&(p101(X1)|~p102(X1)))&(p100(X1)|~p101(X1))))), introduced(definition)).
% 1.10/0.59 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)|p5(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)|epred1_1(X1)))))))))))))))))))))&~p101(X1))&p100(X1)))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_2])).
% 1.10/0.59 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]:(((~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)|p5(X13)))))))))))&(((~r1(esk1_0,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|(~r1(X17,X18)|(~r1(X18,X19)|(~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|epred1_1(X23)))))))))))&~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])])])])])).
% 1.10/0.59 fof(c_0_5, plain, ![X24]:(r1(X24,X24)), inference(variable_rename,[status(thm)],[reflexivity])).
% 1.10/0.59 cnf(c_0_6, negated_conjecture, (epred1_1(X10)|~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)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.10/0.59 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 1.10/0.59 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(X2,X9)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 1.10/0.59 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(X2,X8)), inference(spm,[status(thm)],[c_0_8, c_0_7])).
% 1.10/0.59 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(X2,X7)), inference(spm,[status(thm)],[c_0_9, c_0_7])).
% 1.10/0.59 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(X2,X6)), inference(spm,[status(thm)],[c_0_10, c_0_7])).
% 1.10/0.59 cnf(c_0_12, 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_11, c_0_7])).
% 1.10/0.59 cnf(c_0_13, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_12, c_0_7])).
% 1.10/0.59 cnf(c_0_14, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_13, c_0_7])).
% 1.10/0.59 fof(c_0_15, plain, ![X1]:((epred1_1(X1)=>(((((((((((((((((((((((((((((((((~(![X2]:((~r1(X1,X2)|~(((~p11(X2)&~p111(X2))&p110(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p11(X2)&~p111(X2))&p110(X2)))))))|~((~p110(X1)&p109(X1))))&((~(![X2]:((~r1(X1,X2)|~(((~p10(X2)&~p110(X2))&p109(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p110(X2))&p109(X2)))))))|~((~p109(X1)&p108(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p9(X2)&~p109(X2))&p108(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p9(X2)&~p109(X2))&p108(X2)))))))|~((~p108(X1)&p107(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p8(X2)&~p108(X2))&p107(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p108(X2))&p107(X2)))))))|~((~p107(X1)&p106(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p7(X2)&~p107(X2))&p106(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p7(X2)&~p107(X2))&p106(X2)))))))|~((~p106(X1)&p105(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p6(X2)&~p106(X2))&p105(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p106(X2))&p105(X2)))))))|~((~p105(X1)&p104(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p5(X2)&~p105(X2))&p104(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p5(X2)&~p105(X2))&p104(X2)))))))|~((~p104(X1)&p103(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p4(X2)&~p104(X2))&p103(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p104(X2))&p103(X2)))))))|~((~p103(X1)&p102(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p3(X2)&~p103(X2))&p102(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p3(X2)&~p103(X2))&p102(X2)))))))|~((~p102(X1)&p101(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p2(X2)&~p102(X2))&p101(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p102(X2))&p101(X2)))))))|~((~p101(X1)&p100(X1)))))&(((![X2]:((~r1(X1,X2)|~p11(X2)|~p110(X2)))|p11(X1))&(![X2]:((~r1(X1,X2)|p11(X2)|~p110(X2)))|~p11(X1)))|~p110(X1)))&(((![X2]:((~r1(X1,X2)|~p10(X2)|~p109(X2)))|p10(X1))&(![X2]:((~r1(X1,X2)|p10(X2)|~p109(X2)))|~p10(X1)))|~p109(X1)))&(((![X2]:((~r1(X1,X2)|~p9(X2)|~p108(X2)))|p9(X1))&(![X2]:((~r1(X1,X2)|p9(X2)|~p108(X2)))|~p9(X1)))|~p108(X1)))&(((![X2]:((~r1(X1,X2)|~p8(X2)|~p107(X2)))|p8(X1))&(![X2]:((~r1(X1,X2)|p8(X2)|~p107(X2)))|~p8(X1)))|~p107(X1)))&(((![X2]:((~r1(X1,X2)|~p7(X2)|~p106(X2)))|p7(X1))&(![X2]:((~r1(X1,X2)|p7(X2)|~p106(X2)))|~p7(X1)))|~p106(X1)))&(((![X2]:((~r1(X1,X2)|~p6(X2)|~p105(X2)))|p6(X1))&(![X2]:((~r1(X1,X2)|p6(X2)|~p105(X2)))|~p6(X1)))|~p105(X1)))&(((![X2]:((~r1(X1,X2)|~p5(X2)|~p104(X2)))|p5(X1))&(![X2]:((~r1(X1,X2)|p5(X2)|~p104(X2)))|~p5(X1)))|~p104(X1)))&(((![X2]:((~r1(X1,X2)|~p4(X2)|~p103(X2)))|p4(X1))&(![X2]:((~r1(X1,X2)|p4(X2)|~p103(X2)))|~p4(X1)))|~p103(X1)))&(((![X2]:((~r1(X1,X2)|~p3(X2)|~p102(X2)))|p3(X1))&(![X2]:((~r1(X1,X2)|p3(X2)|~p102(X2)))|~p3(X1)))|~p102(X1)))&(((![X2]:((~r1(X1,X2)|~p2(X2)|~p101(X2)))|p2(X1))&(![X2]:((~r1(X1,X2)|p2(X2)|~p101(X2)))|~p2(X1)))|~p101(X1)))&(((![X2]:((~r1(X1,X2)|~p1(X2)|~p100(X2)))|p1(X1))&(![X2]:((~r1(X1,X2)|p1(X2)|~p100(X2)))|~p1(X1)))|~p100(X1)))&(p110(X1)|~p111(X1)))&(p109(X1)|~p110(X1)))&(p108(X1)|~p109(X1)))&(p107(X1)|~p108(X1)))&(p106(X1)|~p107(X1)))&(p105(X1)|~p106(X1)))&(p104(X1)|~p105(X1)))&(p103(X1)|~p104(X1)))&(p102(X1)|~p103(X1)))&(p101(X1)|~p102(X1)))&(p100(X1)|~p101(X1))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 1.10/0.59 cnf(c_0_16, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_14, c_0_7])).
% 1.10/0.59 fof(c_0_17, plain, ![X25, X46, X47, X48, X49, X50, X51, X52, X53, X54, X55, X56, X57, X58, X59, X60, X61, X62, X63, X64, X65, X66, X67]:(((((((((((((((((((((((((((((((((((r1(X25,esk2_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25))&(((~p11(esk2_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25))&(~p111(esk2_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25)))&(p110(esk2_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25))))&((r1(X25,esk3_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25))&(((p11(esk3_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25))&(~p111(esk3_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25)))&(p110(esk3_1(X25))|(p110(X25)|~p109(X25))|~epred1_1(X25)))))&(((r1(X25,esk4_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))&(((~p10(esk4_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))&(~p110(esk4_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25)))&(p109(esk4_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))))&((r1(X25,esk5_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))&(((p10(esk5_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))&(~p110(esk5_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25)))&(p109(esk5_1(X25))|(p109(X25)|~p108(X25))|~epred1_1(X25))))))&(((r1(X25,esk6_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))&(((~p9(esk6_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))&(~p109(esk6_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25)))&(p108(esk6_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))))&((r1(X25,esk7_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))&(((p9(esk7_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))&(~p109(esk7_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25)))&(p108(esk7_1(X25))|(p108(X25)|~p107(X25))|~epred1_1(X25))))))&(((r1(X25,esk8_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))&(((~p8(esk8_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))&(~p108(esk8_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25)))&(p107(esk8_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))))&((r1(X25,esk9_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))&(((p8(esk9_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))&(~p108(esk9_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25)))&(p107(esk9_1(X25))|(p107(X25)|~p106(X25))|~epred1_1(X25))))))&(((r1(X25,esk10_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))&(((~p7(esk10_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))&(~p107(esk10_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25)))&(p106(esk10_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))))&((r1(X25,esk11_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))&(((p7(esk11_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))&(~p107(esk11_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25)))&(p106(esk11_1(X25))|(p106(X25)|~p105(X25))|~epred1_1(X25))))))&(((r1(X25,esk12_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))&(((~p6(esk12_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))&(~p106(esk12_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25)))&(p105(esk12_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))))&((r1(X25,esk13_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))&(((p6(esk13_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))&(~p106(esk13_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25)))&(p105(esk13_1(X25))|(p105(X25)|~p104(X25))|~epred1_1(X25))))))&(((r1(X25,esk14_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))&(((~p5(esk14_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))&(~p105(esk14_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25)))&(p104(esk14_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))))&((r1(X25,esk15_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))&(((p5(esk15_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))&(~p105(esk15_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25)))&(p104(esk15_1(X25))|(p104(X25)|~p103(X25))|~epred1_1(X25))))))&(((r1(X25,esk16_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))&(((~p4(esk16_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))&(~p104(esk16_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25)))&(p103(esk16_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))))&((r1(X25,esk17_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))&(((p4(esk17_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))&(~p104(esk17_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25)))&(p103(esk17_1(X25))|(p103(X25)|~p102(X25))|~epred1_1(X25))))))&(((r1(X25,esk18_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))&(((~p3(esk18_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))&(~p103(esk18_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25)))&(p102(esk18_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))))&((r1(X25,esk19_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))&(((p3(esk19_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))&(~p103(esk19_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25)))&(p102(esk19_1(X25))|(p102(X25)|~p101(X25))|~epred1_1(X25))))))&(((r1(X25,esk20_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))&(((~p2(esk20_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))&(~p102(esk20_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25)))&(p101(esk20_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))))&((r1(X25,esk21_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))&(((p2(esk21_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))&(~p102(esk21_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25)))&(p101(esk21_1(X25))|(p101(X25)|~p100(X25))|~epred1_1(X25))))))&((~r1(X25,X46)|~p11(X46)|~p110(X46)|p11(X25)|~p110(X25)|~epred1_1(X25))&(~r1(X25,X47)|p11(X47)|~p110(X47)|~p11(X25)|~p110(X25)|~epred1_1(X25))))&((~r1(X25,X48)|~p10(X48)|~p109(X48)|p10(X25)|~p109(X25)|~epred1_1(X25))&(~r1(X25,X49)|p10(X49)|~p109(X49)|~p10(X25)|~p109(X25)|~epred1_1(X25))))&((~r1(X25,X50)|~p9(X50)|~p108(X50)|p9(X25)|~p108(X25)|~epred1_1(X25))&(~r1(X25,X51)|p9(X51)|~p108(X51)|~p9(X25)|~p108(X25)|~epred1_1(X25))))&((~r1(X25,X52)|~p8(X52)|~p107(X52)|p8(X25)|~p107(X25)|~epred1_1(X25))&(~r1(X25,X53)|p8(X53)|~p107(X53)|~p8(X25)|~p107(X25)|~epred1_1(X25))))&((~r1(X25,X54)|~p7(X54)|~p106(X54)|p7(X25)|~p106(X25)|~epred1_1(X25))&(~r1(X25,X55)|p7(X55)|~p106(X55)|~p7(X25)|~p106(X25)|~epred1_1(X25))))&((~r1(X25,X56)|~p6(X56)|~p105(X56)|p6(X25)|~p105(X25)|~epred1_1(X25))&(~r1(X25,X57)|p6(X57)|~p105(X57)|~p6(X25)|~p105(X25)|~epred1_1(X25))))&((~r1(X25,X58)|~p5(X58)|~p104(X58)|p5(X25)|~p104(X25)|~epred1_1(X25))&(~r1(X25,X59)|p5(X59)|~p104(X59)|~p5(X25)|~p104(X25)|~epred1_1(X25))))&((~r1(X25,X60)|~p4(X60)|~p103(X60)|p4(X25)|~p103(X25)|~epred1_1(X25))&(~r1(X25,X61)|p4(X61)|~p103(X61)|~p4(X25)|~p103(X25)|~epred1_1(X25))))&((~r1(X25,X62)|~p3(X62)|~p102(X62)|p3(X25)|~p102(X25)|~epred1_1(X25))&(~r1(X25,X63)|p3(X63)|~p102(X63)|~p3(X25)|~p102(X25)|~epred1_1(X25))))&((~r1(X25,X64)|~p2(X64)|~p101(X64)|p2(X25)|~p101(X25)|~epred1_1(X25))&(~r1(X25,X65)|p2(X65)|~p101(X65)|~p2(X25)|~p101(X25)|~epred1_1(X25))))&((~r1(X25,X66)|~p1(X66)|~p100(X66)|p1(X25)|~p100(X25)|~epred1_1(X25))&(~r1(X25,X67)|p1(X67)|~p100(X67)|~p1(X25)|~p100(X25)|~epred1_1(X25))))&(p110(X25)|~p111(X25)|~epred1_1(X25)))&(p109(X25)|~p110(X25)|~epred1_1(X25)))&(p108(X25)|~p109(X25)|~epred1_1(X25)))&(p107(X25)|~p108(X25)|~epred1_1(X25)))&(p106(X25)|~p107(X25)|~epred1_1(X25)))&(p105(X25)|~p106(X25)|~epred1_1(X25)))&(p104(X25)|~p105(X25)|~epred1_1(X25)))&(p103(X25)|~p104(X25)|~epred1_1(X25)))&(p102(X25)|~p103(X25)|~epred1_1(X25)))&(p101(X25)|~p102(X25)|~epred1_1(X25)))&(p100(X25)|~p101(X25)|~epred1_1(X25)))), 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_15])])])])])])).
% 1.10/0.59 cnf(c_0_18, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_16, c_0_7])).
% 1.10/0.59 cnf(c_0_19, plain, (r1(X1,esk21_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_20, negated_conjecture, (epred1_1(esk1_0)), inference(spm,[status(thm)],[c_0_18, c_0_7])).
% 1.10/0.59 cnf(c_0_21, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.10/0.59 cnf(c_0_22, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.10/0.59 cnf(c_0_23, plain, (p101(X1)|~p102(esk21_1(X1))|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_24, plain, (r1(esk1_0,esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21])]), c_0_22])).
% 1.10/0.59 cnf(c_0_25, plain, (p101(esk21_1(X1))|p101(X1)|~p100(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_26, negated_conjecture, (~epred1_1(esk1_0)|~p102(esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_21]), c_0_22])).
% 1.10/0.59 cnf(c_0_27, plain, (r1(X1,esk18_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_28, negated_conjecture, (epred1_1(esk21_1(esk1_0))), inference(spm,[status(thm)],[c_0_18, c_0_24])).
% 1.10/0.59 cnf(c_0_29, plain, (p101(esk21_1(esk1_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_20]), c_0_21])]), c_0_22])).
% 1.10/0.59 cnf(c_0_30, negated_conjecture, (~p102(esk21_1(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_20])])).
% 1.10/0.59 cnf(c_0_31, negated_conjecture, (epred1_1(X1)|~r1(esk21_1(esk1_0),X1)), inference(spm,[status(thm)],[c_0_16, c_0_24])).
% 1.10/0.59 cnf(c_0_32, plain, (r1(esk21_1(esk1_0),esk18_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_29])]), c_0_30])).
% 1.10/0.59 cnf(c_0_33, plain, (p102(esk18_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_34, plain, (p102(X1)|~p103(esk18_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_35, negated_conjecture, (epred1_1(X1)|~r1(esk21_1(esk1_0),X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_14, c_0_24])).
% 1.10/0.59 cnf(c_0_36, plain, (r1(X1,esk16_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_37, negated_conjecture, (epred1_1(esk18_1(esk21_1(esk1_0)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 1.10/0.59 cnf(c_0_38, plain, (p102(esk18_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_28]), c_0_29])]), c_0_30])).
% 1.10/0.59 cnf(c_0_39, plain, (~p103(esk18_1(esk21_1(esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_29]), c_0_28])]), c_0_30])).
% 1.10/0.59 cnf(c_0_40, plain, (p104(X1)|~p5(esk14_1(X1))|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_41, negated_conjecture, (p5(X10)|~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)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.10/0.59 cnf(c_0_42, plain, (p103(esk16_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_43, negated_conjecture, (epred1_1(X1)|~r1(esk18_1(esk21_1(esk1_0)),X1)), inference(spm,[status(thm)],[c_0_35, c_0_32])).
% 1.10/0.59 cnf(c_0_44, plain, (r1(esk18_1(esk21_1(esk1_0)),esk16_1(esk18_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_38])]), c_0_39])).
% 1.10/0.59 cnf(c_0_45, plain, (p103(X1)|~p104(esk16_1(X1))|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_46, plain, (p104(X1)|~epred1_1(X1)|~p103(X1)|~r1(X2,esk14_1(X1))|~r1(esk1_0,X3)|~r1(X4,X2)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X3,X10)), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 1.10/0.59 cnf(c_0_47, plain, (p103(esk16_1(esk18_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_37]), c_0_38])]), c_0_39])).
% 1.10/0.59 cnf(c_0_48, negated_conjecture, (epred1_1(esk16_1(esk18_1(esk21_1(esk1_0))))), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 1.10/0.59 cnf(c_0_49, plain, (~p104(esk16_1(esk18_1(esk21_1(esk1_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_38]), c_0_37])]), c_0_39])).
% 1.10/0.59 cnf(c_0_50, plain, (r1(X1,esk14_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.10/0.59 cnf(c_0_51, plain, (~r1(X1,esk14_1(esk16_1(esk18_1(esk21_1(esk1_0)))))|~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(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_47]), c_0_48])]), c_0_49])).
% 1.10/0.59 cnf(c_0_52, plain, (r1(esk16_1(esk18_1(esk21_1(esk1_0))),esk14_1(esk16_1(esk18_1(esk21_1(esk1_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_48]), c_0_47])]), c_0_49])).
% 1.10/0.59 cnf(c_0_53, plain, (~r1(X1,esk16_1(esk18_1(esk21_1(esk1_0))))|~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_51, c_0_52])).
% 1.10/0.59 cnf(c_0_54, plain, (~r1(X1,esk18_1(esk21_1(esk1_0)))|~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_53, c_0_44])).
% 1.10/0.59 cnf(c_0_55, plain, (~r1(X1,esk21_1(esk1_0))|~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_54, c_0_32])).
% 1.10/0.59 cnf(c_0_56, plain, (~r1(esk1_0,X1)|~r1(X2,esk1_0)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X1,X5)), inference(spm,[status(thm)],[c_0_55, c_0_24])).
% 1.10/0.59 cnf(c_0_57, plain, (~r1(X1,esk1_0)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_56, c_0_7])).
% 1.10/0.59 cnf(c_0_58, plain, (~r1(esk1_0,X1)|~r1(X2,esk1_0)|~r1(X3,X2)|~r1(X1,X3)), inference(spm,[status(thm)],[c_0_57, c_0_7])).
% 1.10/0.59 cnf(c_0_59, plain, (~r1(X1,esk1_0)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_58, c_0_7])).
% 1.10/0.59 cnf(c_0_60, plain, (~r1(esk1_0,X1)|~r1(X1,esk1_0)), inference(spm,[status(thm)],[c_0_59, c_0_7])).
% 1.10/0.59 cnf(c_0_61, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_7]), c_0_7])]), ['proof']).
% 1.10/0.59 % SZS output end Proof
% 1.10/0.59 % User time : 0.085 s
% 1.10/0.59 % System time : 0.008 s
% 1.10/0.59 % Total time : 0.093 s
% 1.10/0.59 % User time : 0.088 s
% 1.10/0.59 % System time : 0.009 s
% 1.10/0.59 % Total time : 0.097 s
% 1.10/0.59
%------------------------------------------------------------------------------