%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX206+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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 May 5 07:05:05 PM UTC 2026
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX206+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.16/0.33 % Computer : n027.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 11:33:50 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(50 ^ _11376) ^ [_13199] : [x2(_13199, _13199) = _13199], (42 ^ _11376) ^ [_12880] : [-(proj1S(s(_12880)) = _12880)], (44 ^ _11376) ^ [_12961] : [z = s(_12961)], (46 ^ _11376) ^ [_13041] : [-(x2(z, _13041) = _13041)], (48 ^ _11376) ^ [_13116, _13118] : [-(x2(s(_13116), _13118) = s(x2(_13116, _13118)))], (2 ^ _11376) ^ [_11500] : [-(_11500 = _11500)], (4 ^ _11376) ^ [_11607, _11609] : [_11609 = _11607, -(_11607 = _11609)], (10 ^ _11376) ^ [_11811, _11813, _11815] : [-(_11815 = _11811), _11815 = _11813, _11813 = _11811], (20 ^ _11376) ^ [_12124, _12126] : [_12126 = _12124, -(proj1S(_12126) = proj1S(_12124))], (26 ^ _11376) ^ [_12342, _12344] : [_12344 = _12342, -(s(_12344) = s(_12342))], (32 ^ _11376) ^ [_12568, _12570, _12572, _12574] : [-(x2(_12574, _12570) = x2(_12572, _12568)), _12574 = _12572, _12570 = _12568]], input).
% 0.32/1.38 ncf('1',plain,[x2(z, z) = z],start(50 ^ 0,bind([[_13199], [z]]))).
% 0.32/1.38 ncf('1.1',plain,[-(x2(z, z) = z)],extension(46 ^ 1,bind([[_13041], [z]]))).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------