%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEV422_1 : TPTP v9.0.0. Released v5.0.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 : n009.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 09:11:05 PM UTC 2025
% Result : Theorem 168.64s 138.07s
% Output : CNFRefutation 168.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 29 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 50 ( 33 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 38 ( 17 ~; 14 |; 2 &)
% ( 4 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number arithmetic : 25 ( 0 atm; 13 fun; 11 num; 1 var)
% Number of types : 4 ( 2 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 31 usr; 24 con; 0-2 aty)
% Number of variables : 33 ( 33 !; 0 ?; 33 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > member > union > intersection > difference > #nlpp > singleton > complement > cardinality > empty_set > #skF_1 > #skF_2 > #skF_3 > #skF_4
%Foreground sorts:
tff(element,type,
element: $tType ).
tff(set,type,
set: $tType ).
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skF_5',type,
'#skF_5': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(member,type,
member: ( element * set ) > $o ).
tff(intersection,type,
intersection: ( set * set ) > set ).
tff('#skF_1',type,
'#skF_1': set > element ).
tff('#skF_2',type,
'#skF_2': ( set * set ) > element ).
tff('#skF_3',type,
'#skF_3': element ).
tff(complement,type,
complement: set > set ).
tff(cardinality,type,
cardinality: set > $int ).
tff('#skF_4',type,
'#skF_4': set ).
tff(subset,type,
subset: ( set * set ) > $o ).
tff(singleton,type,
singleton: element > set ).
tff(union,type,
union: ( set * set ) > set ).
tff(empty_set,type,
empty_set: set ).
tff(difference,type,
difference: ( set * set ) > set ).
tff(f_99,negated_conjecture,
~ ! [X: element,C: set,Sizea: $int] :
( ( ~ member(X,C)
& ( Sizea = cardinality(C) ) )
=> ( $sum(Sizea,1) = cardinality(union(singleton(X),C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',vc2) ).
tff(f_82,axiom,
! [X: element,S: set] :
( ( intersection(singleton(X),S) = empty_set )
<=> ( cardinality(union(singleton(X),S)) = $sum(cardinality(S),1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cardinality_intersection_2) ).
tff(f_34,axiom,
! [S: set] :
( ! [X: element] : ~ member(X,S)
<=> ( S = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',empty_set) ).
tff(f_51,axiom,
! [X: element,A: set,B: set] :
( member(X,intersection(A,B))
<=> ( member(X,A)
& member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection) ).
tff(f_38,axiom,
! [X: element,A: element] :
( member(X,singleton(A))
<=> ( X = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton) ).
tff(c_60,plain,
cardinality(union(singleton('#skF_3'),'#skF_4')) != $sum('#skF_5',1),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_67,plain,
cardinality(union(singleton('#skF_3'),'#skF_4')) != $sum(1,'#skF_5'),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_60]) ).
tff(c_183827,plain,
cardinality(union(singleton('#skF_3'),'#skF_4')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_67]) ).
tff(c_183829,plain,
$sum(1,'#skF_5') != '#skE_10',
inference(demodulation,[status(thm),theory(equality)],[c_183827,c_67]) ).
tff(c_183832,plain,
'#skF_5' != $sum($uminus(1),'#skE_10'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_183829]) ).
tff(c_66,plain,
cardinality('#skF_4') = '#skF_5',
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_46,plain,
! [X_26: element,S_27: set] :
( ( cardinality(union(singleton(X_26),S_27)) = $sum(cardinality(S_27),1) )
| ( intersection(singleton(X_26),S_27) != empty_set ) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_185954,plain,
! [X_9723: element,S_9724: set] :
( ( cardinality(union(singleton(X_9723),S_9724)) = $sum(1,cardinality(S_9724)) )
| ( intersection(singleton(X_9723),S_9724) != empty_set ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_46]) ).
tff(c_183830,plain,
cardinality(union(singleton('#skF_3'),'#skF_4')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_67]) ).
tff(c_185976,plain,
( ( $sum(1,cardinality('#skF_4')) = '#skE_10' )
| ( intersection(singleton('#skF_3'),'#skF_4') != empty_set ) ),
inference(superposition,[status(thm),theory(equality)],[c_185954,c_183830]) ).
tff(c_186003,plain,
( ( $sum(1,'#skF_5') = '#skE_10' )
| ( intersection(singleton('#skF_3'),'#skF_4') != empty_set ) ),
inference(demodulation,[status(thm),theory(equality)],[c_66,c_185976]) ).
tff(c_186005,plain,
( ( '#skF_5' = $sum($uminus(1),'#skE_10') )
| ( intersection(singleton('#skF_3'),'#skF_4') != empty_set ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_186003]) ).
tff(c_186113,plain,
intersection(singleton('#skF_3'),'#skF_4') != empty_set,
inference(negUnitSimplification,[status(thm)],[c_183832,c_186005]) ).
tff(c_2,plain,
! [S_1: set] :
( ( empty_set = S_1 )
| member('#skF_1'(S_1),S_1) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_183885,plain,
! [X_9600: element,A_9601: set,B_9602: set] :
( member(X_9600,A_9601)
| ~ member(X_9600,intersection(A_9601,B_9602)) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_184110,plain,
! [A_9640: set,B_9641: set] :
( member('#skF_1'(intersection(A_9640,B_9641)),A_9640)
| ( intersection(A_9640,B_9641) = empty_set ) ),
inference(resolution,[status(thm)],[c_2,c_183885]) ).
tff(c_6,plain,
! [X_5: element,A_6: element] :
( ( X_5 = A_6 )
| ~ member(X_5,singleton(A_6)) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_186254,plain,
! [A_9737: element,B_9738: set] :
( ( '#skF_1'(intersection(singleton(A_9737),B_9738)) = A_9737 )
| ( intersection(singleton(A_9737),B_9738) = empty_set ) ),
inference(resolution,[status(thm)],[c_184110,c_6]) ).
tff(c_183893,plain,
! [X_9603: element,B_9604: set,A_9605: set] :
( member(X_9603,B_9604)
| ~ member(X_9603,intersection(A_9605,B_9604)) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_183898,plain,
! [A_9605: set,B_9604: set] :
( member('#skF_1'(intersection(A_9605,B_9604)),B_9604)
| ( intersection(A_9605,B_9604) = empty_set ) ),
inference(resolution,[status(thm)],[c_2,c_183893]) ).
tff(c_340603,plain,
! [A_19499: element,B_19500: set] :
( member(A_19499,B_19500)
| ( intersection(singleton(A_19499),B_19500) = empty_set )
| ( intersection(singleton(A_19499),B_19500) = empty_set ) ),
inference(superposition,[status(thm),theory(equality)],[c_186254,c_183898]) ).
tff(c_65,plain,
~ member('#skF_3','#skF_4'),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_341275,plain,
intersection(singleton('#skF_3'),'#skF_4') = empty_set,
inference(resolution,[status(thm)],[c_340603,c_65]) ).
tff(c_341281,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_186113,c_341275]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEV422_1 : TPTP v9.0.0. Released v5.0.0.
% 0.11/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.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 00:43:41 EDT 2025
% 0.12/0.34 % CPUTime :
% 141.82/117.40 ***********************************************************************
% 141.82/117.40 After 115.8 sec it's time to try something different, got 91.8 sec left
% 141.82/117.40 ***********************************************************************
% 168.64/138.07 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 168.64/138.08
% 168.64/138.08 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------