%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM425+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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:44:35 EDT 2023
% Result : Theorem 0.99s 1.37s
% Output : Proof 0.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM425+3 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n009.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:27:47 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.99/1.37
% 0.99/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.99/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.99/1.37 %-----------------------------------------------------
% 0.99/1.37 ncf(matrix, plain, [(344 ^ _52581) ^ [_63579] : [aInteger0(_63579), sdtasdt0(xq, _63579) = sdtpldt0(xa, smndt0(xb))], (62 ^ _52581) ^ [_54715, _54717, _54719, _54721] : [-(sdtasdt0(_54721, _54717) = sdtasdt0(_54719, _54715)), _54721 = _54719, _54717 = _54715], (82 ^ _52581) ^ [_55385, _55387] : [_55387 = _55385, -(smndt0(_55387) = smndt0(_55385))], (72 ^ _52581) ^ [_55074, _55076, _55078, _55080] : [-(sdtpldt0(_55080, _55076) = sdtpldt0(_55078, _55074)), _55080 = _55078, _55076 = _55074], (2 ^ _52581) ^ [_52725] : [-(_52725 = _52725)], (4 ^ _52581) ^ [_52832, _52834] : [_52834 = _52832, -(_52832 = _52834)], (10 ^ _52581) ^ [_53036, _53038, _53040] : [-(_53040 = _53036), _53040 = _53038, _53038 = _53036], (20 ^ _52581) ^ [_53377, _53379, _53381, _53383] : [-(aDivisorOf0(_53381, _53377)), aDivisorOf0(_53383, _53379), _53383 = _53381, _53379 = _53377], (52 ^ _52581) ^ [_54382, _54384] : [-(aInteger0(_54382)), _54384 = _54382, aInteger0(_54384)], (34 ^ _52581) ^ [_53849, _53851, _53853, _53855, _53857, _53859] : [-(sdteqdtlpzmzozddtrp0(_53857, _53853, _53849)), sdteqdtlpzmzozddtrp0(_53859, _53855, _53851), _53859 = _53857, _53855 = _53853, _53851 = _53849], (88 ^ _52581) ^ [_55599] : [aInteger0(_55599), true___, -(true___)], (98 ^ _52581) ^ [] : [-(aInteger0(sz00))], (100 ^ _52581) ^ [] : [-(aInteger0(sz10))], (102 ^ _52581) ^ [_55960] : [aInteger0(_55960), -(aInteger0(smndt0(_55960)))], (108 ^ _52581) ^ [_56164, _56166] : [-(aInteger0(sdtpldt0(_56166, _56164))), aInteger0(_56166), aInteger0(_56164)], (118 ^ _52581) ^ [_56463, _56465] : [-(aInteger0(sdtasdt0(_56465, _56463))), aInteger0(_56465), aInteger0(_56463)], (128 ^ _52581) ^ [_56776, _56778, _56780] : [-(sdtpldt0(_56780, sdtpldt0(_56778, _56776)) = sdtpldt0(sdtpldt0(_56780, _56778), _56776)), aInteger0(_56780), aInteger0(_56778), aInteger0(_56776)], (142 ^ _52581) ^ [_57196, _57198] : [-(sdtpldt0(_57198, _57196) = sdtpldt0(_57196, _57198)), aInteger0(_57198), aInteger0(_57196)], (152 ^ _52581) ^ [_57489] : [aInteger0(_57489), 155 ^ _52581 : [(156 ^ _52581) ^ [] : [-(sdtpldt0(_57489, sz00) = _57489)], (158 ^ _52581) ^ [] : [-(_57489 = sdtpldt0(sz00, _57489))]]], (160 ^ _52581) ^ [_57762] : [aInteger0(_57762), 163 ^ _52581 : [(164 ^ _52581) ^ [] : [-(sdtpldt0(_57762, smndt0(_57762)) = sz00)], (166 ^ _52581) ^ [] : [-(sz00 = sdtpldt0(smndt0(_57762), _57762))]]], (168 ^ _52581) ^ [_58071, _58073, _58075] : [-(sdtasdt0(_58075, sdtasdt0(_58073, _58071)) = sdtasdt0(sdtasdt0(_58075, _58073), _58071)), aInteger0(_58075), aInteger0(_58073), aInteger0(_58071)], (182 ^ _52581) ^ [_58491, _58493] : [-(sdtasdt0(_58493, _58491) = sdtasdt0(_58491, _58493)), aInteger0(_58493), aInteger0(_58491)], (192 ^ _52581) ^ [_58784] : [aInteger0(_58784), 195 ^ _52581 : [(196 ^ _52581) ^ [] : [-(sdtasdt0(_58784, sz10) = _58784)], (198 ^ _52581) ^ [] : [-(_58784 = sdtasdt0(sz10, _58784))]]], (200 ^ _52581) ^ [_59085, _59087, _59089] : [211 ^ _52581 : [(212 ^ _52581) ^ [] : [-(sdtasdt0(_59089, sdtpldt0(_59087, _59085)) = sdtpldt0(sdtasdt0(_59089, _59087), sdtasdt0(_59089, _59085)))], (214 ^ _52581) ^ [] : [-(sdtasdt0(sdtpldt0(_59089, _59087), _59085) = sdtpldt0(sdtasdt0(_59089, _59085), sdtasdt0(_59087, _59085)))]], aInteger0(_59089), aInteger0(_59087), aInteger0(_59085)], (216 ^ _52581) ^ [_59604] : [aInteger0(_59604), 219 ^ _52581 : [(220 ^ _52581) ^ [] : [-(sdtasdt0(_59604, sz00) = sz00)], (222 ^ _52581) ^ [] : [-(sz00 = sdtasdt0(sz00, _59604))]]], (224 ^ _52581) ^ [_59877] : [aInteger0(_59877), 227 ^ _52581 : [(228 ^ _52581) ^ [] : [-(sdtasdt0(smndt0(sz10), _59877) = smndt0(_59877))], (230 ^ _52581) ^ [] : [-(smndt0(_59877) = sdtasdt0(_59877, smndt0(sz10)))]]], (232 ^ _52581) ^ [_60172, _60174] : [aInteger0(_60174), aInteger0(_60172), sdtasdt0(_60174, _60172) = sz00, -(_60174 = sz00), -(_60172 = sz00)], (250 ^ _52581) ^ [_60640] : [aInteger0(_60640), 253 ^ _52581 : [(254 ^ _52581) ^ [_60826] : [aDivisorOf0(_60826, _60640), 257 ^ _52581 : [(258 ^ _52581) ^ [] : [-(aInteger0(_60826))], (260 ^ _52581) ^ [] : [_60826 = sz00], (263 ^ _52581) ^ [] : [-(aInteger0(261 ^ [_60640, _60826]))], (265 ^ _52581) ^ [] : [-(sdtasdt0(_60826, 261 ^ [_60640, _60826]) = _60640)]]], (267 ^ _52581) ^ [_61288] : [-(aDivisorOf0(_61288, _60640)), aInteger0(_61288), -(_61288 = sz00), 276 ^ _52581 : [(277 ^ _52581) ^ [_61555] : [aInteger0(_61555), sdtasdt0(_61288, _61555) = _60640]]]]], (327 ^ _52581) ^ [] : [-(aInteger0(xa))], (329 ^ _52581) ^ [] : [-(aInteger0(xb))], (331 ^ _52581) ^ [] : [-(aInteger0(xq))], (333 ^ _52581) ^ [] : [xq = sz00], (336 ^ _52581) ^ [] : [-(aInteger0(334 ^ []))], (338 ^ _52581) ^ [] : [-(sdtasdt0(xq, 334 ^ []) = sdtpldt0(xa, smndt0(xb)))], (340 ^ _52581) ^ [] : [-(aDivisorOf0(xq, sdtpldt0(xa, smndt0(xb))))], (342 ^ _52581) ^ [] : [-(sdteqdtlpzmzozddtrp0(xa, xb, xq))], (313 ^ _52581) ^ [_62634, _62636] : [-(sdteqdtlpzmzozddtrp0(_62636, _62636, _62634)), aInteger0(_62636), aInteger0(_62634), -(_62634 = sz00)], (285 ^ _52581) ^ [_61858, _61860, _61862] : [aInteger0(_61862), aInteger0(_61860), aInteger0(_61858), -(_61858 = sz00), 300 ^ _52581 : [(301 ^ _52581) ^ [] : [sdteqdtlpzmzozddtrp0(_61862, _61860, _61858), -(aDivisorOf0(_61858, sdtpldt0(_61862, smndt0(_61860))))], (307 ^ _52581) ^ [] : [aDivisorOf0(_61858, sdtpldt0(_61862, smndt0(_61860))), -(sdteqdtlpzmzozddtrp0(_61862, _61860, _61858))]]]], input).
% 0.99/1.37 ncf('1',plain,[aInteger0(sz00), 254 : aDivisorOf0(sz00, sz00), 260 : sz00 = sz00],start(250 ^ 0,bind([[_60640, _60826], [sz00, sz00]]))).
% 0.99/1.37 ncf('1.1',plain,[-(aInteger0(sz00))],extension(98 ^ 1)).
% 0.99/1.37 ncf('1.2',plain,[-(aDivisorOf0(sz00, sz00)), aInteger0(sz00), -(sz00 = sz00), 277 : aInteger0(sz00), 277 : sdtasdt0(sz00, sz00) = sz00],extension(267 ^ 3,bind([[_61288, _61555], [sz00, sz00]]))).
% 0.99/1.37 ncf('1.2.1',plain,[-(aInteger0(sz00))],extension(98 ^ 4)).
% 0.99/1.37 ncf('1.2.2',plain,[sz00 = sz00, -(aInteger0(sz00)), aInteger0(sz00)],extension(52 ^ 4,bind([[_54382, _54384], [sz00, sz00]]))).
% 0.99/1.37 ncf('1.2.2.1',plain,[aInteger0(sz00), -(aInteger0(sdtpldt0(334 ^ [], sz00))), aInteger0(334 ^ [])],extension(108 ^ 5,bind([[_56164, _56166], [sz00, 334 ^ []]]))).
% 0.99/1.37 ncf('1.2.2.1.1',plain,[aInteger0(sdtpldt0(334 ^ [], sz00)), -(aInteger0(334 ^ [])), sdtpldt0(334 ^ [], sz00) = 334 ^ []],extension(52 ^ 6,bind([[_54382, _54384], [334 ^ [], sdtpldt0(334 ^ [], sz00)]]))).
% 0.99/1.37 ncf('1.2.2.1.1.1',plain,[aInteger0(334 ^ []), sdtasdt0(xq, 334 ^ []) = sdtpldt0(xa, smndt0(xb))],extension(344 ^ 7,bind([[_63579], [334 ^ []]]))).
% 0.99/1.37 ncf('1.2.2.1.1.1.1',plain,[-(sdtasdt0(xq, 334 ^ []) = sdtpldt0(xa, smndt0(xb)))],extension(338 ^ 8)).
% 0.99/1.37 ncf('1.2.2.1.1.2',plain,[-(sdtpldt0(334 ^ [], sz00) = 334 ^ []), aInteger0(334 ^ [])],extension(152 ^ 7,bind([[_57489], [334 ^ []]]))).
% 0.99/1.37 ncf('1.2.2.1.1.2.1',plain,[-(aInteger0(334 ^ []))],extension(336 ^ 8)).
% 0.99/1.37 ncf('1.2.2.1.2',plain,[-(aInteger0(334 ^ []))],extension(336 ^ 6)).
% 0.99/1.37 ncf('1.2.2.2',plain,[-(aInteger0(sz00))],lemmata('[1].x')).
% 0.99/1.37 ncf('1.2.3',plain,[-(aInteger0(sz00))],extension(98 ^ 6)).
% 0.99/1.37 ncf('1.2.4',plain,[-(sdtasdt0(sz00, sz00) = sz00), sz00 = sdtasdt0(sz00, sz00)],extension(4 ^ 6,bind([[_52832, _52834], [sdtasdt0(sz00, sz00), sz00]]))).
% 0.99/1.37 ncf('1.2.4.1',plain,[-(sz00 = sdtasdt0(sz00, sz00)), aInteger0(sz00)],extension(216 ^ 7,bind([[_59604], [sz00]]))).
% 0.99/1.37 ncf('1.2.4.1.1',plain,[-(aInteger0(sz00))],lemmata('[1].x')).
% 0.99/1.37 ncf('1.3',plain,[-(sz00 = sz00)],extension(2 ^ 5,bind([[_52725], [sz00]]))).
% 0.99/1.37 %-----------------------------------------------------
% 0.99/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------