%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU386+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n021.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 : Wed Apr 9 08:53:50 PM UTC 2025
% Result : Theorem 25.52s 12.45s
% Output : CNFRefutation 25.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 6
% Syntax : Number of formulae : 30 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 170 ( 1 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 223 ( 83 ~; 96 |; 23 &)
% ( 3 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 11 con; 0-4 aty)
% Number of variables : 48 ( 48 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ point_neighbourhood > is_often_in > is_eventually_in > is_a_cluster_point_of_netstr > subset > net_str > in > element > transitive_relstr > topological_space > top_str > rel_str > preboolean > one_sorted_str > function > finite > empty_carrier > empty > directed_relstr > diff_closed > cup_closed > lim_points_of_net > #nlpp > the_carrier > powerset > empty_set > #skF_16 > #skF_20 > #skF_18 > #skF_11 > #skF_15 > #skF_8 > #skF_19 > #skF_4 > #skF_7 > #skF_5 > #skF_10 > #skF_6 > #skF_13 > #skF_2 > #skF_17 > #skF_3 > #skF_14 > #skF_1 > #skF_9 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(empty_carrier,type,
empty_carrier: $i > $o ).
tff(directed_relstr,type,
directed_relstr: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(cup_closed,type,
cup_closed: $i > $o ).
tff('#skF_20',type,
'#skF_20': $i ).
tff('#skF_18',type,
'#skF_18': $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(the_carrier,type,
the_carrier: $i > $i ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(finite,type,
finite: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(function,type,
function: $i > $o ).
tff('#skF_19',type,
'#skF_19': $i ).
tff(is_often_in,type,
is_often_in: ( $i * $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(is_a_cluster_point_of_netstr,type,
is_a_cluster_point_of_netstr: ( $i * $i * $i ) > $o ).
tff(is_eventually_in,type,
is_eventually_in: ( $i * $i * $i ) > $o ).
tff(net_str,type,
net_str: ( $i * $i ) > $o ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(one_sorted_str,type,
one_sorted_str: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff(preboolean,type,
preboolean: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff(diff_closed,type,
diff_closed: $i > $o ).
tff(transitive_relstr,type,
transitive_relstr: $i > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(empty,type,
empty: $i > $o ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(point_neighbourhood,type,
point_neighbourhood: ( $i * $i * $i ) > $o ).
tff(rel_str,type,
rel_str: $i > $o ).
tff(lim_points_of_net,type,
lim_points_of_net: ( $i * $i ) > $i ).
tff(powerset,type,
powerset: $i > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i * $i ) > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(topological_space,type,
topological_space: $i > $o ).
tff(top_str,type,
top_str: $i > $o ).
tff(f_304,negated_conjecture,
~ ! [A] :
( ( ~ empty_carrier(A)
& topological_space(A)
& top_str(A) )
=> ! [B] :
( ( ~ empty_carrier(B)
& transitive_relstr(B)
& directed_relstr(B)
& net_str(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,lim_points_of_net(A,B))
=> is_a_cluster_point_of_netstr(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_waybel_9) ).
tff(f_140,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
tff(f_131,axiom,
! [A,B] :
( ( ~ empty_carrier(A)
& topological_space(A)
& top_str(A)
& ~ empty_carrier(B)
& transitive_relstr(B)
& directed_relstr(B)
& net_str(B,A) )
=> element(lim_points_of_net(A,B),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_yellow_6) ).
tff(f_113,axiom,
! [A] :
( ( ~ empty_carrier(A)
& topological_space(A)
& top_str(A) )
=> ! [B] :
( ( ~ empty_carrier(B)
& net_str(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ( is_a_cluster_point_of_netstr(A,B,C)
<=> ! [D] :
( point_neighbourhood(D,A,C)
=> is_often_in(A,B,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_waybel_9) ).
tff(f_90,axiom,
! [A] :
( ( ~ empty_carrier(A)
& topological_space(A)
& top_str(A) )
=> ! [B] :
( ( ~ empty_carrier(B)
& transitive_relstr(B)
& directed_relstr(B)
& net_str(B,A) )
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( ( C = lim_points_of_net(A,B) )
<=> ! [D] :
( element(D,the_carrier(A))
=> ( in(D,C)
<=> ! [E] :
( point_neighbourhood(E,A,D)
=> is_eventually_in(A,B,E) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d18_yellow_6) ).
tff(f_279,axiom,
! [A] :
( ( ~ empty_carrier(A)
& one_sorted_str(A) )
=> ! [B] :
( ( ~ empty_carrier(B)
& transitive_relstr(B)
& directed_relstr(B)
& net_str(B,A) )
=> ! [C] :
( is_eventually_in(A,B,C)
=> is_often_in(A,B,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_yellow_6) ).
tff(c_138,plain,
~ empty_carrier('#skF_18'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_132,plain,
~ empty_carrier('#skF_19'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_120,plain,
~ is_a_cluster_point_of_netstr('#skF_18','#skF_19','#skF_20'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_136,plain,
topological_space('#skF_18'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_134,plain,
top_str('#skF_18'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_130,plain,
transitive_relstr('#skF_19'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_128,plain,
directed_relstr('#skF_19'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_126,plain,
net_str('#skF_19','#skF_18'),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_124,plain,
element('#skF_20',the_carrier('#skF_18')),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_196,plain,
! [A_183] :
( one_sorted_str(A_183)
| ~ top_str(A_183) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_204,plain,
one_sorted_str('#skF_18'),
inference(resolution,[status(thm)],[c_134,c_196]) ).
tff(c_122,plain,
in('#skF_20',lim_points_of_net('#skF_18','#skF_19')),
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_42,plain,
! [A_116,B_117] :
( element(lim_points_of_net(A_116,B_117),powerset(the_carrier(A_116)))
| ~ net_str(B_117,A_116)
| ~ directed_relstr(B_117)
| ~ transitive_relstr(B_117)
| empty_carrier(B_117)
| ~ top_str(A_116)
| ~ topological_space(A_116)
| empty_carrier(A_116) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_40,plain,
! [A_94,B_106,C_112] :
( point_neighbourhood('#skF_4'(A_94,B_106,C_112),A_94,C_112)
| is_a_cluster_point_of_netstr(A_94,B_106,C_112)
| ~ element(C_112,the_carrier(A_94))
| ~ net_str(B_106,A_94)
| empty_carrier(B_106)
| ~ top_str(A_94)
| ~ topological_space(A_94)
| empty_carrier(A_94) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_916,plain,
! [A_312,B_313,E_314,D_315] :
( is_eventually_in(A_312,B_313,E_314)
| ~ point_neighbourhood(E_314,A_312,D_315)
| ~ in(D_315,lim_points_of_net(A_312,B_313))
| ~ element(D_315,the_carrier(A_312))
| ~ element(lim_points_of_net(A_312,B_313),powerset(the_carrier(A_312)))
| ~ net_str(B_313,A_312)
| ~ directed_relstr(B_313)
| ~ transitive_relstr(B_313)
| empty_carrier(B_313)
| ~ top_str(A_312)
| ~ topological_space(A_312)
| empty_carrier(A_312) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_3705,plain,
! [A_498,B_499,B_500,C_501] :
( is_eventually_in(A_498,B_499,'#skF_4'(A_498,B_500,C_501))
| ~ in(C_501,lim_points_of_net(A_498,B_499))
| ~ element(lim_points_of_net(A_498,B_499),powerset(the_carrier(A_498)))
| ~ net_str(B_499,A_498)
| ~ directed_relstr(B_499)
| ~ transitive_relstr(B_499)
| empty_carrier(B_499)
| is_a_cluster_point_of_netstr(A_498,B_500,C_501)
| ~ element(C_501,the_carrier(A_498))
| ~ net_str(B_500,A_498)
| empty_carrier(B_500)
| ~ top_str(A_498)
| ~ topological_space(A_498)
| empty_carrier(A_498) ),
inference(resolution,[status(thm)],[c_40,c_916]) ).
tff(c_12444,plain,
! [A_701,B_702,B_703,C_704] :
( is_eventually_in(A_701,B_702,'#skF_4'(A_701,B_703,C_704))
| ~ in(C_704,lim_points_of_net(A_701,B_702))
| is_a_cluster_point_of_netstr(A_701,B_703,C_704)
| ~ element(C_704,the_carrier(A_701))
| ~ net_str(B_703,A_701)
| empty_carrier(B_703)
| ~ net_str(B_702,A_701)
| ~ directed_relstr(B_702)
| ~ transitive_relstr(B_702)
| empty_carrier(B_702)
| ~ top_str(A_701)
| ~ topological_space(A_701)
| empty_carrier(A_701) ),
inference(resolution,[status(thm)],[c_42,c_3705]) ).
tff(c_118,plain,
! [A_146,B_150,C_152] :
( is_often_in(A_146,B_150,C_152)
| ~ is_eventually_in(A_146,B_150,C_152)
| ~ net_str(B_150,A_146)
| ~ directed_relstr(B_150)
| ~ transitive_relstr(B_150)
| empty_carrier(B_150)
| ~ one_sorted_str(A_146)
| empty_carrier(A_146) ),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_706,plain,
! [A_286,B_287,C_288] :
( ~ is_often_in(A_286,B_287,'#skF_4'(A_286,B_287,C_288))
| is_a_cluster_point_of_netstr(A_286,B_287,C_288)
| ~ element(C_288,the_carrier(A_286))
| ~ net_str(B_287,A_286)
| empty_carrier(B_287)
| ~ top_str(A_286)
| ~ topological_space(A_286)
| empty_carrier(A_286) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_711,plain,
! [A_146,B_150,C_288] :
( is_a_cluster_point_of_netstr(A_146,B_150,C_288)
| ~ element(C_288,the_carrier(A_146))
| ~ top_str(A_146)
| ~ topological_space(A_146)
| ~ is_eventually_in(A_146,B_150,'#skF_4'(A_146,B_150,C_288))
| ~ net_str(B_150,A_146)
| ~ directed_relstr(B_150)
| ~ transitive_relstr(B_150)
| empty_carrier(B_150)
| ~ one_sorted_str(A_146)
| empty_carrier(A_146) ),
inference(resolution,[status(thm)],[c_118,c_706]) ).
tff(c_77717,plain,
! [A_1348,C_1349,B_1350] :
( ~ one_sorted_str(A_1348)
| ~ in(C_1349,lim_points_of_net(A_1348,B_1350))
| is_a_cluster_point_of_netstr(A_1348,B_1350,C_1349)
| ~ element(C_1349,the_carrier(A_1348))
| ~ net_str(B_1350,A_1348)
| ~ directed_relstr(B_1350)
| ~ transitive_relstr(B_1350)
| empty_carrier(B_1350)
| ~ top_str(A_1348)
| ~ topological_space(A_1348)
| empty_carrier(A_1348) ),
inference(resolution,[status(thm)],[c_12444,c_711]) ).
tff(c_77736,plain,
( ~ one_sorted_str('#skF_18')
| is_a_cluster_point_of_netstr('#skF_18','#skF_19','#skF_20')
| ~ element('#skF_20',the_carrier('#skF_18'))
| ~ net_str('#skF_19','#skF_18')
| ~ directed_relstr('#skF_19')
| ~ transitive_relstr('#skF_19')
| empty_carrier('#skF_19')
| ~ top_str('#skF_18')
| ~ topological_space('#skF_18')
| empty_carrier('#skF_18') ),
inference(resolution,[status(thm)],[c_122,c_77717]) ).
tff(c_77743,plain,
( is_a_cluster_point_of_netstr('#skF_18','#skF_19','#skF_20')
| empty_carrier('#skF_19')
| empty_carrier('#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_136,c_134,c_130,c_128,c_126,c_124,c_204,c_77736]) ).
tff(c_77745,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_138,c_132,c_120,c_77743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SEU386+1 : TPTP v9.0.0. Released v3.3.0.
% 0.08/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 23:03:44 EDT 2025
% 0.13/0.35 % CPUTime :
% 25.52/12.45 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.61/12.45
% 25.61/12.45 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------