%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n013.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 14:36:50 EDT 2022
% Result : Theorem 209.95s 210.11s
% Output : Refutation 209.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 18
% Syntax : Number of clauses : 40 ( 14 unt; 16 nHn; 40 RR)
% Number of literals : 183 ( 0 equ; 112 neg)
% Maximal clause size : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
topological_space(skc10),
file('SEU386+1.p',unknown),
[] ).
cnf(2,axiom,
top_str(skc10),
file('SEU386+1.p',unknown),
[] ).
cnf(3,axiom,
transitive_relstr(skc11),
file('SEU386+1.p',unknown),
[] ).
cnf(4,axiom,
directed_relstr(skc11),
file('SEU386+1.p',unknown),
[] ).
cnf(12,axiom,
~ empty_carrier(skc11),
file('SEU386+1.p',unknown),
[] ).
cnf(13,axiom,
~ empty_carrier(skc10),
file('SEU386+1.p',unknown),
[] ).
cnf(14,axiom,
net_str(skc11,skc10),
file('SEU386+1.p',unknown),
[] ).
cnf(22,axiom,
element(skc12,the_carrier(skc10)),
file('SEU386+1.p',unknown),
[] ).
cnf(25,axiom,
in(skc12,lim_points_of_net(skc10,skc11)),
file('SEU386+1.p',unknown),
[] ).
cnf(26,axiom,
~ is_a_cluster_point_of_netstr(skc10,skc11,skc12),
file('SEU386+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ top_str(u)
| one_sorted_str(u) ),
file('SEU386+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ one_sorted_str(u)
| ~ net_str(v,u)
| rel_str(v) ),
file('SEU386+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ in(u,v)
| ~ element(v,powerset(w))
| element(u,w) ),
file('SEU386+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ directed_relstr(u)
| ~ transitive_relstr(u)
| ~ one_sorted_str(v)
| ~ net_str(u,v)
| ~ is_eventually_in(v,u,w)
| empty_carrier(u)
| empty_carrier(v)
| is_often_in(v,u,w) ),
file('SEU386+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ transitive_relstr(u)
| ~ directed_relstr(u)
| ~ top_str(v)
| ~ topological_space(v)
| ~ net_str(u,v)
| empty_carrier(u)
| empty_carrier(v)
| element(lim_points_of_net(v,u),powerset(the_carrier(v))) ),
file('SEU386+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ top_str(u)
| ~ topological_space(u)
| ~ net_str(v,u)
| ~ element(w,the_carrier(u))
| empty_carrier(v)
| empty_carrier(u)
| is_a_cluster_point_of_netstr(u,v,w)
| point_neighbourhood(skf13(w,u,x),u,w) ),
file('SEU386+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ top_str(u)
| ~ topological_space(u)
| ~ net_str(v,u)
| ~ element(w,the_carrier(u))
| ~ is_often_in(u,v,skf13(w,u,v))
| empty_carrier(v)
| empty_carrier(u)
| is_a_cluster_point_of_netstr(u,v,w) ),
file('SEU386+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ topological_space(u)
| ~ top_str(u)
| ~ transitive_relstr(v)
| ~ directed_relstr(v)
| ~ in(w,x)
| ~ point_neighbourhood(y,u,w)
| ~ equal(x,lim_points_of_net(u,v))
| ~ element(w,the_carrier(u))
| ~ net_str(v,u)
| ~ element(x,powerset(the_carrier(u)))
| is_eventually_in(u,v,y)
| empty_carrier(u)
| empty_carrier(v) ),
file('SEU386+1.p',unknown),
[] ).
cnf(70,plain,
( ~ directed_relstr(u)
| ~ transitive_relstr(u)
| ~ top_str(v)
| ~ topological_space(v)
| ~ net_str(u,v)
| ~ in(w,x)
| ~ element(x,powerset(the_carrier(v)))
| ~ equal(x,lim_points_of_net(v,u))
| ~ point_neighbourhood(y,v,w)
| empty_carrier(u)
| empty_carrier(v)
| is_eventually_in(v,u,y) ),
inference(mrr,[status(thm)],[69,55]),
[iquote('0:MRR:69.7,55.2')] ).
cnf(99,plain,
one_sorted_str(skc10),
inference(res,[status(thm),theory(equality)],[2,32]),
[iquote('0:Res:2.0,32.0')] ).
cnf(112,plain,
( ~ topological_space(skc10)
| ~ top_str(skc10)
| ~ transitive_relstr(skc11)
| ~ directed_relstr(skc11)
| ~ in(u,v)
| ~ point_neighbourhood(w,skc10,u)
| ~ equal(v,lim_points_of_net(skc10,skc11))
| ~ element(v,powerset(the_carrier(skc10)))
| is_eventually_in(skc10,skc11,w)
| empty_carrier(skc10)
| empty_carrier(skc11) ),
inference(res,[status(thm),theory(equality)],[14,70]),
[iquote('0:Res:14.0,70.7')] ).
cnf(120,plain,
( ~ topological_space(skc10)
| ~ top_str(skc10)
| ~ element(u,the_carrier(skc10))
| point_neighbourhood(skf13(u,skc10,v),skc10,u)
| is_a_cluster_point_of_netstr(skc10,skc11,u)
| empty_carrier(skc10)
| empty_carrier(skc11) ),
inference(res,[status(thm),theory(equality)],[14,61]),
[iquote('0:Res:14.0,61.2')] ).
cnf(121,plain,
( ~ topological_space(skc10)
| ~ top_str(skc10)
| ~ directed_relstr(skc11)
| ~ transitive_relstr(skc11)
| empty_carrier(skc10)
| element(lim_points_of_net(skc10,skc11),powerset(the_carrier(skc10)))
| empty_carrier(skc11) ),
inference(res,[status(thm),theory(equality)],[14,60]),
[iquote('0:Res:14.0,60.4')] ).
cnf(123,plain,
( ~ one_sorted_str(skc10)
| rel_str(skc11) ),
inference(res,[status(thm),theory(equality)],[14,49]),
[iquote('0:Res:14.0,49.1')] ).
cnf(150,plain,
rel_str(skc11),
inference(mrr,[status(thm)],[123,99]),
[iquote('0:MRR:123.0,99.0')] ).
cnf(156,plain,
element(lim_points_of_net(skc10,skc11),powerset(the_carrier(skc10))),
inference(mrr,[status(thm)],[121,1,2,4,3,13,12]),
[iquote('0:MRR:121.0,121.1,121.2,121.3,121.4,121.6,1.0,2.0,4.0,3.0,13.0,12.0')] ).
cnf(161,plain,
( ~ element(u,the_carrier(skc10))
| is_a_cluster_point_of_netstr(skc10,skc11,u)
| point_neighbourhood(skf13(u,skc10,v),skc10,u) ),
inference(mrr,[status(thm)],[120,1,2,13,12]),
[iquote('0:MRR:120.0,120.1,120.5,120.6,1.0,2.0,13.0,12.0')] ).
cnf(167,plain,
( ~ in(u,v)
| ~ element(v,powerset(the_carrier(skc10)))
| ~ equal(v,lim_points_of_net(skc10,skc11))
| ~ point_neighbourhood(w,skc10,u)
| is_eventually_in(skc10,skc11,w) ),
inference(mrr,[status(thm)],[112,1,2,3,4,13,12]),
[iquote('0:MRR:112.0,112.1,112.2,112.3,112.9,112.10,1.0,2.0,3.0,4.0,13.0,12.0')] ).
cnf(319,plain,
( ~ directed_relstr(u)
| ~ transitive_relstr(u)
| ~ one_sorted_str(v)
| ~ top_str(v)
| ~ topological_space(v)
| ~ net_str(u,v)
| ~ is_eventually_in(v,u,skf13(w,v,u))
| ~ net_str(u,v)
| ~ element(w,the_carrier(v))
| empty_carrier(u)
| empty_carrier(v)
| empty_carrier(u)
| empty_carrier(v)
| is_a_cluster_point_of_netstr(v,u,w) ),
inference(res,[status(thm),theory(equality)],[59,62]),
[iquote('0:Res:59.7,62.4')] ).
cnf(322,plain,
( ~ directed_relstr(u)
| ~ transitive_relstr(u)
| ~ one_sorted_str(v)
| ~ top_str(v)
| ~ topological_space(v)
| ~ is_eventually_in(v,u,skf13(w,v,u))
| ~ net_str(u,v)
| ~ element(w,the_carrier(v))
| empty_carrier(u)
| empty_carrier(v)
| is_a_cluster_point_of_netstr(v,u,w) ),
inference(obv,[status(thm),theory(equality)],[319]),
[iquote('0:Obv:319.10')] ).
cnf(323,plain,
( ~ directed_relstr(u)
| ~ transitive_relstr(u)
| ~ top_str(v)
| ~ topological_space(v)
| ~ is_eventually_in(v,u,skf13(w,v,u))
| ~ net_str(u,v)
| ~ element(w,the_carrier(v))
| empty_carrier(u)
| empty_carrier(v)
| is_a_cluster_point_of_netstr(v,u,w) ),
inference(ssi,[status(thm)],[322,32]),
[iquote('0:SSi:322.2,32.1')] ).
cnf(1668,plain,
( ~ in(u,lim_points_of_net(skc10,skc11))
| ~ equal(lim_points_of_net(skc10,skc11),lim_points_of_net(skc10,skc11))
| ~ point_neighbourhood(v,skc10,u)
| is_eventually_in(skc10,skc11,v) ),
inference(res,[status(thm),theory(equality)],[156,167]),
[iquote('0:Res:156.0,167.1')] ).
cnf(1677,plain,
( ~ in(u,lim_points_of_net(skc10,skc11))
| ~ point_neighbourhood(v,skc10,u)
| is_eventually_in(skc10,skc11,v) ),
inference(obv,[status(thm),theory(equality)],[1668]),
[iquote('0:Obv:1668.1')] ).
cnf(4551,plain,
( ~ point_neighbourhood(u,skc10,skc12)
| is_eventually_in(skc10,skc11,u) ),
inference(res,[status(thm),theory(equality)],[25,1677]),
[iquote('0:Res:25.0,1677.0')] ).
cnf(4620,plain,
( ~ directed_relstr(skc11)
| ~ transitive_relstr(skc11)
| ~ top_str(skc10)
| ~ topological_space(skc10)
| ~ point_neighbourhood(skf13(u,skc10,skc11),skc10,skc12)
| ~ net_str(skc11,skc10)
| ~ element(u,the_carrier(skc10))
| empty_carrier(skc11)
| empty_carrier(skc10)
| is_a_cluster_point_of_netstr(skc10,skc11,u) ),
inference(res,[status(thm),theory(equality)],[4551,323]),
[iquote('0:Res:4551.1,323.4')] ).
cnf(4623,plain,
( ~ point_neighbourhood(skf13(u,skc10,skc11),skc10,skc12)
| ~ net_str(skc11,skc10)
| ~ element(u,the_carrier(skc10))
| empty_carrier(skc11)
| empty_carrier(skc10)
| is_a_cluster_point_of_netstr(skc10,skc11,u) ),
inference(ssi,[status(thm)],[4620,1,2,99,4,3,150]),
[iquote('0:SSi:4620.3,4620.2,4620.1,4620.0,1.0,2.0,99.0,1.0,2.0,99.0,4.0,3.0,150.0,4.0,3.0,150.0')] ).
cnf(4624,plain,
( ~ point_neighbourhood(skf13(u,skc10,skc11),skc10,skc12)
| ~ element(u,the_carrier(skc10))
| is_a_cluster_point_of_netstr(skc10,skc11,u) ),
inference(mrr,[status(thm)],[4623,14,12,13]),
[iquote('0:MRR:4623.1,4623.3,4623.4,14.0,12.0,13.0')] ).
cnf(62594,plain,
( ~ element(skc12,the_carrier(skc10))
| ~ element(skc12,the_carrier(skc10))
| is_a_cluster_point_of_netstr(skc10,skc11,skc12)
| is_a_cluster_point_of_netstr(skc10,skc11,skc12) ),
inference(res,[status(thm),theory(equality)],[161,4624]),
[iquote('0:Res:161.2,4624.0')] ).
cnf(62596,plain,
( ~ element(skc12,the_carrier(skc10))
| is_a_cluster_point_of_netstr(skc10,skc11,skc12) ),
inference(obv,[status(thm),theory(equality)],[62594]),
[iquote('0:Obv:62594.2')] ).
cnf(62597,plain,
$false,
inference(mrr,[status(thm)],[62596,22,26]),
[iquote('0:MRR:62596.0,62596.1,22.0,26.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SEU386+1 : TPTP v8.1.0. Released v3.3.0.
% 0.04/0.15 % Command : run_spass %d %s
% 0.14/0.37 % Computer : n013.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 600
% 0.14/0.37 % DateTime : Sun Jun 19 08:45:29 EDT 2022
% 0.14/0.37 % CPUTime :
% 209.95/210.11
% 209.95/210.11 SPASS V 3.9
% 209.95/210.11 SPASS beiseite: Proof found.
% 209.95/210.11 % SZS status Theorem
% 209.95/210.11 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 209.95/210.11 SPASS derived 53301 clauses, backtracked 5885 clauses, performed 33 splits and kept 32313 clauses.
% 209.95/210.11 SPASS allocated 173223 KBytes.
% 209.95/210.11 SPASS spent 0:3:18.50 on the problem.
% 209.95/210.11 0:00:00.03 for the input.
% 209.95/210.11 0:00:00.09 for the FLOTTER CNF translation.
% 209.95/210.11 0:00:01.59 for inferences.
% 209.95/210.11 0:0:10.65 for the backtracking.
% 209.95/210.11 0:03:03.61 for the reduction.
% 209.95/210.11
% 209.95/210.11
% 209.95/210.11 Here is a proof with depth 5, length 40 :
% 209.95/210.11 % SZS output start Refutation
% See solution above
% 209.95/210.11 Formulae used in the proof : t29_waybel_9 dt_l1_pre_topc dt_l1_waybel_0 t4_subset t28_yellow_6 dt_k11_yellow_6 d9_waybel_9 d18_yellow_6 existence_m1_subset_1
% 209.95/210.11
%------------------------------------------------------------------------------