%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM532+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:53 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.11 % Problem : NUM532+1 : TPTP v8.1.2. Released v4.0.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n016.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:07:11 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.37
% 0.31/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 ncf(matrix, plain, [(232 ^ _26424) ^ [] : [aSubsetOf0(xA, xA)], (2 ^ _26424) ^ [_26548] : [-(_26548 = _26548)], (4 ^ _26424) ^ [_26655, _26657] : [_26657 = _26655, -(_26655 = _26657)], (10 ^ _26424) ^ [_26859, _26861, _26863] : [-(_26863 = _26859), _26863 = _26861, _26861 = _26859], (20 ^ _26424) ^ [_27172, _27174] : [-(aElement0(_27172)), _27174 = _27172, aElement0(_27174)], (30 ^ _26424) ^ [_27467, _27469] : [-(isCountable0(_27467)), _27469 = _27467, isCountable0(_27469)], (40 ^ _26424) ^ [_27790, _27792, _27794, _27796] : [-(aElementOf0(_27794, _27790)), aElementOf0(_27796, _27792), _27796 = _27794, _27792 = _27790], (54 ^ _26424) ^ [_28206, _28208] : [-(isFinite0(_28206)), _28208 = _28206, isFinite0(_28208)], (64 ^ _26424) ^ [_28501, _28503] : [-(aSet0(_28501)), _28503 = _28501, aSet0(_28503)], (74 ^ _26424) ^ [_28804, _28806, _28808, _28810] : [-(aSubsetOf0(_28808, _28804)), aSubsetOf0(_28810, _28806), _28810 = _28808, _28806 = _28804], (88 ^ _26424) ^ [_29222] : [aSet0(_29222), true___, -(true___)], (98 ^ _26424) ^ [_29477] : [aElement0(_29477), true___, -(true___)], (108 ^ _26424) ^ [_29732] : [aSet0(_29732), 111 ^ _26424 : [(112 ^ _26424) ^ [_29862] : [aElementOf0(_29862, _29732), -(aElement0(_29862))]]], (118 ^ _26424) ^ [_30063] : [aSet0(_30063), isFinite0(_30063), true___, -(true___)], (132 ^ _26424) ^ [_30433] : [_30433 = slcrc0, 135 ^ _26424 : [(136 ^ _26424) ^ [] : [-(aSet0(_30433))], (138 ^ _26424) ^ [_30614] : [aElementOf0(_30614, _30433)]]], (140 ^ _26424) ^ [_30682] : [-(_30682 = slcrc0), aSet0(_30682), -(aElementOf0(145 ^ [_30682], _30682))], (151 ^ _26424) ^ [] : [-(isFinite0(slcrc0))], (153 ^ _26424) ^ [_31064] : [aSet0(_31064), isCountable0(_31064), true___, -(true___)], (167 ^ _26424) ^ [_31405] : [isFinite0(_31405), aSet0(_31405), isCountable0(_31405)], (177 ^ _26424) ^ [_31675] : [_31675 = slcrc0, aSet0(_31675), isCountable0(_31675)], (230 ^ _26424) ^ [] : [-(aSet0(xA))], (216 ^ _26424) ^ [_32948] : [aSet0(_32948), isFinite0(_32948), 223 ^ _26424 : [(224 ^ _26424) ^ [_33161] : [aSubsetOf0(_33161, _32948), -(isFinite0(_33161))]]], (187 ^ _26424) ^ [_31947] : [aSet0(_31947), 190 ^ _26424 : [(191 ^ _26424) ^ [_32123] : [aSubsetOf0(_32123, _31947), 194 ^ _26424 : [(195 ^ _26424) ^ [] : [-(aSet0(_32123))], (197 ^ _26424) ^ [_32332] : [aElementOf0(_32332, _32123), -(aElementOf0(_32332, _31947))]]], (203 ^ _26424) ^ [_32511] : [-(aSubsetOf0(_32511, _31947)), aSet0(_32511), 209 ^ _26424 : [(210 ^ _26424) ^ [] : [-(aElementOf0(208 ^ [_31947, _32511], _32511))], (212 ^ _26424) ^ [] : [aElementOf0(208 ^ [_31947, _32511], _31947)]]]]]], input).
% 0.31/1.37 ncf('1',plain,[aSubsetOf0(xA, xA)],start(232 ^ 0)).
% 0.31/1.37 ncf('1.1',plain,[-(aSubsetOf0(xA, xA)), 203 : aSet0(xA), 210 : -(aElementOf0(208 ^ [xA, xA], xA)), 203 : aSet0(xA)],extension(187 ^ 1,bind([[_31947, _32511], [xA, xA]]))).
% 0.31/1.37 ncf('1.1.1',plain,[-(aSet0(xA))],extension(230 ^ 4)).
% 0.31/1.37 ncf('1.1.2',plain,[aElementOf0(208 ^ [xA, xA], xA)],extension(212 ^ 6)).
% 0.31/1.37 ncf('1.1.3',plain,[-(aSet0(xA))],extension(230 ^ 2)).
% 0.31/1.37 %-----------------------------------------------------
% 0.31/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------