%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU251+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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 12:02:52 EDT 2023
% Result : Theorem 237.38s 229.12s
% Output : Proof 237.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU251+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n003.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 13:32:30 EDT 2023
% 0.12/0.33 % CPUTime :
% 237.38/229.12
% 237.38/229.12 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 237.38/229.12 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.38/229.12 %-----------------------------------------------------
% 237.38/229.12 ncf(matrix, plain, [(475 ^ _92191) ^ [] : [-(relation(473 ^ []))], (477 ^ _92191) ^ [] : [subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ []))], !, (118 ^ _76756) ^ [_80619, _80621, _80623, _80625] : [-(ordered_pair(_80625, _80621) = ordered_pair(_80623, _80619)), _80625 = _80623, _80621 = _80619], (255 ^ _76756) ^ [_85447, _85449] : [subset(_85449, _85447), 258 ^ _76756 : [(259 ^ _76756) ^ [_85584] : [in(_85584, _85449), -(in(_85584, _85447))]]], (54 ^ _76756) ^ [_78566, _78568, _78570, _78572] : [-(in(_78570, _78566)), in(_78572, _78568), _78572 = _78570, _78568 = _78566], (208 ^ _76756) ^ [_83690] : [relation(_83690), 211 ^ _76756 : [(234 ^ _76756) ^ [_84642, _84644] : [-(_84642 = fiber(_83690, _84644)), 246 ^ _76756 : [(247 ^ _76756) ^ [] : [235 ^ [_83690, _84642, _84644] = _84644], (251 ^ _76756) ^ [] : [in(235 ^ [_83690, _84642, _84644], _84642)], (249 ^ _76756) ^ [] : [-(in(ordered_pair(235 ^ [_83690, _84642, _84644], _84644), _83690))]], 238 ^ _76756 : [(239 ^ _76756) ^ [] : [-(in(235 ^ [_83690, _84642, _84644], _84642))], (241 ^ _76756) ^ [] : [-(235 ^ [_83690, _84642, _84644] = _84644), in(ordered_pair(235 ^ [_83690, _84642, _84644], _84644), _83690)]]], (212 ^ _76756) ^ [_83894, _83896] : [_83894 = fiber(_83690, _83896), 215 ^ _76756 : [(216 ^ _76756) ^ [_84083] : [in(_84083, _83894), 219 ^ _76756 : [(220 ^ _76756) ^ [] : [_84083 = _83896], (222 ^ _76756) ^ [] : [-(in(ordered_pair(_84083, _83896), _83690))]]], (224 ^ _76756) ^ [_84349] : [-(in(_84349, _83894)), -(_84349 = _83896), in(ordered_pair(_84349, _83896), _83690)]]]]], (300 ^ _76756) ^ [] : [true___, -(true___)], (400 ^ _76756) ^ [_89611, _89613] : [in(_89613, _89611), -(element(_89613, _89611))], (306 ^ _76756) ^ [] : [true___, -(true___)], (88 ^ _76756) ^ [_79580, _79582, _79584, _79586] : [-(subset(_79584, _79580)), subset(_79586, _79582), _79586 = _79584, _79582 = _79580], (378 ^ _76756) ^ [_88955, _88957, _88959] : [relation(_88955), 381 ^ _76756 : [(382 ^ _76756) ^ [] : [in(_88959, relation_restriction(_88955, _88957)), 385 ^ _76756 : [(386 ^ _76756) ^ [] : [-(in(_88959, _88955))], (388 ^ _76756) ^ [] : [-(in(_88959, cartesian_product2(_88957, _88957)))]]], (390 ^ _76756) ^ [] : [-(in(_88959, relation_restriction(_88955, _88957))), in(_88959, _88955), in(_88959, cartesian_product2(_88957, _88957))]]], (318 ^ _76756) ^ [] : [true___, -(true___)], (345 ^ _76756) ^ [] : [-(empty(empty_set))], (138 ^ _76756) ^ [_81337, _81339, _81341, _81343] : [-(set_intersection2(_81343, _81339) = set_intersection2(_81341, _81337)), _81343 = _81341, _81339 = _81337], (374 ^ _76756) ^ [] : [-(one_to_one(368 ^ []))], (376 ^ _76756) ^ [_88832, _88834] : [-(subset(_88834, _88834))], (148 ^ _76756) ^ [_81668, _81670] : [_81670 = _81668, -(powerset(_81670) = powerset(_81668))], (312 ^ _76756) ^ [_87046, _87048] : [relation(_87048), -(relation(relation_restriction(_87048, _87046)))], (68 ^ _76756) ^ [_78982, _78984] : [-(empty(_78982)), _78984 = _78982, empty(_78984)], (347 ^ _76756) ^ [_87893, _87895] : [empty(ordered_pair(_87895, _87893))], (4 ^ _76756) ^ [_76987, _76989] : [_76989 = _76987, -(_76987 = _76989)], (265 ^ _76756) ^ [_85761, _85763] : [267 ^ _76756 : [(268 ^ _76756) ^ [] : [-(in(266 ^ [_85761, _85763], _85763))], (270 ^ _76756) ^ [] : [in(266 ^ [_85761, _85763], _85761)]], -(subset(_85763, _85761))], (343 ^ _76756) ^ [_87744] : [-(element(341 ^ [_87744], _87744))], (102 ^ _76756) ^ [_80042, _80044, _80046, _80048] : [-(unordered_pair(_80048, _80044) = unordered_pair(_80046, _80042)), _80048 = _80046, _80044 = _80042], (112 ^ _76756) ^ [_80373, _80375] : [_80375 = _80373, -(singleton(_80375) = singleton(_80373))], (180 ^ _76756) ^ [_82811] : [empty(_82811), -(function(_82811))], (408 ^ _76756) ^ [_89902, _89904] : [element(_89904, _89902), -(empty(_89902)), -(in(_89904, _89902))], (128 ^ _76756) ^ [_80978, _80980, _80982, _80984] : [-(cartesian_product2(_80984, _80980) = cartesian_product2(_80982, _80978)), _80984 = _80982, _80980 = _80978], (450 ^ _76756) ^ [_91248] : [empty(_91248), -(_91248 = empty_set)], (2 ^ _76756) ^ [_76880] : [-(_76880 = _76880)], (206 ^ _76756) ^ [_83589, _83591] : [-(set_intersection2(_83591, _83589) = set_intersection2(_83589, _83591))], (367 ^ _76756) ^ [] : [empty(365 ^ [])], (20 ^ _76756) ^ [_77504, _77506] : [-(function(_77504)), _77506 = _77504, function(_77506)], (30 ^ _76756) ^ [_77799, _77801] : [-(one_to_one(_77799)), _77801 = _77799, one_to_one(_77801)], (418 ^ _76756) ^ [_90229, _90231] : [element(_90231, powerset(_90229)), -(subset(_90231, _90229))], (462 ^ _76756) ^ [_91637, _91639] : [empty(_91639), -(_91639 = _91637), empty(_91637)], (456 ^ _76756) ^ [_91450, _91452] : [in(_91452, _91450), empty(_91450)], (330 ^ _76756) ^ [] : [true___, -(true___)], (362 ^ _76756) ^ [] : [-(empty(358 ^ []))], (364 ^ _76756) ^ [] : [-(function(358 ^ []))], (336 ^ _76756) ^ [] : [true___, -(true___)], (324 ^ _76756) ^ [] : [true___, -(true___)], (430 ^ _76756) ^ [_90625, _90627, _90629] : [-(element(_90629, _90625)), in(_90629, _90627), element(_90627, powerset(_90625))], (282 ^ _76756) ^ [] : [true___, -(true___)], (186 ^ _76756) ^ [_82997] : [197 ^ _76756 : [(198 ^ _76756) ^ [] : [-(relation(_82997))], (202 ^ _76756) ^ [] : [-(one_to_one(_82997))], (200 ^ _76756) ^ [] : [-(function(_82997))]], relation(_82997), empty(_82997), function(_82997)], (10 ^ _76756) ^ [_77191, _77193, _77195] : [-(_77195 = _77191), _77195 = _77193, _77193 = _77191], (424 ^ _76756) ^ [_90395, _90397] : [subset(_90397, _90395), -(element(_90397, powerset(_90395)))], (360 ^ _76756) ^ [] : [-(relation(358 ^ []))], (164 ^ _76756) ^ [_82253, _82255, _82257, _82259] : [-(fiber(_82259, _82255) = fiber(_82257, _82253)), _82259 = _82257, _82255 = _82253], (370 ^ _76756) ^ [] : [-(relation(368 ^ []))], (204 ^ _76756) ^ [_83489, _83491] : [-(unordered_pair(_83491, _83489) = unordered_pair(_83489, _83491))], (372 ^ _76756) ^ [] : [-(function(368 ^ []))], (406 ^ _76756) ^ [_89792] : [-(set_intersection2(_89792, empty_set) = empty_set)], (440 ^ _76756) ^ [_90952, _90954, _90956] : [in(_90956, _90954), element(_90954, powerset(_90952)), empty(_90952)], (78 ^ _76756) ^ [_79277, _79279] : [-(relation(_79277)), _79279 = _79277, relation(_79279)], (349 ^ _76756) ^ [_87989, _87991] : [-(set_intersection2(_87991, _87991) = _87991)], (274 ^ _76756) ^ [_86103, _86105] : [-(ordered_pair(_86105, _86103) = unordered_pair(unordered_pair(_86105, _86103), singleton(_86105)))], (294 ^ _76756) ^ [] : [true___, -(true___)], (154 ^ _76756) ^ [_81914, _81916, _81918, _81920] : [-(relation_restriction(_81920, _81916) = relation_restriction(_81918, _81914)), _81920 = _81918, _81916 = _81914], (357 ^ _76756) ^ [] : [-(empty(355 ^ []))], (276 ^ _76756) ^ [_86209] : [relation(_86209), 279 ^ _76756 : [(280 ^ _76756) ^ [_86328] : [-(relation_restriction(_86209, _86328) = set_intersection2(_86209, cartesian_product2(_86328, _86328)))]]], (352 ^ _76756) ^ [] : [-(relation(350 ^ []))], (288 ^ _76756) ^ [] : [true___, -(true___)], (174 ^ _76756) ^ [_82614, _82616] : [in(_82616, _82614), in(_82614, _82616)], (40 ^ _76756) ^ [_78122, _78124, _78126, _78128] : [-(element(_78126, _78122)), element(_78128, _78124), _78128 = _78126, _78124 = _78122], (354 ^ _76756) ^ [] : [-(function(350 ^ []))]], input).
% 237.38/229.12 ncf('1',plain,[-(relation(473 ^ []))],start(475 ^ 0)).
% 237.38/229.12 ncf('1.1',plain,[relation(473 ^ []), 212 : fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ []), 224 : -(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ []))), 224 : -(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])] = 472 ^ []), 224 : in(ordered_pair(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], 472 ^ []), 473 ^ [])],extension(208 ^ 1,bind([[_83690, _83894, _83896, _84349], [473 ^ [], fiber(473 ^ [], 472 ^ []), 472 ^ [], 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.1',plain,[-(fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ [])), fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ [])],extension(4 ^ 4,bind([[_76987, _76989], [fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.1.1',plain,[-(fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ []))],extension(2 ^ 5,bind([[_76880], [fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2',plain,[in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ [])), 259 : -(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ []))), 259 : subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []))],extension(255 ^ 6,bind([[_85447, _85449, _85584], [fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []), 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.2.1',plain,[in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ [])), 259 : -(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ []))), 259 : subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []))],extension(255 ^ 9,bind([[_85447, _85449, _85584], [fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []), 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.2.1.1',plain,[in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(473 ^ [], 472 ^ [])), -(subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ [])))],extension(265 ^ 12,bind([[_85761, _85763], [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2.1.1.1',plain,[subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ []))],extension(477 ^ 13)).
% 237.38/229.12 ncf('1.1.2.1.2',plain,[-(subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ [])))],extension(376 ^ 10,bind([[_88832, _88834], [_55372, fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2.2',plain,[-(subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []))), subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ [])), fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ [])],extension(88 ^ 7,bind([[_79580, _79582, _79584, _79586], [fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2.2.1',plain,[-(subset(fiber(473 ^ [], 472 ^ []), fiber(473 ^ [], 472 ^ [])))],extension(376 ^ 8,bind([[_88832, _88834], [_55691, fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2.2.2',plain,[-(fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ []))],extension(2 ^ 8,bind([[_76880], [fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.2.2.3',plain,[-(fiber(473 ^ [], 472 ^ []) = fiber(473 ^ [], 472 ^ []))],extension(2 ^ 8,bind([[_76880], [fiber(473 ^ [], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.3',plain,[266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])] = 472 ^ [], 216 : in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])), 216 : fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), 212 : relation(relation_restriction(473 ^ [], 471 ^ []))],extension(208 ^ 6,bind([[_83690, _83894, _83896, _84083], [relation_restriction(473 ^ [], 471 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), 472 ^ [], 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.3.1',plain,[-(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))), 259 : in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])), 259 : subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))],extension(255 ^ 11,bind([[_85447, _85449, _85584], [fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.3.1.1',plain,[-(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))), -(subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ [])))],extension(265 ^ 14,bind([[_85761, _85763], [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.3.1.1.1',plain,[subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ []))],extension(477 ^ 15)).
% 237.38/229.12 ncf('1.1.3.1.2',plain,[-(subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])))],extension(376 ^ 12,bind([[_88832, _88834], [_57333, fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.3.2',plain,[-(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])],extension(4 ^ 9,bind([[_76987, _76989], [fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.3.2.1',plain,[-(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))],extension(2 ^ 10,bind([[_76880], [fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.3.3',plain,[-(relation(relation_restriction(473 ^ [], 471 ^ []))), relation(473 ^ [])],extension(312 ^ 7,bind([[_87046, _87048], [471 ^ [], 473 ^ []]]))).
% 237.38/229.12 ncf('1.1.3.3.1',plain,[-(relation(473 ^ []))],reduction('1')).
% 237.38/229.12 ncf('1.1.4',plain,[-(in(ordered_pair(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], 472 ^ []), 473 ^ [])), 382 : in(ordered_pair(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], 472 ^ []), relation_restriction(473 ^ [], 471 ^ [])), 382 : relation(473 ^ [])],extension(378 ^ 6,bind([[_88955, _88957, _88959], [473 ^ [], 471 ^ [], ordered_pair(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.4.1',plain,[-(in(ordered_pair(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], 472 ^ []), relation_restriction(473 ^ [], 471 ^ []))), 216 : in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])), 216 : fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), 212 : relation(relation_restriction(473 ^ [], 471 ^ []))],extension(208 ^ 9,bind([[_83690, _83894, _83896, _84083], [relation_restriction(473 ^ [], 471 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), 472 ^ [], 266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]]))).
% 237.38/229.12 ncf('1.1.4.1.1',plain,[-(in(266 ^ [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])], fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))), -(subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ [])))],extension(265 ^ 14,bind([[_85761, _85763], [fiber(473 ^ [], 472 ^ []), fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.4.1.1.1',plain,[subset(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []), fiber(473 ^ [], 472 ^ []))],extension(477 ^ 15)).
% 237.38/229.12 ncf('1.1.4.1.2',plain,[-(fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []) = fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ []))],extension(2 ^ 12,bind([[_76880], [fiber(relation_restriction(473 ^ [], 471 ^ []), 472 ^ [])]]))).
% 237.38/229.12 ncf('1.1.4.1.3',plain,[-(relation(relation_restriction(473 ^ [], 471 ^ []))), relation(473 ^ [])],extension(312 ^ 10,bind([[_87046, _87048], [471 ^ [], 473 ^ []]]))).
% 237.38/229.12 ncf('1.1.4.1.3.1',plain,[-(relation(473 ^ []))],reduction('1')).
% 237.38/229.12 ncf('1.1.4.2',plain,[-(relation(473 ^ []))],reduction('1')).
% 237.38/229.12 %-----------------------------------------------------
% 237.38/229.12 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------