%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET008+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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:55:01 EDT 2023
% Result : Theorem 0.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET008+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n027.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 19:34:05 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(203 ^ _27467) ^ [] : [intersection(difference(200 ^ [], 201 ^ []), 201 ^ []) = empty_set], (58 ^ _27467) ^ [_29436, _29438, _29440, _29442] : [-(intersection(_29442, _29438) = intersection(_29440, _29436)), _29442 = _29440, _29438 = _29436], (68 ^ _27467) ^ [_29775, _29777, _29779, _29781] : [-(difference(_29781, _29777) = difference(_29779, _29775)), _29781 = _29779, _29777 = _29775], (2 ^ _27467) ^ [_27611] : [-(_27611 = _27611)], (4 ^ _27467) ^ [_27718, _27720] : [_27720 = _27718, -(_27718 = _27720)], (10 ^ _27467) ^ [_27922, _27924, _27926] : [-(_27926 = _27922), _27926 = _27924, _27924 = _27922], (20 ^ _27467) ^ [_28263, _28265, _28267, _28269] : [-(subset(_28267, _28263)), subset(_28269, _28265), _28269 = _28267, _28265 = _28263], (34 ^ _27467) ^ [_28679, _28681] : [-(empty(_28679)), _28681 = _28679, empty(_28681)], (44 ^ _27467) ^ [_28982, _28984, _28986, _28988] : [-(member(_28986, _28982)), member(_28988, _28984), _28988 = _28986, _28984 = _28982], (78 ^ _27467) ^ [_30155, _30157, _30159] : [member(_30155, intersection(_30159, _30157)), 81 ^ _27467 : [(82 ^ _27467) ^ [] : [-(member(_30155, _30159))], (84 ^ _27467) ^ [] : [-(member(_30155, _30157))]]], (86 ^ _27467) ^ [_30406, _30408, _30410] : [-(member(_30406, intersection(_30410, _30408))), member(_30406, _30410), member(_30406, _30408)], (96 ^ _27467) ^ [_30766, _30768, _30770] : [member(_30766, difference(_30770, _30768)), 99 ^ _27467 : [(100 ^ _27467) ^ [] : [-(member(_30766, _30770))], (102 ^ _27467) ^ [] : [member(_30766, _30768)]]], (104 ^ _27467) ^ [_31018, _31020, _31022] : [-(member(_31018, difference(_31022, _31020))), member(_31018, _31022), -(member(_31018, _31020))], (114 ^ _27467) ^ [_31308] : [member(_31308, empty_set)], (116 ^ _27467) ^ [_31444, _31446] : [_31446 = _31444, 119 ^ _27467 : [(120 ^ _27467) ^ [] : [-(subset(_31446, _31444))], (122 ^ _27467) ^ [] : [-(subset(_31444, _31446))]]], (124 ^ _27467) ^ [_31681, _31683] : [-(_31683 = _31681), subset(_31683, _31681), subset(_31681, _31683)], (134 ^ _27467) ^ [_31967, _31969] : [-(intersection(_31969, _31967) = intersection(_31967, _31969))], (146 ^ _27467) ^ [_32425, _32427] : [148 ^ _27467 : [(149 ^ _27467) ^ [] : [-(member(147 ^ [_32425, _32427], _32427))], (151 ^ _27467) ^ [] : [member(147 ^ [_32425, _32427], _32425)]], -(subset(_32427, _32425))], (136 ^ _27467) ^ [_32111, _32113] : [subset(_32113, _32111), 139 ^ _27467 : [(140 ^ _27467) ^ [_32248] : [member(_32248, _32113), -(member(_32248, _32111))]]], (155 ^ _27467) ^ [_32753] : [-(subset(_32753, _32753))], (157 ^ _27467) ^ [_32875] : [empty(_32875), 160 ^ _27467 : [(161 ^ _27467) ^ [_32986] : [member(_32986, _32875)]]], (163 ^ _27467) ^ [_33052] : [-(member(164 ^ [_33052], _33052)), -(empty(_33052))], (186 ^ _27467) ^ [_33838, _33840] : [-(_33840 = _33838), 190 ^ _27467 : [(191 ^ _27467) ^ [] : [-(member(187 ^ [_33838, _33840], _33840))], (193 ^ _27467) ^ [] : [member(187 ^ [_33838, _33840], _33838)]], 194 ^ _27467 : [(195 ^ _27467) ^ [] : [-(member(187 ^ [_33838, _33840], _33838))], (197 ^ _27467) ^ [] : [member(187 ^ [_33838, _33840], _33840)]]], (170 ^ _27467) ^ [_33321, _33323] : [_33323 = _33321, 173 ^ _27467 : [(174 ^ _27467) ^ [_33487] : [member(_33487, _33323), -(member(_33487, _33321))], (180 ^ _27467) ^ [_33659] : [member(_33659, _33321), -(member(_33659, _33323))]]]], input).
% 0.37/1.37 ncf('1',plain,[member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], difference(200 ^ [], 201 ^ [])), 102 : member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], 201 ^ [])],start(96 ^ 0,bind([[_30766, _30768, _30770], [187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], 201 ^ [], 200 ^ []]]))).
% 0.37/1.37 ncf('1.1',plain,[-(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], difference(200 ^ [], 201 ^ []))), member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], intersection(difference(200 ^ [], 201 ^ []), 201 ^ []))],extension(78 ^ 1,bind([[_30155, _30157, _30159], [187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], 201 ^ [], difference(200 ^ [], 201 ^ [])]]))).
% 0.37/1.37 ncf('1.1.1',plain,[-(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], intersection(difference(200 ^ [], 201 ^ []), 201 ^ []))), -(intersection(difference(200 ^ [], 201 ^ []), 201 ^ []) = empty_set), 195 : -(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], empty_set))],extension(186 ^ 2,bind([[_33838, _33840], [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])]]))).
% 0.37/1.37 ncf('1.1.1.1',plain,[intersection(difference(200 ^ [], 201 ^ []), 201 ^ []) = empty_set],extension(203 ^ 3)).
% 0.37/1.37 ncf('1.1.1.2',plain,[member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], empty_set)],extension(114 ^ 5,bind([[_31308], [187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])]]]))).
% 0.37/1.37 ncf('1.2',plain,[-(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], 201 ^ [])), member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], intersection(difference(200 ^ [], 201 ^ []), 201 ^ []))],extension(78 ^ 3,bind([[_30155, _30157, _30159], [187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], 201 ^ [], difference(200 ^ [], 201 ^ [])]]))).
% 0.37/1.37 ncf('1.2.1',plain,[-(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], intersection(difference(200 ^ [], 201 ^ []), 201 ^ []))), -(intersection(difference(200 ^ [], 201 ^ []), 201 ^ []) = empty_set), 195 : -(member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], empty_set))],extension(186 ^ 4,bind([[_33838, _33840], [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])]]))).
% 0.37/1.37 ncf('1.2.1.1',plain,[intersection(difference(200 ^ [], 201 ^ []), 201 ^ []) = empty_set],extension(203 ^ 5)).
% 0.37/1.37 ncf('1.2.1.2',plain,[member(187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])], empty_set)],extension(114 ^ 7,bind([[_31308], [187 ^ [empty_set, intersection(difference(200 ^ [], 201 ^ []), 201 ^ [])]]]))).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------