%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET621+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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:09 EDT 2023
% Result : Theorem 42.67s 41.67s
% Output : Proof 42.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET621+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n005.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 18:47:23 EDT 2023
% 0.13/0.33 % CPUTime :
% 42.67/41.67
% 42.67/41.67 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 42.67/41.67 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.67/41.67 %-----------------------------------------------------
% 42.67/41.67 ncf(matrix, plain, [(197 ^ _31903) ^ [] : [difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ []) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))], (48 ^ _31903) ^ [_33575, _33577, _33579, _33581] : [-(symmetric_difference(_33581, _33577) = symmetric_difference(_33579, _33575)), _33581 = _33579, _33577 = _33575], (58 ^ _31903) ^ [_33934, _33936, _33938, _33940] : [-(difference(_33940, _33936) = difference(_33938, _33934)), _33940 = _33938, _33936 = _33934], (68 ^ _31903) ^ [_34273, _34275, _34277, _34279] : [-(union(_34279, _34275) = union(_34277, _34273)), _34279 = _34277, _34275 = _34273], (2 ^ _31903) ^ [_32047] : [-(_32047 = _32047)], (4 ^ _31903) ^ [_32154, _32156] : [_32156 = _32154, -(_32154 = _32156)], (10 ^ _31903) ^ [_32358, _32360, _32362] : [-(_32362 = _32358), _32362 = _32360, _32360 = _32358], (20 ^ _31903) ^ [_32699, _32701, _32703, _32705] : [-(member(_32703, _32699)), member(_32705, _32701), _32705 = _32703, _32701 = _32699], (34 ^ _31903) ^ [_33123, _33125, _33127, _33129] : [-(subset(_33127, _33123)), subset(_33129, _33125), _33129 = _33127, _33125 = _33123], (78 ^ _31903) ^ [_34599, _34601] : [-(symmetric_difference(_34601, _34599) = union(difference(_34601, _34599), difference(_34599, _34601)))], (80 ^ _31903) ^ [_34719, _34721, _34723] : [-(difference(difference(_34723, _34721), _34719) = difference(_34723, union(_34721, _34719)))], (82 ^ _31903) ^ [_34841, _34843, _34845] : [-(difference(union(_34845, _34843), _34841) = union(difference(_34845, _34841), difference(_34843, _34841)))], (94 ^ _31903) ^ [_35278, _35280, _35282] : [95 ^ _31903 : [(96 ^ _31903) ^ [] : [member(_35278, _35282)], (98 ^ _31903) ^ [] : [member(_35278, _35280)]], -(member(_35278, union(_35282, _35280)))], (84 ^ _31903) ^ [_35010, _35012, _35014] : [member(_35010, union(_35014, _35012)), -(member(_35010, _35014)), -(member(_35010, _35012))], (102 ^ _31903) ^ [_35621, _35623, _35625] : [member(_35621, difference(_35625, _35623)), 105 ^ _31903 : [(106 ^ _31903) ^ [] : [-(member(_35621, _35625))], (108 ^ _31903) ^ [] : [member(_35621, _35623)]]], (110 ^ _31903) ^ [_35873, _35875, _35877] : [-(member(_35873, difference(_35877, _35875))), member(_35873, _35877), -(member(_35873, _35875))], (120 ^ _31903) ^ [_36222, _36224] : [_36224 = _36222, 123 ^ _31903 : [(124 ^ _31903) ^ [] : [-(subset(_36224, _36222))], (126 ^ _31903) ^ [] : [-(subset(_36222, _36224))]]], (128 ^ _31903) ^ [_36459, _36461] : [-(_36461 = _36459), subset(_36461, _36459), subset(_36459, _36461)], (138 ^ _31903) ^ [_36745, _36747] : [-(union(_36747, _36745) = union(_36745, _36747))], (140 ^ _31903) ^ [_36845, _36847] : [-(symmetric_difference(_36847, _36845) = symmetric_difference(_36845, _36847))], (192 ^ _31903) ^ [_38689] : [-(subset(_38689, _38689))], (183 ^ _31903) ^ [_38381, _38383] : [185 ^ _31903 : [(186 ^ _31903) ^ [] : [-(member(184 ^ [_38381, _38383], _38383))], (188 ^ _31903) ^ [] : [member(184 ^ [_38381, _38383], _38381)]], -(subset(_38383, _38381))], (173 ^ _31903) ^ [_38067, _38069] : [subset(_38069, _38067), 176 ^ _31903 : [(177 ^ _31903) ^ [_38204] : [member(_38204, _38069), -(member(_38204, _38067))]]], (158 ^ _31903) ^ [_37506, _37508] : [-(_37508 = _37506), 162 ^ _31903 : [(163 ^ _31903) ^ [] : [-(member(159 ^ [_37506, _37508], _37508))], (165 ^ _31903) ^ [] : [member(159 ^ [_37506, _37508], _37506)]], 166 ^ _31903 : [(167 ^ _31903) ^ [] : [-(member(159 ^ [_37506, _37508], _37506))], (169 ^ _31903) ^ [] : [member(159 ^ [_37506, _37508], _37508)]]], (142 ^ _31903) ^ [_36989, _36991] : [_36991 = _36989, 145 ^ _31903 : [(146 ^ _31903) ^ [_37155] : [member(_37155, _36991), -(member(_37155, _36989))], (152 ^ _31903) ^ [_37327] : [member(_37327, _36989), -(member(_37327, _36991))]]]], input).
% 42.67/41.68 ncf('1',plain,[difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ []) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))],start(197 ^ 0)).
% 42.67/41.68 ncf('1.1',plain,[-(difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ []) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))), difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ []) = difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))],extension(10 ^ 1,bind([[_32358, _32360, _32362], [union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ []))), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []), difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ [])]]))).
% 42.67/41.68 ncf('1.1.1',plain,[-(difference(symmetric_difference(193 ^ [], 194 ^ []), 195 ^ []) = difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ [])), symmetric_difference(193 ^ [], 194 ^ []) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ [] = 195 ^ []],extension(58 ^ 2,bind([[_33934, _33936, _33938, _33940], [195 ^ [], 195 ^ [], union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), symmetric_difference(193 ^ [], 194 ^ [])]]))).
% 42.67/41.68 ncf('1.1.1.1',plain,[-(symmetric_difference(193 ^ [], 194 ^ []) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ []))), symmetric_difference(193 ^ [], 194 ^ []) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ []))],extension(10 ^ 3,bind([[_32358, _32360, _32362], [union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), symmetric_difference(193 ^ [], 194 ^ [])]]))).
% 42.67/41.68 ncf('1.1.1.1.1',plain,[-(symmetric_difference(193 ^ [], 194 ^ []) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])))],extension(78 ^ 4,bind([[_34599, _34601], [194 ^ [], 193 ^ []]]))).
% 42.67/41.68 ncf('1.1.1.1.2',plain,[-(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])) = union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])))],extension(2 ^ 4,bind([[_32047], [union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ []))]]))).
% 42.67/41.68 ncf('1.1.1.2',plain,[-(195 ^ [] = 195 ^ [])],extension(2 ^ 3,bind([[_32047], [195 ^ []]]))).
% 42.67/41.68 ncf('1.1.2',plain,[-(difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])), union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))],extension(10 ^ 2,bind([[_32358, _32360, _32362], [union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ []))), union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ [])]]))).
% 42.67/41.68 ncf('1.1.2.1',plain,[-(difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ []))), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])), union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ []))],extension(10 ^ 3,bind([[_32358, _32360, _32362], [union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])), union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])), difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ [])]]))).
% 42.67/41.68 ncf('1.1.2.1.1',plain,[-(difference(union(difference(193 ^ [], 194 ^ []), difference(194 ^ [], 193 ^ [])), 195 ^ []) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])))],extension(82 ^ 4,bind([[_34841, _34843, _34845], [195 ^ [], difference(194 ^ [], 193 ^ []), difference(193 ^ [], 194 ^ [])]]))).
% 42.67/41.68 ncf('1.1.2.1.2',plain,[-(union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])) = union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])))],extension(2 ^ 4,bind([[_32047], [union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ []))]]))).
% 42.67/41.68 ncf('1.1.2.2',plain,[-(union(difference(difference(193 ^ [], 194 ^ []), 195 ^ []), difference(difference(194 ^ [], 193 ^ []), 195 ^ [])) = union(difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(194 ^ [], union(193 ^ [], 195 ^ [])))), difference(difference(193 ^ [], 194 ^ []), 195 ^ []) = difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(difference(194 ^ [], 193 ^ []), 195 ^ []) = difference(194 ^ [], union(193 ^ [], 195 ^ []))],extension(68 ^ 3,bind([[_34273, _34275, _34277, _34279], [difference(194 ^ [], union(193 ^ [], 195 ^ [])), difference(difference(194 ^ [], 193 ^ []), 195 ^ []), difference(193 ^ [], union(194 ^ [], 195 ^ [])), difference(difference(193 ^ [], 194 ^ []), 195 ^ [])]]))).
% 42.67/41.68 ncf('1.1.2.2.1',plain,[-(difference(difference(193 ^ [], 194 ^ []), 195 ^ []) = difference(193 ^ [], union(194 ^ [], 195 ^ [])))],extension(80 ^ 4,bind([[_34719, _34721, _34723], [195 ^ [], 194 ^ [], 193 ^ []]]))).
% 42.67/41.68 ncf('1.1.2.2.2',plain,[-(difference(difference(194 ^ [], 193 ^ []), 195 ^ []) = difference(194 ^ [], union(193 ^ [], 195 ^ [])))],extension(80 ^ 4,bind([[_34719, _34721, _34723], [195 ^ [], 193 ^ [], 194 ^ []]]))).
% 42.67/41.68 %-----------------------------------------------------
% 42.67/41.68 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------