%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU241+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:50 EDT 2023
% Result : Theorem 0.42s 1.37s
% Output : Proof 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SEU241+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n012.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 13:16:02 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.42/1.37
% 0.42/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.42/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/1.37 %-----------------------------------------------------
% 0.42/1.37 ncf(matrix, plain, [(419 ^ _64675) ^ [] : [-(relation(417 ^ []))], (421 ^ _64675) ^ [] : [422 ^ _64675 : [(423 ^ _64675) ^ [] : [-(antisymmetric(417 ^ []))], (427 ^ _64675) ^ [] : [-(in(ordered_pair(424 ^ [], 425 ^ []), 417 ^ []))], (429 ^ _64675) ^ [] : [-(in(ordered_pair(425 ^ [], 424 ^ []), 417 ^ []))], (431 ^ _64675) ^ [] : [424 ^ [] = 425 ^ []]], 432 ^ _64675 : [(443 ^ _64675) ^ [] : [antisymmetric(417 ^ [])], (433 ^ _64675) ^ [_78592, _78594] : [-(_78594 = _78592), in(ordered_pair(_78594, _78592), 417 ^ []), in(ordered_pair(_78592, _78594), 417 ^ [])]]], (112 ^ _64675) ^ [_68278, _68280, _68282, _68284] : [-(unordered_pair(_68284, _68280) = unordered_pair(_68282, _68278)), _68284 = _68282, _68280 = _68278], (122 ^ _64675) ^ [_68609, _68611] : [_68611 = _68609, -(singleton(_68611) = singleton(_68609))], (128 ^ _64675) ^ [_68827, _68829] : [_68829 = _68827, -(relation_dom(_68829) = relation_dom(_68827))], (134 ^ _64675) ^ [_69045, _69047] : [_69047 = _69045, -(relation_rng(_69047) = relation_rng(_69045))], (140 ^ _64675) ^ [_69291, _69293, _69295, _69297] : [-(set_union2(_69297, _69293) = set_union2(_69295, _69291)), _69297 = _69295, _69293 = _69291], (150 ^ _64675) ^ [_69622, _69624] : [_69624 = _69622, -(relation_field(_69624) = relation_field(_69622))], (156 ^ _64675) ^ [_69848, _69850, _69852, _69854] : [-(ordered_pair(_69854, _69850) = ordered_pair(_69852, _69848)), _69854 = _69852, _69850 = _69848], (2 ^ _64675) ^ [_64819] : [-(_64819 = _64819)], (4 ^ _64675) ^ [_64926, _64928] : [_64928 = _64926, -(_64926 = _64928)], (10 ^ _64675) ^ [_65130, _65132, _65134] : [-(_65134 = _65130), _65134 = _65132, _65132 = _65130], (20 ^ _64675) ^ [_65471, _65473, _65475, _65477] : [-(is_antisymmetric_in(_65475, _65471)), is_antisymmetric_in(_65477, _65473), _65477 = _65475, _65473 = _65471], (34 ^ _64675) ^ [_65887, _65889] : [-(function(_65887)), _65889 = _65887, function(_65889)], (44 ^ _64675) ^ [_66182, _66184] : [-(one_to_one(_66182)), _66184 = _66182, one_to_one(_66184)], (54 ^ _64675) ^ [_66505, _66507, _66509, _66511] : [-(element(_66509, _66505)), element(_66511, _66507), _66511 = _66509, _66507 = _66505], (68 ^ _64675) ^ [_66921, _66923] : [-(empty(_66921)), _66923 = _66921, empty(_66923)], (78 ^ _64675) ^ [_67216, _67218] : [-(relation(_67216)), _67218 = _67216, relation(_67218)], (88 ^ _64675) ^ [_67511, _67513] : [-(antisymmetric(_67511)), _67513 = _67511, antisymmetric(_67513)], (98 ^ _64675) ^ [_67814, _67816, _67818, _67820] : [-(in(_67818, _67814)), in(_67820, _67816), _67820 = _67818, _67816 = _67814], (166 ^ _64675) ^ [_70205, _70207] : [in(_70207, _70205), in(_70205, _70207)], (172 ^ _64675) ^ [_70402] : [empty(_70402), -(function(_70402))], (178 ^ _64675) ^ [_70588] : [189 ^ _64675 : [(190 ^ _64675) ^ [] : [-(relation(_70588))], (192 ^ _64675) ^ [] : [-(function(_70588))], (194 ^ _64675) ^ [] : [-(one_to_one(_70588))]], relation(_70588), empty(_70588), function(_70588)], (196 ^ _64675) ^ [_71080, _71082] : [-(unordered_pair(_71082, _71080) = unordered_pair(_71080, _71082))], (198 ^ _64675) ^ [_71180, _71182] : [-(set_union2(_71182, _71180) = set_union2(_71180, _71182))], (200 ^ _64675) ^ [_71281] : [relation(_71281), 203 ^ _64675 : [(204 ^ _64675) ^ [] : [antisymmetric(_71281), -(is_antisymmetric_in(_71281, relation_field(_71281)))], (210 ^ _64675) ^ [] : [is_antisymmetric_in(_71281, relation_field(_71281)), -(antisymmetric(_71281))]]], (216 ^ _64675) ^ [_71712] : [relation(_71712), 219 ^ _64675 : [(242 ^ _64675) ^ [_72580] : [245 ^ _64675 : [(246 ^ _64675) ^ [] : [-(in(243 ^ [_71712, _72580], _72580))], (248 ^ _64675) ^ [] : [-(in(244 ^ [_71712, _72580], _72580))], (250 ^ _64675) ^ [] : [-(in(ordered_pair(243 ^ [_71712, _72580], 244 ^ [_71712, _72580]), _71712))], (252 ^ _64675) ^ [] : [-(in(ordered_pair(244 ^ [_71712, _72580], 243 ^ [_71712, _72580]), _71712))], (254 ^ _64675) ^ [] : [243 ^ [_71712, _72580] = 244 ^ [_71712, _72580]]], -(is_antisymmetric_in(_71712, _72580))], (220 ^ _64675) ^ [_71912] : [is_antisymmetric_in(_71712, _71912), 223 ^ _64675 : [(224 ^ _64675) ^ [_72094, _72096] : [-(_72096 = _72094), in(_72096, _71912), in(_72094, _71912), in(ordered_pair(_72096, _72094), _71712), in(ordered_pair(_72094, _72096), _71712)]]]]], (258 ^ _64675) ^ [_73348, _73350] : [-(ordered_pair(_73350, _73348) = unordered_pair(unordered_pair(_73350, _73348), singleton(_73350)))], (260 ^ _64675) ^ [_73454] : [relation(_73454), -(relation_field(_73454) = set_union2(relation_dom(_73454), relation_rng(_73454)))], (266 ^ _64675) ^ [] : [true___, -(true___)], (272 ^ _64675) ^ [] : [true___, -(true___)], (278 ^ _64675) ^ [] : [true___, -(true___)], (284 ^ _64675) ^ [] : [true___, -(true___)], (290 ^ _64675) ^ [] : [true___, -(true___)], (296 ^ _64675) ^ [] : [true___, -(true___)], (302 ^ _64675) ^ [] : [true___, -(true___)], (308 ^ _64675) ^ [] : [true___, -(true___)], (314 ^ _64675) ^ [] : [true___, -(true___)], (321 ^ _64675) ^ [_74755] : [-(element(319 ^ [_74755], _74755))], (323 ^ _64675) ^ [] : [-(empty(empty_set))], (325 ^ _64675) ^ [_74904, _74906] : [empty(ordered_pair(_74906, _74904))], (327 ^ _64675) ^ [_75015, _75017] : [-(empty(_75017)), empty(set_union2(_75017, _75015))], (333 ^ _64675) ^ [_75231, _75233] : [-(empty(_75233)), empty(set_union2(_75231, _75233))], (339 ^ _64675) ^ [_75432, _75434] : [-(set_union2(_75434, _75434) = _75434)], (342 ^ _64675) ^ [] : [-(relation(340 ^ []))], (344 ^ _64675) ^ [] : [-(function(340 ^ []))], (347 ^ _64675) ^ [] : [-(empty(345 ^ []))], (350 ^ _64675) ^ [] : [-(relation(348 ^ []))], (352 ^ _64675) ^ [] : [-(empty(348 ^ []))], (354 ^ _64675) ^ [] : [-(function(348 ^ []))], (357 ^ _64675) ^ [] : [empty(355 ^ [])], (360 ^ _64675) ^ [] : [-(relation(358 ^ []))], (362 ^ _64675) ^ [] : [-(function(358 ^ []))], (364 ^ _64675) ^ [] : [-(one_to_one(358 ^ []))], (366 ^ _64675) ^ [_76261] : [-(set_union2(_76261, empty_set) = _76261)], (368 ^ _64675) ^ [_76371, _76373] : [in(_76373, _76371), -(element(_76373, _76371))], (374 ^ _64675) ^ [_76581, _76583] : [element(_76583, _76581), -(empty(_76581)), -(in(_76583, _76581))], (384 ^ _64675) ^ [_76893, _76895, _76897] : [relation(_76893), in(ordered_pair(_76897, _76895), _76893), 391 ^ _64675 : [(392 ^ _64675) ^ [] : [-(in(_76897, relation_field(_76893)))], (394 ^ _64675) ^ [] : [-(in(_76895, relation_field(_76893)))]]], (396 ^ _64675) ^ [_77277] : [empty(_77277), -(_77277 = empty_set)], (402 ^ _64675) ^ [_77479, _77481] : [in(_77481, _77479), empty(_77479)], (408 ^ _64675) ^ [_77666, _77668] : [empty(_77668), -(_77668 = _77666), empty(_77666)]], input).
% 0.42/1.37 ncf('1',plain,[431 : 424 ^ [] = 425 ^ [], 443 : antisymmetric(417 ^ [])],start(421 ^ 0)).
% 0.42/1.37 ncf('1.1',plain,[-(424 ^ [] = 425 ^ []), 425 ^ [] = 424 ^ []],extension(4 ^ 3,bind([[_64926, _64928], [424 ^ [], 425 ^ []]]))).
% 0.42/1.37 ncf('1.1.1',plain,[-(425 ^ [] = 424 ^ []), 224 : in(425 ^ [], relation_field(417 ^ [])), 224 : in(424 ^ [], relation_field(417 ^ [])), 224 : in(ordered_pair(425 ^ [], 424 ^ []), 417 ^ []), 224 : in(ordered_pair(424 ^ [], 425 ^ []), 417 ^ []), 224 : is_antisymmetric_in(417 ^ [], relation_field(417 ^ [])), 220 : relation(417 ^ [])],extension(216 ^ 4,bind([[_71712, _71912, _72094, _72096], [417 ^ [], relation_field(417 ^ []), 424 ^ [], 425 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.1',plain,[-(in(425 ^ [], relation_field(417 ^ []))), relation(417 ^ []), in(ordered_pair(425 ^ [], 424 ^ []), 417 ^ [])],extension(384 ^ 9,bind([[_76893, _76895, _76897], [417 ^ [], 424 ^ [], 425 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.1.1',plain,[-(relation(417 ^ []))],extension(419 ^ 10)).
% 0.42/1.37 ncf('1.1.1.1.2',plain,[-(in(ordered_pair(425 ^ [], 424 ^ []), 417 ^ []))],extension(429 ^ 10)).
% 0.42/1.37 ncf('1.1.1.2',plain,[-(in(424 ^ [], relation_field(417 ^ []))), relation(417 ^ []), in(ordered_pair(424 ^ [], 425 ^ []), 417 ^ [])],extension(384 ^ 9,bind([[_76893, _76895, _76897], [417 ^ [], 425 ^ [], 424 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.2.1',plain,[-(relation(417 ^ []))],extension(419 ^ 10)).
% 0.42/1.37 ncf('1.1.1.2.2',plain,[-(in(ordered_pair(424 ^ [], 425 ^ []), 417 ^ []))],extension(427 ^ 10)).
% 0.42/1.37 ncf('1.1.1.3',plain,[-(in(ordered_pair(425 ^ [], 424 ^ []), 417 ^ []))],extension(429 ^ 9)).
% 0.42/1.37 ncf('1.1.1.4',plain,[-(in(ordered_pair(424 ^ [], 425 ^ []), 417 ^ []))],extension(427 ^ 9)).
% 0.42/1.37 ncf('1.1.1.5',plain,[-(is_antisymmetric_in(417 ^ [], relation_field(417 ^ []))), is_antisymmetric_in(417 ^ [], relation_field(417 ^ [])), 417 ^ [] = 417 ^ [], relation_field(417 ^ []) = relation_field(417 ^ [])],extension(20 ^ 7,bind([[_65471, _65473, _65475, _65477], [relation_field(417 ^ []), relation_field(417 ^ []), 417 ^ [], 417 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.5.1',plain,[-(is_antisymmetric_in(417 ^ [], relation_field(417 ^ []))), 204 : antisymmetric(417 ^ []), 204 : relation(417 ^ [])],extension(200 ^ 8,bind([[_71281], [417 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.5.1.1',plain,[-(antisymmetric(417 ^ []))],extension(423 ^ 11)).
% 0.42/1.37 ncf('1.1.1.5.1.2',plain,[-(relation(417 ^ []))],extension(419 ^ 9)).
% 0.42/1.37 ncf('1.1.1.5.2',plain,[-(417 ^ [] = 417 ^ [])],extension(2 ^ 8,bind([[_64819], [417 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.5.3',plain,[-(relation_field(417 ^ []) = relation_field(417 ^ [])), 417 ^ [] = 417 ^ []],extension(150 ^ 8,bind([[_69622, _69624], [417 ^ [], 417 ^ []]]))).
% 0.42/1.37 ncf('1.1.1.5.3.1',plain,[-(417 ^ [] = 417 ^ [])],lemmata('[1, 1, 1].x')).
% 0.42/1.37 ncf('1.1.1.6',plain,[-(relation(417 ^ []))],extension(419 ^ 5)).
% 0.42/1.37 ncf('1.2',plain,[-(antisymmetric(417 ^ [])), 210 : is_antisymmetric_in(417 ^ [], relation_field(417 ^ [])), 210 : relation(417 ^ [])],extension(200 ^ 3,bind([[_71281], [417 ^ []]]))).
% 0.42/1.37 ncf('1.2.1',plain,[-(is_antisymmetric_in(417 ^ [], relation_field(417 ^ []))), 250 : -(in(ordered_pair(243 ^ [417 ^ [], relation_field(417 ^ [])], 244 ^ [417 ^ [], relation_field(417 ^ [])]), 417 ^ [])), 242 : relation(417 ^ [])],extension(216 ^ 6,bind([[_71712, _72580], [417 ^ [], relation_field(417 ^ [])]]))).
% 0.42/1.37 ncf('1.2.1.1',plain,[in(ordered_pair(243 ^ [417 ^ [], relation_field(417 ^ [])], 244 ^ [417 ^ [], relation_field(417 ^ [])]), 417 ^ []), -(243 ^ [417 ^ [], relation_field(417 ^ [])] = 244 ^ [417 ^ [], relation_field(417 ^ [])]), in(ordered_pair(244 ^ [417 ^ [], relation_field(417 ^ [])], 243 ^ [417 ^ [], relation_field(417 ^ [])]), 417 ^ [])],extension(433 ^ 11,bind([[_78592, _78594], [244 ^ [417 ^ [], relation_field(417 ^ [])], 243 ^ [417 ^ [], relation_field(417 ^ [])]]]))).
% 0.42/1.37 ncf('1.2.1.1.1',plain,[243 ^ [417 ^ [], relation_field(417 ^ [])] = 244 ^ [417 ^ [], relation_field(417 ^ [])]],extension(254 ^ 12)).
% 0.42/1.37 ncf('1.2.1.1.2',plain,[-(in(ordered_pair(244 ^ [417 ^ [], relation_field(417 ^ [])], 243 ^ [417 ^ [], relation_field(417 ^ [])]), 417 ^ []))],extension(252 ^ 12)).
% 0.42/1.37 ncf('1.2.1.2',plain,[-(relation(417 ^ []))],extension(419 ^ 7)).
% 0.42/1.37 ncf('1.2.2',plain,[-(relation(417 ^ []))],extension(419 ^ 4)).
% 0.42/1.37 %-----------------------------------------------------
% 0.42/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------