%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM848+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:46 EDT 2023
% Result : Theorem 0.31s 1.37s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUM848+2 : TPTP v8.1.2. Released v4.1.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n007.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:59:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.37
% 0.31/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.31/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 ncf(matrix, plain, [(122 ^ _29806) ^ [] : [vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436)) = vplus(vmul(vd436, vd437), vmul(vd436, vsucc(vd439)))], (80 ^ _29806) ^ [] : [-(vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436) = vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436)))], (82 ^ _29806) ^ [] : [-(vplus(vmul(vd436, vplus(vd437, vd439)), vd436) = vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436))], (84 ^ _29806) ^ [] : [-(vmul(vd436, vsucc(vplus(vd437, vd439))) = vplus(vmul(vd436, vplus(vd437, vd439)), vd436))], (86 ^ _29806) ^ [] : [-(vmul(vd436, vplus(vd437, vsucc(vd439))) = vmul(vd436, vsucc(vplus(vd437, vd439))))], (88 ^ _29806) ^ [] : [-(vmul(vd436, vplus(vd437, vd439)) = vplus(vmul(vd436, vd437), vmul(vd436, vd439)))], (90 ^ _29806) ^ [] : [-(vplus(vmul(vd436, vd437), vd436) = vplus(vmul(vd436, vd437), vmul(vd436, v1)))], (92 ^ _29806) ^ [] : [-(vmul(vd436, vsucc(vd437)) = vplus(vmul(vd436, vd437), vd436))], (94 ^ _29806) ^ [_32974, _32976] : [-(vmul(_32976, vsucc(_32974)) = vplus(vmul(_32976, _32974), _32976))], (96 ^ _29806) ^ [_33031, _33033] : [-(vmul(_33033, v1) = _33033)], (98 ^ _29806) ^ [_33145, _33147] : [less(_33147, vplus(_33145, v1)), -(leq(_33147, _33145))], (104 ^ _29806) ^ [_33346, _33348] : [-(vplus(_33346, _33348) = vplus(_33348, _33346))], (106 ^ _29806) ^ [_33446, _33448] : [-(vplus(vsucc(_33448), _33446) = vsucc(vplus(_33448, _33446)))], (108 ^ _29806) ^ [_33536] : [-(vplus(v1, _33536) = vsucc(_33536))], (110 ^ _29806) ^ [_33647, _33649, _33651] : [-(vplus(vplus(_33651, _33649), _33647) = vplus(_33651, vplus(_33649, _33647)))], (112 ^ _29806) ^ [_33775, _33777] : [-(vplus(_33777, vsucc(_33775)) = vsucc(vplus(_33777, _33775)))], (114 ^ _29806) ^ [_33831, _33833] : [-(vplus(_33833, v1) = vsucc(_33833))], (116 ^ _29806) ^ [_33913] : [-(_33913 = v1), -(_33913 = vsucc(vskolem2(_33913)))], (48 ^ _29806) ^ [_31450, _31452] : [_31452 = _31450, -(vskolem2(_31452) = vskolem2(_31450))], (54 ^ _29806) ^ [_31696, _31698, _31700, _31702] : [-(vplus(_31702, _31698) = vplus(_31700, _31696)), _31702 = _31700, _31698 = _31696], (74 ^ _29806) ^ [_32366, _32368] : [_32368 = _32366, -(vsucc(_32368) = vsucc(_32366))], (64 ^ _29806) ^ [_32055, _32057, _32059, _32061] : [-(vmul(_32061, _32057) = vmul(_32059, _32055)), _32061 = _32059, _32057 = _32055], (2 ^ _29806) ^ [_29950] : [-(_29950 = _29950)], (4 ^ _29806) ^ [_30057, _30059] : [_30059 = _30057, -(_30057 = _30059)], (10 ^ _29806) ^ [_30261, _30263, _30265] : [-(_30265 = _30261), _30265 = _30263, _30263 = _30261], (20 ^ _29806) ^ [_30602, _30604, _30606, _30608] : [-(less(_30606, _30602)), less(_30608, _30604), _30608 = _30606, _30604 = _30602], (34 ^ _29806) ^ [_31026, _31028, _31030, _31032] : [-(leq(_31030, _31026)), leq(_31032, _31028), _31032 = _31030, _31028 = _31026]], input).
% 0.31/1.37 ncf('1',plain,[vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436)) = vplus(vmul(vd436, vd437), vmul(vd436, vsucc(vd439)))],start(122 ^ 0)).
% 0.31/1.37 ncf('1.1',plain,[-(vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436)) = vplus(vmul(vd436, vd437), vmul(vd436, vsucc(vd439)))), vmul(vd436, vd437) = vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436) = vmul(vd436, vsucc(vd439))],extension(54 ^ 1,bind([[_31696, _31698, _31700, _31702], [vmul(vd436, vsucc(vd439)), vplus(vmul(vd436, vd439), vd436), vmul(vd436, vd437), vmul(vd436, vd437)]]))).
% 0.31/1.37 ncf('1.1.1',plain,[-(vmul(vd436, vd437) = vmul(vd436, vd437)), vd436 = vd436, vd437 = vd437],extension(64 ^ 2,bind([[_32055, _32057, _32059, _32061], [vd437, vd437, vd436, vd436]]))).
% 0.31/1.37 ncf('1.1.1.1',plain,[-(vd436 = vd436)],extension(2 ^ 3,bind([[_29950], [vd436]]))).
% 0.31/1.37 ncf('1.1.1.2',plain,[-(vd437 = vd437)],extension(2 ^ 3,bind([[_29950], [vd437]]))).
% 0.31/1.37 ncf('1.1.2',plain,[-(vplus(vmul(vd436, vd439), vd436) = vmul(vd436, vsucc(vd439))), vmul(vd436, vsucc(vd439)) = vplus(vmul(vd436, vd439), vd436)],extension(4 ^ 2,bind([[_30057, _30059], [vplus(vmul(vd436, vd439), vd436), vmul(vd436, vsucc(vd439))]]))).
% 0.31/1.37 ncf('1.1.2.1',plain,[-(vmul(vd436, vsucc(vd439)) = vplus(vmul(vd436, vd439), vd436))],extension(94 ^ 3,bind([[_32974, _32976], [vd439, vd436]]))).
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------