%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM855+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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 1.20s 1.39s
% Output : Proof 1.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM855+2 : TPTP v8.1.2. Released v4.1.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 17:30:17 EDT 2023
% 0.13/0.34 % CPUTime :
% 1.20/1.39
% 1.20/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 1.20/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.20/1.39 %-----------------------------------------------------
% 1.20/1.39 ncf(matrix, plain, [(480 ^ _94214) ^ [] : [greater(vmul(vd508, vd511), vmul(vd509, vd512))], (76 ^ _94214) ^ [_96778, _96780, _96782, _96784] : [-(vplus(_96784, _96780) = vplus(_96782, _96778)), _96784 = _96782, _96780 = _96778], (86 ^ _94214) ^ [_97109, _97111] : [_97111 = _97109, -(vskolem2(_97111) = vskolem2(_97109))], (92 ^ _94214) ^ [_97327, _97329] : [_97329 = _97327, -(vsucc(_97329) = vsucc(_97327))], (98 ^ _94214) ^ [_97553, _97555, _97557, _97559] : [-(vmul(_97559, _97555) = vmul(_97557, _97553)), _97559 = _97557, _97555 = _97553], (2 ^ _94214) ^ [_94358] : [-(_94358 = _94358)], (4 ^ _94214) ^ [_94465, _94467] : [_94467 = _94465, -(_94465 = _94467)], (10 ^ _94214) ^ [_94669, _94671, _94673] : [-(_94673 = _94669), _94673 = _94671, _94671 = _94669], (20 ^ _94214) ^ [_95010, _95012, _95014, _95016] : [-(leq(_95014, _95010)), leq(_95016, _95012), _95016 = _95014, _95012 = _95010], (34 ^ _94214) ^ [_95454, _95456, _95458, _95460] : [-(geq(_95458, _95454)), geq(_95460, _95456), _95460 = _95458, _95456 = _95454], (48 ^ _94214) ^ [_95898, _95900, _95902, _95904] : [-(less(_95902, _95898)), less(_95904, _95900), _95904 = _95902, _95900 = _95898], (62 ^ _94214) ^ [_96322, _96324, _96326, _96328] : [-(greater(_96326, _96322)), greater(_96328, _96324), _96328 = _96326, _96324 = _96322], (108 ^ _94214) ^ [] : [-(vmul(vd512, vd509) = vmul(vd509, vd512))], (110 ^ _94214) ^ [] : [-(greater(vmul(vd511, vd509), vmul(vd512, vd509)))], (112 ^ _94214) ^ [] : [-(vmul(vd509, vd511) = vmul(vd511, vd509))], (114 ^ _94214) ^ [] : [-(greater(vmul(vd508, vd511), vmul(vd509, vd511)))], (116 ^ _94214) ^ [] : [-(greater(vd511, vd512))], (118 ^ _94214) ^ [] : [-(greater(vd508, vd509))], (120 ^ _94214) ^ [_98230, _98232, _98234] : [less(vmul(_98234, _98232), vmul(_98230, _98232)), -(less(_98234, _98230))], (126 ^ _94214) ^ [_98472, _98474, _98476] : [vmul(_98476, _98474) = vmul(_98472, _98474), -(_98476 = _98472)], (132 ^ _94214) ^ [_98714, _98716, _98718] : [greater(vmul(_98718, _98716), vmul(_98714, _98716)), -(greater(_98718, _98714))], (138 ^ _94214) ^ [_98956, _98958, _98960] : [less(_98958, _98956), -(less(vmul(_98958, _98960), vmul(_98956, _98960)))], (144 ^ _94214) ^ [_99198, _99200, _99202] : [_99200 = _99198, -(vmul(_99200, _99202) = vmul(_99198, _99202))], (150 ^ _94214) ^ [_99440, _99442, _99444] : [greater(_99442, _99440), -(greater(vmul(_99442, _99444), vmul(_99440, _99444)))], (156 ^ _94214) ^ [_99667, _99669, _99671] : [-(vmul(vmul(_99671, _99669), _99667) = vmul(_99671, vmul(_99669, _99667)))], (158 ^ _94214) ^ [_99789, _99791, _99793] : [-(vmul(_99793, vplus(_99791, _99789)) = vplus(vmul(_99793, _99791), vmul(_99793, _99789)))], (160 ^ _94214) ^ [_99900, _99902] : [-(vmul(_99902, _99900) = vmul(_99900, _99902))], (162 ^ _94214) ^ [_100000, _100002] : [-(vmul(vsucc(_100002), _100000) = vplus(vmul(_100002, _100000), _100000))], (164 ^ _94214) ^ [_100091] : [-(vmul(v1, _100091) = _100091)], (166 ^ _94214) ^ [_100206, _100208] : [-(vmul(_100208, vsucc(_100206)) = vplus(vmul(_100208, _100206), _100208))], (168 ^ _94214) ^ [_100263, _100265] : [-(vmul(_100265, v1) = _100265)], (170 ^ _94214) ^ [_100377, _100379] : [less(_100379, vplus(_100377, v1)), -(leq(_100379, _100377))], (176 ^ _94214) ^ [_100593, _100595] : [greater(_100595, _100593), -(geq(_100595, vplus(_100593, v1)))], (182 ^ _94214) ^ [_100780] : [-(geq(_100780, v1))], (184 ^ _94214) ^ [_100915, _100917, _100919, _100921] : [-(geq(vplus(_100921, _100917), vplus(_100919, _100915))), geq(_100917, _100915), geq(_100921, _100919)], (194 ^ _94214) ^ [_101274, _101276, _101278, _101280] : [-(greater(vplus(_101280, _101276), vplus(_101278, _101274))), 195 ^ _94214 : [(196 ^ _94214) ^ [] : [greater(_101276, _101274), geq(_101280, _101278)], (202 ^ _94214) ^ [] : [geq(_101276, _101274), greater(_101280, _101278)]]], (210 ^ _94214) ^ [_101808, _101810, _101812, _101814] : [-(greater(vplus(_101814, _101810), vplus(_101812, _101808))), greater(_101810, _101808), greater(_101814, _101812)], (220 ^ _94214) ^ [_102153, _102155, _102157] : [less(vplus(_102157, _102153), vplus(_102155, _102153)), -(less(_102157, _102155))], (226 ^ _94214) ^ [_102395, _102397, _102399] : [vplus(_102399, _102395) = vplus(_102397, _102395), -(_102399 = _102397)], (232 ^ _94214) ^ [_102637, _102639, _102641] : [greater(vplus(_102641, _102637), vplus(_102639, _102637)), -(greater(_102641, _102639))], (238 ^ _94214) ^ [_102879, _102881, _102883] : [less(_102883, _102881), -(less(vplus(_102883, _102879), vplus(_102881, _102879)))], (244 ^ _94214) ^ [_103121, _103123, _103125] : [_103125 = _103123, -(vplus(_103125, _103121) = vplus(_103123, _103121))], (250 ^ _94214) ^ [_103363, _103365, _103367] : [greater(_103367, _103365), -(greater(vplus(_103367, _103363), vplus(_103365, _103363)))], (256 ^ _94214) ^ [_103576, _103578] : [-(greater(vplus(_103578, _103576), _103578))], (258 ^ _94214) ^ [_103702, _103704, _103706] : [-(leq(_103706, _103702)), leq(_103704, _103702), leq(_103706, _103704)], (268 ^ _94214) ^ [_104025, _104027, _104029] : [-(less(_104029, _104025)), 269 ^ _94214 : [(270 ^ _94214) ^ [] : [less(_104027, _104025), leq(_104029, _104027)], (276 ^ _94214) ^ [] : [leq(_104027, _104025), less(_104029, _104027)]]], (284 ^ _94214) ^ [_104517, _104519, _104521] : [-(less(_104521, _104517)), less(_104519, _104517), less(_104521, _104519)], (294 ^ _94214) ^ [_104826, _104828] : [leq(_104828, _104826), -(geq(_104826, _104828))], (300 ^ _94214) ^ [_105036, _105038] : [geq(_105038, _105036), -(leq(_105036, _105038))], (316 ^ _94214) ^ [_105527, _105529] : [317 ^ _94214 : [(318 ^ _94214) ^ [] : [less(_105527, _105529)], (320 ^ _94214) ^ [] : [_105527 = _105529]], -(leq(_105527, _105529))], (306 ^ _94214) ^ [_105275, _105277] : [leq(_105275, _105277), -(less(_105275, _105277)), -(_105275 = _105277)], (334 ^ _94214) ^ [_106094, _106096] : [335 ^ _94214 : [(336 ^ _94214) ^ [] : [greater(_106094, _106096)], (338 ^ _94214) ^ [] : [_106094 = _106096]], -(geq(_106094, _106096))], (324 ^ _94214) ^ [_105842, _105844] : [geq(_105842, _105844), -(greater(_105842, _105844)), -(_105842 = _105844)], (342 ^ _94214) ^ [_106380, _106382] : [less(_106382, _106380), -(greater(_106380, _106382))], (348 ^ _94214) ^ [_106590, _106592] : [greater(_106592, _106590), -(less(_106590, _106592))], (354 ^ _94214) ^ [_106800, _106802] : [-(_106802 = _106800), -(greater(_106802, _106800)), -(less(_106802, _106800))], (364 ^ _94214) ^ [_107101, _107103] : [_107103 = _107101, less(_107103, _107101)], (370 ^ _94214) ^ [_107314, _107316] : [greater(_107316, _107314), less(_107316, _107314)], (376 ^ _94214) ^ [_107527, _107529] : [_107529 = _107527, greater(_107529, _107527)], (382 ^ _94214) ^ [_107769, _107771] : [less(_107769, _107771), -(_107771 = vplus(_107769, 385 ^ [_107769, _107771]))], (389 ^ _94214) ^ [_107997, _107999] : [390 ^ _94214 : [(391 ^ _94214) ^ [_108070] : [_107999 = vplus(_107997, _108070)]], -(less(_107997, _107999))], (395 ^ _94214) ^ [_108266, _108268] : [greater(_108266, _108268), -(_108266 = vplus(_108268, 398 ^ [_108266, _108268]))], (402 ^ _94214) ^ [_108494, _108496] : [403 ^ _94214 : [(404 ^ _94214) ^ [_108567] : [_108494 = vplus(_108496, _108567)]], -(greater(_108494, _108496))], (408 ^ _94214) ^ [_108734, _108736] : [-(_108736 = _108734), -(_108736 = vplus(_108734, 413 ^ [_108734, _108736])), -(_108734 = vplus(_108736, 416 ^ [_108734, _108736]))], (420 ^ _94214) ^ [_109167, _109169] : [_109169 = _109167, 423 ^ _94214 : [(424 ^ _94214) ^ [_109289] : [_109167 = vplus(_109169, _109289)]]], (426 ^ _94214) ^ [_109408, _109410] : [427 ^ _94214 : [(428 ^ _94214) ^ [_109493] : [_109410 = vplus(_109408, _109493)]], 429 ^ _94214 : [(430 ^ _94214) ^ [_109557] : [_109408 = vplus(_109410, _109557)]]], (432 ^ _94214) ^ [_109677, _109679] : [_109679 = _109677, 435 ^ _94214 : [(436 ^ _94214) ^ [_109799] : [_109679 = vplus(_109677, _109799)]]], (438 ^ _94214) ^ [_109918, _109920] : [-(_109920 = _109918), 441 ^ _94214 : [(442 ^ _94214) ^ [_110044] : [vplus(_110044, _109920) = vplus(_110044, _109918)]]], (444 ^ _94214) ^ [_110150, _110152] : [_110150 = vplus(_110152, _110150)], (446 ^ _94214) ^ [_110247, _110249] : [-(vplus(_110247, _110249) = vplus(_110249, _110247))], (448 ^ _94214) ^ [_110347, _110349] : [-(vplus(vsucc(_110349), _110347) = vsucc(vplus(_110349, _110347)))], (450 ^ _94214) ^ [_110437] : [-(vplus(v1, _110437) = vsucc(_110437))], (452 ^ _94214) ^ [_110548, _110550, _110552] : [-(vplus(vplus(_110552, _110550), _110548) = vplus(_110552, vplus(_110550, _110548)))], (454 ^ _94214) ^ [_110676, _110678] : [-(vplus(_110678, vsucc(_110676)) = vsucc(vplus(_110678, _110676)))], (456 ^ _94214) ^ [_110732, _110734] : [-(vplus(_110734, v1) = vsucc(_110734))], (458 ^ _94214) ^ [_110834] : [-(_110834 = v1), -(_110834 = vsucc(vskolem2(_110834)))], (464 ^ _94214) ^ [_111019] : [vsucc(_111019) = _111019], (466 ^ _94214) ^ [_111128, _111130] : [-(_111130 = _111128), vsucc(_111130) = vsucc(_111128)], (478 ^ _94214) ^ [_111518] : [vsucc(_111518) = v1], (472 ^ _94214) ^ [_111350, _111352] : [vsucc(_111352) = vsucc(_111350), -(_111352 = _111350)]], input).
% 1.20/1.39 ncf('1',plain,[greater(vmul(vd508, vd511), vmul(vd509, vd512))],start(480 ^ 0)).
% 1.20/1.39 ncf('1.1',plain,[-(greater(vmul(vd508, vd511), vmul(vd509, vd512))), less(vmul(vd509, vd512), vmul(vd508, vd511))],extension(342 ^ 1,bind([[_106380, _106382], [vmul(vd508, vd511), vmul(vd509, vd512)]]))).
% 1.20/1.39 ncf('1.1.1',plain,[-(less(vmul(vd509, vd512), vmul(vd508, vd511))), less(vmul(vd509, vd511), vmul(vd508, vd511)), less(vmul(vd509, vd512), vmul(vd509, vd511))],extension(284 ^ 2,bind([[_104517, _104519, _104521], [vmul(vd508, vd511), vmul(vd509, vd511), vmul(vd509, vd512)]]))).
% 1.20/1.39 ncf('1.1.1.1',plain,[-(less(vmul(vd509, vd511), vmul(vd508, vd511))), less(vd509, vd508)],extension(138 ^ 3,bind([[_98956, _98958, _98960], [vd508, vd509, vd511]]))).
% 1.20/1.39 ncf('1.1.1.1.1',plain,[-(less(vd509, vd508)), greater(vd508, vd509)],extension(348 ^ 4,bind([[_106590, _106592], [vd509, vd508]]))).
% 1.20/1.39 ncf('1.1.1.1.1.1',plain,[-(greater(vd508, vd509))],extension(118 ^ 5)).
% 1.20/1.39 ncf('1.1.1.2',plain,[-(less(vmul(vd509, vd512), vmul(vd509, vd511))), less(vmul(vd512, vd509), vmul(vd511, vd509)), vmul(vd512, vd509) = vmul(vd509, vd512), vmul(vd511, vd509) = vmul(vd509, vd511)],extension(48 ^ 3,bind([[_95898, _95900, _95902, _95904], [vmul(vd509, vd511), vmul(vd511, vd509), vmul(vd509, vd512), vmul(vd512, vd509)]]))).
% 1.20/1.39 ncf('1.1.1.2.1',plain,[-(less(vmul(vd512, vd509), vmul(vd511, vd509))), greater(vmul(vd511, vd509), vmul(vd512, vd509))],extension(348 ^ 4,bind([[_106590, _106592], [vmul(vd512, vd509), vmul(vd511, vd509)]]))).
% 1.20/1.39 ncf('1.1.1.2.1.1',plain,[-(greater(vmul(vd511, vd509), vmul(vd512, vd509)))],extension(110 ^ 5)).
% 1.20/1.39 ncf('1.1.1.2.2',plain,[-(vmul(vd512, vd509) = vmul(vd509, vd512))],extension(108 ^ 4)).
% 1.20/1.39 ncf('1.1.1.2.3',plain,[-(vmul(vd511, vd509) = vmul(vd509, vd511)), vmul(vd509, vd511) = vmul(vd511, vd509)],extension(4 ^ 4,bind([[_94465, _94467], [vmul(vd511, vd509), vmul(vd509, vd511)]]))).
% 1.20/1.39 ncf('1.1.1.2.3.1',plain,[-(vmul(vd509, vd511) = vmul(vd511, vd509))],extension(112 ^ 5)).
% 1.20/1.39 %-----------------------------------------------------
% 1.20/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------