%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : TOP021+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n024.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 : 600s
% DateTime : Thu Jul 21 21:31:35 EDT 2022
% Result : Theorem 0.37s 1.40s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : TOP021+1 : TPTP v8.1.0. Released v3.1.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n024.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 : 600
% 0.12/0.33 % DateTime : Sun May 29 04:42:51 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.37/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.41
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.41 fof(kelley_5_19a, conjecture, ! [_8143, _8146] : (a_locally_compact_top_space(the_product_top_space_over(_8143, _8146)) => ! [_8168] : a_locally_compact_top_space(apply(_8143, _8168))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', kelley_5_19a)).
% 0.37/1.41 fof(kelley_p90a, axiom, ! [_8348, _8351, _8354] : a_continuous_function_from_onto(the_projection_function(_8348, _8351, _8354), the_product_top_space_over(_8351, _8354), apply(_8351, _8348)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', kelley_p90a)).
% 0.37/1.41 fof(kelley_3_2, axiom, ! [_8539, _8542, _8545, _8548] : an_open_function_from_onto(the_projection_function(_8539, _8542, _8545), the_product_top_space_over(_8548, _8545), apply(_8548, _8539)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', kelley_3_2)).
% 0.37/1.41 fof(kelley_p_147e, axiom, ! [_8741, _8744, _8747] : (an_open_function_from_onto(_8741, _8744, _8747) & a_continuous_function_from_onto(_8741, _8744, _8747) & a_locally_compact_top_space(_8744) => a_locally_compact_top_space(_8747)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', kelley_p_147e)).
% 0.37/1.41
% 0.37/1.41 cnf(1, plain, [-(a_locally_compact_top_space(the_product_top_space_over(1 ^ [], 2 ^ [])))], clausify(kelley_5_19a)).
% 0.37/1.41 cnf(2, plain, [a_locally_compact_top_space(apply(1 ^ [], 3 ^ []))], clausify(kelley_5_19a)).
% 0.37/1.41 cnf(3, plain, [-(a_continuous_function_from_onto(the_projection_function(_3577, _3632, _3686), the_product_top_space_over(_3632, _3686), apply(_3632, _3577)))], clausify(kelley_p90a)).
% 0.37/1.41 cnf(4, plain, [-(an_open_function_from_onto(the_projection_function(_4084, _4144, _4203), the_product_top_space_over(_4261, _4203), apply(_4261, _4084)))], clausify(kelley_3_2)).
% 0.37/1.41 cnf(5, plain, [-(a_locally_compact_top_space(_4783)), an_open_function_from_onto(_4660, _4722, _4783), a_continuous_function_from_onto(_4660, _4722, _4783), a_locally_compact_top_space(_4722)], clausify(kelley_p_147e)).
% 0.37/1.41
% 0.37/1.41 cnf('1',plain,[a_locally_compact_top_space(apply(1 ^ [], 3 ^ []))],start(2)).
% 0.37/1.41 cnf('1.1',plain,[-(a_locally_compact_top_space(apply(1 ^ [], 3 ^ []))), an_open_function_from_onto(the_projection_function(3 ^ [], 1 ^ [], 2 ^ []), the_product_top_space_over(1 ^ [], 2 ^ []), apply(1 ^ [], 3 ^ [])), a_continuous_function_from_onto(the_projection_function(3 ^ [], 1 ^ [], 2 ^ []), the_product_top_space_over(1 ^ [], 2 ^ []), apply(1 ^ [], 3 ^ [])), a_locally_compact_top_space(the_product_top_space_over(1 ^ [], 2 ^ []))],extension(5,bind([[_4660, _4783, _4722], [the_projection_function(3 ^ [], 1 ^ [], 2 ^ []), apply(1 ^ [], 3 ^ []), the_product_top_space_over(1 ^ [], 2 ^ [])]]))).
% 0.37/1.41 cnf('1.1.1',plain,[-(an_open_function_from_onto(the_projection_function(3 ^ [], 1 ^ [], 2 ^ []), the_product_top_space_over(1 ^ [], 2 ^ []), apply(1 ^ [], 3 ^ [])))],extension(4,bind([[_4144, _4203, _4261, _4084], [1 ^ [], 2 ^ [], 1 ^ [], 3 ^ []]]))).
% 0.37/1.41 cnf('1.1.2',plain,[-(a_continuous_function_from_onto(the_projection_function(3 ^ [], 1 ^ [], 2 ^ []), the_product_top_space_over(1 ^ [], 2 ^ []), apply(1 ^ [], 3 ^ [])))],extension(3,bind([[_3686, _3632, _3577], [2 ^ [], 1 ^ [], 3 ^ []]]))).
% 0.37/1.41 cnf('1.1.3',plain,[-(a_locally_compact_top_space(the_product_top_space_over(1 ^ [], 2 ^ [])))],extension(1)).
% 0.37/1.41 %-----------------------------------------------------
% 0.37/1.42
% 0.37/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------