%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM435+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:52:14 AM UTC 2026
% Result : Theorem 222.87s 223.15s
% Output : Proof 223.88s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(mIntegers,axiom,
! [W0] :
( aInteger0(W0)
=> $true ),
file('theBenchmark.p',mIntegers) ).
fof(mIntZero,axiom,
aInteger0(sz00),
file('theBenchmark.p',mIntZero) ).
fof(mIntOne,axiom,
aInteger0(sz10),
file('theBenchmark.p',mIntOne) ).
fof(mIntNeg,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('theBenchmark.p',mIntNeg) ).
fof(mIntPlus,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> aInteger0(sdtpldt0(W0,W1)) ),
file('theBenchmark.p',mIntPlus) ).
fof(mIntMult,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> aInteger0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mIntMult) ).
fof(mAddAsso,axiom,
! [W0,W1,W2] :
( ( aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ),
file('theBenchmark.p',mAddAsso) ).
fof(mAddComm,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('theBenchmark.p',mAddComm) ).
fof(mAddZero,axiom,
! [W0] :
( aInteger0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('theBenchmark.p',mAddZero) ).
fof(mAddNeg,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('theBenchmark.p',mAddNeg) ).
fof(mMulAsso,axiom,
! [W0,W1,W2] :
( ( aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ),
file('theBenchmark.p',mMulAsso) ).
fof(mMulComm,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
fof(mMulOne,axiom,
! [W0] :
( aInteger0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('theBenchmark.p',mMulOne) ).
fof(mDistrib,axiom,
! [W0,W1,W2] :
( ( aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) ) ),
file('theBenchmark.p',mDistrib) ).
fof(mMulZero,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('theBenchmark.p',mMulZero) ).
fof(mMulMinOne,axiom,
! [W0] :
( aInteger0(W0)
=> ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) ) ),
file('theBenchmark.p',mMulMinOne) ).
fof(mZeroDiv,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('theBenchmark.p',mZeroDiv) ).
fof(mDivisor,definition,
! [W0] :
( aInteger0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ),
file('theBenchmark.p',mDivisor) ).
fof(mEquMod,definition,
! [W0,W1,W2] :
( ( W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ),
file('theBenchmark.p',mEquMod) ).
fof(mEquModRef,axiom,
! [W0,W1] :
( ( W1 != sz00
& aInteger0(W1)
& aInteger0(W0) )
=> sdteqdtlpzmzozddtrp0(W0,W0,W1) ),
file('theBenchmark.p',mEquModRef) ).
fof(mEquModSym,axiom,
! [W0,W1,W2] :
( ( W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
=> sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ),
file('theBenchmark.p',mEquModSym) ).
fof(mEquModTrn,axiom,
! [W0,W1,W2,W3] :
( ( aInteger0(W3)
& W2 != sz00
& aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> ( ( sdteqdtlpzmzozddtrp0(W1,W3,W2)
& sdteqdtlpzmzozddtrp0(W0,W1,W2) )
=> sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ),
file('theBenchmark.p',mEquModTrn) ).
fof(m__979,hypothesis,
( xq != sz00
& aInteger0(xq)
& xp != sz00
& aInteger0(xp)
& aInteger0(xb)
& aInteger0(xa) ),
file('theBenchmark.p',m__979) ).
fof(m__1003,hypothesis,
( sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))
& aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb)))
& ? [W0] :
( sdtasdt0(sdtasdt0(xp,xq),W0) = sdtpldt0(xa,smndt0(xb))
& aInteger0(W0) )
& sdtasdt0(xp,xq) != sz00 ),
file('theBenchmark.p',m__1003) ).
fof(m__1032,hypothesis,
( sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb))
& aInteger0(xm) ),
file('theBenchmark.p',m__1032) ).
fof(m__,conjecture,
sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)),
file('theBenchmark.p',m__) ).
fof(f_1_1,plain,
! [W0] :
( $true
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mIntegers]) ).
fof(f_1_2,plain,
! [U_0] :
( $true
| ~ aInteger0(U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_0] : ~ aInteger0(U_0)
| $true ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
! [U_0] :
( ~ aInteger0(U_0)
| $true ),
inference(definitional_conversion,[status(esa)],[f_1_3]) ).
cnf(f_1_5,plain,
( ~ aInteger0(U_0)
| $true ),
inference(clausify,[status(thm)],[f_1_4]) ).
fof(f_2_1,plain,
aInteger0(sz00),
inference(fof_nnf,[status(thm)],[mIntZero]) ).
fof(f_2_2,plain,
aInteger0(sz00),
inference(definitional_conversion,[status(esa)],[f_2_1]) ).
cnf(f_2_3,plain,
aInteger0(sz00),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
aInteger0(sz10),
inference(fof_nnf,[status(thm)],[mIntOne]) ).
fof(f_3_2,plain,
aInteger0(sz10),
inference(definitional_conversion,[status(esa)],[f_3_1]) ).
cnf(f_3_3,plain,
aInteger0(sz10),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [W0] :
( aInteger0(smndt0(W0))
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mIntNeg]) ).
fof(f_4_2,plain,
! [U_1] :
( aInteger0(smndt0(U_1))
| ~ aInteger0(U_1) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_1] :
( aInteger0(smndt0(U_1))
| ~ aInteger0(U_1) ),
inference(definitional_conversion,[status(esa)],[f_4_2]) ).
cnf(f_4_4,plain,
( aInteger0(smndt0(U_1))
| ~ aInteger0(U_1) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [W0,W1] :
( aInteger0(sdtpldt0(W0,W1))
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mIntPlus]) ).
fof(f_5_2,plain,
! [U_3,U_2] :
( aInteger0(sdtpldt0(U_3,U_2))
| ~ aInteger0(U_2)
| ~ aInteger0(U_3) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_2,U_3] :
( aInteger0(sdtpldt0(U_3,U_2))
| ~ aInteger0(U_2)
| ~ aInteger0(U_3) ),
inference(definitional_conversion,[status(esa)],[f_5_2]) ).
cnf(f_5_4,plain,
( aInteger0(sdtpldt0(U_3,U_2))
| ~ aInteger0(U_2)
| ~ aInteger0(U_3) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [W0,W1] :
( aInteger0(sdtasdt0(W0,W1))
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mIntMult]) ).
fof(f_6_2,plain,
! [U_5,U_4] :
( aInteger0(sdtasdt0(U_5,U_4))
| ~ aInteger0(U_4)
| ~ aInteger0(U_5) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_4,U_5] :
( aInteger0(sdtasdt0(U_5,U_4))
| ~ aInteger0(U_4)
| ~ aInteger0(U_5) ),
inference(definitional_conversion,[status(esa)],[f_6_2]) ).
cnf(f_6_4,plain,
( aInteger0(sdtasdt0(U_5,U_4))
| ~ aInteger0(U_4)
| ~ aInteger0(U_5) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [W0,W1,W2] :
( sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2)
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mAddAsso]) ).
fof(f_7_2,plain,
! [U_8,U_7,U_6] :
( sdtpldt0(U_8,sdtpldt0(U_7,U_6)) = sdtpldt0(sdtpldt0(U_8,U_7),U_6)
| ~ aInteger0(U_6)
| ~ aInteger0(U_7)
| ~ aInteger0(U_8) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_7,U_8,U_6] :
( sdtpldt0(U_8,sdtpldt0(U_7,U_6)) = sdtpldt0(sdtpldt0(U_8,U_7),U_6)
| ~ aInteger0(U_6)
| ~ aInteger0(U_7)
| ~ aInteger0(U_8) ),
inference(definitional_conversion,[status(esa)],[f_7_2]) ).
cnf(f_7_4,plain,
( sdtpldt0(U_8,sdtpldt0(U_7,U_6)) = sdtpldt0(sdtpldt0(U_8,U_7),U_6)
| ~ aInteger0(U_6)
| ~ aInteger0(U_7)
| ~ aInteger0(U_8) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mAddComm]) ).
fof(f_8_2,plain,
! [U_10,U_9] :
( sdtpldt0(U_10,U_9) = sdtpldt0(U_9,U_10)
| ~ aInteger0(U_9)
| ~ aInteger0(U_10) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_9,U_10] :
( sdtpldt0(U_10,U_9) = sdtpldt0(U_9,U_10)
| ~ aInteger0(U_9)
| ~ aInteger0(U_10) ),
inference(definitional_conversion,[status(esa)],[f_8_2]) ).
cnf(f_8_4,plain,
( sdtpldt0(U_10,U_9) = sdtpldt0(U_9,U_10)
| ~ aInteger0(U_9)
| ~ aInteger0(U_10) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mAddZero]) ).
fof(f_9_2,plain,
! [U_11] :
( ( U_11 = sdtpldt0(sz00,U_11)
& sdtpldt0(U_11,sz00) = U_11 )
| ~ aInteger0(U_11) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_11] :
( U_11 = sdtpldt0(sz00,U_11)
| ~ sP0(U_11) )
& ! [U_11] :
( sdtpldt0(U_11,sz00) = U_11
| ~ sP0(U_11) )
& ! [U_11] :
( sP0(U_11)
| ~ aInteger0(U_11) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_9_2]) ).
cnf(f_9_4,plain,
( sP0(U_11)
| ~ aInteger0(U_11) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( sdtpldt0(U_11,sz00) = U_11
| ~ sP0(U_11) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( U_11 = sdtpldt0(sz00,U_11)
| ~ sP0(U_11) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mAddNeg]) ).
fof(f_10_2,plain,
! [U_12] :
( ( sz00 = sdtpldt0(smndt0(U_12),U_12)
& sdtpldt0(U_12,smndt0(U_12)) = sz00 )
| ~ aInteger0(U_12) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_12] :
( sz00 = sdtpldt0(smndt0(U_12),U_12)
| ~ sP1(U_12) )
& ! [U_12] :
( sdtpldt0(U_12,smndt0(U_12)) = sz00
| ~ sP1(U_12) )
& ! [U_12] :
( sP1(U_12)
| ~ aInteger0(U_12) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1])],[f_10_2]) ).
cnf(f_10_4,plain,
( sP1(U_12)
| ~ aInteger0(U_12) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_5,plain,
( sdtpldt0(U_12,smndt0(U_12)) = sz00
| ~ sP1(U_12) ),
inference(clausify,[status(thm)],[f_10_3]) ).
cnf(f_10_6,plain,
( sz00 = sdtpldt0(smndt0(U_12),U_12)
| ~ sP1(U_12) ),
inference(clausify,[status(thm)],[f_10_3]) ).
fof(f_11_1,plain,
! [W0,W1,W2] :
( sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2)
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mMulAsso]) ).
fof(f_11_2,plain,
! [U_15,U_14,U_13] :
( sdtasdt0(U_15,sdtasdt0(U_14,U_13)) = sdtasdt0(sdtasdt0(U_15,U_14),U_13)
| ~ aInteger0(U_13)
| ~ aInteger0(U_14)
| ~ aInteger0(U_15) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
! [U_13,U_14,U_15] :
( sdtasdt0(U_15,sdtasdt0(U_14,U_13)) = sdtasdt0(sdtasdt0(U_15,U_14),U_13)
| ~ aInteger0(U_13)
| ~ aInteger0(U_14)
| ~ aInteger0(U_15) ),
inference(definitional_conversion,[status(esa)],[f_11_2]) ).
cnf(f_11_4,plain,
( sdtasdt0(U_15,sdtasdt0(U_14,U_13)) = sdtasdt0(sdtasdt0(U_15,U_14),U_13)
| ~ aInteger0(U_13)
| ~ aInteger0(U_14)
| ~ aInteger0(U_15) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mMulComm]) ).
fof(f_12_2,plain,
! [U_17,U_16] :
( sdtasdt0(U_17,U_16) = sdtasdt0(U_16,U_17)
| ~ aInteger0(U_16)
| ~ aInteger0(U_17) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_16,U_17] :
( sdtasdt0(U_17,U_16) = sdtasdt0(U_16,U_17)
| ~ aInteger0(U_16)
| ~ aInteger0(U_17) ),
inference(definitional_conversion,[status(esa)],[f_12_2]) ).
cnf(f_12_4,plain,
( sdtasdt0(U_17,U_16) = sdtasdt0(U_16,U_17)
| ~ aInteger0(U_16)
| ~ aInteger0(U_17) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mMulOne]) ).
fof(f_13_2,plain,
! [U_18] :
( ( U_18 = sdtasdt0(sz10,U_18)
& sdtasdt0(U_18,sz10) = U_18 )
| ~ aInteger0(U_18) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_18] :
( U_18 = sdtasdt0(sz10,U_18)
| ~ sP2(U_18) )
& ! [U_18] :
( sdtasdt0(U_18,sz10) = U_18
| ~ sP2(U_18) )
& ! [U_18] :
( sP2(U_18)
| ~ aInteger0(U_18) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP2])],[f_13_2]) ).
cnf(f_13_4,plain,
( sP2(U_18)
| ~ aInteger0(U_18) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( sdtasdt0(U_18,sz10) = U_18
| ~ sP2(U_18) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_6,plain,
( U_18 = sdtasdt0(sz10,U_18)
| ~ sP2(U_18) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [W0,W1,W2] :
( ( sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) )
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mDistrib]) ).
fof(f_14_2,plain,
! [U_21,U_20,U_19] :
( ( sdtasdt0(sdtpldt0(U_21,U_20),U_19) = sdtpldt0(sdtasdt0(U_21,U_19),sdtasdt0(U_20,U_19))
& sdtasdt0(U_21,sdtpldt0(U_20,U_19)) = sdtpldt0(sdtasdt0(U_21,U_20),sdtasdt0(U_21,U_19)) )
| ~ aInteger0(U_19)
| ~ aInteger0(U_20)
| ~ aInteger0(U_21) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_19,U_20,U_21] :
( sdtasdt0(sdtpldt0(U_21,U_20),U_19) = sdtpldt0(sdtasdt0(U_21,U_19),sdtasdt0(U_20,U_19))
| ~ sP3(U_19,U_20,U_21) )
& ! [U_19,U_20,U_21] :
( sdtasdt0(U_21,sdtpldt0(U_20,U_19)) = sdtpldt0(sdtasdt0(U_21,U_20),sdtasdt0(U_21,U_19))
| ~ sP3(U_19,U_20,U_21) )
& ! [U_19,U_20,U_21] :
( sP3(U_19,U_20,U_21)
| ~ aInteger0(U_19)
| ~ aInteger0(U_20)
| ~ aInteger0(U_21) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP3])],[f_14_2]) ).
cnf(f_14_4,plain,
( sP3(U_19,U_20,U_21)
| ~ aInteger0(U_19)
| ~ aInteger0(U_20)
| ~ aInteger0(U_21) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_5,plain,
( sdtasdt0(U_21,sdtpldt0(U_20,U_19)) = sdtpldt0(sdtasdt0(U_21,U_20),sdtasdt0(U_21,U_19))
| ~ sP3(U_19,U_20,U_21) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_6,plain,
( sdtasdt0(sdtpldt0(U_21,U_20),U_19) = sdtpldt0(sdtasdt0(U_21,U_19),sdtasdt0(U_20,U_19))
| ~ sP3(U_19,U_20,U_21) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mMulZero]) ).
fof(f_15_2,plain,
! [U_22] :
( ( sz00 = sdtasdt0(sz00,U_22)
& sdtasdt0(U_22,sz00) = sz00 )
| ~ aInteger0(U_22) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_22] :
( sz00 = sdtasdt0(sz00,U_22)
| ~ sP4(U_22) )
& ! [U_22] :
( sdtasdt0(U_22,sz00) = sz00
| ~ sP4(U_22) )
& ! [U_22] :
( sP4(U_22)
| ~ aInteger0(U_22) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP4])],[f_15_2]) ).
cnf(f_15_4,plain,
( sP4(U_22)
| ~ aInteger0(U_22) ),
inference(clausify,[status(thm)],[f_15_3]) ).
cnf(f_15_5,plain,
( sdtasdt0(U_22,sz00) = sz00
| ~ sP4(U_22) ),
inference(clausify,[status(thm)],[f_15_3]) ).
cnf(f_15_6,plain,
( sz00 = sdtasdt0(sz00,U_22)
| ~ sP4(U_22) ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [W0] :
( ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mMulMinOne]) ).
fof(f_16_2,plain,
! [U_23] :
( ( smndt0(U_23) = sdtasdt0(U_23,smndt0(sz10))
& sdtasdt0(smndt0(sz10),U_23) = smndt0(U_23) )
| ~ aInteger0(U_23) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_23] :
( smndt0(U_23) = sdtasdt0(U_23,smndt0(sz10))
| ~ sP5(U_23) )
& ! [U_23] :
( sdtasdt0(smndt0(sz10),U_23) = smndt0(U_23)
| ~ sP5(U_23) )
& ! [U_23] :
( sP5(U_23)
| ~ aInteger0(U_23) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5])],[f_16_2]) ).
cnf(f_16_4,plain,
( sP5(U_23)
| ~ aInteger0(U_23) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( sdtasdt0(smndt0(sz10),U_23) = smndt0(U_23)
| ~ sP5(U_23) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_6,plain,
( smndt0(U_23) = sdtasdt0(U_23,smndt0(sz10))
| ~ sP5(U_23) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mZeroDiv]) ).
fof(f_17_2,plain,
! [U_25,U_24] :
( U_24 = sz00
| U_25 = sz00
| sdtasdt0(U_25,U_24) != sz00
| ~ aInteger0(U_24)
| ~ aInteger0(U_25) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
! [U_24,U_25] :
( U_24 = sz00
| U_25 = sz00
| sdtasdt0(U_25,U_24) != sz00
| ~ aInteger0(U_24)
| ~ aInteger0(U_25) ),
inference(definitional_conversion,[status(esa)],[f_17_2]) ).
cnf(f_17_4,plain,
( U_24 = sz00
| U_25 = sz00
| sdtasdt0(U_25,U_24) != sz00
| ~ aInteger0(U_24)
| ~ aInteger0(U_25) ),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_1,plain,
! [W0] :
( ! [W1] :
( ( aDivisorOf0(W1,W0)
| ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) )
& ( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mDivisor]) ).
fof(f_18_2,plain,
! [U_29] :
( ! [U_28] :
( ( aDivisorOf0(U_28,U_29)
| ! [U_27] :
( sdtasdt0(U_28,U_27) != U_29
| ~ aInteger0(U_27) )
| U_28 = sz00
| ~ aInteger0(U_28) )
& ( ( ? [U_26] :
( sdtasdt0(U_28,U_26) = U_29
& aInteger0(U_26) )
& U_28 != sz00
& aInteger0(U_28) )
| ~ aDivisorOf0(U_28,U_29) ) )
| ~ aInteger0(U_29) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
! [U_29] :
( ( ! [U_31] :
( aDivisorOf0(U_31,U_29)
| ! [U_27] :
( sdtasdt0(U_31,U_27) != U_29
| ~ aInteger0(U_27) )
| U_31 = sz00
| ~ aInteger0(U_31) )
& ! [U_30] :
( ( ? [U_26] :
( sdtasdt0(U_30,U_26) = U_29
& aInteger0(U_26) )
& U_30 != sz00
& aInteger0(U_30) )
| ~ aDivisorOf0(U_30,U_29) ) )
| ~ aInteger0(U_29) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
! [U_29] :
( ( ! [U_31] :
( aDivisorOf0(U_31,U_29)
| ! [U_27] :
( sdtasdt0(U_31,U_27) != U_29
| ~ aInteger0(U_27) )
| U_31 = sz00
| ~ aInteger0(U_31) )
& ! [U_30] :
( ( sdtasdt0(U_30,sK1(U_29,U_30)) = U_29
& aInteger0(sK1(U_29,U_30))
& U_30 != sz00
& aInteger0(U_30) )
| ~ aDivisorOf0(U_30,U_29) ) )
| ~ aInteger0(U_29) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_26,sK1(U_29,U_30))],[f_18_3]) ).
fof(f_18_5,plain,
( ! [U_29,U_30] :
( sdtasdt0(U_30,sK1(U_29,U_30)) = U_29
| ~ sP6(U_29,U_30) )
& ! [U_29,U_30] :
( aInteger0(sK1(U_29,U_30))
| ~ sP6(U_29,U_30) )
& ! [U_29,U_30] :
( U_30 != sz00
| ~ sP6(U_29,U_30) )
& ! [U_29,U_30] :
( aInteger0(U_30)
| ~ sP6(U_29,U_30) )
& ! [U_27,U_29,U_30,U_31] :
( aDivisorOf0(U_31,U_29)
| sdtasdt0(U_31,U_27) != U_29
| ~ aInteger0(U_27)
| U_31 = sz00
| ~ aInteger0(U_31)
| ~ sP7(U_27,U_29,U_30,U_31) )
& ! [U_27,U_29,U_30,U_31] :
( sP6(U_29,U_30)
| ~ aDivisorOf0(U_30,U_29)
| ~ sP7(U_27,U_29,U_30,U_31) )
& ! [U_27,U_29,U_30,U_31] :
( sP7(U_27,U_29,U_30,U_31)
| ~ aInteger0(U_29) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP6,sP7])],[f_18_4]) ).
cnf(f_18_6,plain,
( sP7(U_27,U_29,U_30,U_31)
| ~ aInteger0(U_29) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_7,plain,
( sP6(U_29,U_30)
| ~ aDivisorOf0(U_30,U_29)
| ~ sP7(U_27,U_29,U_30,U_31) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_8,plain,
( aDivisorOf0(U_31,U_29)
| sdtasdt0(U_31,U_27) != U_29
| ~ aInteger0(U_27)
| U_31 = sz00
| ~ aInteger0(U_31)
| ~ sP7(U_27,U_29,U_30,U_31) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_9,plain,
( aInteger0(U_30)
| ~ sP6(U_29,U_30) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_10,plain,
( U_30 != sz00
| ~ sP6(U_29,U_30) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_11,plain,
( aInteger0(sK1(U_29,U_30))
| ~ sP6(U_29,U_30) ),
inference(clausify,[status(thm)],[f_18_5]) ).
cnf(f_18_12,plain,
( sdtasdt0(U_30,sK1(U_29,U_30)) = U_29
| ~ sP6(U_29,U_30) ),
inference(clausify,[status(thm)],[f_18_5]) ).
fof(f_19_1,plain,
! [W0,W1,W2] :
( ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
| ~ aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) )
& ( aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1)))
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2) ) )
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquMod]) ).
fof(f_19_2,plain,
! [U_34,U_33,U_32] :
( ( ( sdteqdtlpzmzozddtrp0(U_34,U_33,U_32)
| ~ aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33))) )
& ( aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33)))
| ~ sdteqdtlpzmzozddtrp0(U_34,U_33,U_32) ) )
| U_32 = sz00
| ~ aInteger0(U_32)
| ~ aInteger0(U_33)
| ~ aInteger0(U_34) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_33,U_32,U_34] :
( sdteqdtlpzmzozddtrp0(U_34,U_33,U_32)
| ~ aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33)))
| ~ sP8(U_33,U_32,U_34) )
& ! [U_33,U_32,U_34] :
( aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33)))
| ~ sdteqdtlpzmzozddtrp0(U_34,U_33,U_32)
| ~ sP8(U_33,U_32,U_34) )
& ! [U_33,U_32,U_34] :
( sP8(U_33,U_32,U_34)
| U_32 = sz00
| ~ aInteger0(U_32)
| ~ aInteger0(U_33)
| ~ aInteger0(U_34) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP8])],[f_19_2]) ).
cnf(f_19_4,plain,
( sP8(U_33,U_32,U_34)
| U_32 = sz00
| ~ aInteger0(U_32)
| ~ aInteger0(U_33)
| ~ aInteger0(U_34) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33)))
| ~ sdteqdtlpzmzozddtrp0(U_34,U_33,U_32)
| ~ sP8(U_33,U_32,U_34) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_6,plain,
( sdteqdtlpzmzozddtrp0(U_34,U_33,U_32)
| ~ aDivisorOf0(U_32,sdtpldt0(U_34,smndt0(U_33)))
| ~ sP8(U_33,U_32,U_34) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [W0,W1] :
( sdteqdtlpzmzozddtrp0(W0,W0,W1)
| W1 = sz00
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquModRef]) ).
fof(f_20_2,plain,
! [U_36,U_35] :
( sdteqdtlpzmzozddtrp0(U_36,U_36,U_35)
| U_35 = sz00
| ~ aInteger0(U_35)
| ~ aInteger0(U_36) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
! [U_36,U_35] :
( sdteqdtlpzmzozddtrp0(U_36,U_36,U_35)
| U_35 = sz00
| ~ aInteger0(U_35)
| ~ aInteger0(U_36) ),
inference(definitional_conversion,[status(esa)],[f_20_2]) ).
cnf(f_20_4,plain,
( sdteqdtlpzmzozddtrp0(U_36,U_36,U_35)
| U_35 = sz00
| ~ aInteger0(U_35)
| ~ aInteger0(U_36) ),
inference(clausify,[status(thm)],[f_20_3]) ).
fof(f_21_1,plain,
! [W0,W1,W2] :
( sdteqdtlpzmzozddtrp0(W1,W0,W2)
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2)
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquModSym]) ).
fof(f_21_2,plain,
! [U_39,U_38,U_37] :
( sdteqdtlpzmzozddtrp0(U_38,U_39,U_37)
| ~ sdteqdtlpzmzozddtrp0(U_39,U_38,U_37)
| U_37 = sz00
| ~ aInteger0(U_37)
| ~ aInteger0(U_38)
| ~ aInteger0(U_39) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
! [U_39,U_38,U_37] :
( sdteqdtlpzmzozddtrp0(U_38,U_39,U_37)
| ~ sdteqdtlpzmzozddtrp0(U_39,U_38,U_37)
| U_37 = sz00
| ~ aInteger0(U_37)
| ~ aInteger0(U_38)
| ~ aInteger0(U_39) ),
inference(definitional_conversion,[status(esa)],[f_21_2]) ).
cnf(f_21_4,plain,
( sdteqdtlpzmzozddtrp0(U_38,U_39,U_37)
| ~ sdteqdtlpzmzozddtrp0(U_39,U_38,U_37)
| U_37 = sz00
| ~ aInteger0(U_37)
| ~ aInteger0(U_38)
| ~ aInteger0(U_39) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [W0,W1,W2,W3] :
( sdteqdtlpzmzozddtrp0(W0,W3,W2)
| ~ sdteqdtlpzmzozddtrp0(W1,W3,W2)
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2)
| ~ aInteger0(W3)
| W2 = sz00
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(fof_nnf,[status(thm)],[mEquModTrn]) ).
fof(f_22_2,plain,
! [U_43,U_42,U_41,U_40] :
( sdteqdtlpzmzozddtrp0(U_43,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_42,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_43,U_42,U_41)
| ~ aInteger0(U_40)
| U_41 = sz00
| ~ aInteger0(U_41)
| ~ aInteger0(U_42)
| ~ aInteger0(U_43) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
! [U_40,U_42,U_41,U_43] :
( sdteqdtlpzmzozddtrp0(U_43,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_42,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_43,U_42,U_41)
| ~ aInteger0(U_40)
| U_41 = sz00
| ~ aInteger0(U_41)
| ~ aInteger0(U_42)
| ~ aInteger0(U_43) ),
inference(definitional_conversion,[status(esa)],[f_22_2]) ).
cnf(f_22_4,plain,
( sdteqdtlpzmzozddtrp0(U_43,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_42,U_40,U_41)
| ~ sdteqdtlpzmzozddtrp0(U_43,U_42,U_41)
| ~ aInteger0(U_40)
| U_41 = sz00
| ~ aInteger0(U_41)
| ~ aInteger0(U_42)
| ~ aInteger0(U_43) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
( xq != sz00
& aInteger0(xq)
& xp != sz00
& aInteger0(xp)
& aInteger0(xb)
& aInteger0(xa) ),
inference(fof_nnf,[status(thm)],[m__979]) ).
fof(f_23_2,plain,
( xq != sz00
& aInteger0(xq)
& xp != sz00
& aInteger0(xp)
& aInteger0(xb)
& aInteger0(xa) ),
inference(definitional_conversion,[status(esa)],[f_23_1]) ).
cnf(f_23_3,plain,
aInteger0(xa),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_4,plain,
aInteger0(xb),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_5,plain,
aInteger0(xp),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_6,plain,
xp != sz00,
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_7,plain,
aInteger0(xq),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_8,plain,
xq != sz00,
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
( sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))
& aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb)))
& ? [W0] :
( sdtasdt0(sdtasdt0(xp,xq),W0) = sdtpldt0(xa,smndt0(xb))
& aInteger0(W0) )
& sdtasdt0(xp,xq) != sz00 ),
inference(fof_nnf,[status(thm)],[m__1003]) ).
fof(f_24_2,plain,
( sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))
& aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb)))
& ? [U_44] :
( sdtasdt0(sdtasdt0(xp,xq),U_44) = sdtpldt0(xa,smndt0(xb))
& aInteger0(U_44) )
& sdtasdt0(xp,xq) != sz00 ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))
& aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb)))
& sdtasdt0(sdtasdt0(xp,xq),sK2) = sdtpldt0(xa,smndt0(xb))
& aInteger0(sK2)
& sdtasdt0(xp,xq) != sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_44,sK2)],[f_24_2]) ).
fof(f_24_4,plain,
( sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))
& aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb)))
& sdtasdt0(sdtasdt0(xp,xq),sK2) = sdtpldt0(xa,smndt0(xb))
& aInteger0(sK2)
& sdtasdt0(xp,xq) != sz00 ),
inference(definitional_conversion,[status(esa)],[f_24_3]) ).
cnf(f_24_5,plain,
sdtasdt0(xp,xq) != sz00,
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_6,plain,
aInteger0(sK2),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_7,plain,
sdtasdt0(sdtasdt0(xp,xq),sK2) = sdtpldt0(xa,smndt0(xb)),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_8,plain,
aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb))),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_9,plain,
sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq)),
inference(clausify,[status(thm)],[f_24_4]) ).
fof(f_25_1,plain,
( sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb))
& aInteger0(xm) ),
inference(fof_nnf,[status(thm)],[m__1032]) ).
fof(f_25_2,plain,
( sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb))
& aInteger0(xm) ),
inference(definitional_conversion,[status(esa)],[f_25_1]) ).
cnf(f_25_3,plain,
aInteger0(xm),
inference(clausify,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb)),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,negated_conjecture,
sdtpldt0(xa,smndt0(xb)) != sdtasdt0(xq,sdtasdt0(xp,xm)),
inference(negate,[status(cth)],[m__]) ).
fof(f_26_2,negated_conjecture,
sdtpldt0(xa,smndt0(xb)) != sdtasdt0(xq,sdtasdt0(xp,xm)),
inference(definitional_conversion,[status(esa)],[f_26_1]) ).
cnf(f_26_3,negated_conjecture,
sdtpldt0(xa,smndt0(xb)) != sdtasdt0(xq,sdtasdt0(xp,xm)),
inference(clausify,[status(thm)],[f_26_2]) ).
cnf(f_1_5_true,plain,
$true,
inference(clause_is_true,[status(thm)],[f_1_5]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( smndt0(Eq_x_0) = smndt0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sdtpldt0(Eq_x_0,Eq_x_1) = sdtpldt0(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sdtasdt0(Eq_x_0,Eq_x_1) = sdtasdt0(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK1(Eq_x_0,Eq_x_1) = sK1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( aInteger0(Eq_y_0)
| ~ aInteger0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( aDivisorOf0(Eq_y_0,Eq_y_1)
| ~ aDivisorOf0(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( sdteqdtlpzmzozddtrp0(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sdteqdtlpzmzozddtrp0(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( sP0(Eq_y_0)
| ~ sP0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( sP1(Eq_y_0)
| ~ sP1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( sP2(Eq_y_0)
| ~ sP2(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( sP3(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP3(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( sP4(Eq_y_0)
| ~ sP4(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( sP5(Eq_y_0)
| ~ sP5(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( sP6(Eq_y_0,Eq_y_1)
| ~ sP6(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( sP7(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP7(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( sP8(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP8(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM435+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 18:25:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 222.87/223.15 % SZS status Theorem for theBenchmark
% 222.87/223.15 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------