%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n028.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:26 AM UTC 2026
% Result : Theorem 34.72s 4.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.36 % Computer : n028.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 08:57:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 34.72/4.96 % Version : CSI_E---1.1
% 34.72/4.96 % Problem : theBenchmark.p
% 34.72/4.96 % Proof found!
% 34.72/4.96 % SZS status Theorem for theBenchmark.p
% 34.72/4.96 % SZS output start Proof
% 34.72/4.96 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|~(p4(X2)))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2))))))))|~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2)))))))&p2(X1))&~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p2(X2))))))))))))))))|(~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p2(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p2(X2)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1)))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 34.72/4.96 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 34.72/4.96 fof(c_0_2, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|~p4(X2))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))|~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2))))))&p2(X1))&~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2)))))))))))))))|(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p2(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 34.72/4.96 fof(c_0_3, negated_conjecture, ![X5, X6, X7, X10, X11, X13, X15, X16, X17, X21, X22, X23, X24, X28, X31, X33, X34, X35]:(((((((~r1(esk1_0,X5)|~p4(X5))&(((((r1(X7,esk2_2(X6,X7))|~r1(X6,X7)|~r1(esk1_0,X6))&((r1(esk2_2(X6,X7),esk3_2(X6,X7))|~r1(X6,X7)|~r1(esk1_0,X6))&(~p3(esk3_2(X6,X7))|~r1(X6,X7)|~r1(esk1_0,X6))))&(p2(esk2_2(X6,X7))|~r1(X6,X7)|~r1(esk1_0,X6)))&((((r1(X13,esk5_3(X6,X10,X13))|~r1(X10,X13)|(r1(X11,esk4_3(X6,X10,X11))|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6))&(~r1(esk5_3(X6,X10,X13),X15)|~p2(X15)|~r1(X10,X13)|(r1(X11,esk4_3(X6,X10,X11))|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6)))&((r1(X13,esk5_3(X6,X10,X13))|~r1(X10,X13)|(~p3(esk4_3(X6,X10,X11))|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6))&(~r1(esk5_3(X6,X10,X13),X15)|~p2(X15)|~r1(X10,X13)|(~p3(esk4_3(X6,X10,X11))|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6))))&((r1(X13,esk5_3(X6,X10,X13))|~r1(X10,X13)|(p2(X11)|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6))&(~r1(esk5_3(X6,X10,X13),X15)|~p2(X15)|~r1(X10,X13)|(p2(X11)|~r1(X10,X11)|~p2(X10))|~r1(X6,X10)|~r1(esk1_0,X6)))))&((((r1(X6,esk8_1(X6))|(r1(X17,esk6_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6))&(~r1(esk8_1(X6),X21)|~p2(X21)|(r1(X17,esk6_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6)))&(((r1(X6,esk8_1(X6))|(r1(esk6_3(X6,X16,X17),esk7_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6))&(~r1(esk8_1(X6),X21)|~p2(X21)|(r1(esk6_3(X6,X16,X17),esk7_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6)))&((r1(X6,esk8_1(X6))|(~p3(esk7_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6))&(~r1(esk8_1(X6),X21)|~p2(X21)|(~p3(esk7_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6)))))&((r1(X6,esk8_1(X6))|(p2(esk6_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6))&(~r1(esk8_1(X6),X21)|~p2(X21)|(p2(esk6_3(X6,X16,X17))|~r1(X16,X17)|~r1(X6,X16))|~r1(esk1_0,X6))))))&((r1(X22,esk9_1(X22))|(~r1(X22,X23)|(~r1(X23,X24)|p1(X24)))|~r1(esk1_0,X22))&(~p1(esk9_1(X22))|(~r1(X22,X23)|(~r1(X23,X24)|p1(X24)))|~r1(esk1_0,X22))))&((r1(esk1_0,esk10_0)&(r1(esk10_0,esk11_0)&(~r1(esk11_0,X28)|p1(X28))))&(r1(esk10_0,esk12_0)&~p1(esk12_0))))&(r1(esk1_0,esk13_0)&((r1(X31,esk14_1(X31))|~r1(esk13_0,X31))&(~p2(esk14_1(X31))|~r1(esk13_0,X31)))))&((r1(X33,esk15_1(X33))|(~r1(esk1_0,X33)|(~r1(X33,X34)|(~r1(X34,X35)|~p1(X35)))))&(p1(esk15_1(X33))|(~r1(esk1_0,X33)|(~r1(X33,X34)|(~r1(X34,X35)|~p1(X35)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])])).
% 34.72/4.96 cnf(c_0_4, negated_conjecture, (r1(X1,esk5_3(X2,X3,X1))|p2(X4)|~r1(X3,X1)|~r1(X3,X4)|~p2(X3)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_5, negated_conjecture, (r1(esk1_0,esk13_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_6, negated_conjecture, (p2(X1)|r1(X2,esk5_3(esk13_0,X3,X2))|~p2(X3)|~r1(esk13_0,X3)|~r1(X3,X1)|~r1(X3,X2)), inference(spm,[status(thm)],[c_0_4, c_0_5])).
% 34.72/4.96 cnf(c_0_7, negated_conjecture, (r1(X1,esk2_2(X2,X1))|~r1(X2,X1)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_8, negated_conjecture, (p2(esk2_2(X1,X2))|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_9, negated_conjecture, (p2(X1)|r1(X2,esk5_3(esk13_0,esk2_2(X3,esk13_0),X2))|~r1(esk2_2(X3,esk13_0),X1)|~r1(esk2_2(X3,esk13_0),X2)|~r1(esk1_0,X3)|~r1(X3,esk13_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6, c_0_7]), c_0_8])).
% 34.72/4.96 cnf(c_0_10, negated_conjecture, (r1(X1,esk14_1(X1))|~r1(esk13_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 fof(c_0_11, plain, ![X3]:(r1(X3,X3)), inference(variable_rename,[status(thm)],[reflexivity])).
% 34.72/4.96 cnf(c_0_12, negated_conjecture, (r1(X1,esk8_1(X1))|r1(X2,esk6_3(X1,X3,X2))|~r1(X3,X2)|~r1(X1,X3)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_13, negated_conjecture, (p2(esk14_1(esk2_2(X1,esk13_0)))|r1(X2,esk5_3(esk13_0,esk2_2(X1,esk13_0),X2))|~r1(esk2_2(X1,esk13_0),X2)|~r1(esk1_0,X1)|~r1(X1,esk13_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_10]), c_0_7])).
% 34.72/4.96 cnf(c_0_14, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 34.72/4.96 cnf(c_0_15, negated_conjecture, (r1(X1,esk8_1(X1))|p2(esk6_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_16, negated_conjecture, (r1(X1,esk6_3(esk13_0,X2,X1))|r1(esk13_0,esk8_1(esk13_0))|~r1(esk13_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_12, c_0_5])).
% 34.72/4.96 cnf(c_0_17, negated_conjecture, (p2(esk14_1(esk2_2(X1,esk13_0)))|r1(esk2_2(X1,esk13_0),esk5_3(esk13_0,esk2_2(X1,esk13_0),esk2_2(X1,esk13_0)))|~r1(esk1_0,X1)|~r1(X1,esk13_0)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 34.72/4.96 cnf(c_0_18, negated_conjecture, (p2(esk6_3(esk13_0,X1,X2))|r1(esk13_0,esk8_1(esk13_0))|~r1(esk13_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_15, c_0_5])).
% 34.72/4.96 cnf(c_0_19, negated_conjecture, (r1(X1,esk6_3(esk13_0,esk2_2(X2,esk13_0),X1))|r1(esk13_0,esk8_1(esk13_0))|~r1(esk2_2(X2,esk13_0),X1)|~r1(esk1_0,X2)|~r1(X2,esk13_0)), inference(spm,[status(thm)],[c_0_16, c_0_7])).
% 34.72/4.96 cnf(c_0_20, negated_conjecture, (p2(esk14_1(esk2_2(esk1_0,esk13_0)))|r1(esk2_2(esk1_0,esk13_0),esk5_3(esk13_0,esk2_2(esk1_0,esk13_0),esk2_2(esk1_0,esk13_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_21, negated_conjecture, (p2(esk6_3(esk13_0,esk2_2(X1,esk13_0),X2))|r1(esk13_0,esk8_1(esk13_0))|~r1(esk2_2(X1,esk13_0),X2)|~r1(esk1_0,X1)|~r1(X1,esk13_0)), inference(spm,[status(thm)],[c_0_18, c_0_7])).
% 34.72/4.96 cnf(c_0_22, negated_conjecture, (p2(X5)|~r1(esk5_3(X1,X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~r1(X2,X5)|~p2(X2)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_23, negated_conjecture, (p2(esk14_1(esk2_2(esk1_0,esk13_0)))|r1(esk5_3(esk13_0,esk2_2(esk1_0,esk13_0),esk2_2(esk1_0,esk13_0)),esk6_3(esk13_0,esk2_2(esk1_0,esk13_0),esk5_3(esk13_0,esk2_2(esk1_0,esk13_0),esk2_2(esk1_0,esk13_0))))|r1(esk13_0,esk8_1(esk13_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_24, negated_conjecture, (p2(esk6_3(esk13_0,esk2_2(esk1_0,esk13_0),esk5_3(esk13_0,esk2_2(esk1_0,esk13_0),esk2_2(esk1_0,esk13_0))))|p2(esk14_1(esk2_2(esk1_0,esk13_0)))|r1(esk13_0,esk8_1(esk13_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_20]), c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_25, negated_conjecture, (~p2(esk14_1(X1))|~r1(esk13_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_26, negated_conjecture, (p2(X1)|r1(esk13_0,esk8_1(esk13_0))|~p2(esk2_2(esk1_0,esk13_0))|~r1(esk13_0,esk2_2(esk1_0,esk13_0))|~r1(esk2_2(esk1_0,esk13_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_5]), c_0_14])]), c_0_24]), c_0_25])).
% 34.72/4.96 cnf(c_0_27, negated_conjecture, (p2(X1)|r1(esk13_0,esk8_1(esk13_0))|~r1(esk13_0,esk2_2(esk1_0,esk13_0))|~r1(esk2_2(esk1_0,esk13_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_8]), c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_28, negated_conjecture, (p2(X1)|r1(esk13_0,esk8_1(esk13_0))|~r1(esk2_2(esk1_0,esk13_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_7]), c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_29, negated_conjecture, (r1(X3,esk6_3(X1,X4,X3))|~r1(esk8_1(X1),X2)|~p2(X2)|~r1(X4,X3)|~r1(X1,X4)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_30, negated_conjecture, (r1(esk13_0,esk8_1(esk13_0))|~r1(esk13_0,esk2_2(esk1_0,esk13_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_10]), c_0_25])).
% 34.72/4.96 cnf(c_0_31, negated_conjecture, (p2(esk6_3(X1,X3,X4))|~r1(esk8_1(X1),X2)|~p2(X2)|~r1(X3,X4)|~r1(X1,X3)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 34.72/4.96 cnf(c_0_32, negated_conjecture, (r1(X1,esk6_3(X2,X3,X1))|~r1(X4,esk8_1(X2))|~r1(esk1_0,X2)|~r1(esk1_0,X4)|~r1(X3,X1)|~r1(X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_7]), c_0_8])).
% 34.72/4.96 cnf(c_0_33, negated_conjecture, (r1(esk13_0,esk8_1(esk13_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_7]), c_0_14]), c_0_5])])).
% 34.72/4.96 cnf(c_0_34, negated_conjecture, (p2(esk6_3(X1,X2,X3))|~r1(X4,esk8_1(X1))|~r1(esk1_0,X1)|~r1(esk1_0,X4)|~r1(X2,X3)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_7]), c_0_8])).
% 34.72/4.96 cnf(c_0_35, negated_conjecture, (r1(X1,esk6_3(esk13_0,X2,X1))|~r1(esk13_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_5])])).
% 34.72/4.96 cnf(c_0_36, negated_conjecture, (p2(esk6_3(esk13_0,X1,X2))|~r1(esk13_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_33]), c_0_5])])).
% 34.72/4.96 cnf(c_0_37, negated_conjecture, (p2(X1)|~p2(X2)|~r1(X3,esk5_3(X4,X2,X5))|~r1(esk1_0,X4)|~r1(esk13_0,X3)|~r1(X2,X1)|~r1(X2,X5)|~r1(X4,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_35]), c_0_36])).
% 34.72/4.96 cnf(c_0_38, negated_conjecture, (p2(esk14_1(esk2_2(esk13_0,esk13_0)))|r1(esk2_2(esk13_0,esk13_0),esk5_3(esk13_0,esk2_2(esk13_0,esk13_0),esk2_2(esk13_0,esk13_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_5]), c_0_14])])).
% 34.72/4.96 cnf(c_0_39, negated_conjecture, (p2(X1)|~p2(esk2_2(esk13_0,esk13_0))|~r1(esk13_0,esk2_2(esk13_0,esk13_0))|~r1(esk2_2(esk13_0,esk13_0),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_5]), c_0_14])]), c_0_25])).
% 34.72/4.96 cnf(c_0_40, negated_conjecture, (p2(X1)|~r1(esk13_0,esk2_2(esk13_0,esk13_0))|~r1(esk2_2(esk13_0,esk13_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_8]), c_0_5]), c_0_14])])).
% 34.72/4.96 cnf(c_0_41, negated_conjecture, (~r1(esk13_0,esk2_2(esk13_0,esk13_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_10]), c_0_25])).
% 34.72/4.96 cnf(c_0_42, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_7]), c_0_5]), c_0_14])]), ['proof']).
% 34.72/4.96 % SZS output end Proof
% 34.72/4.96 % User time : 4.384 s
% 34.72/4.96 % System time : 0.057 s
% 34.72/4.96 % Total time : 4.440 s
% 34.72/4.96 % User time : 21.461 s
% 34.72/4.96 % System time : 0.157 s
% 34.72/4.96 % Total time : 21.618 s
% 34.72/4.96
%------------------------------------------------------------------------------