%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM468+1 : 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 : n014.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:01 PM UTC 2025
% Result : Theorem 104.68s 87.61s
% Output : CNFRefutation 104.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 18
% Syntax : Number of formulae : 156 ( 58 unt; 0 typ; 2 def)
% Number of atoms : 451 ( 157 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 522 ( 227 ~; 243 |; 31 &)
% ( 2 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 104 ( 103 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sdtlseqdt0 > iLess0 > doDivides0 > aNaturalNumber0 > sdtsldt0 > sdtpldt0 > sdtmndt0 > sdtasdt0 > #nlpp > xn > xm > xl > sz10 > sz00 > #skF_2 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(xl,type,
xl: $i ).
tff(sdtasdt0,type,
sdtasdt0: ( $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(sdtpldt0,type,
sdtpldt0: ( $i * $i ) > $i ).
tff(aNaturalNumber0,type,
aNaturalNumber0: $i > $o ).
tff(doDivides0,type,
doDivides0: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(iLess0,type,
iLess0: ( $i * $i ) > $o ).
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_348,negated_conjecture,
~ ( ( xl != sz00 )
=> ( sdtpldt0(xm,xn) = sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
tff(f_340,hypothesis,
( aNaturalNumber0(xl)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1240) ).
tff(f_343,hypothesis,
( doDivides0(xl,xm)
& doDivides0(xl,xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1240_04) ).
tff(f_323,definition,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( ( W0 != sz00 )
& doDivides0(W0,W1) )
=> ! [W2] :
( ( W2 = sdtsldt0(W1,W0) )
<=> ( aNaturalNumber0(W2)
& ( W1 = sdtasdt0(W0,W2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
tff(f_307,definition,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( aNaturalNumber0(W2)
& ( W1 = sdtasdt0(W0,W2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
tff(f_258,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( ( W0 != sz00 )
& ( W1 != W2 )
& sdtlseqdt0(W1,W2) )
=> ( ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& ( sdtasdt0(W1,W0) != sdtasdt0(W2,W0) )
& sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul) ).
tff(f_35,axiom,
( aNaturalNumber0(sz10)
& ( sz10 != sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
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_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_296,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( ( W0 != W1 )
& sdtlseqdt0(W0,W1) )
=> iLess0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH_03) ).
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_81,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulAsso) ).
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_31,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
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_73,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
tff(f_47,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
tff(f_103,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) )
& ( sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAMDistr) ).
tff(c_127,plain,
xl != sz00,
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_119,plain,
aNaturalNumber0(xl),
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_117,plain,
aNaturalNumber0(xm),
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_123,plain,
doDivides0(xl,xm),
inference(cnfTransformation,[status(thm)],[f_343]) ).
tff(c_111,plain,
! [W1_71,W0_70] :
( aNaturalNumber0(sdtsldt0(W1_71,W0_70))
| ~ doDivides0(W0_70,W1_71)
| ( sz00 = W0_70 )
| ~ aNaturalNumber0(W1_71)
| ~ aNaturalNumber0(W0_70) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_115,plain,
aNaturalNumber0(xn),
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_121,plain,
doDivides0(xl,xn),
inference(cnfTransformation,[status(thm)],[f_343]) ).
tff(c_105,plain,
! [W0_65,W1_66] :
( aNaturalNumber0('#skF_2'(W0_65,W1_66))
| ~ doDivides0(W0_65,W1_66)
| ~ aNaturalNumber0(W1_66)
| ~ aNaturalNumber0(W0_65) ),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_103,plain,
! [W0_65,W1_66] :
( ( sdtasdt0(W0_65,'#skF_2'(W0_65,W1_66)) = W1_66 )
| ~ doDivides0(W0_65,W1_66)
| ~ aNaturalNumber0(W1_66)
| ~ aNaturalNumber0(W0_65) ),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_94876,plain,
! [W0_1004,W1_1005,W2_1006] :
( sdtlseqdt0(sdtasdt0(W0_1004,W1_1005),sdtasdt0(W0_1004,W2_1006))
| ~ sdtlseqdt0(W1_1005,W2_1006)
| ( W2_1006 = W1_1005 )
| ( sz00 = W0_1004 )
| ~ aNaturalNumber0(W2_1006)
| ~ aNaturalNumber0(W1_1005)
| ~ aNaturalNumber0(W0_1004) ),
inference(cnfTransformation,[status(thm)],[f_258]) ).
tff(c_216069,plain,
! [W0_1567,W1_1568,W1_1569] :
( sdtlseqdt0(sdtasdt0(W0_1567,W1_1568),W1_1569)
| ~ sdtlseqdt0(W1_1568,'#skF_2'(W0_1567,W1_1569))
| ( W1_1568 = '#skF_2'(W0_1567,W1_1569) )
| ( sz00 = W0_1567 )
| ~ aNaturalNumber0('#skF_2'(W0_1567,W1_1569))
| ~ aNaturalNumber0(W1_1568)
| ~ aNaturalNumber0(W0_1567)
| ~ doDivides0(W0_1567,W1_1569)
| ~ aNaturalNumber0(W1_1569)
| ~ aNaturalNumber0(W0_1567) ),
inference(superposition,[status(thm),theory(equality)],[c_103,c_94876]) ).
tff(c_6,plain,
sz10 != sz00,
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_8,plain,
aNaturalNumber0(sz10),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_162,plain,
! [W0_79] :
( ( sdtasdt0(W0_79,sz10) = W0_79 )
| ~ aNaturalNumber0(W0_79) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_180,plain,
sdtasdt0(sz10,sz10) = sz10,
inference(resolution,[status(thm)],[c_8,c_162]) ).
tff(c_1499,plain,
! [W1_111,W0_112] :
( sdtlseqdt0(W1_111,sdtasdt0(W1_111,W0_112))
| ( sz00 = W0_112 )
| ~ aNaturalNumber0(W1_111)
| ~ aNaturalNumber0(W0_112) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_1550,plain,
( sdtlseqdt0(sz10,sz10)
| ( sz10 = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_180,c_1499]) ).
tff(c_1623,plain,
( sdtlseqdt0(sz10,sz10)
| ( sz10 = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_8,c_1550]) ).
tff(c_1624,plain,
sdtlseqdt0(sz10,sz10),
inference(negUnitSimplification,[status(thm)],[c_6,c_1623]) ).
tff(c_308,plain,
! [W0_83] :
( ( sdtasdt0(sz10,W0_83) = W0_83 )
| ~ aNaturalNumber0(W0_83) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_330,plain,
sdtasdt0(sz10,xl) = xl,
inference(resolution,[status(thm)],[c_119,c_308]) ).
tff(c_1538,plain,
( sdtlseqdt0(sz10,xl)
| ( xl = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_330,c_1499]) ).
tff(c_1613,plain,
( sdtlseqdt0(sz10,xl)
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_8,c_1538]) ).
tff(c_1614,plain,
sdtlseqdt0(sz10,xl),
inference(negUnitSimplification,[status(thm)],[c_127,c_1613]) ).
tff(c_73574,plain,
! [W0_760,W1_761] :
( iLess0(W0_760,W1_761)
| ~ sdtlseqdt0(W0_760,W1_761)
| ( W1_761 = W0_760 )
| ~ aNaturalNumber0(W1_761)
| ~ aNaturalNumber0(W0_760) ),
inference(cnfTransformation,[status(thm)],[f_296]) ).
tff(c_73598,plain,
( iLess0(sz10,xl)
| ( xl = sz10 )
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[c_1614,c_73574]) ).
tff(c_73642,plain,
( iLess0(sz10,xl)
| ( xl = sz10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_119,c_73598]) ).
tff(c_73849,plain,
xl = sz10,
inference(splitLeft,[status(thm)],[c_73642]) ).
tff(c_1652,plain,
! [W1_113,W0_114] :
( ( W1_113 = W0_114 )
| ~ sdtlseqdt0(W1_113,W0_114)
| ~ sdtlseqdt0(W0_114,W1_113)
| ~ aNaturalNumber0(W1_113)
| ~ aNaturalNumber0(W0_114) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_1662,plain,
( ( xl = sz10 )
| ~ sdtlseqdt0(xl,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[c_1614,c_1652]) ).
tff(c_1691,plain,
( ( xl = sz10 )
| ~ sdtlseqdt0(xl,sz10) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_8,c_1662]) ).
tff(c_38224,plain,
~ sdtlseqdt0(xl,sz10),
inference(splitLeft,[status(thm)],[c_1691]) ).
tff(c_73850,plain,
~ sdtlseqdt0(sz10,sz10),
inference(demodulation,[status(thm),theory(equality)],[c_73849,c_38224]) ).
tff(c_73883,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1624,c_73850]) ).
tff(c_73885,plain,
xl != sz10,
inference(splitRight,[status(thm)],[c_73642]) ).
tff(c_329,plain,
sdtasdt0(sz10,xm) = xm,
inference(resolution,[status(thm)],[c_117,c_308]) ).
tff(c_109,plain,
! [W0_70,W1_71] :
( ( sdtasdt0(W0_70,sdtsldt0(W1_71,W0_70)) = W1_71 )
| ~ doDivides0(W0_70,W1_71)
| ( sz00 = W0_70 )
| ~ aNaturalNumber0(W1_71)
| ~ aNaturalNumber0(W0_70) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_4461,plain,
! [W0_168,W1_169,W2_170] :
( ( sdtasdt0(sdtasdt0(W0_168,W1_169),W2_170) = sdtasdt0(W0_168,sdtasdt0(W1_169,W2_170)) )
| ~ aNaturalNumber0(W2_170)
| ~ aNaturalNumber0(W1_169)
| ~ aNaturalNumber0(W0_168) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_4553,plain,
! [W2_170] :
( ( sdtasdt0(sz10,sdtasdt0(xl,W2_170)) = sdtasdt0(xl,W2_170) )
| ~ aNaturalNumber0(W2_170)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_330,c_4461]) ).
tff(c_21983,plain,
! [W2_345] :
( ( sdtasdt0(sz10,sdtasdt0(xl,W2_345)) = sdtasdt0(xl,W2_345) )
| ~ aNaturalNumber0(W2_345) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_119,c_4553]) ).
tff(c_22089,plain,
! [W1_71] :
( ( sdtasdt0(xl,sdtsldt0(W1_71,xl)) = sdtasdt0(sz10,W1_71) )
| ~ aNaturalNumber0(sdtsldt0(W1_71,xl))
| ~ doDivides0(xl,W1_71)
| ( xl = sz00 )
| ~ aNaturalNumber0(W1_71)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_109,c_21983]) ).
tff(c_22179,plain,
! [W1_71] :
( ( sdtasdt0(xl,sdtsldt0(W1_71,xl)) = sdtasdt0(sz10,W1_71) )
| ~ aNaturalNumber0(sdtsldt0(W1_71,xl))
| ~ doDivides0(xl,W1_71)
| ( xl = sz00 )
| ~ aNaturalNumber0(W1_71) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_22089]) ).
tff(c_22187,plain,
! [W1_346] :
( ( sdtasdt0(xl,sdtsldt0(W1_346,xl)) = sdtasdt0(sz10,W1_346) )
| ~ aNaturalNumber0(sdtsldt0(W1_346,xl))
| ~ doDivides0(xl,W1_346)
| ~ aNaturalNumber0(W1_346) ),
inference(negUnitSimplification,[status(thm)],[c_127,c_22179]) ).
tff(c_22197,plain,
! [W1_71] :
( ( sdtasdt0(xl,sdtsldt0(W1_71,xl)) = sdtasdt0(sz10,W1_71) )
| ~ doDivides0(xl,W1_71)
| ( xl = sz00 )
| ~ aNaturalNumber0(W1_71)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[c_111,c_22187]) ).
tff(c_22204,plain,
! [W1_71] :
( ( sdtasdt0(xl,sdtsldt0(W1_71,xl)) = sdtasdt0(sz10,W1_71) )
| ~ doDivides0(xl,W1_71)
| ( xl = sz00 )
| ~ aNaturalNumber0(W1_71) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_22197]) ).
tff(c_22205,plain,
! [W1_71] :
( ( sdtasdt0(xl,sdtsldt0(W1_71,xl)) = sdtasdt0(sz10,W1_71) )
| ~ doDivides0(xl,W1_71)
| ~ aNaturalNumber0(W1_71) ),
inference(negUnitSimplification,[status(thm)],[c_127,c_22204]) ).
tff(c_2736,plain,
! [W1_133,W0_134] :
( aNaturalNumber0(sdtsldt0(W1_133,W0_134))
| ~ doDivides0(W0_134,W1_133)
| ( sz00 = W0_134 )
| ~ aNaturalNumber0(W1_133)
| ~ aNaturalNumber0(W0_134) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_20,plain,
! [W0_11] :
( ( sdtpldt0(W0_11,sz00) = W0_11 )
| ~ aNaturalNumber0(W0_11) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_37923,plain,
! [W1_438,W0_439] :
( ( sdtpldt0(sdtsldt0(W1_438,W0_439),sz00) = sdtsldt0(W1_438,W0_439) )
| ~ doDivides0(W0_439,W1_438)
| ( sz00 = W0_439 )
| ~ aNaturalNumber0(W1_438)
| ~ aNaturalNumber0(W0_439) ),
inference(resolution,[status(thm)],[c_2736,c_20]) ).
tff(c_4,plain,
aNaturalNumber0(sz00),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_129,plain,
! [W0_78] :
( ( sdtasdt0(W0_78,sz00) = sz00 )
| ~ aNaturalNumber0(W0_78) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_149,plain,
sdtasdt0(xl,sz00) = sz00,
inference(resolution,[status(thm)],[c_119,c_129]) ).
tff(c_324,plain,
sdtasdt0(sz10,xn) = xn,
inference(resolution,[status(thm)],[c_115,c_308]) ).
tff(c_1532,plain,
( sdtlseqdt0(sz10,xn)
| ( xn = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_324,c_1499]) ).
tff(c_1609,plain,
( sdtlseqdt0(sz10,xn)
| ( xn = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_8,c_1532]) ).
tff(c_1712,plain,
xn = sz00,
inference(splitLeft,[status(thm)],[c_1609]) ).
tff(c_1737,plain,
doDivides0(xl,sz00),
inference(demodulation,[status(thm),theory(equality)],[c_1712,c_121]) ).
tff(c_7490,plain,
! [W0_209,W2_210] :
( ( sdtsldt0(sdtasdt0(W0_209,W2_210),W0_209) = W2_210 )
| ~ aNaturalNumber0(W2_210)
| ~ doDivides0(W0_209,sdtasdt0(W0_209,W2_210))
| ( sz00 = W0_209 )
| ~ aNaturalNumber0(sdtasdt0(W0_209,W2_210))
| ~ aNaturalNumber0(W0_209) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_7556,plain,
( ( sdtsldt0(sdtasdt0(xl,sz00),xl) = sz00 )
| ~ aNaturalNumber0(sz00)
| ~ doDivides0(xl,sz00)
| ( xl = sz00 )
| ~ aNaturalNumber0(sdtasdt0(xl,sz00))
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_149,c_7490]) ).
tff(c_7619,plain,
( ( sdtsldt0(sz00,xl) = sz00 )
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_4,c_149,c_1737,c_4,c_149,c_7556]) ).
tff(c_7620,plain,
sdtsldt0(sz00,xl) = sz00,
inference(negUnitSimplification,[status(thm)],[c_127,c_7619]) ).
tff(c_237,plain,
! [W0_81] :
( ( sdtpldt0(W0_81,sz00) = W0_81 )
| ~ aNaturalNumber0(W0_81) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_256,plain,
sdtpldt0(xm,sz00) = xm,
inference(resolution,[status(thm)],[c_117,c_237]) ).
tff(c_125,plain,
sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(xn,xl))) != sdtpldt0(xm,xn),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_1736,plain,
sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(sz00,xl))) != sdtpldt0(xm,sz00),
inference(demodulation,[status(thm),theory(equality)],[c_1712,c_1712,c_125]) ).
tff(c_1761,plain,
sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sdtsldt0(sz00,xl))) != xm,
inference(demodulation,[status(thm),theory(equality)],[c_256,c_1736]) ).
tff(c_7710,plain,
sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),sz00)) != xm,
inference(demodulation,[status(thm),theory(equality)],[c_7620,c_1761]) ).
tff(c_37965,plain,
( ( sdtasdt0(xl,sdtsldt0(xm,xl)) != xm )
| ~ doDivides0(xl,xm)
| ( xl = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_37923,c_7710]) ).
tff(c_38104,plain,
( ( sdtasdt0(xl,sdtsldt0(xm,xl)) != xm )
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_117,c_123,c_37965]) ).
tff(c_38105,plain,
sdtasdt0(xl,sdtsldt0(xm,xl)) != xm,
inference(negUnitSimplification,[status(thm)],[c_127,c_38104]) ).
tff(c_38210,plain,
( ( sdtasdt0(sz10,xm) != xm )
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_22205,c_38105]) ).
tff(c_38216,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_117,c_123,c_329,c_38210]) ).
tff(c_38218,plain,
xn != sz00,
inference(splitRight,[status(thm)],[c_1609]) ).
tff(c_178,plain,
sdtasdt0(xn,sz10) = xn,
inference(resolution,[status(thm)],[c_115,c_162]) ).
tff(c_74107,plain,
! [W0_768,W2_769] :
( doDivides0(W0_768,sdtasdt0(W0_768,W2_769))
| ~ aNaturalNumber0(W2_769)
| ~ aNaturalNumber0(sdtasdt0(W0_768,W2_769))
| ~ aNaturalNumber0(W0_768) ),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_74176,plain,
( doDivides0(xn,xn)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtasdt0(xn,sz10))
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_178,c_74107]) ).
tff(c_74235,plain,
doDivides0(xn,xn),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_115,c_178,c_8,c_74176]) ).
tff(c_89492,plain,
! [W0_948,W2_949] :
( ( sdtsldt0(sdtasdt0(W0_948,W2_949),W0_948) = W2_949 )
| ~ aNaturalNumber0(W2_949)
| ~ doDivides0(W0_948,sdtasdt0(W0_948,W2_949))
| ( sz00 = W0_948 )
| ~ aNaturalNumber0(sdtasdt0(W0_948,W2_949))
| ~ aNaturalNumber0(W0_948) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_89597,plain,
( ( sdtsldt0(sdtasdt0(xn,sz10),xn) = sz10 )
| ~ aNaturalNumber0(sz10)
| ~ doDivides0(xn,xn)
| ( xn = sz00 )
| ~ aNaturalNumber0(sdtasdt0(xn,sz10))
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_178,c_89492]) ).
tff(c_89705,plain,
( ( sdtsldt0(xn,xn) = sz10 )
| ( xn = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_115,c_178,c_74235,c_8,c_178,c_89597]) ).
tff(c_89706,plain,
sdtsldt0(xn,xn) = sz10,
inference(negUnitSimplification,[status(thm)],[c_38218,c_89705]) ).
tff(c_589,plain,
! [W1_92,W0_93] :
( ( sdtasdt0(W1_92,W0_93) = sdtasdt0(W0_93,W1_92) )
| ~ aNaturalNumber0(W1_92)
| ~ aNaturalNumber0(W0_93) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_1435,plain,
! [W0_110] :
( ( sdtasdt0(xl,W0_110) = sdtasdt0(W0_110,xl) )
| ~ aNaturalNumber0(W0_110) ),
inference(resolution,[status(thm)],[c_119,c_589]) ).
tff(c_1491,plain,
sdtasdt0(xn,xl) = sdtasdt0(xl,xn),
inference(resolution,[status(thm)],[c_115,c_1435]) ).
tff(c_12,plain,
! [W0_4,W1_5] :
( aNaturalNumber0(sdtasdt0(W0_4,W1_5))
| ~ aNaturalNumber0(W1_5)
| ~ aNaturalNumber0(W0_4) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_81641,plain,
( aNaturalNumber0(sdtasdt0(xl,xn))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_1491,c_12]) ).
tff(c_81653,plain,
aNaturalNumber0(sdtasdt0(xl,xn)),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_119,c_81641]) ).
tff(c_95,plain,
! [W1_60,W0_59] :
( sdtlseqdt0(W1_60,sdtasdt0(W1_60,W0_59))
| ( sz00 = W0_59 )
| ~ aNaturalNumber0(W1_60)
| ~ aNaturalNumber0(W0_59) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_81638,plain,
( sdtlseqdt0(xn,sdtasdt0(xl,xn))
| ( xl = sz00 )
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_1491,c_95]) ).
tff(c_81650,plain,
( sdtlseqdt0(xn,sdtasdt0(xl,xn))
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_115,c_81638]) ).
tff(c_81651,plain,
sdtlseqdt0(xn,sdtasdt0(xl,xn)),
inference(negUnitSimplification,[status(thm)],[c_127,c_81650]) ).
tff(c_99,plain,
! [W0_63,W1_64] :
( iLess0(W0_63,W1_64)
| ~ sdtlseqdt0(W0_63,W1_64)
| ( W1_64 = W0_63 )
| ~ aNaturalNumber0(W1_64)
| ~ aNaturalNumber0(W0_63) ),
inference(cnfTransformation,[status(thm)],[f_296]) ).
tff(c_81657,plain,
( iLess0(xn,sdtasdt0(xl,xn))
| ( sdtasdt0(xl,xn) = xn )
| ~ aNaturalNumber0(sdtasdt0(xl,xn))
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[c_81651,c_99]) ).
tff(c_81662,plain,
( iLess0(xn,sdtasdt0(xl,xn))
| ( sdtasdt0(xl,xn) = xn )
| ~ aNaturalNumber0(sdtasdt0(xl,xn)) ),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_81657]) ).
tff(c_82020,plain,
( iLess0(xn,sdtasdt0(xl,xn))
| ( sdtasdt0(xl,xn) = xn ) ),
inference(demodulation,[status(thm),theory(equality)],[c_81653,c_81662]) ).
tff(c_82021,plain,
sdtasdt0(xl,xn) = xn,
inference(splitLeft,[status(thm)],[c_82020]) ).
tff(c_82028,plain,
sdtasdt0(xn,xl) = xn,
inference(demodulation,[status(thm),theory(equality)],[c_82021,c_1491]) ).
tff(c_89516,plain,
( ( sdtsldt0(sdtasdt0(xn,xl),xn) = xl )
| ~ aNaturalNumber0(xl)
| ~ doDivides0(xn,xn)
| ( xn = sz00 )
| ~ aNaturalNumber0(sdtasdt0(xn,xl))
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_82028,c_89492]) ).
tff(c_89629,plain,
( ( sdtsldt0(xn,xn) = xl )
| ( xn = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_115,c_82028,c_74235,c_119,c_82028,c_89516]) ).
tff(c_89630,plain,
sdtsldt0(xn,xn) = xl,
inference(negUnitSimplification,[status(thm)],[c_38218,c_89629]) ).
tff(c_90003,plain,
xl = sz10,
inference(demodulation,[status(thm),theory(equality)],[c_89706,c_89630]) ).
tff(c_90004,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_73885,c_90003]) ).
tff(c_90006,plain,
sdtasdt0(xl,xn) != xn,
inference(splitRight,[status(thm)],[c_82020]) ).
tff(c_66,plain,
! [W1_45,W0_44] :
( ( W1_45 = W0_44 )
| ~ sdtlseqdt0(W1_45,W0_44)
| ~ sdtlseqdt0(W0_44,W1_45)
| ~ aNaturalNumber0(W1_45)
| ~ aNaturalNumber0(W0_44) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_81659,plain,
( ( sdtasdt0(xl,xn) = xn )
| ~ sdtlseqdt0(sdtasdt0(xl,xn),xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtasdt0(xl,xn)) ),
inference(resolution,[status(thm)],[c_81651,c_66]) ).
tff(c_81665,plain,
( ( sdtasdt0(xl,xn) = xn )
| ~ sdtlseqdt0(sdtasdt0(xl,xn),xn)
| ~ aNaturalNumber0(sdtasdt0(xl,xn)) ),
inference(demodulation,[status(thm),theory(equality)],[c_115,c_81659]) ).
tff(c_90155,plain,
( ( sdtasdt0(xl,xn) = xn )
| ~ sdtlseqdt0(sdtasdt0(xl,xn),xn) ),
inference(demodulation,[status(thm),theory(equality)],[c_81653,c_81665]) ).
tff(c_90156,plain,
~ sdtlseqdt0(sdtasdt0(xl,xn),xn),
inference(negUnitSimplification,[status(thm)],[c_90006,c_90155]) ).
tff(c_216145,plain,
( ~ sdtlseqdt0(xn,'#skF_2'(xl,xn))
| ( '#skF_2'(xl,xn) = xn )
| ( xl = sz00 )
| ~ aNaturalNumber0('#skF_2'(xl,xn))
| ~ doDivides0(xl,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[c_216069,c_90156]) ).
tff(c_216690,plain,
( ~ sdtlseqdt0(xn,'#skF_2'(xl,xn))
| ( '#skF_2'(xl,xn) = xn )
| ( xl = sz00 )
| ~ aNaturalNumber0('#skF_2'(xl,xn)) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_115,c_121,c_216145]) ).
tff(c_216691,plain,
( ~ sdtlseqdt0(xn,'#skF_2'(xl,xn))
| ( '#skF_2'(xl,xn) = xn )
| ~ aNaturalNumber0('#skF_2'(xl,xn)) ),
inference(negUnitSimplification,[status(thm)],[c_127,c_216690]) ).
tff(c_233132,plain,
~ aNaturalNumber0('#skF_2'(xl,xn)),
inference(splitLeft,[status(thm)],[c_216691]) ).
tff(c_233135,plain,
( ~ doDivides0(xl,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[c_105,c_233132]) ).
tff(c_233139,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_119,c_115,c_121,c_233135]) ).
tff(c_233141,plain,
aNaturalNumber0('#skF_2'(xl,xn)),
inference(splitRight,[status(thm)],[c_216691]) ).
tff(c_257,plain,
sdtpldt0(xl,sz00) = xl,
inference(resolution,[status(thm)],[c_119,c_237]) ).
tff(c_253,plain,
sdtpldt0(xn,sz00) = xn,
inference(resolution,[status(thm)],[c_115,c_237]) ).
tff(c_30,plain,
! [W0_18] :
( ( sdtasdt0(sz00,W0_18) = sz00 )
| ~ aNaturalNumber0(W0_18) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_233430,plain,
sdtasdt0(sz00,'#skF_2'(xl,xn)) = sz00,
inference(resolution,[status(thm)],[c_233141,c_30]) ).
tff(c_94012,plain,
! [W1_997,W0_998,W2_999] :
( ( sdtpldt0(sdtasdt0(W1_997,W0_998),sdtasdt0(W2_999,W0_998)) = sdtasdt0(sdtpldt0(W1_997,W2_999),W0_998) )
| ~ aNaturalNumber0(W2_999)
| ~ aNaturalNumber0(W1_997)
| ~ aNaturalNumber0(W0_998) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_94140,plain,
! [W1_66,W2_999,W0_65] :
( ( sdtpldt0(W1_66,sdtasdt0(W2_999,'#skF_2'(W0_65,W1_66))) = sdtasdt0(sdtpldt0(W0_65,W2_999),'#skF_2'(W0_65,W1_66)) )
| ~ aNaturalNumber0(W2_999)
| ~ aNaturalNumber0(W0_65)
| ~ aNaturalNumber0('#skF_2'(W0_65,W1_66))
| ~ doDivides0(W0_65,W1_66)
| ~ aNaturalNumber0(W1_66)
| ~ aNaturalNumber0(W0_65) ),
inference(superposition,[status(thm),theory(equality)],[c_103,c_94012]) ).
tff(c_233504,plain,
( ( sdtasdt0(sdtpldt0(xl,sz00),'#skF_2'(xl,xn)) = sdtpldt0(xn,sz00) )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0('#skF_2'(xl,xn))
| ~ doDivides0(xl,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_233430,c_94140]) ).
tff(c_233702,plain,
sdtasdt0(xl,'#skF_2'(xl,xn)) = xn,
inference(demodulation,[status(thm),theory(equality)],[c_119,c_115,c_121,c_233141,c_119,c_4,c_257,c_253,c_233504]) ).
tff(c_92697,plain,
! [W0_983,W1_984,W2_985] :
( ( sdtpldt0(sdtasdt0(W0_983,W1_984),sdtasdt0(W0_983,W2_985)) = sdtasdt0(W0_983,sdtpldt0(W1_984,W2_985)) )
| ~ aNaturalNumber0(W2_985)
| ~ aNaturalNumber0(W1_984)
| ~ aNaturalNumber0(W0_983) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_92763,plain,
! [W0_70,W1_71,W2_985] :
( ( sdtasdt0(W0_70,sdtpldt0(sdtsldt0(W1_71,W0_70),W2_985)) = sdtpldt0(W1_71,sdtasdt0(W0_70,W2_985)) )
| ~ aNaturalNumber0(W2_985)
| ~ aNaturalNumber0(sdtsldt0(W1_71,W0_70))
| ~ aNaturalNumber0(W0_70)
| ~ doDivides0(W0_70,W1_71)
| ( sz00 = W0_70 )
| ~ aNaturalNumber0(W1_71)
| ~ aNaturalNumber0(W0_70) ),
inference(superposition,[status(thm),theory(equality)],[c_109,c_92697]) ).
tff(c_101,plain,
! [W0_65,W2_69] :
( doDivides0(W0_65,sdtasdt0(W0_65,W2_69))
| ~ aNaturalNumber0(W2_69)
| ~ aNaturalNumber0(sdtasdt0(W0_65,W2_69))
| ~ aNaturalNumber0(W0_65) ),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_96003,plain,
! [W0_1011,W2_1012] :
( ( sdtsldt0(sdtasdt0(W0_1011,W2_1012),W0_1011) = W2_1012 )
| ~ aNaturalNumber0(W2_1012)
| ~ doDivides0(W0_1011,sdtasdt0(W0_1011,W2_1012))
| ( sz00 = W0_1011 )
| ~ aNaturalNumber0(sdtasdt0(W0_1011,W2_1012))
| ~ aNaturalNumber0(W0_1011) ),
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_96157,plain,
! [W0_65,W2_69] :
( ( sdtsldt0(sdtasdt0(W0_65,W2_69),W0_65) = W2_69 )
| ( sz00 = W0_65 )
| ~ aNaturalNumber0(W2_69)
| ~ aNaturalNumber0(sdtasdt0(W0_65,W2_69))
| ~ aNaturalNumber0(W0_65) ),
inference(resolution,[status(thm)],[c_101,c_96003]) ).
tff(c_234364,plain,
( ( sdtsldt0(sdtasdt0(xl,'#skF_2'(xl,xn)),xl) = '#skF_2'(xl,xn) )
| ( xl = sz00 )
| ~ aNaturalNumber0('#skF_2'(xl,xn))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_233702,c_96157]) ).
tff(c_234592,plain,
( ( sdtsldt0(xn,xl) = '#skF_2'(xl,xn) )
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_115,c_233141,c_233702,c_234364]) ).
tff(c_234593,plain,
sdtsldt0(xn,xl) = '#skF_2'(xl,xn),
inference(negUnitSimplification,[status(thm)],[c_127,c_234592]) ).
tff(c_234666,plain,
sdtasdt0(xl,sdtpldt0(sdtsldt0(xm,xl),'#skF_2'(xl,xn))) != sdtpldt0(xm,xn),
inference(demodulation,[status(thm),theory(equality)],[c_234593,c_125]) ).
tff(c_252153,plain,
( ( sdtpldt0(xm,sdtasdt0(xl,'#skF_2'(xl,xn))) != sdtpldt0(xm,xn) )
| ~ aNaturalNumber0('#skF_2'(xl,xn))
| ~ aNaturalNumber0(sdtsldt0(xm,xl))
| ~ aNaturalNumber0(xl)
| ~ doDivides0(xl,xm)
| ( xl = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(superposition,[status(thm),theory(equality)],[c_92763,c_234666]) ).
tff(c_252164,plain,
( ~ aNaturalNumber0(sdtsldt0(xm,xl))
| ( xl = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_117,c_123,c_119,c_233141,c_233702,c_252153]) ).
tff(c_252165,plain,
~ aNaturalNumber0(sdtsldt0(xm,xl)),
inference(negUnitSimplification,[status(thm)],[c_127,c_252164]) ).
tff(c_252175,plain,
( ~ doDivides0(xl,xm)
| ( xl = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[c_111,c_252165]) ).
tff(c_252178,plain,
xl = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_119,c_117,c_123,c_252175]) ).
tff(c_252180,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_127,c_252178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.23 % Problem : NUM468+1 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.24 % 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.47 % Computer : n014.cluster.edu
% 0.12/0.47 % Model : x86_64 x86_64
% 0.12/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.47 % Memory : 8042.1875MB
% 0.12/0.47 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.47 % CPULimit : 300
% 0.12/0.47 % WCLimit : 300
% 0.12/0.47 % DateTime : Tue Apr 8 12:43:05 EDT 2025
% 0.12/0.47 % CPUTime :
% 104.68/87.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 104.68/87.63
% 104.68/87.63 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------