%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL897+1 : TPTP v9.3.1. Released v5.5.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:54 AM UTC 2026
% Result : Theorem 244.09s 36.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL897+1 : TPTP v9.3.1. Released v5.5.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 : Sat Sep 5 15:07:57 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.08/0.36 start to proof:theBenchmark.p
% 244.09/36.35 % Version : CSI_E---1.1
% 244.09/36.35 % Problem : theBenchmark.p
% 244.09/36.35 % Proof found!
% 244.09/36.35 % SZS status Theorem for theBenchmark.p
% 244.09/36.35 % SZS output start Proof
% 244.09/36.35 fof(sos_07, axiom, ![X1, X2, X3]:('==>'('+'(X1,X2),X3)='==>'(X1,'==>'(X2,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_07)).
% 244.09/36.35 fof(sos_02, axiom, ![X1, X2]:('+'(X1,X2)='+'(X2,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_02)).
% 244.09/36.35 fof(sos_04, axiom, ![X1]:('==>'(X1,X1)='0'), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_04)).
% 244.09/36.35 fof(sos_05, axiom, ![X1]:('==>'(X1,'0')='0'), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_05)).
% 244.09/36.35 fof(sos_08, axiom, ![X1, X2]:('+'(X1,'==>'(X1,X2))='+'(X2,'==>'(X2,X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 244.09/36.35 fof(sos_01, axiom, ![X1, X2, X3]:('+'('+'(X1,X2),X3)='+'(X1,'+'(X2,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_01)).
% 244.09/36.35 fof(sos_03, axiom, ![X1]:('+'(X1,'0')=X1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_03)).
% 244.09/36.35 fof(goals_09, conjecture, '+'('+'(a,'==>'(a,b)),'==>'('+'(a,'==>'(a,b)),c))='+'(a,'==>'(a,'+'(b,'==>'(b,c)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals_09)).
% 244.09/36.35 fof(c_0_8, plain, ![X13, X14, X15]:('==>'('+'(X13,X14),X15)='==>'(X13,'==>'(X14,X15))), inference(variable_rename,[status(thm)],[sos_07])).
% 244.09/36.35 fof(c_0_9, plain, ![X7, X8]:('+'(X7,X8)='+'(X8,X7)), inference(variable_rename,[status(thm)],[sos_02])).
% 244.09/36.35 cnf(c_0_10, plain, ('==>'('+'(X1,X2),X3)='==>'(X1,'==>'(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 244.09/36.35 cnf(c_0_11, plain, ('+'(X1,X2)='+'(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 244.09/36.35 fof(c_0_12, plain, ![X10]:('==>'(X10,X10)='0'), inference(variable_rename,[status(thm)],[sos_04])).
% 244.09/36.35 fof(c_0_13, plain, ![X11]:('==>'(X11,'0')='0'), inference(variable_rename,[status(thm)],[sos_05])).
% 244.09/36.35 fof(c_0_14, plain, ![X16, X17]:('+'(X16,'==>'(X16,X17))='+'(X17,'==>'(X17,X16))), inference(variable_rename,[status(thm)],[sos_08])).
% 244.09/36.35 fof(c_0_15, plain, ![X4, X5, X6]:('+'('+'(X4,X5),X6)='+'(X4,'+'(X5,X6))), inference(variable_rename,[status(thm)],[sos_01])).
% 244.09/36.35 cnf(c_0_16, plain, ('==>'(X1,'==>'(X2,X3))='==>'(X2,'==>'(X1,X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_10])).
% 244.09/36.35 cnf(c_0_17, plain, ('==>'(X1,X1)='0'), inference(split_conjunct,[status(thm)],[c_0_12])).
% 244.09/36.35 cnf(c_0_18, plain, ('==>'(X1,'0')='0'), inference(split_conjunct,[status(thm)],[c_0_13])).
% 244.09/36.35 cnf(c_0_19, plain, ('+'(X1,'==>'(X1,X2))='+'(X2,'==>'(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 244.09/36.35 cnf(c_0_20, plain, ('+'('+'(X1,X2),X3)='+'(X1,'+'(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 244.09/36.35 cnf(c_0_21, plain, ('==>'(X1,'==>'(X2,X1))='0'), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18])).
% 244.09/36.35 cnf(c_0_22, plain, ('+'(X1,'+'(X2,'==>'(X1,'==>'(X2,X3))))='+'(X3,'==>'(X3,'+'(X1,X2)))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_10])).
% 244.09/36.35 cnf(c_0_23, plain, ('==>'(X1,'==>'(X2,'==>'(X3,X1)))='0'), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_21]), c_0_18])).
% 244.09/36.35 cnf(c_0_24, plain, ('==>'(X1,'==>'(X2,'==>'('==>'(X1,'==>'(X2,X3)),X4)))='==>'(X3,'==>'('==>'(X3,'+'(X1,X2)),X4))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_22]), c_0_10]), c_0_10])).
% 244.09/36.35 fof(c_0_25, plain, ![X9]:('+'(X9,'0')=X9), inference(variable_rename,[status(thm)],[sos_03])).
% 244.09/36.35 cnf(c_0_26, plain, ('+'(X1,'==>'(X2,'==>'(X1,X3)))='+'('==>'(X2,X3),'==>'('==>'(X2,X3),X1))), inference(spm,[status(thm)],[c_0_19, c_0_16])).
% 244.09/36.35 cnf(c_0_27, plain, ('==>'(X1,'==>'('==>'(X1,'+'(X2,X3)),X2))='0'), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 244.09/36.35 cnf(c_0_28, plain, ('+'(X1,'0')=X1), inference(split_conjunct,[status(thm)],[c_0_25])).
% 244.09/36.35 cnf(c_0_29, plain, ('==>'(X1,'==>'(X2,'+'(X1,X2)))='0'), inference(spm,[status(thm)],[c_0_17, c_0_10])).
% 244.09/36.35 cnf(c_0_30, plain, ('+'('==>'(X1,X2),'==>'(X1,'==>'('==>'(X1,X2),'+'(X2,X3))))='==>'(X1,'+'(X2,X3))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_28]), c_0_16])).
% 244.09/36.35 cnf(c_0_31, plain, ('==>'(X1,'==>'('==>'(X1,X2),'+'(X2,'==>'(X2,X1))))='0'), inference(spm,[status(thm)],[c_0_29, c_0_19])).
% 244.09/36.35 cnf(c_0_32, plain, ('==>'(X1,'+'(X2,'==>'(X2,X1)))='==>'(X1,X2)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_28])).
% 244.09/36.35 cnf(c_0_33, plain, ('==>'(X1,'+'(X1,'==>'(X1,X2)))='==>'(X1,X2)), inference(spm,[status(thm)],[c_0_32, c_0_19])).
% 244.09/36.35 fof(c_0_34, negated_conjecture, '+'('+'(a,'==>'(a,b)),'==>'('+'(a,'==>'(a,b)),c))!='+'(a,'==>'(a,'+'(b,'==>'(b,c)))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[goals_09])])).
% 244.09/36.35 cnf(c_0_35, plain, ('==>'(X1,'==>'('==>'(X1,X2),X3))='==>'(X2,'==>'('==>'(X2,X1),X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_19]), c_0_10])).
% 244.09/36.35 cnf(c_0_36, plain, ('==>'(X1,'==>'(X2,'+'(X1,'==>'(X1,X3))))='==>'(X2,'==>'(X1,X3))), inference(spm,[status(thm)],[c_0_16, c_0_33])).
% 244.09/36.35 fof(c_0_37, negated_conjecture, '+'('+'(a,'==>'(a,b)),'==>'('+'(a,'==>'(a,b)),c))!='+'(a,'==>'(a,'+'(b,'==>'(b,c)))), inference(fof_nnf,[status(thm)],[c_0_34])).
% 244.09/36.35 cnf(c_0_38, plain, ('+'(X1,'+'('==>'(X1,X2),X3))='+'(X2,'+'('==>'(X2,X1),X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_19]), c_0_20])).
% 244.09/36.35 cnf(c_0_39, plain, ('==>'(X1,'==>'('==>'(X1,X2),'+'(X2,'==>'(X2,X3))))='==>'(X2,'==>'('==>'(X2,X1),X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_16])).
% 244.09/36.35 cnf(c_0_40, negated_conjecture, ('+'('+'(a,'==>'(a,b)),'==>'('+'(a,'==>'(a,b)),c))!='+'(a,'==>'(a,'+'(b,'==>'(b,c))))), inference(split_conjunct,[status(thm)],[c_0_37])).
% 244.09/36.35 cnf(c_0_41, plain, ('+'(X1,'+'('==>'(X1,X2),'==>'(X2,'==>'('==>'(X2,X1),X3))))='+'(X3,'==>'(X3,'+'(X2,'==>'(X2,X1))))), inference(spm,[status(thm)],[c_0_22, c_0_38])).
% 244.09/36.35 cnf(c_0_42, plain, ('+'('==>'(X1,X2),'==>'(X2,'==>'('==>'(X2,X1),X3)))='==>'(X1,'+'(X2,'==>'(X2,X3)))), inference(spm,[status(thm)],[c_0_30, c_0_39])).
% 244.09/36.35 cnf(c_0_43, negated_conjecture, ('+'(c,'==>'(c,'+'(a,'==>'(a,b))))!='+'(a,'==>'(a,'+'(b,'==>'(b,c))))), inference(rw,[status(thm)],[c_0_40, c_0_19])).
% 244.09/36.35 cnf(c_0_44, plain, ('+'(X1,'==>'(X1,'+'(X2,'==>'(X2,X3))))='+'(X3,'==>'(X3,'+'(X2,'==>'(X2,X1))))), inference(rw,[status(thm)],[c_0_41, c_0_42])).
% 244.09/36.35 cnf(c_0_45, plain, ('+'(X1,'+'('==>'(X1,X2),'==>'(X2,'==>'('==>'(X2,X1),X3))))='+'(X3,'==>'(X3,'+'(X1,'==>'(X1,X2))))), inference(spm,[status(thm)],[c_0_22, c_0_35])).
% 244.09/36.35 cnf(c_0_46, negated_conjecture, ('+'(b,'==>'(b,'+'(a,'==>'(a,c))))!='+'(a,'==>'(a,'+'(b,'==>'(b,c))))), inference(rw,[status(thm)],[c_0_43, c_0_44])).
% 244.09/36.35 cnf(c_0_47, plain, ('+'(X1,'==>'(X1,'+'(X2,'==>'(X2,X3))))='+'(X3,'==>'(X3,'+'(X1,'==>'(X1,X2))))), inference(rw,[status(thm)],[c_0_45, c_0_42])).
% 244.09/36.35 cnf(c_0_48, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47]), c_0_19])]), ['proof']).
% 244.09/36.35 % SZS output end Proof
% 244.09/36.35 % User time : 33.823 s
% 244.09/36.35 % System time : 1.102 s
% 244.09/36.35 % Total time : 34.924 s
% 244.09/36.35 % User time : 168.688 s
% 244.09/36.35 % System time : 5.448 s
% 244.09/36.35 % Total time : 174.136 s
% 244.09/36.35
%------------------------------------------------------------------------------