%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM465+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/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 : n021.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:00 PM UTC 2025
% Result : Theorem 169.54s 134.66s
% Output : CNFRefutation 169.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 19
% Syntax : Number of formulae : 168 ( 61 unt; 0 typ; 1 def)
% Number of atoms : 499 ( 191 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 595 ( 264 ~; 280 |; 27 &)
% ( 1 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 128 ( 127 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sdtlseqdt0 > aNaturalNumber0 > sdtpldt0 > sdtmndt0 > sdtasdt0 > #nlpp > xn > xm > sz10 > sz00 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
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(xm,type,
xm: $i ).
tff(xn,type,
xn: $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_272,hypothesis,
( aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__987) ).
tff(f_212,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtlseqdt0(W0,W1)
| ( ( W1 != W0 )
& sdtlseqdt0(W1,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETotal) ).
tff(f_87,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtasdt0(W0,sz10) = W0 )
& ( W0 = sdtasdt0(sz10,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulUnit) ).
tff(f_31,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC) ).
tff(f_93,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtasdt0(W0,sz00) = sz00 )
& ( sz00 = sdtasdt0(sz00,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulZero) ).
tff(f_35,axiom,
( aNaturalNumber0(sz10)
& ( sz10 != sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
tff(f_67,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtpldt0(W0,sz00) = W0 )
& ( W0 = sdtpldt0(sz00,W0) ) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mDefLE) ).
tff(f_281,negated_conjecture,
~ ( ( xm != sz00 )
=> sdtlseqdt0(xn,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
tff(f_276,hypothesis,
( ( xm != sz00 )
=> sdtlseqdt0(sz10,xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1007) ).
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/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
tff(f_47,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
tff(f_131,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( W0 != sz00 )
=> ! [W1,W2] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) )
| ( sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) )
=> ( W1 = W2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulCanc) ).
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/sandbox/benchmark/theBenchmark.p',mMonMul) ).
tff(f_189,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W0) )
=> ( W0 = W1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEAsym) ).
tff(f_53,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
tff(f_115,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) )
| ( sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) )
=> ( W1 = W2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddCanc) ).
tff(f_73,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
tff(f_151,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W0,W1) = sz00 )
=> ( ( W0 = sz00 )
| ( W1 = sz00 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroMul) ).
tff(c_95,plain,
aNaturalNumber0(xn),
inference(cnfTransformation,[status(thm)],[f_272]) ).
tff(c_72,plain,
! [W1_50] :
( sdtlseqdt0(W1_50,W1_50)
| ~ aNaturalNumber0(W1_50) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_186,plain,
! [W0_63] :
( ( sdtasdt0(sz10,W0_63) = W0_63 )
| ~ aNaturalNumber0(W0_63) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_201,plain,
sdtasdt0(sz10,xn) = xn,
inference(resolution,[status(thm)],[c_95,c_186]) ).
tff(c_4,plain,
aNaturalNumber0(sz00),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_97,plain,
aNaturalNumber0(xm),
inference(cnfTransformation,[status(thm)],[f_272]) ).
tff(c_223,plain,
! [W0_64] :
( ( sdtasdt0(W0_64,sz00) = sz00 )
| ~ aNaturalNumber0(W0_64) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_239,plain,
sdtasdt0(xm,sz00) = sz00,
inference(resolution,[status(thm)],[c_97,c_223]) ).
tff(c_8,plain,
aNaturalNumber0(sz10),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_139,plain,
! [W0_61] :
( ( sdtpldt0(W0_61,sz00) = W0_61 )
| ~ aNaturalNumber0(W0_61) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_154,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(resolution,[status(thm)],[c_8,c_139]) ).
tff(c_1561,plain,
! [W0_101,W2_102] :
( sdtlseqdt0(W0_101,sdtpldt0(W0_101,W2_102))
| ~ aNaturalNumber0(W2_102)
| ~ aNaturalNumber0(sdtpldt0(W0_101,W2_102))
| ~ aNaturalNumber0(W0_101) ),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_1593,plain,
( sdtlseqdt0(sz10,sz10)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,sz00))
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_154,c_1561]) ).
tff(c_1622,plain,
sdtlseqdt0(sz10,sz10),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_8,c_154,c_4,c_1593]) ).
tff(c_157,plain,
! [W0_62] :
( ( sdtasdt0(W0_62,sz10) = W0_62 )
| ~ aNaturalNumber0(W0_62) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_171,plain,
sdtasdt0(sz10,sz10) = sz10,
inference(resolution,[status(thm)],[c_8,c_157]) ).
tff(c_103,plain,
xm != sz00,
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_99,plain,
( sdtlseqdt0(sz10,xm)
| ( xm = sz00 ) ),
inference(cnfTransformation,[status(thm)],[f_276]) ).
tff(c_104,plain,
sdtlseqdt0(sz10,xm),
inference(negUnitSimplification,[status(thm)],[c_103,c_99]) ).
tff(c_173,plain,
sdtasdt0(xm,sz10) = xm,
inference(resolution,[status(thm)],[c_97,c_157]) ).
tff(c_202,plain,
sdtasdt0(sz10,xm) = xm,
inference(resolution,[status(thm)],[c_97,c_186]) ).
tff(c_2134,plain,
! [W0_114,W1_115,W2_116] :
( ( sdtasdt0(sdtasdt0(W0_114,W1_115),W2_116) = sdtasdt0(W0_114,sdtasdt0(W1_115,W2_116)) )
| ~ aNaturalNumber0(W2_116)
| ~ aNaturalNumber0(W1_115)
| ~ aNaturalNumber0(W0_114) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
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_28089,plain,
! [W0_346,W1_347,W2_348] :
( aNaturalNumber0(sdtasdt0(W0_346,sdtasdt0(W1_347,W2_348)))
| ~ aNaturalNumber0(W2_348)
| ~ aNaturalNumber0(sdtasdt0(W0_346,W1_347))
| ~ aNaturalNumber0(W2_348)
| ~ aNaturalNumber0(W1_347)
| ~ aNaturalNumber0(W0_346) ),
inference(superposition,[status(thm),theory(equality)],[c_2134,c_12]) ).
tff(c_28527,plain,
! [W0_346] :
( aNaturalNumber0(sdtasdt0(W0_346,xm))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtasdt0(W0_346,sz10))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(W0_346) ),
inference(superposition,[status(thm),theory(equality)],[c_202,c_28089]) ).
tff(c_28744,plain,
! [W0_346] :
( aNaturalNumber0(sdtasdt0(W0_346,xm))
| ~ aNaturalNumber0(sdtasdt0(W0_346,sz10))
| ~ aNaturalNumber0(W0_346) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_97,c_97,c_28527]) ).
tff(c_2407,plain,
! [W0_119,W2_120,W1_121] :
( ( sdtasdt0(W0_119,W2_120) != sdtasdt0(W0_119,W1_121) )
| ( W2_120 = W1_121 )
| ~ aNaturalNumber0(W2_120)
| ~ aNaturalNumber0(W1_121)
| ( sz00 = W0_119 )
| ~ aNaturalNumber0(W0_119) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_2473,plain,
! [W1_121] :
( ( sdtasdt0(xm,W1_121) != sz00 )
| ( sz00 = W1_121 )
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(W1_121)
| ( xm = sz00 )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_239,c_2407]) ).
tff(c_2591,plain,
! [W1_121] :
( ( sdtasdt0(xm,W1_121) != sz00 )
| ( sz00 = W1_121 )
| ~ aNaturalNumber0(W1_121)
| ( xm = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_4,c_2473]) ).
tff(c_2636,plain,
! [W1_122] :
( ( sdtasdt0(xm,W1_122) != sz00 )
| ( sz00 = W1_122 )
| ~ aNaturalNumber0(W1_122) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_2591]) ).
tff(c_2672,plain,
( ( sdtasdt0(xm,xm) != sz00 )
| ( xm = sz00 ) ),
inference(resolution,[status(thm)],[c_97,c_2636]) ).
tff(c_2699,plain,
sdtasdt0(xm,xm) != sz00,
inference(negUnitSimplification,[status(thm)],[c_103,c_2672]) ).
tff(c_6,plain,
sz10 != sz00,
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_106,plain,
! [W0_60] :
( ( sdtpldt0(sz00,W0_60) = W0_60 )
| ~ aNaturalNumber0(W0_60) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_120,plain,
sdtpldt0(sz00,sz10) = sz10,
inference(resolution,[status(thm)],[c_8,c_106]) ).
tff(c_1602,plain,
( sdtlseqdt0(sz00,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10))
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[status(thm),theory(equality)],[c_120,c_1561]) ).
tff(c_1628,plain,
sdtlseqdt0(sz00,sz10),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8,c_120,c_8,c_1602]) ).
tff(c_5273,plain,
! [W0_159,W1_160,W2_161] :
( sdtlseqdt0(sdtasdt0(W0_159,W1_160),sdtasdt0(W0_159,W2_161))
| ~ sdtlseqdt0(W1_160,W2_161)
| ( W2_161 = W1_160 )
| ( sz00 = W0_159 )
| ~ aNaturalNumber0(W2_161)
| ~ aNaturalNumber0(W1_160)
| ~ aNaturalNumber0(W0_159) ),
inference(cnfTransformation,[status(thm)],[f_258]) ).
tff(c_5421,plain,
! [W1_160] :
( sdtlseqdt0(sdtasdt0(xm,W1_160),xm)
| ~ sdtlseqdt0(W1_160,sz10)
| ( sz10 = W1_160 )
| ( xm = sz00 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(W1_160)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_173,c_5273]) ).
tff(c_5554,plain,
! [W1_160] :
( sdtlseqdt0(sdtasdt0(xm,W1_160),xm)
| ~ sdtlseqdt0(W1_160,sz10)
| ( sz10 = W1_160 )
| ( xm = sz00 )
| ~ aNaturalNumber0(W1_160) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_5421]) ).
tff(c_5555,plain,
! [W1_160] :
( sdtlseqdt0(sdtasdt0(xm,W1_160),xm)
| ~ sdtlseqdt0(W1_160,sz10)
| ( sz10 = W1_160 )
| ~ aNaturalNumber0(W1_160) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_5554]) ).
tff(c_24,plain,
! [W0_14,W1_15,W2_16] :
( ( sdtasdt0(sdtasdt0(W0_14,W1_15),W2_16) = sdtasdt0(W0_14,sdtasdt0(W1_15,W2_16)) )
| ~ aNaturalNumber0(W2_16)
| ~ aNaturalNumber0(W1_15)
| ~ aNaturalNumber0(W0_14) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_2226,plain,
! [W2_116] :
( ( sdtasdt0(xm,sdtasdt0(sz10,W2_116)) = sdtasdt0(xm,W2_116) )
| ~ aNaturalNumber0(W2_116)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_173,c_2134]) ).
tff(c_2278,plain,
! [W2_116] :
( ( sdtasdt0(xm,sdtasdt0(sz10,W2_116)) = sdtasdt0(xm,W2_116) )
| ~ aNaturalNumber0(W2_116) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_2226]) ).
tff(c_28346,plain,
! [W2_116] :
( aNaturalNumber0(sdtasdt0(xm,W2_116))
| ~ aNaturalNumber0(W2_116)
| ~ aNaturalNumber0(sdtasdt0(xm,sz10))
| ~ aNaturalNumber0(W2_116)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(W2_116) ),
inference(superposition,[status(thm),theory(equality)],[c_2278,c_28089]) ).
tff(c_29278,plain,
! [W2_351] :
( aNaturalNumber0(sdtasdt0(xm,W2_351))
| ~ aNaturalNumber0(W2_351) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_97,c_173,c_28346]) ).
tff(c_32,plain,
! [W0_18] :
( ( sdtasdt0(W0_18,sz00) = sz00 )
| ~ aNaturalNumber0(W0_18) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_29871,plain,
! [W2_354] :
( ( sdtasdt0(sdtasdt0(xm,W2_354),sz00) = sz00 )
| ~ aNaturalNumber0(W2_354) ),
inference(resolution,[status(thm)],[c_29278,c_32]) ).
tff(c_30001,plain,
! [W1_15] :
( ( sdtasdt0(xm,sdtasdt0(W1_15,sz00)) = sz00 )
| ~ aNaturalNumber0(W1_15)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(W1_15)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_29871]) ).
tff(c_37842,plain,
! [W1_410] :
( ( sdtasdt0(xm,sdtasdt0(W1_410,sz00)) = sz00 )
| ~ aNaturalNumber0(W1_410) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_4,c_30001]) ).
tff(c_86,plain,
! [W0_55,W1_56,W2_57] :
( sdtlseqdt0(sdtasdt0(W0_55,W1_56),sdtasdt0(W0_55,W2_57))
| ~ sdtlseqdt0(W1_56,W2_57)
| ( W2_57 = W1_56 )
| ( sz00 = W0_55 )
| ~ aNaturalNumber0(W2_57)
| ~ aNaturalNumber0(W1_56)
| ~ aNaturalNumber0(W0_55) ),
inference(cnfTransformation,[status(thm)],[f_258]) ).
tff(c_37952,plain,
! [W2_57,W1_410] :
( sdtlseqdt0(sz00,sdtasdt0(xm,W2_57))
| ~ sdtlseqdt0(sdtasdt0(W1_410,sz00),W2_57)
| ( sdtasdt0(W1_410,sz00) = W2_57 )
| ( xm = sz00 )
| ~ aNaturalNumber0(W2_57)
| ~ aNaturalNumber0(sdtasdt0(W1_410,sz00))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(W1_410) ),
inference(superposition,[status(thm),theory(equality)],[c_37842,c_86]) ).
tff(c_38129,plain,
! [W2_57,W1_410] :
( sdtlseqdt0(sz00,sdtasdt0(xm,W2_57))
| ~ sdtlseqdt0(sdtasdt0(W1_410,sz00),W2_57)
| ( sdtasdt0(W1_410,sz00) = W2_57 )
| ( xm = sz00 )
| ~ aNaturalNumber0(W2_57)
| ~ aNaturalNumber0(sdtasdt0(W1_410,sz00))
| ~ aNaturalNumber0(W1_410) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_37952]) ).
tff(c_41092,plain,
! [W2_426,W1_427] :
( sdtlseqdt0(sz00,sdtasdt0(xm,W2_426))
| ~ sdtlseqdt0(sdtasdt0(W1_427,sz00),W2_426)
| ( sdtasdt0(W1_427,sz00) = W2_426 )
| ~ aNaturalNumber0(W2_426)
| ~ aNaturalNumber0(sdtasdt0(W1_427,sz00))
| ~ aNaturalNumber0(W1_427) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_38129]) ).
tff(c_41245,plain,
( sdtlseqdt0(sz00,sdtasdt0(xm,xm))
| ( sdtasdt0(xm,sz00) = xm )
| ~ aNaturalNumber0(sdtasdt0(xm,sz00))
| ~ aNaturalNumber0(xm)
| ~ sdtlseqdt0(sz00,sz10)
| ( sz10 = sz00 )
| ~ aNaturalNumber0(sz00) ),
inference(resolution,[status(thm)],[c_5555,c_41092]) ).
tff(c_41403,plain,
( sdtlseqdt0(sz00,sdtasdt0(xm,xm))
| ( xm = sz00 )
| ( sz10 = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1628,c_97,c_4,c_239,c_239,c_41245]) ).
tff(c_41404,plain,
sdtlseqdt0(sz00,sdtasdt0(xm,xm)),
inference(negUnitSimplification,[status(thm)],[c_6,c_103,c_41403]) ).
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_41458,plain,
( ( sdtasdt0(xm,xm) = sz00 )
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(resolution,[status(thm)],[c_41404,c_66]) ).
tff(c_41469,plain,
( ( sdtasdt0(xm,xm) = sz00 )
| ~ sdtlseqdt0(sdtasdt0(xm,xm),sz00)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_41458]) ).
tff(c_41470,plain,
( ~ sdtlseqdt0(sdtasdt0(xm,xm),sz00)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(negUnitSimplification,[status(thm)],[c_2699,c_41469]) ).
tff(c_41471,plain,
~ aNaturalNumber0(sdtasdt0(xm,xm)),
inference(splitLeft,[status(thm)],[c_41470]) ).
tff(c_41474,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,sz10))
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[c_28744,c_41471]) ).
tff(c_41484,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_97,c_97,c_173,c_41474]) ).
tff(c_41486,plain,
aNaturalNumber0(sdtasdt0(xm,xm)),
inference(splitRight,[status(thm)],[c_41470]) ).
tff(c_26,plain,
! [W0_17] :
( ( sdtasdt0(sz10,W0_17) = W0_17 )
| ~ aNaturalNumber0(W0_17) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_41741,plain,
sdtasdt0(sz10,sdtasdt0(xm,xm)) = sdtasdt0(xm,xm),
inference(resolution,[status(thm)],[c_41486,c_26]) ).
tff(c_112847,plain,
! [W0_780,W1_781,W1_782,W2_783] :
( sdtlseqdt0(sdtasdt0(sdtasdt0(W0_780,W1_781),W1_782),sdtasdt0(W0_780,sdtasdt0(W1_781,W2_783)))
| ~ sdtlseqdt0(W1_782,W2_783)
| ( W2_783 = W1_782 )
| ( sdtasdt0(W0_780,W1_781) = sz00 )
| ~ aNaturalNumber0(W2_783)
| ~ aNaturalNumber0(W1_782)
| ~ aNaturalNumber0(sdtasdt0(W0_780,W1_781))
| ~ aNaturalNumber0(W2_783)
| ~ aNaturalNumber0(W1_781)
| ~ aNaturalNumber0(W0_780) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_5273]) ).
tff(c_113084,plain,
! [W1_782] :
( sdtlseqdt0(sdtasdt0(sdtasdt0(sz10,xm),W1_782),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(W1_782,xm)
| ( xm = W1_782 )
| ( sdtasdt0(sz10,xm) = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(W1_782)
| ~ aNaturalNumber0(sdtasdt0(sz10,xm))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_41741,c_112847]) ).
tff(c_113984,plain,
! [W1_782] :
( sdtlseqdt0(sdtasdt0(xm,W1_782),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(W1_782,xm)
| ( xm = W1_782 )
| ( xm = sz00 )
| ~ aNaturalNumber0(W1_782) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_97,c_97,c_97,c_202,c_97,c_202,c_202,c_113084]) ).
tff(c_120946,plain,
! [W1_800] :
( sdtlseqdt0(sdtasdt0(xm,W1_800),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(W1_800,xm)
| ( xm = W1_800 )
| ~ aNaturalNumber0(W1_800) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_113984]) ).
tff(c_120997,plain,
( sdtlseqdt0(xm,sdtasdt0(xm,xm))
| ~ sdtlseqdt0(sz10,xm)
| ( xm = sz10 )
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_173,c_120946]) ).
tff(c_121041,plain,
( sdtlseqdt0(xm,sdtasdt0(xm,xm))
| ( xm = sz10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_104,c_120997]) ).
tff(c_121078,plain,
xm = sz10,
inference(splitLeft,[status(thm)],[c_121041]) ).
tff(c_676,plain,
! [W1_82,W0_83] :
( ( sdtpldt0(W1_82,W0_83) = sdtpldt0(W0_83,W1_82) )
| ~ aNaturalNumber0(W1_82)
| ~ aNaturalNumber0(W0_83) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_716,plain,
! [W0_84] :
( ( sdtpldt0(xm,W0_84) = sdtpldt0(W0_84,xm) )
| ~ aNaturalNumber0(W0_84) ),
inference(resolution,[status(thm)],[c_97,c_676]) ).
tff(c_743,plain,
sdtpldt0(xm,sz10) = sdtpldt0(sz10,xm),
inference(resolution,[status(thm)],[c_8,c_716]) ).
tff(c_1664,plain,
! [W0_103,W2_104,W1_105] :
( ( sdtpldt0(W0_103,W2_104) != sdtpldt0(W0_103,W1_105) )
| ( W2_104 = W1_105 )
| ~ aNaturalNumber0(W2_104)
| ~ aNaturalNumber0(W1_105)
| ~ aNaturalNumber0(W0_103) ),
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_1690,plain,
! [W1_105] :
( ( sdtpldt0(xm,W1_105) != sdtpldt0(sz10,xm) )
| ( sz10 = W1_105 )
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(W1_105)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_743,c_1664]) ).
tff(c_87084,plain,
! [W1_691] :
( ( sdtpldt0(xm,W1_691) != sdtpldt0(sz10,xm) )
| ( sz10 = W1_691 )
| ~ aNaturalNumber0(W1_691) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_1690]) ).
tff(c_87234,plain,
( ( sdtpldt0(xm,xm) != sdtpldt0(sz10,xm) )
| ( xm = sz10 ) ),
inference(resolution,[status(thm)],[c_97,c_87084]) ).
tff(c_87235,plain,
sdtpldt0(xm,xm) != sdtpldt0(sz10,xm),
inference(splitLeft,[status(thm)],[c_87234]) ).
tff(c_121712,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121078,c_87235]) ).
tff(c_121714,plain,
xm != sz10,
inference(splitRight,[status(thm)],[c_121041]) ).
tff(c_486,plain,
! [W1_75,W0_76] :
( ( sdtasdt0(W1_75,W0_76) = sdtasdt0(W0_76,W1_75) )
| ~ aNaturalNumber0(W1_75)
| ~ aNaturalNumber0(W0_76) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_563,plain,
! [W0_79] :
( ( sdtasdt0(xn,W0_79) = sdtasdt0(W0_79,xn) )
| ~ aNaturalNumber0(W0_79) ),
inference(resolution,[status(thm)],[c_95,c_486]) ).
tff(c_590,plain,
sdtasdt0(xn,xm) = sdtasdt0(xm,xn),
inference(resolution,[status(thm)],[c_97,c_563]) ).
tff(c_101,plain,
~ sdtlseqdt0(xn,sdtasdt0(xn,xm)),
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_625,plain,
~ sdtlseqdt0(xn,sdtasdt0(xm,xn)),
inference(demodulation,[status(thm),theory(equality)],[c_590,c_101]) ).
tff(c_238,plain,
sdtasdt0(xn,sz00) = sz00,
inference(resolution,[status(thm)],[c_95,c_223]) ).
tff(c_2471,plain,
! [W2_120] :
( ( sdtasdt0(xn,W2_120) != sz00 )
| ( sz00 = W2_120 )
| ~ aNaturalNumber0(W2_120)
| ~ aNaturalNumber0(sz00)
| ( xn = sz00 )
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_238,c_2407]) ).
tff(c_2589,plain,
! [W2_120] :
( ( sdtasdt0(xn,W2_120) != sz00 )
| ( sz00 = W2_120 )
| ~ aNaturalNumber0(W2_120)
| ( xn = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_95,c_4,c_2471]) ).
tff(c_11938,plain,
xn = sz00,
inference(splitLeft,[status(thm)],[c_2589]) ).
tff(c_1156,plain,
! [W1_92,W0_93] :
( ( sz00 = W1_92 )
| ( sz00 = W0_93 )
| ( sdtasdt0(W0_93,W1_92) != sz00 )
| ~ aNaturalNumber0(W1_92)
| ~ aNaturalNumber0(W0_93) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_1170,plain,
( ( xm = sz00 )
| ( xn = sz00 )
| ( sdtasdt0(xm,xn) != sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_590,c_1156]) ).
tff(c_1224,plain,
( ( xm = sz00 )
| ( xn = sz00 )
| ( sdtasdt0(xm,xn) != sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_95,c_97,c_1170]) ).
tff(c_1225,plain,
( ( xn = sz00 )
| ( sdtasdt0(xm,xn) != sz00 ) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_1224]) ).
tff(c_1273,plain,
sdtasdt0(xm,xn) != sz00,
inference(splitLeft,[status(thm)],[c_1225]) ).
tff(c_629,plain,
( aNaturalNumber0(sdtasdt0(xm,xn))
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_590,c_12]) ).
tff(c_633,plain,
aNaturalNumber0(sdtasdt0(xm,xn)),
inference(demodulation,[status(thm),theory(equality)],[c_95,c_97,c_629]) ).
tff(c_1704,plain,
! [W2_104] :
( ( sdtpldt0(sz10,W2_104) != sz10 )
| ( sz00 = W2_104 )
| ~ aNaturalNumber0(W2_104)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_154,c_1664]) ).
tff(c_6912,plain,
! [W2_180] :
( ( sdtpldt0(sz10,W2_180) != sz10 )
| ( sz00 = W2_180 )
| ~ aNaturalNumber0(W2_180) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_4,c_1704]) ).
tff(c_6930,plain,
( ( sdtpldt0(sz10,sdtasdt0(xm,xn)) != sz10 )
| ( sdtasdt0(xm,xn) = sz00 ) ),
inference(resolution,[status(thm)],[c_633,c_6912]) ).
tff(c_6960,plain,
sdtpldt0(sz10,sdtasdt0(xm,xn)) != sz10,
inference(negUnitSimplification,[status(thm)],[c_1273,c_6930]) ).
tff(c_11965,plain,
sdtpldt0(sz10,sdtasdt0(xm,sz00)) != sz10,
inference(demodulation,[status(thm),theory(equality)],[c_11938,c_6960]) ).
tff(c_12075,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_154,c_239,c_11965]) ).
tff(c_12077,plain,
xn != sz00,
inference(splitRight,[status(thm)],[c_2589]) ).
tff(c_172,plain,
sdtasdt0(xn,sz10) = xn,
inference(resolution,[status(thm)],[c_95,c_157]) ).
tff(c_5406,plain,
! [W2_161] :
( sdtlseqdt0(xn,sdtasdt0(xn,W2_161))
| ~ sdtlseqdt0(sz10,W2_161)
| ( sz10 = W2_161 )
| ( xn = sz00 )
| ~ aNaturalNumber0(W2_161)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[status(thm),theory(equality)],[c_172,c_5273]) ).
tff(c_5541,plain,
! [W2_161] :
( sdtlseqdt0(xn,sdtasdt0(xn,W2_161))
| ~ sdtlseqdt0(sz10,W2_161)
| ( sz10 = W2_161 )
| ( xn = sz00 )
| ~ aNaturalNumber0(W2_161) ),
inference(demodulation,[status(thm),theory(equality)],[c_95,c_8,c_5406]) ).
tff(c_335879,plain,
! [W2_1202] :
( sdtlseqdt0(xn,sdtasdt0(xn,W2_1202))
| ~ sdtlseqdt0(sz10,W2_1202)
| ( sz10 = W2_1202 )
| ~ aNaturalNumber0(W2_1202) ),
inference(negUnitSimplification,[status(thm)],[c_12077,c_5541]) ).
tff(c_335962,plain,
( sdtlseqdt0(xn,sdtasdt0(xm,xn))
| ~ sdtlseqdt0(sz10,xm)
| ( xm = sz10 )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_590,c_335879]) ).
tff(c_336059,plain,
( sdtlseqdt0(xn,sdtasdt0(xm,xn))
| ( xm = sz10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_104,c_335962]) ).
tff(c_336061,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_121714,c_625,c_336059]) ).
tff(c_336062,plain,
xm = sz10,
inference(splitRight,[status(thm)],[c_87234]) ).
tff(c_499,plain,
! [W0_4,W1_5,W0_76] :
( ( sdtasdt0(sdtasdt0(W0_4,W1_5),W0_76) = sdtasdt0(W0_76,sdtasdt0(W0_4,W1_5)) )
| ~ aNaturalNumber0(W0_76)
| ~ aNaturalNumber0(W1_5)
| ~ aNaturalNumber0(W0_4) ),
inference(resolution,[status(thm)],[c_12,c_486]) ).
tff(c_2503,plain,
! [W2_120] :
( ( sdtasdt0(xm,W2_120) != xm )
| ( sz10 = W2_120 )
| ~ aNaturalNumber0(W2_120)
| ~ aNaturalNumber0(sz10)
| ( xm = sz00 )
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_173,c_2407]) ).
tff(c_2634,plain,
! [W2_120] :
( ( sdtasdt0(xm,W2_120) != xm )
| ( sz10 = W2_120 )
| ~ aNaturalNumber0(W2_120)
| ( xm = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_2503]) ).
tff(c_3576,plain,
! [W2_138] :
( ( sdtasdt0(xm,W2_138) != xm )
| ( sz10 = W2_138 )
| ~ aNaturalNumber0(W2_138) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_2634]) ).
tff(c_3629,plain,
( ( sdtasdt0(xm,xm) != xm )
| ( xm = sz10 ) ),
inference(resolution,[status(thm)],[c_97,c_3576]) ).
tff(c_3631,plain,
sdtasdt0(xm,xm) != xm,
inference(splitLeft,[status(thm)],[c_3629]) ).
tff(c_3070,plain,
! [W2_130,W0_131,W1_132] :
( ( sdtasdt0(W2_130,W0_131) != sdtasdt0(W1_132,W0_131) )
| ( W2_130 = W1_132 )
| ~ aNaturalNumber0(W2_130)
| ~ aNaturalNumber0(W1_132)
| ( sz00 = W0_131 )
| ~ aNaturalNumber0(W0_131) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_63118,plain,
! [W2_549,W2_550,W0_551,W1_552] :
( ( sdtasdt0(W2_549,W2_550) != sdtasdt0(W0_551,sdtasdt0(W1_552,W2_550)) )
| ( sdtasdt0(W0_551,W1_552) = W2_549 )
| ~ aNaturalNumber0(W2_549)
| ~ aNaturalNumber0(sdtasdt0(W0_551,W1_552))
| ( sz00 = W2_550 )
| ~ aNaturalNumber0(W2_550)
| ~ aNaturalNumber0(W2_550)
| ~ aNaturalNumber0(W1_552)
| ~ aNaturalNumber0(W0_551) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_3070]) ).
tff(c_63169,plain,
! [W2_549] :
( ( sdtasdt0(xm,xm) != sdtasdt0(W2_549,xm) )
| ( sdtasdt0(sz10,xm) = W2_549 )
| ~ aNaturalNumber0(W2_549)
| ~ aNaturalNumber0(sdtasdt0(sz10,xm))
| ( xm = sz00 )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[status(thm),theory(equality)],[c_41741,c_63118]) ).
tff(c_63577,plain,
! [W2_549] :
( ( sdtasdt0(xm,xm) != sdtasdt0(W2_549,xm) )
| ( xm = W2_549 )
| ~ aNaturalNumber0(W2_549)
| ( xm = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_97,c_97,c_97,c_97,c_202,c_202,c_63169]) ).
tff(c_64241,plain,
! [W2_553] :
( ( sdtasdt0(xm,xm) != sdtasdt0(W2_553,xm) )
| ( xm = W2_553 )
| ~ aNaturalNumber0(W2_553) ),
inference(negUnitSimplification,[status(thm)],[c_103,c_63577]) ).
tff(c_64256,plain,
( ( sdtasdt0(sdtasdt0(xm,xm),xm) != sdtasdt0(xm,xm) )
| ( sdtasdt0(xm,xm) = xm ) ),
inference(resolution,[status(thm)],[c_41486,c_64241]) ).
tff(c_64343,plain,
sdtasdt0(sdtasdt0(xm,xm),xm) != sdtasdt0(xm,xm),
inference(negUnitSimplification,[status(thm)],[c_3631,c_64256]) ).
tff(c_70212,plain,
( ( sdtasdt0(xm,sdtasdt0(xm,xm)) != sdtasdt0(xm,xm) )
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[status(thm),theory(equality)],[c_499,c_64343]) ).
tff(c_70217,plain,
sdtasdt0(xm,sdtasdt0(xm,xm)) != sdtasdt0(xm,xm),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_97,c_97,c_70212]) ).
tff(c_336103,plain,
sdtasdt0(sz10,sdtasdt0(sz10,sz10)) != sdtasdt0(sz10,sz10),
inference(demodulation,[status(thm),theory(equality)],[c_336062,c_336062,c_336062,c_336062,c_336062,c_70217]) ).
tff(c_336532,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_171,c_336103]) ).
tff(c_336533,plain,
xm = sz10,
inference(splitRight,[status(thm)],[c_3629]) ).
tff(c_1072,plain,
! [W1_90,W0_91] :
( ( W1_90 = W0_91 )
| ~ sdtlseqdt0(W1_90,W0_91)
| ~ sdtlseqdt0(W0_91,W1_90)
| ~ aNaturalNumber0(W1_90)
| ~ aNaturalNumber0(W0_91) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_1082,plain,
( ( xm = sz10 )
| ~ sdtlseqdt0(xm,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[c_104,c_1072]) ).
tff(c_1092,plain,
( ( xm = sz10 )
| ~ sdtlseqdt0(xm,sz10) ),
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8,c_1082]) ).
tff(c_1143,plain,
~ sdtlseqdt0(xm,sz10),
inference(splitLeft,[status(thm)],[c_1092]) ).
tff(c_336582,plain,
~ sdtlseqdt0(sz10,sz10),
inference(demodulation,[status(thm),theory(equality)],[c_336533,c_1143]) ).
tff(c_336623,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1622,c_336582]) ).
tff(c_336624,plain,
xn = sz00,
inference(splitRight,[status(thm)],[c_1225]) ).
tff(c_336637,plain,
~ sdtlseqdt0(sz00,sdtasdt0(xm,sz00)),
inference(demodulation,[status(thm),theory(equality)],[c_336624,c_336624,c_625]) ).
tff(c_336658,plain,
~ sdtlseqdt0(sz00,sz00),
inference(demodulation,[status(thm),theory(equality)],[c_239,c_336637]) ).
tff(c_336677,plain,
~ aNaturalNumber0(sz00),
inference(resolution,[status(thm)],[c_72,c_336658]) ).
tff(c_336681,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_336677]) ).
tff(c_336682,plain,
xm = sz10,
inference(splitRight,[status(thm)],[c_1092]) ).
tff(c_336697,plain,
~ sdtlseqdt0(xn,sdtasdt0(sz10,xn)),
inference(demodulation,[status(thm),theory(equality)],[c_336682,c_625]) ).
tff(c_336713,plain,
~ sdtlseqdt0(xn,xn),
inference(demodulation,[status(thm),theory(equality)],[c_201,c_336697]) ).
tff(c_336739,plain,
~ aNaturalNumber0(xn),
inference(resolution,[status(thm)],[c_72,c_336713]) ).
tff(c_336743,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_95,c_336739]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM465+1 : TPTP v9.0.0. Released v4.0.0.
% 0.06/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.14/0.34 % Computer : n021.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 12:42:28 EDT 2025
% 0.14/0.35 % CPUTime :
% 169.54/134.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 169.54/134.68
% 169.54/134.68 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------