%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM836+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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 : Fri May 19 11:45:43 EDT 2023
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUM836+2 : TPTP v8.1.2. Released v4.1.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n009.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 17:32:48 EDT 2023
% 0.14/0.36 % CPUTime :
% 0.36/1.40
% 0.36/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 ncf(matrix, plain, [(138 ^ _27113) ^ [] : [-(greater(vd203, vd204))], (140 ^ _27113) ^ [] : [-(less(vd203, vd204))], (58 ^ _27113) ^ [_29096, _29098] : [_29098 = _29096, -(vsucc(_29098) = vsucc(_29096))], (48 ^ _27113) ^ [_28785, _28787, _28789, _28791] : [-(vplus(_28791, _28787) = vplus(_28789, _28785)), _28791 = _28789, _28787 = _28785], (2 ^ _27113) ^ [_27257] : [-(_27257 = _27257)], (4 ^ _27113) ^ [_27364, _27366] : [_27366 = _27364, -(_27364 = _27366)], (10 ^ _27113) ^ [_27568, _27570, _27572] : [-(_27572 = _27568), _27572 = _27570, _27570 = _27568], (20 ^ _27113) ^ [_27909, _27911, _27913, _27915] : [-(greater(_27913, _27909)), greater(_27915, _27911), _27915 = _27913, _27911 = _27909], (34 ^ _27113) ^ [_28333, _28335, _28337, _28339] : [-(less(_28337, _28333)), less(_28339, _28335), _28339 = _28337, _28335 = _28333], (64 ^ _27113) ^ [] : [vd203 = vd204, greater(vd203, vd204)], (70 ^ _27113) ^ [_29467, _29469] : [less(_29467, _29469), -(_29469 = vplus(_29467, 73 ^ [_29467, _29469]))], (77 ^ _27113) ^ [_29695, _29697] : [78 ^ _27113 : [(79 ^ _27113) ^ [_29768] : [_29697 = vplus(_29695, _29768)]], -(less(_29695, _29697))], (83 ^ _27113) ^ [_29964, _29966] : [greater(_29964, _29966), -(_29964 = vplus(_29966, 86 ^ [_29964, _29966]))], (90 ^ _27113) ^ [_30192, _30194] : [91 ^ _27113 : [(92 ^ _27113) ^ [_30265] : [_30192 = vplus(_30194, _30265)]], -(greater(_30192, _30194))], (96 ^ _27113) ^ [_30432, _30434] : [-(_30434 = _30432), -(_30434 = vplus(_30432, 101 ^ [_30432, _30434])), -(_30432 = vplus(_30434, 104 ^ [_30432, _30434]))], (108 ^ _27113) ^ [_30865, _30867] : [_30867 = _30865, 111 ^ _27113 : [(112 ^ _27113) ^ [_30987] : [_30865 = vplus(_30867, _30987)]]], (114 ^ _27113) ^ [_31106, _31108] : [115 ^ _27113 : [(116 ^ _27113) ^ [_31191] : [_31108 = vplus(_31106, _31191)]], 117 ^ _27113 : [(118 ^ _27113) ^ [_31255] : [_31106 = vplus(_31108, _31255)]]], (120 ^ _27113) ^ [_31375, _31377] : [_31377 = _31375, 123 ^ _27113 : [(124 ^ _27113) ^ [_31497] : [_31377 = vplus(_31375, _31497)]]], (132 ^ _27113) ^ [_31863, _31865, _31867] : [-(vplus(vplus(_31867, _31865), _31863) = vplus(_31867, vplus(_31865, _31863)))], (134 ^ _27113) ^ [_31971, _31973] : [-(vplus(_31973, vsucc(_31971)) = vsucc(vplus(_31973, _31971)))], (136 ^ _27113) ^ [_32027, _32029] : [-(vplus(_32029, v1) = vsucc(_32029))], (126 ^ _27113) ^ [_31616, _31618] : [-(_31618 = _31616), 129 ^ _27113 : [(130 ^ _27113) ^ [_31742] : [vplus(_31742, _31618) = vplus(_31742, _31616)]]]], input).
% 0.36/1.40 ncf('1',plain,[vd203 = vd204, greater(vd203, vd204)],start(64 ^ 0)).
% 0.36/1.40 ncf('1.1',plain,[-(vd203 = vd204), -(vd203 = vplus(vd204, 101 ^ [vd204, vd203])), -(vd204 = vplus(vd203, 104 ^ [vd204, vd203]))],extension(96 ^ 1,bind([[_30432, _30434], [vd204, vd203]]))).
% 0.36/1.40 ncf('1.1.1',plain,[vd203 = vplus(vd204, 101 ^ [vd204, vd203]), 118 : vd204 = vplus(vd203, 73 ^ [vd203, vd204])],extension(114 ^ 2,bind([[_31106, _31108, _31191, _31255], [vd204, vd203, 101 ^ [vd204, vd203], 73 ^ [vd203, vd204]]]))).
% 0.36/1.40 ncf('1.1.1.1',plain,[-(vd204 = vplus(vd203, 73 ^ [vd203, vd204])), less(vd203, vd204)],extension(70 ^ 5,bind([[_29467, _29469], [vd203, vd204]]))).
% 0.36/1.40 ncf('1.1.1.1.1',plain,[-(less(vd203, vd204))],extension(140 ^ 6)).
% 0.36/1.40 ncf('1.1.2',plain,[vd204 = vplus(vd203, 104 ^ [vd204, vd203]), 118 : vd203 = vplus(vd204, 86 ^ [vd203, vd204])],extension(114 ^ 2,bind([[_31106, _31108, _31191, _31255], [vd203, vd204, 104 ^ [vd204, vd203], 86 ^ [vd203, vd204]]]))).
% 0.36/1.40 ncf('1.1.2.1',plain,[-(vd203 = vplus(vd204, 86 ^ [vd203, vd204])), greater(vd203, vd204)],extension(83 ^ 5,bind([[_29964, _29966], [vd203, vd204]]))).
% 0.36/1.40 ncf('1.1.2.1.1',plain,[-(greater(vd203, vd204))],extension(138 ^ 6)).
% 0.36/1.40 ncf('1.2',plain,[-(greater(vd203, vd204))],extension(138 ^ 1)).
% 0.36/1.40 %-----------------------------------------------------
% 0.36/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------