%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM844+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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:45 EDT 2023
% Result : Theorem 0.30s 1.37s
% Output : Proof 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM844+1 : TPTP v8.1.2. Released v4.1.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n005.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 17:15:08 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.30/1.37
% 0.30/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.30/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/1.37 %-----------------------------------------------------
% 0.30/1.37 ncf(matrix, plain, [(438 ^ _82303) ^ [] : [vplus(vmul(vd411, vd413), vplus(vd413, vsucc(vd411))) = vplus(vmul(vd411, vd413), vplus(vsucc(vd411), vd413))], (76 ^ _82303) ^ [_84839, _84841] : [_84841 = _84839, -(vskolem2(_84841) = vskolem2(_84839))], (82 ^ _82303) ^ [_85085, _85087, _85089, _85091] : [-(vmul(_85091, _85087) = vmul(_85089, _85085)), _85091 = _85089, _85087 = _85085], (102 ^ _82303) ^ [_85755, _85757] : [_85757 = _85755, -(vsucc(_85757) = vsucc(_85755))], (92 ^ _82303) ^ [_85444, _85446, _85448, _85450] : [-(vplus(_85450, _85446) = vplus(_85448, _85444)), _85450 = _85448, _85446 = _85444], (2 ^ _82303) ^ [_82447] : [-(_82447 = _82447)], (4 ^ _82303) ^ [_82554, _82556] : [_82556 = _82554, -(_82554 = _82556)], (10 ^ _82303) ^ [_82758, _82760, _82762] : [-(_82762 = _82758), _82762 = _82760, _82760 = _82758], (20 ^ _82303) ^ [_83099, _83101, _83103, _83105] : [-(leq(_83103, _83099)), leq(_83105, _83101), _83105 = _83103, _83101 = _83099], (34 ^ _82303) ^ [_83543, _83545, _83547, _83549] : [-(geq(_83547, _83543)), geq(_83549, _83545), _83549 = _83547, _83545 = _83543], (48 ^ _82303) ^ [_83987, _83989, _83991, _83993] : [-(less(_83991, _83987)), less(_83993, _83989), _83993 = _83991, _83989 = _83987], (62 ^ _82303) ^ [_84411, _84413, _84415, _84417] : [-(greater(_84415, _84411)), greater(_84417, _84413), _84417 = _84415, _84413 = _84411], (108 ^ _82303) ^ [] : [-(vplus(vplus(vmul(vd411, vd413), vd413), vsucc(vd411)) = vplus(vmul(vd411, vd413), vplus(vd413, vsucc(vd411))))], (110 ^ _82303) ^ [] : [-(vplus(vmul(vsucc(vd411), vd413), vsucc(vd411)) = vplus(vplus(vmul(vd411, vd413), vd413), vsucc(vd411)))], (112 ^ _82303) ^ [] : [-(vmul(vsucc(vd411), vsucc(vd413)) = vplus(vmul(vsucc(vd411), vd413), vsucc(vd411)))], (114 ^ _82303) ^ [] : [-(vmul(vsucc(vd411), vd413) = vplus(vmul(vd411, vd413), vd413))], (116 ^ _82303) ^ [] : [-(vsucc(vmul(vd411, v1)) = vplus(vmul(vd411, v1), v1))], (118 ^ _82303) ^ [] : [-(vsucc(vd411) = vsucc(vmul(vd411, v1)))], (120 ^ _82303) ^ [] : [-(vmul(vsucc(vd411), v1) = vsucc(vd411))], (122 ^ _82303) ^ [_86329] : [-(vmul(v1, _86329) = _86329)], (124 ^ _82303) ^ [_86444, _86446] : [-(vmul(_86446, vsucc(_86444)) = vplus(vmul(_86446, _86444), _86446))], (126 ^ _82303) ^ [_86501, _86503] : [-(vmul(_86503, v1) = _86503)], (128 ^ _82303) ^ [_86615, _86617] : [less(_86617, vplus(_86615, v1)), -(leq(_86617, _86615))], (134 ^ _82303) ^ [_86831, _86833] : [greater(_86833, _86831), -(geq(_86833, vplus(_86831, v1)))], (140 ^ _82303) ^ [_87018] : [-(geq(_87018, v1))], (142 ^ _82303) ^ [_87153, _87155, _87157, _87159] : [-(geq(vplus(_87159, _87155), vplus(_87157, _87153))), geq(_87155, _87153), geq(_87159, _87157)], (152 ^ _82303) ^ [_87512, _87514, _87516, _87518] : [-(greater(vplus(_87518, _87514), vplus(_87516, _87512))), 153 ^ _82303 : [(154 ^ _82303) ^ [] : [greater(_87514, _87512), geq(_87518, _87516)], (160 ^ _82303) ^ [] : [geq(_87514, _87512), greater(_87518, _87516)]]], (168 ^ _82303) ^ [_88046, _88048, _88050, _88052] : [-(greater(vplus(_88052, _88048), vplus(_88050, _88046))), greater(_88048, _88046), greater(_88052, _88050)], (178 ^ _82303) ^ [_88391, _88393, _88395] : [less(vplus(_88395, _88391), vplus(_88393, _88391)), -(less(_88395, _88393))], (184 ^ _82303) ^ [_88633, _88635, _88637] : [vplus(_88637, _88633) = vplus(_88635, _88633), -(_88637 = _88635)], (190 ^ _82303) ^ [_88875, _88877, _88879] : [greater(vplus(_88879, _88875), vplus(_88877, _88875)), -(greater(_88879, _88877))], (196 ^ _82303) ^ [_89117, _89119, _89121] : [less(_89121, _89119), -(less(vplus(_89121, _89117), vplus(_89119, _89117)))], (202 ^ _82303) ^ [_89359, _89361, _89363] : [_89363 = _89361, -(vplus(_89363, _89359) = vplus(_89361, _89359))], (208 ^ _82303) ^ [_89601, _89603, _89605] : [greater(_89605, _89603), -(greater(vplus(_89605, _89601), vplus(_89603, _89601)))], (214 ^ _82303) ^ [_89814, _89816] : [-(greater(vplus(_89816, _89814), _89816))], (216 ^ _82303) ^ [_89940, _89942, _89944] : [-(leq(_89944, _89940)), leq(_89942, _89940), leq(_89944, _89942)], (226 ^ _82303) ^ [_90263, _90265, _90267] : [-(less(_90267, _90263)), 227 ^ _82303 : [(228 ^ _82303) ^ [] : [less(_90265, _90263), leq(_90267, _90265)], (234 ^ _82303) ^ [] : [leq(_90265, _90263), less(_90267, _90265)]]], (242 ^ _82303) ^ [_90755, _90757, _90759] : [-(less(_90759, _90755)), less(_90757, _90755), less(_90759, _90757)], (252 ^ _82303) ^ [_91064, _91066] : [leq(_91066, _91064), -(geq(_91064, _91066))], (258 ^ _82303) ^ [_91274, _91276] : [geq(_91276, _91274), -(leq(_91274, _91276))], (274 ^ _82303) ^ [_91765, _91767] : [275 ^ _82303 : [(276 ^ _82303) ^ [] : [less(_91765, _91767)], (278 ^ _82303) ^ [] : [_91765 = _91767]], -(leq(_91765, _91767))], (264 ^ _82303) ^ [_91513, _91515] : [leq(_91513, _91515), -(less(_91513, _91515)), -(_91513 = _91515)], (292 ^ _82303) ^ [_92332, _92334] : [293 ^ _82303 : [(294 ^ _82303) ^ [] : [greater(_92332, _92334)], (296 ^ _82303) ^ [] : [_92332 = _92334]], -(geq(_92332, _92334))], (282 ^ _82303) ^ [_92080, _92082] : [geq(_92080, _92082), -(greater(_92080, _92082)), -(_92080 = _92082)], (300 ^ _82303) ^ [_92618, _92620] : [less(_92620, _92618), -(greater(_92618, _92620))], (306 ^ _82303) ^ [_92828, _92830] : [greater(_92830, _92828), -(less(_92828, _92830))], (312 ^ _82303) ^ [_93038, _93040] : [-(_93040 = _93038), -(greater(_93040, _93038)), -(less(_93040, _93038))], (322 ^ _82303) ^ [_93339, _93341] : [_93341 = _93339, less(_93341, _93339)], (328 ^ _82303) ^ [_93552, _93554] : [greater(_93554, _93552), less(_93554, _93552)], (334 ^ _82303) ^ [_93765, _93767] : [_93767 = _93765, greater(_93767, _93765)], (340 ^ _82303) ^ [_94007, _94009] : [less(_94007, _94009), -(_94009 = vplus(_94007, 343 ^ [_94007, _94009]))], (347 ^ _82303) ^ [_94235, _94237] : [348 ^ _82303 : [(349 ^ _82303) ^ [_94308] : [_94237 = vplus(_94235, _94308)]], -(less(_94235, _94237))], (353 ^ _82303) ^ [_94504, _94506] : [greater(_94504, _94506), -(_94504 = vplus(_94506, 356 ^ [_94504, _94506]))], (360 ^ _82303) ^ [_94732, _94734] : [361 ^ _82303 : [(362 ^ _82303) ^ [_94805] : [_94732 = vplus(_94734, _94805)]], -(greater(_94732, _94734))], (366 ^ _82303) ^ [_94972, _94974] : [-(_94974 = _94972), -(_94974 = vplus(_94972, 371 ^ [_94972, _94974])), -(_94972 = vplus(_94974, 374 ^ [_94972, _94974]))], (378 ^ _82303) ^ [_95405, _95407] : [_95407 = _95405, 381 ^ _82303 : [(382 ^ _82303) ^ [_95527] : [_95405 = vplus(_95407, _95527)]]], (384 ^ _82303) ^ [_95646, _95648] : [385 ^ _82303 : [(386 ^ _82303) ^ [_95731] : [_95648 = vplus(_95646, _95731)]], 387 ^ _82303 : [(388 ^ _82303) ^ [_95795] : [_95646 = vplus(_95648, _95795)]]], (390 ^ _82303) ^ [_95915, _95917] : [_95917 = _95915, 393 ^ _82303 : [(394 ^ _82303) ^ [_96037] : [_95917 = vplus(_95915, _96037)]]], (396 ^ _82303) ^ [_96156, _96158] : [-(_96158 = _96156), 399 ^ _82303 : [(400 ^ _82303) ^ [_96282] : [vplus(_96282, _96158) = vplus(_96282, _96156)]]], (402 ^ _82303) ^ [_96388, _96390] : [_96388 = vplus(_96390, _96388)], (404 ^ _82303) ^ [_96485, _96487] : [-(vplus(_96485, _96487) = vplus(_96487, _96485))], (406 ^ _82303) ^ [_96585, _96587] : [-(vplus(vsucc(_96587), _96585) = vsucc(vplus(_96587, _96585)))], (408 ^ _82303) ^ [_96675] : [-(vplus(v1, _96675) = vsucc(_96675))], (410 ^ _82303) ^ [_96786, _96788, _96790] : [-(vplus(vplus(_96790, _96788), _96786) = vplus(_96790, vplus(_96788, _96786)))], (412 ^ _82303) ^ [_96914, _96916] : [-(vplus(_96916, vsucc(_96914)) = vsucc(vplus(_96916, _96914)))], (414 ^ _82303) ^ [_96970, _96972] : [-(vplus(_96972, v1) = vsucc(_96972))], (416 ^ _82303) ^ [_97072] : [-(_97072 = v1), -(_97072 = vsucc(vskolem2(_97072)))], (422 ^ _82303) ^ [_97257] : [vsucc(_97257) = _97257], (424 ^ _82303) ^ [_97366, _97368] : [-(_97368 = _97366), vsucc(_97368) = vsucc(_97366)], (436 ^ _82303) ^ [_97756] : [vsucc(_97756) = v1], (430 ^ _82303) ^ [_97588, _97590] : [vsucc(_97590) = vsucc(_97588), -(_97590 = _97588)]], input).
% 0.30/1.37 ncf('1',plain,[vplus(vmul(vd411, vd413), vplus(vd413, vsucc(vd411))) = vplus(vmul(vd411, vd413), vplus(vsucc(vd411), vd413))],start(438 ^ 0)).
% 0.30/1.37 ncf('1.1',plain,[-(vplus(vmul(vd411, vd413), vplus(vd413, vsucc(vd411))) = vplus(vmul(vd411, vd413), vplus(vsucc(vd411), vd413))), vmul(vd411, vd413) = vmul(vd411, vd413), vplus(vd413, vsucc(vd411)) = vplus(vsucc(vd411), vd413)],extension(92 ^ 1,bind([[_85444, _85446, _85448, _85450], [vplus(vsucc(vd411), vd413), vplus(vd413, vsucc(vd411)), vmul(vd411, vd413), vmul(vd411, vd413)]]))).
% 0.30/1.37 ncf('1.1.1',plain,[-(vmul(vd411, vd413) = vmul(vd411, vd413))],extension(2 ^ 2,bind([[_82447], [vmul(vd411, vd413)]]))).
% 0.30/1.37 ncf('1.1.2',plain,[-(vplus(vd413, vsucc(vd411)) = vplus(vsucc(vd411), vd413))],extension(404 ^ 2,bind([[_96485, _96487], [vd413, vsucc(vd411)]]))).
% 0.30/1.37 %-----------------------------------------------------
% 0.30/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------