%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n026.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:25 AM UTC 2026
% Result : Theorem 7.31s 1.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n026.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sat Sep 5 07:05:25 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.25/0.46 start to proof:theBenchmark.p
% 7.31/1.46 % Version : CSI_E---1.1
% 7.31/1.46 % Problem : theBenchmark.p
% 7.31/1.46 % Proof found!
% 7.31/1.46 % SZS status Theorem for theBenchmark.p
% 7.31/1.46 % SZS output start Proof
% 7.31/1.46 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))|(((((~(p12(X1))&~(p10(X1)))&~(p8(X1)))&~(p6(X1)))&~(p4(X1)))&~(p2(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))|~(((~(p5(X1))&~(p1(X1)))|(p1(X1)&p5(X1)))))))))))))))))))|![X1]:((~(r1(X2,X1))|p6(X1)))|~(![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))|~(((~(p4(X1))&~(p5(X1)))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~(r1(X1,X2))|p5(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))|~(((~(p3(X1))&~(p4(X1)))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~(r1(X2,X1))|p4(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p3(X1)))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(![X2]:((~(r1(X1,X2))|~(~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p1(X1))&~(p2(X1)))|(p2(X1)&p1(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))|(((((p6(X1)&p5(X1))&p4(X1))&p3(X1))&p2(X1))&p1(X1)))))))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 7.31/1.46 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 7.31/1.46 fof(c_0_2, 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)|(((((~p12(X1)&~p10(X1))&~p8(X1))&~p6(X1))&~p4(X1))&~p2(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)|~(((~p5(X1)&~p1(X1))|(p1(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![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)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(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)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(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)|(((((p6(X1)&p5(X1))&p4(X1))&p3(X1))&p2(X1))&p1(X1))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 7.31/1.46 fof(c_0_3, negated_conjecture, ![X11, X12, X13, X14, X15, X16, X17, X18, X20, X21, X22, X23, X24, X25, X26, X28, X29, X30, X31, X32, X33, X35, X36, X37, X38, X39, X41, X42, X43, X44]:(((((r1(esk1_0,esk2_0)&(r1(esk2_0,esk3_0)&(r1(esk3_0,esk4_0)&(r1(esk4_0,esk5_0)&(r1(esk5_0,esk6_0)&(r1(esk6_0,esk7_0)&(p12(esk7_0)|p10(esk7_0)|p8(esk7_0)|p6(esk7_0)|p4(esk7_0)|p2(esk7_0))))))))&(r1(esk1_0,esk8_0)&~p7(esk8_0)))&((((p5(X18)|p1(X18)|~r1(X17,X18)|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(esk1_0,X11))&(~p1(X18)|~p5(X18)|~r1(X17,X18)|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(esk1_0,X11)))&((r1(X11,esk9_1(X11))|~r1(esk1_0,X11))&(~p6(esk9_1(X11))|~r1(esk1_0,X11))))&((((p4(X26)|p5(X26)|~r1(X25,X26)|~r1(X24,X25)|~r1(X23,X24)|~r1(X22,X23)|~r1(X21,X22)|~r1(X20,X21)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p5(X26)|~p4(X26)|~r1(X25,X26)|~r1(X24,X25)|~r1(X23,X24)|~r1(X22,X23)|~r1(X21,X22)|~r1(X20,X21)|~r1(X11,X20)|~r1(esk1_0,X11)))&((r1(X20,esk10_2(X11,X20))|~r1(X11,X20)|~r1(esk1_0,X11))&(~p5(esk10_2(X11,X20))|~r1(X11,X20)|~r1(esk1_0,X11))))&((((p3(X33)|p4(X33)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p4(X33)|~p3(X33)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11)))&((r1(X28,esk11_3(X11,X20,X28))|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p4(esk11_3(X11,X20,X28))|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))))&((((p2(X39)|p3(X39)|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p3(X39)|~p2(X39)|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11)))&((r1(X35,esk12_4(X11,X20,X28,X35))|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p3(esk12_4(X11,X20,X28,X35))|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))))&((p1(X44)|p2(X44)|~r1(X43,X44)|~r1(X42,X43)|~r1(X41,X42)|~r1(X35,X41)|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))&(~p2(X44)|~p1(X44)|~r1(X43,X44)|~r1(X42,X43)|~r1(X41,X42)|~r1(X35,X41)|~r1(X28,X35)|~r1(X20,X28)|~r1(X11,X20)|~r1(esk1_0,X11))))))))&(r1(esk1_0,esk13_0)&(r1(esk13_0,esk14_0)&(r1(esk14_0,esk15_0)&(r1(esk15_0,esk16_0)&(r1(esk16_0,esk17_0)&(r1(esk17_0,esk18_0)&(~p6(esk18_0)|~p5(esk18_0)|~p4(esk18_0)|~p3(esk18_0)|~p2(esk18_0)|~p1(esk18_0)))))))))), 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_2])])])])])])).
% 7.31/1.46 fof(c_0_4, plain, ![X51]:(r1(X51,X51)), inference(variable_rename,[status(thm)],[reflexivity])).
% 7.31/1.46 cnf(c_0_5, negated_conjecture, (~p2(X1)|~p1(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_6, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 7.31/1.46 cnf(c_0_7, negated_conjecture, (~p4(X1)|~p3(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_8, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_9, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_5, c_0_6])).
% 7.31/1.46 cnf(c_0_10, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_7, c_0_6])).
% 7.31/1.46 cnf(c_0_11, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_8, c_0_6])).
% 7.31/1.46 cnf(c_0_12, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_9, c_0_6])).
% 7.31/1.46 cnf(c_0_13, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_10, c_0_6])).
% 7.31/1.46 cnf(c_0_14, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_11, c_0_6])).
% 7.31/1.46 cnf(c_0_15, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_12, c_0_6])).
% 7.31/1.46 cnf(c_0_16, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_13, c_0_6])).
% 7.31/1.46 cnf(c_0_17, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_14, c_0_6])).
% 7.31/1.46 cnf(c_0_18, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X1)), inference(spm,[status(thm)],[c_0_15, c_0_6])).
% 7.31/1.46 cnf(c_0_19, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X1)), inference(spm,[status(thm)],[c_0_16, c_0_6])).
% 7.31/1.46 cnf(c_0_20, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X1)), inference(spm,[status(thm)],[c_0_17, c_0_6])).
% 7.31/1.46 cnf(c_0_21, negated_conjecture, (p5(X1)|p1(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_22, negated_conjecture, (p2(X1)|p3(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_23, negated_conjecture, (p1(X1)|p2(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_24, negated_conjecture, (p3(X1)|p4(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_25, negated_conjecture, (p4(X1)|p5(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_26, negated_conjecture, (~p1(X1)|~p5(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_27, negated_conjecture, (~p3(X1)|~p2(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(esk1_0,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_28, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_18, c_0_6])).
% 7.31/1.46 cnf(c_0_29, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_19, c_0_6])).
% 7.31/1.46 cnf(c_0_30, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_20, c_0_6])).
% 7.31/1.46 cnf(c_0_31, negated_conjecture, (p1(X1)|p5(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_21, c_0_6])).
% 7.31/1.46 cnf(c_0_32, negated_conjecture, (r1(esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 7.31/1.46 cnf(c_0_33, negated_conjecture, (p3(X1)|p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_22, c_0_6])).
% 7.31/1.46 cnf(c_0_34, negated_conjecture, (p1(X1)|p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_23, c_0_6])).
% 7.31/1.46 cnf(c_0_35, negated_conjecture, (p3(X1)|p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_24, c_0_6])).
% 7.31/1.46 cnf(c_0_36, negated_conjecture, (p5(X1)|p4(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_25, c_0_6])).
% 7.31/1.46 cnf(c_0_37, negated_conjecture, (~p1(X1)|~p5(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_26, c_0_6])).
% 7.31/1.46 cnf(c_0_38, negated_conjecture, (~p3(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X1)), inference(spm,[status(thm)],[c_0_27, c_0_6])).
% 7.31/1.46 cnf(c_0_39, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_28, c_0_6])).
% 7.31/1.46 cnf(c_0_40, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_29, c_0_6])).
% 7.31/1.46 cnf(c_0_41, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_30, c_0_6])).
% 7.31/1.46 cnf(c_0_42, negated_conjecture, (p1(X1)|p5(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 7.31/1.46 cnf(c_0_43, negated_conjecture, (p3(X1)|p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_33, c_0_32])).
% 7.31/1.46 cnf(c_0_44, negated_conjecture, (p1(X1)|p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_34, c_0_32])).
% 7.31/1.46 cnf(c_0_45, negated_conjecture, (p3(X1)|p4(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_35, c_0_32])).
% 7.31/1.46 cnf(c_0_46, negated_conjecture, (p5(X1)|p4(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_36, c_0_32])).
% 7.31/1.46 cnf(c_0_47, negated_conjecture, (~p1(X1)|~p5(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_37, c_0_32])).
% 7.31/1.46 cnf(c_0_48, negated_conjecture, (~p3(X1)|~p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_38, c_0_32])).
% 7.31/1.46 cnf(c_0_49, negated_conjecture, (~p1(X1)|~p2(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_39, c_0_6])).
% 7.31/1.46 cnf(c_0_50, negated_conjecture, (~p3(X1)|~p4(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_40, c_0_6])).
% 7.31/1.46 cnf(c_0_51, negated_conjecture, (~p5(X1)|~p4(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_41, c_0_6])).
% 7.31/1.46 cnf(c_0_52, negated_conjecture, (p1(X1)|p5(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_42, c_0_6])).
% 7.31/1.46 cnf(c_0_53, negated_conjecture, (p3(X1)|p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_43, c_0_6])).
% 7.31/1.46 cnf(c_0_54, negated_conjecture, (p1(X1)|p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_44, c_0_6])).
% 7.31/1.46 cnf(c_0_55, negated_conjecture, (p3(X1)|p4(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_45, c_0_6])).
% 7.31/1.46 cnf(c_0_56, negated_conjecture, (p5(X1)|p4(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_46, c_0_6])).
% 7.31/1.46 cnf(c_0_57, negated_conjecture, (~p1(X1)|~p5(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_47, c_0_6])).
% 7.31/1.46 cnf(c_0_58, negated_conjecture, (~p3(X1)|~p2(X1)|~r1(esk2_0,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_48, c_0_6])).
% 7.31/1.46 cnf(c_0_59, negated_conjecture, (~p1(esk2_0)|~p2(esk2_0)), inference(spm,[status(thm)],[c_0_49, c_0_32])).
% 7.31/1.46 cnf(c_0_60, negated_conjecture, (~p3(esk2_0)|~p4(esk2_0)), inference(spm,[status(thm)],[c_0_50, c_0_32])).
% 7.31/1.46 cnf(c_0_61, negated_conjecture, (~p5(esk2_0)|~p4(esk2_0)), inference(spm,[status(thm)],[c_0_51, c_0_32])).
% 7.31/1.46 cnf(c_0_62, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_52, c_0_53, c_0_54, c_0_55, c_0_56, c_0_57, c_0_58, c_0_59, c_0_60, c_0_61, c_0_6]), ['proof']).
% 7.31/1.46 % SZS output end Proof
% 7.31/1.46 % User time : 0.908 s
% 7.31/1.46 % System time : 0.034 s
% 7.31/1.46 % Total time : 0.942 s
% 7.31/1.46 % User time : 0.910 s
% 7.31/1.46 % System time : 0.037 s
% 7.31/1.46 % Total time : 0.948 s
% 7.31/1.46
%------------------------------------------------------------------------------