%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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 : Tue Jul 19 12:02:27 EDT 2022
% Result : Theorem 0.49s 1.44s
% Output : Proof 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0.
% 0.08/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n019.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Sun Jun 19 08:52:24 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.49/1.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.49/1.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.49/1.45
% 0.49/1.45 %-----------------------------------------------------
% 0.49/1.45 fof(t29_waybel_9, conjecture, ! [_86386] : (~ empty_carrier(_86386) & topological_space(_86386) & top_str(_86386) => ! [_86417] : (~ empty_carrier(_86417) & transitive_relstr(_86417) & directed_relstr(_86417) & net_str(_86417, _86386) => ! [_86458] : (element(_86458, the_carrier(_86386)) => in(_86458, lim_points_of_net(_86386, _86417)) => is_a_cluster_point_of_netstr(_86386, _86417, _86458)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t29_waybel_9)).
% 0.49/1.45 fof(d18_yellow_6, axiom, ! [_86981] : (~ empty_carrier(_86981) & topological_space(_86981) & top_str(_86981) => ! [_87012] : (~ empty_carrier(_87012) & transitive_relstr(_87012) & directed_relstr(_87012) & net_str(_87012, _86981) => ! [_87053] : (element(_87053, powerset(the_carrier(_86981))) => (_87053 = lim_points_of_net(_86981, _87012) <=> ! [_87092] : (element(_87092, the_carrier(_86981)) => (in(_87092, _87053) <=> ! [_87124] : (point_neighbourhood(_87124, _86981, _87092) => is_eventually_in(_86981, _87012, _87124)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d18_yellow_6)).
% 0.49/1.45 fof(d9_waybel_9, axiom, ! [_87569] : (~ empty_carrier(_87569) & topological_space(_87569) & top_str(_87569) => ! [_87600] : (~ empty_carrier(_87600) & net_str(_87600, _87569) => ! [_87627] : (element(_87627, the_carrier(_87569)) => (is_a_cluster_point_of_netstr(_87569, _87600, _87627) <=> ! [_87662] : (point_neighbourhood(_87662, _87569, _87627) => is_often_in(_87569, _87600, _87662)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d9_waybel_9)).
% 0.49/1.45 fof(dt_k11_yellow_6, axiom, ! [_88019, _88022] : (~ empty_carrier(_88019) & topological_space(_88019) & top_str(_88019) & ~ empty_carrier(_88022) & transitive_relstr(_88022) & directed_relstr(_88022) & net_str(_88022, _88019) => element(lim_points_of_net(_88019, _88022), powerset(the_carrier(_88019)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k11_yellow_6)).
% 0.49/1.45 fof(dt_l1_pre_topc, axiom, ! [_88340] : (top_str(_88340) => one_sorted_str(_88340)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_l1_pre_topc)).
% 0.49/1.45 fof(t28_yellow_6, axiom, ! [_88491] : (~ empty_carrier(_88491) & one_sorted_str(_88491) => ! [_88515] : (~ empty_carrier(_88515) & transitive_relstr(_88515) & directed_relstr(_88515) & net_str(_88515, _88491) => ! [_88556] : (is_eventually_in(_88491, _88515, _88556) => is_often_in(_88491, _88515, _88556)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t28_yellow_6)).
% 0.49/1.45
% 0.49/1.45 cnf(1, plain, [empty_carrier(18 ^ [])], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(2, plain, [-(topological_space(18 ^ []))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(3, plain, [-(top_str(18 ^ []))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(4, plain, [empty_carrier(19 ^ [])], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(5, plain, [-(transitive_relstr(19 ^ []))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(6, plain, [-(directed_relstr(19 ^ []))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(7, plain, [-(net_str(19 ^ [], 18 ^ []))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(8, plain, [-(element(20 ^ [], the_carrier(18 ^ [])))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(9, plain, [-(in(20 ^ [], lim_points_of_net(18 ^ [], 19 ^ [])))], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(10, plain, [is_a_cluster_point_of_netstr(18 ^ [], 19 ^ [], 20 ^ [])], clausify(t29_waybel_9)).
% 0.49/1.45 cnf(11, plain, [-(lim_points_of_net(_34233, _34366) = lim_points_of_net(_34300, _34431)), _34233 = _34300, _34366 = _34431], theory(equality)).
% 0.49/1.45 cnf(12, plain, [-(_22147 = _22147)], theory(equality)).
% 0.49/1.45 cnf(13, plain, [-(point_neighbourhood(_30719, _30886, _31049)), point_neighbourhood(_30634, _30803, _30968), _30634 = _30719, _30803 = _30886, _30968 = _31049], theory(equality)).
% 0.49/1.45 cnf(14, plain, [top_str(_37222), topological_space(_37222), -(empty_carrier(_37222)), net_str(_37517, _37222), directed_relstr(_37517), transitive_relstr(_37517), -(empty_carrier(_37517)), element(_37868, powerset(the_carrier(_37222))), _37868 = lim_points_of_net(_37222, _37517), element(_38148, the_carrier(_37222)), in(_38148, _37868), point_neighbourhood(_38355, _37222, _38148), -(is_eventually_in(_37222, _37517, _38355))], clausify(d18_yellow_6)).
% 0.49/1.45 cnf(15, plain, [top_str(_38825), topological_space(_38825), -(empty_carrier(_38825)), net_str(_39087, _38825), -(empty_carrier(_39087)), element(_39299, the_carrier(_38825)), -(is_a_cluster_point_of_netstr(_38825, _39087, _39299)), -(point_neighbourhood(4 ^ [_39299, _39087, _38825], _38825, _39299))], clausify(d9_waybel_9)).
% 0.49/1.45 cnf(16, plain, [top_str(_38825), topological_space(_38825), -(empty_carrier(_38825)), net_str(_39087, _38825), -(empty_carrier(_39087)), element(_39299, the_carrier(_38825)), -(is_a_cluster_point_of_netstr(_38825, _39087, _39299)), is_often_in(_38825, _39087, 4 ^ [_39299, _39087, _38825])], clausify(d9_waybel_9)).
% 0.49/1.45 cnf(17, plain, [-(element(lim_points_of_net(_39972, _40058), powerset(the_carrier(_39972)))), -(empty_carrier(_39972)), topological_space(_39972), top_str(_39972), -(empty_carrier(_40058)), transitive_relstr(_40058), directed_relstr(_40058), net_str(_40058, _39972)], clausify(dt_k11_yellow_6)).
% 0.49/1.45 cnf(18, plain, [top_str(_41259), -(one_sorted_str(_41259))], clausify(dt_l1_pre_topc)).
% 0.49/1.45 cnf(19, plain, [one_sorted_str(_48181), -(empty_carrier(_48181)), -(is_often_in(_48181, _48375, _48683)), is_eventually_in(_48181, _48375, _48683), -(empty_carrier(_48375)), transitive_relstr(_48375), directed_relstr(_48375), net_str(_48375, _48181)], clausify(t28_yellow_6)).
% 0.49/1.45
% 0.49/1.45 cnf('1',plain,[empty_carrier(19 ^ [])],start(4)).
% 0.49/1.45 cnf('1.1',plain,[-(empty_carrier(19 ^ [])), top_str(18 ^ []), topological_space(18 ^ []), -(empty_carrier(18 ^ [])), net_str(19 ^ [], 18 ^ []), directed_relstr(19 ^ []), transitive_relstr(19 ^ []), element(lim_points_of_net(18 ^ [], 19 ^ []), powerset(the_carrier(18 ^ []))), lim_points_of_net(18 ^ [], 19 ^ []) = lim_points_of_net(18 ^ [], 19 ^ []), element(20 ^ [], the_carrier(18 ^ [])), in(20 ^ [], lim_points_of_net(18 ^ [], 19 ^ [])), point_neighbourhood(4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [], 20 ^ []), -(is_eventually_in(18 ^ [], 19 ^ [], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []]))],extension(14,bind([[_37868, _38148, _37222, _37517, _38355], [lim_points_of_net(18 ^ [], 19 ^ []), 20 ^ [], 18 ^ [], 19 ^ [], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []]]]))).
% 0.49/1.45 cnf('1.1.1',plain,[-(top_str(18 ^ []))],extension(3)).
% 0.49/1.45 cnf('1.1.2',plain,[-(topological_space(18 ^ []))],extension(2)).
% 0.49/1.45 cnf('1.1.3',plain,[empty_carrier(18 ^ [])],extension(1)).
% 0.49/1.45 cnf('1.1.4',plain,[-(net_str(19 ^ [], 18 ^ []))],extension(7)).
% 0.49/1.45 cnf('1.1.5',plain,[-(directed_relstr(19 ^ []))],extension(6)).
% 0.49/1.45 cnf('1.1.6',plain,[-(transitive_relstr(19 ^ []))],extension(5)).
% 0.49/1.45 cnf('1.1.7',plain,[-(element(lim_points_of_net(18 ^ [], 19 ^ []), powerset(the_carrier(18 ^ [])))), -(empty_carrier(18 ^ [])), topological_space(18 ^ []), top_str(18 ^ []), -(empty_carrier(19 ^ [])), transitive_relstr(19 ^ []), directed_relstr(19 ^ []), net_str(19 ^ [], 18 ^ [])],extension(17,bind([[_40058, _39972], [19 ^ [], 18 ^ []]]))).
% 0.49/1.45 cnf('1.1.7.1',plain,[empty_carrier(18 ^ [])],extension(1)).
% 0.49/1.45 cnf('1.1.7.2',plain,[-(topological_space(18 ^ []))],extension(2)).
% 0.49/1.45 cnf('1.1.7.3',plain,[-(top_str(18 ^ []))],extension(3)).
% 0.49/1.45 cnf('1.1.7.4',plain,[empty_carrier(19 ^ [])],extension(4)).
% 0.49/1.45 cnf('1.1.7.5',plain,[-(transitive_relstr(19 ^ []))],extension(5)).
% 0.49/1.45 cnf('1.1.7.6',plain,[-(directed_relstr(19 ^ []))],extension(6)).
% 0.49/1.45 cnf('1.1.7.7',plain,[-(net_str(19 ^ [], 18 ^ []))],extension(7)).
% 0.49/1.45 cnf('1.1.8',plain,[-(lim_points_of_net(18 ^ [], 19 ^ []) = lim_points_of_net(18 ^ [], 19 ^ [])), 18 ^ [] = 18 ^ [], 19 ^ [] = 19 ^ []],extension(11,bind([[_34233, _34300, _34366, _34431], [18 ^ [], 18 ^ [], 19 ^ [], 19 ^ []]]))).
% 0.49/1.45 cnf('1.1.8.1',plain,[-(18 ^ [] = 18 ^ [])],extension(12,bind([[_22147], [18 ^ []]]))).
% 0.49/1.45 cnf('1.1.8.2',plain,[-(19 ^ [] = 19 ^ [])],extension(12,bind([[_22147], [19 ^ []]]))).
% 0.49/1.45 cnf('1.1.9',plain,[-(element(20 ^ [], the_carrier(18 ^ [])))],extension(8)).
% 0.49/1.45 cnf('1.1.10',plain,[-(in(20 ^ [], lim_points_of_net(18 ^ [], 19 ^ [])))],extension(9)).
% 0.49/1.45 cnf('1.1.11',plain,[-(point_neighbourhood(4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [], 20 ^ [])), point_neighbourhood(4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [], 20 ^ []), 4 ^ [20 ^ [], 19 ^ [], 18 ^ []] = 4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [] = 18 ^ [], 20 ^ [] = 20 ^ []],extension(13,bind([[_30634, _30719, _30803, _30886, _30968, _31049], [4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [], 18 ^ [], 20 ^ [], 20 ^ []]]))).
% 0.49/1.45 cnf('1.1.11.1',plain,[-(point_neighbourhood(4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 18 ^ [], 20 ^ [])), top_str(18 ^ []), topological_space(18 ^ []), -(empty_carrier(18 ^ [])), net_str(19 ^ [], 18 ^ []), -(empty_carrier(19 ^ [])), element(20 ^ [], the_carrier(18 ^ [])), -(is_a_cluster_point_of_netstr(18 ^ [], 19 ^ [], 20 ^ []))],extension(15,bind([[_38825, _39087, _39299], [18 ^ [], 19 ^ [], 20 ^ []]]))).
% 0.49/1.45 cnf('1.1.11.1.1',plain,[-(top_str(18 ^ []))],extension(3)).
% 0.49/1.45 cnf('1.1.11.1.2',plain,[-(topological_space(18 ^ []))],extension(2)).
% 0.49/1.45 cnf('1.1.11.1.3',plain,[empty_carrier(18 ^ [])],extension(1)).
% 0.49/1.45 cnf('1.1.11.1.4',plain,[-(net_str(19 ^ [], 18 ^ []))],extension(7)).
% 0.49/1.45 cnf('1.1.11.1.5',plain,[empty_carrier(19 ^ [])],extension(4)).
% 0.49/1.45 cnf('1.1.11.1.6',plain,[-(element(20 ^ [], the_carrier(18 ^ [])))],extension(8)).
% 0.49/1.45 cnf('1.1.11.1.7',plain,[is_a_cluster_point_of_netstr(18 ^ [], 19 ^ [], 20 ^ [])],extension(10)).
% 0.49/1.45 cnf('1.1.11.2',plain,[-(4 ^ [20 ^ [], 19 ^ [], 18 ^ []] = 4 ^ [20 ^ [], 19 ^ [], 18 ^ []])],extension(12,bind([[_22147], [4 ^ [20 ^ [], 19 ^ [], 18 ^ []]]]))).
% 0.49/1.45 cnf('1.1.11.3',plain,[-(18 ^ [] = 18 ^ [])],extension(12,bind([[_22147], [18 ^ []]]))).
% 0.49/1.45 cnf('1.1.11.4',plain,[-(20 ^ [] = 20 ^ [])],extension(12,bind([[_22147], [20 ^ []]]))).
% 0.49/1.45 cnf('1.1.12',plain,[is_eventually_in(18 ^ [], 19 ^ [], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []]), one_sorted_str(18 ^ []), -(empty_carrier(18 ^ [])), -(is_often_in(18 ^ [], 19 ^ [], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []])), -(empty_carrier(19 ^ [])), transitive_relstr(19 ^ []), directed_relstr(19 ^ []), net_str(19 ^ [], 18 ^ [])],extension(19,bind([[_48683, _48375, _48181], [4 ^ [20 ^ [], 19 ^ [], 18 ^ []], 19 ^ [], 18 ^ []]]))).
% 0.49/1.45 cnf('1.1.12.1',plain,[-(one_sorted_str(18 ^ [])), top_str(18 ^ [])],extension(18,bind([[_41259], [18 ^ []]]))).
% 0.49/1.45 cnf('1.1.12.1.1',plain,[-(top_str(18 ^ []))],extension(3)).
% 0.49/1.45 cnf('1.1.12.2',plain,[empty_carrier(18 ^ [])],extension(1)).
% 0.49/1.45 cnf('1.1.12.3',plain,[is_often_in(18 ^ [], 19 ^ [], 4 ^ [20 ^ [], 19 ^ [], 18 ^ []]), top_str(18 ^ []), topological_space(18 ^ []), -(empty_carrier(18 ^ [])), net_str(19 ^ [], 18 ^ []), -(empty_carrier(19 ^ [])), element(20 ^ [], the_carrier(18 ^ [])), -(is_a_cluster_point_of_netstr(18 ^ [], 19 ^ [], 20 ^ []))],extension(16,bind([[_38825, _39087, _39299], [18 ^ [], 19 ^ [], 20 ^ []]]))).
% 0.49/1.45 cnf('1.1.12.3.1',plain,[-(top_str(18 ^ []))],extension(3)).
% 0.49/1.45 cnf('1.1.12.3.2',plain,[-(topological_space(18 ^ []))],extension(2)).
% 0.49/1.45 cnf('1.1.12.3.3',plain,[empty_carrier(18 ^ [])],extension(1)).
% 0.49/1.45 cnf('1.1.12.3.4',plain,[-(net_str(19 ^ [], 18 ^ []))],extension(7)).
% 0.49/1.45 cnf('1.1.12.3.5',plain,[empty_carrier(19 ^ [])],extension(4)).
% 0.49/1.45 cnf('1.1.12.3.6',plain,[-(element(20 ^ [], the_carrier(18 ^ [])))],extension(8)).
% 0.49/1.45 cnf('1.1.12.3.7',plain,[is_a_cluster_point_of_netstr(18 ^ [], 19 ^ [], 20 ^ [])],extension(10)).
% 0.49/1.45 cnf('1.1.12.4',plain,[empty_carrier(19 ^ [])],extension(4)).
% 0.49/1.45 cnf('1.1.12.5',plain,[-(transitive_relstr(19 ^ []))],extension(5)).
% 0.49/1.45 cnf('1.1.12.6',plain,[-(directed_relstr(19 ^ []))],extension(6)).
% 0.49/1.45 cnf('1.1.12.7',plain,[-(net_str(19 ^ [], 18 ^ []))],extension(7)).
% 0.49/1.45 %-----------------------------------------------------
% 0.49/1.46
% 0.60/1.46 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------