%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU174+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:31 EDT 2023
% Result : Theorem 49.67s 48.96s
% Output : Proof 49.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU174+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 12:44:02 EDT 2023
% 0.13/0.34 % CPUTime :
% 49.67/48.96
% 49.67/48.96 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 49.67/48.96 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.67/48.96 %-----------------------------------------------------
% 49.67/48.96 ncf(matrix, plain, [(315 ^ _62678) ^ [] : [-(complements_of_subsets(308 ^ [], 309 ^ []) = empty_set)], (313 ^ _62678) ^ [] : [309 ^ [] = empty_set], (311 ^ _62678) ^ [] : [-(element(309 ^ [], powerset(powerset(308 ^ []))))], !, (192 ^ _52206) ^ [] : [true___, -(true___)], (245 ^ _52206) ^ [_60510, _60512] : [element(_60512, _60510), -(empty(_60510)), -(in(_60512, _60510))], (199 ^ _52206) ^ [_58795] : [-(element(197 ^ [_58795], _58795))], (104 ^ _52206) ^ [_55739, _55741] : [subset(_55741, _55739), 107 ^ _52206 : [(108 ^ _52206) ^ [_55876] : [in(_55876, _55741), -(in(_55876, _55739))]]], (180 ^ _52206) ^ [_58210, _58212] : [element(_58210, powerset(_58212)), -(element(subset_complement(_58212, _58210), powerset(_58212)))], (255 ^ _52206) ^ [_60837, _60839] : [element(_60839, powerset(_60837)), -(subset(_60839, _60837))], (98 ^ _52206) ^ [_55499, _55501] : [in(_55501, _55499), in(_55499, _55501)], (114 ^ _52206) ^ [_56053, _56055] : [116 ^ _52206 : [(119 ^ _52206) ^ [] : [in(115 ^ [_56053, _56055], _56053)], (117 ^ _52206) ^ [] : [-(in(115 ^ [_56053, _56055], _56055))]], -(subset(_56055, _56053))], (267 ^ _52206) ^ [_61233, _61235, _61237] : [-(element(_61237, _61233)), in(_61237, _61235), element(_61235, powerset(_61233))], (299 ^ _52206) ^ [_62245, _62247] : [empty(_62247), -(_62247 = _62245), empty(_62245)], (293 ^ _52206) ^ [_62058, _62060] : [in(_62060, _62058), empty(_62058)], (10 ^ _52206) ^ [_52641, _52643, _52645] : [-(_52645 = _52641), _52645 = _52643, _52643 = _52641], (235 ^ _52206) ^ [] : [empty(233 ^ [])], (48 ^ _52206) ^ [_53842, _53844] : [-(empty(_53842)), _53844 = _53842, empty(_53844)], (4 ^ _52206) ^ [_52437, _52439] : [_52439 = _52437, -(_52437 = _52439)], (205 ^ _52206) ^ [_59038, _59040] : [element(_59038, powerset(_59040)), -(subset_complement(_59040, subset_complement(_59040, _59038)) = _59038)], (232 ^ _52206) ^ [_60003] : [-(empty(228 ^ [_60003]))], (277 ^ _52206) ^ [_61560, _61562, _61564] : [in(_61564, _61562), element(_61562, powerset(_61560)), empty(_61560)], (261 ^ _52206) ^ [_61003, _61005] : [subset(_61005, _61003), -(element(_61005, powerset(_61003)))], (174 ^ _52206) ^ [] : [true___, -(true___)], (201 ^ _52206) ^ [_58877] : [empty(powerset(_58877))], (168 ^ _52206) ^ [] : [true___, -(true___)], (82 ^ _52206) ^ [_54932, _54934] : [_54934 = _54932, -(powerset(_54934) = powerset(_54932))], (88 ^ _52206) ^ [_55158, _55160, _55162, _55164] : [-(complements_of_subsets(_55164, _55160) = complements_of_subsets(_55162, _55158)), _55164 = _55162, _55160 = _55158], (230 ^ _52206) ^ [_59952] : [-(element(228 ^ [_59952], powerset(_59952)))], (227 ^ _52206) ^ [] : [-(empty(225 ^ []))], (34 ^ _52206) ^ [_53426, _53428, _53430, _53432] : [-(in(_53430, _53426)), in(_53432, _53428), _53432 = _53430, _53428 = _53426], (72 ^ _52206) ^ [_54601, _54603, _54605, _54607] : [-(subset_complement(_54607, _54603) = subset_complement(_54605, _54601)), _54607 = _54605, _54603 = _54601], (237 ^ _52206) ^ [_60191, _60193] : [-(subset(_60193, _60193))], (217 ^ _52206) ^ [_59480] : [-(empty(_59480)), 221 ^ _52206 : [(224 ^ _52206) ^ [] : [empty(220 ^ [_59480])], (222 ^ _52206) ^ [] : [-(element(220 ^ [_59480], powerset(_59480)))]]], (58 ^ _52206) ^ [_54145, _54147, _54149, _54151] : [-(element(_54149, _54145)), element(_54151, _54147), _54151 = _54149, _54147 = _54145], (20 ^ _52206) ^ [_52982, _52984, _52986, _52988] : [-(subset(_52986, _52982)), subset(_52988, _52984), _52988 = _52986, _52984 = _52982], (211 ^ _52206) ^ [_59264, _59266] : [element(_59264, powerset(powerset(_59266))), -(complements_of_subsets(_59266, complements_of_subsets(_59266, _59264)) = _59264)], (203 ^ _52206) ^ [] : [-(empty(empty_set))], (123 ^ _52206) ^ [_56410, _56412] : [element(_56410, powerset(powerset(_56412))), 126 ^ _52206 : [(127 ^ _52206) ^ [_56590] : [element(_56590, powerset(powerset(_56412))), 130 ^ _52206 : [(131 ^ _52206) ^ [] : [_56590 = complements_of_subsets(_56412, _56410), 134 ^ _52206 : [(135 ^ _52206) ^ [_56878] : [element(_56878, powerset(_56412)), 138 ^ _52206 : [(145 ^ _52206) ^ [] : [in(subset_complement(_56412, _56878), _56410), -(in(_56878, _56590))], (139 ^ _52206) ^ [] : [in(_56878, _56590), -(in(subset_complement(_56412, _56878), _56410))]]]]], (151 ^ _52206) ^ [] : [-(_56590 = complements_of_subsets(_56412, _56410)), 153 ^ _52206 : [(156 ^ _52206) ^ [] : [157 ^ _52206 : [(160 ^ _52206) ^ [] : [in(subset_complement(_56412, 152 ^ [_56410, _56412, _56590]), _56410)], (158 ^ _52206) ^ [] : [-(in(152 ^ [_56410, _56412, _56590], _56590))]], 161 ^ _52206 : [(164 ^ _52206) ^ [] : [in(152 ^ [_56410, _56412, _56590], _56590)], (162 ^ _52206) ^ [] : [-(in(subset_complement(_56412, 152 ^ [_56410, _56412, _56590]), _56410))]]], (154 ^ _52206) ^ [] : [-(element(152 ^ [_56410, _56412, _56590], powerset(_56412)))]]]]]]], (287 ^ _52206) ^ [_61856] : [empty(_61856), -(_61856 = empty_set)], (186 ^ _52206) ^ [_58434, _58436] : [element(_58434, powerset(powerset(_58436))), -(element(complements_of_subsets(_58436, _58434), powerset(powerset(_58436))))], (2 ^ _52206) ^ [_52330] : [-(_52330 = _52330)], (239 ^ _52206) ^ [_60300, _60302] : [in(_60302, _60300), -(element(_60302, _60300))]], input).
% 49.67/48.96 ncf('1',plain,[-(element(309 ^ [], powerset(powerset(308 ^ []))))],start(311 ^ 0)).
% 49.67/48.96 ncf('1.1',plain,[element(309 ^ [], powerset(powerset(308 ^ []))), -(element(complements_of_subsets(308 ^ [], 309 ^ []), powerset(powerset(308 ^ []))))],extension(186 ^ 1,bind([[_58434, _58436], [309 ^ [], 308 ^ []]]))).
% 49.67/48.96 ncf('1.1.1',plain,[element(complements_of_subsets(308 ^ [], 309 ^ []), powerset(powerset(308 ^ []))), 127 : element(complements_of_subsets(308 ^ [], 309 ^ []), powerset(powerset(308 ^ []))), 151 : -(complements_of_subsets(308 ^ [], 309 ^ []) = complements_of_subsets(308 ^ [], complements_of_subsets(308 ^ [], 309 ^ []))), 158 : -(in(152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])], complements_of_subsets(308 ^ [], 309 ^ []))), 162 : -(in(subset_complement(308 ^ [], 152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])]), complements_of_subsets(308 ^ [], 309 ^ [])))],extension(123 ^ 2,bind([[_56410, _56412, _56590], [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])]]))).
% 49.67/48.96 ncf('1.1.1.1',plain,[-(element(complements_of_subsets(308 ^ [], 309 ^ []), powerset(powerset(308 ^ []))))],reduction('1.1')).
% 49.67/48.96 ncf('1.1.1.2',plain,[complements_of_subsets(308 ^ [], 309 ^ []) = complements_of_subsets(308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])), -(complements_of_subsets(308 ^ [], 309 ^ []) = 309 ^ []), complements_of_subsets(308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])) = 309 ^ []],extension(10 ^ 7,bind([[_52641, _52643, _52645], [309 ^ [], complements_of_subsets(308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])), complements_of_subsets(308 ^ [], 309 ^ [])]]))).
% 49.67/48.96 ncf('1.1.1.2.1',plain,[complements_of_subsets(308 ^ [], 309 ^ []) = 309 ^ [], -(309 ^ [] = complements_of_subsets(308 ^ [], 309 ^ []))],extension(4 ^ 8,bind([[_52437, _52439], [309 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])]]))).
% 49.67/48.96 ncf('1.1.1.2.1.1',plain,[309 ^ [] = complements_of_subsets(308 ^ [], 309 ^ []), -(309 ^ [] = empty_set), complements_of_subsets(308 ^ [], 309 ^ []) = empty_set],extension(10 ^ 9,bind([[_52641, _52643, _52645], [empty_set, complements_of_subsets(308 ^ [], 309 ^ []), 309 ^ []]]))).
% 49.67/48.96 ncf('1.1.1.2.1.1.1',plain,[309 ^ [] = empty_set],extension(313 ^ 10)).
% 49.67/48.96 ncf('1.1.1.2.1.1.2',plain,[-(complements_of_subsets(308 ^ [], 309 ^ []) = empty_set)],extension(315 ^ 10)).
% 49.67/48.96 ncf('1.1.1.2.2',plain,[-(complements_of_subsets(308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])) = 309 ^ []), element(309 ^ [], powerset(powerset(308 ^ [])))],extension(211 ^ 8,bind([[_59264, _59266], [309 ^ [], 308 ^ []]]))).
% 49.67/48.96 ncf('1.1.1.2.2.1',plain,[-(element(309 ^ [], powerset(powerset(308 ^ []))))],reduction('1')).
% 49.67/48.96 ncf('1.1.1.3',plain,[in(152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])], complements_of_subsets(308 ^ [], 309 ^ [])), empty(complements_of_subsets(308 ^ [], 309 ^ []))],extension(293 ^ 11,bind([[_62058, _62060], [complements_of_subsets(308 ^ [], 309 ^ []), 152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])]]]))).
% 49.67/48.96 ncf('1.1.1.3.1',plain,[-(empty(complements_of_subsets(308 ^ [], 309 ^ []))), empty_set = complements_of_subsets(308 ^ [], 309 ^ []), empty(empty_set)],extension(48 ^ 12,bind([[_53842, _53844], [complements_of_subsets(308 ^ [], 309 ^ []), empty_set]]))).
% 49.67/48.96 ncf('1.1.1.3.1.1',plain,[-(empty_set = complements_of_subsets(308 ^ [], 309 ^ [])), complements_of_subsets(308 ^ [], 309 ^ []) = empty_set],extension(4 ^ 13,bind([[_52437, _52439], [empty_set, complements_of_subsets(308 ^ [], 309 ^ [])]]))).
% 49.67/48.96 ncf('1.1.1.3.1.1.1',plain,[-(complements_of_subsets(308 ^ [], 309 ^ []) = empty_set)],extension(315 ^ 14)).
% 49.67/48.96 ncf('1.1.1.3.1.2',plain,[-(empty(empty_set))],extension(203 ^ 13)).
% 49.67/48.96 ncf('1.1.1.4',plain,[in(subset_complement(308 ^ [], 152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])]), complements_of_subsets(308 ^ [], 309 ^ [])), empty(complements_of_subsets(308 ^ [], 309 ^ []))],extension(293 ^ 11,bind([[_62058, _62060], [complements_of_subsets(308 ^ [], 309 ^ []), subset_complement(308 ^ [], 152 ^ [complements_of_subsets(308 ^ [], 309 ^ []), 308 ^ [], complements_of_subsets(308 ^ [], 309 ^ [])])]]))).
% 49.67/48.96 ncf('1.1.1.4.1',plain,[-(empty(complements_of_subsets(308 ^ [], 309 ^ []))), empty_set = complements_of_subsets(308 ^ [], 309 ^ []), empty(empty_set)],extension(48 ^ 12,bind([[_53842, _53844], [complements_of_subsets(308 ^ [], 309 ^ []), empty_set]]))).
% 49.67/48.96 ncf('1.1.1.4.1.1',plain,[-(empty_set = complements_of_subsets(308 ^ [], 309 ^ [])), complements_of_subsets(308 ^ [], 309 ^ []) = empty_set],extension(4 ^ 13,bind([[_52437, _52439], [empty_set, complements_of_subsets(308 ^ [], 309 ^ [])]]))).
% 49.67/48.96 ncf('1.1.1.4.1.1.1',plain,[-(complements_of_subsets(308 ^ [], 309 ^ []) = empty_set)],extension(315 ^ 14)).
% 49.67/48.96 ncf('1.1.1.4.1.2',plain,[-(empty(empty_set))],extension(203 ^ 13)).
% 49.67/48.96 %-----------------------------------------------------
% 49.67/48.96 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------