%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET885+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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:36 EDT 2023
% Result : Theorem 160.96s 156.39s
% Output : Proof 160.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET885+1 : TPTP v8.1.2. Released v3.2.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n029.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 19:23:13 EDT 2023
% 0.12/0.34 % CPUTime :
% 160.96/156.39
% 160.96/156.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 160.96/156.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 160.96/156.39 %-----------------------------------------------------
% 160.96/156.39 ncf(matrix, plain, [(186 ^ _32865) ^ [] : [-(subset(unordered_pair(182 ^ [], 183 ^ []), singleton(184 ^ [])))], (188 ^ _32865) ^ [] : [182 ^ [] = 184 ^ []], !, (156 ^ _26405) ^ [_31834, _31836] : [subset(_31836, _31834), 159 ^ _26405 : [(160 ^ _26405) ^ [_31971] : [in(_31971, _31836), -(in(_31971, _31834))]]], (166 ^ _26405) ^ [_32148, _32150] : [168 ^ _26405 : [(169 ^ _26405) ^ [] : [-(in(167 ^ [_32148, _32150], _32150))], (171 ^ _26405) ^ [] : [in(167 ^ [_32148, _32150], _32148)]], -(subset(_32150, _32148))], (98 ^ _26405) ^ [_29750, _29752] : [-(_29750 = singleton(_29752)), 102 ^ _26405 : [(103 ^ _26405) ^ [] : [-(in(99 ^ [_29750, _29752], _29750))], (105 ^ _26405) ^ [] : [99 ^ [_29750, _29752] = _29752]], 106 ^ _26405 : [(107 ^ _26405) ^ [] : [-(99 ^ [_29750, _29752] = _29752)], (109 ^ _26405) ^ [] : [in(99 ^ [_29750, _29752], _29750)]]], (2 ^ _26405) ^ [_26529] : [-(_26529 = _26529)], (74 ^ _26405) ^ [_28889, _28891] : [in(_28891, _28889), in(_28889, _28891)], (68 ^ _26405) ^ [_28665, _28667] : [_28667 = _28665, -(singleton(_28667) = singleton(_28665))], (20 ^ _26405) ^ [_27181, _27183, _27185, _27187] : [-(in(_27185, _27181)), in(_27187, _27183), _27187 = _27185, _27183 = _27181], (44 ^ _26405) ^ [_27900, _27902, _27904, _27906] : [-(subset(_27904, _27900)), subset(_27906, _27902), _27906 = _27904, _27902 = _27900], (82 ^ _26405) ^ [_29229, _29231] : [_29229 = singleton(_29231), 85 ^ _26405 : [(86 ^ _26405) ^ [_29399] : [in(_29399, _29229), -(_29399 = _29231)], (92 ^ _26405) ^ [_29571] : [_29571 = _29231, -(in(_29571, _29229))]]], (10 ^ _26405) ^ [_26840, _26842, _26844] : [-(_26844 = _26840), _26844 = _26842, _26842 = _26840], (176 ^ _26405) ^ [] : [-(empty(174 ^ []))], (181 ^ _26405) ^ [_32649, _32651] : [-(subset(_32651, _32651))], (113 ^ _26405) ^ [_30329, _30331, _30333] : [_30329 = unordered_pair(_30333, _30331), 116 ^ _26405 : [(127 ^ _26405) ^ [_30789] : [128 ^ _26405 : [(129 ^ _26405) ^ [] : [_30789 = _30333], (131 ^ _26405) ^ [] : [_30789 = _30331]], -(in(_30789, _30329))], (117 ^ _26405) ^ [_30511] : [in(_30511, _30329), -(_30511 = _30333), -(_30511 = _30331)]]], (135 ^ _26405) ^ [_31054, _31056, _31058] : [-(_31054 = unordered_pair(_31058, _31056)), 139 ^ _26405 : [(144 ^ _26405) ^ [] : [136 ^ [_31054, _31056, _31058] = _31056], (142 ^ _26405) ^ [] : [136 ^ [_31054, _31056, _31058] = _31058], (140 ^ _26405) ^ [] : [-(in(136 ^ [_31054, _31056, _31058], _31054))]], 145 ^ _26405 : [(152 ^ _26405) ^ [] : [in(136 ^ [_31054, _31056, _31058], _31054)], (146 ^ _26405) ^ [] : [-(136 ^ [_31054, _31056, _31058] = _31058), -(136 ^ [_31054, _31056, _31058] = _31056)]]], (80 ^ _26405) ^ [_29085, _29087] : [-(unordered_pair(_29087, _29085) = unordered_pair(_29085, _29087))], (34 ^ _26405) ^ [_27597, _27599] : [-(empty(_27597)), _27599 = _27597, empty(_27599)], (58 ^ _26405) ^ [_28354, _28356, _28358, _28360] : [-(unordered_pair(_28360, _28356) = unordered_pair(_28358, _28354)), _28360 = _28358, _28356 = _28354], (4 ^ _26405) ^ [_26636, _26638] : [_26638 = _26636, -(_26636 = _26638)], (179 ^ _26405) ^ [] : [empty(177 ^ [])]], input).
% 160.96/156.39 ncf('1',plain,[-(subset(unordered_pair(182 ^ [], 183 ^ []), singleton(184 ^ [])))],start(186 ^ 0)).
% 160.96/156.39 ncf('1.1',plain,[subset(unordered_pair(182 ^ [], 183 ^ []), singleton(184 ^ [])), 160 : in(182 ^ [], unordered_pair(182 ^ [], 183 ^ [])), 160 : -(in(182 ^ [], singleton(184 ^ [])))],extension(156 ^ 1,bind([[_31834, _31836, _31971], [singleton(184 ^ []), unordered_pair(182 ^ [], 183 ^ []), 182 ^ []]]))).
% 160.96/156.39 ncf('1.1.1',plain,[-(in(182 ^ [], unordered_pair(182 ^ [], 183 ^ []))), 129 : 182 ^ [] = 182 ^ [], 127 : unordered_pair(182 ^ [], 183 ^ []) = unordered_pair(182 ^ [], 183 ^ [])],extension(113 ^ 4,bind([[_30329, _30331, _30333, _30789], [unordered_pair(182 ^ [], 183 ^ []), 183 ^ [], 182 ^ [], 182 ^ []]]))).
% 160.96/156.39 ncf('1.1.1.1',plain,[-(182 ^ [] = 182 ^ [])],extension(2 ^ 9,bind([[_26529], [182 ^ []]]))).
% 160.96/156.39 ncf('1.1.1.2',plain,[-(unordered_pair(182 ^ [], 183 ^ []) = unordered_pair(182 ^ [], 183 ^ []))],extension(2 ^ 5,bind([[_26529], [unordered_pair(182 ^ [], 183 ^ [])]]))).
% 160.96/156.39 ncf('1.1.2',plain,[in(182 ^ [], singleton(184 ^ [])), 86 : -(182 ^ [] = 184 ^ []), 86 : singleton(184 ^ []) = singleton(184 ^ [])],extension(82 ^ 4,bind([[_29229, _29231, _29399], [singleton(184 ^ []), 184 ^ [], 182 ^ []]]))).
% 160.96/156.39 ncf('1.1.2.1',plain,[182 ^ [] = 184 ^ []],extension(188 ^ 7)).
% 160.96/156.39 ncf('1.1.2.2',plain,[-(singleton(184 ^ []) = singleton(184 ^ []))],extension(2 ^ 5,bind([[_26529], [singleton(184 ^ [])]]))).
% 160.96/156.39 %-----------------------------------------------------
% 160.96/156.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------