%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET876+1 : TPTP v8.1.2. Released v3.2.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:56:35 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET876+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/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 19:49:26 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(121 ^ _17836) ^ [] : [118 ^ [] = 119 ^ []], (123 ^ _17836) ^ [] : [disjoint(singleton(118 ^ []), singleton(119 ^ []))], (64 ^ _17836) ^ [_19977, _19979] : [in(_19979, _19977), in(_19977, _19979)], (101 ^ _17836) ^ [_21274, _21276] : [-(in(_21276, _21274)), -(disjoint(singleton(_21276), _21274))], (108 ^ _17836) ^ [] : [-(empty(106 ^ []))], (111 ^ _17836) ^ [] : [empty(109 ^ [])], (113 ^ _17836) ^ [_21650, _21652] : [disjoint(_21652, _21650), -(disjoint(_21650, _21652))], (86 ^ _17836) ^ [_20738, _20740] : [-(_20738 = singleton(_20740)), 90 ^ _17836 : [(91 ^ _17836) ^ [] : [-(in(87 ^ [_20738, _20740], _20738))], (93 ^ _17836) ^ [] : [87 ^ [_20738, _20740] = _20740]], 94 ^ _17836 : [(95 ^ _17836) ^ [] : [-(87 ^ [_20738, _20740] = _20740)], (97 ^ _17836) ^ [] : [in(87 ^ [_20738, _20740], _20738)]]], (70 ^ _17836) ^ [_20217, _20219] : [_20217 = singleton(_20219), 73 ^ _17836 : [(74 ^ _17836) ^ [_20387] : [in(_20387, _20217), -(_20387 = _20219)], (80 ^ _17836) ^ [_20559] : [_20559 = _20219, -(in(_20559, _20217))]]], (58 ^ _17836) ^ [_19757, _19759] : [_19759 = _19757, -(singleton(_19759) = singleton(_19757))], (2 ^ _17836) ^ [_17980] : [-(_17980 = _17980)], (4 ^ _17836) ^ [_18087, _18089] : [_18089 = _18087, -(_18087 = _18089)], (10 ^ _17836) ^ [_18291, _18293, _18295] : [-(_18295 = _18291), _18295 = _18293, _18293 = _18291], (20 ^ _17836) ^ [_18632, _18634, _18636, _18638] : [-(in(_18636, _18632)), in(_18638, _18634), _18638 = _18636, _18634 = _18632], (34 ^ _17836) ^ [_19048, _19050] : [-(empty(_19048)), _19050 = _19048, empty(_19050)], (44 ^ _17836) ^ [_19351, _19353, _19355, _19357] : [-(disjoint(_19355, _19351)), disjoint(_19357, _19353), _19357 = _19355, _19353 = _19351]], input).
% 0.34/1.37 ncf('1',plain,[118 ^ [] = 119 ^ []],start(121 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(118 ^ [] = 119 ^ []), 74 : in(118 ^ [], singleton(119 ^ [])), 74 : singleton(119 ^ []) = singleton(119 ^ [])],extension(70 ^ 1,bind([[_20217, _20219, _20387], [singleton(119 ^ []), 119 ^ [], 118 ^ []]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(in(118 ^ [], singleton(119 ^ []))), -(disjoint(singleton(118 ^ []), singleton(119 ^ [])))],extension(101 ^ 4,bind([[_21274, _21276], [singleton(119 ^ []), 118 ^ []]]))).
% 0.34/1.37 ncf('1.1.1.1',plain,[disjoint(singleton(118 ^ []), singleton(119 ^ []))],extension(123 ^ 5)).
% 0.34/1.37 ncf('1.1.2',plain,[-(singleton(119 ^ []) = singleton(119 ^ []))],extension(2 ^ 2,bind([[_17980], [singleton(119 ^ [])]]))).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------