%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU172+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:30 EDT 2023
% Result : Theorem 0.36s 1.38s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU172+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.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.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 13:20:21 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.36/1.38
% 0.36/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 ncf(matrix, plain, [(231 ^ _34621) ^ [] : [-(element(229 ^ [], powerset(227 ^ [])))], (233 ^ _34621) ^ [] : [-(in(228 ^ [], subset_complement(227 ^ [], 229 ^ [])))], (235 ^ _34621) ^ [] : [-(in(228 ^ [], 229 ^ []))], (58 ^ _34621) ^ [_36590, _36592, _36594, _36596] : [-(set_difference(_36596, _36592) = set_difference(_36594, _36590)), _36596 = _36594, _36592 = _36590], (68 ^ _34621) ^ [_36921, _36923] : [_36923 = _36921, -(powerset(_36923) = powerset(_36921))], (74 ^ _34621) ^ [_37147, _37149, _37151, _37153] : [-(subset_complement(_37153, _37149) = subset_complement(_37151, _37147)), _37153 = _37151, _37149 = _37147], (2 ^ _34621) ^ [_34765] : [-(_34765 = _34765)], (4 ^ _34621) ^ [_34872, _34874] : [_34874 = _34872, -(_34872 = _34874)], (10 ^ _34621) ^ [_35076, _35078, _35080] : [-(_35080 = _35076), _35080 = _35078, _35078 = _35076], (20 ^ _34621) ^ [_35389, _35391] : [-(empty(_35389)), _35391 = _35389, empty(_35391)], (30 ^ _34621) ^ [_35712, _35714, _35716, _35718] : [-(element(_35716, _35712)), element(_35718, _35714), _35718 = _35716, _35714 = _35712], (44 ^ _34621) ^ [_36136, _36138, _36140, _36142] : [-(in(_36140, _36136)), in(_36142, _36138), _36142 = _36140, _36138 = _36136], (84 ^ _34621) ^ [] : [true___, -(true___)], (90 ^ _34621) ^ [] : [-(empty(empty_set))], (92 ^ _34621) ^ [_37631] : [-(set_difference(_37631, empty_set) = _37631)], (94 ^ _34621) ^ [_37712] : [-(set_difference(empty_set, _37712) = empty_set)], (96 ^ _34621) ^ [_37808] : [-(empty(_37808)), 100 ^ _34621 : [(101 ^ _34621) ^ [] : [-(element(99 ^ [_37808], powerset(_37808)))], (103 ^ _34621) ^ [] : [empty(99 ^ [_37808])]]], (106 ^ _34621) ^ [_38191] : [-(element(104 ^ [_38191], powerset(_38191)))], (108 ^ _34621) ^ [_38242] : [-(empty(104 ^ [_38242]))], (111 ^ _34621) ^ [] : [-(empty(109 ^ []))], (114 ^ _34621) ^ [] : [empty(112 ^ [])], (116 ^ _34621) ^ [_38520] : [empty(_38520), -(_38520 = empty_set)], (122 ^ _34621) ^ [_38722, _38724] : [empty(_38724), -(_38724 = _38722), empty(_38722)], (132 ^ _34621) ^ [_39019, _39021] : [element(_39019, powerset(_39021)), -(subset_complement(_39021, subset_complement(_39021, _39019)) = _39019)], (138 ^ _34621) ^ [_39245, _39247] : [in(_39247, _39245), in(_39245, _39247)], (145 ^ _34621) ^ [_39466] : [-(element(143 ^ [_39466], _39466))], (147 ^ _34621) ^ [] : [true___, -(true___)], (153 ^ _34621) ^ [_39697, _39699] : [element(_39697, powerset(_39699)), -(element(subset_complement(_39699, _39697), powerset(_39699)))], (159 ^ _34621) ^ [] : [true___, -(true___)], (165 ^ _34621) ^ [] : [true___, -(true___)], (171 ^ _34621) ^ [_40129] : [empty(powerset(_40129))], (173 ^ _34621) ^ [_40237, _40239] : [in(_40239, _40237), empty(_40237)], (179 ^ _34621) ^ [_40444, _40446] : [element(_40444, powerset(_40446)), -(subset_complement(_40446, _40444) = set_difference(_40446, _40444))], (207 ^ _34621) ^ [_41424, _41426, _41428] : [-(_41424 = set_difference(_41428, _41426)), 219 ^ _34621 : [(220 ^ _34621) ^ [] : [-(in(208 ^ [_41424, _41426, _41428], _41428))], (222 ^ _34621) ^ [] : [in(208 ^ [_41424, _41426, _41428], _41426)], (224 ^ _34621) ^ [] : [in(208 ^ [_41424, _41426, _41428], _41424)]], 211 ^ _34621 : [(212 ^ _34621) ^ [] : [-(in(208 ^ [_41424, _41426, _41428], _41424))], (214 ^ _34621) ^ [] : [in(208 ^ [_41424, _41426, _41428], _41428), -(in(208 ^ [_41424, _41426, _41428], _41426))]]], (185 ^ _34621) ^ [_40693, _40695, _40697] : [_40693 = set_difference(_40697, _40695), 188 ^ _34621 : [(189 ^ _34621) ^ [_40877] : [in(_40877, _40693), 192 ^ _34621 : [(193 ^ _34621) ^ [] : [-(in(_40877, _40697))], (195 ^ _34621) ^ [] : [in(_40877, _40695)]]], (197 ^ _34621) ^ [_41137] : [-(in(_41137, _40693)), in(_41137, _40697), -(in(_41137, _40695))]]]], input).
% 0.36/1.38 ncf('1',plain,[set_difference(227 ^ [], 229 ^ []) = set_difference(227 ^ [], 229 ^ []), 189 : in(228 ^ [], set_difference(227 ^ [], 229 ^ [])), 195 : in(228 ^ [], 229 ^ [])],start(185 ^ 0,bind([[_40693, _40695, _40697, _40877], [set_difference(227 ^ [], 229 ^ []), 229 ^ [], 227 ^ [], 228 ^ []]]))).
% 0.36/1.38 ncf('1.1',plain,[-(set_difference(227 ^ [], 229 ^ []) = set_difference(227 ^ [], 229 ^ [])), 227 ^ [] = 227 ^ [], 229 ^ [] = 229 ^ []],extension(58 ^ 1,bind([[_36590, _36592, _36594, _36596], [229 ^ [], 229 ^ [], 227 ^ [], 227 ^ []]]))).
% 0.36/1.38 ncf('1.1.1',plain,[-(227 ^ [] = 227 ^ [])],extension(2 ^ 2,bind([[_34765], [227 ^ []]]))).
% 0.36/1.38 ncf('1.1.2',plain,[-(229 ^ [] = 229 ^ [])],extension(2 ^ 2,bind([[_34765], [229 ^ []]]))).
% 0.36/1.38 ncf('1.2',plain,[-(in(228 ^ [], set_difference(227 ^ [], 229 ^ []))), in(228 ^ [], subset_complement(227 ^ [], 229 ^ [])), 228 ^ [] = 228 ^ [], subset_complement(227 ^ [], 229 ^ []) = set_difference(227 ^ [], 229 ^ [])],extension(44 ^ 3,bind([[_36136, _36138, _36140, _36142], [set_difference(227 ^ [], 229 ^ []), subset_complement(227 ^ [], 229 ^ []), 228 ^ [], 228 ^ []]]))).
% 0.36/1.38 ncf('1.2.1',plain,[-(in(228 ^ [], subset_complement(227 ^ [], 229 ^ [])))],extension(233 ^ 4)).
% 0.36/1.38 ncf('1.2.2',plain,[-(228 ^ [] = 228 ^ [])],extension(2 ^ 4,bind([[_34765], [228 ^ []]]))).
% 0.36/1.38 ncf('1.2.3',plain,[-(subset_complement(227 ^ [], 229 ^ []) = set_difference(227 ^ [], 229 ^ [])), element(229 ^ [], powerset(227 ^ []))],extension(179 ^ 4,bind([[_40444, _40446], [229 ^ [], 227 ^ []]]))).
% 0.36/1.38 ncf('1.2.3.1',plain,[-(element(229 ^ [], powerset(227 ^ [])))],extension(231 ^ 5)).
% 0.36/1.38 ncf('1.3',plain,[-(in(228 ^ [], 229 ^ []))],extension(235 ^ 5)).
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------