%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU255+1 : TPTP v8.1.2. Released v3.3.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 12:02:53 EDT 2023
% Result : Theorem 3.96s 4.48s
% Output : Proof 3.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEU255+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n027.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 13:09:20 EDT 2023
% 0.12/0.33 % CPUTime :
% 3.96/4.48
% 3.96/4.48 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 3.96/4.48 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.96/4.48 %-----------------------------------------------------
% 3.96/4.48 ncf(matrix, plain, [(372 ^ _55260) ^ [] : [-(relation(370 ^ []))], (374 ^ _55260) ^ [] : [-(antisymmetric(370 ^ []))], (376 ^ _55260) ^ [] : [antisymmetric(relation_restriction(370 ^ [], 369 ^ []))], (98 ^ _55260) ^ [_58417, _58419, _58421, _58423] : [-(unordered_pair(_58423, _58419) = unordered_pair(_58421, _58417)), _58423 = _58421, _58419 = _58417], (108 ^ _55260) ^ [_58748, _58750] : [_58750 = _58748, -(singleton(_58750) = singleton(_58748))], (114 ^ _55260) ^ [_58994, _58996, _58998, _59000] : [-(ordered_pair(_59000, _58996) = ordered_pair(_58998, _58994)), _59000 = _58998, _58996 = _58994], (124 ^ _55260) ^ [_59353, _59355, _59357, _59359] : [-(cartesian_product2(_59359, _59355) = cartesian_product2(_59357, _59353)), _59359 = _59357, _59355 = _59353], (134 ^ _55260) ^ [_59712, _59714, _59716, _59718] : [-(set_intersection2(_59718, _59714) = set_intersection2(_59716, _59712)), _59718 = _59716, _59714 = _59712], (144 ^ _55260) ^ [_60051, _60053, _60055, _60057] : [-(relation_restriction(_60057, _60053) = relation_restriction(_60055, _60051)), _60057 = _60055, _60053 = _60051], (2 ^ _55260) ^ [_55404] : [-(_55404 = _55404)], (4 ^ _55260) ^ [_55511, _55513] : [_55513 = _55511, -(_55511 = _55513)], (10 ^ _55260) ^ [_55715, _55717, _55719] : [-(_55719 = _55715), _55719 = _55717, _55717 = _55715], (20 ^ _55260) ^ [_56028, _56030] : [-(function(_56028)), _56030 = _56028, function(_56030)], (30 ^ _55260) ^ [_56323, _56325] : [-(one_to_one(_56323)), _56325 = _56323, one_to_one(_56325)], (40 ^ _55260) ^ [_56646, _56648, _56650, _56652] : [-(element(_56650, _56646)), element(_56652, _56648), _56652 = _56650, _56648 = _56646], (54 ^ _55260) ^ [_57090, _57092, _57094, _57096] : [-(in(_57094, _57090)), in(_57096, _57092), _57096 = _57094, _57092 = _57090], (68 ^ _55260) ^ [_57506, _57508] : [-(empty(_57506)), _57508 = _57506, empty(_57508)], (78 ^ _55260) ^ [_57801, _57803] : [-(relation(_57801)), _57803 = _57801, relation(_57803)], (88 ^ _55260) ^ [_58076, _58078] : [-(antisymmetric(_58076)), _58078 = _58076, antisymmetric(_58078)], (154 ^ _55260) ^ [_60404, _60406] : [in(_60406, _60404), in(_60404, _60406)], (160 ^ _55260) ^ [_60601] : [empty(_60601), -(function(_60601))], (166 ^ _55260) ^ [_60787] : [177 ^ _55260 : [(178 ^ _55260) ^ [] : [-(relation(_60787))], (180 ^ _55260) ^ [] : [-(function(_60787))], (182 ^ _55260) ^ [] : [-(one_to_one(_60787))]], relation(_60787), empty(_60787), function(_60787)], (184 ^ _55260) ^ [_61279, _61281] : [-(unordered_pair(_61281, _61279) = unordered_pair(_61279, _61281))], (186 ^ _55260) ^ [_61379, _61381] : [-(set_intersection2(_61381, _61379) = set_intersection2(_61379, _61381))], (188 ^ _55260) ^ [_61479, _61481] : [-(ordered_pair(_61481, _61479) = unordered_pair(unordered_pair(_61481, _61479), singleton(_61481)))], (190 ^ _55260) ^ [_61585] : [relation(_61585), 193 ^ _55260 : [(194 ^ _55260) ^ [_61704] : [-(relation_restriction(_61585, _61704) = set_intersection2(_61585, cartesian_product2(_61704, _61704)))]]], (196 ^ _55260) ^ [] : [true___, -(true___)], (202 ^ _55260) ^ [] : [true___, -(true___)], (208 ^ _55260) ^ [] : [true___, -(true___)], (214 ^ _55260) ^ [_62184, _62186] : [relation(_62186), -(relation(relation_restriction(_62186, _62184)))], (220 ^ _55260) ^ [] : [true___, -(true___)], (226 ^ _55260) ^ [] : [true___, -(true___)], (232 ^ _55260) ^ [] : [true___, -(true___)], (238 ^ _55260) ^ [] : [true___, -(true___)], (245 ^ _55260) ^ [_62882] : [-(element(243 ^ [_62882], _62882))], (247 ^ _55260) ^ [] : [-(empty(empty_set))], (249 ^ _55260) ^ [_63031, _63033] : [empty(ordered_pair(_63033, _63031))], (251 ^ _55260) ^ [_63127, _63129] : [-(set_intersection2(_63129, _63129) = _63129)], (253 ^ _55260) ^ [_63225] : [relation(_63225), 256 ^ _55260 : [(271 ^ _55260) ^ [] : [274 ^ _55260 : [(275 ^ _55260) ^ [] : [-(in(ordered_pair(272 ^ [_63225], 273 ^ [_63225]), _63225))], (277 ^ _55260) ^ [] : [-(in(ordered_pair(273 ^ [_63225], 272 ^ [_63225]), _63225))], (279 ^ _55260) ^ [] : [272 ^ [_63225] = 273 ^ [_63225]]], -(antisymmetric(_63225))], (257 ^ _55260) ^ [] : [antisymmetric(_63225), 260 ^ _55260 : [(261 ^ _55260) ^ [_63495, _63497] : [-(_63497 = _63495), in(ordered_pair(_63497, _63495), _63225), in(ordered_pair(_63495, _63497), _63225)]]]]], (284 ^ _55260) ^ [] : [-(relation(282 ^ []))], (286 ^ _55260) ^ [] : [-(function(282 ^ []))], (289 ^ _55260) ^ [] : [-(empty(287 ^ []))], (292 ^ _55260) ^ [] : [-(relation(290 ^ []))], (294 ^ _55260) ^ [] : [-(empty(290 ^ []))], (296 ^ _55260) ^ [] : [-(function(290 ^ []))], (299 ^ _55260) ^ [] : [empty(297 ^ [])], (302 ^ _55260) ^ [] : [-(relation(300 ^ []))], (304 ^ _55260) ^ [] : [-(function(300 ^ []))], (306 ^ _55260) ^ [] : [-(one_to_one(300 ^ []))], (308 ^ _55260) ^ [_65021, _65023, _65025] : [relation(_65021), 311 ^ _55260 : [(312 ^ _55260) ^ [] : [in(_65025, relation_restriction(_65021, _65023)), 315 ^ _55260 : [(316 ^ _55260) ^ [] : [-(in(_65025, _65021))], (318 ^ _55260) ^ [] : [-(in(_65025, cartesian_product2(_65023, _65023)))]]], (320 ^ _55260) ^ [] : [-(in(_65025, relation_restriction(_65021, _65023))), in(_65025, _65021), in(_65025, cartesian_product2(_65023, _65023))]]], (330 ^ _55260) ^ [_65677, _65679] : [in(_65679, _65677), -(element(_65679, _65677))], (336 ^ _55260) ^ [_65858] : [-(set_intersection2(_65858, empty_set) = empty_set)], (338 ^ _55260) ^ [_65968, _65970] : [element(_65970, _65968), -(empty(_65968)), -(in(_65970, _65968))], (348 ^ _55260) ^ [_66252] : [empty(_66252), -(_66252 = empty_set)], (354 ^ _55260) ^ [_66454, _66456] : [in(_66456, _66454), empty(_66454)], (360 ^ _55260) ^ [_66641, _66643] : [empty(_66643), -(_66643 = _66641), empty(_66641)]], input).
% 3.96/4.48 ncf('1',plain,[antisymmetric(relation_restriction(370 ^ [], 369 ^ []))],start(376 ^ 0)).
% 3.96/4.48 ncf('1.1',plain,[-(antisymmetric(relation_restriction(370 ^ [], 369 ^ []))), 275 : -(in(ordered_pair(272 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), relation_restriction(370 ^ [], 369 ^ []))), 271 : relation(relation_restriction(370 ^ [], 369 ^ []))],extension(253 ^ 1,bind([[_63225], [relation_restriction(370 ^ [], 369 ^ [])]]))).
% 3.96/4.48 ncf('1.1.1',plain,[in(ordered_pair(272 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), relation_restriction(370 ^ [], 369 ^ [])), 316 : -(in(ordered_pair(272 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 370 ^ [])), 312 : relation(370 ^ [])],extension(308 ^ 6,bind([[_65021, _65023, _65025], [370 ^ [], 369 ^ [], ordered_pair(272 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])])]]))).
% 3.96/4.48 ncf('1.1.1.1',plain,[in(ordered_pair(272 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 370 ^ []), 261 : -(272 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 261 : in(ordered_pair(273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 370 ^ []), 261 : antisymmetric(370 ^ []), 257 : relation(370 ^ [])],extension(253 ^ 11,bind([[_63225, _63495, _63497], [370 ^ [], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]]]))).
% 3.96/4.48 ncf('1.1.1.1.1',plain,[272 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])], -(272 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 273 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])]],extension(10 ^ 16,bind([[_55715, _55717, _55719], [273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]]]))).
% 3.96/4.48 ncf('1.1.1.1.1.1',plain,[272 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 271 : -(antisymmetric(relation_restriction(370 ^ [], 369 ^ []))), 271 : relation(relation_restriction(370 ^ [], 369 ^ []))],extension(253 ^ 17,bind([[_63225], [relation_restriction(370 ^ [], 369 ^ [])]]))).
% 3.96/4.48 ncf('1.1.1.1.1.1.1',plain,[antisymmetric(relation_restriction(370 ^ [], 369 ^ []))],reduction('1')).
% 3.96/4.48 ncf('1.1.1.1.1.1.2',plain,[-(relation(relation_restriction(370 ^ [], 369 ^ []))), relation(370 ^ [])],extension(214 ^ 18,bind([[_62184, _62186], [369 ^ [], 370 ^ []]]))).
% 3.96/4.48 ncf('1.1.1.1.1.1.2.1',plain,[-(relation(370 ^ []))],extension(372 ^ 19)).
% 3.96/4.48 ncf('1.1.1.1.1.2',plain,[-(273 ^ [relation_restriction(370 ^ [], 369 ^ [])] = 273 ^ [relation_restriction(370 ^ [], 369 ^ [])])],extension(2 ^ 17,bind([[_55404], [273 ^ [relation_restriction(370 ^ [], 369 ^ [])]]]))).
% 3.96/4.48 ncf('1.1.1.1.2',plain,[-(in(ordered_pair(273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]), 370 ^ [])), 312 : in(ordered_pair(273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]), relation_restriction(370 ^ [], 369 ^ [])), 312 : relation(370 ^ [])],extension(308 ^ 16,bind([[_65021, _65023, _65025], [370 ^ [], 369 ^ [], ordered_pair(273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])])]]))).
% 3.96/4.48 ncf('1.1.1.1.2.1',plain,[-(in(ordered_pair(273 ^ [relation_restriction(370 ^ [], 369 ^ [])], 272 ^ [relation_restriction(370 ^ [], 369 ^ [])]), relation_restriction(370 ^ [], 369 ^ []))), 271 : -(antisymmetric(relation_restriction(370 ^ [], 369 ^ []))), 271 : relation(relation_restriction(370 ^ [], 369 ^ []))],extension(253 ^ 19,bind([[_63225], [relation_restriction(370 ^ [], 369 ^ [])]]))).
% 3.96/4.48 ncf('1.1.1.1.2.1.1',plain,[antisymmetric(relation_restriction(370 ^ [], 369 ^ []))],reduction('1')).
% 3.96/4.48 ncf('1.1.1.1.2.1.2',plain,[-(relation(relation_restriction(370 ^ [], 369 ^ []))), relation(370 ^ [])],extension(214 ^ 20,bind([[_62184, _62186], [369 ^ [], 370 ^ []]]))).
% 3.96/4.48 ncf('1.1.1.1.2.1.2.1',plain,[-(relation(370 ^ []))],extension(372 ^ 21)).
% 3.96/4.48 ncf('1.1.1.1.2.2',plain,[-(relation(370 ^ []))],extension(372 ^ 17)).
% 3.96/4.48 ncf('1.1.1.1.3',plain,[-(antisymmetric(370 ^ []))],extension(374 ^ 14)).
% 3.96/4.48 ncf('1.1.1.1.4',plain,[-(relation(370 ^ []))],extension(372 ^ 12)).
% 3.96/4.48 ncf('1.1.1.2',plain,[-(relation(370 ^ []))],extension(372 ^ 7)).
% 3.96/4.48 ncf('1.1.2',plain,[-(relation(relation_restriction(370 ^ [], 369 ^ []))), relation(370 ^ [])],extension(214 ^ 2,bind([[_62184, _62186], [369 ^ [], 370 ^ []]]))).
% 3.96/4.48 ncf('1.1.2.1',plain,[-(relation(370 ^ []))],extension(372 ^ 3)).
% 3.96/4.48 %-----------------------------------------------------
% 3.96/4.48 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------