%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET964+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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 43.12s 42.71s
% Output : Proof 43.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.10 % Problem : SET964+1 : TPTP v8.1.2. Released v3.2.0.
% 0.10/0.11 % Command : nanocop.sh %s %d
% 0.11/0.32 % Computer : n006.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu May 18 18:56:51 EDT 2023
% 0.11/0.32 % CPUTime :
% 43.12/42.71
% 43.12/42.71 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 43.12/42.71 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 43.12/42.71 %-----------------------------------------------------
% 43.12/42.71 ncf(matrix, plain, [(230 ^ _47689) ^ [] : [-(subset(cartesian_product2(225 ^ [], 224 ^ []), cartesian_product2(226 ^ [], 224 ^ []))), -(subset(cartesian_product2(224 ^ [], 225 ^ []), cartesian_product2(224 ^ [], 226 ^ [])))], (236 ^ _47689) ^ [] : [subset(225 ^ [], 226 ^ [])], (228 ^ _47689) ^ [] : [224 ^ [] = empty_set], !, (195 ^ _39098) ^ [] : [-(empty(empty_set))], (2 ^ _39098) ^ [_39222] : [-(_39222 = _39222)], (58 ^ _39098) ^ [_41047, _41049, _41051, _41053] : [-(unordered_pair(_41053, _41049) = unordered_pair(_41051, _41047)), _41053 = _41051, _41049 = _41047], (74 ^ _39098) ^ [_41624, _41626, _41628, _41630] : [-(ordered_pair(_41630, _41626) = ordered_pair(_41628, _41624)), _41630 = _41628, _41626 = _41624], (20 ^ _39098) ^ [_39874, _39876, _39878, _39880] : [-(in(_39878, _39874)), in(_39880, _39876), _39880 = _39878, _39876 = _39874], (100 ^ _39098) ^ [_42504, _42506] : [-(unordered_pair(_42506, _42504) = unordered_pair(_42504, _42506))], (223 ^ _39098) ^ [_47375, _47377] : [-(subset(_47377, _47377))], (115 ^ _39098) ^ [_43118, _43120, _43122] : [_43118 = cartesian_product2(_43122, _43120), 118 ^ _39098 : [(131 ^ _39098) ^ [_43879] : [-(in(_43879, _43118)), 132 ^ _39098 : [(133 ^ _39098) ^ [_44009, _44011] : [in(_44011, _43122), in(_44009, _43120), _43879 = ordered_pair(_44011, _44009)]]], (119 ^ _39098) ^ [_43319] : [in(_43319, _43118), 124 ^ _39098 : [(129 ^ _39098) ^ [] : [-(_43319 = ordered_pair(122 ^ [_43118, _43120, _43122, _43319], 123 ^ [_43118, _43120, _43122, _43319]))], (127 ^ _39098) ^ [] : [-(in(123 ^ [_43118, _43120, _43122, _43319], _43120))], (125 ^ _39098) ^ [] : [-(in(122 ^ [_43118, _43120, _43122, _43319], _43122))]]]]], (10 ^ _39098) ^ [_39533, _39535, _39537] : [-(_39537 = _39533), _39537 = _39535, _39535 = _39533], (44 ^ _39098) ^ [_40593, _40595, _40597, _40599] : [-(subset(_40597, _40593)), subset(_40599, _40595), _40599 = _40597, _40595 = _40593], (145 ^ _39098) ^ [_44375, _44377, _44379] : [-(_44375 = cartesian_product2(_44379, _44377)), 163 ^ _39098 : [(166 ^ _39098) ^ [] : [-(in(162 ^ [_44375, _44377, _44379], _44377))], (168 ^ _39098) ^ [] : [-(146 ^ [_44375, _44377, _44379] = ordered_pair(161 ^ [_44375, _44377, _44379], 162 ^ [_44375, _44377, _44379]))], (170 ^ _39098) ^ [] : [in(146 ^ [_44375, _44377, _44379], _44375)], (164 ^ _39098) ^ [] : [-(in(161 ^ [_44375, _44377, _44379], _44379))]], 149 ^ _39098 : [(152 ^ _39098) ^ [_44713, _44715] : [in(_44715, _44379), in(_44713, _44377), 146 ^ [_44375, _44377, _44379] = ordered_pair(_44715, _44713)], (150 ^ _39098) ^ [] : [-(in(146 ^ [_44375, _44377, _44379], _44375))]]], (4 ^ _39098) ^ [_39329, _39331] : [_39331 = _39329, -(_39329 = _39331)], (184 ^ _39098) ^ [_45966, _45968] : [186 ^ _39098 : [(189 ^ _39098) ^ [] : [in(185 ^ [_45966, _45968], _45966)], (187 ^ _39098) ^ [] : [-(in(185 ^ [_45966, _45968], _45968))]], -(subset(_45968, _45966))], (207 ^ _39098) ^ [_46898, _46900, _46902, _46904] : [-(in(ordered_pair(_46904, _46902), cartesian_product2(_46900, _46898))), in(_46904, _46900), in(_46902, _46898)], (108 ^ _39098) ^ [_42813] : [-(in(109 ^ [_42813], _42813)), -(_42813 = empty_set)], (174 ^ _39098) ^ [_45652, _45654] : [subset(_45654, _45652), 177 ^ _39098 : [(178 ^ _39098) ^ [_45789] : [in(_45789, _45654), -(in(_45789, _45652))]]], (218 ^ _39098) ^ [] : [-(empty(216 ^ []))], (84 ^ _39098) ^ [_41963, _41965, _41967, _41969] : [-(cartesian_product2(_41969, _41965) = cartesian_product2(_41967, _41963)), _41969 = _41967, _41965 = _41963], (102 ^ _39098) ^ [_42634] : [_42634 = empty_set, 105 ^ _39098 : [(106 ^ _39098) ^ [_42747] : [in(_42747, _42634)]]], (94 ^ _39098) ^ [_42308, _42310] : [in(_42310, _42308), in(_42308, _42310)], (221 ^ _39098) ^ [] : [empty(219 ^ [])], (34 ^ _39098) ^ [_40290, _40292] : [-(empty(_40290)), _40292 = _40290, empty(_40292)], (197 ^ _39098) ^ [_46465, _46467] : [empty(ordered_pair(_46467, _46465))], (193 ^ _39098) ^ [_46308, _46310] : [-(ordered_pair(_46310, _46308) = unordered_pair(unordered_pair(_46310, _46308), singleton(_46310)))], (68 ^ _39098) ^ [_41378, _41380] : [_41380 = _41378, -(singleton(_41380) = singleton(_41378))], (199 ^ _39098) ^ [_46633, _46635, _46637, _46639] : [in(ordered_pair(_46639, _46637), cartesian_product2(_46635, _46633)), 202 ^ _39098 : [(205 ^ _39098) ^ [] : [-(in(_46637, _46633))], (203 ^ _39098) ^ [] : [-(in(_46639, _46635))]]]], input).
% 43.12/42.71 ncf('1',plain,[-(subset(cartesian_product2(225 ^ [], 224 ^ []), cartesian_product2(226 ^ [], 224 ^ []))), -(subset(cartesian_product2(224 ^ [], 225 ^ []), cartesian_product2(224 ^ [], 226 ^ [])))],start(230 ^ 0)).
% 43.12/42.71 ncf('1.1',plain,[subset(cartesian_product2(225 ^ [], 224 ^ []), cartesian_product2(226 ^ [], 224 ^ [])), 178 : in(ordered_pair(185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]), cartesian_product2(225 ^ [], 224 ^ [])), 178 : -(in(ordered_pair(185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]), cartesian_product2(226 ^ [], 224 ^ [])))],extension(174 ^ 1,bind([[_45652, _45654, _45789], [cartesian_product2(226 ^ [], 224 ^ []), cartesian_product2(225 ^ [], 224 ^ []), ordered_pair(185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []])]]))).
% 43.12/42.71 ncf('1.1.1',plain,[-(in(ordered_pair(185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]), cartesian_product2(225 ^ [], 224 ^ []))), in(185 ^ [226 ^ [], 225 ^ []], 225 ^ []), in(109 ^ [224 ^ []], 224 ^ [])],extension(207 ^ 4,bind([[_46898, _46900, _46902, _46904], [224 ^ [], 225 ^ [], 109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]]]))).
% 43.12/42.71 ncf('1.1.1.1',plain,[-(in(185 ^ [226 ^ [], 225 ^ []], 225 ^ [])), -(subset(225 ^ [], 226 ^ []))],extension(184 ^ 5,bind([[_45966, _45968], [226 ^ [], 225 ^ []]]))).
% 43.12/42.71 ncf('1.1.1.1.1',plain,[subset(225 ^ [], 226 ^ [])],extension(236 ^ 6)).
% 43.12/42.71 ncf('1.1.1.2',plain,[-(in(109 ^ [224 ^ []], 224 ^ [])), -(224 ^ [] = empty_set)],extension(108 ^ 5,bind([[_42813], [224 ^ []]]))).
% 43.12/42.71 ncf('1.1.1.2.1',plain,[224 ^ [] = empty_set],extension(228 ^ 6)).
% 43.12/42.71 ncf('1.1.2',plain,[in(ordered_pair(185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]), cartesian_product2(226 ^ [], 224 ^ [])), 203 : -(in(185 ^ [226 ^ [], 225 ^ []], 226 ^ []))],extension(199 ^ 4,bind([[_46633, _46635, _46637, _46639], [224 ^ [], 226 ^ [], 109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]]]))).
% 43.12/42.71 ncf('1.1.2.1',plain,[in(185 ^ [226 ^ [], 225 ^ []], 226 ^ []), -(subset(225 ^ [], 226 ^ []))],extension(184 ^ 7,bind([[_45966, _45968], [226 ^ [], 225 ^ []]]))).
% 43.12/42.71 ncf('1.1.2.1.1',plain,[subset(225 ^ [], 226 ^ [])],extension(236 ^ 8)).
% 43.12/42.71 ncf('1.2',plain,[subset(cartesian_product2(224 ^ [], 225 ^ []), cartesian_product2(224 ^ [], 226 ^ [])), 178 : in(ordered_pair(109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]), cartesian_product2(224 ^ [], 225 ^ [])), 178 : -(in(ordered_pair(109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]), cartesian_product2(224 ^ [], 226 ^ [])))],extension(174 ^ 1,bind([[_45652, _45654, _45789], [cartesian_product2(224 ^ [], 226 ^ []), cartesian_product2(224 ^ [], 225 ^ []), ordered_pair(109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []])]]))).
% 43.12/42.71 ncf('1.2.1',plain,[-(in(ordered_pair(109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]), cartesian_product2(224 ^ [], 225 ^ []))), in(109 ^ [224 ^ []], 224 ^ []), in(185 ^ [226 ^ [], 225 ^ []], 225 ^ [])],extension(207 ^ 4,bind([[_46898, _46900, _46902, _46904], [225 ^ [], 224 ^ [], 185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]]]))).
% 43.12/42.71 ncf('1.2.1.1',plain,[-(in(109 ^ [224 ^ []], 224 ^ [])), -(224 ^ [] = empty_set)],extension(108 ^ 5,bind([[_42813], [224 ^ []]]))).
% 43.12/42.71 ncf('1.2.1.1.1',plain,[224 ^ [] = empty_set],extension(228 ^ 6)).
% 43.12/42.71 ncf('1.2.1.2',plain,[-(in(185 ^ [226 ^ [], 225 ^ []], 225 ^ [])), -(subset(225 ^ [], 226 ^ []))],extension(184 ^ 5,bind([[_45966, _45968], [226 ^ [], 225 ^ []]]))).
% 43.12/42.71 ncf('1.2.1.2.1',plain,[subset(225 ^ [], 226 ^ [])],extension(236 ^ 6)).
% 43.12/42.71 ncf('1.2.2',plain,[in(ordered_pair(109 ^ [224 ^ []], 185 ^ [226 ^ [], 225 ^ []]), cartesian_product2(224 ^ [], 226 ^ [])), 205 : -(in(185 ^ [226 ^ [], 225 ^ []], 226 ^ []))],extension(199 ^ 4,bind([[_46633, _46635, _46637, _46639], [226 ^ [], 224 ^ [], 185 ^ [226 ^ [], 225 ^ []], 109 ^ [224 ^ []]]]))).
% 43.12/42.71 ncf('1.2.2.1',plain,[in(185 ^ [226 ^ [], 225 ^ []], 226 ^ []), -(subset(225 ^ [], 226 ^ []))],extension(184 ^ 7,bind([[_45966, _45968], [226 ^ [], 225 ^ []]]))).
% 43.12/42.71 ncf('1.2.2.1.1',plain,[subset(225 ^ [], 226 ^ [])],extension(236 ^ 8)).
% 43.12/42.71 %-----------------------------------------------------
% 43.12/42.71 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------