%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU129+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:17 EDT 2023
% Result : Theorem 43.33s 42.72s
% Output : Proof 43.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU129+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n012.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:11:32 EDT 2023
% 0.12/0.33 % CPUTime :
% 43.33/42.72
% 43.33/42.72 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 43.33/42.72 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 43.33/42.72 %-----------------------------------------------------
% 43.33/42.72 ncf(matrix, plain, [(411 ^ _76989) ^ [] : [subset(set_intersection2(405 ^ [], 407 ^ []), set_intersection2(406 ^ [], 407 ^ []))], (409 ^ _76989) ^ [] : [-(subset(405 ^ [], 406 ^ []))], !, (98 ^ _62900) ^ [_66167, _66169] : [-(set_union2(_66169, _66167) = set_union2(_66167, _66169))], (306 ^ _62900) ^ [_73280, _73282] : [-(subset(set_intersection2(_73282, _73280), _73282))], (284 ^ _62900) ^ [_72484, _72486] : [-(set_intersection2(_72486, _72486) = _72486)], (270 ^ _62900) ^ [_71970, _71972] : [-(empty(_71972)), empty(set_union2(_71972, _71970))], (359 ^ _62900) ^ [_75191, _75193] : [-(disjoint(_75193, _75191)), -(in(362 ^ [_75191, _75193], set_intersection2(_75193, _75191)))], (300 ^ _62900) ^ [_73079, _73081] : [subset(_73081, _73079), -(set_union2(_73081, _73079) = _73079)], (366 ^ _62900) ^ [_75426, _75428] : [367 ^ _62900 : [(368 ^ _62900) ^ [_75499] : [in(_75499, set_intersection2(_75428, _75426))]], disjoint(_75428, _75426)], (332 ^ _62900) ^ [_74177] : [-(subset(empty_set, _74177))], (186 ^ _62900) ^ [_69267, _69269] : [188 ^ _62900 : [(191 ^ _62900) ^ [] : [in(187 ^ [_69267, _69269], _69267)], (189 ^ _62900) ^ [] : [-(in(187 ^ [_69267, _69269], _69269))]], -(subset(_69269, _69267))], (396 ^ _62900) ^ [_76448, _76450, _76452] : [-(subset(set_union2(_76452, _76448), _76450)), subset(_76452, _76450), subset(_76448, _76450)], (330 ^ _62900) ^ [_74096] : [-(set_intersection2(_74096, empty_set) = empty_set)], (72 ^ _62900) ^ [_65295, _65297, _65299, _65301] : [-(set_union2(_65301, _65297) = set_union2(_65299, _65295)), _65301 = _65299, _65297 = _65295], (308 ^ _62900) ^ [_73406, _73408, _73410] : [-(subset(_73410, set_intersection2(_73408, _73406))), subset(_73410, _73408), subset(_73410, _73406)], (102 ^ _62900) ^ [_66411, _66413] : [_66413 = _66411, 105 ^ _62900 : [(108 ^ _62900) ^ [] : [-(subset(_66411, _66413))], (106 ^ _62900) ^ [] : [-(subset(_66413, _66411))]]], (372 ^ _62900) ^ [_75651] : [empty(_75651), -(_75651 = empty_set)], (386 ^ _62900) ^ [_76157, _76159] : [empty(_76159), -(_76159 = _76157), empty(_76157)], (217 ^ _62900) ^ [_70392, _70394, _70396] : [-(_70392 = set_intersection2(_70396, _70394)), 229 ^ _62900 : [(234 ^ _62900) ^ [] : [in(218 ^ [_70392, _70394, _70396], _70392)], (232 ^ _62900) ^ [] : [-(in(218 ^ [_70392, _70394, _70396], _70394))], (230 ^ _62900) ^ [] : [-(in(218 ^ [_70392, _70394, _70396], _70396))]], 221 ^ _62900 : [(224 ^ _62900) ^ [] : [in(218 ^ [_70392, _70394, _70396], _70396), in(218 ^ [_70392, _70394, _70396], _70394)], (222 ^ _62900) ^ [] : [-(in(218 ^ [_70392, _70394, _70396], _70392))]]], (282 ^ _62900) ^ [_72387, _72389] : [-(set_union2(_72389, _72389) = _72389)], (294 ^ _62900) ^ [_72869, _72871] : [disjoint(_72871, _72869), -(disjoint(_72869, _72871))], (334 ^ _62900) ^ [_74304, _74306] : [-(disjoint(_74306, _74304)), 338 ^ _62900 : [(341 ^ _62900) ^ [] : [-(in(337 ^ [_74304, _74306], _74304))], (339 ^ _62900) ^ [] : [-(in(337 ^ [_74304, _74306], _74306))]]], (58 ^ _62900) ^ [_64839, _64841, _64843, _64845] : [-(subset(_64843, _64839)), subset(_64845, _64841), _64845 = _64843, _64841 = _64839], (250 ^ _62900) ^ [] : [true___, -(true___)], (262 ^ _62900) ^ [] : [true___, -(true___)], (10 ^ _62900) ^ [_63335, _63337, _63339] : [-(_63339 = _63335), _63339 = _63337, _63337 = _63335], (195 ^ _62900) ^ [_69667, _69669, _69671] : [_69667 = set_intersection2(_69671, _69669), 198 ^ _62900 : [(207 ^ _62900) ^ [_70108] : [-(in(_70108, _69667)), in(_70108, _69671), in(_70108, _69669)], (199 ^ _62900) ^ [_69849] : [in(_69849, _69667), 202 ^ _62900 : [(205 ^ _62900) ^ [] : [-(in(_69849, _69669))], (203 ^ _62900) ^ [] : [-(in(_69849, _69671))]]]]], (292 ^ _62900) ^ [_72760, _72762] : [-(subset(_72762, _72762))], (34 ^ _62900) ^ [_64120, _64122, _64124, _64126] : [-(in(_64124, _64120)), in(_64126, _64122), _64126 = _64124, _64122 = _64120], (48 ^ _62900) ^ [_64536, _64538] : [-(empty(_64536)), _64538 = _64536, empty(_64538)], (155 ^ _62900) ^ [_68173, _68175, _68177] : [-(_68173 = set_union2(_68177, _68175)), 159 ^ _62900 : [(164 ^ _62900) ^ [] : [in(156 ^ [_68173, _68175, _68177], _68175)], (162 ^ _62900) ^ [] : [in(156 ^ [_68173, _68175, _68177], _68177)], (160 ^ _62900) ^ [] : [-(in(156 ^ [_68173, _68175, _68177], _68173))]], 165 ^ _62900 : [(166 ^ _62900) ^ [] : [-(in(156 ^ [_68173, _68175, _68177], _68177)), -(in(156 ^ [_68173, _68175, _68177], _68175))], (172 ^ _62900) ^ [] : [in(156 ^ [_68173, _68175, _68177], _68173)]]], (320 ^ _62900) ^ [_73816, _73818, _73820] : [-(subset(_73820, _73816)), subset(_73820, _73818), subset(_73818, _73816)], (343 ^ _62900) ^ [_74618, _74620] : [disjoint(_74620, _74618), 344 ^ _62900 : [(345 ^ _62900) ^ [_74710] : [in(_74710, _74620), in(_74710, _74618)]]], (176 ^ _62900) ^ [_68953, _68955] : [subset(_68955, _68953), 179 ^ _62900 : [(180 ^ _62900) ^ [_69090] : [in(_69090, _68955), -(in(_69090, _68953))]]], (120 ^ _62900) ^ [_66964] : [_66964 = empty_set, 123 ^ _62900 : [(124 ^ _62900) ^ [_67077] : [in(_67077, _66964)]]], (126 ^ _62900) ^ [_67143] : [-(in(127 ^ [_67143], _67143)), -(_67143 = empty_set)], (244 ^ _62900) ^ [_71342, _71344] : [set_intersection2(_71344, _71342) = empty_set, -(disjoint(_71344, _71342))], (92 ^ _62900) ^ [_65971, _65973] : [in(_65973, _65971), in(_65971, _65973)], (378 ^ _62900) ^ [_75853, _75855] : [in(_75855, _75853), empty(_75853)], (384 ^ _62900) ^ [_76045, _76047] : [-(subset(_76047, set_union2(_76047, _76045)))], (82 ^ _62900) ^ [_65634, _65636, _65638, _65640] : [-(set_intersection2(_65640, _65636) = set_intersection2(_65638, _65634)), _65640 = _65638, _65636 = _65634], (290 ^ _62900) ^ [] : [empty(288 ^ [])], (353 ^ _62900) ^ [_74967] : [subset(_74967, empty_set), -(_74967 = empty_set)], (287 ^ _62900) ^ [] : [-(empty(285 ^ []))], (268 ^ _62900) ^ [] : [-(empty(empty_set))], (238 ^ _62900) ^ [_71174, _71176] : [disjoint(_71176, _71174), -(set_intersection2(_71176, _71174) = empty_set)], (2 ^ _62900) ^ [_63024] : [-(_63024 = _63024)], (276 ^ _62900) ^ [_72186, _72188] : [-(empty(_72188)), empty(set_union2(_72186, _72188))], (100 ^ _62900) ^ [_66267, _66269] : [-(set_intersection2(_66269, _66267) = set_intersection2(_66267, _66269))], (133 ^ _62900) ^ [_67448, _67450, _67452] : [_67448 = set_union2(_67452, _67450), 136 ^ _62900 : [(137 ^ _62900) ^ [_67630] : [in(_67630, _67448), -(in(_67630, _67452)), -(in(_67630, _67450))], (147 ^ _62900) ^ [_67908] : [148 ^ _62900 : [(151 ^ _62900) ^ [] : [in(_67908, _67450)], (149 ^ _62900) ^ [] : [in(_67908, _67452)]], -(in(_67908, _67448))]]], (256 ^ _62900) ^ [] : [true___, -(true___)], (318 ^ _62900) ^ [_73692] : [-(set_union2(_73692, empty_set) = _73692)], (110 ^ _62900) ^ [_66648, _66650] : [-(_66650 = _66648), subset(_66650, _66648), subset(_66648, _66650)], (4 ^ _62900) ^ [_63131, _63133] : [_63133 = _63131, -(_63131 = _63133)], (20 ^ _62900) ^ [_63676, _63678, _63680, _63682] : [-(disjoint(_63680, _63676)), disjoint(_63682, _63678), _63682 = _63680, _63678 = _63676]], input).
% 43.33/42.72 ncf('1',plain,[subset(set_intersection2(405 ^ [], 407 ^ []), set_intersection2(406 ^ [], 407 ^ []))],start(411 ^ 0)).
% 43.33/42.72 ncf('1.1',plain,[-(subset(set_intersection2(405 ^ [], 407 ^ []), set_intersection2(406 ^ [], 407 ^ []))), subset(set_intersection2(405 ^ [], 407 ^ []), 406 ^ []), subset(set_intersection2(405 ^ [], 407 ^ []), 407 ^ [])],extension(308 ^ 1,bind([[_73406, _73408, _73410], [407 ^ [], 406 ^ [], set_intersection2(405 ^ [], 407 ^ [])]]))).
% 43.33/42.72 ncf('1.1.1',plain,[-(subset(set_intersection2(405 ^ [], 407 ^ []), 406 ^ [])), subset(set_intersection2(405 ^ [], 407 ^ []), 405 ^ []), subset(405 ^ [], 406 ^ [])],extension(320 ^ 2,bind([[_73816, _73818, _73820], [406 ^ [], 405 ^ [], set_intersection2(405 ^ [], 407 ^ [])]]))).
% 43.33/42.72 ncf('1.1.1.1',plain,[-(subset(set_intersection2(405 ^ [], 407 ^ []), 405 ^ []))],extension(306 ^ 3,bind([[_73280, _73282], [407 ^ [], 405 ^ []]]))).
% 43.33/42.72 ncf('1.1.1.2',plain,[-(subset(405 ^ [], 406 ^ []))],extension(409 ^ 3)).
% 43.33/42.72 ncf('1.1.2',plain,[-(subset(set_intersection2(405 ^ [], 407 ^ []), 407 ^ [])), 191 : in(187 ^ [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])], 407 ^ [])],extension(186 ^ 2,bind([[_69267, _69269], [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])]]))).
% 43.33/42.72 ncf('1.1.2.1',plain,[-(in(187 ^ [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])], 407 ^ [])), 199 : in(187 ^ [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])], set_intersection2(405 ^ [], 407 ^ [])), 199 : set_intersection2(405 ^ [], 407 ^ []) = set_intersection2(405 ^ [], 407 ^ [])],extension(195 ^ 5,bind([[_69667, _69669, _69671, _69849], [set_intersection2(405 ^ [], 407 ^ []), 407 ^ [], 405 ^ [], 187 ^ [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])]]]))).
% 43.33/42.72 ncf('1.1.2.1.1',plain,[-(in(187 ^ [407 ^ [], set_intersection2(405 ^ [], 407 ^ [])], set_intersection2(405 ^ [], 407 ^ [])))],extension(189 ^ 8)).
% 43.33/42.72 ncf('1.1.2.1.2',plain,[-(set_intersection2(405 ^ [], 407 ^ []) = set_intersection2(405 ^ [], 407 ^ []))],extension(2 ^ 6,bind([[_63024], [set_intersection2(405 ^ [], 407 ^ [])]]))).
% 43.33/42.72 %-----------------------------------------------------
% 43.33/42.72 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------