%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU326+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 : 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:53:39 PM UTC 2025
% Result : Theorem 7.25s 2.74s
% Output : CNFRefutation 7.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 32 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 58 ( 34 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 51 ( 25 ~; 16 |; 5 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 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 : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 32 ( 31 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > in > element > v5_membered > v4_membered > v3_membered > v2_membered > v1_xreal_0 > v1_xcmplx_0 > v1_rat_1 > v1_membered > v1_int_1 > natural > empty > complements_of_subsets > #nlpp > powerset > empty_set > #skF_4 > #skF_1 > #skF_5 > #skF_6 > #skF_2 > #skF_3
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(complements_of_subsets,type,
complements_of_subsets: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(v1_int_1,type,
v1_int_1: $i > $o ).
tff(element,type,
element: ( $i * $i ) > $o ).
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(v3_membered,type,
v3_membered: $i > $o ).
tff(empty,type,
empty: $i > $o ).
tff(v1_xreal_0,type,
v1_xreal_0: $i > $o ).
tff(v5_membered,type,
v5_membered: $i > $o ).
tff(empty_set,type,
empty_set: $i ).
tff(v2_membered,type,
v2_membered: $i > $o ).
tff(v1_membered,type,
v1_membered: $i > $o ).
tff(v1_xcmplx_0,type,
v1_xcmplx_0: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff(v1_rat_1,type,
v1_rat_1: $i > $o ).
tff(powerset,type,
powerset: $i > $i ).
tff(natural,type,
natural: $i > $o ).
tff(v4_membered,type,
v4_membered: $i > $o ).
tff(f_222,axiom,
! [A] :
? [B] :
( element(B,powerset(A))
& empty(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
tff(f_239,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(powerset(A)))
=> ( ~ ( ( B != empty_set )
& ( complements_of_subsets(A,B) = empty_set ) )
& ~ ( ( complements_of_subsets(A,B) != empty_set )
& ( B = empty_set ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_tops_2) ).
tff(f_278,axiom,
! [A] :
( empty(A)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
tff(f_195,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k7_setfam_1) ).
tff(f_174,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(complements_of_subsets(A,B),powerset(powerset(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
tff(f_261,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ~ ( ( B != empty_set )
& ( complements_of_subsets(A,B) = empty_set ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_setfam_1) ).
tff(c_124,plain,
! [A_47] : empty('#skF_4'(A_47)),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_132,plain,
( ( complements_of_subsets('#skF_5','#skF_6') = empty_set )
| ( empty_set = '#skF_6' ) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_165,plain,
empty_set = '#skF_6',
inference(splitLeft,[status(thm)],[c_132]) ).
tff(c_154,plain,
! [A_65] :
( ( empty_set = A_65 )
| ~ empty(A_65) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_191,plain,
! [A_78] :
( ( A_78 = '#skF_6' )
| ~ empty(A_78) ),
inference(demodulation,[status(thm),theory(equality)],[c_165,c_154]) ).
tff(c_200,plain,
! [A_47] : ( '#skF_4'(A_47) = '#skF_6' ),
inference(resolution,[status(thm)],[c_124,c_191]) ).
tff(c_126,plain,
! [A_47] : element('#skF_4'(A_47),powerset(A_47)),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_261,plain,
! [A_47] : element('#skF_6',powerset(A_47)),
inference(demodulation,[status(thm),theory(equality)],[c_200,c_126]) ).
tff(c_1534,plain,
! [A_274,B_275] :
( ( complements_of_subsets(A_274,complements_of_subsets(A_274,B_275)) = B_275 )
| ~ element(B_275,powerset(powerset(A_274))) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_1551,plain,
! [A_274] : ( complements_of_subsets(A_274,complements_of_subsets(A_274,'#skF_6')) = '#skF_6' ),
inference(resolution,[status(thm)],[c_261,c_1534]) ).
tff(c_1589,plain,
! [A_280,B_281] :
( element(complements_of_subsets(A_280,B_281),powerset(powerset(A_280)))
| ~ element(B_281,powerset(powerset(A_280))) ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_148,plain,
! [A_57,B_58] :
( ( complements_of_subsets(A_57,B_58) != empty_set )
| ( empty_set = B_58 )
| ~ element(B_58,powerset(powerset(A_57))) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_1488,plain,
! [A_57,B_58] :
( ( complements_of_subsets(A_57,B_58) != '#skF_6' )
| ( B_58 = '#skF_6' )
| ~ element(B_58,powerset(powerset(A_57))) ),
inference(demodulation,[status(thm),theory(equality)],[c_165,c_165,c_148]) ).
tff(c_2883,plain,
! [A_331,B_332] :
( ( complements_of_subsets(A_331,complements_of_subsets(A_331,B_332)) != '#skF_6' )
| ( complements_of_subsets(A_331,B_332) = '#skF_6' )
| ~ element(B_332,powerset(powerset(A_331))) ),
inference(resolution,[status(thm)],[c_1589,c_1488]) ).
tff(c_2899,plain,
! [A_274] :
( ( complements_of_subsets(A_274,'#skF_6') = '#skF_6' )
| ~ element('#skF_6',powerset(powerset(A_274))) ),
inference(superposition,[status(thm),theory(equality)],[c_1551,c_2883]) ).
tff(c_2908,plain,
! [A_274] : ( complements_of_subsets(A_274,'#skF_6') = '#skF_6' ),
inference(demodulation,[status(thm),theory(equality)],[c_261,c_2899]) ).
tff(c_138,plain,
( ( empty_set != '#skF_6' )
| ( complements_of_subsets('#skF_5','#skF_6') != empty_set ) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_189,plain,
complements_of_subsets('#skF_5','#skF_6') != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_165,c_165,c_138]) ).
tff(c_2912,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2908,c_189]) ).
tff(c_2914,plain,
empty_set != '#skF_6',
inference(splitRight,[status(thm)],[c_132]) ).
tff(c_2913,plain,
complements_of_subsets('#skF_5','#skF_6') = empty_set,
inference(splitRight,[status(thm)],[c_132]) ).
tff(c_130,plain,
element('#skF_6',powerset(powerset('#skF_5'))),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_4616,plain,
! [A_519,B_520] :
( ( complements_of_subsets(A_519,B_520) != empty_set )
| ( empty_set = B_520 )
| ~ element(B_520,powerset(powerset(A_519))) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_4635,plain,
( ( complements_of_subsets('#skF_5','#skF_6') != empty_set )
| ( empty_set = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_130,c_4616]) ).
tff(c_4645,plain,
empty_set = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_2913,c_4635]) ).
tff(c_4647,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2914,c_4645]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU326+1 : TPTP v9.0.0. Released v3.3.0.
% 0.04/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 : n006.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:48:52 EDT 2025
% 0.13/0.35 % CPUTime :
% 7.25/2.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.25/2.74
% 7.25/2.74 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------