%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU169+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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.32s 1.39s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU169+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n014.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:29:57 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.32/1.39
% 0.32/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 ncf(matrix, plain, [(232 ^ _30364) ^ [] : [-(element(230 ^ [], powerset(229 ^ [])))], (235 ^ _30364) ^ [] : [-(in(233 ^ [], 230 ^ []))], (237 ^ _30364) ^ [] : [in(233 ^ [], 229 ^ [])], (72 ^ _30364) ^ [_32731, _32733] : [_32733 = _32731, -(powerset(_32733) = powerset(_32731))], (2 ^ _30364) ^ [_30508] : [-(_30508 = _30508)], (4 ^ _30364) ^ [_30615, _30617] : [_30617 = _30615, -(_30615 = _30617)], (10 ^ _30364) ^ [_30819, _30821, _30823] : [-(_30823 = _30819), _30823 = _30821, _30821 = _30819], (20 ^ _30364) ^ [_31160, _31162, _31164, _31166] : [-(subset(_31164, _31160)), subset(_31166, _31162), _31166 = _31164, _31162 = _31160], (34 ^ _30364) ^ [_31576, _31578] : [-(empty(_31576)), _31578 = _31576, empty(_31578)], (44 ^ _30364) ^ [_31899, _31901, _31903, _31905] : [-(element(_31903, _31899)), element(_31905, _31901), _31905 = _31903, _31901 = _31899], (58 ^ _30364) ^ [_32323, _32325, _32327, _32329] : [-(in(_32327, _32323)), in(_32329, _32325), _32329 = _32327, _32325 = _32323], (78 ^ _30364) ^ [_32951, _32953] : [in(_32953, _32951), in(_32951, _32953)], (100 ^ _30364) ^ [_33712, _33714] : [-(_33712 = powerset(_33714)), 104 ^ _30364 : [(105 ^ _30364) ^ [] : [-(in(101 ^ [_33712, _33714], _33712))], (107 ^ _30364) ^ [] : [subset(101 ^ [_33712, _33714], _33714)]], 108 ^ _30364 : [(109 ^ _30364) ^ [] : [-(subset(101 ^ [_33712, _33714], _33714))], (111 ^ _30364) ^ [] : [in(101 ^ [_33712, _33714], _33712)]]], (84 ^ _30364) ^ [_33191, _33193] : [_33191 = powerset(_33193), 87 ^ _30364 : [(88 ^ _30364) ^ [_33361] : [in(_33361, _33191), -(subset(_33361, _33193))], (94 ^ _30364) ^ [_33533] : [subset(_33533, _33193), -(in(_33533, _33191))]]], (115 ^ _30364) ^ [_34268, _34270] : [-(empty(_34270)), 118 ^ _30364 : [(119 ^ _30364) ^ [] : [element(_34268, _34270), -(in(_34268, _34270))], (125 ^ _30364) ^ [] : [in(_34268, _34270), -(element(_34268, _34270))]]], (131 ^ _30364) ^ [_34681, _34683] : [empty(_34683), 134 ^ _30364 : [(135 ^ _30364) ^ [] : [element(_34681, _34683), -(empty(_34681))], (141 ^ _30364) ^ [] : [empty(_34681), -(element(_34681, _34683))]]], (157 ^ _30364) ^ [_35481, _35483] : [159 ^ _30364 : [(160 ^ _30364) ^ [] : [-(in(158 ^ [_35481, _35483], _35483))], (162 ^ _30364) ^ [] : [in(158 ^ [_35481, _35483], _35481)]], -(subset(_35483, _35481))], (147 ^ _30364) ^ [_35167, _35169] : [subset(_35169, _35167), 150 ^ _30364 : [(151 ^ _30364) ^ [_35304] : [in(_35304, _35169), -(in(_35304, _35167))]]], (166 ^ _30364) ^ [] : [true___, -(true___)], (172 ^ _30364) ^ [] : [true___, -(true___)], (178 ^ _30364) ^ [] : [true___, -(true___)], (185 ^ _30364) ^ [_36205] : [-(element(183 ^ [_36205], _36205))], (187 ^ _30364) ^ [_36287] : [empty(powerset(_36287))], (189 ^ _30364) ^ [] : [-(empty(empty_set))], (191 ^ _30364) ^ [_36434] : [-(empty(_36434)), 195 ^ _30364 : [(196 ^ _30364) ^ [] : [-(element(194 ^ [_36434], powerset(_36434)))], (198 ^ _30364) ^ [] : [empty(194 ^ [_36434])]]], (201 ^ _30364) ^ [] : [-(empty(199 ^ []))], (204 ^ _30364) ^ [] : [empty(202 ^ [])], (206 ^ _30364) ^ [_36944, _36946] : [-(subset(_36946, _36946))], (208 ^ _30364) ^ [_37039] : [empty(_37039), -(_37039 = empty_set)], (214 ^ _30364) ^ [_37241, _37243] : [in(_37243, _37241), empty(_37241)], (220 ^ _30364) ^ [_37428, _37430] : [empty(_37430), -(_37430 = _37428), empty(_37428)]], input).
% 0.32/1.39 ncf('1',plain,[empty(powerset(229 ^ []))],start(187 ^ 0,bind([[_36287], [229 ^ []]]))).
% 0.32/1.39 ncf('1.1',plain,[-(empty(powerset(229 ^ []))), 119 : element(230 ^ [], powerset(229 ^ [])), 119 : -(in(230 ^ [], powerset(229 ^ [])))],extension(115 ^ 1,bind([[_34268, _34270], [230 ^ [], powerset(229 ^ [])]]))).
% 0.32/1.39 ncf('1.1.1',plain,[-(element(230 ^ [], powerset(229 ^ [])))],extension(232 ^ 4)).
% 0.32/1.39 ncf('1.1.2',plain,[in(230 ^ [], powerset(229 ^ [])), 88 : -(subset(230 ^ [], 229 ^ [])), 88 : powerset(229 ^ []) = powerset(229 ^ [])],extension(84 ^ 4,bind([[_33191, _33193, _33361], [powerset(229 ^ []), 229 ^ [], 230 ^ []]]))).
% 0.32/1.39 ncf('1.1.2.1',plain,[subset(230 ^ [], 229 ^ []), 151 : in(233 ^ [], 230 ^ []), 151 : -(in(233 ^ [], 229 ^ []))],extension(147 ^ 7,bind([[_35167, _35169, _35304], [229 ^ [], 230 ^ [], 233 ^ []]]))).
% 0.32/1.39 ncf('1.1.2.1.1',plain,[-(in(233 ^ [], 230 ^ []))],extension(235 ^ 10)).
% 0.32/1.39 ncf('1.1.2.1.2',plain,[in(233 ^ [], 229 ^ [])],extension(237 ^ 10)).
% 0.32/1.39 ncf('1.1.2.2',plain,[-(powerset(229 ^ []) = powerset(229 ^ []))],extension(2 ^ 5,bind([[_30508], [powerset(229 ^ [])]]))).
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------