%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET976+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:45 EDT 2023
% Result : Theorem 0.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SET976+1 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n001.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 19:52:05 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(151 ^ _27650) ^ [] : [160 ^ _27650 : [(161 ^ _27650) ^ [] : [-(in(146 ^ [], 148 ^ []))], (163 ^ _27650) ^ [] : [-(147 ^ [] = 149 ^ [])], (165 ^ _27650) ^ [] : [in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ [])))]], 152 ^ _27650 : [(153 ^ _27650) ^ [] : [-(in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ []))))], (155 ^ _27650) ^ [] : [in(146 ^ [], 148 ^ []), 147 ^ [] = 149 ^ []]]], (80 ^ _27650) ^ [_30434, _30436] : [in(_30436, _30434), in(_30434, _30436)], (86 ^ _27650) ^ [_30630, _30632] : [-(unordered_pair(_30632, _30630) = unordered_pair(_30630, _30632))], (119 ^ _27650) ^ [_31816, _31818] : [-(ordered_pair(_31818, _31816) = unordered_pair(unordered_pair(_31818, _31816), singleton(_31818)))], (121 ^ _27650) ^ [_31920, _31922] : [empty(ordered_pair(_31922, _31920))], (142 ^ _27650) ^ [] : [-(empty(140 ^ []))], (145 ^ _27650) ^ [] : [empty(143 ^ [])], (123 ^ _27650) ^ [_32088, _32090, _32092, _32094] : [in(ordered_pair(_32094, _32092), cartesian_product2(_32090, _32088)), 126 ^ _27650 : [(127 ^ _27650) ^ [] : [-(in(_32094, _32090))], (129 ^ _27650) ^ [] : [-(in(_32092, _32088))]]], (131 ^ _27650) ^ [_32353, _32355, _32357, _32359] : [-(in(ordered_pair(_32359, _32357), cartesian_product2(_32355, _32353))), in(_32359, _32355), in(_32357, _32353)], (104 ^ _27650) ^ [_31295, _31297] : [-(_31295 = singleton(_31297)), 108 ^ _27650 : [(109 ^ _27650) ^ [] : [-(in(105 ^ [_31295, _31297], _31295))], (111 ^ _27650) ^ [] : [105 ^ [_31295, _31297] = _31297]], 112 ^ _27650 : [(113 ^ _27650) ^ [] : [-(105 ^ [_31295, _31297] = _31297)], (115 ^ _27650) ^ [] : [in(105 ^ [_31295, _31297], _31295)]]], (88 ^ _27650) ^ [_30774, _30776] : [_30774 = singleton(_30776), 91 ^ _27650 : [(92 ^ _27650) ^ [_30944] : [in(_30944, _30774), -(_30944 = _30776)], (98 ^ _27650) ^ [_31116] : [_31116 = _30776, -(in(_31116, _30774))]]], (44 ^ _27650) ^ [_29173, _29175, _29177, _29179] : [-(unordered_pair(_29179, _29175) = unordered_pair(_29177, _29173)), _29179 = _29177, _29175 = _29173], (54 ^ _27650) ^ [_29532, _29534, _29536, _29538] : [-(ordered_pair(_29538, _29534) = ordered_pair(_29536, _29532)), _29538 = _29536, _29534 = _29532], (74 ^ _27650) ^ [_30202, _30204] : [_30204 = _30202, -(singleton(_30204) = singleton(_30202))], (64 ^ _27650) ^ [_29891, _29893, _29895, _29897] : [-(cartesian_product2(_29897, _29893) = cartesian_product2(_29895, _29891)), _29897 = _29895, _29893 = _29891], (2 ^ _27650) ^ [_27794] : [-(_27794 = _27794)], (4 ^ _27650) ^ [_27901, _27903] : [_27903 = _27901, -(_27901 = _27903)], (10 ^ _27650) ^ [_28105, _28107, _28109] : [-(_28109 = _28105), _28109 = _28107, _28107 = _28105], (20 ^ _27650) ^ [_28418, _28420] : [-(empty(_28418)), _28420 = _28418, empty(_28420)], (30 ^ _27650) ^ [_28721, _28723, _28725, _28727] : [-(in(_28725, _28721)), in(_28727, _28723), _28727 = _28725, _28723 = _28721]], input).
% 0.32/1.37 ncf('1',plain,[165 : in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ []))), 155 : in(146 ^ [], 148 ^ []), 155 : 147 ^ [] = 149 ^ []],start(151 ^ 0)).
% 0.32/1.37 ncf('1.1',plain,[-(in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ [])))), in(146 ^ [], 148 ^ []), in(147 ^ [], singleton(149 ^ []))],extension(131 ^ 3,bind([[_32353, _32355, _32357, _32359], [singleton(149 ^ []), 148 ^ [], 147 ^ [], 146 ^ []]]))).
% 0.32/1.37 ncf('1.1.1',plain,[-(in(146 ^ [], 148 ^ []))],extension(161 ^ 4)).
% 0.32/1.37 ncf('1.1.2',plain,[-(in(147 ^ [], singleton(149 ^ []))), 98 : 147 ^ [] = 149 ^ [], 98 : singleton(149 ^ []) = singleton(149 ^ [])],extension(88 ^ 4,bind([[_30774, _30776, _31116], [singleton(149 ^ []), 149 ^ [], 147 ^ []]]))).
% 0.32/1.37 ncf('1.1.2.1',plain,[-(147 ^ [] = 149 ^ [])],extension(163 ^ 7)).
% 0.32/1.37 ncf('1.1.2.2',plain,[-(singleton(149 ^ []) = singleton(149 ^ []))],extension(2 ^ 5,bind([[_27794], [singleton(149 ^ [])]]))).
% 0.32/1.37 ncf('1.2',plain,[-(in(146 ^ [], 148 ^ [])), in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ [])))],extension(123 ^ 3,bind([[_32088, _32090, _32092, _32094], [singleton(149 ^ []), 148 ^ [], 147 ^ [], 146 ^ []]]))).
% 0.32/1.37 ncf('1.2.1',plain,[-(in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ []))))],extension(153 ^ 4)).
% 0.32/1.37 ncf('1.3',plain,[-(147 ^ [] = 149 ^ []), 92 : in(147 ^ [], singleton(149 ^ [])), 92 : singleton(149 ^ []) = singleton(149 ^ [])],extension(88 ^ 3,bind([[_30774, _30776, _30944], [singleton(149 ^ []), 149 ^ [], 147 ^ []]]))).
% 0.32/1.37 ncf('1.3.1',plain,[-(in(147 ^ [], singleton(149 ^ []))), in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ [])))],extension(123 ^ 6,bind([[_32088, _32090, _32092, _32094], [singleton(149 ^ []), 148 ^ [], 147 ^ [], 146 ^ []]]))).
% 0.32/1.37 ncf('1.3.1.1',plain,[-(in(ordered_pair(146 ^ [], 147 ^ []), cartesian_product2(148 ^ [], singleton(149 ^ []))))],extension(153 ^ 7)).
% 0.32/1.37 ncf('1.3.2',plain,[-(singleton(149 ^ []) = singleton(149 ^ [])), 149 ^ [] = 149 ^ []],extension(74 ^ 4,bind([[_30202, _30204], [149 ^ [], 149 ^ []]]))).
% 0.32/1.37 ncf('1.3.2.1',plain,[-(149 ^ [] = 149 ^ [])],extension(2 ^ 5,bind([[_27794], [149 ^ []]]))).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------