%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM444+6 : 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 : n023.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:55:56 PM UTC 2025
% Result : Theorem 263.64s 237.37s
% Output : CNFRefutation 263.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 3
% Syntax : Number of formulae : 144 ( 52 unt; 0 typ; 1 def)
% Number of atoms : 458 ( 74 equ)
% Maximal formula atoms : 92 ( 3 avg)
% Number of connectives : 498 ( 184 ~; 231 |; 56 &)
% ( 4 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 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 : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 41 ( 41 usr; 7 con; 0-3 aty)
% Number of variables : 114 ( 102 !; 12 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sdteqdtlpzmzozddtrp0 > aSubsetOf0 > aElementOf0 > aDivisorOf0 > isPrime0 > isOpen0 > isFinite0 > isClosed0 > aSet0 > aInteger0 > szAzrzSzezqlpdtcmdtrp0 > sdtslmnbsdt0 > sdtpldt0 > sdtbsmnsldt0 > sdtasdt0 > #nlpp > stldt0 > smndt0 > sbsmnsldt0 > xq > xa > sz10 > sz00 > cS1395 > #skF_25 > #skF_11 > #skF_2 > #skF_18 > #skF_6 > #skF_19 > #skF_17 > #skF_22 > #skF_12 > #skF_8 > #skF_4 > #skF_3 > #skF_13 > #skF_14 > #skF_26 > #skF_28 > #skF_5 > #skF_10 > #skF_7 > #skF_23 > #skF_15 > #skF_24 > #skF_27 > #skF_21 > #skF_1 > #skF_9 > #skF_20 > #skF_16
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(aInteger0,type,
aInteger0: $i > $o ).
tff(sbsmnsldt0,type,
sbsmnsldt0: $i > $i ).
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff(xq,type,
xq: $i ).
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(stldt0,type,
stldt0: $i > $i ).
tff(sdtasdt0,type,
sdtasdt0: ( $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(aSet0,type,
aSet0: $i > $o ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff(isClosed0,type,
isClosed0: $i > $o ).
tff(xa,type,
xa: $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff(szAzrzSzezqlpdtcmdtrp0,type,
szAzrzSzezqlpdtcmdtrp0: ( $i * $i ) > $i ).
tff(sz10,type,
sz10: $i ).
tff(cS1395,type,
cS1395: $i ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff('#skF_17',type,
'#skF_17': ( $i * $i ) > $i ).
tff('#skF_22',type,
'#skF_22': ( $i * $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i * $i ) > $i ).
tff(sz00,type,
sz00: $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff('#skF_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff('#skF_26',type,
'#skF_26': $i ).
tff(sdtpldt0,type,
sdtpldt0: ( $i * $i ) > $i ).
tff(sdtslmnbsdt0,type,
sdtslmnbsdt0: ( $i * $i ) > $i ).
tff(isPrime0,type,
isPrime0: $i > $o ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff(smndt0,type,
smndt0: $i > $i ).
tff(aSubsetOf0,type,
aSubsetOf0: ( $i * $i ) > $o ).
tff(isOpen0,type,
isOpen0: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff(aElementOf0,type,
aElementOf0: ( $i * $i ) > $o ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff(sdtbsmnsldt0,type,
sdtbsmnsldt0: ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i * $i ) > $i ).
tff(isFinite0,type,
isFinite0: $i > $o ).
tff(aDivisorOf0,type,
aDivisorOf0: ( $i * $i ) > $o ).
tff('#skF_24',type,
'#skF_24': $i ).
tff('#skF_27',type,
'#skF_27': ( $i * $i ) > $i ).
tff(sdteqdtlpzmzozddtrp0,type,
sdteqdtlpzmzozddtrp0: ( $i * $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': ( $i * $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff('#skF_16',type,
'#skF_16': ( $i * $i * $i ) > $i ).
tff(f_422,hypothesis,
( aInteger0(xa)
& aInteger0(xq)
& ( xq != sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1962) ).
tff(f_633,negated_conjecture,
~ ( ! [W0,W1] :
( ( aInteger0(W0)
& aInteger0(W1) )
=> ( ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( aInteger0(W2)
& ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa)) ) )
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& sdteqdtlpzmzozddtrp0(W2,xa,xq) ) )
& ( ( aInteger0(W2)
& ( ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa)) ) )
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(W2,xa,xq) ) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
& ( ? [W2] :
( aInteger0(W2)
& ( sdtasdt0(xq,W2) = sdtpldt0(W1,smndt0(W0)) ) )
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| sdteqdtlpzmzozddtrp0(W1,W0,xq) ) )
=> ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( aInteger0(W2)
& ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa)) ) )
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& sdteqdtlpzmzozddtrp0(W2,xa,xq) ) )
& ( ( aInteger0(W2)
& ( ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa)) ) )
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(W2,xa,xq) ) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) )
=> ( ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( aInteger0(W0)
& ? [W1] :
( aInteger0(W1)
& ( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) )
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& sdteqdtlpzmzozddtrp0(W0,xa,xq) ) )
& ( ( aInteger0(W0)
& ( ? [W1] :
( aInteger0(W1)
& ( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) )
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(W0,xa,xq) ) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( ( aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) ) )
=> ( ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> aElementOf0(W0,cS1395) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395) ) ) )
& ( ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( aInteger0(W0)
& ? [W1] :
( aInteger0(W1)
& ( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) )
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& sdteqdtlpzmzozddtrp0(W0,xa,xq) ) )
& ( ( aInteger0(W0)
& ( ? [W1] :
( aInteger0(W1)
& ( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa)) ) )
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(W0,xa,xq) ) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
=> ( ( ( aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
<=> ( aInteger0(W0)
& ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
=> ? [W1] :
( aInteger0(W1)
& ( W1 != sz00 )
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> ( aInteger0(W2)
& ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) )
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )
& ( ( aInteger0(W2)
& ( ? [W3] :
( aInteger0(W3)
& ( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0)) ) )
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
| sdteqdtlpzmzozddtrp0(W2,W0,W1) ) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) ) )
=> ( ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) ) )
| isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
| isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
tff(f_351,definition,
! [W0,W1] :
( ( aInteger0(W0)
& aInteger0(W1)
& ( W1 != sz00 ) )
=> ! [W2] :
( ( W2 = szAzrzSzezqlpdtcmdtrp0(W0,W1) )
<=> ( aSet0(W2)
& ! [W3] :
( aElementOf0(W3,W2)
<=> ( aInteger0(W3)
& sdteqdtlpzmzozddtrp0(W3,W0,W1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeq) ).
tff(c_268,plain,
xq != sz00,
inference(cnfTransformation,[status(thm)],[f_422]) ).
tff(c_270,plain,
aInteger0(xq),
inference(cnfTransformation,[status(thm)],[f_422]) ).
tff(c_704,plain,
( aSet0(cS1395)
| aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_2131,plain,
aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(splitLeft,[status(thm)],[c_704]) ).
tff(c_968,plain,
! [W0_204] :
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aInteger0(W0_204)
| ~ aElementOf0(W0_204,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_5320,plain,
aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(splitLeft,[status(thm)],[c_968]) ).
tff(c_972,plain,
! [W0_203,W0_204] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| aInteger0(W0_204)
| ~ aElementOf0(W0_204,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_141772,plain,
! [W0_945] :
( aInteger0(W0_945)
| ~ aElementOf0(W0_945,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(splitLeft,[status(thm)],[c_972]) ).
tff(c_141799,plain,
aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_5320,c_141772]) ).
tff(c_732,plain,
! [W0_203,W0_208] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| ~ aElementOf0(W0_208,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_152721,plain,
! [W0_1012] :
( ~ aElementOf0(W0_1012,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_1012,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(splitLeft,[status(thm)],[c_732]) ).
tff(c_152765,plain,
~ aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(resolution,[status(thm)],[c_2131,c_152721]) ).
tff(c_762,plain,
! [W0_203,W0_208] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| aInteger0(W0_208)
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_142493,plain,
! [W0_955] :
( aInteger0(W0_955)
| ~ aElementOf0(W0_955,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(splitLeft,[status(thm)],[c_762]) ).
tff(c_142532,plain,
aInteger0('#skF_26'),
inference(resolution,[status(thm)],[c_2131,c_142493]) ).
tff(c_402,plain,
! [W0_203,W1_222] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_149371,plain,
! [W1_989] :
( aElementOf0('#skF_28'(W1_989),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_989))
| ( sz00 = W1_989 )
| ~ aInteger0(W1_989) ),
inference(splitLeft,[status(thm)],[c_402]) ).
tff(c_228,plain,
! [W3_156,W0_146,W1_147] :
( aInteger0(W3_156)
| ~ aElementOf0(W3_156,szAzrzSzezqlpdtcmdtrp0(W0_146,W1_147))
| ( sz00 = W1_147 )
| ~ aInteger0(W1_147)
| ~ aInteger0(W0_146) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_149374,plain,
! [W1_989] :
( aInteger0('#skF_28'(W1_989))
| ~ aInteger0('#skF_26')
| ( sz00 = W1_989 )
| ~ aInteger0(W1_989) ),
inference(resolution,[status(thm)],[c_149371,c_228]) ).
tff(c_149381,plain,
! [W1_989] :
( aInteger0('#skF_28'(W1_989))
| ( sz00 = W1_989 )
| ~ aInteger0(W1_989) ),
inference(demodulation,[status(thm),theory(equality)],[c_142532,c_149374]) ).
tff(c_149323,plain,
! [W1_222] :
( aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(splitLeft,[status(thm)],[c_402]) ).
tff(c_152435,plain,
! [W3_1009,W0_1010,W1_1011] :
( sdteqdtlpzmzozddtrp0(W3_1009,W0_1010,W1_1011)
| ~ aElementOf0(W3_1009,szAzrzSzezqlpdtcmdtrp0(W0_1010,W1_1011))
| ( sz00 = W1_1011 )
| ~ aInteger0(W1_1011)
| ~ aInteger0(W0_1010) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_152441,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ~ aInteger0('#skF_26')
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(resolution,[status(thm)],[c_149323,c_152435]) ).
tff(c_152471,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_142532,c_152441]) ).
tff(c_179458,plain,
! [W0_1133,W1_1134] :
( aElementOf0(W0_1133,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_1134,W0_1133,xq)
| ~ aElementOf0(W1_1134,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W1_1134)
| ~ aInteger0(W0_1133) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_179461,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_152471,c_179458]) ).
tff(c_179471,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_142532,c_179461]) ).
tff(c_179472,plain,
( ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq)) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_152765,c_179471]) ).
tff(c_180357,plain,
~ aInteger0('#skF_28'(xq)),
inference(splitLeft,[status(thm)],[c_179472]) ).
tff(c_180360,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_149381,c_180357]) ).
tff(c_180363,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_180360]) ).
tff(c_180365,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_180363]) ).
tff(c_180367,plain,
aInteger0('#skF_28'(xq)),
inference(splitRight,[status(thm)],[c_179472]) ).
tff(c_190048,plain,
! [W0_1169,W1_1170] :
( aElementOf0(W0_1169,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_1170,W0_1169,xq)
| aElementOf0(W1_1170,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0(W1_1170)
| ~ aInteger0(W0_1169) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_190053,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_152471,c_190048]) ).
tff(c_190066,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_142532,c_180367,c_190053]) ).
tff(c_190067,plain,
aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(negUnitSimplification,[status(thm)],[c_268,c_152765,c_190066]) ).
tff(c_372,plain,
! [W0_203,W1_222] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_152127,plain,
! [W1_222] :
( ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(splitLeft,[status(thm)],[c_372]) ).
tff(c_190093,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_190067,c_152127]) ).
tff(c_190116,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_190093]) ).
tff(c_190118,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_190116]) ).
tff(c_190120,plain,
! [W0_1171] :
( aElementOf0(W0_1171,cS1395)
| ~ aInteger0(W0_1171) ),
inference(splitRight,[status(thm)],[c_732]) ).
tff(c_966,plain,
! [W0_204] :
( ~ aElementOf0('#skF_24',cS1395)
| aInteger0(W0_204)
| ~ aElementOf0(W0_204,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_2878,plain,
~ aElementOf0('#skF_24',cS1395),
inference(splitLeft,[status(thm)],[c_966]) ).
tff(c_190134,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_190120,c_2878]) ).
tff(c_190146,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_141799,c_190134]) ).
tff(c_190148,plain,
! [W0_1172] :
( aElementOf0(W0_1172,cS1395)
| ~ aInteger0(W0_1172) ),
inference(splitRight,[status(thm)],[c_372]) ).
tff(c_190162,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_190148,c_2878]) ).
tff(c_190174,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_141799,c_190162]) ).
tff(c_190176,plain,
! [W0_1173] :
( aElementOf0(W0_1173,cS1395)
| ~ aInteger0(W0_1173) ),
inference(splitRight,[status(thm)],[c_402]) ).
tff(c_190190,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_190176,c_2878]) ).
tff(c_190202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_141799,c_190190]) ).
tff(c_190204,plain,
! [W0_1174] :
( aElementOf0(W0_1174,cS1395)
| ~ aInteger0(W0_1174) ),
inference(splitRight,[status(thm)],[c_762]) ).
tff(c_190218,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_190204,c_2878]) ).
tff(c_190230,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_141799,c_190218]) ).
tff(c_190294,plain,
! [W0_1175] :
( aElementOf0(W0_1175,cS1395)
| ~ aInteger0(W0_1175) ),
inference(splitRight,[status(thm)],[c_972]) ).
tff(c_190305,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_190294,c_2878]) ).
tff(c_272,plain,
aInteger0(xa),
inference(cnfTransformation,[status(thm)],[f_422]) ).
tff(c_197978,plain,
! [W3_1245,W0_1246,W1_1247] :
( aInteger0(W3_1245)
| ~ aElementOf0(W3_1245,szAzrzSzezqlpdtcmdtrp0(W0_1246,W1_1247))
| ( sz00 = W1_1247 )
| ~ aInteger0(W1_1247)
| ~ aInteger0(W0_1246) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_197985,plain,
( aInteger0('#skF_24')
| ( xq = sz00 )
| ~ aInteger0(xq)
| ~ aInteger0(xa) ),
inference(resolution,[status(thm)],[c_5320,c_197978]) ).
tff(c_198005,plain,
( aInteger0('#skF_24')
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_272,c_270,c_197985]) ).
tff(c_198007,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_190305,c_198005]) ).
tff(c_198009,plain,
~ aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(splitRight,[status(thm)],[c_968]) ).
tff(c_728,plain,
! [W0_208] :
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_208,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_615733,plain,
! [W0_3143] :
( ~ aElementOf0(W0_3143,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_3143,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(negUnitSimplification,[status(thm)],[c_198009,c_728]) ).
tff(c_615777,plain,
~ aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(resolution,[status(thm)],[c_2131,c_615733]) ).
tff(c_758,plain,
! [W0_208] :
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aInteger0(W0_208)
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_608879,plain,
! [W0_3112] :
( aInteger0(W0_3112)
| ~ aElementOf0(W0_3112,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(negUnitSimplification,[status(thm)],[c_198009,c_758]) ).
tff(c_608923,plain,
aInteger0('#skF_26'),
inference(resolution,[status(thm)],[c_2131,c_608879]) ).
tff(c_398,plain,
! [W1_222] :
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_611550,plain,
! [W1_3125] :
( aElementOf0('#skF_28'(W1_3125),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_3125))
| ( sz00 = W1_3125 )
| ~ aInteger0(W1_3125) ),
inference(negUnitSimplification,[status(thm)],[c_198009,c_398]) ).
tff(c_611553,plain,
! [W1_3125] :
( aInteger0('#skF_28'(W1_3125))
| ~ aInteger0('#skF_26')
| ( sz00 = W1_3125 )
| ~ aInteger0(W1_3125) ),
inference(resolution,[status(thm)],[c_611550,c_228]) ).
tff(c_611560,plain,
! [W1_3125] :
( aInteger0('#skF_28'(W1_3125))
| ( sz00 = W1_3125 )
| ~ aInteger0(W1_3125) ),
inference(demodulation,[status(thm),theory(equality)],[c_608923,c_611553]) ).
tff(c_611549,plain,
! [W1_222] :
( aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(negUnitSimplification,[status(thm)],[c_198009,c_398]) ).
tff(c_615259,plain,
! [W3_3135,W0_3136,W1_3137] :
( sdteqdtlpzmzozddtrp0(W3_3135,W0_3136,W1_3137)
| ~ aElementOf0(W3_3135,szAzrzSzezqlpdtcmdtrp0(W0_3136,W1_3137))
| ( sz00 = W1_3137 )
| ~ aInteger0(W1_3137)
| ~ aInteger0(W0_3136) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_615262,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ~ aInteger0('#skF_26')
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(resolution,[status(thm)],[c_611549,c_615259]) ).
tff(c_615285,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_608923,c_615262]) ).
tff(c_643329,plain,
! [W0_3274,W1_3275] :
( aElementOf0(W0_3274,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_3275,W0_3274,xq)
| ~ aElementOf0(W1_3275,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W1_3275)
| ~ aInteger0(W0_3274) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_643334,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_615285,c_643329]) ).
tff(c_643343,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_608923,c_643334]) ).
tff(c_643344,plain,
( ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq)) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_615777,c_643343]) ).
tff(c_643600,plain,
~ aInteger0('#skF_28'(xq)),
inference(splitLeft,[status(thm)],[c_643344]) ).
tff(c_643603,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_611560,c_643600]) ).
tff(c_643606,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_643603]) ).
tff(c_643608,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_643606]) ).
tff(c_643610,plain,
aInteger0('#skF_28'(xq)),
inference(splitRight,[status(thm)],[c_643344]) ).
tff(c_653943,plain,
! [W0_3308,W1_3309] :
( aElementOf0(W0_3308,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_3309,W0_3308,xq)
| aElementOf0(W1_3309,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0(W1_3309)
| ~ aInteger0(W0_3308) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_653948,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_615285,c_653943]) ).
tff(c_653957,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_608923,c_643610,c_653948]) ).
tff(c_653958,plain,
aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(negUnitSimplification,[status(thm)],[c_268,c_615777,c_653957]) ).
tff(c_368,plain,
! [W1_222] :
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_618364,plain,
! [W1_222] :
( ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(negUnitSimplification,[status(thm)],[c_198009,c_368]) ).
tff(c_653969,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_653958,c_618364]) ).
tff(c_653994,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_653969]) ).
tff(c_653996,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_653994]) ).
tff(c_653998,plain,
aElementOf0('#skF_24',cS1395),
inference(splitRight,[status(thm)],[c_966]) ).
tff(c_726,plain,
! [W0_208] :
( ~ aElementOf0('#skF_24',cS1395)
| ~ aElementOf0(W0_208,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_664241,plain,
! [W0_3395] :
( ~ aElementOf0(W0_3395,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0(W0_3395,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(demodulation,[status(thm),theory(equality)],[c_653998,c_726]) ).
tff(c_664285,plain,
~ aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(resolution,[status(thm)],[c_2131,c_664241]) ).
tff(c_756,plain,
! [W0_208] :
( ~ aElementOf0('#skF_24',cS1395)
| aInteger0(W0_208)
| ~ aElementOf0(W0_208,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_655614,plain,
! [W0_3331] :
( aInteger0(W0_3331)
| ~ aElementOf0(W0_3331,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(demodulation,[status(thm),theory(equality)],[c_653998,c_756]) ).
tff(c_655646,plain,
aInteger0('#skF_26'),
inference(resolution,[status(thm)],[c_2131,c_655614]) ).
tff(c_396,plain,
! [W1_222] :
( ~ aElementOf0('#skF_24',cS1395)
| aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_658107,plain,
! [W1_222] :
( aElementOf0('#skF_28'(W1_222),szAzrzSzezqlpdtcmdtrp0('#skF_26',W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_653998,c_396]) ).
tff(c_659632,plain,
! [W3_3363,W0_3364,W1_3365] :
( aInteger0(W3_3363)
| ~ aElementOf0(W3_3363,szAzrzSzezqlpdtcmdtrp0(W0_3364,W1_3365))
| ( sz00 = W1_3365 )
| ~ aInteger0(W1_3365)
| ~ aInteger0(W0_3364) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_659635,plain,
! [W1_222] :
( aInteger0('#skF_28'(W1_222))
| ~ aInteger0('#skF_26')
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(resolution,[status(thm)],[c_658107,c_659632]) ).
tff(c_659658,plain,
! [W1_222] :
( aInteger0('#skF_28'(W1_222))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_655646,c_659635]) ).
tff(c_676420,plain,
! [W3_3492,W0_3493,W1_3494] :
( sdteqdtlpzmzozddtrp0(W3_3492,W0_3493,W1_3494)
| ~ aElementOf0(W3_3492,szAzrzSzezqlpdtcmdtrp0(W0_3493,W1_3494))
| ( sz00 = W1_3494 )
| ~ aInteger0(W1_3494)
| ~ aInteger0(W0_3493) ),
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_676429,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ~ aInteger0('#skF_26')
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(resolution,[status(thm)],[c_658107,c_676420]) ).
tff(c_676460,plain,
! [W1_222] :
( sdteqdtlpzmzozddtrp0('#skF_28'(W1_222),'#skF_26',W1_222)
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_655646,c_676429]) ).
tff(c_697786,plain,
! [W0_3589,W1_3590] :
( aElementOf0(W0_3589,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_3590,W0_3589,xq)
| ~ aElementOf0(W1_3590,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W1_3590)
| ~ aInteger0(W0_3589) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_697789,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_676460,c_697786]) ).
tff(c_697797,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_655646,c_697789]) ).
tff(c_697798,plain,
( ~ aElementOf0('#skF_28'(xq),szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0('#skF_28'(xq)) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_664285,c_697797]) ).
tff(c_697814,plain,
~ aInteger0('#skF_28'(xq)),
inference(splitLeft,[status(thm)],[c_697798]) ).
tff(c_697817,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_659658,c_697814]) ).
tff(c_697820,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_697817]) ).
tff(c_697822,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_697820]) ).
tff(c_697824,plain,
aInteger0('#skF_28'(xq)),
inference(splitRight,[status(thm)],[c_697798]) ).
tff(c_710422,plain,
! [W0_3628,W1_3629] :
( aElementOf0(W0_3628,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(W1_3629,W0_3628,xq)
| aElementOf0(W1_3629,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0(W1_3629)
| ~ aInteger0(W0_3628) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_710425,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0('#skF_28'(xq))
| ~ aInteger0('#skF_26')
| ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_676460,c_710422]) ).
tff(c_710433,plain,
( aElementOf0('#skF_26',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( xq = sz00 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_270,c_655646,c_697824,c_710425]) ).
tff(c_710434,plain,
aElementOf0('#skF_28'(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(negUnitSimplification,[status(thm)],[c_268,c_664285,c_710433]) ).
tff(c_366,plain,
! [W1_222] :
( ~ aElementOf0('#skF_24',cS1395)
| ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_660635,plain,
! [W1_222] :
( ~ aElementOf0('#skF_28'(W1_222),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ( sz00 = W1_222 )
| ~ aInteger0(W1_222) ),
inference(demodulation,[status(thm),theory(equality)],[c_653998,c_366]) ).
tff(c_710451,plain,
( ( xq = sz00 )
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[c_710434,c_660635]) ).
tff(c_710474,plain,
xq = sz00,
inference(demodulation,[status(thm),theory(equality)],[c_270,c_710451]) ).
tff(c_710476,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_268,c_710474]) ).
tff(c_710478,plain,
~ aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(splitRight,[status(thm)],[c_704]) ).
tff(c_702,plain,
! [W0_203] :
( aElementOf0(W0_203,cS1395)
| ~ aInteger0(W0_203)
| aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_715458,plain,
! [W0_3700] :
( aElementOf0(W0_3700,cS1395)
| ~ aInteger0(W0_3700) ),
inference(negUnitSimplification,[status(thm)],[c_710478,c_702]) ).
tff(c_696,plain,
( ~ aElementOf0('#skF_24',cS1395)
| aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_710828,plain,
~ aElementOf0('#skF_24',cS1395),
inference(negUnitSimplification,[status(thm)],[c_710478,c_696]) ).
tff(c_715466,plain,
~ aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_715458,c_710828]) ).
tff(c_698,plain,
( aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_715683,plain,
aElementOf0('#skF_24',szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(negUnitSimplification,[status(thm)],[c_710478,c_698]) ).
tff(c_716,plain,
! [W0_199] :
( aInteger0(W0_199)
| ~ aElementOf0(W0_199,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| aElementOf0('#skF_26',stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_718917,plain,
! [W0_3728] :
( aInteger0(W0_3728)
| ~ aElementOf0(W0_3728,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(negUnitSimplification,[status(thm)],[c_710478,c_716]) ).
tff(c_718928,plain,
aInteger0('#skF_24'),
inference(resolution,[status(thm)],[c_715683,c_718917]) ).
tff(c_718950,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_715466,c_718928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM444+6 : TPTP v9.0.0. Released v4.0.0.
% 0.03/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.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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 12:29:24 EDT 2025
% 0.13/0.34 % CPUTime :
% 263.64/237.37 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 263.69/237.39
% 263.69/237.39 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------