%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU413+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:28 EDT 2023
% Result : Theorem 0.33s 1.39s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU413+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n026.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 13:33:05 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.33/1.39
% 0.33/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 ncf(matrix, plain, [(538 ^ _84757) ^ [] : [-(l1_orders_2(536 ^ []))], (541 ^ _84757) ^ [] : [-(l1_orders_2(539 ^ []))], (544 ^ _84757) ^ [] : [-(m1_subset_1(542 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))))], (547 ^ _84757) ^ [] : [-(m1_subset_1(545 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))))], (549 ^ _84757) ^ [] : [-(v12_waybel_0(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), 539 ^ []))], (551 ^ _84757) ^ [] : [-(m1_subset_1(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), k1_zfmisc_1(u1_struct_0(539 ^ []))))], (553 ^ _84757) ^ [] : [-(r1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []), 542 ^ [], 545 ^ []))], (555 ^ _84757) ^ [] : [-(r2_hidden(545 ^ [], u1_struct_0(536 ^ [])))], (557 ^ _84757) ^ [] : [r2_hidden(542 ^ [], u1_struct_0(536 ^ []))], (180 ^ _84757) ^ [_90639, _90641, _90643, _90645] : [-(k2_zfmisc_1(_90645, _90641) = k2_zfmisc_1(_90643, _90639)), _90645 = _90643, _90641 = _90639], (190 ^ _84757) ^ [_90998, _91000, _91002, _91004] : [-(g1_orders_2(_91004, _91000) = g1_orders_2(_91002, _90998)), _91004 = _91002, _91000 = _90998], (200 ^ _84757) ^ [_91357, _91359, _91361, _91363] : [-(k4_tarski(_91363, _91359) = k4_tarski(_91361, _91357)), _91363 = _91361, _91359 = _91357], (210 ^ _84757) ^ [_91688, _91690] : [_91690 = _91688, -(u1_orders_2(_91690) = u1_orders_2(_91688))], (216 ^ _84757) ^ [_91934, _91936, _91938, _91940] : [-(k3_xboole_0(_91940, _91936) = k3_xboole_0(_91938, _91934)), _91940 = _91938, _91936 = _91934], (226 ^ _84757) ^ [_92265, _92267] : [_92267 = _92265, -(k1_zfmisc_1(_92267) = k1_zfmisc_1(_92265))], (242 ^ _84757) ^ [_92822, _92824] : [_92824 = _92822, -(u1_struct_0(_92824) = u1_struct_0(_92822))], (232 ^ _84757) ^ [_92511, _92513, _92515, _92517] : [-(k1_latsum_1(_92517, _92513) = k1_latsum_1(_92515, _92511)), _92517 = _92515, _92513 = _92511], (2 ^ _84757) ^ [_84901] : [-(_84901 = _84901)], (4 ^ _84757) ^ [_85008, _85010] : [_85010 = _85008, -(_85008 = _85010)], (10 ^ _84757) ^ [_85212, _85214, _85216] : [-(_85216 = _85212), _85216 = _85214, _85214 = _85212], (20 ^ _84757) ^ [_85525, _85527] : [-(v1_relat_1(_85525)), _85527 = _85525, v1_relat_1(_85527)], (30 ^ _84757) ^ [_85820, _85822] : [-(v1_orders_2(_85820)), _85822 = _85820, v1_orders_2(_85822)], (40 ^ _84757) ^ [_86115, _86117] : [-(l1_struct_0(_86115)), _86117 = _86115, l1_struct_0(_86117)], (50 ^ _84757) ^ [_86466, _86468, _86470, _86472, _86474, _86476] : [-(m2_relset_1(_86474, _86470, _86466)), m2_relset_1(_86476, _86472, _86468), _86476 = _86474, _86472 = _86470, _86468 = _86466], (68 ^ _84757) ^ [_87075, _87077, _87079, _87081, _87083, _87085] : [-(m1_relset_1(_87083, _87079, _87075)), m1_relset_1(_87085, _87081, _87077), _87085 = _87083, _87081 = _87079, _87077 = _87075], (86 ^ _84757) ^ [_87656, _87658, _87660, _87662] : [-(r1_tarski(_87660, _87656)), r1_tarski(_87662, _87658), _87662 = _87660, _87658 = _87656], (100 ^ _84757) ^ [_88072, _88074] : [-(v1_xboole_0(_88072)), _88074 = _88072, v1_xboole_0(_88074)], (110 ^ _84757) ^ [_88367, _88369] : [-(l1_orders_2(_88367)), _88369 = _88367, l1_orders_2(_88369)], (120 ^ _84757) ^ [_88690, _88692, _88694, _88696] : [-(v12_waybel_0(_88694, _88690)), v12_waybel_0(_88696, _88692), _88696 = _88694, _88692 = _88690], (134 ^ _84757) ^ [_89134, _89136, _89138, _89140] : [-(m1_subset_1(_89138, _89134)), m1_subset_1(_89140, _89136), _89140 = _89138, _89136 = _89134], (166 ^ _84757) ^ [_90167, _90169, _90171, _90173] : [-(r2_hidden(_90171, _90167)), r2_hidden(_90173, _90169), _90173 = _90171, _90169 = _90167], (148 ^ _84757) ^ [_89606, _89608, _89610, _89612, _89614, _89616] : [-(r1_orders_2(_89614, _89610, _89606)), r1_orders_2(_89616, _89612, _89608), _89616 = _89614, _89612 = _89610, _89608 = _89606], (248 ^ _84757) ^ [_93088] : [l1_orders_2(_93088), v1_orders_2(_93088), -(_93088 = g1_orders_2(u1_struct_0(_93088), u1_orders_2(_93088)))], (258 ^ _84757) ^ [_93387, _93389] : [r2_hidden(_93389, _93387), r2_hidden(_93387, _93389)], (264 ^ _84757) ^ [_93612, _93614, _93616] : [m1_subset_1(_93612, k1_zfmisc_1(k2_zfmisc_1(_93616, _93614))), -(v1_relat_1(_93612))], (270 ^ _84757) ^ [_93821, _93823] : [-(k3_xboole_0(_93823, _93821) = k3_xboole_0(_93821, _93823))], (272 ^ _84757) ^ [_93922] : [l1_orders_2(_93922), 275 ^ _84757 : [(276 ^ _84757) ^ [_94080] : [m1_subset_1(_94080, u1_struct_0(_93922)), 279 ^ _84757 : [(280 ^ _84757) ^ [_94237] : [m1_subset_1(_94237, u1_struct_0(_93922)), 283 ^ _84757 : [(284 ^ _84757) ^ [] : [r1_orders_2(_93922, _94080, _94237), -(r2_hidden(k4_tarski(_94080, _94237), u1_orders_2(_93922)))], (290 ^ _84757) ^ [] : [r2_hidden(k4_tarski(_94080, _94237), u1_orders_2(_93922)), -(r1_orders_2(_93922, _94080, _94237))]]]]]]], (296 ^ _84757) ^ [_94749, _94751] : [m1_relset_1(_94749, _94751, _94751), 299 ^ _84757 : [(300 ^ _84757) ^ [] : [-(v1_orders_2(g1_orders_2(_94751, _94749)))], (302 ^ _84757) ^ [] : [-(l1_orders_2(g1_orders_2(_94751, _94749)))]]], (304 ^ _84757) ^ [_95044, _95046] : [311 ^ _84757 : [(312 ^ _84757) ^ [] : [-(v1_orders_2(k1_latsum_1(_95046, _95044)))], (314 ^ _84757) ^ [] : [-(l1_orders_2(k1_latsum_1(_95046, _95044)))]], l1_orders_2(_95046), l1_orders_2(_95044)], (316 ^ _84757) ^ [] : [true___, -(true___)], (322 ^ _84757) ^ [] : [true___, -(true___)], (328 ^ _84757) ^ [] : [true___, -(true___)], (334 ^ _84757) ^ [] : [true___, -(true___)], (340 ^ _84757) ^ [] : [true___, -(true___)], (346 ^ _84757) ^ [_96003] : [l1_orders_2(_96003), -(l1_struct_0(_96003))], (352 ^ _84757) ^ [] : [true___, -(true___)], (358 ^ _84757) ^ [] : [true___, -(true___)], (364 ^ _84757) ^ [] : [true___, -(true___)], (370 ^ _84757) ^ [_96574, _96576, _96578] : [m2_relset_1(_96574, _96578, _96576), -(m1_subset_1(_96574, k1_zfmisc_1(k2_zfmisc_1(_96578, _96576))))], (376 ^ _84757) ^ [_96788] : [l1_orders_2(_96788), -(m2_relset_1(u1_orders_2(_96788), u1_struct_0(_96788), u1_struct_0(_96788)))], (382 ^ _84757) ^ [] : [true___, -(true___)], (389 ^ _84757) ^ [] : [-(l1_orders_2(387 ^ []))], (392 ^ _84757) ^ [] : [-(l1_struct_0(390 ^ []))], (395 ^ _84757) ^ [_97328, _97330] : [-(m1_relset_1(393 ^ [_97328, _97330], _97330, _97328))], (398 ^ _84757) ^ [_97455] : [-(m1_subset_1(396 ^ [_97455], _97455))], (401 ^ _84757) ^ [_97594, _97596] : [-(m2_relset_1(399 ^ [_97594, _97596], _97596, _97594))], (403 ^ _84757) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (405 ^ _84757) ^ [_97764, _97766] : [m1_relset_1(_97764, _97766, _97766), 408 ^ _84757 : [(409 ^ _84757) ^ [_97934, _97936] : [g1_orders_2(_97766, _97764) = g1_orders_2(_97936, _97934), 412 ^ _84757 : [(413 ^ _84757) ^ [] : [-(_97766 = _97936)], (415 ^ _84757) ^ [] : [-(_97764 = _97934)]]]]], (417 ^ _84757) ^ [_98241, _98243] : [-(k3_xboole_0(_98243, _98243) = _98243)], (420 ^ _84757) ^ [] : [-(v1_xboole_0(418 ^ []))], (423 ^ _84757) ^ [] : [v1_xboole_0(421 ^ [])], (425 ^ _84757) ^ [_98575, _98577, _98579] : [m2_relset_1(_98575, _98579, _98577), -(m1_relset_1(_98575, _98579, _98577))], (431 ^ _84757) ^ [_98747, _98749, _98751] : [m1_relset_1(_98747, _98751, _98749), -(m2_relset_1(_98747, _98751, _98749))], (437 ^ _84757) ^ [_98954, _98956] : [-(r1_tarski(_98956, _98956))], (439 ^ _84757) ^ [_99063, _99065] : [r2_hidden(_99065, _99063), -(m1_subset_1(_99065, _99063))], (445 ^ _84757) ^ [_99259] : [l1_orders_2(_99259), 448 ^ _84757 : [(449 ^ _84757) ^ [_99453] : [l1_orders_2(_99453), 452 ^ _84757 : [(453 ^ _84757) ^ [_99657, _99659] : [-(r2_hidden(_99659, u1_struct_0(_99259))), v12_waybel_0(k3_xboole_0(u1_struct_0(_99259), u1_struct_0(_99453)), _99453), m1_subset_1(k3_xboole_0(u1_struct_0(_99259), u1_struct_0(_99453)), k1_zfmisc_1(u1_struct_0(_99453))), r2_hidden(k4_tarski(_99659, _99657), u1_orders_2(k1_latsum_1(_99259, _99453))), r2_hidden(_99657, u1_struct_0(_99259))]]]]], (471 ^ _84757) ^ [_100215] : [-(k3_xboole_0(_100215, k1_xboole_0) = k1_xboole_0)], (473 ^ _84757) ^ [_100325, _100327] : [m1_subset_1(_100327, _100325), -(v1_xboole_0(_100325)), -(r2_hidden(_100327, _100325))], (483 ^ _84757) ^ [_100652, _100654] : [m1_subset_1(_100654, k1_zfmisc_1(_100652)), -(r1_tarski(_100654, _100652))], (489 ^ _84757) ^ [_100818, _100820] : [r1_tarski(_100820, _100818), -(m1_subset_1(_100820, k1_zfmisc_1(_100818)))], (495 ^ _84757) ^ [_101048, _101050, _101052] : [-(m1_subset_1(_101052, _101048)), r2_hidden(_101052, _101050), m1_subset_1(_101050, k1_zfmisc_1(_101048))], (505 ^ _84757) ^ [_101375, _101377, _101379] : [r2_hidden(_101379, _101377), m1_subset_1(_101377, k1_zfmisc_1(_101375)), v1_xboole_0(_101375)], (515 ^ _84757) ^ [_101671] : [v1_xboole_0(_101671), -(_101671 = k1_xboole_0)], (521 ^ _84757) ^ [_101873, _101875] : [r2_hidden(_101875, _101873), v1_xboole_0(_101873)], (527 ^ _84757) ^ [_102060, _102062] : [v1_xboole_0(_102062), -(_102062 = _102060), v1_xboole_0(_102060)]], input).
% 0.33/1.39 ncf('1',plain,[r2_hidden(542 ^ [], u1_struct_0(536 ^ []))],start(557 ^ 0)).
% 0.33/1.39 ncf('1.1',plain,[-(r2_hidden(542 ^ [], u1_struct_0(536 ^ []))), 453 : v12_waybel_0(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), 539 ^ []), 453 : m1_subset_1(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), k1_zfmisc_1(u1_struct_0(539 ^ []))), 453 : r2_hidden(k4_tarski(542 ^ [], 545 ^ []), u1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []))), 453 : r2_hidden(545 ^ [], u1_struct_0(536 ^ [])), 453 : l1_orders_2(539 ^ []), 449 : l1_orders_2(536 ^ [])],extension(445 ^ 1,bind([[_99259, _99453, _99657, _99659], [536 ^ [], 539 ^ [], 545 ^ [], 542 ^ []]]))).
% 0.33/1.39 ncf('1.1.1',plain,[-(v12_waybel_0(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), 539 ^ []))],extension(549 ^ 6)).
% 0.33/1.39 ncf('1.1.2',plain,[-(m1_subset_1(k3_xboole_0(u1_struct_0(536 ^ []), u1_struct_0(539 ^ [])), k1_zfmisc_1(u1_struct_0(539 ^ []))))],extension(551 ^ 6)).
% 0.33/1.39 ncf('1.1.3',plain,[-(r2_hidden(k4_tarski(542 ^ [], 545 ^ []), u1_orders_2(k1_latsum_1(536 ^ [], 539 ^ [])))), 284 : r1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []), 542 ^ [], 545 ^ []), 284 : m1_subset_1(545 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))), 280 : m1_subset_1(542 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))), 276 : l1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []))],extension(272 ^ 6,bind([[_93922, _94080, _94237], [k1_latsum_1(536 ^ [], 539 ^ []), 542 ^ [], 545 ^ []]]))).
% 0.33/1.39 ncf('1.1.3.1',plain,[-(r1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []), 542 ^ [], 545 ^ []))],extension(553 ^ 13)).
% 0.33/1.39 ncf('1.1.3.2',plain,[-(m1_subset_1(545 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))))],extension(547 ^ 11)).
% 0.33/1.39 ncf('1.1.3.3',plain,[-(m1_subset_1(542 ^ [], u1_struct_0(k1_latsum_1(536 ^ [], 539 ^ []))))],extension(544 ^ 9)).
% 0.33/1.39 ncf('1.1.3.4',plain,[-(l1_orders_2(k1_latsum_1(536 ^ [], 539 ^ []))), l1_orders_2(536 ^ []), l1_orders_2(539 ^ [])],extension(304 ^ 7,bind([[_95044, _95046], [539 ^ [], 536 ^ []]]))).
% 0.33/1.39 ncf('1.1.3.4.1',plain,[-(l1_orders_2(536 ^ []))],extension(538 ^ 8)).
% 0.33/1.39 ncf('1.1.3.4.2',plain,[-(l1_orders_2(539 ^ []))],extension(541 ^ 8)).
% 0.33/1.39 ncf('1.1.4',plain,[-(r2_hidden(545 ^ [], u1_struct_0(536 ^ [])))],extension(555 ^ 6)).
% 0.33/1.39 ncf('1.1.5',plain,[-(l1_orders_2(539 ^ []))],extension(541 ^ 4)).
% 0.33/1.39 ncf('1.1.6',plain,[-(l1_orders_2(536 ^ []))],extension(538 ^ 2)).
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------