%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : TOP021+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:39:03 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : TOP021+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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 20:01:48 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(22 ^ _8575) ^ [] : [-(a_locally_compact_top_space(the_product_top_space_over(19 ^ [], 20 ^ [])))], (25 ^ _8575) ^ [] : [a_locally_compact_top_space(apply(19 ^ [], 23 ^ []))], (2 ^ _8575) ^ [_8687, _8689, _8691] : [-(a_continuous_function_from_onto(the_projection_function(_8691, _8689, _8687), the_product_top_space_over(_8689, _8687), apply(_8689, _8691)))], (4 ^ _8575) ^ [_8822, _8824, _8826, _8828] : [-(an_open_function_from_onto(the_projection_function(_8828, _8826, _8824), the_product_top_space_over(_8822, _8824), apply(_8822, _8828)))], (6 ^ _8575) ^ [_8940, _8942, _8944] : [-(a_locally_compact_top_space(_8940)), an_open_function_from_onto(_8944, _8942, _8940), a_continuous_function_from_onto(_8944, _8942, _8940), a_locally_compact_top_space(_8942)]], input).
% 0.33/1.37 ncf('1',plain,[a_locally_compact_top_space(apply(19 ^ [], 23 ^ []))],start(25 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(a_locally_compact_top_space(apply(19 ^ [], 23 ^ []))), an_open_function_from_onto(the_projection_function(23 ^ [], 19 ^ [], 20 ^ []), the_product_top_space_over(19 ^ [], 20 ^ []), apply(19 ^ [], 23 ^ [])), a_continuous_function_from_onto(the_projection_function(23 ^ [], 19 ^ [], 20 ^ []), the_product_top_space_over(19 ^ [], 20 ^ []), apply(19 ^ [], 23 ^ [])), a_locally_compact_top_space(the_product_top_space_over(19 ^ [], 20 ^ []))],extension(6 ^ 1,bind([[_8940, _8942, _8944], [apply(19 ^ [], 23 ^ []), the_product_top_space_over(19 ^ [], 20 ^ []), the_projection_function(23 ^ [], 19 ^ [], 20 ^ [])]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(an_open_function_from_onto(the_projection_function(23 ^ [], 19 ^ [], 20 ^ []), the_product_top_space_over(19 ^ [], 20 ^ []), apply(19 ^ [], 23 ^ [])))],extension(4 ^ 2,bind([[_8822, _8824, _8826, _8828], [19 ^ [], 20 ^ [], 19 ^ [], 23 ^ []]]))).
% 0.33/1.37 ncf('1.1.2',plain,[-(a_continuous_function_from_onto(the_projection_function(23 ^ [], 19 ^ [], 20 ^ []), the_product_top_space_over(19 ^ [], 20 ^ []), apply(19 ^ [], 23 ^ [])))],extension(2 ^ 2,bind([[_8687, _8689, _8691], [20 ^ [], 19 ^ [], 23 ^ []]]))).
% 0.33/1.37 ncf('1.1.3',plain,[-(a_locally_compact_top_space(the_product_top_space_over(19 ^ [], 20 ^ [])))],extension(22 ^ 2)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------