%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU373+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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 0.35s 1.37s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SEU373+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.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:40:37 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.37
% 0.35/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 ncf(matrix, plain, [(755 ^ _111372) ^ [] : [-(one_sorted_str(753 ^ []))], (758 ^ _111372) ^ [] : [-(net_str(756 ^ [], 753 ^ []))], (761 ^ _111372) ^ [] : [-(subnetstr(759 ^ [], 753 ^ [], 756 ^ []))], (763 ^ _111372) ^ [] : [subset(the_carrier(759 ^ []), the_carrier(756 ^ []))], (232 ^ _111372) ^ [_118909, _118911] : [_118911 = _118909, -(the_InternalRel(_118911) = the_InternalRel(_118909))], (238 ^ _111372) ^ [_119155, _119157, _119159, _119161] : [-(the_mapping(_119161, _119157) = the_mapping(_119159, _119155)), _119161 = _119159, _119157 = _119155], (248 ^ _111372) ^ [_119514, _119516, _119518, _119520] : [-(cartesian_product2(_119520, _119516) = cartesian_product2(_119518, _119514)), _119520 = _119518, _119516 = _119514], (258 ^ _111372) ^ [_119929, _119931, _119933, _119935, _119937, _119939, _119941, _119943] : [-(relation_dom_restr_as_relation_of(_119943, _119939, _119935, _119931) = relation_dom_restr_as_relation_of(_119941, _119937, _119933, _119929)), _119943 = _119941, _119939 = _119937, _119935 = _119933, _119931 = _119929], (276 ^ _111372) ^ [_120562, _120564, _120566, _120568] : [-(relation_dom_restriction(_120568, _120564) = relation_dom_restriction(_120566, _120562)), _120568 = _120566, _120564 = _120562], (286 ^ _111372) ^ [_120893, _120895] : [_120895 = _120893, -(powerset(_120895) = powerset(_120893))], (292 ^ _111372) ^ [_121091, _121093] : [_121093 = _121091, -(the_carrier(_121093) = the_carrier(_121091))], (2 ^ _111372) ^ [_111516] : [-(_111516 = _111516)], (4 ^ _111372) ^ [_111623, _111625] : [_111625 = _111623, -(_111623 = _111625)], (10 ^ _111372) ^ [_111827, _111829, _111831] : [-(_111831 = _111827), _111831 = _111829, _111829 = _111827], (20 ^ _111372) ^ [_112196, _112198, _112200, _112202, _112204, _112206] : [-(quasi_total(_112204, _112200, _112196)), quasi_total(_112206, _112202, _112198), _112206 = _112204, _112202 = _112200, _112198 = _112196], (38 ^ _111372) ^ [_112749, _112751] : [-(rel_str(_112749)), _112751 = _112749, rel_str(_112751)], (48 ^ _111372) ^ [_113072, _113074, _113076, _113078] : [-(subrelstr(_113076, _113072)), subrelstr(_113078, _113074), _113078 = _113076, _113074 = _113072], (62 ^ _111372) ^ [_113488, _113490] : [-(one_to_one(_113488)), _113490 = _113488, one_to_one(_113490)], (72 ^ _111372) ^ [_113783, _113785] : [-(relation(_113783)), _113785 = _113783, relation(_113785)], (82 ^ _111372) ^ [_114078, _114080] : [-(relation_empty_yielding(_114078)), _114080 = _114078, relation_empty_yielding(_114080)], (92 ^ _111372) ^ [_114373, _114375] : [-(function(_114373)), _114375 = _114373, function(_114375)], (102 ^ _111372) ^ [_114724, _114726, _114728, _114730, _114732, _114734] : [-(relation_of2_as_subset(_114732, _114728, _114724)), relation_of2_as_subset(_114734, _114730, _114726), _114734 = _114732, _114730 = _114728, _114726 = _114724], (120 ^ _111372) ^ [_115333, _115335, _115337, _115339, _115341, _115343] : [-(relation_of2(_115341, _115337, _115333)), relation_of2(_115343, _115339, _115335), _115343 = _115341, _115339 = _115337, _115335 = _115333], (138 ^ _111372) ^ [_115914, _115916, _115918, _115920] : [-(element(_115918, _115914)), element(_115920, _115916), _115920 = _115918, _115916 = _115914], (152 ^ _111372) ^ [_116358, _116360, _116362, _116364] : [-(in(_116362, _116358)), in(_116364, _116360), _116364 = _116362, _116360 = _116358], (166 ^ _111372) ^ [_116774, _116776] : [-(empty(_116774)), _116776 = _116774, empty(_116776)], (176 ^ _111372) ^ [_117069, _117071] : [-(one_sorted_str(_117069)), _117071 = _117069, one_sorted_str(_117071)], (186 ^ _111372) ^ [_117392, _117394, _117396, _117398] : [-(net_str(_117396, _117392)), net_str(_117398, _117394), _117398 = _117396, _117394 = _117392], (218 ^ _111372) ^ [_118425, _118427, _118429, _118431] : [-(subset(_118429, _118425)), subset(_118431, _118427), _118431 = _118429, _118427 = _118425], (200 ^ _111372) ^ [_117864, _117866, _117868, _117870, _117872, _117874] : [-(subnetstr(_117872, _117868, _117864)), subnetstr(_117874, _117870, _117866), _117874 = _117872, _117870 = _117868, _117866 = _117864], (298 ^ _111372) ^ [_121339, _121341] : [in(_121341, _121339), in(_121339, _121341)], (304 ^ _111372) ^ [_121536] : [empty(_121536), -(function(_121536))], (310 ^ _111372) ^ [_121722] : [empty(_121722), -(relation(_121722))], (316 ^ _111372) ^ [_121936, _121938, _121940] : [element(_121936, powerset(cartesian_product2(_121940, _121938))), -(relation(_121936))], (322 ^ _111372) ^ [_122146] : [333 ^ _111372 : [(334 ^ _111372) ^ [] : [-(relation(_122146))], (336 ^ _111372) ^ [] : [-(function(_122146))], (338 ^ _111372) ^ [] : [-(one_to_one(_122146))]], relation(_122146), empty(_122146), function(_122146)], (340 ^ _111372) ^ [_122639] : [rel_str(_122639), 343 ^ _111372 : [(344 ^ _111372) ^ [_122789] : [rel_str(_122789), 347 ^ _111372 : [(348 ^ _111372) ^ [] : [subrelstr(_122789, _122639), 351 ^ _111372 : [(352 ^ _111372) ^ [] : [-(subset(the_carrier(_122789), the_carrier(_122639)))], (354 ^ _111372) ^ [] : [-(subset(the_InternalRel(_122789), the_InternalRel(_122639)))]]], (356 ^ _111372) ^ [] : [-(subrelstr(_122789, _122639)), subset(the_carrier(_122789), the_carrier(_122639)), subset(the_InternalRel(_122789), the_InternalRel(_122639))]]]]], (366 ^ _111372) ^ [_123422] : [one_sorted_str(_123422), 369 ^ _111372 : [(370 ^ _111372) ^ [_123594] : [net_str(_123594, _123422), 373 ^ _111372 : [(374 ^ _111372) ^ [_123763] : [net_str(_123763, _123422), 377 ^ _111372 : [(378 ^ _111372) ^ [] : [subnetstr(_123763, _123422, _123594), 381 ^ _111372 : [(382 ^ _111372) ^ [] : [-(subrelstr(_123763, _123594))], (384 ^ _111372) ^ [] : [-(the_mapping(_123422, _123763) = relation_dom_restr_as_relation_of(the_carrier(_123594), the_carrier(_123422), the_mapping(_123422, _123594), the_carrier(_123763)))]]], (386 ^ _111372) ^ [] : [-(subnetstr(_123763, _123422, _123594)), subrelstr(_123763, _123594), the_mapping(_123422, _123763) = relation_dom_restr_as_relation_of(the_carrier(_123594), the_carrier(_123422), the_mapping(_123422, _123594), the_carrier(_123763))]]]]]]], (396 ^ _111372) ^ [] : [true___, -(true___)], (402 ^ _111372) ^ [] : [true___, -(true___)], (408 ^ _111372) ^ [] : [true___, -(true___)], (414 ^ _111372) ^ [_124828, _124830] : [relation(_124830), -(relation(relation_dom_restriction(_124830, _124828)))], (420 ^ _111372) ^ [_125068, _125070, _125072, _125074] : [relation_of2(_125070, _125074, _125072), -(relation_of2_as_subset(relation_dom_restr_as_relation_of(_125074, _125072, _125070, _125068), _125074, _125072))], (426 ^ _111372) ^ [_125290] : [rel_str(_125290), -(one_sorted_str(_125290))], (432 ^ _111372) ^ [] : [true___, -(true___)], (438 ^ _111372) ^ [_125595] : [one_sorted_str(_125595), 441 ^ _111372 : [(442 ^ _111372) ^ [_125725] : [net_str(_125725, _125595), -(rel_str(_125725))]]], (448 ^ _111372) ^ [] : [true___, -(true___)], (454 ^ _111372) ^ [] : [true___, -(true___)], (460 ^ _111372) ^ [_126164] : [rel_str(_126164), 463 ^ _111372 : [(464 ^ _111372) ^ [_126294] : [subrelstr(_126294, _126164), -(rel_str(_126294))]]], (470 ^ _111372) ^ [_126509, _126511] : [one_sorted_str(_126511), net_str(_126509, _126511), 477 ^ _111372 : [(478 ^ _111372) ^ [_126734] : [subnetstr(_126734, _126511, _126509), -(net_str(_126734, _126511))]]], (484 ^ _111372) ^ [_126977, _126979, _126981] : [relation_of2_as_subset(_126977, _126981, _126979), -(element(_126977, powerset(cartesian_product2(_126981, _126979))))], (490 ^ _111372) ^ [_127191] : [rel_str(_127191), -(relation_of2_as_subset(the_InternalRel(_127191), the_carrier(_127191), the_carrier(_127191)))], (496 ^ _111372) ^ [] : [true___, -(true___)], (502 ^ _111372) ^ [_127526, _127528] : [509 ^ _111372 : [(510 ^ _111372) ^ [] : [-(function(the_mapping(_127528, _127526)))], (512 ^ _111372) ^ [] : [-(quasi_total(the_mapping(_127528, _127526), the_carrier(_127526), the_carrier(_127528)))], (514 ^ _111372) ^ [] : [-(relation_of2_as_subset(the_mapping(_127528, _127526), the_carrier(_127526), the_carrier(_127528)))]], one_sorted_str(_127528), net_str(_127526, _127528)], (517 ^ _111372) ^ [] : [-(rel_str(515 ^ []))], (520 ^ _111372) ^ [] : [-(one_sorted_str(518 ^ []))], (522 ^ _111372) ^ [_128172] : [one_sorted_str(_128172), -(net_str(525 ^ [_128172], _128172))], (530 ^ _111372) ^ [_128452, _128454] : [-(relation_of2(528 ^ [_128452, _128454], _128454, _128452))], (533 ^ _111372) ^ [_128579] : [-(element(531 ^ [_128579], _128579))], (535 ^ _111372) ^ [_128677] : [rel_str(_128677), -(subrelstr(538 ^ [_128677], _128677))], (542 ^ _111372) ^ [_128930, _128932] : [-(subnetstr(549 ^ [_128930, _128932], _128932, _128930)), one_sorted_str(_128932), net_str(_128930, _128932)], (554 ^ _111372) ^ [_129314, _129316] : [-(relation_of2_as_subset(552 ^ [_129314, _129316], _129316, _129314))], (556 ^ _111372) ^ [] : [-(empty(empty_set))], (558 ^ _111372) ^ [] : [-(relation(empty_set))], (560 ^ _111372) ^ [] : [-(relation_empty_yielding(empty_set))], (562 ^ _111372) ^ [_129594, _129596] : [569 ^ _111372 : [(570 ^ _111372) ^ [] : [-(relation(relation_dom_restriction(_129596, _129594)))], (572 ^ _111372) ^ [] : [-(relation_empty_yielding(relation_dom_restriction(_129596, _129594)))]], relation(_129596), relation_empty_yielding(_129596)], (574 ^ _111372) ^ [_129942] : [empty(powerset(_129942))], (576 ^ _111372) ^ [_130050, _130052] : [583 ^ _111372 : [(584 ^ _111372) ^ [] : [-(relation(relation_dom_restriction(_130052, _130050)))], (586 ^ _111372) ^ [] : [-(function(relation_dom_restriction(_130052, _130050)))]], relation(_130052), function(_130052)], (588 ^ _111372) ^ [] : [-(empty(empty_set))], (590 ^ _111372) ^ [] : [-(relation(empty_set))], (592 ^ _111372) ^ [_130536, _130538] : [empty(cartesian_product2(_130538, _130536)), -(empty(_130538)), -(empty(_130536))], (603 ^ _111372) ^ [] : [-(relation(601 ^ []))], (605 ^ _111372) ^ [] : [-(function(601 ^ []))], (608 ^ _111372) ^ [] : [-(relation(606 ^ []))], (610 ^ _111372) ^ [] : [-(relation_empty_yielding(606 ^ []))], (612 ^ _111372) ^ [] : [-(function(606 ^ []))], (615 ^ _111372) ^ [] : [-(empty(613 ^ []))], (617 ^ _111372) ^ [] : [-(relation(613 ^ []))], (619 ^ _111372) ^ [_131335] : [-(empty(_131335)), 623 ^ _111372 : [(624 ^ _111372) ^ [] : [-(element(622 ^ [_131335], powerset(_131335)))], (626 ^ _111372) ^ [] : [empty(622 ^ [_131335])]]], (629 ^ _111372) ^ [] : [-(relation(627 ^ []))], (631 ^ _111372) ^ [] : [-(empty(627 ^ []))], (633 ^ _111372) ^ [] : [-(function(627 ^ []))], (636 ^ _111372) ^ [] : [empty(634 ^ [])], (638 ^ _111372) ^ [] : [-(relation(634 ^ []))], (641 ^ _111372) ^ [_132077] : [-(element(639 ^ [_132077], powerset(_132077)))], (643 ^ _111372) ^ [_132128] : [-(empty(639 ^ [_132128]))], (646 ^ _111372) ^ [] : [-(relation(644 ^ []))], (648 ^ _111372) ^ [] : [-(function(644 ^ []))], (650 ^ _111372) ^ [] : [-(one_to_one(644 ^ []))], (653 ^ _111372) ^ [] : [-(relation(651 ^ []))], (655 ^ _111372) ^ [] : [-(relation_empty_yielding(651 ^ []))], (658 ^ _111372) ^ [] : [-(relation(656 ^ []))], (660 ^ _111372) ^ [] : [-(relation_empty_yielding(656 ^ []))], (662 ^ _111372) ^ [] : [-(function(656 ^ []))], (664 ^ _111372) ^ [_132836, _132838, _132840, _132842] : [relation_of2(_132838, _132842, _132840), -(relation_dom_restr_as_relation_of(_132842, _132840, _132838, _132836) = relation_dom_restriction(_132838, _132836))], (670 ^ _111372) ^ [_133119, _133121, _133123] : [relation_of2_as_subset(_133119, _133123, _133121), -(relation_of2(_133119, _133123, _133121))], (676 ^ _111372) ^ [_133291, _133293, _133295] : [relation_of2(_133291, _133295, _133293), -(relation_of2_as_subset(_133291, _133295, _133293))], (682 ^ _111372) ^ [_133498, _133500] : [-(subset(_133500, _133500))], (684 ^ _111372) ^ [_133607, _133609] : [in(_133609, _133607), -(element(_133609, _133607))], (690 ^ _111372) ^ [_133817, _133819] : [element(_133819, _133817), -(empty(_133817)), -(in(_133819, _133817))], (700 ^ _111372) ^ [_134144, _134146] : [element(_134146, powerset(_134144)), -(subset(_134146, _134144))], (706 ^ _111372) ^ [_134310, _134312] : [subset(_134312, _134310), -(element(_134312, powerset(_134310)))], (712 ^ _111372) ^ [_134540, _134542, _134544] : [-(element(_134544, _134540)), in(_134544, _134542), element(_134542, powerset(_134540))], (722 ^ _111372) ^ [_134867, _134869, _134871] : [in(_134871, _134869), element(_134869, powerset(_134867)), empty(_134867)], (732 ^ _111372) ^ [_135163] : [empty(_135163), -(_135163 = empty_set)], (738 ^ _111372) ^ [_135365, _135367] : [in(_135367, _135365), empty(_135365)], (744 ^ _111372) ^ [_135552, _135554] : [empty(_135554), -(_135554 = _135552), empty(_135552)]], input).
% 0.35/1.37 ncf('1',plain,[subset(the_carrier(759 ^ []), the_carrier(756 ^ []))],start(763 ^ 0)).
% 0.35/1.37 ncf('1.1',plain,[-(subset(the_carrier(759 ^ []), the_carrier(756 ^ []))), 348 : subrelstr(759 ^ [], 756 ^ []), 348 : rel_str(759 ^ []), 344 : rel_str(756 ^ [])],extension(340 ^ 1,bind([[_122639, _122789], [756 ^ [], 759 ^ []]]))).
% 0.35/1.37 ncf('1.1.1',plain,[-(subrelstr(759 ^ [], 756 ^ [])), 378 : subnetstr(759 ^ [], 753 ^ [], 756 ^ []), 378 : net_str(759 ^ [], 753 ^ []), 374 : net_str(756 ^ [], 753 ^ []), 370 : one_sorted_str(753 ^ [])],extension(366 ^ 6,bind([[_123422, _123594, _123763], [753 ^ [], 756 ^ [], 759 ^ []]]))).
% 0.35/1.37 ncf('1.1.1.1',plain,[-(subnetstr(759 ^ [], 753 ^ [], 756 ^ []))],extension(761 ^ 13)).
% 0.35/1.37 ncf('1.1.1.2',plain,[-(net_str(759 ^ [], 753 ^ [])), 478 : subnetstr(759 ^ [], 753 ^ [], 756 ^ []), 478 : one_sorted_str(753 ^ []), 478 : net_str(756 ^ [], 753 ^ [])],extension(470 ^ 11,bind([[_126509, _126511, _126734], [756 ^ [], 753 ^ [], 759 ^ []]]))).
% 0.35/1.37 ncf('1.1.1.2.1',plain,[-(subnetstr(759 ^ [], 753 ^ [], 756 ^ []))],extension(761 ^ 14)).
% 0.35/1.37 ncf('1.1.1.2.2',plain,[-(one_sorted_str(753 ^ []))],extension(755 ^ 12)).
% 0.35/1.37 ncf('1.1.1.2.3',plain,[-(net_str(756 ^ [], 753 ^ []))],extension(758 ^ 12)).
% 0.35/1.37 ncf('1.1.1.3',plain,[-(net_str(756 ^ [], 753 ^ []))],extension(758 ^ 9)).
% 0.35/1.37 ncf('1.1.1.4',plain,[-(one_sorted_str(753 ^ []))],extension(755 ^ 7)).
% 0.35/1.37 ncf('1.1.2',plain,[-(rel_str(759 ^ [])), 442 : net_str(759 ^ [], 753 ^ []), 442 : one_sorted_str(753 ^ [])],extension(438 ^ 4,bind([[_125595, _125725], [753 ^ [], 759 ^ []]]))).
% 0.35/1.37 ncf('1.1.2.1',plain,[-(net_str(759 ^ [], 753 ^ [])), 478 : subnetstr(759 ^ [], 753 ^ [], 756 ^ []), 478 : one_sorted_str(753 ^ []), 478 : net_str(756 ^ [], 753 ^ [])],extension(470 ^ 7,bind([[_126509, _126511, _126734], [756 ^ [], 753 ^ [], 759 ^ []]]))).
% 0.35/1.37 ncf('1.1.2.1.1',plain,[-(subnetstr(759 ^ [], 753 ^ [], 756 ^ []))],extension(761 ^ 10)).
% 0.35/1.37 ncf('1.1.2.1.2',plain,[-(one_sorted_str(753 ^ []))],extension(755 ^ 8)).
% 0.35/1.37 ncf('1.1.2.1.3',plain,[-(net_str(756 ^ [], 753 ^ []))],extension(758 ^ 8)).
% 0.35/1.37 ncf('1.1.2.2',plain,[-(one_sorted_str(753 ^ []))],extension(755 ^ 5)).
% 0.35/1.37 ncf('1.1.3',plain,[-(rel_str(756 ^ [])), 442 : net_str(756 ^ [], 753 ^ []), 442 : one_sorted_str(753 ^ [])],extension(438 ^ 2,bind([[_125595, _125725], [753 ^ [], 756 ^ []]]))).
% 0.35/1.37 ncf('1.1.3.1',plain,[-(net_str(756 ^ [], 753 ^ []))],extension(758 ^ 5)).
% 0.35/1.37 ncf('1.1.3.2',plain,[-(one_sorted_str(753 ^ []))],extension(755 ^ 3)).
% 0.35/1.37 %-----------------------------------------------------
% 0.35/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------