%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU211+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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 12:02:40 EDT 2023
% Result : Theorem 44.14s 42.99s
% Output : Proof 44.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU211+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n002.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 13:45:49 EDT 2023
% 0.12/0.34 % CPUTime :
% 44.14/42.99
% 44.14/42.99 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 44.14/42.99 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.14/42.99 %-----------------------------------------------------
% 44.14/42.99 ncf(matrix, plain, [(376 ^ _73663) ^ [] : [subset(relation_inverse_image(370 ^ [], 368 ^ []), relation_inverse_image(370 ^ [], 369 ^ []))], (374 ^ _73663) ^ [] : [-(subset(368 ^ [], 369 ^ []))], (372 ^ _73663) ^ [] : [-(relation(370 ^ []))], !, (299 ^ _61139) ^ [_71202, _71204] : [in(_71204, _71202), -(element(_71204, _71202))], (347 ^ _61139) ^ [_72758] : [empty(_72758), -(_72758 = empty_set)], (253 ^ _61139) ^ [_69560] : [empty(powerset(_69560))], (68 ^ _61139) ^ [_63373, _63375, _63377, _63379] : [-(subset(_63377, _63373)), subset(_63379, _63375), _63379 = _63377, _63375 = _63373], (337 ^ _61139) ^ [_72462, _72464, _72466] : [in(_72466, _72464), element(_72464, powerset(_72462)), empty(_72462)], (268 ^ _61139) ^ [] : [-(empty(266 ^ []))], (261 ^ _61139) ^ [_69878, _69880] : [empty(unordered_pair(_69880, _69878))], (259 ^ _61139) ^ [_69786] : [empty(singleton(_69786))], (315 ^ _61139) ^ [_71739, _71741] : [element(_71741, powerset(_71739)), -(subset(_71741, _71739))], (20 ^ _61139) ^ [_61915, _61917, _61919, _61921] : [-(element(_61919, _61915)), element(_61921, _61917), _61921 = _61919, _61917 = _61915], (226 ^ _61139) ^ [] : [true___, -(true___)], (4 ^ _61139) ^ [_61370, _61372] : [_61372 = _61370, -(_61370 = _61372)], (287 ^ _61139) ^ [] : [-(relation(283 ^ []))], (295 ^ _61139) ^ [] : [empty(293 ^ [])], (263 ^ _61139) ^ [] : [-(empty(empty_set))], (187 ^ _61139) ^ [_67859, _67861] : [subset(_67861, _67859), 190 ^ _61139 : [(191 ^ _61139) ^ [_67996] : [in(_67996, _67861), -(in(_67996, _67859))]]], (270 ^ _61139) ^ [] : [-(relation(266 ^ []))], (297 ^ _61139) ^ [_71093, _71095] : [-(subset(_71095, _71095))], (292 ^ _61139) ^ [_70905] : [-(empty(288 ^ [_70905]))], (114 ^ _61139) ^ [_64965, _64967, _64969, _64971] : [-(relation_inverse_image(_64971, _64967) = relation_inverse_image(_64969, _64965)), _64971 = _64969, _64967 = _64965], (244 ^ _61139) ^ [] : [true___, -(true___)], (138 ^ _61139) ^ [_65797] : [relation(_65797), 141 ^ _61139 : [(142 ^ _61139) ^ [_66004, _66006] : [_66004 = relation_inverse_image(_65797, _66006), 145 ^ _61139 : [(155 ^ _61139) ^ [_66550] : [-(in(_66550, _66004)), 156 ^ _61139 : [(157 ^ _61139) ^ [_66655] : [in(ordered_pair(_66550, _66655), _65797), in(_66655, _66006)]]], (146 ^ _61139) ^ [_66196] : [in(_66196, _66004), 150 ^ _61139 : [(153 ^ _61139) ^ [] : [-(in(149 ^ [_65797, _66004, _66006, _66196], _66006))], (151 ^ _61139) ^ [] : [-(in(ordered_pair(_66196, 149 ^ [_65797, _66004, _66006, _66196]), _65797))]]]]], (165 ^ _61139) ^ [_66910, _66912] : [-(_66910 = relation_inverse_image(_65797, _66912)), 178 ^ _61139 : [(183 ^ _61139) ^ [] : [in(166 ^ [_65797, _66910, _66912], _66910)], (181 ^ _61139) ^ [] : [-(in(177 ^ [_65797, _66910, _66912], _66912))], (179 ^ _61139) ^ [] : [-(in(ordered_pair(166 ^ [_65797, _66910, _66912], 177 ^ [_65797, _66910, _66912]), _65797))]], 169 ^ _61139 : [(172 ^ _61139) ^ [_67214] : [in(ordered_pair(166 ^ [_65797, _66910, _66912], _67214), _65797), in(_67214, _66912)], (170 ^ _61139) ^ [] : [-(in(166 ^ [_65797, _66910, _66912], _66910))]]]]], (321 ^ _61139) ^ [_71905, _71907] : [subset(_71907, _71905), -(element(_71907, powerset(_71905)))], (92 ^ _61139) ^ [_64162, _64164] : [_64164 = _64162, -(singleton(_64164) = singleton(_64162))], (208 ^ _61139) ^ [] : [true___, -(true___)], (285 ^ _61139) ^ [] : [empty(283 ^ [])], (214 ^ _61139) ^ [] : [true___, -(true___)], (255 ^ _61139) ^ [] : [-(empty(empty_set))], (290 ^ _61139) ^ [_70854] : [-(element(288 ^ [_70854], powerset(_70854)))], (220 ^ _61139) ^ [] : [true___, -(true___)], (130 ^ _61139) ^ [_65511] : [empty(_65511), -(relation(_65511))], (353 ^ _61139) ^ [_72960, _72962] : [in(_72962, _72960), empty(_72960)], (282 ^ _61139) ^ [] : [-(empty(280 ^ []))], (272 ^ _61139) ^ [_70232] : [-(empty(_70232)), 276 ^ _61139 : [(279 ^ _61139) ^ [] : [empty(275 ^ [_70232])], (277 ^ _61139) ^ [] : [-(element(275 ^ [_70232], powerset(_70232)))]]], (206 ^ _61139) ^ [_68515, _68517] : [-(ordered_pair(_68517, _68515) = unordered_pair(unordered_pair(_68517, _68515), singleton(_68517)))], (265 ^ _61139) ^ [] : [-(relation(empty_set))], (82 ^ _61139) ^ [_63831, _63833, _63835, _63837] : [-(ordered_pair(_63837, _63833) = ordered_pair(_63835, _63831)), _63837 = _63835, _63833 = _63831], (238 ^ _61139) ^ [] : [true___, -(true___)], (136 ^ _61139) ^ [_65696, _65698] : [-(unordered_pair(_65698, _65696) = unordered_pair(_65696, _65698))], (98 ^ _61139) ^ [_64408, _64410, _64412, _64414] : [-(unordered_pair(_64414, _64410) = unordered_pair(_64412, _64408)), _64414 = _64412, _64410 = _64408], (359 ^ _61139) ^ [_73147, _73149] : [empty(_73149), -(_73149 = _73147), empty(_73147)], (48 ^ _61139) ^ [_62775, _62777] : [-(empty(_62775)), _62777 = _62775, empty(_62777)], (327 ^ _61139) ^ [_72135, _72137, _72139] : [-(element(_72139, _72135)), in(_72139, _72137), element(_72137, powerset(_72135))], (197 ^ _61139) ^ [_68173, _68175] : [199 ^ _61139 : [(202 ^ _61139) ^ [] : [in(198 ^ [_68173, _68175], _68173)], (200 ^ _61139) ^ [] : [-(in(198 ^ [_68173, _68175], _68175))]], -(subset(_68175, _68173))], (124 ^ _61139) ^ [_65314, _65316] : [in(_65316, _65314), in(_65314, _65316)], (251 ^ _61139) ^ [_69478] : [-(element(249 ^ [_69478], _69478))], (257 ^ _61139) ^ [_69705, _69707] : [empty(ordered_pair(_69707, _69705))], (34 ^ _61139) ^ [_62359, _62361, _62363, _62365] : [-(in(_62363, _62359)), in(_62365, _62361), _62365 = _62363, _62361 = _62359], (58 ^ _61139) ^ [_63070, _63072] : [-(relation(_63070)), _63072 = _63070, relation(_63072)], (232 ^ _61139) ^ [] : [true___, -(true___)], (108 ^ _61139) ^ [_64739, _64741] : [_64741 = _64739, -(powerset(_64741) = powerset(_64739))], (305 ^ _61139) ^ [_71412, _71414] : [element(_71414, _71412), -(empty(_71412)), -(in(_71414, _71412))], (2 ^ _61139) ^ [_61263] : [-(_61263 = _61263)], (10 ^ _61139) ^ [_61574, _61576, _61578] : [-(_61578 = _61574), _61578 = _61576, _61576 = _61574]], input).
% 44.14/42.99 ncf('1',plain,[subset(relation_inverse_image(370 ^ [], 368 ^ []), relation_inverse_image(370 ^ [], 369 ^ []))],start(376 ^ 0)).
% 44.14/42.99 ncf('1.1',plain,[-(subset(relation_inverse_image(370 ^ [], 368 ^ []), relation_inverse_image(370 ^ [], 369 ^ []))), 202 : in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 369 ^ []))],extension(197 ^ 1,bind([[_68173, _68175], [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]))).
% 44.14/42.99 ncf('1.1.1',plain,[-(in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 369 ^ []))), 157 : in(ordered_pair(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]), 370 ^ []), 157 : in(149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]], 369 ^ []), 155 : relation_inverse_image(370 ^ [], 369 ^ []) = relation_inverse_image(370 ^ [], 369 ^ []), 142 : relation(370 ^ [])],extension(138 ^ 4,bind([[_65797, _66004, _66006, _66550, _66655], [370 ^ [], relation_inverse_image(370 ^ [], 369 ^ []), 369 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]]]))).
% 44.14/42.99 ncf('1.1.1.1',plain,[-(in(ordered_pair(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]), 370 ^ [])), 191 : in(ordered_pair(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]), 370 ^ []), 191 : subset(370 ^ [], 370 ^ [])],extension(187 ^ 11,bind([[_67859, _67861, _67996], [370 ^ [], 370 ^ [], ordered_pair(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]])]]))).
% 44.14/42.99 ncf('1.1.1.1.1',plain,[-(in(ordered_pair(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]), 370 ^ [])), 146 : in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 368 ^ [])), 146 : relation_inverse_image(370 ^ [], 368 ^ []) = relation_inverse_image(370 ^ [], 368 ^ [])],extension(142 ^ 14,bind([[_66004, _66006, _66196], [relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]]))).
% 44.14/42.99 ncf('1.1.1.1.1.1',plain,[-(in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 368 ^ [])))],extension(200 ^ 17)).
% 44.14/42.99 ncf('1.1.1.1.1.2',plain,[-(relation_inverse_image(370 ^ [], 368 ^ []) = relation_inverse_image(370 ^ [], 368 ^ []))],extension(2 ^ 15,bind([[_61263], [relation_inverse_image(370 ^ [], 368 ^ [])]]))).
% 44.14/42.99 ncf('1.1.1.1.2',plain,[-(subset(370 ^ [], 370 ^ []))],extension(297 ^ 12,bind([[_71093, _71095], [_44923, 370 ^ []]]))).
% 44.14/42.99 ncf('1.1.1.2',plain,[-(in(149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]], 369 ^ [])), 191 : in(149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]], 368 ^ []), 191 : subset(368 ^ [], 369 ^ [])],extension(187 ^ 11,bind([[_67859, _67861, _67996], [369 ^ [], 368 ^ [], 149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]]]))).
% 44.14/42.99 ncf('1.1.1.2.1',plain,[-(in(149 ^ [370 ^ [], relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]], 368 ^ [])), 146 : in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 368 ^ [])), 146 : relation_inverse_image(370 ^ [], 368 ^ []) = relation_inverse_image(370 ^ [], 368 ^ [])],extension(142 ^ 14,bind([[_66004, _66006, _66196], [relation_inverse_image(370 ^ [], 368 ^ []), 368 ^ [], 198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])]]]))).
% 44.14/42.99 ncf('1.1.1.2.1.1',plain,[-(in(198 ^ [relation_inverse_image(370 ^ [], 369 ^ []), relation_inverse_image(370 ^ [], 368 ^ [])], relation_inverse_image(370 ^ [], 368 ^ [])))],extension(200 ^ 17)).
% 44.14/42.99 ncf('1.1.1.2.1.2',plain,[-(relation_inverse_image(370 ^ [], 368 ^ []) = relation_inverse_image(370 ^ [], 368 ^ []))],extension(2 ^ 15,bind([[_61263], [relation_inverse_image(370 ^ [], 368 ^ [])]]))).
% 44.14/42.99 ncf('1.1.1.2.2',plain,[-(subset(368 ^ [], 369 ^ []))],extension(374 ^ 12)).
% 44.14/42.99 ncf('1.1.1.3',plain,[-(relation_inverse_image(370 ^ [], 369 ^ []) = relation_inverse_image(370 ^ [], 369 ^ [])), 370 ^ [] = 370 ^ [], 369 ^ [] = 369 ^ []],extension(114 ^ 7,bind([[_64965, _64967, _64969, _64971], [369 ^ [], 369 ^ [], 370 ^ [], 370 ^ []]]))).
% 44.14/42.99 ncf('1.1.1.3.1',plain,[-(370 ^ [] = 370 ^ [])],extension(2 ^ 8,bind([[_61263], [370 ^ []]]))).
% 44.14/42.99 ncf('1.1.1.3.2',plain,[-(369 ^ [] = 369 ^ [])],extension(2 ^ 8,bind([[_61263], [369 ^ []]]))).
% 44.14/42.99 ncf('1.1.1.4',plain,[-(relation(370 ^ []))],extension(372 ^ 5)).
% 44.14/42.99 %-----------------------------------------------------
% 44.14/42.99 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------