%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET199+4 : 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 : n006.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:14 PM UTC 2025
% Result : Theorem 226.06s 204.70s
% Output : CNFRefutation 226.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 3
% Syntax : Number of formulae : 83 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 166 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 148 ( 65 ~; 77 |; 2 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 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 : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 111 ( 111 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > member > equal_set > unordered_pair > union > intersection > difference > #nlpp > sum > singleton > product > power_set > empty_set > #skF_7 > #skF_3 > #skF_5 > #skF_6 > #skF_9 > #skF_8 > #skF_4 > #skF_2 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(equal_set,type,
equal_set: ( $i * $i ) > $o ).
tff(power_set,type,
power_set: $i > $i ).
tff(product,type,
product: $i > $i ).
tff(singleton,type,
singleton: $i > $i ).
tff(unordered_pair,type,
unordered_pair: ( $i * $i ) > $i ).
tff(sum,type,
sum: $i > $i ).
tff(intersection,type,
intersection: ( $i * $i ) > $i ).
tff(union,type,
union: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
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('#skF_9',type,
'#skF_9': $i ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(difference,type,
difference: ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_56,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax',subset) ).
tff(f_121,negated_conjecture,
~ ! [A,X,Y] :
( ( subset(A,X)
& subset(A,Y) )
<=> subset(A,intersection(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thI46) ).
tff(f_72,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,A)
& member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax',intersection) ).
tff(c_112,plain,
! [A_71,B_72] :
( member('#skF_1'(A_71,B_72),A_71)
| subset(A_71,B_72) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_4,plain,
! [A_1,B_2] :
( ~ member('#skF_1'(A_1,B_2),B_2)
| subset(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_149,plain,
! [A_71] : subset(A_71,A_71),
inference(resolution,[status(thm)],[c_112,c_4]) ).
tff(c_66,plain,
( subset('#skF_4',intersection('#skF_5','#skF_6'))
| subset('#skF_7','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_153,plain,
subset('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_70,plain,
( subset('#skF_4',intersection('#skF_5','#skF_6'))
| subset('#skF_7','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_89,plain,
subset('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_6,plain,
! [A_1,B_2] :
( member('#skF_1'(A_1,B_2),A_1)
| subset(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_156,plain,
! [X_75,B_76,A_77] :
( member(X_75,B_76)
| ~ member(X_75,A_77)
| ~ subset(A_77,B_76) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_6083,plain,
! [A_345,B_346,B_347] :
( member('#skF_1'(A_345,B_346),B_347)
| ~ subset(A_345,B_347)
| subset(A_345,B_346) ),
inference(resolution,[status(thm)],[c_6,c_156]) ).
tff(c_2,plain,
! [X_5,B_2,A_1] :
( member(X_5,B_2)
| ~ member(X_5,A_1)
| ~ subset(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_99594,plain,
! [A_1917,B_1918,B_1919,B_1920] :
( member('#skF_1'(A_1917,B_1918),B_1919)
| ~ subset(B_1920,B_1919)
| ~ subset(A_1917,B_1920)
| subset(A_1917,B_1918) ),
inference(resolution,[status(thm)],[c_6083,c_2]) ).
tff(c_100444,plain,
! [A_1917,B_1918] :
( member('#skF_1'(A_1917,B_1918),'#skF_8')
| ~ subset(A_1917,'#skF_7')
| subset(A_1917,B_1918) ),
inference(resolution,[status(thm)],[c_89,c_99594]) ).
tff(c_171,plain,
! [A_1,B_2,B_76] :
( member('#skF_1'(A_1,B_2),B_76)
| ~ subset(A_1,B_76)
| subset(A_1,B_2) ),
inference(resolution,[status(thm)],[c_6,c_156]) ).
tff(c_1172,plain,
! [X_166,A_167,B_168] :
( member(X_166,intersection(A_167,B_168))
| ~ member(X_166,B_168)
| ~ member(X_166,A_167) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_19601,plain,
! [A_826,A_827,B_828] :
( subset(A_826,intersection(A_827,B_828))
| ~ member('#skF_1'(A_826,intersection(A_827,B_828)),B_828)
| ~ member('#skF_1'(A_826,intersection(A_827,B_828)),A_827) ),
inference(resolution,[status(thm)],[c_1172,c_4]) ).
tff(c_156716,plain,
! [A_2421,A_2422,B_2423] :
( ~ member('#skF_1'(A_2421,intersection(A_2422,B_2423)),A_2422)
| ~ subset(A_2421,B_2423)
| subset(A_2421,intersection(A_2422,B_2423)) ),
inference(resolution,[status(thm)],[c_171,c_19601]) ).
tff(c_157696,plain,
! [A_2424,B_2425] :
( ~ subset(A_2424,B_2425)
| ~ subset(A_2424,'#skF_7')
| subset(A_2424,intersection('#skF_8',B_2425)) ),
inference(resolution,[status(thm)],[c_100444,c_156716]) ).
tff(c_62,plain,
( subset('#skF_4',intersection('#skF_5','#skF_6'))
| ~ subset('#skF_7',intersection('#skF_8','#skF_9')) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_421,plain,
~ subset('#skF_7',intersection('#skF_8','#skF_9')),
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_157833,plain,
( ~ subset('#skF_7','#skF_9')
| ~ subset('#skF_7','#skF_7') ),
inference(resolution,[status(thm)],[c_157696,c_421]) ).
tff(c_157896,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_149,c_153,c_157833]) ).
tff(c_157898,plain,
subset('#skF_7',intersection('#skF_8','#skF_9')),
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_60,plain,
( ~ subset('#skF_4','#skF_6')
| ~ subset('#skF_4','#skF_5')
| ~ subset('#skF_7',intersection('#skF_8','#skF_9')) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_158009,plain,
( ~ subset('#skF_4','#skF_6')
| ~ subset('#skF_4','#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_157898,c_60]) ).
tff(c_158010,plain,
~ subset('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_158009]) ).
tff(c_157897,plain,
subset('#skF_4',intersection('#skF_5','#skF_6')),
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_162624,plain,
! [A_2625,B_2626,B_2627] :
( member('#skF_1'(A_2625,B_2626),B_2627)
| ~ subset(A_2625,B_2627)
| subset(A_2625,B_2626) ),
inference(resolution,[status(thm)],[c_6,c_156]) ).
tff(c_22,plain,
! [X_10,A_11,B_12] :
( member(X_10,A_11)
| ~ member(X_10,intersection(A_11,B_12)) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_237879,plain,
! [A_3924,B_3925,A_3926,B_3927] :
( member('#skF_1'(A_3924,B_3925),A_3926)
| ~ subset(A_3924,intersection(A_3926,B_3927))
| subset(A_3924,B_3925) ),
inference(resolution,[status(thm)],[c_162624,c_22]) ).
tff(c_239344,plain,
! [B_3936] :
( member('#skF_1'('#skF_4',B_3936),'#skF_5')
| subset('#skF_4',B_3936) ),
inference(resolution,[status(thm)],[c_157897,c_237879]) ).
tff(c_239388,plain,
subset('#skF_4','#skF_5'),
inference(resolution,[status(thm)],[c_239344,c_4]) ).
tff(c_239408,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_158010,c_158010,c_239388]) ).
tff(c_239409,plain,
~ subset('#skF_4','#skF_6'),
inference(splitRight,[status(thm)],[c_158009]) ).
tff(c_243655,plain,
! [A_4115,B_4116,B_4117] :
( member('#skF_1'(A_4115,B_4116),B_4117)
| ~ subset(A_4115,B_4117)
| subset(A_4115,B_4116) ),
inference(resolution,[status(thm)],[c_6,c_156]) ).
tff(c_20,plain,
! [X_10,B_12,A_11] :
( member(X_10,B_12)
| ~ member(X_10,intersection(A_11,B_12)) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_313969,plain,
! [A_5364,B_5365,B_5366,A_5367] :
( member('#skF_1'(A_5364,B_5365),B_5366)
| ~ subset(A_5364,intersection(A_5367,B_5366))
| subset(A_5364,B_5365) ),
inference(resolution,[status(thm)],[c_243655,c_20]) ).
tff(c_314704,plain,
! [B_5376] :
( member('#skF_1'('#skF_4',B_5376),'#skF_6')
| subset('#skF_4',B_5376) ),
inference(resolution,[status(thm)],[c_157897,c_313969]) ).
tff(c_314746,plain,
subset('#skF_4','#skF_6'),
inference(resolution,[status(thm)],[c_314704,c_4]) ).
tff(c_314765,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_239409,c_239409,c_314746]) ).
tff(c_314767,plain,
~ subset('#skF_7','#skF_9'),
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_64,plain,
( ~ subset('#skF_4','#skF_6')
| ~ subset('#skF_4','#skF_5')
| subset('#skF_7','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_314816,plain,
( ~ subset('#skF_4','#skF_6')
| ~ subset('#skF_4','#skF_5') ),
inference(negUnitSimplification,[status(thm)],[c_314767,c_64]) ).
tff(c_314817,plain,
~ subset('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_314816]) ).
tff(c_314766,plain,
subset('#skF_4',intersection('#skF_5','#skF_6')),
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_314835,plain,
! [X_5385,B_5386,A_5387] :
( member(X_5385,B_5386)
| ~ member(X_5385,A_5387)
| ~ subset(A_5387,B_5386) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_319687,plain,
! [A_5615,B_5616,B_5617] :
( member('#skF_1'(A_5615,B_5616),B_5617)
| ~ subset(A_5615,B_5617)
| subset(A_5615,B_5616) ),
inference(resolution,[status(thm)],[c_6,c_314835]) ).
tff(c_367873,plain,
! [A_6695,B_6696,A_6697,B_6698] :
( member('#skF_1'(A_6695,B_6696),A_6697)
| ~ subset(A_6695,intersection(A_6697,B_6698))
| subset(A_6695,B_6696) ),
inference(resolution,[status(thm)],[c_319687,c_22]) ).
tff(c_368261,plain,
! [B_6699] :
( member('#skF_1'('#skF_4',B_6699),'#skF_5')
| subset('#skF_4',B_6699) ),
inference(resolution,[status(thm)],[c_314766,c_367873]) ).
tff(c_368297,plain,
subset('#skF_4','#skF_5'),
inference(resolution,[status(thm)],[c_368261,c_4]) ).
tff(c_368313,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_314817,c_314817,c_368297]) ).
tff(c_368314,plain,
~ subset('#skF_4','#skF_6'),
inference(splitRight,[status(thm)],[c_314816]) ).
tff(c_368328,plain,
! [X_6700,B_6701,A_6702] :
( member(X_6700,B_6701)
| ~ member(X_6700,A_6702)
| ~ subset(A_6702,B_6701) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_372249,plain,
! [A_6914,B_6915,B_6916] :
( member('#skF_1'(A_6914,B_6915),B_6916)
| ~ subset(A_6914,B_6916)
| subset(A_6914,B_6915) ),
inference(resolution,[status(thm)],[c_6,c_368328]) ).
tff(c_422433,plain,
! [A_7983,B_7984,B_7985,A_7986] :
( member('#skF_1'(A_7983,B_7984),B_7985)
| ~ subset(A_7983,intersection(A_7986,B_7985))
| subset(A_7983,B_7984) ),
inference(resolution,[status(thm)],[c_372249,c_20]) ).
tff(c_422907,plain,
! [B_7989] :
( member('#skF_1'('#skF_4',B_7989),'#skF_6')
| subset('#skF_4',B_7989) ),
inference(resolution,[status(thm)],[c_314766,c_422433]) ).
tff(c_422943,plain,
subset('#skF_4','#skF_6'),
inference(resolution,[status(thm)],[c_422907,c_4]) ).
tff(c_422959,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_368314,c_368314,c_422943]) ).
tff(c_422961,plain,
~ subset('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_423095,plain,
~ subset('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_422960,plain,
subset('#skF_4',intersection('#skF_5','#skF_6')),
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_423201,plain,
! [X_8028,B_8029,A_8030] :
( member(X_8028,B_8029)
| ~ member(X_8028,A_8030)
| ~ subset(A_8030,B_8029) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_428277,plain,
! [A_8270,B_8271,B_8272] :
( member('#skF_1'(A_8270,B_8271),B_8272)
| ~ subset(A_8270,B_8272)
| subset(A_8270,B_8271) ),
inference(resolution,[status(thm)],[c_6,c_423201]) ).
tff(c_486057,plain,
! [A_9396,B_9397,A_9398,B_9399] :
( member('#skF_1'(A_9396,B_9397),A_9398)
| ~ subset(A_9396,intersection(A_9398,B_9399))
| subset(A_9396,B_9397) ),
inference(resolution,[status(thm)],[c_428277,c_22]) ).
tff(c_486490,plain,
! [B_9400] :
( member('#skF_1'('#skF_4',B_9400),'#skF_5')
| subset('#skF_4',B_9400) ),
inference(resolution,[status(thm)],[c_422960,c_486057]) ).
tff(c_486530,plain,
subset('#skF_4','#skF_5'),
inference(resolution,[status(thm)],[c_486490,c_4]) ).
tff(c_486548,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_423095,c_423095,c_486530]) ).
tff(c_486550,plain,
subset('#skF_4','#skF_5'),
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_486549,plain,
( ~ subset('#skF_4','#skF_6')
| subset('#skF_7','#skF_9') ),
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_486552,plain,
~ subset('#skF_4','#skF_6'),
inference(splitLeft,[status(thm)],[c_486549]) ).
tff(c_486647,plain,
! [X_9411,B_9412,A_9413] :
( member(X_9411,B_9412)
| ~ member(X_9411,A_9413)
| ~ subset(A_9413,B_9412) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_491658,plain,
! [A_9647,B_9648,B_9649] :
( member('#skF_1'(A_9647,B_9648),B_9649)
| ~ subset(A_9647,B_9649)
| subset(A_9647,B_9648) ),
inference(resolution,[status(thm)],[c_6,c_486647]) ).
tff(c_556645,plain,
! [A_10865,B_10866,B_10867,A_10868] :
( member('#skF_1'(A_10865,B_10866),B_10867)
| ~ subset(A_10865,intersection(A_10868,B_10867))
| subset(A_10865,B_10866) ),
inference(resolution,[status(thm)],[c_491658,c_20]) ).
tff(c_557270,plain,
! [B_10870] :
( member('#skF_1'('#skF_4',B_10870),'#skF_6')
| subset('#skF_4',B_10870) ),
inference(resolution,[status(thm)],[c_422960,c_556645]) ).
tff(c_557310,plain,
subset('#skF_4','#skF_6'),
inference(resolution,[status(thm)],[c_557270,c_4]) ).
tff(c_557328,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_486552,c_486552,c_557310]) ).
tff(c_557330,plain,
subset('#skF_4','#skF_6'),
inference(splitRight,[status(thm)],[c_486549]) ).
tff(c_68,plain,
( ~ subset('#skF_4','#skF_6')
| ~ subset('#skF_4','#skF_5')
| subset('#skF_7','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_557399,plain,
subset('#skF_7','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_486550,c_557330,c_68]) ).
tff(c_557400,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_422961,c_557399]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET199+4 : TPTP v9.0.0. Released v2.2.0.
% 0.03/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.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Apr 8 20:18:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 226.06/204.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.20/204.71
% 226.20/204.71 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------