%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL688+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n006.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:32 AM UTC 2026
% Result : Theorem 14.64s 2.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL688+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.06/0.33 % Computer : n006.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Fri Sep 4 17:57:32 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.12/0.46 start to proof:theBenchmark.p
% 14.64/2.40 % Version : CSI_E---1.1
% 14.64/2.40 % Problem : theBenchmark.p
% 14.64/2.40 % Proof found!
% 14.64/2.40 % SZS status Theorem for theBenchmark.p
% 14.64/2.40 % SZS output start Proof
% 14.64/2.40 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)))))))))))))))))))))|((~(p1(X1))&~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))))&![X2]:((~(r1(X1,X2))|p1(X2)|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|p1(X2))))&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/sandbox2/benchmark/theBenchmark.p', main)).
% 14.64/2.40 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 14.64/2.40 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity)).
% 14.64/2.40 fof(c_0_3, 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))))))))))))))))))))|((~p1(X1)&~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))))&![X2]:((~r1(X1,X2)|p1(X2)|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|p1(X2))))&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])])).
% 14.64/2.40 fof(c_0_4, negated_conjecture, ![X9, X10, X11, X14, X15, X17, X19, X20, X23, X24, X27, X30, X32, X33, X34]:(((((((~r1(esk1_0,X9)|~p4(X9))&((((r1(X11,esk2_2(X10,X11))|~r1(X10,X11)|~r1(esk1_0,X10))&((r1(esk2_2(X10,X11),esk3_2(X10,X11))|~r1(X10,X11)|~r1(esk1_0,X10))&(~p3(esk3_2(X10,X11))|~r1(X10,X11)|~r1(esk1_0,X10))))&(p2(esk2_2(X10,X11))|~r1(X10,X11)|~r1(esk1_0,X10)))&((((r1(X17,esk5_3(X10,X14,X17))|~r1(X14,X17)|(r1(X15,esk4_3(X10,X14,X15))|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10))&(~r1(esk5_3(X10,X14,X17),X19)|~p2(X19)|~r1(X14,X17)|(r1(X15,esk4_3(X10,X14,X15))|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10)))&((r1(X17,esk5_3(X10,X14,X17))|~r1(X14,X17)|(~p3(esk4_3(X10,X14,X15))|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10))&(~r1(esk5_3(X10,X14,X17),X19)|~p2(X19)|~r1(X14,X17)|(~p3(esk4_3(X10,X14,X15))|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10))))&((r1(X17,esk5_3(X10,X14,X17))|~r1(X14,X17)|(p2(X15)|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10))&(~r1(esk5_3(X10,X14,X17),X19)|~p2(X19)|~r1(X14,X17)|(p2(X15)|~r1(X14,X15)|~p2(X14))|~r1(X10,X14)|~r1(esk1_0,X10))))))&((((r1(esk1_0,esk7_0)|(r1(X20,esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0)))&(~p1(esk7_0)|(r1(X20,esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0))))&(~r1(esk7_0,X23)|(~r1(X23,X24)|p1(X24)|~p1(X23))|(r1(X20,esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0))))&(((r1(esk1_0,esk7_0)|(~p1(esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0)))&(~p1(esk7_0)|(~p1(esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0))))&(~r1(esk7_0,X23)|(~r1(X23,X24)|p1(X24)|~p1(X23))|(~p1(esk6_1(X20))|~r1(esk1_0,X20)|p1(esk1_0))))))&((r1(esk1_0,esk8_0)&(r1(esk8_0,esk9_0)&(~r1(esk9_0,X27)|p1(X27))))&(r1(esk8_0,esk10_0)&~p1(esk10_0))))&(r1(esk1_0,esk11_0)&((r1(X30,esk12_1(X30))|~r1(esk11_0,X30))&(~p2(esk12_1(X30))|~r1(esk11_0,X30)))))&((r1(X32,esk13_1(X32))|(~r1(esk1_0,X32)|(~r1(X32,X33)|(~r1(X33,X34)|~p1(X34)))))&(p1(esk13_1(X32))|(~r1(esk1_0,X32)|(~r1(X32,X33)|(~r1(X33,X34)|~p1(X34)))))))), 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_3])])])])])])).
% 14.64/2.40 cnf(c_0_5, negated_conjecture, (r1(esk2_2(X1,X2),esk3_2(X1,X2))|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 cnf(c_0_6, negated_conjecture, (r1(esk1_0,esk11_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 fof(c_0_7, plain, ![X4]:(r1(X4,X4)), inference(variable_rename,[status(thm)],[reflexivity])).
% 14.64/2.40 fof(c_0_8, 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])])])).
% 14.64/2.40 cnf(c_0_9, negated_conjecture, (r1(esk2_2(esk11_0,X1),esk3_2(esk11_0,X1))|~r1(esk11_0,X1)), inference(spm,[status(thm)],[c_0_5, c_0_6])).
% 14.64/2.40 cnf(c_0_10, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 14.64/2.40 cnf(c_0_11, negated_conjecture, (r1(X1,esk2_2(X2,X1))|~r1(X2,X1)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 cnf(c_0_12, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 14.64/2.40 cnf(c_0_13, negated_conjecture, (r1(esk2_2(esk11_0,esk11_0),esk3_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 14.64/2.40 cnf(c_0_14, negated_conjecture, (r1(X1,esk2_2(esk11_0,X1))|~r1(esk11_0,X1)), inference(spm,[status(thm)],[c_0_11, c_0_6])).
% 14.64/2.40 cnf(c_0_15, negated_conjecture, (r1(X1,esk3_2(esk11_0,esk11_0))|~r1(X1,esk2_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 14.64/2.40 cnf(c_0_16, negated_conjecture, (r1(esk11_0,esk2_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_14, c_0_10])).
% 14.64/2.40 cnf(c_0_17, negated_conjecture, (p2(esk2_2(X1,X2))|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 cnf(c_0_18, negated_conjecture, (r1(X1,esk12_1(X1))|~r1(esk11_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 cnf(c_0_19, negated_conjecture, (r1(esk11_0,esk3_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 14.64/2.40 cnf(c_0_20, 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_4])).
% 14.64/2.40 cnf(c_0_21, negated_conjecture, (r1(X1,esk2_2(esk11_0,esk11_0))|~r1(X1,esk11_0)), inference(spm,[status(thm)],[c_0_12, c_0_16])).
% 14.64/2.40 cnf(c_0_22, negated_conjecture, (p2(esk2_2(esk11_0,X1))|~r1(esk11_0,X1)), inference(spm,[status(thm)],[c_0_17, c_0_6])).
% 14.64/2.40 cnf(c_0_23, negated_conjecture, (r1(esk3_2(esk11_0,esk11_0),esk12_1(esk3_2(esk11_0,esk11_0)))), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 14.64/2.40 cnf(c_0_24, negated_conjecture, (p2(X1)|r1(X2,esk5_3(esk1_0,X3,X2))|~p2(X3)|~r1(esk1_0,X3)|~r1(X3,X1)|~r1(X3,X2)), inference(spm,[status(thm)],[c_0_20, c_0_10])).
% 14.64/2.40 cnf(c_0_25, negated_conjecture, (r1(esk1_0,esk2_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_21, c_0_6])).
% 14.64/2.40 cnf(c_0_26, negated_conjecture, (p2(esk2_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_22, c_0_10])).
% 14.64/2.40 cnf(c_0_27, negated_conjecture, (r1(X1,esk12_1(esk3_2(esk11_0,esk11_0)))|~r1(X1,esk3_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_12, c_0_23])).
% 14.64/2.40 cnf(c_0_28, negated_conjecture, (p2(X1)|r1(X2,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),X2))|~r1(esk2_2(esk11_0,esk11_0),X1)|~r1(esk2_2(esk11_0,esk11_0),X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])])).
% 14.64/2.40 cnf(c_0_29, negated_conjecture, (r1(esk2_2(esk11_0,esk11_0),esk12_1(esk3_2(esk11_0,esk11_0)))), inference(spm,[status(thm)],[c_0_27, c_0_13])).
% 14.64/2.40 cnf(c_0_30, negated_conjecture, (p2(esk12_1(esk3_2(esk11_0,esk11_0)))|r1(X1,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),X1))|~r1(esk2_2(esk11_0,esk11_0),X1)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 14.64/2.40 cnf(c_0_31, negated_conjecture, (~p2(esk12_1(X1))|~r1(esk11_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 14.64/2.40 cnf(c_0_32, negated_conjecture, (p2(esk12_1(esk3_2(esk11_0,esk11_0)))|r1(esk2_2(esk11_0,esk11_0),esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0)))), inference(spm,[status(thm)],[c_0_30, c_0_10])).
% 14.64/2.40 cnf(c_0_33, negated_conjecture, (r1(esk2_2(esk11_0,esk11_0),esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_19])])).
% 14.64/2.40 cnf(c_0_34, negated_conjecture, (r1(X1,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0)))|~r1(X1,esk2_2(esk11_0,esk11_0))), inference(spm,[status(thm)],[c_0_12, c_0_33])).
% 14.64/2.40 cnf(c_0_35, negated_conjecture, (r1(esk11_0,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0)))), inference(spm,[status(thm)],[c_0_34, c_0_16])).
% 14.64/2.40 cnf(c_0_36, 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_4])).
% 14.64/2.40 cnf(c_0_37, negated_conjecture, (r1(esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0)),esk2_2(esk11_0,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0))))), inference(spm,[status(thm)],[c_0_14, c_0_35])).
% 14.64/2.40 cnf(c_0_38, negated_conjecture, (p2(esk2_2(esk11_0,esk5_3(esk1_0,esk2_2(esk11_0,esk11_0),esk2_2(esk11_0,esk11_0))))), inference(spm,[status(thm)],[c_0_22, c_0_35])).
% 14.64/2.40 cnf(c_0_39, negated_conjecture, (p2(X1)|~r1(esk2_2(esk11_0,esk11_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_37]), c_0_38]), c_0_26]), c_0_10]), c_0_10]), c_0_25])])).
% 14.64/2.40 cnf(c_0_40, negated_conjecture, (p2(esk12_1(esk3_2(esk11_0,esk11_0)))), inference(spm,[status(thm)],[c_0_39, c_0_29])).
% 14.64/2.40 cnf(c_0_41, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_40]), c_0_19])]), ['proof']).
% 14.64/2.40 % SZS output end Proof
% 14.64/2.40 % User time : 1.847 s
% 14.64/2.40 % System time : 0.052 s
% 14.64/2.40 % Total time : 1.898 s
% 14.64/2.40 % User time : 9.316 s
% 14.64/2.40 % System time : 0.100 s
% 14.64/2.40 % Total time : 9.416 s
% 14.64/2.40
%------------------------------------------------------------------------------