%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET702+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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:19 EDT 2023
% Result : Theorem 0.96s 1.37s
% Output : Proof 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET702+4 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n005.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 18:44:53 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.96/1.37
% 0.96/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.96/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.96/1.37 %-----------------------------------------------------
% 0.96/1.37 ncf(matrix, plain, [(301 ^ _43108) ^ [] : [subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], (2 ^ _43108) ^ [_43252] : [-(_43252 = _43252)], (4 ^ _43108) ^ [_43359, _43361] : [_43361 = _43359, -(_43359 = _43361)], (10 ^ _43108) ^ [_43563, _43565, _43567] : [-(_43567 = _43563), _43567 = _43565, _43565 = _43563], (20 ^ _43108) ^ [_43904, _43906, _43908, _43910] : [-(equal_set(_43908, _43904)), equal_set(_43910, _43906), _43910 = _43908, _43906 = _43904], (34 ^ _43108) ^ [_44348, _44350, _44352, _44354] : [-(member(_44352, _44348)), member(_44354, _44350), _44354 = _44352, _44350 = _44348], (48 ^ _43108) ^ [_44772, _44774, _44776, _44778] : [-(subset(_44776, _44772)), subset(_44778, _44774), _44778 = _44776, _44774 = _44772], (62 ^ _43108) ^ [_45198, _45200] : [_45200 = _45198, -(power_set(_45200) = power_set(_45198))], (68 ^ _43108) ^ [_45444, _45446, _45448, _45450] : [-(union(_45450, _45446) = union(_45448, _45444)), _45450 = _45448, _45446 = _45444], (78 ^ _43108) ^ [_45803, _45805, _45807, _45809] : [-(difference(_45809, _45805) = difference(_45807, _45803)), _45809 = _45807, _45805 = _45803], (88 ^ _43108) ^ [_46134, _46136] : [_46136 = _46134, -(singleton(_46136) = singleton(_46134))], (94 ^ _43108) ^ [_46380, _46382, _46384, _46386] : [-(unordered_pair(_46386, _46382) = unordered_pair(_46384, _46380)), _46386 = _46384, _46382 = _46380], (104 ^ _43108) ^ [_46711, _46713] : [_46713 = _46711, -(sum(_46713) = sum(_46711))], (110 ^ _43108) ^ [_46929, _46931] : [_46931 = _46929, -(product(_46931) = product(_46929))], (116 ^ _43108) ^ [_47155, _47157, _47159, _47161] : [-(intersection(_47161, _47157) = intersection(_47159, _47155)), _47161 = _47159, _47157 = _47155], (136 ^ _43108) ^ [_47855, _47857] : [138 ^ _43108 : [(139 ^ _43108) ^ [] : [-(member(137 ^ [_47855, _47857], _47857))], (141 ^ _43108) ^ [] : [member(137 ^ [_47855, _47857], _47855)]], -(subset(_47857, _47855))], (126 ^ _43108) ^ [_47541, _47543] : [subset(_47543, _47541), 129 ^ _43108 : [(130 ^ _43108) ^ [_47678] : [member(_47678, _47543), -(member(_47678, _47541))]]], (145 ^ _43108) ^ [_48241, _48243] : [equal_set(_48243, _48241), 148 ^ _43108 : [(149 ^ _43108) ^ [] : [-(subset(_48243, _48241))], (151 ^ _43108) ^ [] : [-(subset(_48241, _48243))]]], (153 ^ _43108) ^ [_48478, _48480] : [-(equal_set(_48480, _48478)), subset(_48480, _48478), subset(_48478, _48480)], (163 ^ _43108) ^ [_48808, _48810] : [member(_48810, power_set(_48808)), -(subset(_48810, _48808))], (169 ^ _43108) ^ [_48974, _48976] : [subset(_48976, _48974), -(member(_48976, power_set(_48974)))], (175 ^ _43108) ^ [_49233, _49235, _49237] : [member(_49237, intersection(_49235, _49233)), 178 ^ _43108 : [(179 ^ _43108) ^ [] : [-(member(_49237, _49235))], (181 ^ _43108) ^ [] : [-(member(_49237, _49233))]]], (183 ^ _43108) ^ [_49484, _49486, _49488] : [-(member(_49488, intersection(_49486, _49484))), member(_49488, _49486), member(_49488, _49484)], (203 ^ _43108) ^ [_50112, _50114, _50116] : [204 ^ _43108 : [(205 ^ _43108) ^ [] : [member(_50116, _50114)], (207 ^ _43108) ^ [] : [member(_50116, _50112)]], -(member(_50116, union(_50114, _50112)))], (193 ^ _43108) ^ [_49844, _49846, _49848] : [member(_49848, union(_49846, _49844)), -(member(_49848, _49846)), -(member(_49848, _49844))], (211 ^ _43108) ^ [_50382] : [member(_50382, empty_set)], (213 ^ _43108) ^ [_50532, _50534, _50536] : [member(_50536, difference(_50532, _50534)), 216 ^ _43108 : [(217 ^ _43108) ^ [] : [-(member(_50536, _50532))], (219 ^ _43108) ^ [] : [member(_50536, _50534)]]], (221 ^ _43108) ^ [_50784, _50786, _50788] : [-(member(_50788, difference(_50784, _50786))), member(_50788, _50784), -(member(_50788, _50786))], (231 ^ _43108) ^ [_51133, _51135] : [member(_51135, singleton(_51133)), -(_51135 = _51133)], (237 ^ _43108) ^ [_51299, _51301] : [_51301 = _51299, -(member(_51301, singleton(_51299)))], (253 ^ _43108) ^ [_51826, _51828, _51830] : [254 ^ _43108 : [(255 ^ _43108) ^ [] : [_51830 = _51828], (257 ^ _43108) ^ [] : [_51830 = _51826]], -(member(_51830, unordered_pair(_51828, _51826)))], (243 ^ _43108) ^ [_51558, _51560, _51562] : [member(_51562, unordered_pair(_51560, _51558)), -(_51562 = _51560), -(_51562 = _51558)], (261 ^ _43108) ^ [_52155, _52157] : [member(_52157, sum(_52155)), 265 ^ _43108 : [(266 ^ _43108) ^ [] : [-(member(264 ^ [_52155, _52157], _52155))], (268 ^ _43108) ^ [] : [-(member(_52157, 264 ^ [_52155, _52157]))]]], (270 ^ _43108) ^ [_52466, _52468] : [-(member(_52468, sum(_52466))), 271 ^ _43108 : [(272 ^ _43108) ^ [_52560] : [member(_52560, _52466), member(_52468, _52560)]]], (290 ^ _43108) ^ [_53161, _53163] : [292 ^ _43108 : [(293 ^ _43108) ^ [] : [-(member(291 ^ [_53161, _53163], _53161))], (295 ^ _43108) ^ [] : [member(_53163, 291 ^ [_53161, _53163])]], -(member(_53163, product(_53161)))], (280 ^ _43108) ^ [_52843, _52845] : [member(_52845, product(_52843)), 283 ^ _43108 : [(284 ^ _43108) ^ [_52984] : [member(_52984, _52843), -(member(_52845, _52984))]]]], input).
% 0.96/1.37 ncf('1',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))), 219 : member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ [])))],start(213 ^ 0,bind([[_50532, _50534, _50536], [intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))))), -(subset(difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))), product(intersection(298 ^ [], 299 ^ []))))],extension(136 ^ 1,bind([[_47855, _47857], [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]))).
% 0.96/1.37 ncf('1.1.1',plain,[subset(difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))), product(intersection(298 ^ [], 299 ^ []))), 130 : member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))), 130 : -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], product(intersection(298 ^ [], 299 ^ []))))],extension(126 ^ 2,bind([[_47541, _47543, _47678], [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))]]]))).
% 0.96/1.37 ncf('1.1.1.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))))), member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], intersection(product(298 ^ []), product(299 ^ []))), -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], product(intersection(298 ^ [], 299 ^ []))))],extension(221 ^ 5,bind([[_50784, _50786, _50788], [intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))]]]))).
% 0.96/1.37 ncf('1.1.1.1.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], intersection(product(298 ^ []), product(299 ^ [])))), -(subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))))],extension(136 ^ 6,bind([[_47855, _47857], [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))]]))).
% 0.96/1.37 ncf('1.1.1.1.1.1',plain,[subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))],extension(301 ^ 7)).
% 0.96/1.37 ncf('1.1.1.1.2',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], product(intersection(298 ^ [], 299 ^ []))), -(subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))))],extension(136 ^ 6,bind([[_47855, _47857], [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))]]))).
% 0.96/1.37 ncf('1.1.1.1.2.1',plain,[subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))],extension(301 ^ 7)).
% 0.96/1.37 ncf('1.1.1.2',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))], product(intersection(298 ^ [], 299 ^ []))), -(subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ []))))],extension(136 ^ 5,bind([[_47855, _47857], [product(intersection(298 ^ [], 299 ^ [])), intersection(product(298 ^ []), product(299 ^ []))]]))).
% 0.96/1.37 ncf('1.1.1.2.1',plain,[subset(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))],extension(301 ^ 6)).
% 0.96/1.37 ncf('1.2',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ [])))), member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], union(product(intersection(298 ^ [], 299 ^ [])), product(298 ^ []))), -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(298 ^ [])))],extension(193 ^ 3,bind([[_49844, _49846, _49848], [product(298 ^ []), product(intersection(298 ^ [], 299 ^ [])), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.2.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], union(product(intersection(298 ^ [], 299 ^ [])), product(298 ^ [])))), 207 : member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(298 ^ []))],extension(203 ^ 4,bind([[_50112, _50114, _50116], [product(298 ^ []), product(intersection(298 ^ [], 299 ^ [])), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.2.1.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(298 ^ []))), member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], intersection(product(298 ^ []), product(299 ^ [])))],extension(175 ^ 7,bind([[_49233, _49235, _49237], [product(299 ^ []), product(298 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.2.1.1.1',plain,[-(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], intersection(product(298 ^ []), product(299 ^ []))))],extension(217 ^ 8)).
% 0.96/1.37 ncf('1.2.2',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(298 ^ [])), 284 : member(291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]], 298 ^ []), 284 : -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], 291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]))],extension(280 ^ 4,bind([[_52843, _52845, _52984], [298 ^ [], 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], 291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]]))).
% 0.96/1.37 ncf('1.2.2.1',plain,[-(member(291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]], 298 ^ [])), member(291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]], intersection(298 ^ [], 299 ^ []))],extension(175 ^ 7,bind([[_49233, _49235, _49237], [299 ^ [], 298 ^ [], 291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]]))).
% 0.96/1.37 ncf('1.2.2.1.1',plain,[-(member(291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]], intersection(298 ^ [], 299 ^ []))), -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ []))))],extension(290 ^ 8,bind([[_53161, _53163], [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.2.2.1.1.1',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ [])))],reduction('1')).
% 0.96/1.37 ncf('1.2.2.2',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], 291 ^ [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]), -(member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ []))))],extension(290 ^ 7,bind([[_53161, _53163], [intersection(298 ^ [], 299 ^ []), 137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))]]]))).
% 0.96/1.37 ncf('1.2.2.2.1',plain,[member(137 ^ [product(intersection(298 ^ [], 299 ^ [])), difference(intersection(product(298 ^ []), product(299 ^ [])), product(intersection(298 ^ [], 299 ^ [])))], product(intersection(298 ^ [], 299 ^ [])))],reduction('1')).
% 0.96/1.37 %-----------------------------------------------------
% 0.96/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------