%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET956+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:44 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : SET956+1 : TPTP v8.1.2. Released v3.2.0.
% 0.09/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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:15:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(161 ^ _31078) ^ [] : [subset(148 ^ [], 151 ^ [])], (153 ^ _31078) ^ [] : [-(subset(148 ^ [], cartesian_product2(149 ^ [], 150 ^ [])))], (155 ^ _31078) ^ [_36930, _36932] : [in(ordered_pair(_36932, _36930), 148 ^ []), -(in(ordered_pair(_36932, _36930), 151 ^ []))], (94 ^ _31078) ^ [_34308, _34310] : [in(_34310, _34308), in(_34308, _34310)], (100 ^ _31078) ^ [_34504, _34506] : [-(unordered_pair(_34506, _34504) = unordered_pair(_34504, _34506))], (121 ^ _31078) ^ [_35304, _35306] : [-(ordered_pair(_35306, _35304) = unordered_pair(unordered_pair(_35306, _35304), singleton(_35306)))], (123 ^ _31078) ^ [_35408, _35410] : [empty(ordered_pair(_35410, _35408))], (126 ^ _31078) ^ [] : [-(empty(124 ^ []))], (129 ^ _31078) ^ [] : [empty(127 ^ [])], (131 ^ _31078) ^ [_35683, _35685] : [-(subset(_35685, _35685))], (133 ^ _31078) ^ [_35800, _35802, _35804, _35806] : [subset(_35806, cartesian_product2(_35804, _35802)), in(_35800, _35806), 142 ^ _31078 : [(143 ^ _31078) ^ [] : [-(in(140 ^ [_35800, _35802, _35804, _35806], _35804))], (145 ^ _31078) ^ [] : [-(in(141 ^ [_35800, _35802, _35804, _35806], _35802))], (147 ^ _31078) ^ [] : [-(_35800 = ordered_pair(140 ^ [_35800, _35802, _35804, _35806], 141 ^ [_35800, _35802, _35804, _35806]))]]], (112 ^ _31078) ^ [_34962, _34964] : [114 ^ _31078 : [(115 ^ _31078) ^ [] : [-(in(113 ^ [_34962, _34964], _34964))], (117 ^ _31078) ^ [] : [in(113 ^ [_34962, _34964], _34962)]], -(subset(_34964, _34962))], (102 ^ _31078) ^ [_34648, _34650] : [subset(_34650, _34648), 105 ^ _31078 : [(106 ^ _31078) ^ [_34785] : [in(_34785, _34650), -(in(_34785, _34648))]]], (58 ^ _31078) ^ [_33047, _33049, _33051, _33053] : [-(unordered_pair(_33053, _33049) = unordered_pair(_33051, _33047)), _33053 = _33051, _33049 = _33047], (68 ^ _31078) ^ [_33378, _33380] : [_33380 = _33378, -(singleton(_33380) = singleton(_33378))], (74 ^ _31078) ^ [_33624, _33626, _33628, _33630] : [-(cartesian_product2(_33630, _33626) = cartesian_product2(_33628, _33624)), _33630 = _33628, _33626 = _33624], (84 ^ _31078) ^ [_33963, _33965, _33967, _33969] : [-(ordered_pair(_33969, _33965) = ordered_pair(_33967, _33963)), _33969 = _33967, _33965 = _33963], (2 ^ _31078) ^ [_31222] : [-(_31222 = _31222)], (4 ^ _31078) ^ [_31329, _31331] : [_31331 = _31329, -(_31329 = _31331)], (10 ^ _31078) ^ [_31533, _31535, _31537] : [-(_31537 = _31533), _31537 = _31535, _31535 = _31533], (20 ^ _31078) ^ [_31846, _31848] : [-(empty(_31846)), _31848 = _31846, empty(_31848)], (30 ^ _31078) ^ [_32169, _32171, _32173, _32175] : [-(in(_32173, _32169)), in(_32175, _32171), _32175 = _32173, _32171 = _32169], (44 ^ _31078) ^ [_32593, _32595, _32597, _32599] : [-(subset(_32597, _32593)), subset(_32599, _32595), _32599 = _32597, _32595 = _32593]], input).
% 0.36/1.37 ncf('1',plain,[subset(148 ^ [], 151 ^ [])],start(161 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(subset(148 ^ [], 151 ^ [])), 117 : in(113 ^ [151 ^ [], 148 ^ []], 151 ^ [])],extension(112 ^ 1,bind([[_34962, _34964], [151 ^ [], 148 ^ []]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(in(113 ^ [151 ^ [], 148 ^ []], 151 ^ [])), in(ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 151 ^ []), ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]) = 113 ^ [151 ^ [], 148 ^ []], 151 ^ [] = 151 ^ []],extension(30 ^ 4,bind([[_32169, _32171, _32173, _32175], [151 ^ [], 151 ^ [], 113 ^ [151 ^ [], 148 ^ []], ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []])]]))).
% 0.36/1.37 ncf('1.1.1.1',plain,[-(in(ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 151 ^ [])), in(ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 148 ^ [])],extension(155 ^ 5,bind([[_36930, _36932], [141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]]]))).
% 0.36/1.37 ncf('1.1.1.1.1',plain,[-(in(ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 148 ^ [])), in(113 ^ [151 ^ [], 148 ^ []], 148 ^ []), 113 ^ [151 ^ [], 148 ^ []] = ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 148 ^ [] = 148 ^ []],extension(30 ^ 6,bind([[_32169, _32171, _32173, _32175], [148 ^ [], 148 ^ [], ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 113 ^ [151 ^ [], 148 ^ []]]]))).
% 0.36/1.37 ncf('1.1.1.1.1.1',plain,[-(in(113 ^ [151 ^ [], 148 ^ []], 148 ^ []))],extension(115 ^ 7)).
% 0.36/1.37 ncf('1.1.1.1.1.2',plain,[-(113 ^ [151 ^ [], 148 ^ []] = ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []])), subset(148 ^ [], cartesian_product2(149 ^ [], 150 ^ [])), in(113 ^ [151 ^ [], 148 ^ []], 148 ^ [])],extension(133 ^ 7,bind([[_35800, _35802, _35804, _35806], [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.1.1.2.1',plain,[-(subset(148 ^ [], cartesian_product2(149 ^ [], 150 ^ [])))],extension(153 ^ 8)).
% 0.36/1.37 ncf('1.1.1.1.1.2.2',plain,[-(in(113 ^ [151 ^ [], 148 ^ []], 148 ^ []))],lemmata('[1, 1, 1, 1].x')).
% 0.36/1.37 ncf('1.1.1.1.1.3',plain,[-(148 ^ [] = 148 ^ [])],extension(2 ^ 7,bind([[_31222], [148 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.2',plain,[-(ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]) = 113 ^ [151 ^ [], 148 ^ []]), 113 ^ [151 ^ [], 148 ^ []] = ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []])],extension(4 ^ 5,bind([[_31329, _31331], [ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]), 113 ^ [151 ^ [], 148 ^ []]]]))).
% 0.36/1.37 ncf('1.1.1.2.1',plain,[-(113 ^ [151 ^ [], 148 ^ []] = ordered_pair(140 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []], 141 ^ [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []])), subset(148 ^ [], cartesian_product2(149 ^ [], 150 ^ [])), in(113 ^ [151 ^ [], 148 ^ []], 148 ^ [])],extension(133 ^ 6,bind([[_35800, _35802, _35804, _35806], [113 ^ [151 ^ [], 148 ^ []], 150 ^ [], 149 ^ [], 148 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.2.1.1',plain,[-(subset(148 ^ [], cartesian_product2(149 ^ [], 150 ^ [])))],extension(153 ^ 7)).
% 0.36/1.37 ncf('1.1.1.2.1.2',plain,[-(in(113 ^ [151 ^ [], 148 ^ []], 148 ^ []))],extension(115 ^ 7)).
% 0.36/1.37 ncf('1.1.1.3',plain,[-(151 ^ [] = 151 ^ [])],extension(2 ^ 5,bind([[_31222], [151 ^ []]]))).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------