%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM857+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:49 EDT 2023
% Result : Theorem 70.13s 68.59s
% Output : Proof 70.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM857+1 : TPTP v8.1.2. Released v4.1.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n011.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:24:33 EDT 2023
% 0.14/0.35 % CPUTime :
% 70.13/68.59
% 70.13/68.59 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 70.13/68.59 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 70.13/68.59 %-----------------------------------------------------
% 70.13/68.59 ncf(matrix, plain, [(498 ^ _122499) ^ [] : [geq(vmul(vd526, vd529), vmul(vd527, vd530))], !, (262 ^ _104213) ^ [_113781, _113783, _113785] : [_113785 = _113783, -(vplus(_113785, _113781) = vplus(_113783, _113781))], (382 ^ _104213) ^ [_117761, _117763] : [_117763 = _117761, less(_117763, _117761)], (456 ^ _104213) ^ [_120578, _120580] : [-(_120580 = _120578), 459 ^ _104213 : [(460 ^ _104213) ^ [_120704] : [vplus(_120704, _120580) = vplus(_120704, _120578)]]], (360 ^ _104213) ^ [_117040, _117042] : [less(_117042, _117040), -(greater(_117040, _117042))], (490 ^ _104213) ^ [_122010, _122012] : [vsucc(_122012) = vsucc(_122010), -(_122012 = _122010)], (92 ^ _104213) ^ [_107306, _107308] : [_107308 = _107306, -(vsucc(_107308) = vsucc(_107306))], (462 ^ _104213) ^ [_120810, _120812] : [_120810 = vplus(_120812, _120810)], (194 ^ _104213) ^ [_111253, _111255] : [greater(_111255, _111253), -(geq(_111255, vplus(_111253, v1)))], (150 ^ _104213) ^ [_109374, _109376, _109378] : [greater(vmul(_109378, _109376), vmul(_109374, _109376)), -(greater(_109378, _109374))], (474 ^ _104213) ^ [_121392, _121394] : [-(vplus(_121394, v1) = vsucc(_121394))], (98 ^ _104213) ^ [_107532, _107534, _107536, _107538] : [-(vmul(_107538, _107534) = vmul(_107536, _107532)), _107538 = _107536, _107534 = _107532], (62 ^ _104213) ^ [_106301, _106303, _106305, _106307] : [-(geq(_106305, _106301)), geq(_106307, _106303), _106307 = _106305, _106303 = _106301], (138 ^ _104213) ^ [_108890, _108892, _108894] : [less(vmul(_108894, _108892), vmul(_108890, _108892)), -(less(_108894, _108890))], (174 ^ _104213) ^ [_110327, _110329, _110331] : [-(vmul(vmul(_110331, _110329), _110327) = vmul(_110331, vmul(_110329, _110327)))], (200 ^ _104213) ^ [_111440] : [-(geq(_111440, v1))], (256 ^ _104213) ^ [_113539, _113541, _113543] : [less(_113543, _113541), -(less(vplus(_113543, _113539), vplus(_113541, _113539)))], (110 ^ _104213) ^ [] : [-(geq(vd526, vd527))], (268 ^ _104213) ^ [_114023, _114025, _114027] : [greater(_114027, _114025), -(greater(vplus(_114027, _114023), vplus(_114025, _114023)))], (450 ^ _104213) ^ [_120337, _120339] : [_120339 = _120337, 453 ^ _104213 : [(454 ^ _104213) ^ [_120459] : [_120339 = vplus(_120337, _120459)]]], (352 ^ _104213) ^ [_116754, _116756] : [353 ^ _104213 : [(356 ^ _104213) ^ [] : [_116754 = _116756], (354 ^ _104213) ^ [] : [greater(_116754, _116756)]], -(geq(_116754, _116756))], (426 ^ _104213) ^ [_119394, _119396] : [-(_119396 = _119394), -(_119396 = vplus(_119394, 431 ^ [_119394, _119396])), -(_119394 = vplus(_119396, 434 ^ [_119394, _119396]))], (182 ^ _104213) ^ [_110751] : [-(vmul(v1, _110751) = _110751)], (162 ^ _104213) ^ [_109858, _109860, _109862] : [_109860 = _109858, -(vmul(_109860, _109862) = vmul(_109858, _109862))], (212 ^ _104213) ^ [_111934, _111936, _111938, _111940] : [-(greater(vplus(_111940, _111936), vplus(_111938, _111934))), 213 ^ _104213 : [(220 ^ _104213) ^ [] : [geq(_111936, _111934), greater(_111940, _111938)], (214 ^ _104213) ^ [] : [greater(_111936, _111934), geq(_111940, _111938)]]], (400 ^ _104213) ^ [_118429, _118431] : [less(_118429, _118431), -(_118431 = vplus(_118429, 403 ^ [_118429, _118431]))], (388 ^ _104213) ^ [_117974, _117976] : [greater(_117976, _117974), less(_117976, _117974)], (176 ^ _104213) ^ [_110449, _110451, _110453] : [-(vmul(_110453, vplus(_110451, _110449)) = vplus(vmul(_110453, _110451), vmul(_110453, _110449)))], (86 ^ _104213) ^ [_107088, _107090] : [_107090 = _107088, -(vskolem2(_107090) = vskolem2(_107088))], (302 ^ _104213) ^ [_115177, _115179, _115181] : [-(less(_115181, _115177)), less(_115179, _115177), less(_115181, _115179)], (286 ^ _104213) ^ [_114685, _114687, _114689] : [-(less(_114689, _114685)), 287 ^ _104213 : [(294 ^ _104213) ^ [] : [leq(_114687, _114685), less(_114689, _114687)], (288 ^ _104213) ^ [] : [less(_114687, _114685), leq(_114689, _114687)]]], (184 ^ _104213) ^ [_110866, _110868] : [-(vmul(_110868, vsucc(_110866)) = vplus(vmul(_110868, _110866), _110868))], (444 ^ _104213) ^ [_120068, _120070] : [445 ^ _104213 : [(446 ^ _104213) ^ [_120153] : [_120070 = vplus(_120068, _120153)]], 447 ^ _104213 : [(448 ^ _104213) ^ [_120217] : [_120068 = vplus(_120070, _120217)]]], (48 ^ _104213) ^ [_105877, _105879, _105881, _105883] : [-(greater(_105881, _105877)), greater(_105883, _105879), _105883 = _105881, _105879 = _105877], (482 ^ _104213) ^ [_121679] : [vsucc(_121679) = _121679], (2 ^ _104213) ^ [_104337] : [-(_104337 = _104337)], (420 ^ _104213) ^ [_119154, _119156] : [421 ^ _104213 : [(422 ^ _104213) ^ [_119227] : [_119154 = vplus(_119156, _119227)]], -(greater(_119154, _119156))], (144 ^ _104213) ^ [_109132, _109134, _109136] : [vmul(_109136, _109134) = vmul(_109132, _109134), -(_109136 = _109132)], (20 ^ _104213) ^ [_104989, _104991, _104993, _104995] : [-(leq(_104993, _104989)), leq(_104995, _104991), _104995 = _104993, _104991 = _104989], (366 ^ _104213) ^ [_117250, _117252] : [greater(_117252, _117250), -(less(_117250, _117252))], (470 ^ _104213) ^ [_121208, _121210, _121212] : [-(vplus(vplus(_121212, _121210), _121208) = vplus(_121212, vplus(_121210, _121208)))], (496 ^ _104213) ^ [_122178] : [vsucc(_122178) = v1], (334 ^ _104213) ^ [_116187, _116189] : [335 ^ _104213 : [(338 ^ _104213) ^ [] : [_116187 = _116189], (336 ^ _104213) ^ [] : [less(_116187, _116189)]], -(leq(_116187, _116189))], (250 ^ _104213) ^ [_113297, _113299, _113301] : [greater(vplus(_113301, _113297), vplus(_113299, _113297)), -(greater(_113301, _113299))], (76 ^ _104213) ^ [_106757, _106759, _106761, _106763] : [-(vplus(_106763, _106759) = vplus(_106761, _106757)), _106763 = _106761, _106759 = _106757], (312 ^ _104213) ^ [_115486, _115488] : [leq(_115488, _115486), -(geq(_115486, _115488))], (413 ^ _104213) ^ [_118926, _118928] : [greater(_118926, _118928), -(_118926 = vplus(_118928, 416 ^ [_118926, _118928]))], (128 ^ _104213) ^ [_108545, _108547, _108549, _108551] : [-(greater(vmul(_108551, _108547), vmul(_108549, _108545))), greater(_108547, _108545), greater(_108551, _108549)], (394 ^ _104213) ^ [_118187, _118189] : [_118189 = _118187, greater(_118189, _118187)], (372 ^ _104213) ^ [_117460, _117462] : [-(_117462 = _117460), -(greater(_117462, _117460)), -(less(_117462, _117460))], (178 ^ _104213) ^ [_110560, _110562] : [-(vmul(_110562, _110560) = vmul(_110560, _110562))], (472 ^ _104213) ^ [_121336, _121338] : [-(vplus(_121338, vsucc(_121336)) = vsucc(vplus(_121338, _121336)))], (476 ^ _104213) ^ [_121494] : [-(_121494 = v1), -(_121494 = vsucc(vskolem2(_121494)))], (276 ^ _104213) ^ [_114362, _114364, _114366] : [-(leq(_114366, _114362)), leq(_114364, _114362), leq(_114366, _114364)], (34 ^ _104213) ^ [_105433, _105435, _105437, _105439] : [-(less(_105437, _105433)), less(_105439, _105435), _105439 = _105437, _105435 = _105433], (202 ^ _104213) ^ [_111575, _111577, _111579, _111581] : [-(geq(vplus(_111581, _111577), vplus(_111579, _111575))), geq(_111577, _111575), geq(_111581, _111579)], (112 ^ _104213) ^ [_108011, _108013, _108015, _108017] : [-(greater(vmul(_108017, _108013), vmul(_108015, _108011))), 113 ^ _104213 : [(120 ^ _104213) ^ [] : [geq(_108013, _108011), greater(_108017, _108015)], (114 ^ _104213) ^ [] : [greater(_108013, _108011), geq(_108017, _108015)]]], (464 ^ _104213) ^ [_120907, _120909] : [-(vplus(_120907, _120909) = vplus(_120909, _120907))], (466 ^ _104213) ^ [_121007, _121009] : [-(vplus(vsucc(_121009), _121007) = vsucc(vplus(_121009, _121007)))], (342 ^ _104213) ^ [_116502, _116504] : [geq(_116502, _116504), -(greater(_116502, _116504)), -(_116502 = _116504)], (4 ^ _104213) ^ [_104444, _104446] : [_104446 = _104444, -(_104444 = _104446)], (186 ^ _104213) ^ [_110923, _110925] : [-(vmul(_110925, v1) = _110925)], (407 ^ _104213) ^ [_118657, _118659] : [408 ^ _104213 : [(409 ^ _104213) ^ [_118730] : [_118659 = vplus(_118657, _118730)]], -(less(_118657, _118659))], (180 ^ _104213) ^ [_110660, _110662] : [-(vmul(vsucc(_110662), _110660) = vplus(vmul(_110662, _110660), _110660))], (318 ^ _104213) ^ [_115696, _115698] : [geq(_115698, _115696), -(leq(_115696, _115698))], (156 ^ _104213) ^ [_109616, _109618, _109620] : [less(_109618, _109616), -(less(vmul(_109618, _109620), vmul(_109616, _109620)))], (108 ^ _104213) ^ [] : [-(geq(vd529, vd530))], (484 ^ _104213) ^ [_121788, _121790] : [-(_121790 = _121788), vsucc(_121790) = vsucc(_121788)], (188 ^ _104213) ^ [_111037, _111039] : [less(_111039, vplus(_111037, v1)), -(leq(_111039, _111037))], (228 ^ _104213) ^ [_112468, _112470, _112472, _112474] : [-(greater(vplus(_112474, _112470), vplus(_112472, _112468))), greater(_112470, _112468), greater(_112474, _112472)], (324 ^ _104213) ^ [_115935, _115937] : [leq(_115935, _115937), -(less(_115935, _115937)), -(_115935 = _115937)], (274 ^ _104213) ^ [_114236, _114238] : [-(greater(vplus(_114238, _114236), _114238))], (244 ^ _104213) ^ [_113055, _113057, _113059] : [vplus(_113059, _113055) = vplus(_113057, _113055), -(_113059 = _113057)], (10 ^ _104213) ^ [_104648, _104650, _104652] : [-(_104652 = _104648), _104652 = _104650, _104650 = _104648], (238 ^ _104213) ^ [_112813, _112815, _112817] : [less(vplus(_112817, _112813), vplus(_112815, _112813)), -(less(_112817, _112815))], (438 ^ _104213) ^ [_119827, _119829] : [_119829 = _119827, 441 ^ _104213 : [(442 ^ _104213) ^ [_119949] : [_119827 = vplus(_119829, _119949)]]], (468 ^ _104213) ^ [_121097] : [-(vplus(v1, _121097) = vsucc(_121097))], (168 ^ _104213) ^ [_110100, _110102, _110104] : [greater(_110102, _110100), -(greater(vmul(_110102, _110104), vmul(_110100, _110104)))]], input).
% 70.13/68.59 ncf('1',plain,[geq(vmul(vd526, vd529), vmul(vd527, vd530))],start(498 ^ 0)).
% 70.13/68.59 ncf('1.1',plain,[-(geq(vmul(vd526, vd529), vmul(vd527, vd530))), 354 : greater(vmul(vd526, vd529), vmul(vd527, vd530))],extension(352 ^ 1,bind([[_116754, _116756], [vmul(vd526, vd529), vmul(vd527, vd530)]]))).
% 70.13/68.59 ncf('1.1.1',plain,[-(greater(vmul(vd526, vd529), vmul(vd527, vd530))), 120 : geq(vd529, vd530), 120 : greater(vd526, vd527)],extension(112 ^ 4,bind([[_108011, _108013, _108015, _108017], [vd530, vd529, vd527, vd526]]))).
% 70.13/68.59 ncf('1.1.1.1',plain,[-(geq(vd529, vd530))],extension(108 ^ 7)).
% 70.13/68.59 ncf('1.1.1.2',plain,[-(greater(vd526, vd527)), -(vd526 = vd527), -(less(vd526, vd527))],extension(372 ^ 7,bind([[_117460, _117462], [vd527, vd526]]))).
% 70.13/68.59 ncf('1.1.1.2.1',plain,[vd526 = vd527, -(vmul(vd526, vd529) = vmul(vd527, vd530)), vd529 = vd530],extension(98 ^ 8,bind([[_107532, _107534, _107536, _107538], [vd530, vd529, vd527, vd526]]))).
% 70.13/68.59 ncf('1.1.1.2.1.1',plain,[vmul(vd526, vd529) = vmul(vd527, vd530)],extension(356 ^ 9)).
% 70.13/68.59 ncf('1.1.1.2.1.2',plain,[-(vd529 = vd530), geq(vd529, vd530), -(greater(vd529, vd530))],extension(342 ^ 9,bind([[_116502, _116504], [vd529, vd530]]))).
% 70.13/68.59 ncf('1.1.1.2.1.2.1',plain,[-(geq(vd529, vd530))],lemmata('[1, 1].x')).
% 70.13/68.59 ncf('1.1.1.2.1.2.2',plain,[greater(vd529, vd530), geq(vd526, vd527)],extension(114 ^ 10)).
% 70.13/68.59 ncf('1.1.1.2.1.2.2.1',plain,[-(geq(vd526, vd527))],extension(110 ^ 11)).
% 70.13/68.59 ncf('1.1.1.2.2',plain,[less(vd526, vd527), vd526 = vd527],extension(382 ^ 8,bind([[_117761, _117763], [vd527, vd526]]))).
% 70.13/68.59 ncf('1.1.1.2.2.1',plain,[-(vd526 = vd527), geq(vd526, vd527), -(greater(vd526, vd527))],extension(342 ^ 9,bind([[_116502, _116504], [vd526, vd527]]))).
% 70.13/68.59 ncf('1.1.1.2.2.1.1',plain,[-(geq(vd526, vd527))],extension(110 ^ 10)).
% 70.13/68.59 ncf('1.1.1.2.2.1.2',plain,[greater(vd526, vd527)],reduction('1.1.1')).
% 70.13/68.59 %-----------------------------------------------------
% 70.13/68.59 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------