%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU146+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 : n005.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:52:55 PM UTC 2025
% Result : Theorem 3.72s 2.06s
% Output : CNFRefutation 4.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 78 ( 43 unt; 0 typ; 0 def)
% Number of atoms : 131 ( 56 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 97 ( 44 ~; 46 |; 1 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 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 : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 51 ( 51 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > in > empty > set_difference > #nlpp > singleton > empty_set > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(set_difference,type,
set_difference: ( $i * $i ) > $i ).
tff(singleton,type,
singleton: $i > $i ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(empty,type,
empty: $i > $o ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(f_63,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
tff(f_69,axiom,
! [A,B] :
( ( set_difference(A,B) = empty_set )
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_xboole_1) ).
tff(f_43,axiom,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_zfmisc_1) ).
tff(f_56,negated_conjecture,
~ ! [A,B] :
( subset(A,singleton(B))
<=> ( ( A = empty_set )
| ( A = singleton(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l4_zfmisc_1) ).
tff(f_37,axiom,
! [A,B] :
( ( A = B )
<=> ( subset(A,B)
& subset(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
tff(f_65,axiom,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_xboole_1) ).
tff(f_49,axiom,
! [A,B,C] :
( subset(A,B)
=> ( in(C,A)
| subset(A,set_difference(B,singleton(C))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l3_zfmisc_1) ).
tff(f_73,axiom,
! [A] :
( subset(A,empty_set)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_1) ).
tff(c_40,plain,
! [A_10] : subset(A_10,A_10),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_91,plain,
! [A_28,B_29] :
( ( set_difference(A_28,B_29) = empty_set )
| ~ subset(A_28,B_29) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_103,plain,
! [A_10] : ( set_difference(A_10,A_10) = empty_set ),
inference(resolution,[status(thm)],[c_40,c_91]) ).
tff(c_20,plain,
! [A_5,B_6] :
( subset(singleton(A_5),B_6)
| ~ in(A_5,B_6) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_24,plain,
( ~ subset('#skF_1',singleton('#skF_2'))
| ( singleton('#skF_4') != '#skF_3' ) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_138,plain,
singleton('#skF_4') != '#skF_3',
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_34,plain,
( ( singleton('#skF_2') = '#skF_1' )
| ( empty_set = '#skF_1' )
| subset('#skF_3',singleton('#skF_4')) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_214,plain,
subset('#skF_3',singleton('#skF_4')),
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_4,plain,
! [B_4,A_3] :
( ( B_4 = A_3 )
| ~ subset(B_4,A_3)
| ~ subset(A_3,B_4) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_216,plain,
( ( singleton('#skF_4') = '#skF_3' )
| ~ subset(singleton('#skF_4'),'#skF_3') ),
inference(resolution,[status(thm)],[c_214,c_4]) ).
tff(c_222,plain,
~ subset(singleton('#skF_4'),'#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_138,c_216]) ).
tff(c_230,plain,
~ in('#skF_4','#skF_3'),
inference(resolution,[status(thm)],[c_20,c_222]) ).
tff(c_28,plain,
( ~ subset('#skF_1',singleton('#skF_2'))
| ( empty_set != '#skF_3' ) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_66,plain,
empty_set != '#skF_3',
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_42,plain,
! [A_12] : subset(empty_set,A_12),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_102,plain,
! [A_12] : ( set_difference(empty_set,A_12) = empty_set ),
inference(resolution,[status(thm)],[c_42,c_91]) ).
tff(c_46,plain,
! [A_13,B_14] :
( ( set_difference(A_13,B_14) = empty_set )
| ~ subset(A_13,B_14) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_223,plain,
set_difference('#skF_3',singleton('#skF_4')) = empty_set,
inference(resolution,[status(thm)],[c_214,c_46]) ).
tff(c_240,plain,
! [A_41,B_42,C_43] :
( subset(A_41,set_difference(B_42,singleton(C_43)))
| in(C_43,A_41)
| ~ subset(A_41,B_42) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_297,plain,
! [A_46] :
( subset(A_46,empty_set)
| in('#skF_4',A_46)
| ~ subset(A_46,'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_223,c_240]) ).
tff(c_44,plain,
! [A_13,B_14] :
( subset(A_13,B_14)
| ( set_difference(A_13,B_14) != empty_set ) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_159,plain,
! [B_35,A_36] :
( ( B_35 = A_36 )
| ~ subset(B_35,A_36)
| ~ subset(A_36,B_35) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_169,plain,
! [B_14,A_13] :
( ( B_14 = A_13 )
| ~ subset(B_14,A_13)
| ( set_difference(A_13,B_14) != empty_set ) ),
inference(resolution,[status(thm)],[c_44,c_159]) ).
tff(c_300,plain,
! [A_46] :
( ( empty_set = A_46 )
| ( set_difference(empty_set,A_46) != empty_set )
| in('#skF_4',A_46)
| ~ subset(A_46,'#skF_3') ),
inference(resolution,[status(thm)],[c_297,c_169]) ).
tff(c_322,plain,
! [A_47] :
( ( empty_set = A_47 )
| in('#skF_4',A_47)
| ~ subset(A_47,'#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_300]) ).
tff(c_338,plain,
( ( empty_set = '#skF_3' )
| in('#skF_4','#skF_3') ),
inference(resolution,[status(thm)],[c_40,c_322]) ).
tff(c_346,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_230,c_66,c_338]) ).
tff(c_347,plain,
( ( empty_set = '#skF_1' )
| ( singleton('#skF_2') = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_353,plain,
singleton('#skF_2') = '#skF_1',
inference(splitLeft,[status(thm)],[c_347]) ).
tff(c_32,plain,
( ~ subset('#skF_1',singleton('#skF_2'))
| subset('#skF_3',singleton('#skF_4')) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_139,plain,
~ subset('#skF_1',singleton('#skF_2')),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_143,plain,
set_difference('#skF_1',singleton('#skF_2')) != empty_set,
inference(resolution,[status(thm)],[c_44,c_139]) ).
tff(c_354,plain,
set_difference('#skF_1','#skF_1') != empty_set,
inference(demodulation,[status(thm),theory(equality)],[c_353,c_143]) ).
tff(c_358,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_103,c_354]) ).
tff(c_359,plain,
empty_set = '#skF_1',
inference(splitRight,[status(thm)],[c_347]) ).
tff(c_372,plain,
! [A_12] : subset('#skF_1',A_12),
inference(demodulation,[status(thm),theory(equality)],[c_359,c_42]) ).
tff(c_380,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_372,c_139]) ).
tff(c_381,plain,
subset('#skF_3',singleton('#skF_4')),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_414,plain,
! [B_51,A_52] :
( ( B_51 = A_52 )
| ~ subset(B_51,A_52)
| ~ subset(A_52,B_51) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_420,plain,
( ( singleton('#skF_4') = '#skF_3' )
| ~ subset(singleton('#skF_4'),'#skF_3') ),
inference(resolution,[status(thm)],[c_381,c_414]) ).
tff(c_431,plain,
~ subset(singleton('#skF_4'),'#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_138,c_420]) ).
tff(c_444,plain,
~ in('#skF_4','#skF_3'),
inference(resolution,[status(thm)],[c_20,c_431]) ).
tff(c_386,plain,
set_difference('#skF_3',singleton('#skF_4')) = empty_set,
inference(resolution,[status(thm)],[c_381,c_46]) ).
tff(c_463,plain,
! [A_55,B_56,C_57] :
( subset(A_55,set_difference(B_56,singleton(C_57)))
| in(C_57,A_55)
| ~ subset(A_55,B_56) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_567,plain,
! [A_62] :
( subset(A_62,empty_set)
| in('#skF_4',A_62)
| ~ subset(A_62,'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_386,c_463]) ).
tff(c_48,plain,
! [A_15] :
( ( empty_set = A_15 )
| ~ subset(A_15,empty_set) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_617,plain,
! [A_64] :
( ( empty_set = A_64 )
| in('#skF_4',A_64)
| ~ subset(A_64,'#skF_3') ),
inference(resolution,[status(thm)],[c_567,c_48]) ).
tff(c_633,plain,
( ( empty_set = '#skF_3' )
| in('#skF_4','#skF_3') ),
inference(resolution,[status(thm)],[c_40,c_617]) ).
tff(c_641,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_444,c_66,c_633]) ).
tff(c_643,plain,
singleton('#skF_4') = '#skF_3',
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_26,plain,
( ( singleton('#skF_2') = '#skF_1' )
| ( empty_set = '#skF_1' )
| ( singleton('#skF_4') != '#skF_3' ) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_694,plain,
( ( singleton('#skF_2') = '#skF_1' )
| ( empty_set = '#skF_1' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_643,c_26]) ).
tff(c_695,plain,
empty_set = '#skF_1',
inference(splitLeft,[status(thm)],[c_694]) ).
tff(c_704,plain,
! [A_12] : subset('#skF_1',A_12),
inference(demodulation,[status(thm),theory(equality)],[c_695,c_42]) ).
tff(c_642,plain,
~ subset('#skF_1',singleton('#skF_2')),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_712,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_704,c_642]) ).
tff(c_713,plain,
singleton('#skF_2') = '#skF_1',
inference(splitRight,[status(thm)],[c_694]) ).
tff(c_663,plain,
set_difference('#skF_1',singleton('#skF_2')) != empty_set,
inference(resolution,[status(thm)],[c_44,c_642]) ).
tff(c_715,plain,
set_difference('#skF_1','#skF_1') != empty_set,
inference(demodulation,[status(thm),theory(equality)],[c_713,c_663]) ).
tff(c_719,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_103,c_715]) ).
tff(c_721,plain,
empty_set = '#skF_3',
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_30,plain,
( ( singleton('#skF_2') = '#skF_1' )
| ( empty_set = '#skF_1' )
| ( empty_set != '#skF_3' ) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_731,plain,
( ( singleton('#skF_2') = '#skF_1' )
| ( '#skF_3' = '#skF_1' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_721,c_721,c_30]) ).
tff(c_732,plain,
'#skF_3' = '#skF_1',
inference(splitLeft,[status(thm)],[c_731]) ).
tff(c_723,plain,
! [A_12] : subset('#skF_3',A_12),
inference(demodulation,[status(thm),theory(equality)],[c_721,c_42]) ).
tff(c_733,plain,
! [A_12] : subset('#skF_1',A_12),
inference(demodulation,[status(thm),theory(equality)],[c_732,c_723]) ).
tff(c_720,plain,
~ subset('#skF_1',singleton('#skF_2')),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_746,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_733,c_720]) ).
tff(c_747,plain,
singleton('#skF_2') = '#skF_1',
inference(splitRight,[status(thm)],[c_731]) ).
tff(c_754,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_747,c_720]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SEU146+1 : TPTP v9.0.0. Released v3.3.0.
% 0.10/0.13 % 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.13/0.34 % Computer : n005.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:08:12 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.72/2.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.72/2.07
% 3.72/2.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------