%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU139+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:20 EDT 2023
% Result : Theorem 0.43s 1.38s
% Output : Proof 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU139+2 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n031.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.34 % DateTime : Thu May 18 13:01:10 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.43/1.38
% 0.43/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.43/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.43/1.38 %-----------------------------------------------------
% 0.43/1.38 ncf(matrix, plain, [(582 ^ _81764) ^ [] : [-(subset(579 ^ [], 580 ^ []))], (584 ^ _81764) ^ [] : [-(proper_subset(580 ^ [], 579 ^ []))], (86 ^ _81764) ^ [_84625, _84627, _84629, _84631] : [-(set_difference(_84631, _84627) = set_difference(_84629, _84625)), _84631 = _84629, _84627 = _84625], (96 ^ _81764) ^ [_84984, _84986, _84988, _84990] : [-(set_intersection2(_84990, _84986) = set_intersection2(_84988, _84984)), _84990 = _84988, _84986 = _84984], (106 ^ _81764) ^ [_85323, _85325, _85327, _85329] : [-(set_union2(_85329, _85325) = set_union2(_85327, _85323)), _85329 = _85327, _85325 = _85323], (2 ^ _81764) ^ [_81908] : [-(_81908 = _81908)], (4 ^ _81764) ^ [_82015, _82017] : [_82017 = _82015, -(_82015 = _82017)], (10 ^ _81764) ^ [_82219, _82221, _82223] : [-(_82223 = _82219), _82223 = _82221, _82221 = _82219], (20 ^ _81764) ^ [_82560, _82562, _82564, _82566] : [-(disjoint(_82564, _82560)), disjoint(_82566, _82562), _82566 = _82564, _82562 = _82560], (34 ^ _81764) ^ [_83004, _83006, _83008, _83010] : [-(in(_83008, _83004)), in(_83010, _83006), _83010 = _83008, _83006 = _83004], (48 ^ _81764) ^ [_83420, _83422] : [-(empty(_83420)), _83422 = _83420, empty(_83422)], (58 ^ _81764) ^ [_83743, _83745, _83747, _83749] : [-(subset(_83747, _83743)), subset(_83749, _83745), _83749 = _83747, _83745 = _83743], (72 ^ _81764) ^ [_84167, _84169, _84171, _84173] : [-(proper_subset(_84171, _84167)), proper_subset(_84173, _84169), _84173 = _84171, _84169 = _84167], (116 ^ _81764) ^ [_85664, _85666] : [in(_85666, _85664), in(_85664, _85666)], (122 ^ _81764) ^ [_85875, _85877] : [proper_subset(_85877, _85875), proper_subset(_85875, _85877)], (128 ^ _81764) ^ [_86071, _86073] : [-(set_union2(_86073, _86071) = set_union2(_86071, _86073))], (130 ^ _81764) ^ [_86171, _86173] : [-(set_intersection2(_86173, _86171) = set_intersection2(_86171, _86173))], (132 ^ _81764) ^ [_86315, _86317] : [_86317 = _86315, 135 ^ _81764 : [(136 ^ _81764) ^ [] : [-(subset(_86317, _86315))], (138 ^ _81764) ^ [] : [-(subset(_86315, _86317))]]], (140 ^ _81764) ^ [_86552, _86554] : [-(_86554 = _86552), subset(_86554, _86552), subset(_86552, _86554)], (150 ^ _81764) ^ [_86868] : [_86868 = empty_set, 153 ^ _81764 : [(154 ^ _81764) ^ [_86981] : [in(_86981, _86868)]]], (156 ^ _81764) ^ [_87047] : [-(in(157 ^ [_87047], _87047)), -(_87047 = empty_set)], (185 ^ _81764) ^ [_88077, _88079, _88081] : [-(_88077 = set_union2(_88081, _88079)), 189 ^ _81764 : [(190 ^ _81764) ^ [] : [-(in(186 ^ [_88077, _88079, _88081], _88077))], (192 ^ _81764) ^ [] : [in(186 ^ [_88077, _88079, _88081], _88081)], (194 ^ _81764) ^ [] : [in(186 ^ [_88077, _88079, _88081], _88079)]], 195 ^ _81764 : [(202 ^ _81764) ^ [] : [in(186 ^ [_88077, _88079, _88081], _88077)], (196 ^ _81764) ^ [] : [-(in(186 ^ [_88077, _88079, _88081], _88081)), -(in(186 ^ [_88077, _88079, _88081], _88079))]]], (163 ^ _81764) ^ [_87352, _87354, _87356] : [_87352 = set_union2(_87356, _87354), 166 ^ _81764 : [(177 ^ _81764) ^ [_87812] : [178 ^ _81764 : [(179 ^ _81764) ^ [] : [in(_87812, _87356)], (181 ^ _81764) ^ [] : [in(_87812, _87354)]], -(in(_87812, _87352))], (167 ^ _81764) ^ [_87534] : [in(_87534, _87352), -(in(_87534, _87356)), -(in(_87534, _87354))]]], (216 ^ _81764) ^ [_89171, _89173] : [218 ^ _81764 : [(219 ^ _81764) ^ [] : [-(in(217 ^ [_89171, _89173], _89173))], (221 ^ _81764) ^ [] : [in(217 ^ [_89171, _89173], _89171)]], -(subset(_89173, _89171))], (206 ^ _81764) ^ [_88857, _88859] : [subset(_88859, _88857), 209 ^ _81764 : [(210 ^ _81764) ^ [_88994] : [in(_88994, _88859), -(in(_88994, _88857))]]], (247 ^ _81764) ^ [_90296, _90298, _90300] : [-(_90296 = set_intersection2(_90300, _90298)), 259 ^ _81764 : [(260 ^ _81764) ^ [] : [-(in(248 ^ [_90296, _90298, _90300], _90300))], (262 ^ _81764) ^ [] : [-(in(248 ^ [_90296, _90298, _90300], _90298))], (264 ^ _81764) ^ [] : [in(248 ^ [_90296, _90298, _90300], _90296)]], 251 ^ _81764 : [(252 ^ _81764) ^ [] : [-(in(248 ^ [_90296, _90298, _90300], _90296))], (254 ^ _81764) ^ [] : [in(248 ^ [_90296, _90298, _90300], _90300), in(248 ^ [_90296, _90298, _90300], _90298)]]], (225 ^ _81764) ^ [_89571, _89573, _89575] : [_89571 = set_intersection2(_89575, _89573), 228 ^ _81764 : [(229 ^ _81764) ^ [_89753] : [in(_89753, _89571), 232 ^ _81764 : [(233 ^ _81764) ^ [] : [-(in(_89753, _89575))], (235 ^ _81764) ^ [] : [-(in(_89753, _89573))]]], (237 ^ _81764) ^ [_90012] : [-(in(_90012, _89571)), in(_90012, _89575), in(_90012, _89573)]]], (290 ^ _81764) ^ [_91823, _91825, _91827] : [-(_91823 = set_difference(_91827, _91825)), 302 ^ _81764 : [(303 ^ _81764) ^ [] : [-(in(291 ^ [_91823, _91825, _91827], _91827))], (305 ^ _81764) ^ [] : [in(291 ^ [_91823, _91825, _91827], _91825)], (307 ^ _81764) ^ [] : [in(291 ^ [_91823, _91825, _91827], _91823)]], 294 ^ _81764 : [(295 ^ _81764) ^ [] : [-(in(291 ^ [_91823, _91825, _91827], _91823))], (297 ^ _81764) ^ [] : [in(291 ^ [_91823, _91825, _91827], _91827), -(in(291 ^ [_91823, _91825, _91827], _91825))]]], (268 ^ _81764) ^ [_91092, _91094, _91096] : [_91092 = set_difference(_91096, _91094), 271 ^ _81764 : [(272 ^ _81764) ^ [_91276] : [in(_91276, _91092), 275 ^ _81764 : [(276 ^ _81764) ^ [] : [-(in(_91276, _91096))], (278 ^ _81764) ^ [] : [in(_91276, _91094)]]], (280 ^ _81764) ^ [_91536] : [-(in(_91536, _91092)), in(_91536, _91096), -(in(_91536, _91094))]]], (311 ^ _81764) ^ [_92609, _92611] : [disjoint(_92611, _92609), -(set_intersection2(_92611, _92609) = empty_set)], (317 ^ _81764) ^ [_92777, _92779] : [set_intersection2(_92779, _92777) = empty_set, -(disjoint(_92779, _92777))], (323 ^ _81764) ^ [_93024, _93026] : [proper_subset(_93026, _93024), 326 ^ _81764 : [(327 ^ _81764) ^ [] : [-(subset(_93026, _93024))], (329 ^ _81764) ^ [] : [_93026 = _93024]]], (331 ^ _81764) ^ [_93262, _93264] : [-(proper_subset(_93264, _93262)), subset(_93264, _93262), -(_93264 = _93262)], (341 ^ _81764) ^ [] : [true___, -(true___)], (347 ^ _81764) ^ [] : [true___, -(true___)], (353 ^ _81764) ^ [] : [true___, -(true___)], (359 ^ _81764) ^ [] : [true___, -(true___)], (365 ^ _81764) ^ [] : [-(empty(empty_set))], (367 ^ _81764) ^ [_94095, _94097] : [-(empty(_94097)), empty(set_union2(_94097, _94095))], (373 ^ _81764) ^ [_94311, _94313] : [-(empty(_94313)), empty(set_union2(_94311, _94313))], (379 ^ _81764) ^ [_94512, _94514] : [-(set_union2(_94514, _94514) = _94514)], (381 ^ _81764) ^ [_94609, _94611] : [-(set_intersection2(_94611, _94611) = _94611)], (383 ^ _81764) ^ [_94705, _94707] : [proper_subset(_94707, _94707)], (385 ^ _81764) ^ [_94843, _94845] : [set_difference(_94845, _94843) = empty_set, -(subset(_94845, _94843))], (391 ^ _81764) ^ [_95011, _95013] : [subset(_95013, _95011), -(set_difference(_95013, _95011) = empty_set)], (398 ^ _81764) ^ [] : [-(empty(396 ^ []))], (401 ^ _81764) ^ [] : [empty(399 ^ [])], (403 ^ _81764) ^ [_95393, _95395] : [-(subset(_95395, _95395))], (405 ^ _81764) ^ [_95502, _95504] : [disjoint(_95504, _95502), -(disjoint(_95502, _95504))], (411 ^ _81764) ^ [_95712, _95714] : [subset(_95714, _95712), -(set_union2(_95714, _95712) = _95712)], (417 ^ _81764) ^ [_95913, _95915] : [-(subset(set_intersection2(_95915, _95913), _95915))], (419 ^ _81764) ^ [_96039, _96041, _96043] : [-(subset(_96043, set_intersection2(_96041, _96039))), subset(_96043, _96041), subset(_96043, _96039)], (429 ^ _81764) ^ [_96325] : [-(set_union2(_96325, empty_set) = _96325)], (431 ^ _81764) ^ [_96449, _96451, _96453] : [-(subset(_96453, _96449)), subset(_96453, _96451), subset(_96451, _96449)], (441 ^ _81764) ^ [_96772, _96774, _96776] : [subset(_96776, _96774), -(subset(set_intersection2(_96776, _96772), set_intersection2(_96774, _96772)))], (447 ^ _81764) ^ [_97000, _97002] : [subset(_97002, _97000), -(set_intersection2(_97002, _97000) = _97002)], (453 ^ _81764) ^ [_97187] : [-(set_intersection2(_97187, empty_set) = empty_set)], (455 ^ _81764) ^ [_97297, _97299] : [-(_97299 = _97297), 459 ^ _81764 : [(460 ^ _81764) ^ [] : [-(in(456 ^ [_97297, _97299], _97299))], (462 ^ _81764) ^ [] : [in(456 ^ [_97297, _97299], _97297)]], 463 ^ _81764 : [(464 ^ _81764) ^ [] : [-(in(456 ^ [_97297, _97299], _97297))], (466 ^ _81764) ^ [] : [in(456 ^ [_97297, _97299], _97299)]]], (470 ^ _81764) ^ [_97798] : [-(subset(empty_set, _97798))], (472 ^ _81764) ^ [_97919, _97921, _97923] : [subset(_97923, _97921), -(subset(set_difference(_97923, _97919), set_difference(_97921, _97919)))], (478 ^ _81764) ^ [_98132, _98134] : [-(subset(set_difference(_98134, _98132), _98134))], (480 ^ _81764) ^ [_98273, _98275] : [set_difference(_98275, _98273) = empty_set, -(subset(_98275, _98273))], (486 ^ _81764) ^ [_98441, _98443] : [subset(_98443, _98441), -(set_difference(_98443, _98441) = empty_set)], (492 ^ _81764) ^ [_98644, _98646] : [-(set_union2(_98646, set_difference(_98644, _98646)) = set_union2(_98646, _98644))], (494 ^ _81764) ^ [_98733] : [-(set_difference(_98733, empty_set) = _98733)], (496 ^ _81764) ^ [_98863, _98865] : [-(disjoint(_98865, _98863)), 500 ^ _81764 : [(501 ^ _81764) ^ [] : [-(in(499 ^ [_98863, _98865], _98865))], (503 ^ _81764) ^ [] : [-(in(499 ^ [_98863, _98865], _98863))]]], (505 ^ _81764) ^ [_99177, _99179] : [disjoint(_99179, _99177), 506 ^ _81764 : [(507 ^ _81764) ^ [_99269] : [in(_99269, _99179), in(_99269, _99177)]]], (515 ^ _81764) ^ [_99526] : [subset(_99526, empty_set), -(_99526 = empty_set)], (521 ^ _81764) ^ [_99715, _99717] : [-(set_difference(set_union2(_99717, _99715), _99715) = set_difference(_99717, _99715))], (523 ^ _81764) ^ [_99833, _99835] : [subset(_99835, _99833), -(_99833 = set_union2(_99835, set_difference(_99833, _99835)))], (529 ^ _81764) ^ [_100040, _100042] : [-(set_difference(_100042, set_difference(_100042, _100040)) = set_intersection2(_100042, _100040))], (531 ^ _81764) ^ [_100129] : [-(set_difference(empty_set, _100129) = empty_set)], (533 ^ _81764) ^ [_100259, _100261] : [-(disjoint(_100261, _100259)), -(in(536 ^ [_100259, _100261], set_intersection2(_100261, _100259)))], (540 ^ _81764) ^ [_100494, _100496] : [541 ^ _81764 : [(542 ^ _81764) ^ [_100567] : [in(_100567, set_intersection2(_100496, _100494))]], disjoint(_100496, _100494)], (546 ^ _81764) ^ [_100719] : [empty(_100719), -(_100719 = empty_set)], (552 ^ _81764) ^ [_100921, _100923] : [in(_100923, _100921), empty(_100921)], (558 ^ _81764) ^ [_101113, _101115] : [-(subset(_101115, set_union2(_101115, _101113)))], (560 ^ _81764) ^ [_101225, _101227] : [empty(_101227), -(_101227 = _101225), empty(_101225)], (570 ^ _81764) ^ [_101516, _101518, _101520] : [-(subset(set_union2(_101520, _101516), _101518)), subset(_101520, _101518), subset(_101516, _101518)]], input).
% 0.43/1.38 ncf('1',plain,[proper_subset(580 ^ [], 579 ^ []), 329 : 580 ^ [] = 579 ^ []],start(323 ^ 0,bind([[_93024, _93026], [579 ^ [], 580 ^ []]]))).
% 0.43/1.38 ncf('1.1',plain,[-(proper_subset(580 ^ [], 579 ^ []))],extension(584 ^ 1)).
% 0.43/1.38 ncf('1.2',plain,[-(580 ^ [] = 579 ^ []), subset(580 ^ [], 579 ^ []), subset(579 ^ [], 580 ^ [])],extension(140 ^ 3,bind([[_86552, _86554], [579 ^ [], 580 ^ []]]))).
% 0.43/1.38 ncf('1.2.1',plain,[-(subset(580 ^ [], 579 ^ []))],extension(327 ^ 4)).
% 0.43/1.38 ncf('1.2.2',plain,[-(subset(579 ^ [], 580 ^ []))],extension(582 ^ 4)).
% 0.43/1.38 %-----------------------------------------------------
% 0.43/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------