%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET932+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:42 EDT 2023
% Result : Theorem 161.52s 156.72s
% Output : Proof 161.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET932+1 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % 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:17:42 EDT 2023
% 0.12/0.33 % CPUTime :
% 161.52/156.72
% 161.52/156.72 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 161.52/156.72 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 161.52/156.72 %-----------------------------------------------------
% 161.52/156.72 ncf(matrix, plain, [(140 ^ _26577) ^ [] : [-(subset(137 ^ [], 138 ^ []))], (142 ^ _26577) ^ [] : [subset(powerset(137 ^ []), powerset(138 ^ []))], !, (4 ^ _21841) ^ [_22072, _22074] : [_22074 = _22072, -(_22072 = _22074)], (86 ^ _21841) ^ [_24723, _24725] : [-(_24723 = powerset(_24725)), 90 ^ _21841 : [(91 ^ _21841) ^ [] : [-(in(87 ^ [_24723, _24725], _24723))], (93 ^ _21841) ^ [] : [subset(87 ^ [_24723, _24725], _24725)]], 94 ^ _21841 : [(95 ^ _21841) ^ [] : [-(subset(87 ^ [_24723, _24725], _24725))], (97 ^ _21841) ^ [] : [in(87 ^ [_24723, _24725], _24723)]]], (111 ^ _21841) ^ [_25602, _25604] : [113 ^ _21841 : [(114 ^ _21841) ^ [] : [-(in(112 ^ [_25602, _25604], _25604))], (116 ^ _21841) ^ [] : [in(112 ^ [_25602, _25604], _25602)]], -(subset(_25604, _25602))], (64 ^ _21841) ^ [_23962, _23964] : [in(_23964, _23962), in(_23962, _23964)], (58 ^ _21841) ^ [_23742, _23744] : [_23744 = _23742, -(powerset(_23744) = powerset(_23742))], (101 ^ _21841) ^ [_25288, _25290] : [subset(_25290, _25288), 104 ^ _21841 : [(105 ^ _21841) ^ [_25425] : [in(_25425, _25290), -(in(_25425, _25288))]]], (2 ^ _21841) ^ [_21965] : [-(_21965 = _21965)], (126 ^ _21841) ^ [_26123, _26125] : [-(subset(_26125, _26125))], (121 ^ _21841) ^ [] : [-(empty(119 ^ []))], (128 ^ _21841) ^ [_26226, _26228, _26230] : [-(subset(_26230, _26226)), subset(_26230, _26228), subset(_26228, _26226)], (44 ^ _21841) ^ [_23336, _23338, _23340, _23342] : [-(subset(_23340, _23336)), subset(_23342, _23338), _23342 = _23340, _23338 = _23336], (70 ^ _21841) ^ [_24202, _24204] : [_24202 = powerset(_24204), 73 ^ _21841 : [(74 ^ _21841) ^ [_24372] : [in(_24372, _24202), -(subset(_24372, _24204))], (80 ^ _21841) ^ [_24544] : [subset(_24544, _24204), -(in(_24544, _24202))]]], (10 ^ _21841) ^ [_22276, _22278, _22280] : [-(_22280 = _22276), _22280 = _22278, _22278 = _22276], (20 ^ _21841) ^ [_22617, _22619, _22621, _22623] : [-(in(_22621, _22617)), in(_22623, _22619), _22623 = _22621, _22619 = _22617], (34 ^ _21841) ^ [_23033, _23035] : [-(empty(_23033)), _23035 = _23033, empty(_23035)], (124 ^ _21841) ^ [] : [empty(122 ^ [])]], input).
% 161.52/156.72 ncf('1',plain,[-(subset(137 ^ [], 138 ^ []))],start(140 ^ 0)).
% 161.52/156.72 ncf('1.1',plain,[subset(137 ^ [], 138 ^ []), -(subset(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], 138 ^ [])), subset(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], 137 ^ [])],extension(128 ^ 1,bind([[_26226, _26228, _26230], [138 ^ [], 137 ^ [], 112 ^ [powerset(138 ^ []), powerset(137 ^ [])]]]))).
% 161.52/156.72 ncf('1.1.1',plain,[subset(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], 138 ^ []), 80 : -(in(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], powerset(138 ^ []))), 80 : powerset(138 ^ []) = powerset(138 ^ [])],extension(70 ^ 2,bind([[_24202, _24204, _24544], [powerset(138 ^ []), 138 ^ [], 112 ^ [powerset(138 ^ []), powerset(137 ^ [])]]]))).
% 161.52/156.72 ncf('1.1.1.1',plain,[in(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], powerset(138 ^ [])), -(subset(powerset(137 ^ []), powerset(138 ^ [])))],extension(111 ^ 5,bind([[_25602, _25604], [powerset(138 ^ []), powerset(137 ^ [])]]))).
% 161.52/156.72 ncf('1.1.1.1.1',plain,[subset(powerset(137 ^ []), powerset(138 ^ []))],extension(142 ^ 6)).
% 161.52/156.72 ncf('1.1.1.2',plain,[-(powerset(138 ^ []) = powerset(138 ^ []))],extension(2 ^ 3,bind([[_21965], [powerset(138 ^ [])]]))).
% 161.52/156.72 ncf('1.1.2',plain,[-(subset(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], 137 ^ [])), 74 : in(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], powerset(137 ^ [])), 74 : powerset(137 ^ []) = powerset(137 ^ [])],extension(70 ^ 2,bind([[_24202, _24204, _24372], [powerset(137 ^ []), 137 ^ [], 112 ^ [powerset(138 ^ []), powerset(137 ^ [])]]]))).
% 161.52/156.72 ncf('1.1.2.1',plain,[-(in(112 ^ [powerset(138 ^ []), powerset(137 ^ [])], powerset(137 ^ []))), -(subset(powerset(137 ^ []), powerset(138 ^ [])))],extension(111 ^ 5,bind([[_25602, _25604], [powerset(138 ^ []), powerset(137 ^ [])]]))).
% 161.52/156.72 ncf('1.1.2.1.1',plain,[subset(powerset(137 ^ []), powerset(138 ^ []))],extension(142 ^ 6)).
% 161.52/156.72 ncf('1.1.2.2',plain,[-(powerset(137 ^ []) = powerset(137 ^ []))],extension(2 ^ 3,bind([[_21965], [powerset(137 ^ [])]]))).
% 161.52/156.72 %-----------------------------------------------------
% 161.52/156.72 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------