%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET013+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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:03 EDT 2023
% Result : Theorem 1.52s 2.41s
% Output : Proof 1.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET013+4 : TPTP v8.1.2. Released v2.2.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n019.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:51:57 EDT 2023
% 0.12/0.33 % CPUTime :
% 1.52/2.41
% 1.52/2.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 1.52/2.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.52/2.41 %-----------------------------------------------------
% 1.52/2.41 ncf(matrix, plain, [(301 ^ _41617) ^ [] : [equal_set(intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ []))], (2 ^ _41617) ^ [_41761] : [-(_41761 = _41761)], (4 ^ _41617) ^ [_41868, _41870] : [_41870 = _41868, -(_41868 = _41870)], (10 ^ _41617) ^ [_42072, _42074, _42076] : [-(_42076 = _42072), _42076 = _42074, _42074 = _42072], (20 ^ _41617) ^ [_42413, _42415, _42417, _42419] : [-(subset(_42417, _42413)), subset(_42419, _42415), _42419 = _42417, _42415 = _42413], (34 ^ _41617) ^ [_42857, _42859, _42861, _42863] : [-(member(_42861, _42857)), member(_42863, _42859), _42863 = _42861, _42859 = _42857], (48 ^ _41617) ^ [_43281, _43283, _43285, _43287] : [-(equal_set(_43285, _43281)), equal_set(_43287, _43283), _43287 = _43285, _43283 = _43281], (62 ^ _41617) ^ [_43707, _43709] : [_43709 = _43707, -(power_set(_43709) = power_set(_43707))], (68 ^ _41617) ^ [_43953, _43955, _43957, _43959] : [-(union(_43959, _43955) = union(_43957, _43953)), _43959 = _43957, _43955 = _43953], (78 ^ _41617) ^ [_44312, _44314, _44316, _44318] : [-(difference(_44318, _44314) = difference(_44316, _44312)), _44318 = _44316, _44314 = _44312], (88 ^ _41617) ^ [_44643, _44645] : [_44645 = _44643, -(singleton(_44645) = singleton(_44643))], (94 ^ _41617) ^ [_44889, _44891, _44893, _44895] : [-(unordered_pair(_44895, _44891) = unordered_pair(_44893, _44889)), _44895 = _44893, _44891 = _44889], (104 ^ _41617) ^ [_45220, _45222] : [_45222 = _45220, -(sum(_45222) = sum(_45220))], (110 ^ _41617) ^ [_45438, _45440] : [_45440 = _45438, -(product(_45440) = product(_45438))], (116 ^ _41617) ^ [_45664, _45666, _45668, _45670] : [-(intersection(_45670, _45666) = intersection(_45668, _45664)), _45670 = _45668, _45666 = _45664], (136 ^ _41617) ^ [_46364, _46366] : [138 ^ _41617 : [(139 ^ _41617) ^ [] : [-(member(137 ^ [_46364, _46366], _46366))], (141 ^ _41617) ^ [] : [member(137 ^ [_46364, _46366], _46364)]], -(subset(_46366, _46364))], (126 ^ _41617) ^ [_46050, _46052] : [subset(_46052, _46050), 129 ^ _41617 : [(130 ^ _41617) ^ [_46187] : [member(_46187, _46052), -(member(_46187, _46050))]]], (145 ^ _41617) ^ [_46750, _46752] : [equal_set(_46752, _46750), 148 ^ _41617 : [(149 ^ _41617) ^ [] : [-(subset(_46752, _46750))], (151 ^ _41617) ^ [] : [-(subset(_46750, _46752))]]], (153 ^ _41617) ^ [_46987, _46989] : [-(equal_set(_46989, _46987)), subset(_46989, _46987), subset(_46987, _46989)], (163 ^ _41617) ^ [_47317, _47319] : [member(_47319, power_set(_47317)), -(subset(_47319, _47317))], (169 ^ _41617) ^ [_47483, _47485] : [subset(_47485, _47483), -(member(_47485, power_set(_47483)))], (175 ^ _41617) ^ [_47742, _47744, _47746] : [member(_47746, intersection(_47744, _47742)), 178 ^ _41617 : [(179 ^ _41617) ^ [] : [-(member(_47746, _47744))], (181 ^ _41617) ^ [] : [-(member(_47746, _47742))]]], (183 ^ _41617) ^ [_47993, _47995, _47997] : [-(member(_47997, intersection(_47995, _47993))), member(_47997, _47995), member(_47997, _47993)], (203 ^ _41617) ^ [_48621, _48623, _48625] : [204 ^ _41617 : [(205 ^ _41617) ^ [] : [member(_48625, _48623)], (207 ^ _41617) ^ [] : [member(_48625, _48621)]], -(member(_48625, union(_48623, _48621)))], (193 ^ _41617) ^ [_48353, _48355, _48357] : [member(_48357, union(_48355, _48353)), -(member(_48357, _48355)), -(member(_48357, _48353))], (211 ^ _41617) ^ [_48891] : [member(_48891, empty_set)], (213 ^ _41617) ^ [_49041, _49043, _49045] : [member(_49045, difference(_49041, _49043)), 216 ^ _41617 : [(217 ^ _41617) ^ [] : [-(member(_49045, _49041))], (219 ^ _41617) ^ [] : [member(_49045, _49043)]]], (221 ^ _41617) ^ [_49293, _49295, _49297] : [-(member(_49297, difference(_49293, _49295))), member(_49297, _49293), -(member(_49297, _49295))], (231 ^ _41617) ^ [_49642, _49644] : [member(_49644, singleton(_49642)), -(_49644 = _49642)], (237 ^ _41617) ^ [_49808, _49810] : [_49810 = _49808, -(member(_49810, singleton(_49808)))], (253 ^ _41617) ^ [_50335, _50337, _50339] : [254 ^ _41617 : [(255 ^ _41617) ^ [] : [_50339 = _50337], (257 ^ _41617) ^ [] : [_50339 = _50335]], -(member(_50339, unordered_pair(_50337, _50335)))], (243 ^ _41617) ^ [_50067, _50069, _50071] : [member(_50071, unordered_pair(_50069, _50067)), -(_50071 = _50069), -(_50071 = _50067)], (261 ^ _41617) ^ [_50664, _50666] : [member(_50666, sum(_50664)), 265 ^ _41617 : [(266 ^ _41617) ^ [] : [-(member(264 ^ [_50664, _50666], _50664))], (268 ^ _41617) ^ [] : [-(member(_50666, 264 ^ [_50664, _50666]))]]], (270 ^ _41617) ^ [_50975, _50977] : [-(member(_50977, sum(_50975))), 271 ^ _41617 : [(272 ^ _41617) ^ [_51069] : [member(_51069, _50975), member(_50977, _51069)]]], (290 ^ _41617) ^ [_51670, _51672] : [292 ^ _41617 : [(293 ^ _41617) ^ [] : [-(member(291 ^ [_51670, _51672], _51670))], (295 ^ _41617) ^ [] : [member(_51672, 291 ^ [_51670, _51672])]], -(member(_51672, product(_51670)))], (280 ^ _41617) ^ [_51352, _51354] : [member(_51354, product(_51352)), 283 ^ _41617 : [(284 ^ _41617) ^ [_51493] : [member(_51493, _51352), -(member(_51354, _51493))]]]], input).
% 1.52/2.41 ncf('1',plain,[equal_set(intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ []))],start(301 ^ 0)).
% 1.52/2.41 ncf('1.1',plain,[-(equal_set(intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ []))), subset(intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])), subset(intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ []))],extension(153 ^ 1,bind([[_46987, _46989], [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])]]))).
% 1.52/2.41 ncf('1.1.1',plain,[-(subset(intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ []))), 139 : -(member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], intersection(298 ^ [], 299 ^ [])))],extension(136 ^ 2,bind([[_46364, _46366], [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])]]))).
% 1.52/2.41 ncf('1.1.1.1',plain,[member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], intersection(298 ^ [], 299 ^ [])), 179 : -(member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], 298 ^ []))],extension(175 ^ 5,bind([[_47742, _47744, _47746], [299 ^ [], 298 ^ [], 137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])]]]))).
% 1.52/2.41 ncf('1.1.1.1.1',plain,[member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], 298 ^ []), -(member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], intersection(299 ^ [], 298 ^ []))), member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], 299 ^ [])],extension(183 ^ 8,bind([[_47993, _47995, _47997], [298 ^ [], 299 ^ [], 137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])]]]))).
% 1.52/2.41 ncf('1.1.1.1.1.1',plain,[member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], intersection(299 ^ [], 298 ^ []))],extension(141 ^ 9)).
% 1.52/2.41 ncf('1.1.1.1.1.2',plain,[-(member(137 ^ [intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ [])], 299 ^ []))],extension(181 ^ 9)).
% 1.52/2.41 ncf('1.1.2',plain,[-(subset(intersection(299 ^ [], 298 ^ []), intersection(298 ^ [], 299 ^ []))), 139 : -(member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], intersection(299 ^ [], 298 ^ [])))],extension(136 ^ 2,bind([[_46364, _46366], [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])]]))).
% 1.52/2.41 ncf('1.1.2.1',plain,[member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], intersection(299 ^ [], 298 ^ [])), 179 : -(member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], 299 ^ []))],extension(175 ^ 5,bind([[_47742, _47744, _47746], [298 ^ [], 299 ^ [], 137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])]]]))).
% 1.52/2.41 ncf('1.1.2.1.1',plain,[member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], 299 ^ []), -(member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], intersection(298 ^ [], 299 ^ []))), member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], 298 ^ [])],extension(183 ^ 8,bind([[_47993, _47995, _47997], [299 ^ [], 298 ^ [], 137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])]]]))).
% 1.52/2.41 ncf('1.1.2.1.1.1',plain,[member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], intersection(298 ^ [], 299 ^ []))],extension(141 ^ 9)).
% 1.52/2.41 ncf('1.1.2.1.1.2',plain,[-(member(137 ^ [intersection(298 ^ [], 299 ^ []), intersection(299 ^ [], 298 ^ [])], 298 ^ []))],extension(181 ^ 9)).
% 1.52/2.41 %-----------------------------------------------------
% 1.52/2.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------