%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET940+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:56:42 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET940+1 : TPTP v8.1.2. Released v3.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n026.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 19:22:50 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(84 ^ _17268) ^ [] : [union(unordered_pair(81 ^ [], 82 ^ [])) = set_union2(81 ^ [], 82 ^ [])], (56 ^ _17268) ^ [_19241, _19243] : [-(empty(_19243)), empty(set_union2(_19243, _19241))], (68 ^ _17268) ^ [_19658, _19660] : [-(unordered_pair(_19660, _19658) = unordered_pair(_19658, _19660))], (70 ^ _17268) ^ [_19758, _19760] : [-(set_union2(_19760, _19758) = set_union2(_19758, _19760))], (72 ^ _17268) ^ [_19858, _19860] : [-(set_union2(_19860, _19860) = _19860)], (75 ^ _17268) ^ [] : [-(empty(73 ^ []))], (78 ^ _17268) ^ [] : [empty(76 ^ [])], (80 ^ _17268) ^ [_20114, _20116] : [-(union(unordered_pair(_20116, _20114)) = set_union2(_20116, _20114))], (62 ^ _17268) ^ [_19457, _19459] : [-(empty(_19459)), empty(set_union2(_19457, _19459))], (20 ^ _17268) ^ [_18016, _18018] : [-(empty(_18016)), _18018 = _18016, empty(_18018)], (2 ^ _17268) ^ [_17412] : [-(_17412 = _17412)], (4 ^ _17268) ^ [_17519, _17521] : [_17521 = _17519, -(_17519 = _17521)], (10 ^ _17268) ^ [_17723, _17725, _17727] : [-(_17727 = _17723), _17727 = _17725, _17725 = _17723], (30 ^ _17268) ^ [_18313, _18315] : [_18315 = _18313, -(union(_18315) = union(_18313))], (36 ^ _17268) ^ [_18559, _18561, _18563, _18565] : [-(unordered_pair(_18565, _18561) = unordered_pair(_18563, _18559)), _18565 = _18563, _18561 = _18559], (46 ^ _17268) ^ [_18898, _18900, _18902, _18904] : [-(set_union2(_18904, _18900) = set_union2(_18902, _18898)), _18904 = _18902, _18900 = _18898]], input).
% 0.33/1.38 ncf('1',plain,[union(unordered_pair(81 ^ [], 82 ^ [])) = set_union2(81 ^ [], 82 ^ [])],start(84 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(union(unordered_pair(81 ^ [], 82 ^ [])) = set_union2(81 ^ [], 82 ^ []))],extension(80 ^ 1,bind([[_20114, _20116], [82 ^ [], 81 ^ []]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------