%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Apr 1 02:14:32 AM UTC 2025
% Result : Theorem 4.33s 4.49s
% Output : Proof 4.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Mar 31 14:28:20 EDT 2025
% 0.12/0.33 % CPUTime :
% 4.33/4.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.33/4.50 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.33/4.51
% 4.33/4.51 %-----------------------------------------------------
% 4.33/4.51 fof('corollary-(times:successor)', conjecture, ! [_142958, _142961] : (nat_succeeds(_142958) & nat_succeeds(_142961) => @*(s(_142958), _142961) = @+(_142961, @*(_142958, _142961))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'corollary-(times:successor)')).
% 4.33/4.51 fof(id15, axiom, ! [_143259, _143262, _143265] : (times_succeeds(_143259, _143262, _143265) <=> ? [_143286, _143289] : (_143259 = s(_143286) & times_succeeds(_143286, _143262, _143289) & plus_succeeds(_143262, _143289, _143265)) | _143259 = '0' & _143265 = '0'), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id15)).
% 4.33/4.51 fof(id27, axiom, ! [_143687] : (nat_succeeds(_143687) <=> ? [_143702] : (_143687 = s(_143702) & nat_succeeds(_143702)) | _143687 = '0'), file('/export/starexec/sandbox/benchmark/theBenchmark.p', id27)).
% 4.33/4.51 fof('(@+)/2', axiom, ! [_143904, _143907, _143910] : (nat_succeeds(_143904) => (@+(_143904, _143907) = _143910 <=> plus_succeeds(_143904, _143907, _143910))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', '(@+)/2')).
% 4.33/4.51 fof('(@*)/2', axiom, ! [_144102, _144105, _144108] : (nat_succeeds(_144102) & nat_succeeds(_144105) => (@*(_144102, _144105) = _144108 <=> times_succeeds(_144102, _144105, _144108))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', '(@*)/2')).
% 4.33/4.51
% 4.33/4.51 cnf(1, plain, [-(nat_succeeds(36 ^ []))], clausify('corollary-(times:successor)')).
% 4.33/4.51 cnf(2, plain, [-(nat_succeeds(37 ^ []))], clausify('corollary-(times:successor)')).
% 4.33/4.51 cnf(3, plain, [@*(s(36 ^ []), 37 ^ []) = @+(37 ^ [], @*(36 ^ [], 37 ^ []))], clausify('corollary-(times:successor)')).
% 4.33/4.51 cnf(4, plain, [_47298 = _47347, -(s(_47298) = s(_47347))], theory(equality)).
% 4.33/4.51 cnf(5, plain, [-(_33712 = _33712)], theory(equality)).
% 4.33/4.51 cnf(6, plain, [-(times_succeeds(_52699, _52788, _52876)), _52699 = s(_53073), times_succeeds(_53073, _52788, _53141), plus_succeeds(_52788, _53141, _52876)], clausify(id15)).
% 4.33/4.51 cnf(7, plain, [-(nat_succeeds(_65718)), _65718 = s(_65824), nat_succeeds(_65824)], clausify(id27)).
% 4.33/4.51 cnf(8, plain, [nat_succeeds(_67189), @+(_67189, _67248) = _67306, -(plus_succeeds(_67189, _67248, _67306))], clausify('(@+)/2')).
% 4.33/4.51 cnf(9, plain, [nat_succeeds(_67785), nat_succeeds(_67721), @*(_67721, _67785) = _67848, -(times_succeeds(_67721, _67785, _67848))], clausify('(@*)/2')).
% 4.33/4.51 cnf(10, plain, [nat_succeeds(_67785), nat_succeeds(_67721), -(@*(_67721, _67785) = _67848), times_succeeds(_67721, _67785, _67848)], clausify('(@*)/2')).
% 4.33/4.51
% 4.33/4.51 cnf('1',plain,[@*(s(36 ^ []), 37 ^ []) = @+(37 ^ [], @*(36 ^ [], 37 ^ []))],start(3)).
% 4.33/4.51 cnf('1.1',plain,[-(@*(s(36 ^ []), 37 ^ []) = @+(37 ^ [], @*(36 ^ [], 37 ^ []))), nat_succeeds(37 ^ []), nat_succeeds(s(36 ^ [])), times_succeeds(s(36 ^ []), 37 ^ [], @+(37 ^ [], @*(36 ^ [], 37 ^ [])))],extension(10,bind([[_67721, _67785, _67848], [s(36 ^ []), 37 ^ [], @+(37 ^ [], @*(36 ^ [], 37 ^ []))]]))).
% 4.33/4.51 cnf('1.1.1',plain,[-(nat_succeeds(37 ^ []))],extension(2)).
% 4.33/4.51 cnf('1.1.2',plain,[-(nat_succeeds(s(36 ^ []))), s(36 ^ []) = s(36 ^ []), nat_succeeds(36 ^ [])],extension(7,bind([[_65718, _65824], [s(36 ^ []), 36 ^ []]]))).
% 4.33/4.51 cnf('1.1.2.1',plain,[-(s(36 ^ []) = s(36 ^ [])), 36 ^ [] = 36 ^ []],extension(4,bind([[_47298, _47347], [36 ^ [], 36 ^ []]]))).
% 4.33/4.51 cnf('1.1.2.1.1',plain,[-(36 ^ [] = 36 ^ [])],extension(5,bind([[_33712], [36 ^ []]]))).
% 4.33/4.51 cnf('1.1.2.2',plain,[-(nat_succeeds(36 ^ []))],extension(1)).
% 4.33/4.51 cnf('1.1.3',plain,[-(times_succeeds(s(36 ^ []), 37 ^ [], @+(37 ^ [], @*(36 ^ [], 37 ^ [])))), s(36 ^ []) = s(36 ^ []), times_succeeds(36 ^ [], 37 ^ [], @*(36 ^ [], 37 ^ [])), plus_succeeds(37 ^ [], @*(36 ^ [], 37 ^ []), @+(37 ^ [], @*(36 ^ [], 37 ^ [])))],extension(6,bind([[_52699, _53073, _52788, _53141, _52876], [s(36 ^ []), 36 ^ [], 37 ^ [], @*(36 ^ [], 37 ^ []), @+(37 ^ [], @*(36 ^ [], 37 ^ []))]]))).
% 4.33/4.51 cnf('1.1.3.1',plain,[-(s(36 ^ []) = s(36 ^ [])), 36 ^ [] = 36 ^ []],extension(4,bind([[_47298, _47347], [36 ^ [], 36 ^ []]]))).
% 4.33/4.51 cnf('1.1.3.1.1',plain,[-(36 ^ [] = 36 ^ [])],extension(5,bind([[_33712], [36 ^ []]]))).
% 4.33/4.51 cnf('1.1.3.2',plain,[-(times_succeeds(36 ^ [], 37 ^ [], @*(36 ^ [], 37 ^ []))), nat_succeeds(37 ^ []), nat_succeeds(36 ^ []), @*(36 ^ [], 37 ^ []) = @*(36 ^ [], 37 ^ [])],extension(9,bind([[_67721, _67785, _67848], [36 ^ [], 37 ^ [], @*(36 ^ [], 37 ^ [])]]))).
% 4.33/4.51 cnf('1.1.3.2.1',plain,[-(nat_succeeds(37 ^ []))],extension(2)).
% 4.33/4.51 cnf('1.1.3.2.2',plain,[-(nat_succeeds(36 ^ []))],extension(1)).
% 4.33/4.51 cnf('1.1.3.2.3',plain,[-(@*(36 ^ [], 37 ^ []) = @*(36 ^ [], 37 ^ []))],extension(5,bind([[_33712], [@*(36 ^ [], 37 ^ [])]]))).
% 4.33/4.51 cnf('1.1.3.3',plain,[-(plus_succeeds(37 ^ [], @*(36 ^ [], 37 ^ []), @+(37 ^ [], @*(36 ^ [], 37 ^ [])))), nat_succeeds(37 ^ []), @+(37 ^ [], @*(36 ^ [], 37 ^ [])) = @+(37 ^ [], @*(36 ^ [], 37 ^ []))],extension(8,bind([[_67189, _67248, _67306], [37 ^ [], @*(36 ^ [], 37 ^ []), @+(37 ^ [], @*(36 ^ [], 37 ^ []))]]))).
% 4.33/4.51 cnf('1.1.3.3.1',plain,[-(nat_succeeds(37 ^ []))],extension(2)).
% 4.33/4.51 cnf('1.1.3.3.2',plain,[-(@+(37 ^ [], @*(36 ^ [], 37 ^ [])) = @+(37 ^ [], @*(36 ^ [], 37 ^ [])))],extension(5,bind([[_33712], [@+(37 ^ [], @*(36 ^ [], 37 ^ []))]]))).
% 4.33/4.51 %-----------------------------------------------------
% 4.33/4.51
% 4.33/4.51 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------