%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SET156+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:55:30 EDT 2023
% Result : Theorem 78.87s 76.90s
% Output : Proof 78.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SET156+4 : TPTP v8.1.2. Released v2.2.0.
% 0.00/0.11 % Command : nanocop.sh %s %d
% 0.11/0.31 % Computer : n002.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu May 18 19:05:04 EDT 2023
% 0.11/0.31 % CPUTime :
% 78.87/76.90
% 78.87/76.90 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 78.87/76.90 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 78.87/76.90 %-----------------------------------------------------
% 78.87/76.90 ncf(matrix, plain, [(306 ^ _61811) ^ [] : [equal_set(difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))], (304 ^ _61811) ^ [] : [-(subset(299 ^ [], 300 ^ []))], (302 ^ _61811) ^ [] : [-(subset(298 ^ [], 300 ^ []))], !, (183 ^ _51208) ^ [_57564, _57566, _57568] : [-(member(_57568, intersection(_57566, _57564))), member(_57568, _57566), member(_57568, _57564)], (221 ^ _51208) ^ [_58864, _58866, _58868] : [-(member(_58868, difference(_58864, _58866))), member(_58868, _58864), -(member(_58868, _58866))], (243 ^ _51208) ^ [_59638, _59640, _59642] : [member(_59642, unordered_pair(_59640, _59638)), -(_59642 = _59640), -(_59642 = _59638)], (74 ^ _51208) ^ [_53742, _53744, _53746, _53748] : [-(unordered_pair(_53748, _53744) = unordered_pair(_53746, _53742)), _53748 = _53746, _53744 = _53742], (203 ^ _51208) ^ [_58192, _58194, _58196] : [204 ^ _51208 : [(207 ^ _51208) ^ [] : [member(_58196, _58192)], (205 ^ _51208) ^ [] : [member(_58196, _58194)]], -(member(_58196, union(_58194, _58192)))], (237 ^ _51208) ^ [_59379, _59381] : [_59381 = _59379, -(member(_59381, singleton(_59379)))], (4 ^ _51208) ^ [_51439, _51441] : [_51441 = _51439, -(_51439 = _51441)], (193 ^ _51208) ^ [_57924, _57926, _57928] : [member(_57928, union(_57926, _57924)), -(member(_57928, _57926)), -(member(_57928, _57924))], (2 ^ _51208) ^ [_51332] : [-(_51332 = _51332)], (116 ^ _51208) ^ [_55235, _55237, _55239, _55241] : [-(difference(_55241, _55237) = difference(_55239, _55235)), _55241 = _55239, _55237 = _55235], (96 ^ _51208) ^ [_54537, _54539, _54541, _54543] : [-(intersection(_54543, _54539) = intersection(_54541, _54537)), _54543 = _54541, _54539 = _54537], (126 ^ _51208) ^ [_55621, _55623] : [subset(_55623, _55621), 129 ^ _51208 : [(130 ^ _51208) ^ [_55758] : [member(_55758, _55623), -(member(_55758, _55621))]]], (62 ^ _51208) ^ [_53278, _53280] : [_53280 = _53278, -(power_set(_53280) = power_set(_53278))], (136 ^ _51208) ^ [_55935, _55937] : [138 ^ _51208 : [(141 ^ _51208) ^ [] : [member(137 ^ [_55935, _55937], _55935)], (139 ^ _51208) ^ [] : [-(member(137 ^ [_55935, _55937], _55937))]], -(subset(_55937, _55935))], (169 ^ _51208) ^ [_57054, _57056] : [subset(_57056, _57054), -(member(_57056, power_set(_57054)))], (253 ^ _51208) ^ [_59906, _59908, _59910] : [254 ^ _51208 : [(257 ^ _51208) ^ [] : [_59910 = _59906], (255 ^ _51208) ^ [] : [_59910 = _59908]], -(member(_59910, unordered_pair(_59908, _59906)))], (270 ^ _51208) ^ [_60546, _60548] : [-(member(_60548, sum(_60546))), 271 ^ _51208 : [(272 ^ _51208) ^ [_60640] : [member(_60640, _60546), member(_60548, _60640)]]], (68 ^ _51208) ^ [_53496, _53498] : [_53498 = _53496, -(singleton(_53498) = singleton(_53496))], (280 ^ _51208) ^ [_60923, _60925] : [member(_60925, product(_60923)), 283 ^ _51208 : [(284 ^ _51208) ^ [_61064] : [member(_61064, _60923), -(member(_60925, _61064))]]], (20 ^ _51208) ^ [_51984, _51986, _51988, _51990] : [-(member(_51988, _51984)), member(_51990, _51986), _51990 = _51988, _51986 = _51984], (153 ^ _51208) ^ [_56558, _56560] : [-(equal_set(_56560, _56558)), subset(_56560, _56558), subset(_56558, _56560)], (211 ^ _51208) ^ [_58462] : [member(_58462, empty_set)], (84 ^ _51208) ^ [_54073, _54075] : [_54075 = _54073, -(sum(_54075) = sum(_54073))], (145 ^ _51208) ^ [_56321, _56323] : [equal_set(_56323, _56321), 148 ^ _51208 : [(151 ^ _51208) ^ [] : [-(subset(_56321, _56323))], (149 ^ _51208) ^ [] : [-(subset(_56323, _56321))]]], (261 ^ _51208) ^ [_60235, _60237] : [member(_60237, sum(_60235)), 265 ^ _51208 : [(268 ^ _51208) ^ [] : [-(member(_60237, 264 ^ [_60235, _60237]))], (266 ^ _51208) ^ [] : [-(member(264 ^ [_60235, _60237], _60235))]]], (90 ^ _51208) ^ [_54291, _54293] : [_54293 = _54291, -(product(_54293) = product(_54291))], (290 ^ _51208) ^ [_61241, _61243] : [292 ^ _51208 : [(295 ^ _51208) ^ [] : [member(_61243, 291 ^ [_61241, _61243])], (293 ^ _51208) ^ [] : [-(member(291 ^ [_61241, _61243], _61241))]], -(member(_61243, product(_61241)))], (163 ^ _51208) ^ [_56888, _56890] : [member(_56890, power_set(_56888)), -(subset(_56890, _56888))], (48 ^ _51208) ^ [_52852, _52854, _52856, _52858] : [-(equal_set(_52856, _52852)), equal_set(_52858, _52854), _52858 = _52856, _52854 = _52852], (34 ^ _51208) ^ [_52428, _52430, _52432, _52434] : [-(subset(_52432, _52428)), subset(_52434, _52430), _52434 = _52432, _52430 = _52428], (175 ^ _51208) ^ [_57313, _57315, _57317] : [member(_57317, intersection(_57315, _57313)), 178 ^ _51208 : [(181 ^ _51208) ^ [] : [-(member(_57317, _57313))], (179 ^ _51208) ^ [] : [-(member(_57317, _57315))]]], (10 ^ _51208) ^ [_51643, _51645, _51647] : [-(_51647 = _51643), _51647 = _51645, _51645 = _51643], (106 ^ _51208) ^ [_54896, _54898, _54900, _54902] : [-(union(_54902, _54898) = union(_54900, _54896)), _54902 = _54900, _54898 = _54896], (231 ^ _51208) ^ [_59213, _59215] : [member(_59215, singleton(_59213)), -(_59215 = _59213)], (213 ^ _51208) ^ [_58612, _58614, _58616] : [member(_58616, difference(_58612, _58614)), 216 ^ _51208 : [(219 ^ _51208) ^ [] : [member(_58616, _58614)], (217 ^ _51208) ^ [] : [-(member(_58616, _58612))]]]], input).
% 78.87/76.90 ncf('1',plain,[equal_set(difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))],start(306 ^ 0)).
% 78.87/76.90 ncf('1.1',plain,[-(equal_set(difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))), subset(difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))), subset(union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(153 ^ 1,bind([[_56558, _56560], [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]))).
% 78.87/76.90 ncf('1.1.1',plain,[-(subset(difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))), 139 : -(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))],extension(136 ^ 2,bind([[_55935, _55937], [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]))).
% 78.87/76.90 ncf('1.1.1.1',plain,[member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), 219 : member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ []))],extension(213 ^ 5,bind([[_58612, _58614, _58616], [300 ^ [], intersection(298 ^ [], 299 ^ []), 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1',plain,[-(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ []))), member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 298 ^ []), member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 299 ^ [])],extension(183 ^ 8,bind([[_57564, _57566, _57568], [299 ^ [], 298 ^ [], 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1.1',plain,[-(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 298 ^ [])), -(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ []))), member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 300 ^ [])],extension(221 ^ 9,bind([[_58864, _58866, _58868], [300 ^ [], 298 ^ [], 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1.1.1',plain,[member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ [])), -(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))))],extension(203 ^ 10,bind([[_58192, _58194, _58196], [difference(300 ^ [], 299 ^ []), difference(300 ^ [], 298 ^ []), 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1.1.1.1',plain,[member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))],extension(141 ^ 11)).
% 78.87/76.90 ncf('1.1.1.1.1.1.2',plain,[-(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 300 ^ []))],extension(217 ^ 10)).
% 78.87/76.90 ncf('1.1.1.1.1.2',plain,[-(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 299 ^ [])), -(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ []))), member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 300 ^ [])],extension(221 ^ 9,bind([[_58864, _58866, _58868], [300 ^ [], 299 ^ [], 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1.2.1',plain,[member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ [])), -(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))))],extension(203 ^ 10,bind([[_58192, _58194, _58196], [difference(300 ^ [], 299 ^ []), difference(300 ^ [], 298 ^ []), 137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.1.1.1.2.1.1',plain,[member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])))],extension(141 ^ 11)).
% 78.87/76.90 ncf('1.1.1.1.1.2.2',plain,[-(member(137 ^ [union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))], 300 ^ []))],extension(217 ^ 10)).
% 78.87/76.90 ncf('1.1.2',plain,[-(subset(union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ [])), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), 139 : -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))))],extension(136 ^ 2,bind([[_55935, _55937], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]))).
% 78.87/76.90 ncf('1.1.2.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ []))), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ [])))],extension(193 ^ 5,bind([[_57924, _57926, _57928], [difference(300 ^ [], 299 ^ []), difference(300 ^ [], 298 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ [])), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(183 ^ 6,bind([[_57564, _57566, _57568], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), difference(300 ^ [], 298 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(183 ^ 7,bind([[_57564, _57566, _57568], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), 181 : -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.1.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(141 ^ 11)).
% 78.87/76.90 ncf('1.1.2.1.1.1.2',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), difference(300 ^ [], 298 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.1.2.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 298 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))))],reduction('1.1.2.1.1')).
% 78.87/76.90 ncf('1.1.2.1.1.2',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 300 ^ []), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ [])))],extension(221 ^ 7,bind([[_58864, _58866, _58868], [300 ^ [], intersection(298 ^ [], 299 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.2.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 300 ^ [])), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ []))],extension(213 ^ 8,bind([[_58612, _58614, _58616], [300 ^ [], 298 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.2.1.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ [])))],reduction('1.1.2.1')).
% 78.87/76.90 ncf('1.1.2.1.1.2.2',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ [])), 179 : -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 298 ^ []))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [299 ^ [], 298 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.2.2.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 298 ^ []), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ []))],extension(213 ^ 11,bind([[_58612, _58614, _58616], [300 ^ [], 298 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.1.2.2.1.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 298 ^ [])))],reduction('1.1.2.1')).
% 78.87/76.90 ncf('1.1.2.1.2',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ [])), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(183 ^ 6,bind([[_57564, _57566, _57568], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), difference(300 ^ [], 299 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(183 ^ 7,bind([[_57564, _57566, _57568], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), 181 : -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.1.1.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))],extension(141 ^ 11)).
% 78.87/76.90 ncf('1.1.2.1.2.1.2',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ []))))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), difference(300 ^ [], 299 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.1.2.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(difference(300 ^ [], 299 ^ []), difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))))],reduction('1.1.2.1.2')).
% 78.87/76.90 ncf('1.1.2.1.2.2',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], intersection(298 ^ [], 299 ^ [])))), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 300 ^ []), -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ [])))],extension(221 ^ 7,bind([[_58864, _58866, _58868], [300 ^ [], intersection(298 ^ [], 299 ^ []), 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.2.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 300 ^ [])), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ []))],extension(213 ^ 8,bind([[_58612, _58614, _58616], [300 ^ [], 299 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.2.1.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ [])))],reduction('1.1.2.1')).
% 78.87/76.90 ncf('1.1.2.1.2.2.2',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], intersection(298 ^ [], 299 ^ [])), 181 : -(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 299 ^ []))],extension(175 ^ 8,bind([[_57313, _57315, _57317], [299 ^ [], 298 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.2.2.1',plain,[member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], 299 ^ []), member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ []))],extension(213 ^ 11,bind([[_58612, _58614, _58616], [300 ^ [], 299 ^ [], 137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))]]]))).
% 78.87/76.90 ncf('1.1.2.1.2.2.2.1.1',plain,[-(member(137 ^ [difference(300 ^ [], intersection(298 ^ [], 299 ^ [])), union(difference(300 ^ [], 298 ^ []), difference(300 ^ [], 299 ^ []))], difference(300 ^ [], 299 ^ [])))],reduction('1.1.2.1')).
% 78.87/76.90 %-----------------------------------------------------
% 78.87/76.90 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------