%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG227+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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 10:08:18 EDT 2023
% Result : Theorem 0.60s 1.37s
% Output : Proof 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ALG227+1 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n028.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 23:33:18 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.60/1.37
% 0.60/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.60/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.60/1.37 %-----------------------------------------------------
% 0.60/1.37 ncf(matrix, plain, [(384 ^ _52675) ^ [] : [v1_xboole_0(382 ^ [])], (387 ^ _52675) ^ [] : [-(m1_pboole(385 ^ [], 382 ^ []))], (390 ^ _52675) ^ [] : [-(m1_subset_1(388 ^ [], 382 ^ []))], (392 ^ _52675) ^ [] : [r2_hidden(388 ^ [], k1_closure3(382 ^ [], 385 ^ []))], (394 ^ _52675) ^ [] : [k1_funct_1(385 ^ [], 388 ^ []) = k1_xboole_0], (122 ^ _52675) ^ [_56575, _56577, _56579, _56581] : [-(a_2_0_closure3(_56581, _56577) = a_2_0_closure3(_56579, _56575)), _56581 = _56579, _56577 = _56575], (132 ^ _52675) ^ [_56934, _56936, _56938, _56940] : [-(k1_closure3(_56940, _56936) = k1_closure3(_56938, _56934)), _56940 = _56938, _56936 = _56934], (142 ^ _52675) ^ [_57273, _57275, _57277, _57279] : [-(k1_funct_1(_57279, _57275) = k1_funct_1(_57277, _57273)), _57279 = _57277, _57275 = _57273], (2 ^ _52675) ^ [_52819] : [-(_52819 = _52819)], (4 ^ _52675) ^ [_52926, _52928] : [_52928 = _52926, -(_52926 = _52928)], (10 ^ _52675) ^ [_53130, _53132, _53134] : [-(_53134 = _53130), _53134 = _53132, _53132 = _53130], (20 ^ _52675) ^ [_53443, _53445] : [-(v1_fraenkel(_53443)), _53445 = _53443, v1_fraenkel(_53445)], (30 ^ _52675) ^ [_53738, _53740] : [-(v1_finset_1(_53738)), _53740 = _53738, v1_finset_1(_53740)], (40 ^ _52675) ^ [_54033, _54035] : [-(v1_relat_1(_54033)), _54035 = _54033, v1_relat_1(_54035)], (50 ^ _52675) ^ [_54328, _54330] : [-(v1_funct_1(_54328)), _54330 = _54328, v1_funct_1(_54330)], (60 ^ _52675) ^ [_54623, _54625] : [-(v2_funct_1(_54623)), _54625 = _54623, v2_funct_1(_54625)], (70 ^ _52675) ^ [_54918, _54920] : [-(v1_xboole_0(_54918)), _54920 = _54918, v1_xboole_0(_54920)], (80 ^ _52675) ^ [_55241, _55243, _55245, _55247] : [-(m1_pboole(_55245, _55241)), m1_pboole(_55247, _55243), _55247 = _55245, _55243 = _55241], (94 ^ _52675) ^ [_55685, _55687, _55689, _55691] : [-(m1_subset_1(_55689, _55685)), m1_subset_1(_55691, _55687), _55691 = _55689, _55687 = _55685], (108 ^ _52675) ^ [_56109, _56111, _56113, _56115] : [-(r2_hidden(_56113, _56109)), r2_hidden(_56115, _56111), _56115 = _56113, _56111 = _56109], (152 ^ _52675) ^ [_57614, _57616] : [r2_hidden(_57616, _57614), r2_hidden(_57614, _57616)], (158 ^ _52675) ^ [_57811] : [v1_xboole_0(_57811), -(v1_fraenkel(_57811))], (164 ^ _52675) ^ [_57997] : [v1_xboole_0(_57997), -(v1_finset_1(_57997))], (170 ^ _52675) ^ [_58183] : [v1_xboole_0(_58183), -(v1_funct_1(_58183))], (176 ^ _52675) ^ [_58369] : [187 ^ _52675 : [(188 ^ _52675) ^ [] : [-(v1_relat_1(_58369))], (190 ^ _52675) ^ [] : [-(v1_funct_1(_58369))], (192 ^ _52675) ^ [] : [-(v2_funct_1(_58369))]], v1_relat_1(_58369), v1_xboole_0(_58369), v1_funct_1(_58369)], (194 ^ _52675) ^ [_58862] : [-(v1_xboole_0(_58862)), 197 ^ _52675 : [(198 ^ _52675) ^ [_59013] : [m1_pboole(_59013, _58862), 201 ^ _52675 : [(202 ^ _52675) ^ [_59187] : [_59187 = k1_closure3(_58862, _59013), -(_59187 = a_2_0_closure3(_58862, _59013))], (208 ^ _52675) ^ [_59371] : [_59371 = a_2_0_closure3(_58862, _59013), -(_59371 = k1_closure3(_58862, _59013))]]]]], (214 ^ _52675) ^ [] : [true___, -(true___)], (220 ^ _52675) ^ [] : [true___, -(true___)], (226 ^ _52675) ^ [] : [true___, -(true___)], (232 ^ _52675) ^ [_59972, _59974] : [m1_pboole(_59972, _59974), 235 ^ _52675 : [(236 ^ _52675) ^ [] : [-(v1_relat_1(_59972))], (238 ^ _52675) ^ [] : [-(v1_funct_1(_59972))]]], (240 ^ _52675) ^ [] : [true___, -(true___)], (247 ^ _52675) ^ [_60382] : [-(m1_pboole(245 ^ [_60382], _60382))], (250 ^ _52675) ^ [_60504] : [-(m1_subset_1(248 ^ [_60504], _60504))], (252 ^ _52675) ^ [] : [-(v1_xboole_0(k1_xboole_0))], (254 ^ _52675) ^ [_60683, _60685, _60687] : [-(v1_xboole_0(_60685)), m1_pboole(_60683, _60685), 261 ^ _52675 : [(262 ^ _52675) ^ [] : [r2_hidden(_60687, a_2_0_closure3(_60685, _60683)), 266 ^ _52675 : [(267 ^ _52675) ^ [] : [-(m1_subset_1(265 ^ [_60683, _60685, _60687], _60685))], (269 ^ _52675) ^ [] : [-(_60687 = 265 ^ [_60683, _60685, _60687])], (271 ^ _52675) ^ [] : [k1_funct_1(_60683, 265 ^ [_60683, _60685, _60687]) = k1_xboole_0]]], (273 ^ _52675) ^ [] : [-(r2_hidden(_60687, a_2_0_closure3(_60685, _60683))), 274 ^ _52675 : [(275 ^ _52675) ^ [_61377] : [m1_subset_1(_61377, _60685), _60687 = _61377, -(k1_funct_1(_60683, _61377) = k1_xboole_0)]]]]], (288 ^ _52675) ^ [] : [-(v1_xboole_0(286 ^ []))], (290 ^ _52675) ^ [] : [-(v1_relat_1(286 ^ []))], (292 ^ _52675) ^ [] : [-(v1_funct_1(286 ^ []))], (294 ^ _52675) ^ [] : [-(v2_funct_1(286 ^ []))], (296 ^ _52675) ^ [] : [-(v1_finset_1(286 ^ []))], (298 ^ _52675) ^ [] : [-(v1_fraenkel(286 ^ []))], (301 ^ _52675) ^ [] : [v1_xboole_0(299 ^ [])], (303 ^ _52675) ^ [] : [-(v1_finset_1(299 ^ []))], (306 ^ _52675) ^ [] : [-(v1_relat_1(304 ^ []))], (308 ^ _52675) ^ [] : [-(v1_funct_1(304 ^ []))], (311 ^ _52675) ^ [] : [-(v1_xboole_0(309 ^ []))], (314 ^ _52675) ^ [] : [-(v1_relat_1(312 ^ []))], (316 ^ _52675) ^ [] : [-(v1_xboole_0(312 ^ []))], (318 ^ _52675) ^ [] : [-(v1_funct_1(312 ^ []))], (321 ^ _52675) ^ [] : [v1_xboole_0(319 ^ [])], (324 ^ _52675) ^ [] : [-(v1_relat_1(322 ^ []))], (326 ^ _52675) ^ [] : [-(v1_funct_1(322 ^ []))], (328 ^ _52675) ^ [] : [-(v2_funct_1(322 ^ []))], (330 ^ _52675) ^ [_63060, _63062] : [r2_hidden(_63062, _63060), -(m1_subset_1(_63062, _63060))], (336 ^ _52675) ^ [_63270, _63272] : [m1_subset_1(_63272, _63270), -(v1_xboole_0(_63270)), -(r2_hidden(_63272, _63270))], (346 ^ _52675) ^ [_63568, _63570] : [-(_63570 = _63568), 350 ^ _52675 : [(351 ^ _52675) ^ [] : [-(r2_hidden(347 ^ [_63568, _63570], _63570))], (353 ^ _52675) ^ [] : [r2_hidden(347 ^ [_63568, _63570], _63568)]], 354 ^ _52675 : [(355 ^ _52675) ^ [] : [-(r2_hidden(347 ^ [_63568, _63570], _63568))], (357 ^ _52675) ^ [] : [r2_hidden(347 ^ [_63568, _63570], _63570)]]], (361 ^ _52675) ^ [_64084] : [v1_xboole_0(_64084), -(_64084 = k1_xboole_0)], (367 ^ _52675) ^ [_64286, _64288] : [r2_hidden(_64288, _64286), v1_xboole_0(_64286)], (373 ^ _52675) ^ [_64473, _64475] : [v1_xboole_0(_64475), -(_64475 = _64473), v1_xboole_0(_64473)]], input).
% 0.60/1.37 ncf('1',plain,[v1_xboole_0(382 ^ [])],start(384 ^ 0)).
% 0.60/1.37 ncf('1.1',plain,[-(v1_xboole_0(382 ^ [])), 198 : m1_pboole(385 ^ [], 382 ^ []), 208 : a_2_0_closure3(382 ^ [], 385 ^ []) = a_2_0_closure3(382 ^ [], 385 ^ []), 208 : -(a_2_0_closure3(382 ^ [], 385 ^ []) = k1_closure3(382 ^ [], 385 ^ []))],extension(194 ^ 1,bind([[_58862, _59013, _59371], [382 ^ [], 385 ^ [], a_2_0_closure3(382 ^ [], 385 ^ [])]]))).
% 0.60/1.37 ncf('1.1.1',plain,[-(m1_pboole(385 ^ [], 382 ^ []))],extension(387 ^ 4)).
% 0.60/1.37 ncf('1.1.2',plain,[-(a_2_0_closure3(382 ^ [], 385 ^ []) = a_2_0_closure3(382 ^ [], 385 ^ [])), 382 ^ [] = 382 ^ [], 385 ^ [] = 385 ^ []],extension(122 ^ 6,bind([[_56575, _56577, _56579, _56581], [385 ^ [], 385 ^ [], 382 ^ [], 382 ^ []]]))).
% 0.60/1.37 ncf('1.1.2.1',plain,[-(382 ^ [] = 382 ^ [])],extension(2 ^ 7,bind([[_52819], [382 ^ []]]))).
% 0.60/1.37 ncf('1.1.2.2',plain,[-(385 ^ [] = 385 ^ [])],extension(2 ^ 7,bind([[_52819], [385 ^ []]]))).
% 0.60/1.37 ncf('1.1.3',plain,[a_2_0_closure3(382 ^ [], 385 ^ []) = k1_closure3(382 ^ [], 385 ^ []), -(r2_hidden(388 ^ [], k1_closure3(382 ^ [], 385 ^ []))), r2_hidden(388 ^ [], a_2_0_closure3(382 ^ [], 385 ^ [])), 388 ^ [] = 388 ^ []],extension(108 ^ 6,bind([[_56109, _56111, _56113, _56115], [k1_closure3(382 ^ [], 385 ^ []), a_2_0_closure3(382 ^ [], 385 ^ []), 388 ^ [], 388 ^ []]]))).
% 0.60/1.37 ncf('1.1.3.1',plain,[r2_hidden(388 ^ [], k1_closure3(382 ^ [], 385 ^ []))],extension(392 ^ 7)).
% 0.60/1.37 ncf('1.1.3.2',plain,[-(r2_hidden(388 ^ [], a_2_0_closure3(382 ^ [], 385 ^ []))), 275 : m1_subset_1(388 ^ [], 382 ^ []), 275 : 388 ^ [] = 388 ^ [], 275 : -(k1_funct_1(385 ^ [], 388 ^ []) = k1_xboole_0), 273 : -(v1_xboole_0(382 ^ [])), 273 : m1_pboole(385 ^ [], 382 ^ [])],extension(254 ^ 7,bind([[_60683, _60685, _60687, _61377], [385 ^ [], 382 ^ [], 388 ^ [], 388 ^ []]]))).
% 0.60/1.37 ncf('1.1.3.2.1',plain,[-(m1_subset_1(388 ^ [], 382 ^ []))],extension(390 ^ 12)).
% 0.60/1.37 ncf('1.1.3.2.2',plain,[-(388 ^ [] = 388 ^ [])],extension(2 ^ 12,bind([[_52819], [388 ^ []]]))).
% 0.60/1.37 ncf('1.1.3.2.3',plain,[k1_funct_1(385 ^ [], 388 ^ []) = k1_xboole_0],extension(394 ^ 12)).
% 0.60/1.37 ncf('1.1.3.2.4',plain,[v1_xboole_0(382 ^ [])],reduction('1')).
% 0.60/1.37 ncf('1.1.3.2.5',plain,[-(m1_pboole(385 ^ [], 382 ^ []))],lemmata('[1].x')).
% 0.60/1.37 ncf('1.1.3.3',plain,[-(388 ^ [] = 388 ^ [])],extension(2 ^ 7,bind([[_52819], [388 ^ []]]))).
% 0.60/1.37 %-----------------------------------------------------
% 0.60/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------