%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n012.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.07s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.01 % Command : java -jar mcs_scs.jar %d %s
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Fri Sep 4 18:46:42 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.07/0.36 start to proof:theBenchmark.p
% 0.07/0.40 % Version : CSI_E---1.1
% 0.07/0.40 % Problem : theBenchmark.p
% 0.07/0.40 % Proof found!
% 0.07/0.40 % SZS status Theorem for theBenchmark.p
% 0.07/0.40 % SZS output start Proof
% 0.07/0.40 fof(main, conjecture, ~(?[X1]:(~((![X2]:((~(r1(X1,X2))|~(p15(X2))|![X1]:((~(r1(X2,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))|![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))|~$true))|~(![X2]:((~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2)))))))))|~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:((~(r1(X1,X2))|p15(X2)))|![X2]:((~(r1(X1,X2))|(~(p13(X2))&~(p14(X2)))|(p14(X2)&p13(X2))|(~(p12(X2))&~(p13(X2)))|(p13(X2)&p12(X2))|(~(p11(X2))&~(p12(X2)))|(p12(X2)&p11(X2))|(~(p10(X2))&~(p11(X2)))|(p11(X2)&p10(X2))|(~(p9(X2))&~(p10(X2)))|(p10(X2)&p9(X2))|(~(p8(X2))&~(p9(X2)))|(p9(X2)&p8(X2))|(~(p7(X2))&~(p8(X2)))|(p8(X2)&p7(X2))|(~(p6(X2))&~(p7(X2)))|(p7(X2)&p6(X2))|(~(p5(X2))&~(p6(X2)))|(p6(X2)&p5(X2))|(~(p4(X2))&~(p5(X2)))|(p5(X2)&p4(X2))|(~(p3(X2))&~(p4(X2)))|(p4(X2)&p3(X2))|(~(p2(X2))&~(p3(X2)))|(p3(X2)&p2(X2))|(~(p1(X2))&~(p2(X2)))|(p2(X2)&p1(X2))))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.07/0.40 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 0.07/0.40 fof(c_0_2, plain, ![X1]:((epred1_1(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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~($true)))|~(![X2]:((~r1(X1,X2)|~(((p14(X2)&~p13(X2))|(~p14(X2)&p13(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p12(X1))|(~p13(X1)&p12(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p12(X2)&~p11(X2))|(~p12(X2)&p11(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p10(X1))|(~p11(X1)&p10(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p9(X2))|(~p10(X2)&p9(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p8(X1))|(~p9(X1)&p8(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p7(X2))|(~p8(X2)&p7(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p6(X1))|(~p7(X1)&p6(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p5(X2))|(~p6(X2)&p5(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p4(X1))|(~p5(X1)&p4(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p3(X2))|(~p4(X2)&p3(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p2(X1))|(~p3(X1)&p2(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p1(X2))|(~p2(X2)&p1(X2)))))))|![X2]:((~r1(X1,X2)|p15(X2)))|![X2]:((~r1(X1,X2)|(~p13(X2)&~p14(X2))|(p14(X2)&p13(X2))|(~p12(X2)&~p13(X2))|(p13(X2)&p12(X2))|(~p11(X2)&~p12(X2))|(p12(X2)&p11(X2))|(~p10(X2)&~p11(X2))|(p11(X2)&p10(X2))|(~p9(X2)&~p10(X2))|(p10(X2)&p9(X2))|(~p8(X2)&~p9(X2))|(p9(X2)&p8(X2))|(~p7(X2)&~p8(X2))|(p8(X2)&p7(X2))|(~p6(X2)&~p7(X2))|(p7(X2)&p6(X2))|(~p5(X2)&~p6(X2))|(p6(X2)&p5(X2))|(~p4(X2)&~p5(X2))|(p5(X2)&p4(X2))|(~p3(X2)&~p4(X2))|(p4(X2)&p3(X2))|(~p2(X2)&~p3(X2))|(p3(X2)&p2(X2))|(~p1(X2)&~p2(X2))|(p2(X2)&p1(X2)))))))), introduced(definition)).
% 0.07/0.40 fof(c_0_3, plain, ![X1]:((epred1_1(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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~($true)))|~(![X2]:((~r1(X1,X2)|~(((p14(X2)&~p13(X2))|(~p14(X2)&p13(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p13(X1)&~p12(X1))|(~p13(X1)&p12(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p12(X2)&~p11(X2))|(~p12(X2)&p11(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p11(X1)&~p10(X1))|(~p11(X1)&p10(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p10(X2)&~p9(X2))|(~p10(X2)&p9(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p9(X1)&~p8(X1))|(~p9(X1)&p8(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p8(X2)&~p7(X2))|(~p8(X2)&p7(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p7(X1)&~p6(X1))|(~p7(X1)&p6(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p5(X2))|(~p6(X2)&p5(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p4(X1))|(~p5(X1)&p4(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p3(X2))|(~p4(X2)&p3(X2)))))))))|~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p2(X1))|(~p3(X1)&p2(X1)))))))))|~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p1(X2))|(~p2(X2)&p1(X2)))))))|![X2]:((~r1(X1,X2)|p15(X2)))|![X2]:((~r1(X1,X2)|(~p13(X2)&~p14(X2))|(p14(X2)&p13(X2))|(~p12(X2)&~p13(X2))|(p13(X2)&p12(X2))|(~p11(X2)&~p12(X2))|(p12(X2)&p11(X2))|(~p10(X2)&~p11(X2))|(p11(X2)&p10(X2))|(~p9(X2)&~p10(X2))|(p10(X2)&p9(X2))|(~p8(X2)&~p9(X2))|(p9(X2)&p8(X2))|(~p7(X2)&~p8(X2))|(p8(X2)&p7(X2))|(~p6(X2)&~p7(X2))|(p7(X2)&p6(X2))|(~p5(X2)&~p6(X2))|(p6(X2)&p5(X2))|(~p4(X2)&~p5(X2))|(p5(X2)&p4(X2))|(~p3(X2)&~p4(X2))|(p4(X2)&p3(X2))|(~p2(X2)&~p3(X2))|(p3(X2)&p2(X2))|(~p1(X2)&~p2(X2))|(p2(X2)&p1(X2)))))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 0.07/0.40 fof(c_0_4, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|~p15(X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|epred1_1(X1))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_2])).
% 0.07/0.40 fof(c_0_5, plain, ![X13, X27, X28, X29, X30, X31, X32, X33, X34, X35, X36, X37, X38, X39]:(((((((r1(X13,esk5_1(X13))|~epred1_1(X13))&(((r1(esk5_1(X13),esk6_1(X13))|~epred1_1(X13))&(((r1(esk6_1(X13),esk7_1(X13))|~epred1_1(X13))&(((r1(esk7_1(X13),esk8_1(X13))|~epred1_1(X13))&(((r1(esk8_1(X13),esk9_1(X13))|~epred1_1(X13))&(((r1(esk9_1(X13),esk10_1(X13))|~epred1_1(X13))&(((r1(esk10_1(X13),esk11_1(X13))|~epred1_1(X13))&(((r1(esk11_1(X13),esk12_1(X13))|~epred1_1(X13))&(((r1(esk12_1(X13),esk13_1(X13))|~epred1_1(X13))&(((r1(esk13_1(X13),esk14_1(X13))|~epred1_1(X13))&(((r1(esk14_1(X13),esk15_1(X13))|~epred1_1(X13))&(((r1(esk15_1(X13),esk16_1(X13))|~epred1_1(X13))&((r1(esk16_1(X13),esk17_1(X13))|~epred1_1(X13))&($true|~epred1_1(X13))))&((~p14(X27)|p13(X27)|~r1(esk16_1(X13),X27)|~epred1_1(X13))&(p14(X27)|~p13(X27)|~r1(esk16_1(X13),X27)|~epred1_1(X13)))))&((~p13(X28)|p12(X28)|~r1(esk15_1(X13),X28)|~epred1_1(X13))&(p13(X28)|~p12(X28)|~r1(esk15_1(X13),X28)|~epred1_1(X13)))))&((~p12(X29)|p11(X29)|~r1(esk14_1(X13),X29)|~epred1_1(X13))&(p12(X29)|~p11(X29)|~r1(esk14_1(X13),X29)|~epred1_1(X13)))))&((~p11(X30)|p10(X30)|~r1(esk13_1(X13),X30)|~epred1_1(X13))&(p11(X30)|~p10(X30)|~r1(esk13_1(X13),X30)|~epred1_1(X13)))))&((~p10(X31)|p9(X31)|~r1(esk12_1(X13),X31)|~epred1_1(X13))&(p10(X31)|~p9(X31)|~r1(esk12_1(X13),X31)|~epred1_1(X13)))))&((~p9(X32)|p8(X32)|~r1(esk11_1(X13),X32)|~epred1_1(X13))&(p9(X32)|~p8(X32)|~r1(esk11_1(X13),X32)|~epred1_1(X13)))))&((~p8(X33)|p7(X33)|~r1(esk10_1(X13),X33)|~epred1_1(X13))&(p8(X33)|~p7(X33)|~r1(esk10_1(X13),X33)|~epred1_1(X13)))))&((~p7(X34)|p6(X34)|~r1(esk9_1(X13),X34)|~epred1_1(X13))&(p7(X34)|~p6(X34)|~r1(esk9_1(X13),X34)|~epred1_1(X13)))))&((~p6(X35)|p5(X35)|~r1(esk8_1(X13),X35)|~epred1_1(X13))&(p6(X35)|~p5(X35)|~r1(esk8_1(X13),X35)|~epred1_1(X13)))))&((~p5(X36)|p4(X36)|~r1(esk7_1(X13),X36)|~epred1_1(X13))&(p5(X36)|~p4(X36)|~r1(esk7_1(X13),X36)|~epred1_1(X13)))))&((~p4(X37)|p3(X37)|~r1(esk6_1(X13),X37)|~epred1_1(X13))&(p4(X37)|~p3(X37)|~r1(esk6_1(X13),X37)|~epred1_1(X13)))))&((~p3(X38)|p2(X38)|~r1(esk5_1(X13),X38)|~epred1_1(X13))&(p3(X38)|~p2(X38)|~r1(esk5_1(X13),X38)|~epred1_1(X13))))&((~p2(X39)|p1(X39)|~r1(X13,X39)|~epred1_1(X13))&(p2(X39)|~p1(X39)|~r1(X13,X39)|~epred1_1(X13))))&((r1(X13,esk18_1(X13))|~epred1_1(X13))&(~p15(esk18_1(X13))|~epred1_1(X13))))&(((((((((((((((((((((((((((r1(X13,esk19_1(X13))|~epred1_1(X13))&(p13(esk19_1(X13))|p14(esk19_1(X13))|~epred1_1(X13)))&(~p14(esk19_1(X13))|~p13(esk19_1(X13))|~epred1_1(X13)))&(p12(esk19_1(X13))|p13(esk19_1(X13))|~epred1_1(X13)))&(~p13(esk19_1(X13))|~p12(esk19_1(X13))|~epred1_1(X13)))&(p11(esk19_1(X13))|p12(esk19_1(X13))|~epred1_1(X13)))&(~p12(esk19_1(X13))|~p11(esk19_1(X13))|~epred1_1(X13)))&(p10(esk19_1(X13))|p11(esk19_1(X13))|~epred1_1(X13)))&(~p11(esk19_1(X13))|~p10(esk19_1(X13))|~epred1_1(X13)))&(p9(esk19_1(X13))|p10(esk19_1(X13))|~epred1_1(X13)))&(~p10(esk19_1(X13))|~p9(esk19_1(X13))|~epred1_1(X13)))&(p8(esk19_1(X13))|p9(esk19_1(X13))|~epred1_1(X13)))&(~p9(esk19_1(X13))|~p8(esk19_1(X13))|~epred1_1(X13)))&(p7(esk19_1(X13))|p8(esk19_1(X13))|~epred1_1(X13)))&(~p8(esk19_1(X13))|~p7(esk19_1(X13))|~epred1_1(X13)))&(p6(esk19_1(X13))|p7(esk19_1(X13))|~epred1_1(X13)))&(~p7(esk19_1(X13))|~p6(esk19_1(X13))|~epred1_1(X13)))&(p5(esk19_1(X13))|p6(esk19_1(X13))|~epred1_1(X13)))&(~p6(esk19_1(X13))|~p5(esk19_1(X13))|~epred1_1(X13)))&(p4(esk19_1(X13))|p5(esk19_1(X13))|~epred1_1(X13)))&(~p5(esk19_1(X13))|~p4(esk19_1(X13))|~epred1_1(X13)))&(p3(esk19_1(X13))|p4(esk19_1(X13))|~epred1_1(X13)))&(~p4(esk19_1(X13))|~p3(esk19_1(X13))|~epred1_1(X13)))&(p2(esk19_1(X13))|p3(esk19_1(X13))|~epred1_1(X13)))&(~p3(esk19_1(X13))|~p2(esk19_1(X13))|~epred1_1(X13)))&(p1(esk19_1(X13))|p2(esk19_1(X13))|~epred1_1(X13)))&(~p2(esk19_1(X13))|~p1(esk19_1(X13))|~epred1_1(X13))))), 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])])])])])])).
% 0.07/0.40 fof(c_0_6, plain, ![X9]:(r1(X9,X9)), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.07/0.40 fof(c_0_7, negated_conjecture, ![X8]:((((r1(esk1_0,esk2_0)&p15(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))&(r1(esk1_0,esk4_0)&(~r1(esk4_0,X8)|epred1_1(X8))))), 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_4])])])])])).
% 0.07/0.40 cnf(c_0_8, plain, (p1(X1)|~p2(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.07/0.40 cnf(c_0_9, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.07/0.40 cnf(c_0_10, plain, (p2(X1)|~p1(X1)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.07/0.40 cnf(c_0_11, plain, (r1(X1,esk19_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.07/0.40 cnf(c_0_12, plain, (p1(esk19_1(X1))|p2(esk19_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.07/0.40 cnf(c_0_13, negated_conjecture, (epred1_1(X1)|~r1(esk4_0,X1)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.07/0.40 cnf(c_0_14, plain, (~p2(esk19_1(X1))|~p1(esk19_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.07/0.40 cnf(c_0_15, plain, (p1(X1)|~epred1_1(X1)|~p2(X1)), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 0.07/0.40 cnf(c_0_16, plain, (p2(esk19_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_12])).
% 0.07/0.40 cnf(c_0_17, negated_conjecture, (epred1_1(esk4_0)), inference(spm,[status(thm)],[c_0_13, c_0_9])).
% 0.07/0.40 cnf(c_0_18, plain, (~epred1_1(esk19_1(X1))|~epred1_1(X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_14, c_0_15]), c_0_16])).
% 0.07/0.40 cnf(c_0_19, negated_conjecture, (epred1_1(esk19_1(esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_11]), c_0_17])])).
% 0.07/0.40 cnf(c_0_20, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_17])]), ['proof']).
% 0.07/0.40 % SZS output end Proof
% 0.07/0.40 % User time : 0.006 s
% 0.07/0.40 % System time : 0.003 s
% 0.07/0.40 % Total time : 0.009 s
% 0.07/0.40 % User time : 0.008 s
% 0.07/0.40 % System time : 0.004 s
% 0.07/0.40 % Total time : 0.012 s
% 0.07/0.40
%------------------------------------------------------------------------------