%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET964+1 : TPTP v9.0.0. Released v3.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 : n018.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:39:41 PM UTC 2025
% Result : Theorem 8.31s 2.93s
% Output : CNFRefutation 8.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 51 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 103 ( 16 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 93 ( 41 ~; 41 |; 5 &)
% ( 5 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 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 : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-4 aty)
% Number of variables : 93 ( 91 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > in > empty > unordered_pair > ordered_pair > cartesian_product2 > #nlpp > singleton > empty_set > #skF_11 > #skF_1 > #skF_4 > #skF_10 > #skF_13 > #skF_5 > #skF_2 > #skF_7 > #skF_6 > #skF_8 > #skF_9 > #skF_3 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(singleton,type,
singleton: $i > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(unordered_pair,type,
unordered_pair: ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(ordered_pair,type,
ordered_pair: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(empty,type,
empty: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(empty_set,type,
empty_set: $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff(cartesian_product2,type,
cartesian_product2: ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_89,negated_conjecture,
~ ! [A,B,C] :
~ ( ( A != empty_set )
& ( subset(cartesian_product2(B,A),cartesian_product2(C,A))
| subset(cartesian_product2(A,B),cartesian_product2(A,C)) )
& ~ subset(B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_zfmisc_1) ).
tff(f_58,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
tff(f_39,axiom,
! [A] :
( ( A = empty_set )
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
tff(f_51,axiom,
! [A,B,C] :
( ( C = cartesian_product2(A,B) )
<=> ! [D] :
( in(D,C)
<=> ? [E,F] :
( in(E,A)
& in(F,B)
& ( D = ordered_pair(E,F) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_zfmisc_1) ).
tff(f_70,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',l55_zfmisc_1) ).
tff(c_58,plain,
~ subset('#skF_12','#skF_13'),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_38,plain,
! [A_43,B_44] :
( in('#skF_8'(A_43,B_44),A_43)
| subset(A_43,B_44) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_62,plain,
empty_set != '#skF_11',
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_8,plain,
! [A_5] :
( ( empty_set = A_5 )
| in('#skF_1'(A_5),A_5) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_3795,plain,
! [A_364,B_365,D_366] :
( in('#skF_7'(A_364,B_365,cartesian_product2(A_364,B_365),D_366),B_365)
| ~ in(D_366,cartesian_product2(A_364,B_365)) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_6,plain,
! [B_8] : ~ in(B_8,empty_set),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_3812,plain,
! [D_367,A_368] : ~ in(D_367,cartesian_product2(A_368,empty_set)),
inference(resolution,[status(thm)],[c_3795,c_6]) ).
tff(c_3837,plain,
! [A_368] : ( cartesian_product2(A_368,empty_set) = empty_set ),
inference(resolution,[status(thm)],[c_8,c_3812]) ).
tff(c_3957,plain,
! [A_376,B_377,C_378] :
( in('#skF_4'(A_376,B_377,C_378),B_377)
| in('#skF_5'(A_376,B_377,C_378),C_378)
| ( cartesian_product2(A_376,B_377) = C_378 ) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_3969,plain,
! [A_376,C_378] :
( in('#skF_5'(A_376,empty_set,C_378),C_378)
| ( cartesian_product2(A_376,empty_set) = C_378 ) ),
inference(resolution,[status(thm)],[c_3957,c_6]) ).
tff(c_3984,plain,
! [A_376,C_378] :
( in('#skF_5'(A_376,empty_set,C_378),C_378)
| ( empty_set = C_378 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3837,c_3969]) ).
tff(c_459,plain,
! [A_110,B_111,D_112] :
( in('#skF_7'(A_110,B_111,cartesian_product2(A_110,B_111),D_112),B_111)
| ~ in(D_112,cartesian_product2(A_110,B_111)) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_480,plain,
! [D_113,A_114] : ~ in(D_113,cartesian_product2(A_114,empty_set)),
inference(resolution,[status(thm)],[c_459,c_6]) ).
tff(c_513,plain,
! [A_114] : ( cartesian_product2(A_114,empty_set) = empty_set ),
inference(resolution,[status(thm)],[c_8,c_480]) ).
tff(c_673,plain,
! [A_131,B_132,C_133] :
( in('#skF_4'(A_131,B_132,C_133),B_132)
| in('#skF_5'(A_131,B_132,C_133),C_133)
| ( cartesian_product2(A_131,B_132) = C_133 ) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_685,plain,
! [A_131,C_133] :
( in('#skF_5'(A_131,empty_set,C_133),C_133)
| ( cartesian_product2(A_131,empty_set) = C_133 ) ),
inference(resolution,[status(thm)],[c_673,c_6]) ).
tff(c_700,plain,
! [A_131,C_133] :
( in('#skF_5'(A_131,empty_set,C_133),C_133)
| ( empty_set = C_133 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_685]) ).
tff(c_60,plain,
( subset(cartesian_product2('#skF_11','#skF_12'),cartesian_product2('#skF_11','#skF_13'))
| subset(cartesian_product2('#skF_12','#skF_11'),cartesian_product2('#skF_13','#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_67,plain,
subset(cartesian_product2('#skF_12','#skF_11'),cartesian_product2('#skF_13','#skF_11')),
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_365,plain,
! [A_99,B_100,C_101,D_102] :
( in(ordered_pair(A_99,B_100),cartesian_product2(C_101,D_102))
| ~ in(B_100,D_102)
| ~ in(A_99,C_101) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_34,plain,
! [C_47,B_44,A_43] :
( in(C_47,B_44)
| ~ in(C_47,A_43)
| ~ subset(A_43,B_44) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_3304,plain,
! [B_315,D_317,C_316,B_314,A_313] :
( in(ordered_pair(A_313,B_314),B_315)
| ~ subset(cartesian_product2(C_316,D_317),B_315)
| ~ in(B_314,D_317)
| ~ in(A_313,C_316) ),
inference(resolution,[status(thm)],[c_365,c_34]) ).
tff(c_3324,plain,
! [A_318,B_319] :
( in(ordered_pair(A_318,B_319),cartesian_product2('#skF_13','#skF_11'))
| ~ in(B_319,'#skF_11')
| ~ in(A_318,'#skF_12') ),
inference(resolution,[status(thm)],[c_67,c_3304]) ).
tff(c_50,plain,
! [A_52,C_54,B_53,D_55] :
( in(A_52,C_54)
| ~ in(ordered_pair(A_52,B_53),cartesian_product2(C_54,D_55)) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_3358,plain,
! [A_318,B_319] :
( in(A_318,'#skF_13')
| ~ in(B_319,'#skF_11')
| ~ in(A_318,'#skF_12') ),
inference(resolution,[status(thm)],[c_3324,c_50]) ).
tff(c_3362,plain,
! [B_320] : ~ in(B_320,'#skF_11'),
inference(splitLeft,[status(thm)],[c_3358]) ).
tff(c_3378,plain,
empty_set = '#skF_11',
inference(resolution,[status(thm)],[c_700,c_3362]) ).
tff(c_3429,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62,c_3378]) ).
tff(c_3432,plain,
! [A_321] :
( in(A_321,'#skF_13')
| ~ in(A_321,'#skF_12') ),
inference(splitRight,[status(thm)],[c_3358]) ).
tff(c_36,plain,
! [A_43,B_44] :
( ~ in('#skF_8'(A_43,B_44),B_44)
| subset(A_43,B_44) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_3458,plain,
! [A_323] :
( subset(A_323,'#skF_13')
| ~ in('#skF_8'(A_323,'#skF_13'),'#skF_12') ),
inference(resolution,[status(thm)],[c_3432,c_36]) ).
tff(c_3466,plain,
subset('#skF_12','#skF_13'),
inference(resolution,[status(thm)],[c_38,c_3458]) ).
tff(c_3471,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_58,c_3466]) ).
tff(c_3472,plain,
subset(cartesian_product2('#skF_11','#skF_12'),cartesian_product2('#skF_11','#skF_13')),
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_3754,plain,
! [A_357,B_358,C_359,D_360] :
( in(ordered_pair(A_357,B_358),cartesian_product2(C_359,D_360))
| ~ in(B_358,D_360)
| ~ in(A_357,C_359) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_7162,plain,
! [C_601,D_600,B_604,A_602,B_603] :
( in(ordered_pair(A_602,B_604),B_603)
| ~ subset(cartesian_product2(C_601,D_600),B_603)
| ~ in(B_604,D_600)
| ~ in(A_602,C_601) ),
inference(resolution,[status(thm)],[c_3754,c_34]) ).
tff(c_7182,plain,
! [A_605,B_606] :
( in(ordered_pair(A_605,B_606),cartesian_product2('#skF_11','#skF_13'))
| ~ in(B_606,'#skF_12')
| ~ in(A_605,'#skF_11') ),
inference(resolution,[status(thm)],[c_3472,c_7162]) ).
tff(c_48,plain,
! [B_53,D_55,A_52,C_54] :
( in(B_53,D_55)
| ~ in(ordered_pair(A_52,B_53),cartesian_product2(C_54,D_55)) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_7235,plain,
! [B_606,A_605] :
( in(B_606,'#skF_13')
| ~ in(B_606,'#skF_12')
| ~ in(A_605,'#skF_11') ),
inference(resolution,[status(thm)],[c_7182,c_48]) ).
tff(c_7240,plain,
! [A_607] : ~ in(A_607,'#skF_11'),
inference(splitLeft,[status(thm)],[c_7235]) ).
tff(c_7270,plain,
empty_set = '#skF_11',
inference(resolution,[status(thm)],[c_3984,c_7240]) ).
tff(c_7310,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62,c_7270]) ).
tff(c_7331,plain,
! [B_610] :
( in(B_610,'#skF_13')
| ~ in(B_610,'#skF_12') ),
inference(splitRight,[status(thm)],[c_7235]) ).
tff(c_7365,plain,
! [A_612] :
( subset(A_612,'#skF_13')
| ~ in('#skF_8'(A_612,'#skF_13'),'#skF_12') ),
inference(resolution,[status(thm)],[c_7331,c_36]) ).
tff(c_7373,plain,
subset('#skF_12','#skF_13'),
inference(resolution,[status(thm)],[c_38,c_7365]) ).
tff(c_7378,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_58,c_7373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SET964+1 : TPTP v9.0.0. Released v3.2.0.
% 0.07/0.12 % 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.12/0.32 % Computer : n018.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Tue Apr 8 21:52:02 EDT 2025
% 0.12/0.33 % CPUTime :
% 8.31/2.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.34/2.94
% 8.34/2.94 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------