%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n018.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:53 AM UTC 2026
% Result : Theorem 96.13s 12.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 4 21:15:03 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.14/0.47 start to proof:theBenchmark.p
% 96.13/12.80 % Version : CSI_E---1.1
% 96.13/12.80 % Problem : theBenchmark.p
% 96.13/12.80 % Proof found!
% 96.13/12.80 % SZS status Theorem for theBenchmark.p
% 96.13/12.80 % SZS output start Proof
% 96.13/12.80 fof(sos_07, axiom, ![X1, X2, X3]:('==>'('+'(X1,X2),X3)='==>'(X1,'==>'(X2,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 96.13/12.80 fof(sos_02, axiom, ![X1, X2]:('+'(X1,X2)='+'(X2,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 96.13/12.80 fof(sos_01, axiom, ![X1, X2, X3]:('+'('+'(X1,X2),X3)='+'(X1,'+'(X2,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_01)).
% 96.13/12.80 fof(sos_08, axiom, ![X1, X2]:('+'(X1,'==>'(X1,X2))='+'(X2,'==>'(X2,X1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 96.13/12.80 fof(sos_04, axiom, ![X1]:('==>'(X1,X1)='0'), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 96.13/12.80 fof(sos_05, axiom, ![X1]:('==>'(X1,'0')='0'), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_05)).
% 96.13/12.80 fof(sos_03, axiom, ![X1]:('+'(X1,'0')=X1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_03)).
% 96.13/12.80 fof(goals_09, conjecture, (('==>'(c,a)='0'&'==>'(c,b)='0')<=>'==>'(c,'+'(a,'==>'(a,b)))='0'), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals_09)).
% 96.13/12.80 fof(sos_06, axiom, ![X1]:('==>'('0',X1)=X1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_06)).
% 96.13/12.80 fof(c_0_9, plain, ![X13, X14, X15]:('==>'('+'(X13,X14),X15)='==>'(X13,'==>'(X14,X15))), inference(variable_rename,[status(thm)],[sos_07])).
% 96.13/12.80 fof(c_0_10, plain, ![X7, X8]:('+'(X7,X8)='+'(X8,X7)), inference(variable_rename,[status(thm)],[sos_02])).
% 96.13/12.80 fof(c_0_11, plain, ![X4, X5, X6]:('+'('+'(X4,X5),X6)='+'(X4,'+'(X5,X6))), inference(variable_rename,[status(thm)],[sos_01])).
% 96.13/12.80 fof(c_0_12, plain, ![X16, X17]:('+'(X16,'==>'(X16,X17))='+'(X17,'==>'(X17,X16))), inference(variable_rename,[status(thm)],[sos_08])).
% 96.13/12.80 cnf(c_0_13, plain, ('==>'('+'(X1,X2),X3)='==>'(X1,'==>'(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 96.13/12.80 cnf(c_0_14, plain, ('+'(X1,X2)='+'(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 96.13/12.80 fof(c_0_15, plain, ![X10]:('==>'(X10,X10)='0'), inference(variable_rename,[status(thm)],[sos_04])).
% 96.13/12.80 fof(c_0_16, plain, ![X11]:('==>'(X11,'0')='0'), inference(variable_rename,[status(thm)],[sos_05])).
% 96.13/12.80 cnf(c_0_17, plain, ('+'('+'(X1,X2),X3)='+'(X1,'+'(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 96.13/12.80 cnf(c_0_18, plain, ('+'(X1,'==>'(X1,X2))='+'(X2,'==>'(X2,X1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 96.13/12.80 cnf(c_0_19, plain, ('==>'(X1,'==>'(X2,X3))='==>'(X2,'==>'(X1,X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_14]), c_0_13])).
% 96.13/12.80 cnf(c_0_20, plain, ('==>'(X1,X1)='0'), inference(split_conjunct,[status(thm)],[c_0_15])).
% 96.13/12.80 cnf(c_0_21, plain, ('==>'(X1,'0')='0'), inference(split_conjunct,[status(thm)],[c_0_16])).
% 96.13/12.80 fof(c_0_22, plain, ![X9]:('+'(X9,'0')=X9), inference(variable_rename,[status(thm)],[sos_03])).
% 96.13/12.80 cnf(c_0_23, plain, ('+'(X1,'==>'(X1,'+'(X2,X3)))='+'(X2,'+'(X3,'==>'(X2,'==>'(X3,X1))))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_13])).
% 96.13/12.80 cnf(c_0_24, plain, ('==>'(X1,'==>'(X2,X1))='0'), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21])).
% 96.13/12.80 cnf(c_0_25, plain, ('+'(X1,'0')=X1), inference(split_conjunct,[status(thm)],[c_0_22])).
% 96.13/12.80 fof(c_0_26, negated_conjecture, ~((('==>'(c,a)='0'&'==>'(c,b)='0')<=>'==>'(c,'+'(a,'==>'(a,b)))='0')), inference(assume_negation,[status(cth)],[goals_09])).
% 96.13/12.80 cnf(c_0_27, plain, ('+'(X1,'==>'(X1,'+'(X1,X2)))='+'(X1,X2)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25])).
% 96.13/12.80 fof(c_0_28, negated_conjecture, (('==>'(c,a)!='0'|'==>'(c,b)!='0'|'==>'(c,'+'(a,'==>'(a,b)))!='0')&(('==>'(c,a)='0'|'==>'(c,'+'(a,'==>'(a,b)))='0')&('==>'(c,b)='0'|'==>'(c,'+'(a,'==>'(a,b)))='0'))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])).
% 96.13/12.80 cnf(c_0_29, plain, ('+'(X1,'==>'(X1,'+'(X2,'==>'(X2,'+'(X1,X3)))))='+'(X2,'==>'(X2,'+'(X1,X3)))), inference(spm,[status(thm)],[c_0_27, c_0_23])).
% 96.13/12.80 cnf(c_0_30, negated_conjecture, ('==>'(c,a)='0'|'==>'(c,'+'(a,'==>'(a,b)))='0'), inference(split_conjunct,[status(thm)],[c_0_28])).
% 96.13/12.80 cnf(c_0_31, negated_conjecture, ('+'(a,'==>'(a,c))=c|'==>'(c,a)='0'), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_25]), c_0_25])).
% 96.13/12.80 cnf(c_0_32, negated_conjecture, ('==>'(a,'==>'('==>'(a,c),X1))='==>'(c,X1)|'==>'(c,a)='0'), inference(spm,[status(thm)],[c_0_13, c_0_31])).
% 96.13/12.80 cnf(c_0_33, plain, ('+'(X1,'+'(X2,X3))='+'(X2,'+'(X1,X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_14]), c_0_17])).
% 96.13/12.80 cnf(c_0_34, plain, ('+'(X1,'+'('==>'(X1,X2),X3))='+'(X2,'+'('==>'(X2,X1),X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_17])).
% 96.13/12.80 cnf(c_0_35, negated_conjecture, ('==>'(c,a)='0'), inference(spm,[status(thm)],[c_0_24, c_0_32])).
% 96.13/12.80 cnf(c_0_36, plain, ('+'('0',X1)=X1), inference(spm,[status(thm)],[c_0_25, c_0_14])).
% 96.13/12.80 cnf(c_0_37, plain, ('+'(X1,'+'(X2,'==>'(X1,X3)))='+'(X2,'+'(X3,'==>'(X3,X1)))), inference(spm,[status(thm)],[c_0_33, c_0_18])).
% 96.13/12.80 cnf(c_0_38, negated_conjecture, ('+'(a,'+'('==>'(a,c),X1))='+'(c,X1)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])).
% 96.13/12.80 cnf(c_0_39, plain, ('+'(X1,'+'('==>'(X1,X2),'==>'('==>'(X1,X2),X3)))='+'(X2,'==>'(X2,'+'(X3,X1)))), inference(spm,[status(thm)],[c_0_23, c_0_37])).
% 96.13/12.80 fof(c_0_40, plain, ![X12]:('==>'('0',X12)=X12), inference(variable_rename,[status(thm)],[sos_06])).
% 96.13/12.80 cnf(c_0_41, plain, ('==>'(X1,'==>'('==>'(X1,X2),X2))='0'), inference(spm,[status(thm)],[c_0_20, c_0_19])).
% 96.13/12.80 cnf(c_0_42, plain, ('+'(X1,'==>'(X1,'+'(X2,'==>'(X2,X1))))='+'(X2,'==>'(X2,X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_20]), c_0_25]), c_0_14]), c_0_14])).
% 96.13/12.80 cnf(c_0_43, negated_conjecture, ('==>'(c,b)='0'|'==>'(c,'+'(a,'==>'(a,b)))='0'), inference(split_conjunct,[status(thm)],[c_0_28])).
% 96.13/12.80 cnf(c_0_44, negated_conjecture, ('+'(c,'==>'(c,'+'(X1,a)))='+'(c,'==>'('==>'(a,c),X1))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 96.13/12.80 cnf(c_0_45, plain, ('==>'(X1,'==>'('==>'(X1,X2),X3))='==>'(X2,'==>'('==>'(X2,X1),X3))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_18]), c_0_13])).
% 96.13/12.80 cnf(c_0_46, plain, ('==>'('0',X1)=X1), inference(split_conjunct,[status(thm)],[c_0_40])).
% 96.13/12.80 cnf(c_0_47, plain, ('==>'(X1,'==>'(X2,'==>'('==>'(X1,X3),X3)))='0'), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_41]), c_0_21])).
% 96.13/12.80 cnf(c_0_48, negated_conjecture, ('+'(c,'==>'(c,'+'(a,'==>'(a,b))))=c|'==>'(c,b)='0'), 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_42, c_0_43]), c_0_25]), c_0_13]), c_0_17]), c_0_25]), c_0_23])).
% 96.13/12.80 cnf(c_0_49, negated_conjecture, ('+'(c,'==>'(c,'+'(a,X1)))='+'(c,'==>'('==>'(a,c),X1))), inference(spm,[status(thm)],[c_0_44, c_0_14])).
% 96.13/12.80 cnf(c_0_50, negated_conjecture, ('==>'(a,'==>'('==>'(a,c),X1))='==>'(c,X1)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_35]), c_0_46])).
% 96.13/12.80 cnf(c_0_51, plain, ('==>'(X1,'==>'(X2,'==>'(X3,'+'(X1,X2))))='0'), inference(spm,[status(thm)],[c_0_13, c_0_24])).
% 96.13/12.80 cnf(c_0_52, plain, ('==>'(X1,'==>'('==>'(X1,X2),'==>'('==>'(X2,X3),X3)))='0'), inference(spm,[status(thm)],[c_0_47, c_0_45])).
% 96.13/12.80 cnf(c_0_53, negated_conjecture, ('+'(c,'==>'(c,b))=c|'==>'(c,b)='0'), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49]), c_0_19]), c_0_50])).
% 96.13/12.80 cnf(c_0_54, plain, ('==>'(X1,'==>'(X2,'==>'('==>'(X2,X3),'+'(X1,X3))))='0'), inference(spm,[status(thm)],[c_0_51, c_0_45])).
% 96.13/12.80 cnf(c_0_55, plain, ('==>'(X1,'==>'('==>'(X2,X3),'==>'('==>'(X1,X2),X3)))='0'), inference(spm,[status(thm)],[c_0_52, c_0_19])).
% 96.13/12.80 cnf(c_0_56, negated_conjecture, ('==>'(c,'==>'('==>'(c,b),X1))='==>'(c,X1)|'==>'(c,b)='0'), inference(spm,[status(thm)],[c_0_13, c_0_53])).
% 96.13/12.80 cnf(c_0_57, negated_conjecture, ('==>'(c,a)!='0'|'==>'(c,b)!='0'|'==>'(c,'+'(a,'==>'(a,b)))!='0'), inference(split_conjunct,[status(thm)],[c_0_28])).
% 96.13/12.80 cnf(c_0_58, negated_conjecture, ('==>'(c,'==>'('==>'('==>'(a,c),X1),'+'(a,X1)))='0'), inference(spm,[status(thm)],[c_0_54, c_0_50])).
% 96.13/12.80 cnf(c_0_59, negated_conjecture, ('==>'(c,b)='0'), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_20]), c_0_46])])).
% 96.13/12.80 cnf(c_0_60, negated_conjecture, ('==>'(c,'+'(a,'==>'(a,b)))!='0'|'==>'(c,b)!='0'), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_35])])).
% 96.13/12.80 cnf(c_0_61, negated_conjecture, ('==>'(c,'==>'('==>'(c,X1),'+'(X1,'==>'(X1,a))))='0'), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_18]), c_0_19]), c_0_50])).
% 96.13/12.80 cnf(c_0_62, negated_conjecture, ('==>'(X1,'==>'('==>'(X1,c),b))='0'), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_59]), c_0_46])).
% 96.13/12.80 cnf(c_0_63, negated_conjecture, ('==>'(c,'+'(a,'==>'(a,b)))!='0'), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_59])])).
% 96.13/12.80 cnf(c_0_64, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(rw,[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_61, c_0_62]), c_0_20]), c_0_46]), c_0_20]), c_0_46]), c_0_46]), c_0_18]), c_0_63]), ['proof']).
% 96.13/12.80 % SZS output end Proof
% 96.13/12.80 % User time : 11.076 s
% 96.13/12.80 % System time : 0.469 s
% 96.13/12.80 % Total time : 11.545 s
% 96.13/12.80 % User time : 58.245 s
% 96.13/12.80 % System time : 0.990 s
% 96.13/12.80 % Total time : 59.235 s
% 96.13/12.80
%------------------------------------------------------------------------------