%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU375+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:03:19 EDT 2023
% Result : Theorem 2.51s 3.44s
% Output : Proof 2.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU375+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu May 18 13:54:03 EDT 2023
% 0.12/0.32 % CPUTime :
% 2.51/3.44
% 2.51/3.44 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.51/3.44 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.51/3.44 %-----------------------------------------------------
% 2.51/3.44 ncf(matrix, plain, [(586 ^ _88023) ^ [] : [-(one_sorted_str(584 ^ []))], (589 ^ _88023) ^ [] : [empty_carrier(587 ^ [])], (591 ^ _88023) ^ [] : [-(net_str(587 ^ [], 584 ^ []))], (594 ^ _88023) ^ [] : [empty_carrier(592 ^ [])], (596 ^ _88023) ^ [] : [-(full_subnetstr(592 ^ [], 584 ^ [], 587 ^ []))], (598 ^ _88023) ^ [] : [-(subnetstr(592 ^ [], 584 ^ [], 587 ^ []))], (601 ^ _88023) ^ [] : [-(element(599 ^ [], the_carrier(587 ^ [])))], (604 ^ _88023) ^ [] : [-(element(602 ^ [], the_carrier(587 ^ [])))], (607 ^ _88023) ^ [] : [-(element(605 ^ [], the_carrier(592 ^ [])))], (610 ^ _88023) ^ [] : [-(element(608 ^ [], the_carrier(592 ^ [])))], (612 ^ _88023) ^ [] : [-(599 ^ [] = 605 ^ [])], (614 ^ _88023) ^ [] : [-(602 ^ [] = 608 ^ [])], (616 ^ _88023) ^ [] : [-(related(587 ^ [], 599 ^ [], 602 ^ []))], (618 ^ _88023) ^ [] : [related(592 ^ [], 605 ^ [], 608 ^ [])], (234 ^ _88023) ^ [_95527, _95529] : [_95529 = _95527, -(the_carrier(_95529) = the_carrier(_95527))], (2 ^ _88023) ^ [_88167] : [-(_88167 = _88167)], (4 ^ _88023) ^ [_88274, _88276] : [_88276 = _88274, -(_88274 = _88276)], (10 ^ _88023) ^ [_88478, _88480, _88482] : [-(_88482 = _88478), _88482 = _88480, _88480 = _88478], (20 ^ _88023) ^ [_88791, _88793] : [-(v1_yellow_3(_88791)), _88793 = _88791, v1_yellow_3(_88793)], (30 ^ _88023) ^ [_89086, _89088] : [-(one_to_one(_89086)), _89088 = _89086, one_to_one(_89088)], (40 ^ _88023) ^ [_89381, _89383] : [-(relation(_89381)), _89383 = _89381, relation(_89383)], (50 ^ _88023) ^ [_89676, _89678] : [-(relation_empty_yielding(_89676)), _89678 = _89676, relation_empty_yielding(_89678)], (60 ^ _88023) ^ [_89971, _89973] : [-(function(_89971)), _89973 = _89971, function(_89973)], (70 ^ _88023) ^ [_90266, _90268] : [-(rel_str(_90266)), _90268 = _90266, rel_str(_90268)], (80 ^ _88023) ^ [_90589, _90591, _90593, _90595] : [-(full_subrelstr(_90593, _90589)), full_subrelstr(_90595, _90591), _90595 = _90593, _90591 = _90589], (94 ^ _88023) ^ [_91033, _91035, _91037, _91039] : [-(subrelstr(_91037, _91033)), subrelstr(_91039, _91035), _91039 = _91037, _91035 = _91033], (108 ^ _88023) ^ [_91477, _91479, _91481, _91483] : [-(in(_91481, _91477)), in(_91483, _91479), _91483 = _91481, _91479 = _91477], (122 ^ _88023) ^ [_91893, _91895] : [-(empty(_91893)), _91895 = _91893, empty(_91895)], (132 ^ _88023) ^ [_92188, _92190] : [-(one_sorted_str(_92188)), _92190 = _92188, one_sorted_str(_92190)], (142 ^ _88023) ^ [_92511, _92513, _92515, _92517] : [-(net_str(_92515, _92511)), net_str(_92517, _92513), _92517 = _92515, _92513 = _92511], (156 ^ _88023) ^ [_92927, _92929] : [-(empty_carrier(_92927)), _92929 = _92927, empty_carrier(_92929)], (166 ^ _88023) ^ [_93278, _93280, _93282, _93284, _93286, _93288] : [-(full_subnetstr(_93286, _93282, _93278)), full_subnetstr(_93288, _93284, _93280), _93288 = _93286, _93284 = _93282, _93280 = _93278], (184 ^ _88023) ^ [_93887, _93889, _93891, _93893, _93895, _93897] : [-(subnetstr(_93895, _93891, _93887)), subnetstr(_93897, _93893, _93889), _93897 = _93895, _93893 = _93891, _93889 = _93887], (202 ^ _88023) ^ [_94468, _94470, _94472, _94474] : [-(element(_94472, _94468)), element(_94474, _94470), _94474 = _94472, _94470 = _94468], (216 ^ _88023) ^ [_94920, _94922, _94924, _94926, _94928, _94930] : [-(related(_94928, _94924, _94920)), related(_94930, _94926, _94922), _94930 = _94928, _94926 = _94924, _94922 = _94920], (240 ^ _88023) ^ [_95751, _95753] : [in(_95753, _95751), in(_95751, _95753)], (246 ^ _88023) ^ [_95948] : [empty(_95948), -(function(_95948))], (252 ^ _88023) ^ [_96134] : [empty(_96134), -(relation(_96134))], (258 ^ _88023) ^ [_96320] : [rel_str(_96320), empty_carrier(_96320), -(v1_yellow_3(_96320))], (268 ^ _88023) ^ [_96589] : [279 ^ _88023 : [(280 ^ _88023) ^ [] : [-(relation(_96589))], (282 ^ _88023) ^ [] : [-(function(_96589))], (284 ^ _88023) ^ [] : [-(one_to_one(_96589))]], relation(_96589), empty(_96589), function(_96589)], (286 ^ _88023) ^ [_97082] : [rel_str(_97082), -(v1_yellow_3(_97082)), empty_carrier(_97082)], (296 ^ _88023) ^ [_97355] : [one_sorted_str(_97355), 299 ^ _88023 : [(300 ^ _88023) ^ [_97511] : [net_str(_97511, _97355), 303 ^ _88023 : [(304 ^ _88023) ^ [_97664] : [subnetstr(_97664, _97355, _97511), 307 ^ _88023 : [(308 ^ _88023) ^ [] : [full_subnetstr(_97664, _97355, _97511), 311 ^ _88023 : [(312 ^ _88023) ^ [] : [-(full_subrelstr(_97664, _97511))], (314 ^ _88023) ^ [] : [-(subrelstr(_97664, _97511))]]], (316 ^ _88023) ^ [] : [-(full_subnetstr(_97664, _97355, _97511)), full_subrelstr(_97664, _97511), subrelstr(_97664, _97511)]]]]]]], (326 ^ _88023) ^ [] : [true___, -(true___)], (332 ^ _88023) ^ [_98428] : [rel_str(_98428), -(one_sorted_str(_98428))], (338 ^ _88023) ^ [] : [true___, -(true___)], (344 ^ _88023) ^ [_98733] : [one_sorted_str(_98733), 347 ^ _88023 : [(348 ^ _88023) ^ [_98863] : [net_str(_98863, _98733), -(rel_str(_98863))]]], (354 ^ _88023) ^ [] : [true___, -(true___)], (360 ^ _88023) ^ [_99183] : [rel_str(_99183), 363 ^ _88023 : [(364 ^ _88023) ^ [_99313] : [subrelstr(_99313, _99183), -(rel_str(_99313))]]], (370 ^ _88023) ^ [_99528, _99530] : [one_sorted_str(_99530), net_str(_99528, _99530), 377 ^ _88023 : [(378 ^ _88023) ^ [_99753] : [subnetstr(_99753, _99530, _99528), -(net_str(_99753, _99530))]]], (384 ^ _88023) ^ [] : [true___, -(true___)], (391 ^ _88023) ^ [] : [-(rel_str(389 ^ []))], (394 ^ _88023) ^ [] : [-(one_sorted_str(392 ^ []))], (396 ^ _88023) ^ [_100265] : [one_sorted_str(_100265), -(net_str(399 ^ [_100265], _100265))], (404 ^ _88023) ^ [_100528] : [-(element(402 ^ [_100528], _100528))], (406 ^ _88023) ^ [_100626] : [rel_str(_100626), -(subrelstr(409 ^ [_100626], _100626))], (413 ^ _88023) ^ [_100879, _100881] : [-(subnetstr(420 ^ [_100879, _100881], _100881, _100879)), one_sorted_str(_100881), net_str(_100879, _100881)], (424 ^ _88023) ^ [] : [-(empty(empty_set))], (426 ^ _88023) ^ [] : [-(relation(empty_set))], (428 ^ _88023) ^ [] : [-(relation_empty_yielding(empty_set))], (430 ^ _88023) ^ [_101385] : [empty(the_carrier(_101385)), -(empty_carrier(_101385)), one_sorted_str(_101385)], (440 ^ _88023) ^ [] : [-(empty(empty_set))], (442 ^ _88023) ^ [] : [-(relation(empty_set))], (445 ^ _88023) ^ [] : [-(relation(443 ^ []))], (447 ^ _88023) ^ [] : [-(function(443 ^ []))], (450 ^ _88023) ^ [] : [-(relation(448 ^ []))], (452 ^ _88023) ^ [] : [-(relation_empty_yielding(448 ^ []))], (454 ^ _88023) ^ [] : [-(function(448 ^ []))], (457 ^ _88023) ^ [] : [-(empty(455 ^ []))], (459 ^ _88023) ^ [] : [-(relation(455 ^ []))], (462 ^ _88023) ^ [] : [-(relation(460 ^ []))], (464 ^ _88023) ^ [] : [-(empty(460 ^ []))], (466 ^ _88023) ^ [] : [-(function(460 ^ []))], (469 ^ _88023) ^ [] : [empty(467 ^ [])], (471 ^ _88023) ^ [] : [-(relation(467 ^ []))], (474 ^ _88023) ^ [] : [-(relation(472 ^ []))], (476 ^ _88023) ^ [] : [-(function(472 ^ []))], (478 ^ _88023) ^ [] : [-(one_to_one(472 ^ []))], (481 ^ _88023) ^ [] : [-(relation(479 ^ []))], (483 ^ _88023) ^ [] : [-(relation_empty_yielding(479 ^ []))], (486 ^ _88023) ^ [] : [-(one_sorted_str(484 ^ []))], (488 ^ _88023) ^ [] : [empty_carrier(484 ^ [])], (491 ^ _88023) ^ [] : [-(relation(489 ^ []))], (493 ^ _88023) ^ [] : [-(relation_empty_yielding(489 ^ []))], (495 ^ _88023) ^ [] : [-(function(489 ^ []))], (497 ^ _88023) ^ [_103367, _103369] : [in(_103369, _103367), -(element(_103369, _103367))], (503 ^ _88023) ^ [_103577, _103579] : [element(_103579, _103577), -(empty(_103577)), -(in(_103579, _103577))], (563 ^ _88023) ^ [_105807] : [empty(_105807), -(_105807 = empty_set)], (569 ^ _88023) ^ [_106009, _106011] : [in(_106011, _106009), empty(_106009)], (575 ^ _88023) ^ [_106196, _106198] : [empty(_106198), -(_106198 = _106196), empty(_106196)], (513 ^ _88023) ^ [_103861] : [rel_str(_103861), 516 ^ _88023 : [(517 ^ _88023) ^ [_104086] : [full_subrelstr(_104086, _103861), subrelstr(_104086, _103861), 524 ^ _88023 : [(525 ^ _88023) ^ [_104391] : [element(_104391, the_carrier(_103861)), 528 ^ _88023 : [(529 ^ _88023) ^ [_104604] : [element(_104604, the_carrier(_103861)), 532 ^ _88023 : [(533 ^ _88023) ^ [_104810] : [element(_104810, the_carrier(_104086)), 536 ^ _88023 : [(537 ^ _88023) ^ [_105009] : [element(_105009, the_carrier(_104086)), -(related(_104086, _104810, _105009)), _104810 = _104391, _105009 = _104604, related(_103861, _104391, _104604), in(_104810, the_carrier(_104086)), in(_105009, the_carrier(_104086))]]]]]]]]]]]], input).
% 2.51/3.44 ncf('1',plain,[empty_carrier(592 ^ [])],start(594 ^ 0)).
% 2.51/3.44 ncf('1.1',plain,[-(empty_carrier(592 ^ [])), empty(the_carrier(592 ^ [])), one_sorted_str(592 ^ [])],extension(430 ^ 1,bind([[_101385], [592 ^ []]]))).
% 2.51/3.44 ncf('1.1.1',plain,[-(empty(the_carrier(592 ^ []))), element(605 ^ [], the_carrier(592 ^ [])), -(in(605 ^ [], the_carrier(592 ^ [])))],extension(503 ^ 2,bind([[_103577, _103579], [the_carrier(592 ^ []), 605 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.1',plain,[-(element(605 ^ [], the_carrier(592 ^ [])))],extension(607 ^ 3)).
% 2.51/3.44 ncf('1.1.1.2',plain,[in(605 ^ [], the_carrier(592 ^ [])), 537 : element(608 ^ [], the_carrier(592 ^ [])), 537 : -(related(592 ^ [], 605 ^ [], 608 ^ [])), 537 : 605 ^ [] = 599 ^ [], 537 : 608 ^ [] = 602 ^ [], 537 : related(587 ^ [], 599 ^ [], 602 ^ []), 537 : in(608 ^ [], the_carrier(592 ^ [])), 537 : element(605 ^ [], the_carrier(592 ^ [])), 533 : element(602 ^ [], the_carrier(587 ^ [])), 529 : element(599 ^ [], the_carrier(587 ^ [])), 525 : full_subrelstr(592 ^ [], 587 ^ []), 525 : subrelstr(592 ^ [], 587 ^ []), 517 : rel_str(587 ^ [])],extension(513 ^ 3,bind([[_103861, _104086, _104391, _104604, _104810, _105009], [587 ^ [], 592 ^ [], 599 ^ [], 602 ^ [], 605 ^ [], 608 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.1',plain,[-(element(608 ^ [], the_carrier(592 ^ [])))],extension(610 ^ 14)).
% 2.51/3.44 ncf('1.1.1.2.2',plain,[related(592 ^ [], 605 ^ [], 608 ^ [])],extension(618 ^ 14)).
% 2.51/3.44 ncf('1.1.1.2.3',plain,[-(605 ^ [] = 599 ^ []), 599 ^ [] = 605 ^ []],extension(4 ^ 14,bind([[_88274, _88276], [605 ^ [], 599 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.3.1',plain,[-(599 ^ [] = 605 ^ [])],extension(612 ^ 15)).
% 2.51/3.44 ncf('1.1.1.2.4',plain,[-(608 ^ [] = 602 ^ []), 602 ^ [] = 608 ^ []],extension(4 ^ 14,bind([[_88274, _88276], [608 ^ [], 602 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.4.1',plain,[-(602 ^ [] = 608 ^ [])],extension(614 ^ 15)).
% 2.51/3.44 ncf('1.1.1.2.5',plain,[-(related(587 ^ [], 599 ^ [], 602 ^ []))],extension(616 ^ 14)).
% 2.51/3.44 ncf('1.1.1.2.6',plain,[-(in(608 ^ [], the_carrier(592 ^ []))), element(608 ^ [], the_carrier(592 ^ [])), -(empty(the_carrier(592 ^ [])))],extension(503 ^ 14,bind([[_103577, _103579], [the_carrier(592 ^ []), 608 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.6.1',plain,[-(element(608 ^ [], the_carrier(592 ^ [])))],lemmata('[1, 1, 1].x')).
% 2.51/3.44 ncf('1.1.1.2.6.2',plain,[empty(the_carrier(592 ^ []))],reduction('1.1')).
% 2.51/3.44 ncf('1.1.1.2.7',plain,[-(element(605 ^ [], the_carrier(592 ^ [])))],lemmata('[1, 1].x')).
% 2.51/3.44 ncf('1.1.1.2.8',plain,[-(element(602 ^ [], the_carrier(587 ^ [])))],extension(604 ^ 10)).
% 2.51/3.44 ncf('1.1.1.2.9',plain,[-(element(599 ^ [], the_carrier(587 ^ [])))],extension(601 ^ 8)).
% 2.51/3.44 ncf('1.1.1.2.10',plain,[-(full_subrelstr(592 ^ [], 587 ^ [])), 308 : full_subnetstr(592 ^ [], 584 ^ [], 587 ^ []), 308 : subnetstr(592 ^ [], 584 ^ [], 587 ^ []), 304 : net_str(587 ^ [], 584 ^ []), 300 : one_sorted_str(584 ^ [])],extension(296 ^ 6,bind([[_97355, _97511, _97664], [584 ^ [], 587 ^ [], 592 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.10.1',plain,[-(full_subnetstr(592 ^ [], 584 ^ [], 587 ^ []))],extension(596 ^ 13)).
% 2.51/3.44 ncf('1.1.1.2.10.2',plain,[-(subnetstr(592 ^ [], 584 ^ [], 587 ^ []))],extension(598 ^ 11)).
% 2.51/3.44 ncf('1.1.1.2.10.3',plain,[-(net_str(587 ^ [], 584 ^ []))],extension(591 ^ 9)).
% 2.51/3.44 ncf('1.1.1.2.10.4',plain,[-(one_sorted_str(584 ^ []))],extension(586 ^ 7)).
% 2.51/3.44 ncf('1.1.1.2.11',plain,[-(subrelstr(592 ^ [], 587 ^ [])), 308 : full_subnetstr(592 ^ [], 584 ^ [], 587 ^ []), 308 : subnetstr(592 ^ [], 584 ^ [], 587 ^ []), 304 : net_str(587 ^ [], 584 ^ []), 300 : one_sorted_str(584 ^ [])],extension(296 ^ 6,bind([[_97355, _97511, _97664], [584 ^ [], 587 ^ [], 592 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.11.1',plain,[-(full_subnetstr(592 ^ [], 584 ^ [], 587 ^ []))],extension(596 ^ 13)).
% 2.51/3.44 ncf('1.1.1.2.11.2',plain,[-(subnetstr(592 ^ [], 584 ^ [], 587 ^ []))],extension(598 ^ 11)).
% 2.51/3.44 ncf('1.1.1.2.11.3',plain,[-(net_str(587 ^ [], 584 ^ []))],extension(591 ^ 9)).
% 2.51/3.44 ncf('1.1.1.2.11.4',plain,[-(one_sorted_str(584 ^ []))],extension(586 ^ 7)).
% 2.51/3.44 ncf('1.1.1.2.12',plain,[-(rel_str(587 ^ [])), 348 : net_str(587 ^ [], 584 ^ []), 348 : one_sorted_str(584 ^ [])],extension(344 ^ 4,bind([[_98733, _98863], [584 ^ [], 587 ^ []]]))).
% 2.51/3.44 ncf('1.1.1.2.12.1',plain,[-(net_str(587 ^ [], 584 ^ []))],extension(591 ^ 7)).
% 2.51/3.44 ncf('1.1.1.2.12.2',plain,[-(one_sorted_str(584 ^ []))],extension(586 ^ 5)).
% 2.51/3.44 ncf('1.1.2',plain,[-(one_sorted_str(592 ^ [])), rel_str(592 ^ [])],extension(332 ^ 2,bind([[_98428], [592 ^ []]]))).
% 2.51/3.44 ncf('1.1.2.1',plain,[-(rel_str(592 ^ [])), 348 : net_str(592 ^ [], 584 ^ []), 348 : one_sorted_str(584 ^ [])],extension(344 ^ 3,bind([[_98733, _98863], [584 ^ [], 592 ^ []]]))).
% 2.51/3.44 ncf('1.1.2.1.1',plain,[-(net_str(592 ^ [], 584 ^ [])), 378 : subnetstr(592 ^ [], 584 ^ [], 587 ^ []), 378 : one_sorted_str(584 ^ []), 378 : net_str(587 ^ [], 584 ^ [])],extension(370 ^ 6,bind([[_99528, _99530, _99753], [587 ^ [], 584 ^ [], 592 ^ []]]))).
% 2.51/3.44 ncf('1.1.2.1.1.1',plain,[-(subnetstr(592 ^ [], 584 ^ [], 587 ^ []))],extension(598 ^ 9)).
% 2.51/3.44 ncf('1.1.2.1.1.2',plain,[-(one_sorted_str(584 ^ []))],extension(586 ^ 7)).
% 2.51/3.44 ncf('1.1.2.1.1.3',plain,[-(net_str(587 ^ [], 584 ^ []))],extension(591 ^ 7)).
% 2.51/3.44 ncf('1.1.2.1.2',plain,[-(one_sorted_str(584 ^ []))],extension(586 ^ 4)).
% 2.51/3.44 %-----------------------------------------------------
% 2.51/3.44 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------