%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM853+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:48 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM853+2 : TPTP v8.1.2. Released v4.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n028.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:56:03 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(296 ^ _60757) ^ [] : [greater(vd486, vd488)], (76 ^ _60757) ^ [_63321, _63323, _63325, _63327] : [-(vmul(_63327, _63323) = vmul(_63325, _63321)), _63327 = _63325, _63323 = _63321], (86 ^ _60757) ^ [_63680, _63682, _63684, _63686] : [-(vplus(_63686, _63682) = vplus(_63684, _63680)), _63686 = _63684, _63682 = _63680], (96 ^ _60757) ^ [_64011, _64013] : [_64013 = _64011, -(vskolem2(_64013) = vskolem2(_64011))], (102 ^ _60757) ^ [_64209, _64211] : [_64211 = _64209, -(vsucc(_64211) = vsucc(_64209))], (2 ^ _60757) ^ [_60901] : [-(_60901 = _60901)], (4 ^ _60757) ^ [_61008, _61010] : [_61010 = _61008, -(_61008 = _61010)], (10 ^ _60757) ^ [_61212, _61214, _61216] : [-(_61216 = _61212), _61216 = _61214, _61214 = _61212], (20 ^ _60757) ^ [_61553, _61555, _61557, _61559] : [-(leq(_61557, _61553)), leq(_61559, _61555), _61559 = _61557, _61555 = _61553], (34 ^ _60757) ^ [_61997, _61999, _62001, _62003] : [-(geq(_62001, _61997)), geq(_62003, _61999), _62003 = _62001, _61999 = _61997], (48 ^ _60757) ^ [_62441, _62443, _62445, _62447] : [-(less(_62445, _62441)), less(_62447, _62443), _62447 = _62445, _62443 = _62441], (62 ^ _60757) ^ [_62865, _62867, _62869, _62871] : [-(greater(_62869, _62865)), greater(_62871, _62867), _62871 = _62869, _62867 = _62865], (108 ^ _60757) ^ [] : [-(greater(vmul(vd486, vd487), vmul(vd488, vd487)))], (110 ^ _60757) ^ [_64508, _64510, _64512] : [less(_64510, _64508), -(less(vmul(_64510, _64512), vmul(_64508, _64512)))], (116 ^ _60757) ^ [_64750, _64752, _64754] : [_64752 = _64750, -(vmul(_64752, _64754) = vmul(_64750, _64754))], (122 ^ _60757) ^ [_64992, _64994, _64996] : [greater(_64994, _64992), -(greater(vmul(_64994, _64996), vmul(_64992, _64996)))], (128 ^ _60757) ^ [_65219, _65221, _65223] : [-(vmul(vmul(_65223, _65221), _65219) = vmul(_65223, vmul(_65221, _65219)))], (130 ^ _60757) ^ [_65341, _65343, _65345] : [-(vmul(_65345, vplus(_65343, _65341)) = vplus(vmul(_65345, _65343), vmul(_65345, _65341)))], (132 ^ _60757) ^ [_65452, _65454] : [-(vmul(_65454, _65452) = vmul(_65452, _65454))], (134 ^ _60757) ^ [_65552, _65554] : [-(vmul(vsucc(_65554), _65552) = vplus(vmul(_65554, _65552), _65552))], (136 ^ _60757) ^ [_65643] : [-(vmul(v1, _65643) = _65643)], (138 ^ _60757) ^ [_65758, _65760] : [-(vmul(_65760, vsucc(_65758)) = vplus(vmul(_65760, _65758), _65760))], (140 ^ _60757) ^ [_65815, _65817] : [-(vmul(_65817, v1) = _65817)], (142 ^ _60757) ^ [_65929, _65931] : [less(_65931, vplus(_65929, v1)), -(leq(_65931, _65929))], (148 ^ _60757) ^ [_66145, _66147] : [greater(_66147, _66145), -(geq(_66147, vplus(_66145, v1)))], (154 ^ _60757) ^ [_66332] : [-(geq(_66332, v1))], (156 ^ _60757) ^ [_66467, _66469, _66471, _66473] : [-(geq(vplus(_66473, _66469), vplus(_66471, _66467))), geq(_66469, _66467), geq(_66473, _66471)], (166 ^ _60757) ^ [_66798, _66800] : [less(_66800, _66798), -(greater(_66798, _66800))], (172 ^ _60757) ^ [_67008, _67010] : [greater(_67010, _67008), -(less(_67008, _67010))], (178 ^ _60757) ^ [_67218, _67220] : [-(_67220 = _67218), -(greater(_67220, _67218)), -(less(_67220, _67218))], (188 ^ _60757) ^ [_67519, _67521] : [_67521 = _67519, less(_67521, _67519)], (194 ^ _60757) ^ [_67732, _67734] : [greater(_67734, _67732), less(_67734, _67732)], (200 ^ _60757) ^ [_67945, _67947] : [_67947 = _67945, greater(_67947, _67945)], (206 ^ _60757) ^ [_68187, _68189] : [less(_68187, _68189), -(_68189 = vplus(_68187, 209 ^ [_68187, _68189]))], (213 ^ _60757) ^ [_68415, _68417] : [214 ^ _60757 : [(215 ^ _60757) ^ [_68488] : [_68417 = vplus(_68415, _68488)]], -(less(_68415, _68417))], (219 ^ _60757) ^ [_68684, _68686] : [greater(_68684, _68686), -(_68684 = vplus(_68686, 222 ^ [_68684, _68686]))], (226 ^ _60757) ^ [_68912, _68914] : [227 ^ _60757 : [(228 ^ _60757) ^ [_68985] : [_68912 = vplus(_68914, _68985)]], -(greater(_68912, _68914))], (232 ^ _60757) ^ [_69152, _69154] : [-(_69154 = _69152), -(_69154 = vplus(_69152, 237 ^ [_69152, _69154])), -(_69152 = vplus(_69154, 240 ^ [_69152, _69154]))], (244 ^ _60757) ^ [_69585, _69587] : [_69587 = _69585, 247 ^ _60757 : [(248 ^ _60757) ^ [_69707] : [_69585 = vplus(_69587, _69707)]]], (250 ^ _60757) ^ [_69826, _69828] : [251 ^ _60757 : [(252 ^ _60757) ^ [_69911] : [_69828 = vplus(_69826, _69911)]], 253 ^ _60757 : [(254 ^ _60757) ^ [_69975] : [_69826 = vplus(_69828, _69975)]]], (256 ^ _60757) ^ [_70095, _70097] : [_70097 = _70095, 259 ^ _60757 : [(260 ^ _60757) ^ [_70217] : [_70097 = vplus(_70095, _70217)]]], (262 ^ _60757) ^ [_70336, _70338] : [-(_70338 = _70336), 265 ^ _60757 : [(266 ^ _60757) ^ [_70462] : [vplus(_70462, _70338) = vplus(_70462, _70336)]]], (268 ^ _60757) ^ [_70568, _70570] : [_70568 = vplus(_70570, _70568)], (270 ^ _60757) ^ [_70665, _70667] : [-(vplus(_70665, _70667) = vplus(_70667, _70665))], (272 ^ _60757) ^ [_70765, _70767] : [-(vplus(vsucc(_70767), _70765) = vsucc(vplus(_70767, _70765)))], (274 ^ _60757) ^ [_70855] : [-(vplus(v1, _70855) = vsucc(_70855))], (276 ^ _60757) ^ [_70966, _70968, _70970] : [-(vplus(vplus(_70970, _70968), _70966) = vplus(_70970, vplus(_70968, _70966)))], (278 ^ _60757) ^ [_71094, _71096] : [-(vplus(_71096, vsucc(_71094)) = vsucc(vplus(_71096, _71094)))], (280 ^ _60757) ^ [_71150, _71152] : [-(vplus(_71152, v1) = vsucc(_71152))], (282 ^ _60757) ^ [_71252] : [-(_71252 = v1), -(_71252 = vsucc(vskolem2(_71252)))], (288 ^ _60757) ^ [_71437] : [vsucc(_71437) = _71437], (290 ^ _60757) ^ [_71526, _71528] : [-(_71528 = _71526), vsucc(_71528) = vsucc(_71526)]], input).
% 0.34/1.37 ncf('1',plain,[greater(vd486, vd488)],start(296 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(greater(vd486, vd488)), -(vd486 = vd488), -(less(vd486, vd488))],extension(178 ^ 1,bind([[_67218, _67220], [vd488, vd486]]))).
% 0.34/1.37 ncf('1.1.1',plain,[vd486 = vd488, -(vmul(vd486, vd487) = vmul(vd488, vd487)), vd487 = vd487],extension(76 ^ 2,bind([[_63321, _63323, _63325, _63327], [vd487, vd487, vd488, vd486]]))).
% 0.34/1.37 ncf('1.1.1.1',plain,[vmul(vd486, vd487) = vmul(vd488, vd487), greater(vmul(vd486, vd487), vmul(vd488, vd487))],extension(200 ^ 3,bind([[_67945, _67947], [vmul(vd488, vd487), vmul(vd486, vd487)]]))).
% 0.34/1.37 ncf('1.1.1.1.1',plain,[-(greater(vmul(vd486, vd487), vmul(vd488, vd487)))],extension(108 ^ 4)).
% 0.34/1.37 ncf('1.1.1.2',plain,[-(vd487 = vd487)],extension(2 ^ 3,bind([[_60901], [vd487]]))).
% 0.34/1.37 ncf('1.1.2',plain,[less(vd486, vd488), -(less(vmul(vd486, vd487), vmul(vd488, vd487)))],extension(110 ^ 2,bind([[_64508, _64510, _64512], [vd488, vd486, vd487]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[less(vmul(vd486, vd487), vmul(vd488, vd487)), greater(vmul(vd486, vd487), vmul(vd488, vd487))],extension(194 ^ 3,bind([[_67732, _67734], [vmul(vd488, vd487), vmul(vd486, vd487)]]))).
% 0.34/1.37 ncf('1.1.2.1.1',plain,[-(greater(vmul(vd486, vd487), vmul(vd488, vd487)))],extension(108 ^ 4)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------