%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM847+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM847+2 : TPTP v8.1.2. Released v4.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n003.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:54:00 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(160 ^ _34185) ^ [] : [vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436) = vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436))], (108 ^ _34185) ^ [] : [-(vplus(vmul(vd436, vplus(vd437, vd439)), vd436) = vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436))], (110 ^ _34185) ^ [] : [-(vmul(vd436, vsucc(vplus(vd437, vd439))) = vplus(vmul(vd436, vplus(vd437, vd439)), vd436))], (112 ^ _34185) ^ [] : [-(vmul(vd436, vplus(vd437, vsucc(vd439))) = vmul(vd436, vsucc(vplus(vd437, vd439))))], (114 ^ _34185) ^ [] : [-(vmul(vd436, vplus(vd437, vd439)) = vplus(vmul(vd436, vd437), vmul(vd436, vd439)))], (116 ^ _34185) ^ [] : [-(vplus(vmul(vd436, vd437), vd436) = vplus(vmul(vd436, vd437), vmul(vd436, v1)))], (118 ^ _34185) ^ [] : [-(vmul(vd436, vsucc(vd437)) = vplus(vmul(vd436, vd437), vd436))], (120 ^ _34185) ^ [] : [-(vmul(vd436, vplus(vd437, v1)) = vmul(vd436, vsucc(vd437)))], (122 ^ _34185) ^ [_38211] : [-(vmul(v1, _38211) = _38211)], (124 ^ _34185) ^ [_38326, _38328] : [-(vmul(_38328, vsucc(_38326)) = vplus(vmul(_38328, _38326), _38328))], (126 ^ _34185) ^ [_38383, _38385] : [-(vmul(_38385, v1) = _38385)], (128 ^ _34185) ^ [_38497, _38499] : [less(_38499, vplus(_38497, v1)), -(leq(_38499, _38497))], (134 ^ _34185) ^ [_38713, _38715] : [greater(_38715, _38713), -(geq(_38715, vplus(_38713, v1)))], (140 ^ _34185) ^ [_38914, _38916] : [-(vplus(_38914, _38916) = vplus(_38916, _38914))], (142 ^ _34185) ^ [_39014, _39016] : [-(vplus(vsucc(_39016), _39014) = vsucc(vplus(_39016, _39014)))], (144 ^ _34185) ^ [_39104] : [-(vplus(v1, _39104) = vsucc(_39104))], (146 ^ _34185) ^ [_39215, _39217, _39219] : [-(vplus(vplus(_39219, _39217), _39215) = vplus(_39219, vplus(_39217, _39215)))], (148 ^ _34185) ^ [_39343, _39345] : [-(vplus(_39345, vsucc(_39343)) = vsucc(vplus(_39345, _39343)))], (150 ^ _34185) ^ [_39399, _39401] : [-(vplus(_39401, v1) = vsucc(_39401))], (158 ^ _34185) ^ [_39666] : [vsucc(_39666) = _39666], (152 ^ _34185) ^ [_39501] : [-(_39501 = v1), -(_39501 = vsucc(vskolem2(_39501)))], (76 ^ _34185) ^ [_36721, _36723] : [_36723 = _36721, -(vskolem2(_36723) = vskolem2(_36721))], (82 ^ _34185) ^ [_36939, _36941] : [_36941 = _36939, -(vsucc(_36941) = vsucc(_36939))], (88 ^ _34185) ^ [_37185, _37187, _37189, _37191] : [-(vplus(_37191, _37187) = vplus(_37189, _37185)), _37191 = _37189, _37187 = _37185], (98 ^ _34185) ^ [_37524, _37526, _37528, _37530] : [-(vmul(_37530, _37526) = vmul(_37528, _37524)), _37530 = _37528, _37526 = _37524], (2 ^ _34185) ^ [_34329] : [-(_34329 = _34329)], (4 ^ _34185) ^ [_34436, _34438] : [_34438 = _34436, -(_34436 = _34438)], (10 ^ _34185) ^ [_34640, _34642, _34644] : [-(_34644 = _34640), _34644 = _34642, _34642 = _34640], (20 ^ _34185) ^ [_34981, _34983, _34985, _34987] : [-(less(_34985, _34981)), less(_34987, _34983), _34987 = _34985, _34983 = _34981], (34 ^ _34185) ^ [_35425, _35427, _35429, _35431] : [-(leq(_35429, _35425)), leq(_35431, _35427), _35431 = _35429, _35427 = _35425], (48 ^ _34185) ^ [_35869, _35871, _35873, _35875] : [-(greater(_35873, _35869)), greater(_35875, _35871), _35875 = _35873, _35871 = _35869], (62 ^ _34185) ^ [_36293, _36295, _36297, _36299] : [-(geq(_36297, _36293)), geq(_36299, _36295), _36299 = _36297, _36295 = _36293]], input).
% 0.33/1.37 ncf('1',plain,[vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436) = vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436))],start(160 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(vplus(vplus(vmul(vd436, vd437), vmul(vd436, vd439)), vd436) = vplus(vmul(vd436, vd437), vplus(vmul(vd436, vd439), vd436)))],extension(146 ^ 1,bind([[_39215, _39217, _39219], [vd436, vmul(vd436, vd439), vmul(vd436, vd437)]]))).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------