%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU339+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 : n014.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:41 PM UTC 2025
% Result : Theorem 167.34s 135.30s
% Output : CNFRefutation 167.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 19
% Syntax : Number of formulae : 136 ( 41 unt; 0 typ; 0 def)
% Number of atoms : 374 ( 28 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 448 ( 210 ~; 204 |; 11 &)
% ( 6 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 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 : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 228 ( 225 !; 3 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ relation_of2_as_subset > relation_of2 > related > subset > is_antisymmetric_in > in > element > relation > rel_str > one_sorted_str > empty > antisymmetric_relstr > unordered_pair > ordered_pair > cartesian_product2 > #nlpp > the_carrier > the_InternalRel > singleton > powerset > empty_set > #skF_11 > #skF_8 > #skF_14 > #skF_10 > #skF_13 > #skF_3 > #skF_9 > #skF_4 > #skF_2 > #skF_7 > #skF_1 > #skF_5 > #skF_6 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(relation,type,
relation: $i > $o ).
tff(the_InternalRel,type,
the_InternalRel: $i > $i ).
tff(singleton,type,
singleton: $i > $i ).
tff(related,type,
related: ( $i * $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(unordered_pair,type,
unordered_pair: ( $i * $i ) > $i ).
tff(the_carrier,type,
the_carrier: $i > $i ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(ordered_pair,type,
ordered_pair: ( $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(antisymmetric_relstr,type,
antisymmetric_relstr: $i > $o ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': $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('#skF_13',type,
'#skF_13': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff(empty,type,
empty: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(empty_set,type,
empty_set: $i ).
tff(relation_of2,type,
relation_of2: ( $i * $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(rel_str,type,
rel_str: $i > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(powerset,type,
powerset: $i > $i ).
tff(is_antisymmetric_in,type,
is_antisymmetric_in: ( $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff(cartesian_product2,type,
cartesian_product2: ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(relation_of2_as_subset,type,
relation_of2_as_subset: ( $i * $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_170,negated_conjecture,
~ ! [A] :
( ( antisymmetric_relstr(A)
& rel_str(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( related(A,B,C)
& related(A,C,B) )
=> ( B = C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
tff(f_73,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
tff(f_153,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
tff(f_86,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
tff(f_82,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
tff(f_35,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
tff(f_202,axiom,
! [A,B] :
~ ( in(A,B)
& empty(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
tff(f_61,axiom,
! [A] :
( rel_str(A)
=> ( antisymmetric_relstr(A)
<=> is_antisymmetric_in(the_InternalRel(A),the_carrier(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_orders_2) ).
tff(f_96,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
tff(f_129,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
tff(f_141,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
tff(f_176,axiom,
! [A,B] :
( element(A,B)
=> ( empty(B)
| in(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
tff(f_186,axiom,
! [A,B,C] :
( ( in(A,B)
& element(B,powerset(C)) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
tff(f_197,axiom,
! [A] :
( empty(A)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
tff(f_134,axiom,
! [A] :
? [B] :
( element(B,powerset(A))
& empty(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
tff(f_193,axiom,
! [A,B,C] :
~ ( in(A,B)
& element(B,powerset(C))
& empty(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
tff(f_149,axiom,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(A,C)
& in(B,D) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
tff(f_180,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
tff(f_53,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( ( in(C,B)
& in(D,B)
& in(ordered_pair(C,D),A)
& in(ordered_pair(D,C),A) )
=> ( C = D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_2) ).
tff(c_102,plain,
'#skF_14' != '#skF_13',
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_104,plain,
related('#skF_12','#skF_14','#skF_13'),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_106,plain,
related('#skF_12','#skF_13','#skF_14'),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_110,plain,
element('#skF_13',the_carrier('#skF_12')),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_112,plain,
rel_str('#skF_12'),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_108,plain,
element('#skF_14',the_carrier('#skF_12')),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_1110,plain,
! [B_269,C_270,A_271] :
( in(ordered_pair(B_269,C_270),the_InternalRel(A_271))
| ~ related(A_271,B_269,C_270)
| ~ element(C_270,the_carrier(A_271))
| ~ element(B_269,the_carrier(A_271))
| ~ rel_str(A_271) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_100,plain,
! [A_67,B_68] :
( element(A_67,B_68)
| ~ in(A_67,B_68) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_1136,plain,
! [B_269,C_270,A_271] :
( element(ordered_pair(B_269,C_270),the_InternalRel(A_271))
| ~ related(A_271,B_269,C_270)
| ~ element(C_270,the_carrier(A_271))
| ~ element(B_269,the_carrier(A_271))
| ~ rel_str(A_271) ),
inference(resolution,[status(thm)],[c_1110,c_100]) ).
tff(c_52,plain,
! [A_39] :
( relation_of2_as_subset(the_InternalRel(A_39),the_carrier(A_39),the_carrier(A_39))
| ~ rel_str(A_39) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_535,plain,
! [C_174,A_175,B_176] :
( element(C_174,powerset(cartesian_product2(A_175,B_176)))
| ~ relation_of2_as_subset(C_174,A_175,B_176) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_4,plain,
! [C_5,A_3,B_4] :
( relation(C_5)
| ~ element(C_5,powerset(cartesian_product2(A_3,B_4))) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_547,plain,
! [C_177,A_178,B_179] :
( relation(C_177)
| ~ relation_of2_as_subset(C_177,A_178,B_179) ),
inference(resolution,[status(thm)],[c_535,c_4]) ).
tff(c_557,plain,
! [A_39] :
( relation(the_InternalRel(A_39))
| ~ rel_str(A_39) ),
inference(resolution,[status(thm)],[c_52,c_547]) ).
tff(c_128,plain,
! [B_85,A_84] :
( ~ empty(B_85)
| ~ in(A_84,B_85) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_129136,plain,
! [A_4197,B_4198,C_4199] :
( ~ empty(the_InternalRel(A_4197))
| ~ related(A_4197,B_4198,C_4199)
| ~ element(C_4199,the_carrier(A_4197))
| ~ element(B_4198,the_carrier(A_4197))
| ~ rel_str(A_4197) ),
inference(resolution,[status(thm)],[c_1110,c_128]) ).
tff(c_129138,plain,
( ~ empty(the_InternalRel('#skF_12'))
| ~ element('#skF_14',the_carrier('#skF_12'))
| ~ element('#skF_13',the_carrier('#skF_12'))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_106,c_129136]) ).
tff(c_129143,plain,
~ empty(the_InternalRel('#skF_12')),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_110,c_108,c_129138]) ).
tff(c_114,plain,
antisymmetric_relstr('#skF_12'),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_24,plain,
! [A_27] :
( is_antisymmetric_in(the_InternalRel(A_27),the_carrier(A_27))
| ~ antisymmetric_relstr(A_27)
| ~ rel_str(A_27) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_62,plain,
! [A_43] : element('#skF_6'(A_43),A_43),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_80,plain,
empty('#skF_9'),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_90,plain,
! [C_60,A_58,B_59] :
( relation_of2_as_subset(C_60,A_58,B_59)
| ~ relation_of2(C_60,A_58,B_59) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_116,plain,
! [A_73,B_74] :
( in(A_73,B_74)
| empty(B_74)
| ~ element(A_73,B_74) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_50,plain,
! [C_38,A_36,B_37] :
( element(C_38,powerset(cartesian_product2(A_36,B_37)))
| ~ relation_of2_as_subset(C_38,A_36,B_37) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_682,plain,
! [A_206,C_207,B_208] :
( element(A_206,C_207)
| ~ element(B_208,powerset(C_207))
| ~ in(A_206,B_208) ),
inference(cnfTransformation,[status(thm)],[f_186]) ).
tff(c_1225,plain,
! [A_287,A_288,B_289,C_290] :
( element(A_287,cartesian_product2(A_288,B_289))
| ~ in(A_287,C_290)
| ~ relation_of2_as_subset(C_290,A_288,B_289) ),
inference(resolution,[status(thm)],[c_50,c_682]) ).
tff(c_129673,plain,
! [A_4216,A_4217,B_4218,B_4219] :
( element(A_4216,cartesian_product2(A_4217,B_4218))
| ~ relation_of2_as_subset(B_4219,A_4217,B_4218)
| empty(B_4219)
| ~ element(A_4216,B_4219) ),
inference(resolution,[status(thm)],[c_116,c_1225]) ).
tff(c_130348,plain,
! [A_4243,A_4244,B_4245,C_4246] :
( element(A_4243,cartesian_product2(A_4244,B_4245))
| empty(C_4246)
| ~ element(A_4243,C_4246)
| ~ relation_of2(C_4246,A_4244,B_4245) ),
inference(resolution,[status(thm)],[c_90,c_129673]) ).
tff(c_130438,plain,
! [A_4244,B_4245] :
( element('#skF_13',cartesian_product2(A_4244,B_4245))
| empty(the_carrier('#skF_12'))
| ~ relation_of2(the_carrier('#skF_12'),A_4244,B_4245) ),
inference(resolution,[status(thm)],[c_110,c_130348]) ).
tff(c_130441,plain,
empty(the_carrier('#skF_12')),
inference(splitLeft,[status(thm)],[c_130438]) ).
tff(c_135,plain,
! [A_92] :
( ( empty_set = A_92 )
| ~ empty(A_92) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_146,plain,
empty_set = '#skF_9',
inference(resolution,[status(thm)],[c_80,c_135]) ).
tff(c_126,plain,
! [A_83] :
( ( empty_set = A_83 )
| ~ empty(A_83) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_149,plain,
! [A_83] :
( ( A_83 = '#skF_9' )
| ~ empty(A_83) ),
inference(demodulation,[status(thm),theory(equality)],[c_146,c_126]) ).
tff(c_130457,plain,
the_carrier('#skF_12') = '#skF_9',
inference(resolution,[status(thm)],[c_130441,c_149]) ).
tff(c_130488,plain,
( relation_of2_as_subset(the_InternalRel('#skF_12'),the_carrier('#skF_12'),'#skF_9')
| ~ rel_str('#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_130457,c_52]) ).
tff(c_130506,plain,
relation_of2_as_subset(the_InternalRel('#skF_12'),'#skF_9','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_130457,c_130488]) ).
tff(c_130461,plain,
element('#skF_13','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_130457,c_110]) ).
tff(c_130462,plain,
element('#skF_14','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_130457,c_108]) ).
tff(c_82,plain,
! [A_56] : empty('#skF_10'(A_56)),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_145,plain,
! [A_56] : ( '#skF_10'(A_56) = empty_set ),
inference(resolution,[status(thm)],[c_82,c_135]) ).
tff(c_157,plain,
! [A_56] : ( '#skF_10'(A_56) = '#skF_9' ),
inference(demodulation,[status(thm),theory(equality)],[c_146,c_145]) ).
tff(c_84,plain,
! [A_56] : element('#skF_10'(A_56),powerset(A_56)),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_185,plain,
! [A_56] : element('#skF_9',powerset(A_56)),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_84]) ).
tff(c_335,plain,
! [C_148,B_149,A_150] :
( ~ empty(C_148)
| ~ element(B_149,powerset(C_148))
| ~ in(A_150,B_149) ),
inference(cnfTransformation,[status(thm)],[f_193]) ).
tff(c_347,plain,
! [A_56,A_150] :
( ~ empty(A_56)
| ~ in(A_150,'#skF_9') ),
inference(resolution,[status(thm)],[c_185,c_335]) ).
tff(c_349,plain,
! [A_150] : ~ in(A_150,'#skF_9'),
inference(splitLeft,[status(thm)],[c_347]) ).
tff(c_1246,plain,
! [A_73,A_288,B_289,B_74] :
( element(A_73,cartesian_product2(A_288,B_289))
| ~ relation_of2_as_subset(B_74,A_288,B_289)
| empty(B_74)
| ~ element(A_73,B_74) ),
inference(resolution,[status(thm)],[c_116,c_1225]) ).
tff(c_130554,plain,
! [A_73] :
( element(A_73,cartesian_product2('#skF_9','#skF_9'))
| empty(the_InternalRel('#skF_12'))
| ~ element(A_73,the_InternalRel('#skF_12')) ),
inference(resolution,[status(thm)],[c_130506,c_1246]) ).
tff(c_130602,plain,
! [A_4257] :
( element(A_4257,cartesian_product2('#skF_9','#skF_9'))
| ~ element(A_4257,the_InternalRel('#skF_12')) ),
inference(negUnitSimplification,[status(thm)],[c_129143,c_130554]) ).
tff(c_573,plain,
! [A_188,C_189,B_190,D_191] :
( in(A_188,C_189)
| ~ in(ordered_pair(A_188,B_190),cartesian_product2(C_189,D_191)) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_577,plain,
! [A_188,C_189,D_191,B_190] :
( in(A_188,C_189)
| empty(cartesian_product2(C_189,D_191))
| ~ element(ordered_pair(A_188,B_190),cartesian_product2(C_189,D_191)) ),
inference(resolution,[status(thm)],[c_116,c_573]) ).
tff(c_130608,plain,
! [A_188,B_190] :
( in(A_188,'#skF_9')
| empty(cartesian_product2('#skF_9','#skF_9'))
| ~ element(ordered_pair(A_188,B_190),the_InternalRel('#skF_12')) ),
inference(resolution,[status(thm)],[c_130602,c_577]) ).
tff(c_130626,plain,
! [A_188,B_190] :
( empty(cartesian_product2('#skF_9','#skF_9'))
| ~ element(ordered_pair(A_188,B_190),the_InternalRel('#skF_12')) ),
inference(negUnitSimplification,[status(thm)],[c_349,c_130608]) ).
tff(c_130636,plain,
! [A_4259,B_4260] : ~ element(ordered_pair(A_4259,B_4260),the_InternalRel('#skF_12')),
inference(splitLeft,[status(thm)],[c_130626]) ).
tff(c_130640,plain,
! [B_269,C_270] :
( ~ related('#skF_12',B_269,C_270)
| ~ element(C_270,the_carrier('#skF_12'))
| ~ element(B_269,the_carrier('#skF_12'))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_1136,c_130636]) ).
tff(c_130680,plain,
! [B_4264,C_4265] :
( ~ related('#skF_12',B_4264,C_4265)
| ~ element(C_4265,'#skF_9')
| ~ element(B_4264,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_130457,c_130457,c_130640]) ).
tff(c_130687,plain,
( ~ element('#skF_14','#skF_9')
| ~ element('#skF_13','#skF_9') ),
inference(resolution,[status(thm)],[c_106,c_130680]) ).
tff(c_130697,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_130461,c_130462,c_130687]) ).
tff(c_130698,plain,
empty(cartesian_product2('#skF_9','#skF_9')),
inference(splitRight,[status(thm)],[c_130626]) ).
tff(c_130734,plain,
cartesian_product2('#skF_9','#skF_9') = '#skF_9',
inference(resolution,[status(thm)],[c_130698,c_149]) ).
tff(c_118,plain,
! [A_75,B_76] :
( subset(A_75,B_76)
| ~ element(A_75,powerset(B_76)) ),
inference(cnfTransformation,[status(thm)],[f_180]) ).
tff(c_546,plain,
! [C_174,A_175,B_176] :
( subset(C_174,cartesian_product2(A_175,B_176))
| ~ relation_of2_as_subset(C_174,A_175,B_176) ),
inference(resolution,[status(thm)],[c_535,c_118]) ).
tff(c_131264,plain,
! [C_4274] :
( subset(C_4274,'#skF_9')
| ~ relation_of2_as_subset(C_4274,'#skF_9','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_130734,c_546]) ).
tff(c_131276,plain,
subset(the_InternalRel('#skF_12'),'#skF_9'),
inference(resolution,[status(thm)],[c_130506,c_131264]) ).
tff(c_120,plain,
! [A_75,B_76] :
( element(A_75,powerset(B_76))
| ~ subset(A_75,B_76) ),
inference(cnfTransformation,[status(thm)],[f_180]) ).
tff(c_364,plain,
! [B_155,A_156,A_157] :
( ~ empty(B_155)
| ~ in(A_156,A_157)
| ~ subset(A_157,B_155) ),
inference(resolution,[status(thm)],[c_120,c_335]) ).
tff(c_367,plain,
! [B_155,B_74,A_73] :
( ~ empty(B_155)
| ~ subset(B_74,B_155)
| empty(B_74)
| ~ element(A_73,B_74) ),
inference(resolution,[status(thm)],[c_116,c_364]) ).
tff(c_131293,plain,
! [A_73] :
( ~ empty('#skF_9')
| empty(the_InternalRel('#skF_12'))
| ~ element(A_73,the_InternalRel('#skF_12')) ),
inference(resolution,[status(thm)],[c_131276,c_367]) ).
tff(c_131312,plain,
! [A_73] :
( empty(the_InternalRel('#skF_12'))
| ~ element(A_73,the_InternalRel('#skF_12')) ),
inference(demodulation,[status(thm),theory(equality)],[c_80,c_131293]) ).
tff(c_131341,plain,
! [A_4279] : ~ element(A_4279,the_InternalRel('#skF_12')),
inference(negUnitSimplification,[status(thm)],[c_129143,c_131312]) ).
tff(c_131443,plain,
$false,
inference(resolution,[status(thm)],[c_62,c_131341]) ).
tff(c_131445,plain,
~ empty(the_carrier('#skF_12')),
inference(splitRight,[status(thm)],[c_130438]) ).
tff(c_345,plain,
! [B_76,A_150,A_75] :
( ~ empty(B_76)
| ~ in(A_150,A_75)
| ~ subset(A_75,B_76) ),
inference(resolution,[status(thm)],[c_120,c_335]) ).
tff(c_137774,plain,
! [B_4746,A_4747,B_4748,C_4749] :
( ~ empty(B_4746)
| ~ subset(the_InternalRel(A_4747),B_4746)
| ~ related(A_4747,B_4748,C_4749)
| ~ element(C_4749,the_carrier(A_4747))
| ~ element(B_4748,the_carrier(A_4747))
| ~ rel_str(A_4747) ),
inference(resolution,[status(thm)],[c_1110,c_345]) ).
tff(c_413750,plain,
! [A_11043,B_11042,C_11040,A_11041,B_11044] :
( ~ empty(cartesian_product2(A_11041,B_11042))
| ~ related(A_11043,B_11044,C_11040)
| ~ element(C_11040,the_carrier(A_11043))
| ~ element(B_11044,the_carrier(A_11043))
| ~ rel_str(A_11043)
| ~ relation_of2_as_subset(the_InternalRel(A_11043),A_11041,B_11042) ),
inference(resolution,[status(thm)],[c_546,c_137774]) ).
tff(c_413756,plain,
! [A_11041,B_11042] :
( ~ empty(cartesian_product2(A_11041,B_11042))
| ~ element('#skF_14',the_carrier('#skF_12'))
| ~ element('#skF_13',the_carrier('#skF_12'))
| ~ rel_str('#skF_12')
| ~ relation_of2_as_subset(the_InternalRel('#skF_12'),A_11041,B_11042) ),
inference(resolution,[status(thm)],[c_106,c_413750]) ).
tff(c_413767,plain,
! [A_11045,B_11046] :
( ~ empty(cartesian_product2(A_11045,B_11046))
| ~ relation_of2_as_subset(the_InternalRel('#skF_12'),A_11045,B_11046) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_110,c_108,c_413756]) ).
tff(c_413771,plain,
( ~ empty(cartesian_product2(the_carrier('#skF_12'),the_carrier('#skF_12')))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_52,c_413767]) ).
tff(c_413778,plain,
~ empty(cartesian_product2(the_carrier('#skF_12'),the_carrier('#skF_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_413771]) ).
tff(c_330,plain,
! [A_147] :
( relation_of2_as_subset(the_InternalRel(A_147),the_carrier(A_147),the_carrier(A_147))
| ~ rel_str(A_147) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_88,plain,
! [C_60,A_58,B_59] :
( relation_of2(C_60,A_58,B_59)
| ~ relation_of2_as_subset(C_60,A_58,B_59) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_334,plain,
! [A_147] :
( relation_of2(the_InternalRel(A_147),the_carrier(A_147),the_carrier(A_147))
| ~ rel_str(A_147) ),
inference(resolution,[status(thm)],[c_330,c_88]) ).
tff(c_28,plain,
! [B_32,C_34,A_28] :
( in(ordered_pair(B_32,C_34),the_InternalRel(A_28))
| ~ related(A_28,B_32,C_34)
| ~ element(C_34,the_carrier(A_28))
| ~ element(B_32,the_carrier(A_28))
| ~ rel_str(A_28) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_143800,plain,
! [A_5013,C_5011,A_5012,B_5010,B_5014] :
( element(ordered_pair(B_5010,C_5011),cartesian_product2(A_5013,B_5014))
| ~ relation_of2_as_subset(the_InternalRel(A_5012),A_5013,B_5014)
| ~ related(A_5012,B_5010,C_5011)
| ~ element(C_5011,the_carrier(A_5012))
| ~ element(B_5010,the_carrier(A_5012))
| ~ rel_str(A_5012) ),
inference(resolution,[status(thm)],[c_28,c_1225]) ).
tff(c_490337,plain,
! [A_11928,A_11927,C_11929,B_11925,B_11926] :
( element(ordered_pair(B_11926,C_11929),cartesian_product2(A_11928,B_11925))
| ~ related(A_11927,B_11926,C_11929)
| ~ element(C_11929,the_carrier(A_11927))
| ~ element(B_11926,the_carrier(A_11927))
| ~ rel_str(A_11927)
| ~ relation_of2(the_InternalRel(A_11927),A_11928,B_11925) ),
inference(resolution,[status(thm)],[c_90,c_143800]) ).
tff(c_490343,plain,
! [A_11928,B_11925] :
( element(ordered_pair('#skF_13','#skF_14'),cartesian_product2(A_11928,B_11925))
| ~ element('#skF_14',the_carrier('#skF_12'))
| ~ element('#skF_13',the_carrier('#skF_12'))
| ~ rel_str('#skF_12')
| ~ relation_of2(the_InternalRel('#skF_12'),A_11928,B_11925) ),
inference(resolution,[status(thm)],[c_106,c_490337]) ).
tff(c_490354,plain,
! [A_11930,B_11931] :
( element(ordered_pair('#skF_13','#skF_14'),cartesian_product2(A_11930,B_11931))
| ~ relation_of2(the_InternalRel('#skF_12'),A_11930,B_11931) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_110,c_108,c_490343]) ).
tff(c_585,plain,
! [B_195,D_196,A_197,C_198] :
( in(B_195,D_196)
| ~ in(ordered_pair(A_197,B_195),cartesian_product2(C_198,D_196)) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_589,plain,
! [B_195,D_196,C_198,A_197] :
( in(B_195,D_196)
| empty(cartesian_product2(C_198,D_196))
| ~ element(ordered_pair(A_197,B_195),cartesian_product2(C_198,D_196)) ),
inference(resolution,[status(thm)],[c_116,c_585]) ).
tff(c_490421,plain,
! [B_11936,A_11937] :
( in('#skF_14',B_11936)
| empty(cartesian_product2(A_11937,B_11936))
| ~ relation_of2(the_InternalRel('#skF_12'),A_11937,B_11936) ),
inference(resolution,[status(thm)],[c_490354,c_589]) ).
tff(c_490425,plain,
( in('#skF_14',the_carrier('#skF_12'))
| empty(cartesian_product2(the_carrier('#skF_12'),the_carrier('#skF_12')))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_334,c_490421]) ).
tff(c_490428,plain,
( in('#skF_14',the_carrier('#skF_12'))
| empty(cartesian_product2(the_carrier('#skF_12'),the_carrier('#skF_12'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_490425]) ).
tff(c_490429,plain,
in('#skF_14',the_carrier('#skF_12')),
inference(negUnitSimplification,[status(thm)],[c_413778,c_490428]) ).
tff(c_1140,plain,
! [D_277,C_278,A_279,B_280] :
( ( D_277 = C_278 )
| ~ in(ordered_pair(D_277,C_278),A_279)
| ~ in(ordered_pair(C_278,D_277),A_279)
| ~ in(D_277,B_280)
| ~ in(C_278,B_280)
| ~ is_antisymmetric_in(A_279,B_280)
| ~ relation(A_279) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_131911,plain,
! [D_4318,C_4319,B_4320,B_4321] :
( ( D_4318 = C_4319 )
| ~ in(ordered_pair(C_4319,D_4318),B_4320)
| ~ in(D_4318,B_4321)
| ~ in(C_4319,B_4321)
| ~ is_antisymmetric_in(B_4320,B_4321)
| ~ relation(B_4320)
| empty(B_4320)
| ~ element(ordered_pair(D_4318,C_4319),B_4320) ),
inference(resolution,[status(thm)],[c_116,c_1140]) ).
tff(c_142960,plain,
! [D_4950,C_4951,B_4952,B_4953] :
( ( D_4950 = C_4951 )
| ~ in(D_4950,B_4952)
| ~ in(C_4951,B_4952)
| ~ is_antisymmetric_in(B_4953,B_4952)
| ~ relation(B_4953)
| ~ element(ordered_pair(D_4950,C_4951),B_4953)
| empty(B_4953)
| ~ element(ordered_pair(C_4951,D_4950),B_4953) ),
inference(resolution,[status(thm)],[c_116,c_131911]) ).
tff(c_505183,plain,
! [C_12123,A_12124,B_12125,B_12126] :
( ( C_12123 = A_12124 )
| ~ in(C_12123,B_12125)
| ~ is_antisymmetric_in(B_12126,B_12125)
| ~ relation(B_12126)
| ~ element(ordered_pair(A_12124,C_12123),B_12126)
| empty(B_12126)
| ~ element(ordered_pair(C_12123,A_12124),B_12126)
| empty(B_12125)
| ~ element(A_12124,B_12125) ),
inference(resolution,[status(thm)],[c_116,c_142960]) ).
tff(c_505185,plain,
! [A_12124,B_12126] :
( ( A_12124 = '#skF_14' )
| ~ is_antisymmetric_in(B_12126,the_carrier('#skF_12'))
| ~ relation(B_12126)
| ~ element(ordered_pair(A_12124,'#skF_14'),B_12126)
| empty(B_12126)
| ~ element(ordered_pair('#skF_14',A_12124),B_12126)
| empty(the_carrier('#skF_12'))
| ~ element(A_12124,the_carrier('#skF_12')) ),
inference(resolution,[status(thm)],[c_490429,c_505183]) ).
tff(c_505323,plain,
! [A_12127,B_12128] :
( ( A_12127 = '#skF_14' )
| ~ is_antisymmetric_in(B_12128,the_carrier('#skF_12'))
| ~ relation(B_12128)
| ~ element(ordered_pair(A_12127,'#skF_14'),B_12128)
| empty(B_12128)
| ~ element(ordered_pair('#skF_14',A_12127),B_12128)
| ~ element(A_12127,the_carrier('#skF_12')) ),
inference(negUnitSimplification,[status(thm)],[c_131445,c_505185]) ).
tff(c_505683,plain,
! [A_12127] :
( ( A_12127 = '#skF_14' )
| ~ relation(the_InternalRel('#skF_12'))
| ~ element(ordered_pair(A_12127,'#skF_14'),the_InternalRel('#skF_12'))
| empty(the_InternalRel('#skF_12'))
| ~ element(ordered_pair('#skF_14',A_12127),the_InternalRel('#skF_12'))
| ~ element(A_12127,the_carrier('#skF_12'))
| ~ antisymmetric_relstr('#skF_12')
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_24,c_505323]) ).
tff(c_506009,plain,
! [A_12127] :
( ( A_12127 = '#skF_14' )
| ~ relation(the_InternalRel('#skF_12'))
| ~ element(ordered_pair(A_12127,'#skF_14'),the_InternalRel('#skF_12'))
| empty(the_InternalRel('#skF_12'))
| ~ element(ordered_pair('#skF_14',A_12127),the_InternalRel('#skF_12'))
| ~ element(A_12127,the_carrier('#skF_12')) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_114,c_505683]) ).
tff(c_506010,plain,
! [A_12127] :
( ( A_12127 = '#skF_14' )
| ~ relation(the_InternalRel('#skF_12'))
| ~ element(ordered_pair(A_12127,'#skF_14'),the_InternalRel('#skF_12'))
| ~ element(ordered_pair('#skF_14',A_12127),the_InternalRel('#skF_12'))
| ~ element(A_12127,the_carrier('#skF_12')) ),
inference(negUnitSimplification,[status(thm)],[c_129143,c_506009]) ).
tff(c_506012,plain,
~ relation(the_InternalRel('#skF_12')),
inference(splitLeft,[status(thm)],[c_506010]) ).
tff(c_506015,plain,
~ rel_str('#skF_12'),
inference(resolution,[status(thm)],[c_557,c_506012]) ).
tff(c_506019,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_112,c_506015]) ).
tff(c_506022,plain,
! [A_12129] :
( ( A_12129 = '#skF_14' )
| ~ element(ordered_pair(A_12129,'#skF_14'),the_InternalRel('#skF_12'))
| ~ element(ordered_pair('#skF_14',A_12129),the_InternalRel('#skF_12'))
| ~ element(A_12129,the_carrier('#skF_12')) ),
inference(splitRight,[status(thm)],[c_506010]) ).
tff(c_506025,plain,
! [B_269] :
( ( B_269 = '#skF_14' )
| ~ element(ordered_pair('#skF_14',B_269),the_InternalRel('#skF_12'))
| ~ related('#skF_12',B_269,'#skF_14')
| ~ element('#skF_14',the_carrier('#skF_12'))
| ~ element(B_269,the_carrier('#skF_12'))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_1136,c_506022]) ).
tff(c_506029,plain,
! [B_12130] :
( ( B_12130 = '#skF_14' )
| ~ element(ordered_pair('#skF_14',B_12130),the_InternalRel('#skF_12'))
| ~ related('#skF_12',B_12130,'#skF_14')
| ~ element(B_12130,the_carrier('#skF_12')) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_108,c_506025]) ).
tff(c_506033,plain,
! [C_270] :
( ( C_270 = '#skF_14' )
| ~ related('#skF_12',C_270,'#skF_14')
| ~ related('#skF_12','#skF_14',C_270)
| ~ element(C_270,the_carrier('#skF_12'))
| ~ element('#skF_14',the_carrier('#skF_12'))
| ~ rel_str('#skF_12') ),
inference(resolution,[status(thm)],[c_1136,c_506029]) ).
tff(c_506038,plain,
! [C_12131] :
( ( C_12131 = '#skF_14' )
| ~ related('#skF_12',C_12131,'#skF_14')
| ~ related('#skF_12','#skF_14',C_12131)
| ~ element(C_12131,the_carrier('#skF_12')) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_108,c_506033]) ).
tff(c_506477,plain,
( ( '#skF_14' = '#skF_13' )
| ~ related('#skF_12','#skF_13','#skF_14')
| ~ related('#skF_12','#skF_14','#skF_13') ),
inference(resolution,[status(thm)],[c_110,c_506038]) ).
tff(c_506634,plain,
'#skF_14' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_104,c_106,c_506477]) ).
tff(c_506636,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_102,c_506634]) ).
tff(c_506637,plain,
! [A_56] : ~ empty(A_56),
inference(splitRight,[status(thm)],[c_347]) ).
tff(c_506645,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_506637,c_80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU339+1 : TPTP v9.0.0. Released v3.3.0.
% 0.06/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 : n014.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 22:52:34 EDT 2025
% 0.13/0.35 % CPUTime :
% 167.34/135.30 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 167.34/135.32
% 167.34/135.32 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------