%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU374+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 43.41s 42.85s
% Output : Proof 43.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU374+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 12:49:48 EDT 2023
% 0.14/0.34 % CPUTime :
% 43.41/42.85
% 43.41/42.85 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 43.41/42.85 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.41/42.85 %-----------------------------------------------------
% 43.41/42.85 ncf(matrix, plain, [(788 ^ _155596) ^ [] : [-(element(786 ^ [], the_carrier(777 ^ [])))], (797 ^ _155596) ^ [] : [-(related(777 ^ [], 786 ^ [], 789 ^ []))], (785 ^ _155596) ^ [] : [-(element(783 ^ [], the_carrier(774 ^ [])))], (791 ^ _155596) ^ [] : [-(element(789 ^ [], the_carrier(777 ^ [])))], (773 ^ _155596) ^ [] : [-(one_sorted_str(771 ^ []))], (776 ^ _155596) ^ [] : [-(net_str(774 ^ [], 771 ^ []))], (779 ^ _155596) ^ [] : [-(subnetstr(777 ^ [], 771 ^ [], 774 ^ []))], (782 ^ _155596) ^ [] : [-(element(780 ^ [], the_carrier(774 ^ [])))], (793 ^ _155596) ^ [] : [-(780 ^ [] = 786 ^ [])], (795 ^ _155596) ^ [] : [-(783 ^ [] = 789 ^ [])], (799 ^ _155596) ^ [] : [related(774 ^ [], 780 ^ [], 783 ^ [])], !, (388 ^ _129833) ^ [] : [true___, -(true___)], (260 ^ _129833) ^ [_138352, _138354, _138356, _138358] : [-(cartesian_product2(_138358, _138354) = cartesian_product2(_138356, _138352)), _138358 = _138356, _138354 = _138352], (500 ^ _129833) ^ [] : [-(one_sorted_str(498 ^ []))], (588 ^ _129833) ^ [] : [-(relation(586 ^ []))], (434 ^ _129833) ^ [] : [true___, -(true___)], (534 ^ _129833) ^ [_147163, _147165] : [-(relation_of2_as_subset(532 ^ [_147163, _147165], _147165, _147163))], (662 ^ _129833) ^ [_151347, _151349] : [-(subset(_151349, _151349))], (128 ^ _129833) ^ [_134032, _134034] : [-(rel_str(_134032)), _134034 = _134032, rel_str(_134034)], (418 ^ _129833) ^ [] : [true___, -(true___)], (58 ^ _129833) ^ [_131780, _131782] : [-(relation_empty_yielding(_131780)), _131782 = _131780, relation_empty_yielding(_131782)], (20 ^ _129833) ^ [_130637, _130639, _130641, _130643, _130645, _130647] : [-(quasi_total(_130645, _130641, _130637)), quasi_total(_130647, _130643, _130639), _130647 = _130645, _130643 = _130641, _130639 = _130637], (328 ^ _129833) ^ [_140770, _140772, _140774] : [element(_140770, powerset(cartesian_product2(_140774, _140772))), -(relation(_140770))], (664 ^ _129833) ^ [_151456, _151458] : [in(_151458, _151456), -(element(_151458, _151456))], (166 ^ _129833) ^ [_135215, _135217] : [-(empty(_135215)), _135217 = _135215, empty(_135217)], (200 ^ _129833) ^ [_136305, _136307, _136309, _136311, _136313, _136315] : [-(subnetstr(_136313, _136309, _136305)), subnetstr(_136315, _136311, _136307), _136315 = _136313, _136311 = _136309, _136307 = _136305], (568 ^ _129833) ^ [] : [-(empty(empty_set))], (613 ^ _129833) ^ [] : [-(function(607 ^ []))], (650 ^ _129833) ^ [_150968, _150970, _150972] : [relation_of2_as_subset(_150968, _150972, _150970), -(relation_of2(_150968, _150972, _150970))], (304 ^ _129833) ^ [_139929, _139931] : [_139931 = _139929, -(the_carrier(_139931) = the_carrier(_139929))], (78 ^ _129833) ^ [_132426, _132428, _132430, _132432, _132434, _132436] : [-(relation_of2_as_subset(_132434, _132430, _132426)), relation_of2_as_subset(_132436, _132432, _132428), _132436 = _132434, _132432 = _132430, _132428 = _132426], (599 ^ _129833) ^ [_149184] : [-(empty(_149184)), 603 ^ _129833 : [(606 ^ _129833) ^ [] : [empty(602 ^ [_149184])], (604 ^ _129833) ^ [] : [-(element(602 ^ [_149184], powerset(_149184)))]]], (322 ^ _129833) ^ [_140556] : [empty(_140556), -(relation(_140556))], (670 ^ _129833) ^ [_151666, _151668] : [element(_151668, _151666), -(empty(_151666)), -(in(_151668, _151666))], (114 ^ _129833) ^ [_133616, _133618, _133620, _133622] : [-(subset(_133620, _133616)), subset(_133622, _133618), _133622 = _133620, _133618 = _133616], (595 ^ _129833) ^ [] : [-(empty(593 ^ []))], (762 ^ _129833) ^ [_154952, _154954] : [empty(_154954), -(_154954 = _154952), empty(_154952)], (2 ^ _129833) ^ [_129957] : [-(_129957 = _129957)], (482 ^ _129833) ^ [_145375, _145377] : [489 ^ _129833 : [(494 ^ _129833) ^ [] : [-(relation_of2_as_subset(the_mapping(_145377, _145375), the_carrier(_145375), the_carrier(_145377)))], (492 ^ _129833) ^ [] : [-(quasi_total(the_mapping(_145377, _145375), the_carrier(_145375), the_carrier(_145377)))], (490 ^ _129833) ^ [] : [-(function(the_mapping(_145377, _145375)))]], one_sorted_str(_145377), net_str(_145375, _145377)], (513 ^ _129833) ^ [_146428] : [-(element(511 ^ [_146428], _146428))], (232 ^ _129833) ^ [_137338, _137340, _137342, _137344, _137346, _137348] : [-(related(_137346, _137342, _137338)), related(_137348, _137344, _137340), _137348 = _137346, _137344 = _137342, _137340 = _137338], (497 ^ _129833) ^ [] : [-(rel_str(495 ^ []))], (152 ^ _129833) ^ [_134799, _134801, _134803, _134805] : [-(in(_134803, _134799)), in(_134805, _134801), _134805 = _134803, _134801 = _134799], (590 ^ _129833) ^ [] : [-(relation_empty_yielding(586 ^ []))], (446 ^ _129833) ^ [_144215] : [rel_str(_144215), 449 ^ _129833 : [(450 ^ _129833) ^ [_144345] : [subrelstr(_144345, _144215), -(rel_str(_144345))]]], (456 ^ _129833) ^ [_144560, _144562] : [one_sorted_str(_144562), net_str(_144560, _144562), 463 ^ _129833 : [(464 ^ _129833) ^ [_144785] : [subnetstr(_144785, _144562, _144560), -(net_str(_144785, _144562))]]], (352 ^ _129833) ^ [_141473] : [one_sorted_str(_141473), 355 ^ _129833 : [(356 ^ _129833) ^ [_141645] : [net_str(_141645, _141473), 359 ^ _129833 : [(360 ^ _129833) ^ [_141814] : [net_str(_141814, _141473), 363 ^ _129833 : [(372 ^ _129833) ^ [] : [-(subnetstr(_141814, _141473, _141645)), subrelstr(_141814, _141645), the_mapping(_141473, _141814) = relation_dom_restr_as_relation_of(the_carrier(_141645), the_carrier(_141473), the_mapping(_141473, _141645), the_carrier(_141814))], (364 ^ _129833) ^ [] : [subnetstr(_141814, _141473, _141645), 367 ^ _129833 : [(370 ^ _129833) ^ [] : [-(the_mapping(_141473, _141814) = relation_dom_restr_as_relation_of(the_carrier(_141645), the_carrier(_141473), the_mapping(_141473, _141645), the_carrier(_141814)))], (368 ^ _129833) ^ [] : [-(subrelstr(_141814, _141645))]]]]]]]]], (502 ^ _129833) ^ [_146021] : [one_sorted_str(_146021), -(net_str(505 ^ [_146021], _146021))], (702 ^ _129833) ^ [_152716, _152718, _152720] : [in(_152720, _152718), element(_152718, powerset(_152716)), empty(_152716)], (310 ^ _129833) ^ [_140173, _140175] : [in(_140175, _140173), in(_140173, _140175)], (538 ^ _129833) ^ [] : [-(relation(empty_set))], (618 ^ _129833) ^ [] : [-(relation(614 ^ []))], (522 ^ _129833) ^ [_146779, _146781] : [-(subnetstr(529 ^ [_146779, _146781], _146781, _146779)), one_sorted_str(_146781), net_str(_146779, _146781)], (750 ^ _129833) ^ [_154563] : [empty(_154563), -(_154563 = empty_set)], (424 ^ _129833) ^ [_143646] : [one_sorted_str(_143646), 427 ^ _129833 : [(428 ^ _129833) ^ [_143776] : [net_str(_143776, _143646), -(rel_str(_143776))]]], (638 ^ _129833) ^ [] : [-(relation(636 ^ []))], (623 ^ _129833) ^ [_149977] : [-(empty(619 ^ [_149977]))], (572 ^ _129833) ^ [_148385, _148387] : [empty(cartesian_product2(_148387, _148385)), -(empty(_148387)), -(empty(_148385))], (394 ^ _129833) ^ [] : [true___, -(true___)], (642 ^ _129833) ^ [] : [-(function(636 ^ []))], (621 ^ _129833) ^ [_149926] : [-(element(619 ^ [_149926], powerset(_149926)))], (536 ^ _129833) ^ [] : [-(empty(empty_set))], (288 ^ _129833) ^ [_139400, _139402, _139404, _139406] : [-(relation_dom_restriction(_139406, _139402) = relation_dom_restriction(_139404, _139400)), _139406 = _139404, _139402 = _139400], (470 ^ _129833) ^ [_145028, _145030, _145032] : [relation_of2_as_subset(_145028, _145032, _145030), -(element(_145028, powerset(cartesian_product2(_145032, _145030))))], (640 ^ _129833) ^ [] : [-(relation_empty_yielding(636 ^ []))], (400 ^ _129833) ^ [_142879, _142881] : [relation(_142881), -(relation(relation_dom_restriction(_142881, _142879)))], (628 ^ _129833) ^ [] : [-(function(624 ^ []))], (96 ^ _129833) ^ [_133035, _133037, _133039, _133041, _133043, _133045] : [-(relation_of2(_133043, _133039, _133035)), relation_of2(_133045, _133041, _133037), _133045 = _133043, _133041 = _133039, _133037 = _133035], (656 ^ _129833) ^ [_151140, _151142, _151144] : [relation_of2(_151140, _151144, _151142), -(relation_of2_as_subset(_151140, _151144, _151142))], (540 ^ _129833) ^ [] : [-(relation_empty_yielding(empty_set))], (250 ^ _129833) ^ [_137993, _137995, _137997, _137999] : [-(the_mapping(_137999, _137995) = the_mapping(_137997, _137993)), _137999 = _137997, _137995 = _137993], (585 ^ _129833) ^ [] : [-(function(581 ^ []))], (542 ^ _129833) ^ [_147443, _147445] : [549 ^ _129833 : [(552 ^ _129833) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_147445, _147443)))], (550 ^ _129833) ^ [] : [-(relation(relation_dom_restriction(_147445, _147443)))]], relation(_147445), relation_empty_yielding(_147445)], (10 ^ _129833) ^ [_130268, _130270, _130272] : [-(_130272 = _130268), _130272 = _130270, _130270 = _130268], (644 ^ _129833) ^ [_150685, _150687, _150689, _150691] : [relation_of2(_150687, _150691, _150689), -(relation_dom_restr_as_relation_of(_150691, _150689, _150687, _150685) = relation_dom_restriction(_150687, _150685))], (4 ^ _129833) ^ [_130064, _130066] : [_130066 = _130064, -(_130064 = _130066)], (692 ^ _129833) ^ [_152389, _152391, _152393] : [-(element(_152393, _152389)), in(_152393, _152391), element(_152391, powerset(_152389))], (609 ^ _129833) ^ [] : [-(relation(607 ^ []))], (515 ^ _129833) ^ [_146526] : [rel_str(_146526), -(subrelstr(518 ^ [_146526], _146526))], (611 ^ _129833) ^ [] : [-(empty(607 ^ []))], (510 ^ _129833) ^ [_146301, _146303] : [-(relation_of2(508 ^ [_146301, _146303], _146303, _146301))], (756 ^ _129833) ^ [_154765, _154767] : [in(_154767, _154765), empty(_154765)], (440 ^ _129833) ^ [] : [true___, -(true___)], (633 ^ _129833) ^ [] : [-(relation(631 ^ []))], (138 ^ _129833) ^ [_134355, _134357, _134359, _134361] : [-(subrelstr(_134359, _134355)), subrelstr(_134361, _134357), _134361 = _134359, _134357 = _134355], (680 ^ _129833) ^ [_151993, _151995] : [element(_151995, powerset(_151993)), -(subset(_151995, _151993))], (616 ^ _129833) ^ [] : [empty(614 ^ [])], (635 ^ _129833) ^ [] : [-(relation_empty_yielding(631 ^ []))], (712 ^ _129833) ^ [_153012] : [rel_str(_153012), 715 ^ _129833 : [(716 ^ _129833) ^ [_153215] : [subrelstr(_153215, _153012), 719 ^ _129833 : [(720 ^ _129833) ^ [_153415] : [element(_153415, the_carrier(_153012)), 723 ^ _129833 : [(724 ^ _129833) ^ [_153612] : [element(_153612, the_carrier(_153012)), 727 ^ _129833 : [(728 ^ _129833) ^ [_153802] : [element(_153802, the_carrier(_153215)), 731 ^ _129833 : [(732 ^ _129833) ^ [_153985] : [element(_153985, the_carrier(_153215)), -(related(_153012, _153415, _153612)), _153802 = _153415, _153985 = _153612, related(_153215, _153802, _153985)]]]]]]]]]]], (626 ^ _129833) ^ [] : [-(relation(624 ^ []))], (218 ^ _129833) ^ [_136886, _136888, _136890, _136892] : [-(element(_136890, _136886)), element(_136892, _136888), _136892 = _136890, _136888 = _136886], (48 ^ _129833) ^ [_131485, _131487] : [-(relation(_131485)), _131487 = _131485, relation(_131487)], (298 ^ _129833) ^ [_139731, _139733] : [_139733 = _139731, -(powerset(_139733) = powerset(_139731))], (583 ^ _129833) ^ [] : [-(relation(581 ^ []))], (38 ^ _129833) ^ [_131190, _131192] : [-(one_to_one(_131190)), _131192 = _131190, one_to_one(_131192)], (554 ^ _129833) ^ [_147791] : [empty(powerset(_147791))], (592 ^ _129833) ^ [] : [-(function(586 ^ []))], (630 ^ _129833) ^ [] : [-(one_to_one(624 ^ []))], (334 ^ _129833) ^ [_140980] : [345 ^ _129833 : [(350 ^ _129833) ^ [] : [-(one_to_one(_140980))], (348 ^ _129833) ^ [] : [-(function(_140980))], (346 ^ _129833) ^ [] : [-(relation(_140980))]], relation(_140980), empty(_140980), function(_140980)], (476 ^ _129833) ^ [] : [true___, -(true___)], (686 ^ _129833) ^ [_152159, _152161] : [subset(_152161, _152159), -(element(_152161, powerset(_152159)))], (176 ^ _129833) ^ [_135510, _135512] : [-(one_sorted_str(_135510)), _135512 = _135510, one_sorted_str(_135512)], (570 ^ _129833) ^ [] : [-(relation(empty_set))], (316 ^ _129833) ^ [_140370] : [empty(_140370), -(function(_140370))], (186 ^ _129833) ^ [_135833, _135835, _135837, _135839] : [-(net_str(_135837, _135833)), net_str(_135839, _135835), _135839 = _135837, _135835 = _135833], (382 ^ _129833) ^ [] : [true___, -(true___)], (68 ^ _129833) ^ [_132075, _132077] : [-(function(_132075)), _132077 = _132075, function(_132077)], (556 ^ _129833) ^ [_147899, _147901] : [563 ^ _129833 : [(566 ^ _129833) ^ [] : [-(function(relation_dom_restriction(_147901, _147899)))], (564 ^ _129833) ^ [] : [-(relation(relation_dom_restriction(_147901, _147899)))]], relation(_147901), function(_147901)], (270 ^ _129833) ^ [_138767, _138769, _138771, _138773, _138775, _138777, _138779, _138781] : [-(relation_dom_restr_as_relation_of(_138781, _138777, _138773, _138769) = relation_dom_restr_as_relation_of(_138779, _138775, _138771, _138767)), _138781 = _138779, _138777 = _138775, _138773 = _138771, _138769 = _138767], (406 ^ _129833) ^ [_143119, _143121, _143123, _143125] : [relation_of2(_143121, _143125, _143123), -(relation_of2_as_subset(relation_dom_restr_as_relation_of(_143125, _143123, _143121, _143119), _143125, _143123))], (412 ^ _129833) ^ [_143341] : [rel_str(_143341), -(one_sorted_str(_143341))], (597 ^ _129833) ^ [] : [-(relation(593 ^ []))]], input).
% 43.41/42.85 ncf('1',plain,[-(related(777 ^ [], 786 ^ [], 789 ^ []))],start(797 ^ 0)).
% 43.41/42.85 ncf('1.1',plain,[related(777 ^ [], 786 ^ [], 789 ^ []), 732 : element(789 ^ [], the_carrier(777 ^ [])), 732 : -(related(774 ^ [], 780 ^ [], 783 ^ [])), 732 : 786 ^ [] = 780 ^ [], 732 : 789 ^ [] = 783 ^ [], 732 : element(786 ^ [], the_carrier(777 ^ [])), 728 : element(783 ^ [], the_carrier(774 ^ [])), 724 : element(780 ^ [], the_carrier(774 ^ [])), 720 : subrelstr(777 ^ [], 774 ^ []), 716 : rel_str(774 ^ [])],extension(712 ^ 1,bind([[_153012, _153215, _153415, _153612, _153802, _153985], [774 ^ [], 777 ^ [], 780 ^ [], 783 ^ [], 786 ^ [], 789 ^ []]]))).
% 43.41/42.85 ncf('1.1.1',plain,[-(element(789 ^ [], the_carrier(777 ^ [])))],extension(791 ^ 12)).
% 43.41/42.85 ncf('1.1.2',plain,[related(774 ^ [], 780 ^ [], 783 ^ [])],extension(799 ^ 12)).
% 43.41/42.85 ncf('1.1.3',plain,[-(786 ^ [] = 780 ^ []), 780 ^ [] = 786 ^ []],extension(4 ^ 12,bind([[_130064, _130066], [786 ^ [], 780 ^ []]]))).
% 43.41/42.85 ncf('1.1.3.1',plain,[-(780 ^ [] = 786 ^ [])],extension(793 ^ 13)).
% 43.41/42.85 ncf('1.1.4',plain,[-(789 ^ [] = 783 ^ []), 783 ^ [] = 789 ^ []],extension(4 ^ 12,bind([[_130064, _130066], [789 ^ [], 783 ^ []]]))).
% 43.41/42.85 ncf('1.1.4.1',plain,[-(783 ^ [] = 789 ^ [])],extension(795 ^ 13)).
% 43.41/42.85 ncf('1.1.5',plain,[-(element(786 ^ [], the_carrier(777 ^ [])))],extension(788 ^ 10)).
% 43.41/42.85 ncf('1.1.6',plain,[-(element(783 ^ [], the_carrier(774 ^ [])))],extension(785 ^ 8)).
% 43.41/42.85 ncf('1.1.7',plain,[-(element(780 ^ [], the_carrier(774 ^ [])))],extension(782 ^ 6)).
% 43.41/42.85 ncf('1.1.8',plain,[-(subrelstr(777 ^ [], 774 ^ [])), 364 : subnetstr(777 ^ [], 771 ^ [], 774 ^ []), 364 : net_str(777 ^ [], 771 ^ []), 360 : net_str(774 ^ [], 771 ^ []), 356 : one_sorted_str(771 ^ [])],extension(352 ^ 4,bind([[_141473, _141645, _141814], [771 ^ [], 774 ^ [], 777 ^ []]]))).
% 43.41/42.85 ncf('1.1.8.1',plain,[-(subnetstr(777 ^ [], 771 ^ [], 774 ^ []))],extension(779 ^ 11)).
% 43.41/42.85 ncf('1.1.8.2',plain,[-(net_str(777 ^ [], 771 ^ [])), 464 : subnetstr(777 ^ [], 771 ^ [], 774 ^ []), 464 : one_sorted_str(771 ^ []), 464 : net_str(774 ^ [], 771 ^ [])],extension(456 ^ 9,bind([[_144560, _144562, _144785], [774 ^ [], 771 ^ [], 777 ^ []]]))).
% 43.41/42.85 ncf('1.1.8.2.1',plain,[-(subnetstr(777 ^ [], 771 ^ [], 774 ^ []))],extension(779 ^ 12)).
% 43.41/42.85 ncf('1.1.8.2.2',plain,[-(one_sorted_str(771 ^ []))],extension(773 ^ 10)).
% 43.41/42.85 ncf('1.1.8.2.3',plain,[-(net_str(774 ^ [], 771 ^ []))],extension(776 ^ 10)).
% 43.41/42.85 ncf('1.1.8.3',plain,[-(net_str(774 ^ [], 771 ^ []))],extension(776 ^ 7)).
% 43.41/42.85 ncf('1.1.8.4',plain,[-(one_sorted_str(771 ^ []))],extension(773 ^ 5)).
% 43.41/42.85 ncf('1.1.9',plain,[-(rel_str(774 ^ [])), 428 : net_str(774 ^ [], 771 ^ []), 428 : one_sorted_str(771 ^ [])],extension(424 ^ 2,bind([[_143646, _143776], [771 ^ [], 774 ^ []]]))).
% 43.41/42.85 ncf('1.1.9.1',plain,[-(net_str(774 ^ [], 771 ^ []))],extension(776 ^ 5)).
% 43.41/42.85 ncf('1.1.9.2',plain,[-(one_sorted_str(771 ^ []))],extension(773 ^ 3)).
% 43.41/42.85 %-----------------------------------------------------
% 43.41/42.85 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------