%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM835+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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 101.65s 98.81s
% Output : Proof 101.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM835+1 : TPTP v8.1.2. Released v4.1.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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 : Thu May 18 17:03:20 EDT 2023
% 0.12/0.33 % CPUTime :
% 101.65/98.81
% 101.65/98.81 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 101.65/98.81 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.65/98.81 %-----------------------------------------------------
% 101.65/98.81 ncf(matrix, plain, [(309 ^ _57882) ^ [_68371] : [vd165 = vplus(vd151, _68371)], (311 ^ _57882) ^ [_68451] : [vd151 = vplus(vd165, _68451)], (313 ^ _57882) ^ [] : [vd151 = vd165], (30 ^ _57882) ^ [_58927, _58929] : [_58929 = _58927, -(vskolem2(_58929) = vskolem2(_58927))], (36 ^ _57882) ^ [_59145, _59147] : [_59147 = _59145, -(vsucc(_59147) = vsucc(_59145))], (42 ^ _57882) ^ [_59371, _59373, _59375, _59377] : [-(vplus(_59377, _59373) = vplus(_59375, _59371)), _59377 = _59375, _59373 = _59371], (20 ^ _57882) ^ [_58630, _58632] : [-(m(_58630)), _58632 = _58630, m(_58632)], (2 ^ _57882) ^ [_58026] : [-(_58026 = _58026)], (4 ^ _57882) ^ [_58133, _58135] : [_58135 = _58133, -(_58133 = _58135)], (10 ^ _57882) ^ [_58337, _58339, _58341] : [-(_58341 = _58337), _58341 = _58339, _58339 = _58337], (52 ^ _57882) ^ [_59698] : [vd165 = vplus(vd151, _59698), -(m(vsucc(vd165)))], (58 ^ _57882) ^ [_59885] : [vd165 = vplus(vd151, _59885), -(vsucc(vplus(vd151, _59885)) = vplus(vd151, vsucc(_59885)))], (64 ^ _57882) ^ [_60101] : [vd165 = vplus(vd151, _60101), -(vsucc(vd165) = vsucc(vplus(vd151, _60101)))], (70 ^ _57882) ^ [_60307] : [vd151 = vplus(vd165, _60307), -(_60307 = v1), -(m(vsucc(vd165)))], (80 ^ _57882) ^ [_60585] : [vd151 = vplus(vd165, _60585), -(_60585 = v1), -(vplus(vplus(vd165, v1), vskolem3) = vplus(vsucc(vd165), vskolem3))], (90 ^ _57882) ^ [_60863] : [vd151 = vplus(vd165, _60863), -(_60863 = v1), -(vplus(vd165, vplus(v1, vskolem3)) = vplus(vplus(vd165, v1), vskolem3))], (100 ^ _57882) ^ [_61141] : [vd151 = vplus(vd165, _61141), -(_61141 = v1), -(vd151 = vplus(vd165, vplus(v1, vskolem3)))], (110 ^ _57882) ^ [_61419] : [vd151 = vplus(vd165, _61419), -(_61419 = v1), -(vsucc(vskolem3) = vplus(v1, vskolem3))], (120 ^ _57882) ^ [_61697] : [vd151 = vplus(vd165, _61697), -(_61697 = v1), -(_61697 = vsucc(vskolem3))], (130 ^ _57882) ^ [_61981] : [vd151 = vplus(vd165, _61981), _61981 = v1, -(m(vsucc(vd165)))], (140 ^ _57882) ^ [_62256] : [vd151 = vplus(vd165, _62256), _62256 = v1, -(vplus(vd165, v1) = vsucc(vd165))], (150 ^ _57882) ^ [_62531] : [vd151 = vplus(vd165, _62531), _62531 = v1, -(vd151 = vplus(vd165, v1))], (160 ^ _57882) ^ [] : [vd151 = vd165, -(m(vsucc(vd165)))], (166 ^ _57882) ^ [] : [vd151 = vd165, -(vplus(vd165, v1) = vplus(vd151, v1))], (172 ^ _57882) ^ [] : [vd151 = vd165, -(vsucc(vd165) = vplus(vd165, v1))], (178 ^ _57882) ^ [] : [-(m(vd165))], (180 ^ _57882) ^ [] : [-(m(v1))], (182 ^ _57882) ^ [_63269] : [_63269 = v1, 187 ^ _57882 : [(188 ^ _57882) ^ [] : [-(v1 = _63269)], (190 ^ _57882) ^ [] : [-(vd151 = v1)]], 192 ^ _57882 : [(193 ^ _57882) ^ [] : [-(vplus(v1, 191 ^ [_63269]) = vplus(_63269, 191 ^ [_63269]))], (195 ^ _57882) ^ [] : [-(vsucc(191 ^ [_63269]) = vplus(v1, 191 ^ [_63269]))], (197 ^ _57882) ^ [] : [-(vd151 = vsucc(191 ^ [_63269]))]]], (215 ^ _57882) ^ [_64394, _64396] : [216 ^ _57882 : [(217 ^ _57882) ^ [] : [_64396 = _64394], (219 ^ _57882) ^ [_64571] : [_64396 = vplus(_64394, _64571)], (221 ^ _57882) ^ [_64635] : [_64394 = vplus(_64396, _64635)]], -(m(_64394))], (199 ^ _57882) ^ [_63922, _63924] : [m(_63922), -(_63924 = _63922), -(_63924 = vplus(_63922, 208 ^ [_63922, _63924])), -(_63922 = vplus(_63924, 211 ^ [_63922, _63924]))], (225 ^ _57882) ^ [_64805, _64807] : [_64807 = _64805, 228 ^ _57882 : [(229 ^ _57882) ^ [_64927] : [_64805 = vplus(_64807, _64927)]]], (231 ^ _57882) ^ [_65046, _65048] : [232 ^ _57882 : [(233 ^ _57882) ^ [_65131] : [_65048 = vplus(_65046, _65131)]], 234 ^ _57882 : [(235 ^ _57882) ^ [_65195] : [_65046 = vplus(_65048, _65195)]]], (237 ^ _57882) ^ [_65315, _65317] : [_65317 = _65315, 240 ^ _57882 : [(241 ^ _57882) ^ [_65437] : [_65317 = vplus(_65315, _65437)]]], (243 ^ _57882) ^ [_65584, _65586, _65588, _65590] : [_65588 = vplus(_65590, _65584), _65590 = vplus(_65588, _65586)], (249 ^ _57882) ^ [_65845, _65847, _65849, _65851] : [_65849 = vplus(_65851, _65845), _65851 = vplus(_65849, _65847)], (255 ^ _57882) ^ [_66092, _66094, _66096] : [_66094 = vplus(_66096, _66092), _66096 = _66094], (261 ^ _57882) ^ [_66327, _66329, _66331] : [_66331 = vplus(_66329, _66327), _66331 = _66329], (267 ^ _57882) ^ [_66548, _66550] : [-(_66550 = _66548), 270 ^ _57882 : [(271 ^ _57882) ^ [_66674] : [vplus(_66674, _66550) = vplus(_66674, _66548)]]], (273 ^ _57882) ^ [_66780, _66782] : [_66780 = vplus(_66782, _66780)], (275 ^ _57882) ^ [_66877, _66879] : [-(vplus(_66877, _66879) = vplus(_66879, _66877))], (277 ^ _57882) ^ [_66977, _66979] : [-(vplus(vsucc(_66979), _66977) = vsucc(vplus(_66979, _66977)))], (279 ^ _57882) ^ [_67067] : [-(vplus(v1, _67067) = vsucc(_67067))], (281 ^ _57882) ^ [_67178, _67180, _67182] : [-(vplus(vplus(_67182, _67180), _67178) = vplus(_67182, vplus(_67180, _67178)))], (283 ^ _57882) ^ [_67306, _67308] : [-(vplus(_67308, vsucc(_67306)) = vsucc(vplus(_67308, _67306)))], (285 ^ _57882) ^ [_67362, _67364] : [-(vplus(_67364, v1) = vsucc(_67364))], (287 ^ _57882) ^ [_67464] : [-(_67464 = v1), -(_67464 = vsucc(vskolem2(_67464)))], (293 ^ _57882) ^ [_67649] : [vsucc(_67649) = _67649], (295 ^ _57882) ^ [_67758, _67760] : [-(_67760 = _67758), vsucc(_67760) = vsucc(_67758)], (307 ^ _57882) ^ [_68148] : [vsucc(_68148) = v1], (301 ^ _57882) ^ [_67980, _67982] : [vsucc(_67982) = vsucc(_67980), -(_67982 = _67980)]], input).
% 101.65/98.81 ncf('1',plain,[vd165 = vplus(vd151, 211 ^ [vd165, vd151])],start(309 ^ 0,bind([[_68371], [211 ^ [vd165, vd151]]]))).
% 101.65/98.81 ncf('1.1',plain,[-(vd165 = vplus(vd151, 211 ^ [vd165, vd151])), m(vd165), -(vd151 = vd165), -(vd151 = vplus(vd165, 208 ^ [vd165, vd151]))],extension(199 ^ 1,bind([[_63922, _63924], [vd165, vd151]]))).
% 101.65/98.81 ncf('1.1.1',plain,[-(m(vd165))],extension(178 ^ 2)).
% 101.65/98.81 ncf('1.1.2',plain,[vd151 = vd165],extension(313 ^ 2)).
% 101.65/98.81 ncf('1.1.3',plain,[vd151 = vplus(vd165, 208 ^ [vd165, vd151])],extension(311 ^ 2,bind([[_68451], [208 ^ [vd165, vd151]]]))).
% 101.65/98.81 %-----------------------------------------------------
% 101.65/98.81 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------