%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET636+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/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 : n015.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 11.10s 3.77s
% Output : CNFRefutation 11.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 90 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 171 ( 21 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 149 ( 68 ~; 69 |; 3 &)
% ( 7 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 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 : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 134 ( 133 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > member > intersect > disjoint > empty > intersection > #nlpp > empty_set > #skF_7 > #skF_6 > #skF_9 > #skF_8 > #skF_3 > #skF_2 > #skF_1 > #skF_5 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(intersect,type,
intersect: ( $i * $i ) > $o ).
tff(intersection,type,
intersection: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $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('#skF_9',type,
'#skF_9': $i ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_8',type,
'#skF_8': $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('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(f_99,negated_conjecture,
~ ! [B,C] :
( disjoint(B,C)
<=> ( intersection(B,C) = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_th118) ).
tff(f_52,axiom,
! [B,C] :
( disjoint(B,C)
<=> ~ intersect(B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',disjoint_defn) ).
tff(f_67,axiom,
! [B,C] :
( intersect(B,C)
=> intersect(C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_intersect) ).
tff(f_42,axiom,
! [B,C] :
( intersect(B,C)
<=> ? [D] :
( member(D,B)
& member(D,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersect_defn) ).
tff(f_46,axiom,
! [B] : ~ member(B,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',empty_set_defn) ).
tff(f_85,axiom,
! [B] :
( empty(B)
<=> ! [C] : ~ member(C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',empty_defn) ).
tff(f_34,axiom,
! [B,C,D] :
( member(D,intersection(B,C))
<=> ( member(D,B)
& member(D,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection_defn) ).
tff(f_75,axiom,
! [B,C] :
( subset(B,C)
<=> ! [D] :
( member(D,B)
=> member(D,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset_defn) ).
tff(f_59,axiom,
! [B,C] :
( ( B = C )
<=> ( subset(B,C)
& subset(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_defn) ).
tff(c_58,plain,
( ~ disjoint('#skF_6','#skF_7')
| disjoint('#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_119,plain,
~ disjoint('#skF_6','#skF_7'),
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_18,plain,
! [B_10,C_11] :
( disjoint(B_10,C_11)
| intersect(B_10,C_11) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_105,plain,
! [C_43,B_44] :
( intersect(C_43,B_44)
| ~ intersect(B_44,C_43) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_108,plain,
! [C_11,B_10] :
( intersect(C_11,B_10)
| disjoint(B_10,C_11) ),
inference(resolution,[status(thm)],[c_18,c_105]) ).
tff(c_10,plain,
! [B_4,C_5] :
( member('#skF_1'(B_4,C_5),C_5)
| ~ intersect(B_4,C_5) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_12,plain,
! [B_4,C_5] :
( member('#skF_1'(B_4,C_5),B_4)
| ~ intersect(B_4,C_5) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_14,plain,
! [B_9] : ~ member(B_9,empty_set),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_56,plain,
( ( intersection('#skF_6','#skF_7') = empty_set )
| ( intersection('#skF_8','#skF_9') != empty_set ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_154,plain,
intersection('#skF_8','#skF_9') != empty_set,
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_60,plain,
( ( intersection('#skF_6','#skF_7') = empty_set )
| disjoint('#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_129,plain,
disjoint('#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_120,plain,
! [C_46,B_47] :
( intersect(C_46,B_47)
| disjoint(B_47,C_46) ),
inference(resolution,[status(thm)],[c_18,c_105]) ).
tff(c_16,plain,
! [B_10,C_11] :
( ~ intersect(B_10,C_11)
| ~ disjoint(B_10,C_11) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_127,plain,
! [C_46,B_47] :
( ~ disjoint(C_46,B_47)
| disjoint(B_47,C_46) ),
inference(resolution,[status(thm)],[c_120,c_16]) ).
tff(c_132,plain,
disjoint('#skF_9','#skF_8'),
inference(resolution,[status(thm)],[c_129,c_127]) ).
tff(c_40,plain,
! [B_24] :
( empty(B_24)
| member('#skF_3'(B_24),B_24) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_176,plain,
! [D_57,B_58,C_59] :
( member(D_57,B_58)
| ~ member(D_57,intersection(B_58,C_59)) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_554,plain,
! [B_109,C_110] :
( member('#skF_3'(intersection(B_109,C_110)),B_109)
| empty(intersection(B_109,C_110)) ),
inference(resolution,[status(thm)],[c_40,c_176]) ).
tff(c_354,plain,
! [B_87,C_88,D_89] :
( intersect(B_87,C_88)
| ~ member(D_89,C_88)
| ~ member(D_89,B_87) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_366,plain,
! [B_87,B_24] :
( intersect(B_87,B_24)
| ~ member('#skF_3'(B_24),B_87)
| empty(B_24) ),
inference(resolution,[status(thm)],[c_40,c_354]) ).
tff(c_583,plain,
! [B_109,C_110] :
( intersect(B_109,intersection(B_109,C_110))
| empty(intersection(B_109,C_110)) ),
inference(resolution,[status(thm)],[c_554,c_366]) ).
tff(c_255,plain,
! [D_71,C_72,B_73] :
( member(D_71,C_72)
| ~ member(D_71,intersection(B_73,C_72)) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_12715,plain,
! [B_3480,B_3481,C_3482] :
( member('#skF_1'(B_3480,intersection(B_3481,C_3482)),C_3482)
| ~ intersect(B_3480,intersection(B_3481,C_3482)) ),
inference(resolution,[status(thm)],[c_10,c_255]) ).
tff(c_365,plain,
! [B_87,B_4,C_5] :
( intersect(B_87,B_4)
| ~ member('#skF_1'(B_4,C_5),B_87)
| ~ intersect(B_4,C_5) ),
inference(resolution,[status(thm)],[c_12,c_354]) ).
tff(c_13606,plain,
! [C_3629,B_3630,B_3631] :
( intersect(C_3629,B_3630)
| ~ intersect(B_3630,intersection(B_3631,C_3629)) ),
inference(resolution,[status(thm)],[c_12715,c_365]) ).
tff(c_13751,plain,
! [C_3654,B_3655] :
( intersect(C_3654,B_3655)
| empty(intersection(B_3655,C_3654)) ),
inference(resolution,[status(thm)],[c_583,c_13606]) ).
tff(c_277,plain,
! [B_74,C_75] :
( member('#skF_2'(B_74,C_75),B_74)
| subset(B_74,C_75) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_38,plain,
! [C_27,B_24] :
( ~ member(C_27,B_24)
| ~ empty(B_24) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_295,plain,
! [B_74,C_75] :
( ~ empty(B_74)
| subset(B_74,C_75) ),
inference(resolution,[status(thm)],[c_277,c_38]) ).
tff(c_297,plain,
! [C_76] : subset(empty_set,C_76),
inference(resolution,[status(thm)],[c_277,c_14]) ).
tff(c_20,plain,
! [C_13,B_12] :
( ( C_13 = B_12 )
| ~ subset(C_13,B_12)
| ~ subset(B_12,C_13) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_312,plain,
! [C_81] :
( ( empty_set = C_81 )
| ~ subset(C_81,empty_set) ),
inference(resolution,[status(thm)],[c_297,c_20]) ).
tff(c_325,plain,
! [B_74] :
( ( empty_set = B_74 )
| ~ empty(B_74) ),
inference(resolution,[status(thm)],[c_295,c_312]) ).
tff(c_14073,plain,
! [B_3702,C_3703] :
( ( intersection(B_3702,C_3703) = empty_set )
| intersect(C_3703,B_3702) ),
inference(resolution,[status(thm)],[c_13751,c_325]) ).
tff(c_14371,plain,
! [C_3776,B_3777] :
( ~ disjoint(C_3776,B_3777)
| ( intersection(B_3777,C_3776) = empty_set ) ),
inference(resolution,[status(thm)],[c_14073,c_16]) ).
tff(c_14448,plain,
intersection('#skF_8','#skF_9') = empty_set,
inference(resolution,[status(thm)],[c_132,c_14371]) ).
tff(c_14467,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_154,c_14448]) ).
tff(c_14468,plain,
intersection('#skF_6','#skF_7') = empty_set,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_14715,plain,
! [D_3839,B_3840,C_3841] :
( member(D_3839,intersection(B_3840,C_3841))
| ~ member(D_3839,C_3841)
| ~ member(D_3839,B_3840) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_14735,plain,
! [D_3839] :
( member(D_3839,empty_set)
| ~ member(D_3839,'#skF_7')
| ~ member(D_3839,'#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_14468,c_14715]) ).
tff(c_14753,plain,
! [D_3842] :
( ~ member(D_3842,'#skF_7')
| ~ member(D_3842,'#skF_6') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_14735]) ).
tff(c_14834,plain,
! [C_3846] :
( ~ member('#skF_1'('#skF_7',C_3846),'#skF_6')
| ~ intersect('#skF_7',C_3846) ),
inference(resolution,[status(thm)],[c_12,c_14753]) ).
tff(c_14839,plain,
~ intersect('#skF_7','#skF_6'),
inference(resolution,[status(thm)],[c_10,c_14834]) ).
tff(c_14842,plain,
disjoint('#skF_6','#skF_7'),
inference(resolution,[status(thm)],[c_108,c_14839]) ).
tff(c_14849,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_119,c_14842]) ).
tff(c_14850,plain,
intersection('#skF_6','#skF_7') = empty_set,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_15113,plain,
! [D_3890,B_3891,C_3892] :
( member(D_3890,intersection(B_3891,C_3892))
| ~ member(D_3890,C_3892)
| ~ member(D_3890,B_3891) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_15133,plain,
! [D_3890] :
( member(D_3890,empty_set)
| ~ member(D_3890,'#skF_7')
| ~ member(D_3890,'#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_14850,c_15113]) ).
tff(c_15147,plain,
! [D_3893] :
( ~ member(D_3893,'#skF_7')
| ~ member(D_3893,'#skF_6') ),
inference(negUnitSimplification,[status(thm)],[c_14,c_15133]) ).
tff(c_15170,plain,
! [C_3894] :
( ~ member('#skF_1'('#skF_7',C_3894),'#skF_6')
| ~ intersect('#skF_7',C_3894) ),
inference(resolution,[status(thm)],[c_12,c_15147]) ).
tff(c_15175,plain,
~ intersect('#skF_7','#skF_6'),
inference(resolution,[status(thm)],[c_10,c_15170]) ).
tff(c_15179,plain,
disjoint('#skF_6','#skF_7'),
inference(resolution,[status(thm)],[c_108,c_15175]) ).
tff(c_15186,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_119,c_15179]) ).
tff(c_15188,plain,
disjoint('#skF_6','#skF_7'),
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_54,plain,
( ~ disjoint('#skF_6','#skF_7')
| ( intersection('#skF_8','#skF_9') != empty_set ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_15214,plain,
intersection('#skF_8','#skF_9') != empty_set,
inference(demodulation,[status(thm),theory(equality)],[c_15188,c_54]) ).
tff(c_15187,plain,
disjoint('#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_15189,plain,
! [C_3896,B_3897] :
( intersect(C_3896,B_3897)
| disjoint(B_3897,C_3896) ),
inference(resolution,[status(thm)],[c_18,c_105]) ).
tff(c_15197,plain,
! [C_3898,B_3899] :
( ~ disjoint(C_3898,B_3899)
| disjoint(B_3899,C_3898) ),
inference(resolution,[status(thm)],[c_15189,c_16]) ).
tff(c_15203,plain,
disjoint('#skF_9','#skF_8'),
inference(resolution,[status(thm)],[c_15187,c_15197]) ).
tff(c_15252,plain,
! [D_3907,B_3908,C_3909] :
( member(D_3907,B_3908)
| ~ member(D_3907,intersection(B_3908,C_3909)) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_16462,plain,
! [B_4002,C_4003] :
( member('#skF_3'(intersection(B_4002,C_4003)),B_4002)
| empty(intersection(B_4002,C_4003)) ),
inference(resolution,[status(thm)],[c_40,c_15252]) ).
tff(c_15381,plain,
! [B_3931,C_3932,D_3933] :
( intersect(B_3931,C_3932)
| ~ member(D_3933,C_3932)
| ~ member(D_3933,B_3931) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_15393,plain,
! [B_3931,B_24] :
( intersect(B_3931,B_24)
| ~ member('#skF_3'(B_24),B_3931)
| empty(B_24) ),
inference(resolution,[status(thm)],[c_40,c_15381]) ).
tff(c_16509,plain,
! [B_4002,C_4003] :
( intersect(B_4002,intersection(B_4002,C_4003))
| empty(intersection(B_4002,C_4003)) ),
inference(resolution,[status(thm)],[c_16462,c_15393]) ).
tff(c_15304,plain,
! [B_3919,C_3920] :
( member('#skF_1'(B_3919,C_3920),C_3920)
| ~ intersect(B_3919,C_3920) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_4,plain,
! [D_3,C_2,B_1] :
( member(D_3,C_2)
| ~ member(D_3,intersection(B_1,C_2)) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_25958,plain,
! [B_7058,B_7059,C_7060] :
( member('#skF_1'(B_7058,intersection(B_7059,C_7060)),C_7060)
| ~ intersect(B_7058,intersection(B_7059,C_7060)) ),
inference(resolution,[status(thm)],[c_15304,c_4]) ).
tff(c_15392,plain,
! [B_3931,B_4,C_5] :
( intersect(B_3931,B_4)
| ~ member('#skF_1'(B_4,C_5),B_3931)
| ~ intersect(B_4,C_5) ),
inference(resolution,[status(thm)],[c_12,c_15381]) ).
tff(c_28860,plain,
! [C_7450,B_7451,B_7452] :
( intersect(C_7450,B_7451)
| ~ intersect(B_7451,intersection(B_7452,C_7450)) ),
inference(resolution,[status(thm)],[c_25958,c_15392]) ).
tff(c_29273,plain,
! [C_7500,B_7501] :
( intersect(C_7500,B_7501)
| empty(intersection(B_7501,C_7500)) ),
inference(resolution,[status(thm)],[c_16509,c_28860]) ).
tff(c_15347,plain,
! [B_3926,C_3927] :
( member('#skF_2'(B_3926,C_3927),B_3926)
| subset(B_3926,C_3927) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_15371,plain,
! [B_3926,C_3927] :
( ~ empty(B_3926)
| subset(B_3926,C_3927) ),
inference(resolution,[status(thm)],[c_15347,c_38]) ).
tff(c_15373,plain,
! [C_3928] : subset(empty_set,C_3928),
inference(resolution,[status(thm)],[c_15347,c_14]) ).
tff(c_15394,plain,
! [C_3934] :
( ( empty_set = C_3934 )
| ~ subset(C_3934,empty_set) ),
inference(resolution,[status(thm)],[c_15373,c_20]) ).
tff(c_15407,plain,
! [B_3926] :
( ( empty_set = B_3926 )
| ~ empty(B_3926) ),
inference(resolution,[status(thm)],[c_15371,c_15394]) ).
tff(c_29595,plain,
! [B_7548,C_7549] :
( ( intersection(B_7548,C_7549) = empty_set )
| intersect(C_7549,B_7548) ),
inference(resolution,[status(thm)],[c_29273,c_15407]) ).
tff(c_29698,plain,
! [C_7572,B_7573] :
( ~ disjoint(C_7572,B_7573)
| ( intersection(B_7573,C_7572) = empty_set ) ),
inference(resolution,[status(thm)],[c_29595,c_16]) ).
tff(c_29775,plain,
intersection('#skF_8','#skF_9') = empty_set,
inference(resolution,[status(thm)],[c_15203,c_29698]) ).
tff(c_29800,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15214,c_29775]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET636+3 : TPTP v9.0.0. Released v2.2.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 : n015.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:21:50 EDT 2025
% 0.13/0.34 % CPUTime :
% 11.10/3.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.10/3.78
% 11.10/3.78 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------