%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET632+3 : TPTP v9.0.0. Released v2.2.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 : n028.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:38:57 PM UTC 2025
% Result : Theorem 4.42s 2.06s
% Output : CNFRefutation 4.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 48 ( 16 unt; 0 typ; 0 def)
% Number of atoms : 94 ( 7 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 81 ( 35 ~; 34 |; 4 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 67 ( 66 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > member > intersect > disjoint > empty > #nlpp > empty_set > #skF_5 > #skF_6 > #skF_4 > #skF_3 > #skF_2 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(intersect,type,
intersect: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff(member,type,
member: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff(empty,type,
empty: $i > $o ).
tff(disjoint,type,
disjoint: ( $i * $i ) > $o ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_85,negated_conjecture,
~ ! [B,C,D] :
( ( subset(B,C)
& subset(B,D)
& disjoint(C,D) )
=> ( B = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_th114) ).
tff(f_53,axiom,
! [B,C] :
( disjoint(B,C)
<=> ~ intersect(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',disjoint_defn) ).
tff(f_65,axiom,
! [B,C] :
( intersect(B,C)
=> intersect(C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_intersect) ).
tff(f_75,axiom,
! [B] :
( empty(B)
<=> ! [C] : ~ member(C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',empty_defn) ).
tff(f_35,axiom,
! [B,C] :
( subset(B,C)
<=> ! [D] :
( member(D,B)
=> member(D,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subset_defn) ).
tff(f_43,axiom,
! [B,C] :
( intersect(B,C)
<=> ? [D] :
( member(D,B)
& member(D,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersect_defn) ).
tff(f_47,axiom,
! [B] : ~ member(B,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',empty_set_defn) ).
tff(f_60,axiom,
! [B,C] :
( ( B = C )
<=> ( subset(B,C)
& subset(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_defn) ).
tff(c_36,plain,
disjoint('#skF_5','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_18,plain,
! [B_12,C_13] :
( disjoint(B_12,C_13)
| intersect(B_12,C_13) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_47,plain,
! [C_29,B_30] :
( intersect(C_29,B_30)
| ~ intersect(B_30,C_29) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_66,plain,
! [C_34,B_35] :
( intersect(C_34,B_35)
| disjoint(B_35,C_34) ),
inference(resolution,[status(thm)],[c_18,c_47]) ).
tff(c_16,plain,
! [B_12,C_13] :
( ~ intersect(B_12,C_13)
| ~ disjoint(B_12,C_13) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_74,plain,
! [C_36,B_37] :
( ~ disjoint(C_36,B_37)
| disjoint(B_37,C_36) ),
inference(resolution,[status(thm)],[c_66,c_16]) ).
tff(c_77,plain,
disjoint('#skF_6','#skF_5'),
inference(resolution,[status(thm)],[c_36,c_74]) ).
tff(c_34,plain,
empty_set != '#skF_4',
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_38,plain,
subset('#skF_4','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_32,plain,
! [B_19] :
( empty(B_19)
| member('#skF_3'(B_19),B_19) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_273,plain,
! [D_72,C_73,B_74] :
( member(D_72,C_73)
| ~ member(D_72,B_74)
| ~ subset(B_74,C_73) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_342,plain,
! [B_79,C_80] :
( member('#skF_3'(B_79),C_80)
| ~ subset(B_79,C_80)
| empty(B_79) ),
inference(resolution,[status(thm)],[c_32,c_273]) ).
tff(c_234,plain,
! [B_65,C_66,D_67] :
( intersect(B_65,C_66)
| ~ member(D_67,C_66)
| ~ member(D_67,B_65) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_246,plain,
! [B_65,B_19] :
( intersect(B_65,B_19)
| ~ member('#skF_3'(B_19),B_65)
| empty(B_19) ),
inference(resolution,[status(thm)],[c_32,c_234]) ).
tff(c_402,plain,
! [C_84,B_85] :
( intersect(C_84,B_85)
| ~ subset(B_85,C_84)
| empty(B_85) ),
inference(resolution,[status(thm)],[c_342,c_246]) ).
tff(c_423,plain,
( intersect('#skF_6','#skF_4')
| empty('#skF_4') ),
inference(resolution,[status(thm)],[c_38,c_402]) ).
tff(c_425,plain,
empty('#skF_4'),
inference(splitLeft,[status(thm)],[c_423]) ).
tff(c_97,plain,
! [B_40,C_41] :
( member('#skF_1'(B_40,C_41),B_40)
| subset(B_40,C_41) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_30,plain,
! [C_22,B_19] :
( ~ member(C_22,B_19)
| ~ empty(B_19) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_105,plain,
! [B_40,C_41] :
( ~ empty(B_40)
| subset(B_40,C_41) ),
inference(resolution,[status(thm)],[c_97,c_30]) ).
tff(c_14,plain,
! [B_11] : ~ member(B_11,empty_set),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_107,plain,
! [C_42] : subset(empty_set,C_42),
inference(resolution,[status(thm)],[c_97,c_14]) ).
tff(c_20,plain,
! [C_15,B_14] :
( ( C_15 = B_14 )
| ~ subset(C_15,B_14)
| ~ subset(B_14,C_15) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_170,plain,
! [C_54] :
( ( empty_set = C_54 )
| ~ subset(C_54,empty_set) ),
inference(resolution,[status(thm)],[c_107,c_20]) ).
tff(c_183,plain,
! [B_40] :
( ( empty_set = B_40 )
| ~ empty(B_40) ),
inference(resolution,[status(thm)],[c_105,c_170]) ).
tff(c_430,plain,
empty_set = '#skF_4',
inference(resolution,[status(thm)],[c_425,c_183]) ).
tff(c_435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_430]) ).
tff(c_437,plain,
~ empty('#skF_4'),
inference(splitRight,[status(thm)],[c_423]) ).
tff(c_40,plain,
subset('#skF_4','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_424,plain,
( intersect('#skF_5','#skF_4')
| empty('#skF_4') ),
inference(resolution,[status(thm)],[c_40,c_402]) ).
tff(c_493,plain,
intersect('#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_437,c_424]) ).
tff(c_10,plain,
! [B_6,C_7] :
( member('#skF_2'(B_6,C_7),C_7)
| ~ intersect(B_6,C_7) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_283,plain,
! [B_6,C_7,C_73] :
( member('#skF_2'(B_6,C_7),C_73)
| ~ subset(C_7,C_73)
| ~ intersect(B_6,C_7) ),
inference(resolution,[status(thm)],[c_10,c_273]) ).
tff(c_12,plain,
! [B_6,C_7] :
( member('#skF_2'(B_6,C_7),B_6)
| ~ intersect(B_6,C_7) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_631,plain,
! [B_102,B_103,C_104] :
( intersect(B_102,B_103)
| ~ member('#skF_2'(B_103,C_104),B_102)
| ~ intersect(B_103,C_104) ),
inference(resolution,[status(thm)],[c_12,c_234]) ).
tff(c_2230,plain,
! [C_1058,B_1059,C_1060] :
( intersect(C_1058,B_1059)
| ~ subset(C_1060,C_1058)
| ~ intersect(B_1059,C_1060) ),
inference(resolution,[status(thm)],[c_283,c_631]) ).
tff(c_2249,plain,
! [B_1071] :
( intersect('#skF_6',B_1071)
| ~ intersect(B_1071,'#skF_4') ),
inference(resolution,[status(thm)],[c_38,c_2230]) ).
tff(c_2310,plain,
intersect('#skF_6','#skF_5'),
inference(resolution,[status(thm)],[c_493,c_2249]) ).
tff(c_2330,plain,
~ disjoint('#skF_6','#skF_5'),
inference(resolution,[status(thm)],[c_2310,c_16]) ).
tff(c_2376,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_77,c_2330]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SET632+3 : TPTP v9.0.0. Released v2.2.0.
% 0.12/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 : n028.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 21:20:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 4.42/2.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.42/2.07
% 4.42/2.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------