%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET889+1 : TPTP v8.1.2. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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 11:56:37 EDT 2023
% Result : Theorem 44.19s 43.76s
% Output : Proof 44.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET889+1 : TPTP v8.1.2. Bugfixed v4.0.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n019.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 18:58:27 EDT 2023
% 0.13/0.33 % CPUTime :
% 44.19/43.76
% 44.19/43.76 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 44.19/43.76 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.19/43.76 %-----------------------------------------------------
% 44.19/43.76 ncf(matrix, plain, [(206 ^ _40893) ^ [] : [powerset(singleton(204 ^ [])) = unordered_pair(empty_set, singleton(204 ^ []))], !, (4 ^ _33843) ^ [_34074, _34076] : [_34076 = _34074, -(_34074 = _34076)], (174 ^ _33843) ^ [_39807, _39809] : [175 ^ _33843 : [(178 ^ _33843) ^ [] : [_39809 = singleton(_39807)], (176 ^ _33843) ^ [] : [_39809 = empty_set]], -(subset(_39809, singleton(_39807)))], (58 ^ _33843) ^ [_35764, _35766] : [_35766 = _35764, -(powerset(_35766) = powerset(_35764))], (190 ^ _33843) ^ [_40354, _40356] : [-(_40356 = _40354), 194 ^ _33843 : [(197 ^ _33843) ^ [] : [in(191 ^ [_40354, _40356], _40354)], (195 ^ _33843) ^ [] : [-(in(191 ^ [_40354, _40356], _40356))]], 198 ^ _33843 : [(201 ^ _33843) ^ [] : [in(191 ^ [_40354, _40356], _40356)], (199 ^ _33843) ^ [] : [-(in(191 ^ [_40354, _40356], _40354))]]], (119 ^ _33843) ^ [_37989, _37991, _37993] : [_37989 = unordered_pair(_37993, _37991), 122 ^ _33843 : [(123 ^ _33843) ^ [_38171] : [in(_38171, _37989), -(_38171 = _37993), -(_38171 = _37991)], (133 ^ _33843) ^ [_38449] : [134 ^ _33843 : [(137 ^ _33843) ^ [] : [_38449 = _37991], (135 ^ _33843) ^ [] : [_38449 = _37993]], -(in(_38449, _37989))]]], (88 ^ _33843) ^ [_36889, _36891] : [_36889 = powerset(_36891), 91 ^ _33843 : [(98 ^ _33843) ^ [_37231] : [subset(_37231, _36891), -(in(_37231, _36889))], (92 ^ _33843) ^ [_37059] : [in(_37059, _36889), -(subset(_37059, _36891))]]], (30 ^ _33843) ^ [_34914, _34916, _34918, _34920] : [-(subset(_34918, _34914)), subset(_34920, _34916), _34920 = _34918, _34916 = _34914], (104 ^ _33843) ^ [_37410, _37412] : [-(_37410 = powerset(_37412)), 108 ^ _33843 : [(111 ^ _33843) ^ [] : [subset(105 ^ [_37410, _37412], _37412)], (109 ^ _33843) ^ [] : [-(in(105 ^ [_37410, _37412], _37410))]], 112 ^ _33843 : [(115 ^ _33843) ^ [] : [in(105 ^ [_37410, _37412], _37410)], (113 ^ _33843) ^ [] : [-(subset(105 ^ [_37410, _37412], _37412))]]], (183 ^ _33843) ^ [] : [-(empty(181 ^ []))], (162 ^ _33843) ^ [] : [-(empty(empty_set))], (86 ^ _33843) ^ [_36745, _36747] : [-(unordered_pair(_36747, _36745) = unordered_pair(_36745, _36747))], (186 ^ _33843) ^ [] : [empty(184 ^ [])], (10 ^ _33843) ^ [_34278, _34280, _34282] : [-(_34282 = _34278), _34282 = _34280, _34280 = _34278], (20 ^ _33843) ^ [_34591, _34593] : [-(empty(_34591)), _34593 = _34591, empty(_34593)], (64 ^ _33843) ^ [_36010, _36012, _36014, _36016] : [-(unordered_pair(_36016, _36012) = unordered_pair(_36014, _36010)), _36016 = _36014, _36012 = _36010], (2 ^ _33843) ^ [_33967] : [-(_33967 = _33967)], (164 ^ _33843) ^ [_39547, _39549] : [subset(_39549, singleton(_39547)), -(_39549 = empty_set), -(_39549 = singleton(_39547))], (44 ^ _33843) ^ [_35338, _35340, _35342, _35344] : [-(in(_35342, _35338)), in(_35344, _35340), _35344 = _35342, _35340 = _35338], (80 ^ _33843) ^ [_36549, _36551] : [in(_36551, _36549), in(_36549, _36551)], (141 ^ _33843) ^ [_38714, _38716, _38718] : [-(_38714 = unordered_pair(_38718, _38716)), 145 ^ _33843 : [(150 ^ _33843) ^ [] : [142 ^ [_38714, _38716, _38718] = _38716], (148 ^ _33843) ^ [] : [142 ^ [_38714, _38716, _38718] = _38718], (146 ^ _33843) ^ [] : [-(in(142 ^ [_38714, _38716, _38718], _38714))]], 151 ^ _33843 : [(152 ^ _33843) ^ [] : [-(142 ^ [_38714, _38716, _38718] = _38718), -(142 ^ [_38714, _38716, _38718] = _38716)], (158 ^ _33843) ^ [] : [in(142 ^ [_38714, _38716, _38718], _38714)]]], (188 ^ _33843) ^ [_40265, _40267] : [-(subset(_40267, _40267))], (74 ^ _33843) ^ [_36321, _36323] : [_36323 = _36321, -(singleton(_36323) = singleton(_36321))]], input).
% 44.19/43.76 ncf('1',plain,[powerset(singleton(204 ^ [])) = unordered_pair(empty_set, singleton(204 ^ []))],start(206 ^ 0)).
% 44.19/43.76 ncf('1.1',plain,[-(powerset(singleton(204 ^ [])) = unordered_pair(empty_set, singleton(204 ^ []))), 146 : -(in(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], powerset(singleton(204 ^ [])))), 158 : in(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], powerset(singleton(204 ^ [])))],extension(141 ^ 1,bind([[_38714, _38716, _38718], [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]))).
% 44.19/43.76 ncf('1.1.1',plain,[in(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], powerset(singleton(204 ^ []))), 92 : -(subset(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], singleton(204 ^ []))), 92 : powerset(singleton(204 ^ [])) = powerset(singleton(204 ^ []))],extension(88 ^ 4,bind([[_36889, _36891, _37059], [powerset(singleton(204 ^ [])), singleton(204 ^ []), 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.1.1',plain,[subset(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], singleton(204 ^ [])), -(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set), -(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ []))],extension(164 ^ 7,bind([[_39547, _39549], [204 ^ [], 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.1.1.1',plain,[142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set, -(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set), 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]],extension(10 ^ 8,bind([[_34278, _34280, _34282], [empty_set, 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.1.1.1.1',plain,[142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set],extension(148 ^ 9)).
% 44.19/43.76 ncf('1.1.1.1.1.2',plain,[-(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set])],extension(2 ^ 9,bind([[_33967], [142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.1.1.2',plain,[142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ []), -(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ [])), singleton(204 ^ []) = singleton(204 ^ [])],extension(10 ^ 8,bind([[_34278, _34280, _34282], [singleton(204 ^ []), singleton(204 ^ []), 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.1.1.2.1',plain,[142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ [])],extension(150 ^ 9)).
% 44.19/43.76 ncf('1.1.1.1.2.2',plain,[-(singleton(204 ^ []) = singleton(204 ^ []))],extension(2 ^ 9,bind([[_33967], [singleton(204 ^ [])]]))).
% 44.19/43.76 ncf('1.1.1.2',plain,[-(powerset(singleton(204 ^ [])) = powerset(singleton(204 ^ []))), singleton(204 ^ []) = singleton(204 ^ [])],extension(58 ^ 5,bind([[_35764, _35766], [singleton(204 ^ []), singleton(204 ^ [])]]))).
% 44.19/43.76 ncf('1.1.1.2.1',plain,[-(singleton(204 ^ []) = singleton(204 ^ [])), 197 : in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])), 201 : in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ []))],extension(190 ^ 6,bind([[_40354, _40356], [singleton(204 ^ []), singleton(204 ^ [])]]))).
% 44.19/43.76 ncf('1.1.1.2.1.1',plain,[-(in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])))],extension(195 ^ 9)).
% 44.19/43.76 ncf('1.1.1.2.1.2',plain,[-(in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])))],extension(199 ^ 9)).
% 44.19/43.76 ncf('1.1.2',plain,[-(in(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], powerset(singleton(204 ^ [])))), 98 : subset(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], singleton(204 ^ [])), 98 : powerset(singleton(204 ^ [])) = powerset(singleton(204 ^ []))],extension(88 ^ 4,bind([[_36889, _36891, _37231], [powerset(singleton(204 ^ [])), singleton(204 ^ []), 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.2.1',plain,[-(subset(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set], singleton(204 ^ []))), 178 : 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ [])],extension(174 ^ 7,bind([[_39807, _39809], [204 ^ [], 142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set]]]))).
% 44.19/43.76 ncf('1.1.2.1.1',plain,[-(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = singleton(204 ^ [])), -(142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set)],extension(152 ^ 10)).
% 44.19/43.76 ncf('1.1.2.1.1.1',plain,[142 ^ [powerset(singleton(204 ^ [])), singleton(204 ^ []), empty_set] = empty_set],extension(176 ^ 11)).
% 44.19/43.76 ncf('1.1.2.2',plain,[-(powerset(singleton(204 ^ [])) = powerset(singleton(204 ^ []))), singleton(204 ^ []) = singleton(204 ^ [])],extension(58 ^ 5,bind([[_35764, _35766], [singleton(204 ^ []), singleton(204 ^ [])]]))).
% 44.19/43.76 ncf('1.1.2.2.1',plain,[-(singleton(204 ^ []) = singleton(204 ^ [])), 197 : in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])), 201 : in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ []))],extension(190 ^ 6,bind([[_40354, _40356], [singleton(204 ^ []), singleton(204 ^ [])]]))).
% 44.19/43.76 ncf('1.1.2.2.1.1',plain,[-(in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])))],extension(195 ^ 9)).
% 44.19/43.76 ncf('1.1.2.2.1.2',plain,[-(in(191 ^ [singleton(204 ^ []), singleton(204 ^ [])], singleton(204 ^ [])))],extension(199 ^ 9)).
% 44.19/43.76 %-----------------------------------------------------
% 44.19/43.76 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------