%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM850+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:47 EDT 2023
% Result : Theorem 0.31s 1.38s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM850+1 : TPTP v8.1.2. Released v4.1.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n021.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 16:43:57 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.38
% 0.31/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.31/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 ncf(matrix, plain, [(434 ^ _81729) ^ [_97625] : [vd470 = vplus(vd471, _97625)], (76 ^ _81729) ^ [_84293, _84295, _84297, _84299] : [-(vmul(_84299, _84295) = vmul(_84297, _84293)), _84299 = _84297, _84295 = _84293], (86 ^ _81729) ^ [_84624, _84626] : [_84626 = _84624, -(vskolem2(_84626) = vskolem2(_84624))], (92 ^ _81729) ^ [_84842, _84844] : [_84844 = _84842, -(vsucc(_84844) = vsucc(_84842))], (98 ^ _81729) ^ [_85068, _85070, _85072, _85074] : [-(vplus(_85074, _85070) = vplus(_85072, _85068)), _85074 = _85072, _85070 = _85068], (2 ^ _81729) ^ [_81873] : [-(_81873 = _81873)], (4 ^ _81729) ^ [_81980, _81982] : [_81982 = _81980, -(_81980 = _81982)], (10 ^ _81729) ^ [_82184, _82186, _82188] : [-(_82188 = _82184), _82188 = _82186, _82186 = _82184], (20 ^ _81729) ^ [_82525, _82527, _82529, _82531] : [-(leq(_82529, _82525)), leq(_82531, _82527), _82531 = _82529, _82527 = _82525], (34 ^ _81729) ^ [_82969, _82971, _82973, _82975] : [-(geq(_82973, _82969)), geq(_82975, _82971), _82975 = _82973, _82971 = _82969], (48 ^ _81729) ^ [_83413, _83415, _83417, _83419] : [-(less(_83417, _83413)), less(_83419, _83415), _83419 = _83417, _83415 = _83413], (62 ^ _81729) ^ [_83837, _83839, _83841, _83843] : [-(greater(_83841, _83837)), greater(_83843, _83839), _83843 = _83841, _83839 = _83837], (108 ^ _81729) ^ [] : [-(greater(vd470, vd471))], (110 ^ _81729) ^ [_85465, _85467, _85469] : [-(vmul(vmul(_85469, _85467), _85465) = vmul(_85469, vmul(_85467, _85465)))], (112 ^ _81729) ^ [_85587, _85589, _85591] : [-(vmul(_85591, vplus(_85589, _85587)) = vplus(vmul(_85591, _85589), vmul(_85591, _85587)))], (114 ^ _81729) ^ [_85698, _85700] : [-(vmul(_85700, _85698) = vmul(_85698, _85700))], (116 ^ _81729) ^ [_85798, _85800] : [-(vmul(vsucc(_85800), _85798) = vplus(vmul(_85800, _85798), _85798))], (118 ^ _81729) ^ [_85889] : [-(vmul(v1, _85889) = _85889)], (120 ^ _81729) ^ [_86004, _86006] : [-(vmul(_86006, vsucc(_86004)) = vplus(vmul(_86006, _86004), _86006))], (122 ^ _81729) ^ [_86061, _86063] : [-(vmul(_86063, v1) = _86063)], (124 ^ _81729) ^ [_86175, _86177] : [less(_86177, vplus(_86175, v1)), -(leq(_86177, _86175))], (130 ^ _81729) ^ [_86391, _86393] : [greater(_86393, _86391), -(geq(_86393, vplus(_86391, v1)))], (136 ^ _81729) ^ [_86578] : [-(geq(_86578, v1))], (138 ^ _81729) ^ [_86713, _86715, _86717, _86719] : [-(geq(vplus(_86719, _86715), vplus(_86717, _86713))), geq(_86715, _86713), geq(_86719, _86717)], (148 ^ _81729) ^ [_87072, _87074, _87076, _87078] : [-(greater(vplus(_87078, _87074), vplus(_87076, _87072))), 149 ^ _81729 : [(150 ^ _81729) ^ [] : [greater(_87074, _87072), geq(_87078, _87076)], (156 ^ _81729) ^ [] : [geq(_87074, _87072), greater(_87078, _87076)]]], (164 ^ _81729) ^ [_87606, _87608, _87610, _87612] : [-(greater(vplus(_87612, _87608), vplus(_87610, _87606))), greater(_87608, _87606), greater(_87612, _87610)], (174 ^ _81729) ^ [_87951, _87953, _87955] : [less(vplus(_87955, _87951), vplus(_87953, _87951)), -(less(_87955, _87953))], (180 ^ _81729) ^ [_88193, _88195, _88197] : [vplus(_88197, _88193) = vplus(_88195, _88193), -(_88197 = _88195)], (186 ^ _81729) ^ [_88435, _88437, _88439] : [greater(vplus(_88439, _88435), vplus(_88437, _88435)), -(greater(_88439, _88437))], (192 ^ _81729) ^ [_88677, _88679, _88681] : [less(_88681, _88679), -(less(vplus(_88681, _88677), vplus(_88679, _88677)))], (198 ^ _81729) ^ [_88919, _88921, _88923] : [_88923 = _88921, -(vplus(_88923, _88919) = vplus(_88921, _88919))], (204 ^ _81729) ^ [_89161, _89163, _89165] : [greater(_89165, _89163), -(greater(vplus(_89165, _89161), vplus(_89163, _89161)))], (210 ^ _81729) ^ [_89374, _89376] : [-(greater(vplus(_89376, _89374), _89376))], (212 ^ _81729) ^ [_89500, _89502, _89504] : [-(leq(_89504, _89500)), leq(_89502, _89500), leq(_89504, _89502)], (222 ^ _81729) ^ [_89823, _89825, _89827] : [-(less(_89827, _89823)), 223 ^ _81729 : [(224 ^ _81729) ^ [] : [less(_89825, _89823), leq(_89827, _89825)], (230 ^ _81729) ^ [] : [leq(_89825, _89823), less(_89827, _89825)]]], (238 ^ _81729) ^ [_90315, _90317, _90319] : [-(less(_90319, _90315)), less(_90317, _90315), less(_90319, _90317)], (248 ^ _81729) ^ [_90624, _90626] : [leq(_90626, _90624), -(geq(_90624, _90626))], (254 ^ _81729) ^ [_90834, _90836] : [geq(_90836, _90834), -(leq(_90834, _90836))], (270 ^ _81729) ^ [_91325, _91327] : [271 ^ _81729 : [(272 ^ _81729) ^ [] : [less(_91325, _91327)], (274 ^ _81729) ^ [] : [_91325 = _91327]], -(leq(_91325, _91327))], (260 ^ _81729) ^ [_91073, _91075] : [leq(_91073, _91075), -(less(_91073, _91075)), -(_91073 = _91075)], (288 ^ _81729) ^ [_91892, _91894] : [289 ^ _81729 : [(290 ^ _81729) ^ [] : [greater(_91892, _91894)], (292 ^ _81729) ^ [] : [_91892 = _91894]], -(geq(_91892, _91894))], (278 ^ _81729) ^ [_91640, _91642] : [geq(_91640, _91642), -(greater(_91640, _91642)), -(_91640 = _91642)], (296 ^ _81729) ^ [_92178, _92180] : [less(_92180, _92178), -(greater(_92178, _92180))], (302 ^ _81729) ^ [_92388, _92390] : [greater(_92390, _92388), -(less(_92388, _92390))], (308 ^ _81729) ^ [_92598, _92600] : [-(_92600 = _92598), -(greater(_92600, _92598)), -(less(_92600, _92598))], (318 ^ _81729) ^ [_92899, _92901] : [_92901 = _92899, less(_92901, _92899)], (324 ^ _81729) ^ [_93112, _93114] : [greater(_93114, _93112), less(_93114, _93112)], (330 ^ _81729) ^ [_93325, _93327] : [_93327 = _93325, greater(_93327, _93325)], (336 ^ _81729) ^ [_93567, _93569] : [less(_93567, _93569), -(_93569 = vplus(_93567, 339 ^ [_93567, _93569]))], (343 ^ _81729) ^ [_93795, _93797] : [344 ^ _81729 : [(345 ^ _81729) ^ [_93868] : [_93797 = vplus(_93795, _93868)]], -(less(_93795, _93797))], (349 ^ _81729) ^ [_94064, _94066] : [greater(_94064, _94066), -(_94064 = vplus(_94066, 352 ^ [_94064, _94066]))], (356 ^ _81729) ^ [_94292, _94294] : [357 ^ _81729 : [(358 ^ _81729) ^ [_94365] : [_94292 = vplus(_94294, _94365)]], -(greater(_94292, _94294))], (362 ^ _81729) ^ [_94532, _94534] : [-(_94534 = _94532), -(_94534 = vplus(_94532, 367 ^ [_94532, _94534])), -(_94532 = vplus(_94534, 370 ^ [_94532, _94534]))], (374 ^ _81729) ^ [_94965, _94967] : [_94967 = _94965, 377 ^ _81729 : [(378 ^ _81729) ^ [_95087] : [_94965 = vplus(_94967, _95087)]]], (380 ^ _81729) ^ [_95206, _95208] : [381 ^ _81729 : [(382 ^ _81729) ^ [_95291] : [_95208 = vplus(_95206, _95291)]], 383 ^ _81729 : [(384 ^ _81729) ^ [_95355] : [_95206 = vplus(_95208, _95355)]]], (386 ^ _81729) ^ [_95475, _95477] : [_95477 = _95475, 389 ^ _81729 : [(390 ^ _81729) ^ [_95597] : [_95477 = vplus(_95475, _95597)]]], (392 ^ _81729) ^ [_95716, _95718] : [-(_95718 = _95716), 395 ^ _81729 : [(396 ^ _81729) ^ [_95842] : [vplus(_95842, _95718) = vplus(_95842, _95716)]]], (398 ^ _81729) ^ [_95948, _95950] : [_95948 = vplus(_95950, _95948)], (400 ^ _81729) ^ [_96045, _96047] : [-(vplus(_96045, _96047) = vplus(_96047, _96045))], (402 ^ _81729) ^ [_96145, _96147] : [-(vplus(vsucc(_96147), _96145) = vsucc(vplus(_96147, _96145)))], (404 ^ _81729) ^ [_96235] : [-(vplus(v1, _96235) = vsucc(_96235))], (406 ^ _81729) ^ [_96346, _96348, _96350] : [-(vplus(vplus(_96350, _96348), _96346) = vplus(_96350, vplus(_96348, _96346)))], (408 ^ _81729) ^ [_96474, _96476] : [-(vplus(_96476, vsucc(_96474)) = vsucc(vplus(_96476, _96474)))], (410 ^ _81729) ^ [_96530, _96532] : [-(vplus(_96532, v1) = vsucc(_96532))], (412 ^ _81729) ^ [_96632] : [-(_96632 = v1), -(_96632 = vsucc(vskolem2(_96632)))], (418 ^ _81729) ^ [_96817] : [vsucc(_96817) = _96817], (420 ^ _81729) ^ [_96926, _96928] : [-(_96928 = _96926), vsucc(_96928) = vsucc(_96926)], (432 ^ _81729) ^ [_97316] : [vsucc(_97316) = v1], (426 ^ _81729) ^ [_97148, _97150] : [vsucc(_97150) = vsucc(_97148), -(_97150 = _97148)]], input).
% 0.31/1.38 ncf('1',plain,[vd470 = vplus(vd471, 352 ^ [vd470, vd471])],start(434 ^ 0,bind([[_97625], [352 ^ [vd470, vd471]]]))).
% 0.31/1.38 ncf('1.1',plain,[-(vd470 = vplus(vd471, 352 ^ [vd470, vd471])), greater(vd470, vd471)],extension(349 ^ 1,bind([[_94064, _94066], [vd470, vd471]]))).
% 0.31/1.38 ncf('1.1.1',plain,[-(greater(vd470, vd471))],extension(108 ^ 2)).
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------