%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET692+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:18 EDT 2023
% Result : Theorem 0.46s 1.33s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.09 % Problem : SET692+4 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.09 % Command : nanocop.sh %s %d
% 0.09/0.28 % Computer : n017.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Thu May 18 18:28:00 EDT 2023
% 0.09/0.28 % CPUTime :
% 0.46/1.33
% 0.46/1.33 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.46/1.33 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/1.33 %-----------------------------------------------------
% 0.46/1.33 ncf(matrix, plain, [(301 ^ _43064) ^ [] : [302 ^ _43064 : [(303 ^ _43064) ^ [] : [-(equal_set(298 ^ [], intersection(298 ^ [], 299 ^ [])))], (305 ^ _43064) ^ [] : [subset(298 ^ [], 299 ^ [])]], 306 ^ _43064 : [(307 ^ _43064) ^ [] : [-(subset(298 ^ [], 299 ^ []))], (309 ^ _43064) ^ [] : [equal_set(298 ^ [], intersection(298 ^ [], 299 ^ []))]]], (2 ^ _43064) ^ [_43208] : [-(_43208 = _43208)], (4 ^ _43064) ^ [_43315, _43317] : [_43317 = _43315, -(_43315 = _43317)], (10 ^ _43064) ^ [_43519, _43521, _43523] : [-(_43523 = _43519), _43523 = _43521, _43521 = _43519], (20 ^ _43064) ^ [_43860, _43862, _43864, _43866] : [-(member(_43864, _43860)), member(_43866, _43862), _43866 = _43864, _43862 = _43860], (34 ^ _43064) ^ [_44304, _44306, _44308, _44310] : [-(equal_set(_44308, _44304)), equal_set(_44310, _44306), _44310 = _44308, _44306 = _44304], (48 ^ _43064) ^ [_44728, _44730, _44732, _44734] : [-(subset(_44732, _44728)), subset(_44734, _44730), _44734 = _44732, _44730 = _44728], (62 ^ _43064) ^ [_45154, _45156] : [_45156 = _45154, -(power_set(_45156) = power_set(_45154))], (68 ^ _43064) ^ [_45400, _45402, _45404, _45406] : [-(union(_45406, _45402) = union(_45404, _45400)), _45406 = _45404, _45402 = _45400], (78 ^ _43064) ^ [_45759, _45761, _45763, _45765] : [-(difference(_45765, _45761) = difference(_45763, _45759)), _45765 = _45763, _45761 = _45759], (88 ^ _43064) ^ [_46090, _46092] : [_46092 = _46090, -(singleton(_46092) = singleton(_46090))], (94 ^ _43064) ^ [_46336, _46338, _46340, _46342] : [-(unordered_pair(_46342, _46338) = unordered_pair(_46340, _46336)), _46342 = _46340, _46338 = _46336], (104 ^ _43064) ^ [_46667, _46669] : [_46669 = _46667, -(sum(_46669) = sum(_46667))], (110 ^ _43064) ^ [_46885, _46887] : [_46887 = _46885, -(product(_46887) = product(_46885))], (116 ^ _43064) ^ [_47111, _47113, _47115, _47117] : [-(intersection(_47117, _47113) = intersection(_47115, _47111)), _47117 = _47115, _47113 = _47111], (136 ^ _43064) ^ [_47811, _47813] : [138 ^ _43064 : [(139 ^ _43064) ^ [] : [-(member(137 ^ [_47811, _47813], _47813))], (141 ^ _43064) ^ [] : [member(137 ^ [_47811, _47813], _47811)]], -(subset(_47813, _47811))], (126 ^ _43064) ^ [_47497, _47499] : [subset(_47499, _47497), 129 ^ _43064 : [(130 ^ _43064) ^ [_47634] : [member(_47634, _47499), -(member(_47634, _47497))]]], (145 ^ _43064) ^ [_48197, _48199] : [equal_set(_48199, _48197), 148 ^ _43064 : [(149 ^ _43064) ^ [] : [-(subset(_48199, _48197))], (151 ^ _43064) ^ [] : [-(subset(_48197, _48199))]]], (153 ^ _43064) ^ [_48434, _48436] : [-(equal_set(_48436, _48434)), subset(_48436, _48434), subset(_48434, _48436)], (163 ^ _43064) ^ [_48764, _48766] : [member(_48766, power_set(_48764)), -(subset(_48766, _48764))], (169 ^ _43064) ^ [_48930, _48932] : [subset(_48932, _48930), -(member(_48932, power_set(_48930)))], (175 ^ _43064) ^ [_49189, _49191, _49193] : [member(_49193, intersection(_49191, _49189)), 178 ^ _43064 : [(179 ^ _43064) ^ [] : [-(member(_49193, _49191))], (181 ^ _43064) ^ [] : [-(member(_49193, _49189))]]], (183 ^ _43064) ^ [_49440, _49442, _49444] : [-(member(_49444, intersection(_49442, _49440))), member(_49444, _49442), member(_49444, _49440)], (203 ^ _43064) ^ [_50068, _50070, _50072] : [204 ^ _43064 : [(205 ^ _43064) ^ [] : [member(_50072, _50070)], (207 ^ _43064) ^ [] : [member(_50072, _50068)]], -(member(_50072, union(_50070, _50068)))], (193 ^ _43064) ^ [_49800, _49802, _49804] : [member(_49804, union(_49802, _49800)), -(member(_49804, _49802)), -(member(_49804, _49800))], (211 ^ _43064) ^ [_50338] : [member(_50338, empty_set)], (213 ^ _43064) ^ [_50488, _50490, _50492] : [member(_50492, difference(_50488, _50490)), 216 ^ _43064 : [(217 ^ _43064) ^ [] : [-(member(_50492, _50488))], (219 ^ _43064) ^ [] : [member(_50492, _50490)]]], (221 ^ _43064) ^ [_50740, _50742, _50744] : [-(member(_50744, difference(_50740, _50742))), member(_50744, _50740), -(member(_50744, _50742))], (231 ^ _43064) ^ [_51089, _51091] : [member(_51091, singleton(_51089)), -(_51091 = _51089)], (237 ^ _43064) ^ [_51255, _51257] : [_51257 = _51255, -(member(_51257, singleton(_51255)))], (253 ^ _43064) ^ [_51782, _51784, _51786] : [254 ^ _43064 : [(255 ^ _43064) ^ [] : [_51786 = _51784], (257 ^ _43064) ^ [] : [_51786 = _51782]], -(member(_51786, unordered_pair(_51784, _51782)))], (243 ^ _43064) ^ [_51514, _51516, _51518] : [member(_51518, unordered_pair(_51516, _51514)), -(_51518 = _51516), -(_51518 = _51514)], (261 ^ _43064) ^ [_52111, _52113] : [member(_52113, sum(_52111)), 265 ^ _43064 : [(266 ^ _43064) ^ [] : [-(member(264 ^ [_52111, _52113], _52111))], (268 ^ _43064) ^ [] : [-(member(_52113, 264 ^ [_52111, _52113]))]]], (270 ^ _43064) ^ [_52422, _52424] : [-(member(_52424, sum(_52422))), 271 ^ _43064 : [(272 ^ _43064) ^ [_52516] : [member(_52516, _52422), member(_52424, _52516)]]], (290 ^ _43064) ^ [_53117, _53119] : [292 ^ _43064 : [(293 ^ _43064) ^ [] : [-(member(291 ^ [_53117, _53119], _53117))], (295 ^ _43064) ^ [] : [member(_53119, 291 ^ [_53117, _53119])]], -(member(_53119, product(_53117)))], (280 ^ _43064) ^ [_52799, _52801] : [member(_52801, product(_52799)), 283 ^ _43064 : [(284 ^ _43064) ^ [_52940] : [member(_52940, _52799), -(member(_52801, _52940))]]]], input).
% 0.46/1.33 ncf('1',plain,[305 : subset(298 ^ [], 299 ^ []), 309 : equal_set(298 ^ [], intersection(298 ^ [], 299 ^ []))],start(301 ^ 0)).
% 0.46/1.33 ncf('1.1',plain,[-(subset(298 ^ [], 299 ^ [])), 141 : member(137 ^ [299 ^ [], 298 ^ []], 299 ^ [])],extension(136 ^ 3,bind([[_47811, _47813], [299 ^ [], 298 ^ []]]))).
% 0.46/1.33 ncf('1.1.1',plain,[-(member(137 ^ [299 ^ [], 298 ^ []], 299 ^ [])), member(137 ^ [299 ^ [], 298 ^ []], intersection(298 ^ [], 299 ^ []))],extension(175 ^ 6,bind([[_49189, _49191, _49193], [299 ^ [], 298 ^ [], 137 ^ [299 ^ [], 298 ^ []]]]))).
% 0.46/1.33 ncf('1.1.1.1',plain,[-(member(137 ^ [299 ^ [], 298 ^ []], intersection(298 ^ [], 299 ^ []))), 130 : member(137 ^ [299 ^ [], 298 ^ []], 298 ^ []), 130 : subset(298 ^ [], intersection(298 ^ [], 299 ^ []))],extension(126 ^ 7,bind([[_47497, _47499, _47634], [intersection(298 ^ [], 299 ^ []), 298 ^ [], 137 ^ [299 ^ [], 298 ^ []]]]))).
% 0.46/1.33 ncf('1.1.1.1.1',plain,[-(member(137 ^ [299 ^ [], 298 ^ []], 298 ^ []))],extension(139 ^ 10)).
% 0.46/1.33 ncf('1.1.1.1.2',plain,[-(subset(298 ^ [], intersection(298 ^ [], 299 ^ []))), equal_set(298 ^ [], intersection(298 ^ [], 299 ^ []))],extension(145 ^ 8,bind([[_48197, _48199], [intersection(298 ^ [], 299 ^ []), 298 ^ []]]))).
% 0.46/1.33 ncf('1.1.1.1.2.1',plain,[-(equal_set(298 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(303 ^ 9)).
% 0.46/1.33 ncf('1.2',plain,[-(equal_set(298 ^ [], intersection(298 ^ [], 299 ^ []))), subset(298 ^ [], intersection(298 ^ [], 299 ^ [])), subset(intersection(298 ^ [], 299 ^ []), 298 ^ [])],extension(153 ^ 3,bind([[_48434, _48436], [intersection(298 ^ [], 299 ^ []), 298 ^ []]]))).
% 0.46/1.33 ncf('1.2.1',plain,[-(subset(298 ^ [], intersection(298 ^ [], 299 ^ []))), 139 : -(member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 298 ^ []))],extension(136 ^ 4,bind([[_47811, _47813], [intersection(298 ^ [], 299 ^ []), 298 ^ []]]))).
% 0.46/1.33 ncf('1.2.1.1',plain,[member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 298 ^ []), -(member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], intersection(298 ^ [], 299 ^ []))), member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 299 ^ [])],extension(183 ^ 7,bind([[_49440, _49442, _49444], [299 ^ [], 298 ^ [], 137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []]]]))).
% 0.46/1.33 ncf('1.2.1.1.1',plain,[member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], intersection(298 ^ [], 299 ^ []))],extension(141 ^ 8)).
% 0.46/1.33 ncf('1.2.1.1.2',plain,[-(member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 299 ^ [])), 130 : member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 298 ^ []), 130 : subset(298 ^ [], 299 ^ [])],extension(126 ^ 8,bind([[_47497, _47499, _47634], [299 ^ [], 298 ^ [], 137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []]]]))).
% 0.46/1.33 ncf('1.2.1.1.2.1',plain,[-(member(137 ^ [intersection(298 ^ [], 299 ^ []), 298 ^ []], 298 ^ []))],reduction('1.2.1')).
% 0.46/1.33 ncf('1.2.1.1.2.2',plain,[-(subset(298 ^ [], 299 ^ []))],extension(307 ^ 9)).
% 0.46/1.33 ncf('1.2.2',plain,[-(subset(intersection(298 ^ [], 299 ^ []), 298 ^ [])), 139 : -(member(137 ^ [298 ^ [], intersection(298 ^ [], 299 ^ [])], intersection(298 ^ [], 299 ^ [])))],extension(136 ^ 4,bind([[_47811, _47813], [298 ^ [], intersection(298 ^ [], 299 ^ [])]]))).
% 0.46/1.33 ncf('1.2.2.1',plain,[member(137 ^ [298 ^ [], intersection(298 ^ [], 299 ^ [])], intersection(298 ^ [], 299 ^ [])), 179 : -(member(137 ^ [298 ^ [], intersection(298 ^ [], 299 ^ [])], 298 ^ []))],extension(175 ^ 7,bind([[_49189, _49191, _49193], [299 ^ [], 298 ^ [], 137 ^ [298 ^ [], intersection(298 ^ [], 299 ^ [])]]]))).
% 0.46/1.33 ncf('1.2.2.1.1',plain,[member(137 ^ [298 ^ [], intersection(298 ^ [], 299 ^ [])], 298 ^ [])],extension(141 ^ 10)).
% 0.46/1.33 %-----------------------------------------------------
% 0.46/1.33 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------