%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM838+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:44 EDT 2023
% Result : Theorem 0.23s 1.33s
% Output : Proof 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NUM838+2 : TPTP v8.1.2. Released v4.1.0.
% 0.09/0.10 % Command : nanocop.sh %s %d
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Thu May 18 17:05:04 EDT 2023
% 0.09/0.29 % CPUTime :
% 0.23/1.33
% 0.23/1.33 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.23/1.33 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/1.33 %-----------------------------------------------------
% 0.23/1.33 ncf(matrix, plain, [(268 ^ _53792) ^ [] : [greater(vplus(vd301, vd303), vplus(vd302, vd303))], (62 ^ _53792) ^ [_55910, _55912, _55914, _55916] : [-(vskolem7(_55916, _55912) = vskolem7(_55914, _55910)), _55916 = _55914, _55912 = _55910], (72 ^ _53792) ^ [_56241, _56243] : [_56243 = _56241, -(vsucc(_56243) = vsucc(_56241))], (78 ^ _53792) ^ [_56467, _56469, _56471, _56473] : [-(vplus(_56473, _56469) = vplus(_56471, _56467)), _56473 = _56471, _56469 = _56467], (2 ^ _53792) ^ [_53936] : [-(_53936 = _53936)], (4 ^ _53792) ^ [_54043, _54045] : [_54045 = _54043, -(_54043 = _54045)], (10 ^ _53792) ^ [_54247, _54249, _54251] : [-(_54251 = _54247), _54251 = _54249, _54249 = _54247], (20 ^ _53792) ^ [_54588, _54590, _54592, _54594] : [-(leq(_54592, _54588)), leq(_54594, _54590), _54594 = _54592, _54590 = _54588], (34 ^ _53792) ^ [_55032, _55034, _55036, _55038] : [-(less(_55036, _55032)), less(_55038, _55034), _55038 = _55036, _55034 = _55032], (48 ^ _53792) ^ [_55456, _55458, _55460, _55462] : [-(greater(_55460, _55456)), greater(_55462, _55458), _55462 = _55460, _55458 = _55456], (88 ^ _53792) ^ [] : [-(greater(vd301, vd302))], (90 ^ _53792) ^ [_56875, _56877, _56879] : [less(_56877, _56875), -(less(vplus(_56877, _56879), vplus(_56875, _56879)))], (96 ^ _53792) ^ [_57117, _57119, _57121] : [less(_57119, _57117), -(greater(vplus(_57117, _57121), vplus(_57119, _57121)))], (102 ^ _53792) ^ [_57359, _57361, _57363] : [less(_57361, _57359), -(greater(_57359, _57361))], (108 ^ _53792) ^ [_57589, _57591, _57593] : [_57591 = _57589, -(vplus(_57591, _57593) = vplus(_57589, _57593))], (114 ^ _53792) ^ [_57831, _57833, _57835] : [greater(_57833, _57831), -(greater(vplus(_57833, _57835), vplus(_57831, _57835)))], (120 ^ _53792) ^ [_58073, _58075, _58077] : [greater(_58075, _58073), -(vplus(vskolem7(_58075, _58073), vplus(_58073, _58077)) = vplus(vplus(_58073, _58077), vskolem7(_58075, _58073)))], (126 ^ _53792) ^ [_58339, _58341, _58343] : [greater(_58341, _58339), -(vplus(vplus(vskolem7(_58341, _58339), _58339), _58343) = vplus(vskolem7(_58341, _58339), vplus(_58339, _58343)))], (132 ^ _53792) ^ [_58605, _58607, _58609] : [greater(_58607, _58605), -(vplus(vplus(_58605, vskolem7(_58607, _58605)), _58609) = vplus(vplus(vskolem7(_58607, _58605), _58605), _58609))], (138 ^ _53792) ^ [_58871, _58873, _58875] : [greater(_58873, _58871), -(vplus(_58873, _58875) = vplus(vplus(_58871, vskolem7(_58873, _58871)), _58875))], (144 ^ _53792) ^ [_59125, _59127, _59129] : [greater(_59127, _59125), -(_59127 = vplus(_59125, vskolem7(_59127, _59125)))], (150 ^ _53792) ^ [_59338, _59340] : [-(greater(vplus(_59340, _59338), _59340))], (152 ^ _53792) ^ [_59464, _59466, _59468] : [-(leq(_59468, _59464)), leq(_59466, _59464), leq(_59468, _59466)], (162 ^ _53792) ^ [_59773, _59775] : [less(_59775, _59773), -(greater(_59773, _59775))], (168 ^ _53792) ^ [_59983, _59985] : [greater(_59985, _59983), -(less(_59983, _59985))], (174 ^ _53792) ^ [_60193, _60195] : [-(_60195 = _60193), -(greater(_60195, _60193)), -(less(_60195, _60193))], (184 ^ _53792) ^ [_60494, _60496] : [_60496 = _60494, less(_60496, _60494)], (190 ^ _53792) ^ [_60707, _60709] : [greater(_60709, _60707), less(_60709, _60707)], (196 ^ _53792) ^ [_60920, _60922] : [_60922 = _60920, greater(_60922, _60920)], (202 ^ _53792) ^ [_61162, _61164] : [less(_61162, _61164), -(_61164 = vplus(_61162, 205 ^ [_61162, _61164]))], (209 ^ _53792) ^ [_61390, _61392] : [210 ^ _53792 : [(211 ^ _53792) ^ [_61463] : [_61392 = vplus(_61390, _61463)]], -(less(_61390, _61392))], (215 ^ _53792) ^ [_61659, _61661] : [greater(_61659, _61661), -(_61659 = vplus(_61661, 218 ^ [_61659, _61661]))], (222 ^ _53792) ^ [_61887, _61889] : [223 ^ _53792 : [(224 ^ _53792) ^ [_61960] : [_61887 = vplus(_61889, _61960)]], -(greater(_61887, _61889))], (228 ^ _53792) ^ [_62127, _62129] : [-(_62129 = _62127), -(_62129 = vplus(_62127, 233 ^ [_62127, _62129])), -(_62127 = vplus(_62129, 236 ^ [_62127, _62129]))], (240 ^ _53792) ^ [_62560, _62562] : [_62562 = _62560, 243 ^ _53792 : [(244 ^ _53792) ^ [_62682] : [_62560 = vplus(_62562, _62682)]]], (246 ^ _53792) ^ [_62801, _62803] : [247 ^ _53792 : [(248 ^ _53792) ^ [_62886] : [_62803 = vplus(_62801, _62886)]], 249 ^ _53792 : [(250 ^ _53792) ^ [_62950] : [_62801 = vplus(_62803, _62950)]]], (258 ^ _53792) ^ [_63296, _63298] : [-(vplus(_63296, _63298) = vplus(_63298, _63296))], (260 ^ _53792) ^ [_63396, _63398] : [-(vplus(vsucc(_63398), _63396) = vsucc(vplus(_63398, _63396)))], (262 ^ _53792) ^ [_63514, _63516, _63518] : [-(vplus(vplus(_63518, _63516), _63514) = vplus(_63518, vplus(_63516, _63514)))], (264 ^ _53792) ^ [_63622, _63624] : [-(vplus(_63624, vsucc(_63622)) = vsucc(vplus(_63624, _63622)))], (266 ^ _53792) ^ [_63678, _63680] : [-(vplus(_63680, v1) = vsucc(_63680))], (252 ^ _53792) ^ [_63070, _63072] : [_63072 = _63070, 255 ^ _53792 : [(256 ^ _53792) ^ [_63192] : [_63072 = vplus(_63070, _63192)]]]], input).
% 0.23/1.33 ncf('1',plain,[greater(vplus(vd301, vd303), vplus(vd302, vd303))],start(268 ^ 0)).
% 0.23/1.33 ncf('1.1',plain,[-(greater(vplus(vd301, vd303), vplus(vd302, vd303))), greater(vd301, vd302)],extension(114 ^ 1,bind([[_57831, _57833, _57835], [vd302, vd301, vd303]]))).
% 0.23/1.33 ncf('1.1.1',plain,[-(greater(vd301, vd302))],extension(88 ^ 2)).
% 0.23/1.33 %-----------------------------------------------------
% 0.23/1.33 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------