%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM498+3 : TPTP v9.0.0. Released v4.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 : n007.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 07:56:08 PM UTC 2025
% Result : Theorem 12.37s 3.95s
% Output : CNFRefutation 12.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 14
% Syntax : Number of formulae : 78 ( 41 unt; 0 typ; 1 def)
% Number of atoms : 178 ( 87 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 156 ( 56 ~; 56 |; 31 &)
% ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-3 aty)
% Number of variables : 36 ( 29 !; 7 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sdtlseqdt0 > iLess0 > doDivides0 > isPrime0 > aNaturalNumber0 > sdtsldt0 > sdtpldt0 > sdtmndt0 > sdtasdt0 > #nlpp > xp > xn > xm > xk > sz10 > sz00 > #skF_4 > #skF_11 > #skF_6 > #skF_10 > #skF_5 > #skF_9 > #skF_7 > #skF_3 > #skF_2 > #skF_8 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(xk,type,
xk: $i ).
tff(sdtasdt0,type,
sdtasdt0: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff(sz10,type,
sz10: $i ).
tff(sdtmndt0,type,
sdtmndt0: ( $i * $i ) > $i ).
tff(sdtlseqdt0,type,
sdtlseqdt0: ( $i * $i ) > $o ).
tff(sz00,type,
sz00: $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(sdtpldt0,type,
sdtpldt0: ( $i * $i ) > $i ).
tff(isPrime0,type,
isPrime0: $i > $o ).
tff(aNaturalNumber0,type,
aNaturalNumber0: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff(doDivides0,type,
doDivides0: ( $i * $i ) > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(xp,type,
xp: $i ).
tff(iLess0,type,
iLess0: ( $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff(xm,type,
xm: $i ).
tff(sdtsldt0,type,
sdtsldt0: ( $i * $i ) > $i ).
tff(xn,type,
xn: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_535,hypothesis,
( ( xn != xp )
& ? [W0] :
( aNaturalNumber0(W0)
& ( sdtpldt0(xn,W0) = xp ) )
& sdtlseqdt0(xn,xp)
& ( xm != xp )
& ? [W0] :
( aNaturalNumber0(W0)
& ( sdtpldt0(xm,W0) = xp ) )
& sdtlseqdt0(xm,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2287) ).
tff(f_423,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
tff(f_87,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtasdt0(W0,sz10) = W0 )
& ( W0 = sdtasdt0(sz10,W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulUnit) ).
tff(f_502,hypothesis,
( ( xp != sz00 )
& ( xp != sz10 )
& ! [W0] :
( ( aNaturalNumber0(W0)
& ( ? [W1] :
( aNaturalNumber0(W1)
& ( xp = sdtasdt0(W0,W1) ) )
| doDivides0(W0,xp) ) )
=> ( ( W0 = sz10 )
| ( W0 = xp ) ) )
& isPrime0(xp)
& ? [W0] :
( aNaturalNumber0(W0)
& ( sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1860) ).
tff(f_35,axiom,
( aNaturalNumber0(sz10)
& ( sz10 != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
tff(f_278,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( W0 != sz00 )
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul2) ).
tff(f_93,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtasdt0(W0,sz00) = sz00 )
& ( sz00 = sdtasdt0(sz00,W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
tff(f_31,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
tff(f_558,negated_conjecture,
~ ( ( ( xk = sz00 )
| ( xk = sz10 ) )
=> ( ? [W0] :
( aNaturalNumber0(W0)
& ( xn = sdtasdt0(xp,W0) ) )
| doDivides0(xp,xn)
| ? [W0] :
( aNaturalNumber0(W0)
& ( xm = sdtasdt0(xp,W0) ) )
| doDivides0(xp,xm) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
tff(f_540,hypothesis,
( aNaturalNumber0(xk)
& ( sdtasdt0(xn,xm) = sdtasdt0(xp,xk) )
& ( xk = sdtsldt0(sdtasdt0(xn,xm),xp) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2306) ).
tff(f_189,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W0) )
=> ( W0 = W1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEAsym) ).
tff(f_67,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtpldt0(W0,sz00) = W0 )
& ( W0 = sdtpldt0(sz00,W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_AddZero) ).
tff(f_162,definition,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( aNaturalNumber0(W2)
& ( sdtpldt0(W0,W2) = W1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefLE) ).
tff(f_151,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W0,W1) = sz00 )
=> ( ( W0 = sz00 )
| ( W1 = sz00 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroMul) ).
tff(c_431,plain,
xp != xm,
inference(cnfTransformation,[status(thm)],[f_535]) ).
tff(c_145,plain,
aNaturalNumber0(xm),
inference(cnfTransformation,[status(thm)],[f_423]) ).
tff(c_7132,plain,
! [W0_241] :
( ( sdtasdt0(sz10,W0_241) = W0_241 )
| ~ aNaturalNumber0(W0_241) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_7163,plain,
sdtasdt0(sz10,xm) = xm,
inference(resolution,[status(thm)],[c_145,c_7132]) ).
tff(c_439,plain,
xp != xn,
inference(cnfTransformation,[status(thm)],[f_535]) ).
tff(c_147,plain,
aNaturalNumber0(xn),
inference(cnfTransformation,[status(thm)],[f_423]) ).
tff(c_143,plain,
aNaturalNumber0(xp),
inference(cnfTransformation,[status(thm)],[f_423]) ).
tff(c_7301,plain,
! [W0_245] :
( ( sdtasdt0(W0_245,sz10) = W0_245 )
| ~ aNaturalNumber0(W0_245) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_7331,plain,
sdtasdt0(xp,sz10) = xp,
inference(resolution,[status(thm)],[c_143,c_7301]) ).
tff(c_411,plain,
xp != sz00,
inference(cnfTransformation,[status(thm)],[f_502]) ).
tff(c_405,plain,
aNaturalNumber0('#skF_9'),
inference(cnfTransformation,[status(thm)],[f_502]) ).
tff(c_8,plain,
aNaturalNumber0(sz10),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_819,plain,
! [W0_122] :
( ( sdtasdt0(sz10,W0_122) = W0_122 )
| ~ aNaturalNumber0(W0_122) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_845,plain,
sdtasdt0(sz10,'#skF_9') = '#skF_9',
inference(resolution,[status(thm)],[c_405,c_819]) ).
tff(c_3104,plain,
! [W1_158,W0_159] :
( sdtlseqdt0(W1_158,sdtasdt0(W1_158,W0_159))
| ( sz00 = W0_159 )
| ~ aNaturalNumber0(W1_158)
| ~ aNaturalNumber0(W0_159) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_3140,plain,
( sdtlseqdt0(sz10,'#skF_9')
| ( sz00 = '#skF_9' )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0('#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_845,c_3104]) ).
tff(c_3255,plain,
( sdtlseqdt0(sz10,'#skF_9')
| ( sz00 = '#skF_9' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_405,c_8,c_3140]) ).
tff(c_5154,plain,
sz00 = '#skF_9',
inference(splitLeft,[status(thm)],[c_3255]) ).
tff(c_713,plain,
! [W0_120] :
( ( sdtasdt0(W0_120,sz00) = sz00 )
| ~ aNaturalNumber0(W0_120) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_743,plain,
sdtasdt0(xp,sz00) = sz00,
inference(resolution,[status(thm)],[c_143,c_713]) ).
tff(c_4,plain,
aNaturalNumber0(sz00),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_476,plain,
! [W0_114] :
( ( sdtasdt0(xp,W0_114) != xn )
| ~ aNaturalNumber0(W0_114) ),
inference(cnfTransformation,[status(thm)],[f_558]) ).
tff(c_503,plain,
sdtasdt0(xp,sz00) != xn,
inference(resolution,[status(thm)],[c_4,c_476]) ).
tff(c_810,plain,
xn != sz00,
inference(demodulation,[status(thm),theory(equality)],[c_743,c_503]) ).
tff(c_5221,plain,
xn != '#skF_9',
inference(demodulation,[status(thm),theory(equality)],[c_5154,c_810]) ).
tff(c_514,plain,
! [W0_115] :
( ( sdtasdt0(xp,W0_115) != xm )
| ~ aNaturalNumber0(W0_115) ),
inference(cnfTransformation,[status(thm)],[f_558]) ).
tff(c_542,plain,
sdtasdt0(xp,sz00) != xm,
inference(resolution,[status(thm)],[c_4,c_514]) ).
tff(c_809,plain,
xm != sz00,
inference(demodulation,[status(thm),theory(equality)],[c_743,c_542]) ).
tff(c_455,plain,
( ( xk = sz10 )
| ( xk = sz00 ) ),
inference(cnfTransformation,[status(thm)],[f_558]) ).
tff(c_464,plain,
xk = sz00,
inference(splitLeft,[status(thm)],[c_455]) ).
tff(c_443,plain,
sdtasdt0(xp,xk) = sdtasdt0(xn,xm),
inference(cnfTransformation,[status(thm)],[f_540]) ).
tff(c_913,plain,
sdtasdt0(xn,xm) = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_743,c_464,c_443]) ).
tff(c_3164,plain,
( sdtlseqdt0(xn,sz00)
| ( xm = sz00 )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_913,c_3104]) ).
tff(c_3276,plain,
( sdtlseqdt0(xn,sz00)
| ( xm = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_145,c_147,c_3164]) ).
tff(c_3277,plain,
sdtlseqdt0(xn,sz00),
inference(negUnitSimplification,[status(thm)],[c_809,c_3276]) ).
tff(c_5168,plain,
sdtlseqdt0(xn,'#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_5154,c_3277]) ).
tff(c_5436,plain,
! [W1_211,W0_212] :
( ( W1_211 = W0_212 )
| ~ sdtlseqdt0(W1_211,W0_212)
| ~ sdtlseqdt0(W0_212,W1_211)
| ~ aNaturalNumber0(W1_211)
| ~ aNaturalNumber0(W0_212) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_5438,plain,
( ( xn = '#skF_9' )
| ~ sdtlseqdt0('#skF_9',xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0('#skF_9') ),
inference(resolution,[status(thm)],[c_5168,c_5436]) ).
tff(c_5475,plain,
( ( xn = '#skF_9' )
| ~ sdtlseqdt0('#skF_9',xn) ),
inference(demodulation,[status(thm),theory(equality)],[c_405,c_147,c_5438]) ).
tff(c_5476,plain,
~ sdtlseqdt0('#skF_9',xn),
inference(negUnitSimplification,[status(thm)],[c_5221,c_5475]) ).
tff(c_586,plain,
! [W0_117] :
( ( sdtpldt0(sz00,W0_117) = W0_117 )
| ~ aNaturalNumber0(W0_117) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_618,plain,
sdtpldt0(sz00,xn) = xn,
inference(resolution,[status(thm)],[c_147,c_586]) ).
tff(c_5234,plain,
sdtpldt0('#skF_9',xn) = xn,
inference(demodulation,[status(thm),theory(equality)],[c_5154,c_618]) ).
tff(c_6274,plain,
! [W0_225,W2_226] :
( sdtlseqdt0(W0_225,sdtpldt0(W0_225,W2_226))
| ~ aNaturalNumber0(W2_226)
| ~ aNaturalNumber0(sdtpldt0(W0_225,W2_226))
| ~ aNaturalNumber0(W0_225) ),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_6315,plain,
( sdtlseqdt0('#skF_9',xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtpldt0('#skF_9',xn))
| ~ aNaturalNumber0('#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_5234,c_6274]) ).
tff(c_6365,plain,
sdtlseqdt0('#skF_9',xn),
inference(demodulation,[status(thm),theory(equality)],[c_405,c_147,c_5234,c_147,c_6315]) ).
tff(c_6367,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5476,c_6365]) ).
tff(c_6369,plain,
sz00 != '#skF_9',
inference(splitRight,[status(thm)],[c_3255]) ).
tff(c_403,plain,
sdtasdt0(xp,'#skF_9') = sdtasdt0(xn,xm),
inference(cnfTransformation,[status(thm)],[f_502]) ).
tff(c_917,plain,
sdtasdt0(xp,'#skF_9') = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_913,c_403]) ).
tff(c_6757,plain,
! [W1_233,W0_234] :
( ( sz00 = W1_233 )
| ( sz00 = W0_234 )
| ( sdtasdt0(W0_234,W1_233) != sz00 )
| ~ aNaturalNumber0(W1_233)
| ~ aNaturalNumber0(W0_234) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_6783,plain,
( ( sz00 = '#skF_9' )
| ( xp = sz00 )
| ~ aNaturalNumber0('#skF_9')
| ~ aNaturalNumber0(xp) ),
inference(superposition,[status(thm),theory(equality)],[c_917,c_6757]) ).
tff(c_6904,plain,
( ( sz00 = '#skF_9' )
| ( xp = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_143,c_405,c_6783]) ).
tff(c_6906,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_411,c_6369,c_6904]) ).
tff(c_6907,plain,
xk = sz10,
inference(splitRight,[status(thm)],[c_455]) ).
tff(c_6987,plain,
sdtasdt0(xp,sz10) = sdtasdt0(xn,xm),
inference(demodulation,[status(thm),theory(equality)],[c_6907,c_443]) ).
tff(c_8035,plain,
sdtasdt0(xn,xm) = xp,
inference(demodulation,[status(thm),theory(equality)],[c_7331,c_6987]) ).
tff(c_11757,plain,
! [W0_325,W1_326] :
( ( sdtasdt0(W0_325,W1_326) != xp )
| ~ aNaturalNumber0(W1_326)
| ( xp = W0_325 )
| ( sz10 = W0_325 )
| ~ aNaturalNumber0(W0_325) ),
inference(cnfTransformation,[status(thm)],[f_502]) ).
tff(c_11787,plain,
( ~ aNaturalNumber0(xm)
| ( xp = xn )
| ( xn = sz10 )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_8035,c_11757]) ).
tff(c_11882,plain,
( ( xp = xn )
| ( xn = sz10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_147,c_145,c_11787]) ).
tff(c_11883,plain,
xn = sz10,
inference(negUnitSimplification,[status(thm)],[c_439,c_11882]) ).
tff(c_12003,plain,
sdtasdt0(sz10,xm) = xp,
inference(demodulation,[status(thm),theory(equality)],[c_11883,c_8035]) ).
tff(c_12033,plain,
xp = xm,
inference(demodulation,[status(thm),theory(equality)],[c_7163,c_12003]) ).
tff(c_12035,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_431,c_12033]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM498+3 : TPTP v9.0.0. Released v4.0.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.14/0.34 % Computer : n007.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 13:02:09 EDT 2025
% 0.14/0.35 % CPUTime :
% 12.37/3.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.37/3.95
% 12.37/3.95 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------