%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU146+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:21 EDT 2023
% Result : Theorem 48.95s 48.04s
% Output : Proof 48.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU146+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n023.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 12:49:59 EDT 2023
% 0.11/0.34 % CPUTime :
% 48.95/48.04
% 48.95/48.04 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 48.95/48.04 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 48.95/48.04 %-----------------------------------------------------
% 48.95/48.04 ncf(matrix, plain, [(170 ^ _37971) ^ [] : [171 ^ _37971 : [(176 ^ _37971) ^ [] : [167 ^ [] = singleton(168 ^ [])], (174 ^ _37971) ^ [] : [167 ^ [] = empty_set], (172 ^ _37971) ^ [] : [-(subset(167 ^ [], singleton(168 ^ [])))]], 177 ^ _37971 : [(178 ^ _37971) ^ [] : [-(167 ^ [] = empty_set), -(167 ^ [] = singleton(168 ^ []))], (184 ^ _37971) ^ [] : [subset(167 ^ [], singleton(168 ^ []))]]], !, (148 ^ _32548) ^ [_37209] : [-(subset(empty_set, _37209))], (68 ^ _32548) ^ [_34808, _34810] : [_34810 = _34808, -(singleton(_34810) = singleton(_34808))], (10 ^ _32548) ^ [_32983, _32985, _32987] : [-(_32987 = _32983), _32987 = _32985, _32985 = _32983], (4 ^ _32548) ^ [_32779, _32781] : [_32781 = _32779, -(_32779 = _32781)], (141 ^ _32548) ^ [] : [-(empty(139 ^ []))], (20 ^ _32548) ^ [_33324, _33326, _33328, _33330] : [-(in(_33328, _33324)), in(_33330, _33326), _33330 = _33328, _33326 = _33324], (144 ^ _32548) ^ [] : [empty(142 ^ [])], (150 ^ _32548) ^ [_37345, _37347] : [set_difference(_37347, _37345) = empty_set, -(subset(_37347, _37345))], (146 ^ _32548) ^ [_37129, _37131] : [-(subset(_37131, _37131))], (130 ^ _32548) ^ [_36645, _36647, _36649] : [subset(_36649, _36647), -(in(_36645, _36649)), -(subset(_36649, set_difference(_36647, singleton(_36645))))], (2 ^ _32548) ^ [_32672] : [-(_32672 = _32672)], (34 ^ _32548) ^ [_33740, _33742] : [-(empty(_33740)), _33742 = _33740, empty(_33742)], (118 ^ _32548) ^ [_36249, _36251] : [subset(singleton(_36251), _36249), -(in(_36251, _36249))], (162 ^ _32548) ^ [_37697] : [subset(_37697, empty_set), -(_37697 = empty_set)], (104 ^ _32548) ^ [] : [true___, -(true___)], (110 ^ _32548) ^ [] : [true___, -(true___)], (44 ^ _32548) ^ [_34043, _34045, _34047, _34049] : [-(subset(_34047, _34043)), subset(_34049, _34045), _34049 = _34047, _34045 = _34043], (124 ^ _32548) ^ [_36415, _36417] : [in(_36417, _36415), -(subset(singleton(_36417), _36415))], (88 ^ _32548) ^ [_35509, _35511] : [-(_35511 = _35509), subset(_35511, _35509), subset(_35509, _35511)], (156 ^ _32548) ^ [_37513, _37515] : [subset(_37515, _37513), -(set_difference(_37515, _37513) = empty_set)], (74 ^ _32548) ^ [_35032, _35034] : [in(_35034, _35032), in(_35032, _35034)], (116 ^ _32548) ^ [] : [-(empty(empty_set))], (58 ^ _32548) ^ [_34497, _34499, _34501, _34503] : [-(set_difference(_34503, _34499) = set_difference(_34501, _34497)), _34503 = _34501, _34499 = _34497], (98 ^ _32548) ^ [] : [true___, -(true___)], (80 ^ _32548) ^ [_35272, _35274] : [_35274 = _35272, 83 ^ _32548 : [(86 ^ _32548) ^ [] : [-(subset(_35272, _35274))], (84 ^ _32548) ^ [] : [-(subset(_35274, _35272))]]]], input).
% 48.95/48.04 ncf('1',plain,[172 : -(subset(167 ^ [], singleton(168 ^ []))), 178 : -(167 ^ [] = empty_set), 178 : -(167 ^ [] = singleton(168 ^ []))],start(170 ^ 0)).
% 48.95/48.04 ncf('1.1',plain,[subset(167 ^ [], singleton(168 ^ [])), -(set_difference(167 ^ [], singleton(168 ^ [])) = empty_set)],extension(156 ^ 3,bind([[_37513, _37515], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1',plain,[set_difference(167 ^ [], singleton(168 ^ [])) = empty_set, -(empty_set = set_difference(167 ^ [], singleton(168 ^ [])))],extension(4 ^ 4,bind([[_32779, _32781], [empty_set, set_difference(167 ^ [], singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.1.1.1',plain,[empty_set = set_difference(167 ^ [], singleton(168 ^ [])), -(subset(set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ [])), subset(empty_set, 167 ^ []), 167 ^ [] = 167 ^ []],extension(44 ^ 5,bind([[_34043, _34045, _34047, _34049], [167 ^ [], 167 ^ [], set_difference(167 ^ [], singleton(168 ^ [])), empty_set]]))).
% 48.95/48.04 ncf('1.1.1.1.1',plain,[subset(set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []), -(167 ^ [] = set_difference(167 ^ [], singleton(168 ^ []))), subset(167 ^ [], set_difference(167 ^ [], singleton(168 ^ [])))],extension(88 ^ 6,bind([[_35509, _35511], [set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.1',plain,[167 ^ [] = set_difference(167 ^ [], singleton(168 ^ [])), -(set_difference(167 ^ [], singleton(168 ^ [])) = 167 ^ [])],extension(4 ^ 7,bind([[_32779, _32781], [set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.1.1',plain,[set_difference(167 ^ [], singleton(168 ^ [])) = 167 ^ [], -(subset(167 ^ [], empty_set)), subset(set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []), 167 ^ [] = empty_set],extension(44 ^ 8,bind([[_34043, _34045, _34047, _34049], [empty_set, 167 ^ [], 167 ^ [], set_difference(167 ^ [], singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.1',plain,[subset(167 ^ [], empty_set), -(167 ^ [] = empty_set)],extension(162 ^ 9,bind([[_37697], [167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.1.1',plain,[167 ^ [] = empty_set],extension(174 ^ 10)).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.2',plain,[-(subset(set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []))],reduction('1.1.1.1')).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.3',plain,[-(167 ^ [] = empty_set), 167 ^ [] = set_difference(167 ^ [], singleton(168 ^ [])), set_difference(167 ^ [], singleton(168 ^ [])) = empty_set],extension(10 ^ 9,bind([[_32983, _32985, _32987], [empty_set, set_difference(167 ^ [], singleton(168 ^ [])), 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.3.1',plain,[-(167 ^ [] = set_difference(167 ^ [], singleton(168 ^ [])))],reduction('1.1.1.1.1')).
% 48.95/48.04 ncf('1.1.1.1.1.1.1.3.2',plain,[-(set_difference(167 ^ [], singleton(168 ^ [])) = empty_set)],reduction('1.1')).
% 48.95/48.04 ncf('1.1.1.1.1.2',plain,[-(subset(167 ^ [], set_difference(167 ^ [], singleton(168 ^ [])))), subset(167 ^ [], 167 ^ []), -(in(168 ^ [], 167 ^ []))],extension(130 ^ 7,bind([[_36645, _36647, _36649], [168 ^ [], 167 ^ [], 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.2.1',plain,[-(subset(167 ^ [], 167 ^ []))],extension(146 ^ 8,bind([[_37129, _37131], [_21721, 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.2.2',plain,[in(168 ^ [], 167 ^ []), -(subset(singleton(168 ^ []), 167 ^ []))],extension(124 ^ 8,bind([[_36415, _36417], [167 ^ [], 168 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.2.2.1',plain,[subset(singleton(168 ^ []), 167 ^ []), -(167 ^ [] = singleton(168 ^ [])), subset(167 ^ [], singleton(168 ^ []))],extension(88 ^ 9,bind([[_35509, _35511], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.1.2.2.1.1',plain,[167 ^ [] = singleton(168 ^ [])],extension(176 ^ 10)).
% 48.95/48.04 ncf('1.1.1.1.1.2.2.1.2',plain,[-(subset(167 ^ [], singleton(168 ^ [])))],reduction('1')).
% 48.95/48.04 ncf('1.1.1.1.2',plain,[-(subset(empty_set, 167 ^ []))],extension(148 ^ 6,bind([[_37209], [167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.3',plain,[-(167 ^ [] = 167 ^ []), 167 ^ [] = 167 ^ []],extension(4 ^ 6,bind([[_32779, _32781], [167 ^ [], 167 ^ []]]))).
% 48.95/48.04 ncf('1.1.1.1.3.1',plain,[-(167 ^ [] = 167 ^ [])],extension(2 ^ 7,bind([[_32672], [167 ^ []]]))).
% 48.95/48.04 ncf('1.2',plain,[167 ^ [] = empty_set, -(empty_set = 167 ^ [])],extension(4 ^ 3,bind([[_32779, _32781], [empty_set, 167 ^ []]]))).
% 48.95/48.04 ncf('1.2.1',plain,[empty_set = 167 ^ [], -(subset(167 ^ [], singleton(168 ^ []))), subset(empty_set, singleton(168 ^ [])), singleton(168 ^ []) = singleton(168 ^ [])],extension(44 ^ 4,bind([[_34043, _34045, _34047, _34049], [singleton(168 ^ []), singleton(168 ^ []), 167 ^ [], empty_set]]))).
% 48.95/48.04 ncf('1.2.1.1',plain,[subset(167 ^ [], singleton(168 ^ []))],extension(184 ^ 5)).
% 48.95/48.04 ncf('1.2.1.2',plain,[-(subset(empty_set, singleton(168 ^ [])))],extension(148 ^ 5,bind([[_37209], [singleton(168 ^ [])]]))).
% 48.95/48.04 ncf('1.2.1.3',plain,[-(singleton(168 ^ []) = singleton(168 ^ [])), 168 ^ [] = 168 ^ []],extension(68 ^ 5,bind([[_34808, _34810], [168 ^ [], 168 ^ []]]))).
% 48.95/48.04 ncf('1.2.1.3.1',plain,[-(168 ^ [] = 168 ^ []), 168 ^ [] = 168 ^ []],extension(4 ^ 6,bind([[_32779, _32781], [168 ^ [], 168 ^ []]]))).
% 48.95/48.04 ncf('1.2.1.3.1.1',plain,[-(168 ^ [] = 168 ^ [])],extension(2 ^ 7,bind([[_32672], [168 ^ []]]))).
% 48.95/48.04 ncf('1.3',plain,[167 ^ [] = singleton(168 ^ []), -(singleton(167 ^ []) = singleton(singleton(168 ^ [])))],extension(68 ^ 3,bind([[_34808, _34810], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.3.1',plain,[singleton(167 ^ []) = singleton(singleton(168 ^ [])), 86 : -(subset(singleton(singleton(168 ^ [])), singleton(167 ^ [])))],extension(80 ^ 4,bind([[_35272, _35274], [singleton(singleton(168 ^ [])), singleton(167 ^ [])]]))).
% 48.95/48.04 ncf('1.3.1.1',plain,[subset(singleton(singleton(168 ^ [])), singleton(167 ^ [])), -(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set)],extension(156 ^ 7,bind([[_37513, _37515], [singleton(167 ^ []), singleton(singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1',plain,[set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set, -(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ []))), empty_set = set_difference(167 ^ [], singleton(168 ^ []))],extension(10 ^ 8,bind([[_32983, _32985, _32987], [set_difference(167 ^ [], singleton(168 ^ [])), empty_set, set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1',plain,[set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ [])), -(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set), set_difference(167 ^ [], singleton(168 ^ [])) = empty_set],extension(10 ^ 9,bind([[_32983, _32985, _32987], [empty_set, set_difference(167 ^ [], singleton(168 ^ [])), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.1',plain,[set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set, -(set_difference(167 ^ [], singleton(168 ^ [])) = empty_set), set_difference(167 ^ [], singleton(168 ^ [])) = set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))],extension(10 ^ 10,bind([[_32983, _32985, _32987], [empty_set, set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])), set_difference(167 ^ [], singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.1.1',plain,[set_difference(167 ^ [], singleton(168 ^ [])) = empty_set, -(subset(167 ^ [], singleton(168 ^ [])))],extension(150 ^ 11,bind([[_37345, _37347], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.1.1.1',plain,[subset(167 ^ [], singleton(168 ^ []))],extension(184 ^ 12)).
% 48.95/48.04 ncf('1.3.1.1.1.1.1.2',plain,[-(set_difference(167 ^ [], singleton(168 ^ [])) = set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ []))],extension(4 ^ 11,bind([[_32779, _32781], [set_difference(167 ^ [], singleton(168 ^ [])), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.1.2.1',plain,[-(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ [])))],reduction('1.3.1.1.1')).
% 48.95/48.04 ncf('1.3.1.1.1.1.2',plain,[-(set_difference(167 ^ [], singleton(168 ^ [])) = empty_set), set_difference(167 ^ [], singleton(168 ^ [])) = set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set],extension(10 ^ 10,bind([[_32983, _32985, _32987], [empty_set, set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])), set_difference(167 ^ [], singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.2.1',plain,[-(set_difference(167 ^ [], singleton(168 ^ [])) = set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ []))],extension(4 ^ 11,bind([[_32779, _32781], [set_difference(167 ^ [], singleton(168 ^ [])), set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.1.2.1.1',plain,[-(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = set_difference(167 ^ [], singleton(168 ^ [])))],reduction('1.3.1.1.1')).
% 48.95/48.04 ncf('1.3.1.1.1.1.2.2',plain,[-(set_difference(singleton(singleton(168 ^ [])), singleton(167 ^ [])) = empty_set)],reduction('1.3.1.1')).
% 48.95/48.04 ncf('1.3.1.1.1.2',plain,[-(empty_set = set_difference(167 ^ [], singleton(168 ^ []))), set_difference(167 ^ [], singleton(168 ^ [])) = empty_set],extension(4 ^ 9,bind([[_32779, _32781], [empty_set, set_difference(167 ^ [], singleton(168 ^ []))]]))).
% 48.95/48.04 ncf('1.3.1.1.1.2.1',plain,[-(set_difference(167 ^ [], singleton(168 ^ [])) = empty_set), subset(167 ^ [], singleton(168 ^ []))],extension(156 ^ 10,bind([[_37513, _37515], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.3.1.1.1.2.1.1',plain,[-(subset(167 ^ [], singleton(168 ^ []))), 167 ^ [] = singleton(168 ^ [])],extension(80 ^ 11,bind([[_35272, _35274], [singleton(168 ^ []), 167 ^ []]]))).
% 48.95/48.04 ncf('1.3.1.1.1.2.1.1.1',plain,[-(167 ^ [] = singleton(168 ^ []))],reduction('1')).
% 48.95/48.04 %-----------------------------------------------------
% 48.95/48.04 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------