%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n003.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:31 AM UTC 2026
% Result : Theorem 0.23s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 09:52:05 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.23/0.47 start to proof:theBenchmark.p
% 0.23/0.54 % Version : CSI_E---1.1
% 0.23/0.54 % Problem : theBenchmark.p
% 0.23/0.54 % Proof found!
% 0.23/0.54 % SZS status Theorem for theBenchmark.p
% 0.23/0.54 % SZS output start Proof
% 0.23/0.54 fof(main, conjecture, ~(?[X1]:(~((![X2]:((~(r1(X1,X2))|~(p3(X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|~$true))|~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:((~(r1(X1,X2))|p3(X2)))|![X2]:((~(r1(X1,X2))|(~(p1(X2))&~(p2(X2)))|(p2(X2)&p1(X2))))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.23/0.54 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 0.23/0.54 fof(c_0_2, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|~p3(X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|~($true)))|~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p1(X2))|(~p2(X2)&p1(X2)))))))|![X2]:((~r1(X1,X2)|p3(X2)))|![X2]:((~r1(X1,X2)|(~p1(X2)&~p2(X2))|(p2(X2)&p1(X2)))))))))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 0.23/0.54 fof(c_0_3, negated_conjecture, ![X8, X10]:((((r1(esk1_0,esk2_0)&p3(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))&(r1(esk1_0,esk4_0)&(((((r1(X8,esk5_1(X8))|~r1(esk4_0,X8))&($true|~r1(esk4_0,X8)))&((~p2(X10)|p1(X10)|~r1(X8,X10)|~r1(esk4_0,X8))&(p2(X10)|~p1(X10)|~r1(X8,X10)|~r1(esk4_0,X8))))&((r1(X8,esk6_1(X8))|~r1(esk4_0,X8))&(~p3(esk6_1(X8))|~r1(esk4_0,X8))))&(((r1(X8,esk7_1(X8))|~r1(esk4_0,X8))&(p1(esk7_1(X8))|p2(esk7_1(X8))|~r1(esk4_0,X8)))&(~p2(esk7_1(X8))|~p1(esk7_1(X8))|~r1(esk4_0,X8))))))), 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])])])])])])).
% 0.23/0.54 fof(c_0_4, plain, ![X13]:(r1(X13,X13)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.23/0.54 cnf(c_0_5, negated_conjecture, (p1(X1)|~p2(X1)|~r1(X2,X1)|~r1(esk4_0,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.54 cnf(c_0_6, negated_conjecture, (r1(X1,esk7_1(X1))|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.54 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.23/0.54 cnf(c_0_8, negated_conjecture, (p2(X1)|~p1(X1)|~r1(X2,X1)|~r1(esk4_0,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.54 cnf(c_0_9, negated_conjecture, (p1(X1)|~p2(X1)|~r1(esk7_1(esk4_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5, c_0_6]), c_0_7])])).
% 0.23/0.54 cnf(c_0_10, negated_conjecture, (~p2(esk7_1(X1))|~p1(esk7_1(X1))|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.54 cnf(c_0_11, negated_conjecture, (p2(X1)|~p1(X1)|~r1(esk4_0,X1)), inference(spm,[status(thm)],[c_0_8, c_0_7])).
% 0.23/0.54 cnf(c_0_12, negated_conjecture, (p1(esk7_1(esk4_0))|~p2(esk7_1(esk4_0))), inference(spm,[status(thm)],[c_0_9, c_0_7])).
% 0.23/0.54 cnf(c_0_13, negated_conjecture, (p1(esk7_1(X1))|p2(esk7_1(X1))|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.54 cnf(c_0_14, negated_conjecture, (~p1(esk7_1(X1))|~r1(esk4_0,esk7_1(X1))|~r1(esk4_0,X1)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 0.23/0.54 cnf(c_0_15, negated_conjecture, (p1(esk7_1(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_7])])).
% 0.23/0.54 cnf(c_0_16, negated_conjecture, (~r1(esk4_0,esk7_1(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14, c_0_15]), c_0_7])])).
% 0.23/0.54 cnf(c_0_17, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_6]), c_0_7])]), ['proof']).
% 0.23/0.54 % SZS output end Proof
% 0.23/0.54 % User time : 0.006 s
% 0.23/0.54 % System time : 0.002 s
% 0.23/0.54 % Total time : 0.008 s
% 0.23/0.54 % User time : 0.008 s
% 0.23/0.54 % System time : 0.004 s
% 0.23/0.54 % Total time : 0.013 s
% 0.23/0.54
%------------------------------------------------------------------------------