%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU394+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n020.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:52 PM UTC 2025
% Result : Theorem 25.98s 10.50s
% Output : CNFRefutation 25.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 44 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 153 ( 14 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 179 ( 70 ~; 73 |; 26 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 44 ( 42 usr; 1 prp; 0-3 aty)
% Number of functors : 56 ( 56 usr; 18 con; 0-4 aty)
% Number of variables : 35 ( 34 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ relation_of2_as_subset > relation_of2 > quasi_total > is_eventually_in > upper_relstr_subset > subset > strict_net_str > proper_element > net_str > lower_relstr_subset > in > filtered_subset > element > directed_subset > with_suprema_relstr > with_infima_relstr > v1_yellow_3 > upper_bounded_relstr > up_complete_relstr > trivial_carrier > transitive_relstr > strict_rel_str > relation_empty_yielding > relation > rel_str > reflexive_relstr > one_sorted_str > lower_bounded_relstr > join_complete_relstr > heyting_relstr > function > finite > empty_carrier > empty > distributive_relstr > directed_relstr > connected_relstr > complete_relstr > complemented_relstr > bounded_relstr > boolean_relstr > antisymmetric_relstr > net_str_of > net_of_bool_filter > the_mapping > set_difference > rel_str_of > filter_of_net_str > cartesian_product2 > a_2_1_yellow19 > #nlpp > the_carrier > the_InternalRel > singleton > powerset > cast_as_carrier_subset > boole_POSet > empty_set > #skF_9 > #skF_36 > #skF_25 > #skF_5 > #skF_21 > #skF_41 > #skF_16 > #skF_6 > #skF_20 > #skF_18 > #skF_17 > #skF_35 > #skF_11 > #skF_31 > #skF_22 > #skF_38 > #skF_37 > #skF_8 > #skF_19 > #skF_10 > #skF_34 > #skF_29 > #skF_15 > #skF_26 > #skF_14 > #skF_28 > #skF_39 > #skF_13 > #skF_2 > #skF_1 > #skF_32 > #skF_7 > #skF_23 > #skF_33 > #skF_3 > #skF_24 > #skF_27 > #skF_40 > #skF_30 > #skF_12 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_36',type,
'#skF_36': $i > $i ).
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(empty_carrier,type,
empty_carrier: $i > $o ).
tff(directed_relstr,type,
directed_relstr: $i > $o ).
tff(relation,type,
relation: $i > $o ).
tff(filter_of_net_str,type,
filter_of_net_str: ( $i * $i ) > $i ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff('#skF_41',type,
'#skF_41': ( $i * $i ) > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(set_difference,type,
set_difference: ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff(the_InternalRel,type,
the_InternalRel: $i > $i ).
tff(complete_relstr,type,
complete_relstr: $i > $o ).
tff('#skF_20',type,
'#skF_20': $i ).
tff('#skF_18',type,
'#skF_18': $i ).
tff(singleton,type,
singleton: $i > $i ).
tff('#skF_17',type,
'#skF_17': $i ).
tff(with_suprema_relstr,type,
with_suprema_relstr: $i > $o ).
tff('#skF_35',type,
'#skF_35': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(upper_relstr_subset,type,
upper_relstr_subset: ( $i * $i ) > $o ).
tff(quasi_total,type,
quasi_total: ( $i * $i * $i ) > $o ).
tff('#skF_31',type,
'#skF_31': $i > $i ).
tff(the_carrier,type,
the_carrier: $i > $i ).
tff(net_of_bool_filter,type,
net_of_bool_filter: ( $i * $i * $i ) > $i ).
tff(filtered_subset,type,
filtered_subset: ( $i * $i ) > $o ).
tff('#skF_22',type,
'#skF_22': $i > $i ).
tff(directed_subset,type,
directed_subset: ( $i * $i ) > $o ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(finite,type,
finite: $i > $o ).
tff('#skF_38',type,
'#skF_38': $i ).
tff('#skF_37',type,
'#skF_37': $i > $i ).
tff(proper_element,type,
proper_element: ( $i * $i ) > $o ).
tff(heyting_relstr,type,
heyting_relstr: $i > $o ).
tff(lower_relstr_subset,type,
lower_relstr_subset: ( $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(function,type,
function: $i > $o ).
tff('#skF_19',type,
'#skF_19': $i ).
tff(relation_empty_yielding,type,
relation_empty_yielding: $i > $o ).
tff(is_eventually_in,type,
is_eventually_in: ( $i * $i * $i ) > $o ).
tff(antisymmetric_relstr,type,
antisymmetric_relstr: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(up_complete_relstr,type,
up_complete_relstr: $i > $o ).
tff('#skF_34',type,
'#skF_34': $i > $i ).
tff(net_str,type,
net_str: ( $i * $i ) > $o ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff('#skF_15',type,
'#skF_15': $i > $i ).
tff('#skF_26',type,
'#skF_26': $i ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff(strict_rel_str,type,
strict_rel_str: $i > $o ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(boole_POSet,type,
boole_POSet: $i > $i ).
tff(reflexive_relstr,type,
reflexive_relstr: $i > $o ).
tff(one_sorted_str,type,
one_sorted_str: $i > $o ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff('#skF_39',type,
'#skF_39': $i ).
tff(a_2_1_yellow19,type,
a_2_1_yellow19: ( $i * $i ) > $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff(v1_yellow_3,type,
v1_yellow_3: $i > $o ).
tff(lower_bounded_relstr,type,
lower_bounded_relstr: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(transitive_relstr,type,
transitive_relstr: $i > $o ).
tff(rel_str_of,type,
rel_str_of: ( $i * $i ) > $i ).
tff(bounded_relstr,type,
bounded_relstr: $i > $o ).
tff(net_str_of,type,
net_str_of: ( $i * $i * $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(cast_as_carrier_subset,type,
cast_as_carrier_subset: $i > $i ).
tff(connected_relstr,type,
connected_relstr: $i > $o ).
tff(empty,type,
empty: $i > $o ).
tff(strict_net_str,type,
strict_net_str: ( $i * $i ) > $o ).
tff(distributive_relstr,type,
distributive_relstr: $i > $o ).
tff('#skF_32',type,
'#skF_32': $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff(relation_of2,type,
relation_of2: ( $i * $i * $i ) > $o ).
tff('#skF_33',type,
'#skF_33': $i > $i ).
tff(with_infima_relstr,type,
with_infima_relstr: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff(the_mapping,type,
the_mapping: ( $i * $i ) > $i ).
tff(boolean_relstr,type,
boolean_relstr: $i > $o ).
tff(rel_str,type,
rel_str: $i > $o ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_27',type,
'#skF_27': $i ).
tff('#skF_40',type,
'#skF_40': ( $i * $i ) > $i ).
tff(powerset,type,
powerset: $i > $i ).
tff(cartesian_product2,type,
cartesian_product2: ( $i * $i ) > $i ).
tff(complemented_relstr,type,
complemented_relstr: $i > $o ).
tff(join_complete_relstr,type,
join_complete_relstr: $i > $o ).
tff(trivial_carrier,type,
trivial_carrier: $i > $o ).
tff(relation_of2_as_subset,type,
relation_of2_as_subset: ( $i * $i * $i ) > $o ).
tff('#skF_30',type,
'#skF_30': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(upper_bounded_relstr,type,
upper_bounded_relstr: $i > $o ).
tff(f_1347,negated_conjecture,
~ ! [A] :
( ( ~ empty_carrier(A)
& one_sorted_str(A) )
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& proper_element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )
=> ( B = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_yellow19) ).
tff(f_702,axiom,
! [A,B,C] :
( ( ~ empty_carrier(A)
& one_sorted_str(A)
& ~ empty(B)
& element(B,powerset(the_carrier(A)))
& ~ empty(C)
& filtered_subset(C,boole_POSet(B))
& upper_relstr_subset(C,boole_POSet(B))
& element(C,powerset(the_carrier(boole_POSet(B)))) )
=> ( ~ empty_carrier(net_of_bool_filter(A,B,C))
& reflexive_relstr(net_of_bool_filter(A,B,C))
& transitive_relstr(net_of_bool_filter(A,B,C))
& strict_net_str(net_of_bool_filter(A,B,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_yellow19) ).
tff(f_533,axiom,
! [A] :
( ( ~ empty_carrier(A)
& one_sorted_str(A) )
=> ~ empty(cast_as_carrier_subset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_pre_topc) ).
tff(f_990,axiom,
? [A] :
( empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_relat_1) ).
tff(f_1411,axiom,
! [A,B] :
( ( set_difference(A,singleton(B)) = A )
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
tff(f_1415,axiom,
! [A] :
( empty(A)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
tff(f_1327,axiom,
! [A] :
( ( ~ empty_carrier(A)
& one_sorted_str(A) )
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& upper_relstr_subset(B,boole_POSet(cast_as_carrier_subset(A)))
& element(B,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) )
=> ( set_difference(B,singleton(empty_set)) = filter_of_net_str(A,net_of_bool_filter(A,cast_as_carrier_subset(A),B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_yellow19) ).
tff(f_1385,axiom,
! [A] :
( ~ empty(A)
=> ! [B] :
( ( ~ empty(B)
& filtered_subset(B,boole_POSet(A))
& upper_relstr_subset(B,boole_POSet(A))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& element(B,powerset(the_carrier(boole_POSet(A)))) )
=> ! [C] :
~ ( in(C,B)
& empty(C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_yellow19) ).
tff(c_760,plain,
~ empty_carrier('#skF_38'),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_758,plain,
one_sorted_str('#skF_38'),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_756,plain,
~ empty('#skF_39'),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_754,plain,
filtered_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38'))),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_752,plain,
upper_relstr_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38'))),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_748,plain,
element('#skF_39',powerset(the_carrier(boole_POSet(cast_as_carrier_subset('#skF_38'))))),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_13430,plain,
! [A_1321,B_1322,C_1323] :
( reflexive_relstr(net_of_bool_filter(A_1321,B_1322,C_1323))
| ~ element(C_1323,powerset(the_carrier(boole_POSet(B_1322))))
| ~ upper_relstr_subset(C_1323,boole_POSet(B_1322))
| ~ filtered_subset(C_1323,boole_POSet(B_1322))
| empty(C_1323)
| ~ element(B_1322,powerset(the_carrier(A_1321)))
| empty(B_1322)
| ~ one_sorted_str(A_1321)
| empty_carrier(A_1321) ),
inference(cnfTransformation,[status(thm)],[f_702]) ).
tff(c_13587,plain,
! [A_1321] :
( reflexive_relstr(net_of_bool_filter(A_1321,cast_as_carrier_subset('#skF_38'),'#skF_39'))
| ~ upper_relstr_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| ~ filtered_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| empty('#skF_39')
| ~ element(cast_as_carrier_subset('#skF_38'),powerset(the_carrier(A_1321)))
| empty(cast_as_carrier_subset('#skF_38'))
| ~ one_sorted_str(A_1321)
| empty_carrier(A_1321) ),
inference(resolution,[status(thm)],[c_748,c_13430]) ).
tff(c_13692,plain,
! [A_1321] :
( reflexive_relstr(net_of_bool_filter(A_1321,cast_as_carrier_subset('#skF_38'),'#skF_39'))
| empty('#skF_39')
| ~ element(cast_as_carrier_subset('#skF_38'),powerset(the_carrier(A_1321)))
| empty(cast_as_carrier_subset('#skF_38'))
| ~ one_sorted_str(A_1321)
| empty_carrier(A_1321) ),
inference(demodulation,[status(thm),theory(equality)],[c_754,c_752,c_13587]) ).
tff(c_13693,plain,
! [A_1321] :
( reflexive_relstr(net_of_bool_filter(A_1321,cast_as_carrier_subset('#skF_38'),'#skF_39'))
| ~ element(cast_as_carrier_subset('#skF_38'),powerset(the_carrier(A_1321)))
| empty(cast_as_carrier_subset('#skF_38'))
| ~ one_sorted_str(A_1321)
| empty_carrier(A_1321) ),
inference(negUnitSimplification,[status(thm)],[c_756,c_13692]) ).
tff(c_13695,plain,
empty(cast_as_carrier_subset('#skF_38')),
inference(splitLeft,[status(thm)],[c_13693]) ).
tff(c_254,plain,
! [A_77] :
( ~ empty(cast_as_carrier_subset(A_77))
| ~ one_sorted_str(A_77)
| empty_carrier(A_77) ),
inference(cnfTransformation,[status(thm)],[f_533]) ).
tff(c_13705,plain,
( ~ one_sorted_str('#skF_38')
| empty_carrier('#skF_38') ),
inference(resolution,[status(thm)],[c_13695,c_254]) ).
tff(c_13722,plain,
empty_carrier('#skF_38'),
inference(demodulation,[status(thm),theory(equality)],[c_758,c_13705]) ).
tff(c_13724,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_760,c_13722]) ).
tff(c_13726,plain,
~ empty(cast_as_carrier_subset('#skF_38')),
inference(splitRight,[status(thm)],[c_13693]) ).
tff(c_750,plain,
proper_element('#skF_39',powerset(the_carrier(boole_POSet(cast_as_carrier_subset('#skF_38'))))),
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_518,plain,
empty('#skF_14'),
inference(cnfTransformation,[status(thm)],[f_990]) ).
tff(c_790,plain,
! [A_197,B_198] :
( ( set_difference(A_197,singleton(B_198)) = A_197 )
| in(B_198,A_197) ),
inference(cnfTransformation,[status(thm)],[f_1411]) ).
tff(c_869,plain,
! [A_231] :
( ( empty_set = A_231 )
| ~ empty(A_231) ),
inference(cnfTransformation,[status(thm)],[f_1415]) ).
tff(c_882,plain,
empty_set = '#skF_14',
inference(resolution,[status(thm)],[c_518,c_869]) ).
tff(c_744,plain,
! [A_169,B_171] :
( ( filter_of_net_str(A_169,net_of_bool_filter(A_169,cast_as_carrier_subset(A_169),B_171)) = set_difference(B_171,singleton(empty_set)) )
| ~ element(B_171,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A_169)))))
| ~ upper_relstr_subset(B_171,boole_POSet(cast_as_carrier_subset(A_169)))
| ~ filtered_subset(B_171,boole_POSet(cast_as_carrier_subset(A_169)))
| empty(B_171)
| ~ one_sorted_str(A_169)
| empty_carrier(A_169) ),
inference(cnfTransformation,[status(thm)],[f_1327]) ).
tff(c_15553,plain,
! [A_1368,B_1369] :
( ( filter_of_net_str(A_1368,net_of_bool_filter(A_1368,cast_as_carrier_subset(A_1368),B_1369)) = set_difference(B_1369,singleton('#skF_14')) )
| ~ element(B_1369,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A_1368)))))
| ~ upper_relstr_subset(B_1369,boole_POSet(cast_as_carrier_subset(A_1368)))
| ~ filtered_subset(B_1369,boole_POSet(cast_as_carrier_subset(A_1368)))
| empty(B_1369)
| ~ one_sorted_str(A_1368)
| empty_carrier(A_1368) ),
inference(demodulation,[status(thm),theory(equality)],[c_882,c_744]) ).
tff(c_15710,plain,
( ( filter_of_net_str('#skF_38',net_of_bool_filter('#skF_38',cast_as_carrier_subset('#skF_38'),'#skF_39')) = set_difference('#skF_39',singleton('#skF_14')) )
| ~ upper_relstr_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| ~ filtered_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| empty('#skF_39')
| ~ one_sorted_str('#skF_38')
| empty_carrier('#skF_38') ),
inference(resolution,[status(thm)],[c_748,c_15553]) ).
tff(c_15815,plain,
( ( filter_of_net_str('#skF_38',net_of_bool_filter('#skF_38',cast_as_carrier_subset('#skF_38'),'#skF_39')) = set_difference('#skF_39',singleton('#skF_14')) )
| empty('#skF_39')
| empty_carrier('#skF_38') ),
inference(demodulation,[status(thm),theory(equality)],[c_758,c_754,c_752,c_15710]) ).
tff(c_15816,plain,
filter_of_net_str('#skF_38',net_of_bool_filter('#skF_38',cast_as_carrier_subset('#skF_38'),'#skF_39')) = set_difference('#skF_39',singleton('#skF_14')),
inference(negUnitSimplification,[status(thm)],[c_760,c_756,c_15815]) ).
tff(c_746,plain,
filter_of_net_str('#skF_38',net_of_bool_filter('#skF_38',cast_as_carrier_subset('#skF_38'),'#skF_39')) != '#skF_39',
inference(cnfTransformation,[status(thm)],[f_1347]) ).
tff(c_15817,plain,
set_difference('#skF_39',singleton('#skF_14')) != '#skF_39',
inference(demodulation,[status(thm),theory(equality)],[c_15816,c_746]) ).
tff(c_15855,plain,
in('#skF_14','#skF_39'),
inference(superposition,[status(thm),theory(equality)],[c_790,c_15817]) ).
tff(c_774,plain,
! [C_186,B_184,A_180] :
( ~ empty(C_186)
| ~ in(C_186,B_184)
| ~ element(B_184,powerset(the_carrier(boole_POSet(A_180))))
| ~ proper_element(B_184,powerset(the_carrier(boole_POSet(A_180))))
| ~ upper_relstr_subset(B_184,boole_POSet(A_180))
| ~ filtered_subset(B_184,boole_POSet(A_180))
| empty(B_184)
| empty(A_180) ),
inference(cnfTransformation,[status(thm)],[f_1385]) ).
tff(c_15859,plain,
! [A_180] :
( ~ empty('#skF_14')
| ~ element('#skF_39',powerset(the_carrier(boole_POSet(A_180))))
| ~ proper_element('#skF_39',powerset(the_carrier(boole_POSet(A_180))))
| ~ upper_relstr_subset('#skF_39',boole_POSet(A_180))
| ~ filtered_subset('#skF_39',boole_POSet(A_180))
| empty('#skF_39')
| empty(A_180) ),
inference(resolution,[status(thm)],[c_15855,c_774]) ).
tff(c_15884,plain,
! [A_180] :
( ~ element('#skF_39',powerset(the_carrier(boole_POSet(A_180))))
| ~ proper_element('#skF_39',powerset(the_carrier(boole_POSet(A_180))))
| ~ upper_relstr_subset('#skF_39',boole_POSet(A_180))
| ~ filtered_subset('#skF_39',boole_POSet(A_180))
| empty('#skF_39')
| empty(A_180) ),
inference(demodulation,[status(thm),theory(equality)],[c_518,c_15859]) ).
tff(c_19406,plain,
! [A_1451] :
( ~ element('#skF_39',powerset(the_carrier(boole_POSet(A_1451))))
| ~ proper_element('#skF_39',powerset(the_carrier(boole_POSet(A_1451))))
| ~ upper_relstr_subset('#skF_39',boole_POSet(A_1451))
| ~ filtered_subset('#skF_39',boole_POSet(A_1451))
| empty(A_1451) ),
inference(negUnitSimplification,[status(thm)],[c_756,c_15884]) ).
tff(c_19409,plain,
( ~ element('#skF_39',powerset(the_carrier(boole_POSet(cast_as_carrier_subset('#skF_38')))))
| ~ upper_relstr_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| ~ filtered_subset('#skF_39',boole_POSet(cast_as_carrier_subset('#skF_38')))
| empty(cast_as_carrier_subset('#skF_38')) ),
inference(resolution,[status(thm)],[c_750,c_19406]) ).
tff(c_19412,plain,
empty(cast_as_carrier_subset('#skF_38')),
inference(demodulation,[status(thm),theory(equality)],[c_754,c_752,c_748,c_19409]) ).
tff(c_19414,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13726,c_19412]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : SEU394+1 : TPTP v9.0.0. Released v3.3.0.
% 0.07/0.15 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.15/0.35 % Computer : n020.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Tue Apr 8 23:05:34 EDT 2025
% 0.15/0.35 % CPUTime :
% 25.98/10.50 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.98/10.51
% 25.98/10.51 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------