%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU170+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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 147.28s 143.03s
% Output : Proof 147.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU170+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n007.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 12:37:38 EDT 2023
% 0.19/0.34 % CPUTime :
% 147.28/143.03
% 147.28/143.03 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 147.28/143.03 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 147.28/143.03 %-----------------------------------------------------
% 147.28/143.03 ncf(matrix, plain, [(204 ^ _33286) ^ [] : [-(element(202 ^ [], powerset(201 ^ [])))], (207 ^ _33286) ^ [] : [-(element(205 ^ [], powerset(201 ^ [])))], (209 ^ _33286) ^ [] : [210 ^ _33286 : [(211 ^ _33286) ^ [] : [-(disjoint(202 ^ [], 205 ^ []))], (213 ^ _33286) ^ [] : [subset(202 ^ [], subset_complement(201 ^ [], 205 ^ []))]], 214 ^ _33286 : [(215 ^ _33286) ^ [] : [-(subset(202 ^ [], subset_complement(201 ^ [], 205 ^ [])))], (217 ^ _33286) ^ [] : [disjoint(202 ^ [], 205 ^ [])]]], (2 ^ _33286) ^ [_33399, _33401] : [in(_33401, _33399), in(_33399, _33401)], (18 ^ _33286) ^ [_33953, _33955] : [20 ^ _33286 : [(21 ^ _33286) ^ [] : [-(in(19 ^ [_33953, _33955], _33955))], (23 ^ _33286) ^ [] : [in(19 ^ [_33953, _33955], _33953)]], -(subset(_33955, _33953))], (8 ^ _33286) ^ [_33639, _33641] : [subset(_33641, _33639), 11 ^ _33286 : [(12 ^ _33286) ^ [_33776] : [in(_33776, _33641), -(in(_33776, _33639))]]], (49 ^ _33286) ^ [_35084, _35086, _35088] : [-(_35084 = set_difference(_35088, _35086)), 61 ^ _33286 : [(62 ^ _33286) ^ [] : [-(in(50 ^ [_35084, _35086, _35088], _35088))], (64 ^ _33286) ^ [] : [in(50 ^ [_35084, _35086, _35088], _35086)], (66 ^ _33286) ^ [] : [in(50 ^ [_35084, _35086, _35088], _35084)]], 53 ^ _33286 : [(54 ^ _33286) ^ [] : [-(in(50 ^ [_35084, _35086, _35088], _35084))], (56 ^ _33286) ^ [] : [in(50 ^ [_35084, _35086, _35088], _35088), -(in(50 ^ [_35084, _35086, _35088], _35086))]]], (27 ^ _33286) ^ [_34353, _34355, _34357] : [_34353 = set_difference(_34357, _34355), 30 ^ _33286 : [(31 ^ _33286) ^ [_34537] : [in(_34537, _34353), 34 ^ _33286 : [(35 ^ _33286) ^ [] : [-(in(_34537, _34357))], (37 ^ _33286) ^ [] : [in(_34537, _34355)]]], (39 ^ _33286) ^ [_34797] : [-(in(_34797, _34353)), in(_34797, _34357), -(in(_34797, _34355))]]], (70 ^ _33286) ^ [_35841, _35843] : [element(_35841, powerset(_35843)), -(subset_complement(_35843, _35841) = set_difference(_35843, _35841))], (76 ^ _33286) ^ [] : [true___, -(true___)], (82 ^ _33286) ^ [] : [true___, -(true___)], (88 ^ _33286) ^ [_36305, _36307] : [element(_36305, powerset(_36307)), -(element(subset_complement(_36307, _36305), powerset(_36307)))], (94 ^ _33286) ^ [] : [true___, -(true___)], (100 ^ _33286) ^ [] : [true___, -(true___)], (107 ^ _33286) ^ [_36777] : [-(element(105 ^ [_36777], _36777))], (109 ^ _33286) ^ [_36859] : [empty(powerset(_36859))], (111 ^ _33286) ^ [] : [-(empty(empty_set))], (113 ^ _33286) ^ [_37020, _37022] : [element(_37020, powerset(_37022)), -(subset_complement(_37022, subset_complement(_37022, _37020)) = _37020)], (119 ^ _33286) ^ [_37246, _37248] : [element(_37246, powerset(_37248)), 122 ^ _33286 : [(123 ^ _33286) ^ [_37387] : [in(_37387, _37246), -(in(_37387, _37248))]]], (129 ^ _33286) ^ [_37598] : [-(empty(_37598)), 133 ^ _33286 : [(134 ^ _33286) ^ [] : [-(element(132 ^ [_37598], powerset(_37598)))], (136 ^ _33286) ^ [] : [empty(132 ^ [_37598])]]], (139 ^ _33286) ^ [] : [-(empty(137 ^ []))], (142 ^ _33286) ^ [_38070] : [-(element(140 ^ [_38070], powerset(_38070)))], (144 ^ _33286) ^ [_38121] : [-(empty(140 ^ [_38121]))], (147 ^ _33286) ^ [] : [empty(145 ^ [])], (149 ^ _33286) ^ [_38309, _38311] : [-(subset(_38311, _38311))], (151 ^ _33286) ^ [_38418, _38420] : [disjoint(_38420, _38418), -(disjoint(_38418, _38420))], (157 ^ _33286) ^ [_38599] : [-(set_difference(_38599, empty_set) = _38599)], (159 ^ _33286) ^ [_38729, _38731] : [-(disjoint(_38731, _38729)), 163 ^ _33286 : [(164 ^ _33286) ^ [] : [-(in(162 ^ [_38729, _38731], _38731))], (166 ^ _33286) ^ [] : [-(in(162 ^ [_38729, _38731], _38729))]]], (168 ^ _33286) ^ [_39043, _39045] : [disjoint(_39045, _39043), 169 ^ _33286 : [(170 ^ _33286) ^ [_39135] : [in(_39135, _39045), in(_39135, _39043)]]], (178 ^ _33286) ^ [_39377] : [-(set_difference(empty_set, _39377) = empty_set)], (180 ^ _33286) ^ [_39473] : [empty(_39473), -(_39473 = empty_set)], (186 ^ _33286) ^ [_39675, _39677] : [in(_39677, _39675), empty(_39675)], (192 ^ _33286) ^ [_39862, _39864] : [empty(_39864), -(_39864 = _39862), empty(_39862)]], input).
% 147.28/143.03 ncf('1',plain,[213 : subset(202 ^ [], subset_complement(201 ^ [], 205 ^ [])), 217 : disjoint(202 ^ [], 205 ^ [])],start(209 ^ 0)).
% 147.28/143.03 ncf('1.1',plain,[-(subset(202 ^ [], subset_complement(201 ^ [], 205 ^ []))), 21 : -(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []))],extension(18 ^ 3,bind([[_33953, _33955], [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]))).
% 147.28/143.03 ncf('1.1.1',plain,[in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []), 39 : -(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], set_difference(set_difference(202 ^ [], 201 ^ []), empty_set))), 39 : -(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 201 ^ [])), 39 : set_difference(set_difference(202 ^ [], 201 ^ []), empty_set) = set_difference(202 ^ [], 201 ^ [])],extension(27 ^ 6,bind([[_34353, _34355, _34357, _34797], [set_difference(set_difference(202 ^ [], 201 ^ []), empty_set), 201 ^ [], 202 ^ [], 19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]]))).
% 147.28/143.03 ncf('1.1.1.1',plain,[in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], set_difference(set_difference(202 ^ [], 201 ^ []), empty_set)), 37 : in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 201 ^ [])],extension(31 ^ 9,bind([[_34537], [19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]]))).
% 147.28/143.03 ncf('1.1.1.1.1',plain,[-(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 201 ^ [])), 123 : in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []), 123 : element(202 ^ [], powerset(201 ^ []))],extension(119 ^ 12,bind([[_37246, _37248, _37387], [202 ^ [], 201 ^ [], 19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]]))).
% 147.28/143.03 ncf('1.1.1.1.1.1',plain,[-(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []))],reduction('1.1')).
% 147.28/143.03 ncf('1.1.1.1.1.2',plain,[-(element(202 ^ [], powerset(201 ^ [])))],extension(204 ^ 13)).
% 147.28/143.03 ncf('1.1.1.2',plain,[in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 201 ^ []), 39 : -(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], subset_complement(201 ^ [], 205 ^ []))), 39 : -(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 205 ^ [])), 39 : subset_complement(201 ^ [], 205 ^ []) = set_difference(201 ^ [], 205 ^ [])],extension(27 ^ 9,bind([[_34353, _34355, _34357, _34797], [subset_complement(201 ^ [], 205 ^ []), 205 ^ [], 201 ^ [], 19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]]))).
% 147.28/143.03 ncf('1.1.1.2.1',plain,[in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], subset_complement(201 ^ [], 205 ^ []))],extension(23 ^ 12)).
% 147.28/143.03 ncf('1.1.1.2.2',plain,[in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 205 ^ []), 170 : in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []), 170 : disjoint(202 ^ [], 205 ^ [])],extension(168 ^ 12,bind([[_39043, _39045, _39135], [205 ^ [], 202 ^ [], 19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []]]]))).
% 147.28/143.03 ncf('1.1.1.2.2.1',plain,[-(in(19 ^ [subset_complement(201 ^ [], 205 ^ []), 202 ^ []], 202 ^ []))],reduction('1.1')).
% 147.28/143.03 ncf('1.1.1.2.2.2',plain,[-(disjoint(202 ^ [], 205 ^ []))],extension(211 ^ 13)).
% 147.28/143.03 ncf('1.1.1.2.3',plain,[-(subset_complement(201 ^ [], 205 ^ []) = set_difference(201 ^ [], 205 ^ [])), element(205 ^ [], powerset(201 ^ []))],extension(70 ^ 10,bind([[_35841, _35843], [205 ^ [], 201 ^ []]]))).
% 147.28/143.03 ncf('1.1.1.2.3.1',plain,[-(element(205 ^ [], powerset(201 ^ [])))],extension(207 ^ 11)).
% 147.28/143.03 ncf('1.1.1.3',plain,[-(set_difference(set_difference(202 ^ [], 201 ^ []), empty_set) = set_difference(202 ^ [], 201 ^ []))],extension(157 ^ 7,bind([[_38599], [set_difference(202 ^ [], 201 ^ [])]]))).
% 147.28/143.03 ncf('1.2',plain,[-(disjoint(202 ^ [], 205 ^ [])), 164 : -(in(162 ^ [205 ^ [], 202 ^ []], 202 ^ []))],extension(159 ^ 3,bind([[_38729, _38731], [205 ^ [], 202 ^ []]]))).
% 147.28/143.03 ncf('1.2.1',plain,[in(162 ^ [205 ^ [], 202 ^ []], 202 ^ []), 12 : -(in(162 ^ [205 ^ [], 202 ^ []], subset_complement(201 ^ [], 205 ^ []))), 12 : subset(202 ^ [], subset_complement(201 ^ [], 205 ^ []))],extension(8 ^ 6,bind([[_33639, _33641, _33776], [subset_complement(201 ^ [], 205 ^ []), 202 ^ [], 162 ^ [205 ^ [], 202 ^ []]]]))).
% 147.28/143.03 ncf('1.2.1.1',plain,[in(162 ^ [205 ^ [], 202 ^ []], subset_complement(201 ^ [], 205 ^ [])), 37 : in(162 ^ [205 ^ [], 202 ^ []], 205 ^ []), 31 : subset_complement(201 ^ [], 205 ^ []) = set_difference(201 ^ [], 205 ^ [])],extension(27 ^ 9,bind([[_34353, _34355, _34357, _34537], [subset_complement(201 ^ [], 205 ^ []), 205 ^ [], 201 ^ [], 162 ^ [205 ^ [], 202 ^ []]]]))).
% 147.28/143.03 ncf('1.2.1.1.1',plain,[-(in(162 ^ [205 ^ [], 202 ^ []], 205 ^ []))],extension(166 ^ 14)).
% 147.28/143.03 ncf('1.2.1.1.2',plain,[-(subset_complement(201 ^ [], 205 ^ []) = set_difference(201 ^ [], 205 ^ [])), element(205 ^ [], powerset(201 ^ []))],extension(70 ^ 10,bind([[_35841, _35843], [205 ^ [], 201 ^ []]]))).
% 147.28/143.03 ncf('1.2.1.1.2.1',plain,[-(element(205 ^ [], powerset(201 ^ [])))],extension(207 ^ 11)).
% 147.28/143.03 ncf('1.2.1.2',plain,[-(subset(202 ^ [], subset_complement(201 ^ [], 205 ^ [])))],extension(215 ^ 7)).
% 147.28/143.03 %-----------------------------------------------------
% 147.28/143.03 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------