%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM454+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 08:17:03 AM UTC 2026
% Result : Theorem 5.97s 6.30s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 17
% Syntax : Number of formulae : 217 ( 140 unt; 0 def)
% Number of atoms : 397 ( 229 equ)
% Maximal formula atoms : 26 ( 1 avg)
% Number of connectives : 285 ( 105 ~; 102 |; 60 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 120 ( 0 sgn 25 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mIntNeg,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('theBenchmark.p',mIntNeg) ).
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(m__2171,axiom,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
| ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
file('theBenchmark.p',m__2171) ).
fof(m__2232,axiom,
( aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
& aInteger0(W0) )
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(W0) ) ),
file('theBenchmark.p',m__2232) ).
fof(m__,conjecture,
( sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10)
| sdtpldt0(sz10,xp) != smndt0(sz10) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10)
| sdtpldt0(sz10,xp) != smndt0(sz10) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mIntZero,axiom,
aInteger0(sz00),
file('theBenchmark.p',mIntZero) ).
cnf(c_66,plain,
aInteger0(sz00),
inference(clausify,[status(thm)],[mIntZero]) ).
fof(mIntOne,axiom,
aInteger0(sz10),
file('theBenchmark.p',mIntOne) ).
cnf(c_67,plain,
aInteger0(sz10),
inference(clausify,[status(thm)],[mIntOne]) ).
cnf(c_68,plain,
( aInteger0(smndt0(A))
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mIntNeg]) ).
cnf(c_71,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_72,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddComm]) ).
cnf(c_73,plain,
( sdtpldt0(A,sz00) = A
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_74,plain,
( sdtpldt0(sz00,A) = A
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_75,plain,
( sdtpldt0(A,smndt0(A)) = sz00
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddNeg]) ).
cnf(c_76,plain,
( sdtpldt0(smndt0(A),A) = sz00
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mAddNeg]) ).
cnf(c_77,plain,
( sdtasdt0(sdtasdt0(A,B),C) = sdtasdt0(A,sdtasdt0(B,C))
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulAsso]) ).
cnf(c_78,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_79,plain,
( sdtasdt0(A,sz10) = A
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulOne]) ).
cnf(c_81,plain,
( sdtasdt0(A,sdtpldt0(B,C)) = sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C))
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mDistrib]) ).
cnf(c_82,plain,
( sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C)) = sdtasdt0(A,sdtpldt0(B,C))
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_81]) ).
cnf(c_83,plain,
( sdtasdt0(sdtpldt0(A,B),C) = sdtpldt0(sdtasdt0(A,C),sdtasdt0(B,C))
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mDistrib]) ).
cnf(c_84,plain,
( sdtpldt0(sdtasdt0(A,C),sdtasdt0(B,C)) = sdtasdt0(sdtpldt0(A,B),C)
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_83]) ).
cnf(c_85,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulZero]) ).
cnf(c_87,plain,
( sdtasdt0(smndt0(sz10),A) = smndt0(A)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulMinOne]) ).
cnf(c_88,plain,
( sdtasdt0(A,smndt0(sz10)) = smndt0(A)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mMulMinOne]) ).
cnf(c_89,plain,
( B = sz00
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mZeroDiv]) ).
cnf(c_90,plain,
( sz00 = B
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_89]) ).
cnf(c_285,plain,
aInteger0(xp),
inference(clausify,[status(thm)],[m__2171]) ).
cnf(c_286,plain,
xp != sz00,
inference(clausify,[status(thm)],[m__2171]) ).
fof(nnf_44,plain,
( aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
& aInteger0(W0) )
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ? [X5] :
( sdtasdt0(xp,X5) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(X5) ) ),
inference(fof_nnf,[status(thm)],[m__2232]) ).
fof(sk_m__2232,plain,
( aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& sdtasdt0(xp,sK1) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
& aInteger0(sK1)
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& sdtasdt0(xp,sK0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X5,sK0),skolemize(W0,sK1)],[nnf_44]) ).
cnf(c_305,plain,
aInteger0(sK0),
inference(split_conjunct,[status(thm)],[sk_m__2232]) ).
cnf(c_306,plain,
sdtasdt0(xp,sK0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)),
inference(split_conjunct,[status(thm)],[sk_m__2232]) ).
cnf(c_307,plain,
sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) = sdtasdt0(xp,sK0),
inference(copy,[status(thm)],[c_306]) ).
cnf(c_312,plain,
aInteger0(sK1),
inference(split_conjunct,[status(thm)],[sk_m__2232]) ).
cnf(c_313,plain,
sdtasdt0(xp,sK1) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)),
inference(split_conjunct,[status(thm)],[sk_m__2232]) ).
cnf(c_314,plain,
sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) = sdtasdt0(xp,sK1),
inference(copy,[status(thm)],[c_313]) ).
cnf(c_321,negated_conjecture,
sdtpldt0(sz10,xp) = smndt0(sz10),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_322,negated_conjecture,
sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_348,plain,
( sdtpldt0(sdtasdt0(A,A),sdtasdt0(A,B)) = sdtasdt0(A,sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_82]) ).
cnf(c_351,plain,
( sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,B)) = sdtasdt0(sdtpldt0(A,A),B)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_84]) ).
cnf(c_2832,plain,
( sz00 = A
| sz00 = A
| sdtasdt0(A,A) != sz00
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_90]) ).
cnf(c_354,plain,
( sz00 = A
| sdtasdt0(A,A) != sz00
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_2832]) ).
cnf(c_444,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(xp,sK0),
inference(paramod,[status(thm)],[c_321,c_307]) ).
cnf(c_2833,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(xp,sK1),
inference(paramod,[status(thm)],[c_322,c_314]) ).
cnf(c_2834,plain,
sdtasdt0(xp,sK0) = sdtasdt0(xp,sK1),
inference(paramod,[status(thm)],[c_444,c_2833]) ).
cnf(c_445,plain,
sdtasdt0(xp,sK1) = sdtasdt0(xp,sK0),
inference(copy,[status(thm)],[c_2834]) ).
cnf(c_457,plain,
( sdtpldt0(sdtasdt0(A,A),sdtasdt0(A,A)) = sdtasdt0(A,sdtpldt0(A,A))
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_348]) ).
cnf(c_458,plain,
( sdtpldt0(sdtasdt0(A,A),sdtasdt0(A,A)) = sdtasdt0(sdtpldt0(A,A),A)
| ~ aInteger0(A) ),
inference(factor,[status(thm)],[c_351]) ).
cnf(c_478,plain,
aInteger0(smndt0(sz10)),
inference(resolve,[status(thm)],[c_68,c_67]) ).
cnf(c_524,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(resolve,[status(thm)],[c_73,c_66]) ).
cnf(c_528,plain,
sdtpldt0(sz10,smndt0(sz10)) = sz00,
inference(resolve,[status(thm)],[c_75,c_67]) ).
cnf(c_530,plain,
sdtpldt0(smndt0(sz10),sz10) = sz00,
inference(resolve,[status(thm)],[c_76,c_67]) ).
cnf(c_2835,plain,
( sdtasdt0(A,sz10) = sdtasdt0(sz10,A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_78,c_67]) ).
cnf(c_2836,plain,
sdtasdt0(sz00,sz10) = sdtasdt0(sz10,sz00),
inference(resolve,[status(thm)],[c_2835,c_66]) ).
cnf(c_554,plain,
sdtasdt0(sz10,sz00) = sdtasdt0(sz00,sz10),
inference(copy,[status(thm)],[c_2836]) ).
cnf(c_560,plain,
sdtasdt0(sz00,sz10) = sz00,
inference(resolve,[status(thm)],[c_79,c_66]) ).
cnf(c_562,plain,
sdtasdt0(sz10,sz00) = sz00,
inference(paramod,[status(thm)],[c_560,c_554]) ).
cnf(c_596,plain,
sdtasdt0(smndt0(sz10),sz10) = smndt0(sz10),
inference(resolve,[status(thm)],[c_87,c_67]) ).
cnf(c_597,plain,
sdtasdt0(smndt0(sz10),sz00) = smndt0(sz00),
inference(resolve,[status(thm)],[c_87,c_66]) ).
cnf(c_599,plain,
sdtasdt0(sz00,smndt0(sz10)) = smndt0(sz00),
inference(resolve,[status(thm)],[c_88,c_66]) ).
cnf(c_699,plain,
sdtasdt0(xp,smndt0(sz10)) = smndt0(xp),
inference(resolve,[status(thm)],[c_285,c_88]) ).
cnf(c_700,plain,
sdtasdt0(smndt0(sz10),xp) = smndt0(xp),
inference(resolve,[status(thm)],[c_285,c_87]) ).
cnf(c_702,plain,
sdtasdt0(xp,sz00) = sz00,
inference(resolve,[status(thm)],[c_285,c_85]) ).
cnf(c_710,plain,
sdtasdt0(xp,sz10) = xp,
inference(resolve,[status(thm)],[c_285,c_79]) ).
cnf(c_717,plain,
sdtpldt0(sz00,xp) = xp,
inference(resolve,[status(thm)],[c_285,c_74]) ).
cnf(c_718,plain,
sdtpldt0(xp,sz00) = xp,
inference(resolve,[status(thm)],[c_285,c_73]) ).
cnf(c_727,plain,
aInteger0(smndt0(xp)),
inference(resolve,[status(thm)],[c_285,c_68]) ).
cnf(c_2837,plain,
( sdtpldt0(sdtasdt0(sz10,B),sdtasdt0(A,B)) = sdtasdt0(sdtpldt0(sz10,A),B)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_84,c_67]) ).
cnf(c_2838,plain,
( sdtpldt0(sdtasdt0(sz10,A),sdtasdt0(xp,A)) = sdtasdt0(sdtpldt0(sz10,xp),A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2837,c_285]) ).
cnf(c_2839,plain,
sdtpldt0(sdtasdt0(sz10,sz00),sdtasdt0(xp,sz00)) = sdtasdt0(sdtpldt0(sz10,xp),sz00),
inference(resolve,[status(thm)],[c_2838,c_66]) ).
cnf(c_2840,plain,
sdtpldt0(sz00,sdtasdt0(xp,sz00)) = sdtasdt0(sdtpldt0(sz10,xp),sz00),
inference(paramod,[status(thm)],[c_562,c_2839]) ).
cnf(c_2841,plain,
sdtpldt0(sz00,sz00) = sdtasdt0(sdtpldt0(sz10,xp),sz00),
inference(paramod,[status(thm)],[c_702,c_2840]) ).
cnf(c_2842,plain,
sz00 = sdtasdt0(sdtpldt0(sz10,xp),sz00),
inference(paramod,[status(thm)],[c_524,c_2841]) ).
cnf(c_2843,plain,
sz00 = sdtasdt0(smndt0(sz10),sz00),
inference(paramod,[status(thm)],[c_321,c_2842]) ).
cnf(c_2844,plain,
sz00 = smndt0(sz00),
inference(paramod,[status(thm)],[c_597,c_2843]) ).
cnf(c_767,plain,
smndt0(sz00) = sz00,
inference(copy,[status(thm)],[c_2844]) ).
cnf(c_2845,plain,
( sdtpldt0(A,sz10) = sdtpldt0(sz10,A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_72,c_67]) ).
cnf(c_2846,plain,
sdtpldt0(xp,sz10) = sdtpldt0(sz10,xp),
inference(resolve,[status(thm)],[c_2845,c_285]) ).
cnf(c_782,plain,
sdtpldt0(xp,sz10) = smndt0(sz10),
inference(paramod,[status(thm)],[c_321,c_2846]) ).
cnf(c_810,plain,
sdtasdt0(sz00,smndt0(sz10)) = sz00,
inference(paramod,[status(thm)],[c_767,c_599]) ).
cnf(c_903,plain,
sdtasdt0(sK0,smndt0(sz10)) = smndt0(sK0),
inference(resolve,[status(thm)],[c_305,c_88]) ).
cnf(c_904,plain,
sdtasdt0(smndt0(sz10),sK0) = smndt0(sK0),
inference(resolve,[status(thm)],[c_305,c_87]) ).
cnf(c_2847,plain,
( sdtpldt0(sdtasdt0(xp,A),sdtasdt0(xp,B)) = sdtasdt0(xp,sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_82,c_285]) ).
cnf(c_2848,plain,
( sdtpldt0(sdtasdt0(xp,sz10),sdtasdt0(xp,A)) = sdtasdt0(xp,sdtpldt0(sz10,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2847,c_67]) ).
cnf(c_2849,plain,
sdtpldt0(sdtasdt0(xp,sz10),sdtasdt0(xp,sK0)) = sdtasdt0(xp,sdtpldt0(sz10,sK0)),
inference(resolve,[status(thm)],[c_2848,c_305]) ).
cnf(c_2850,plain,
sdtpldt0(xp,sdtasdt0(xp,sK0)) = sdtasdt0(xp,sdtpldt0(sz10,sK0)),
inference(paramod,[status(thm)],[c_710,c_2849]) ).
cnf(c_1027,plain,
sdtasdt0(xp,sdtpldt0(sz10,sK0)) = sdtpldt0(xp,sdtasdt0(xp,sK0)),
inference(copy,[status(thm)],[c_2850]) ).
cnf(c_2851,plain,
( sdtasdt0(A,xp) = sdtasdt0(xp,A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_78,c_285]) ).
cnf(c_1046,plain,
sdtasdt0(sK0,xp) = sdtasdt0(xp,sK0),
inference(resolve,[status(thm)],[c_2851,c_305]) ).
cnf(c_2852,plain,
( sdtasdt0(sdtasdt0(xp,A),B) = sdtasdt0(xp,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_285]) ).
cnf(c_2853,plain,
( sdtasdt0(sdtasdt0(xp,sK0),A) = sdtasdt0(xp,sdtasdt0(sK0,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2852,c_305]) ).
cnf(c_2854,plain,
sdtasdt0(sdtasdt0(xp,sK0),xp) = sdtasdt0(xp,sdtasdt0(sK0,xp)),
inference(resolve,[status(thm)],[c_2853,c_285]) ).
cnf(c_1058,plain,
sdtasdt0(sdtasdt0(xp,sK0),xp) = sdtasdt0(xp,sdtasdt0(xp,sK0)),
inference(paramod,[status(thm)],[c_1046,c_2854]) ).
cnf(c_2855,plain,
( sdtpldt0(A,sz10) = sdtpldt0(sz10,A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_72,c_67]) ).
cnf(c_1063,plain,
sdtpldt0(sK0,sz10) = sdtpldt0(sz10,sK0),
inference(resolve,[status(thm)],[c_2855,c_305]) ).
cnf(c_1145,plain,
sdtasdt0(sK1,smndt0(sz10)) = smndt0(sK1),
inference(resolve,[status(thm)],[c_312,c_88]) ).
cnf(c_2856,plain,
( sdtasdt0(A,xp) = sdtasdt0(xp,A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_78,c_285]) ).
cnf(c_2857,plain,
sdtasdt0(sK1,xp) = sdtasdt0(xp,sK1),
inference(resolve,[status(thm)],[c_2856,c_312]) ).
cnf(c_1351,plain,
sdtasdt0(sK1,xp) = sdtasdt0(xp,sK0),
inference(paramod,[status(thm)],[c_445,c_2857]) ).
cnf(c_2858,plain,
( sz00 = xp
| sdtasdt0(xp,xp) != sz00 ),
inference(resolve,[status(thm)],[c_354,c_285]) ).
cnf(c_2859,plain,
( xp = sz00
| sdtasdt0(xp,xp) != sz00 ),
inference(copy,[status(thm)],[c_2858]) ).
cnf(c_1543,plain,
sdtasdt0(xp,xp) != sz00,
inference(resolve,[status(thm)],[c_286,c_2859]) ).
cnf(c_2860,plain,
sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(sz10)),sdtasdt0(smndt0(sz10),smndt0(sz10))) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),smndt0(sz10)),
inference(resolve,[status(thm)],[c_478,c_458]) ).
cnf(c_1691,plain,
sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(sz10)),sdtasdt0(smndt0(sz10),smndt0(sz10))) = sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)),
inference(paramod,[status(thm)],[c_444,c_2860]) ).
cnf(c_2861,plain,
sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(sz10)),sdtasdt0(smndt0(sz10),smndt0(sz10))) = sdtasdt0(smndt0(sz10),sdtpldt0(smndt0(sz10),smndt0(sz10))),
inference(resolve,[status(thm)],[c_478,c_457]) ).
cnf(c_2862,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtpldt0(smndt0(sz10),smndt0(sz10))),
inference(paramod,[status(thm)],[c_1691,c_2861]) ).
cnf(c_1692,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)),
inference(paramod,[status(thm)],[c_444,c_2862]) ).
cnf(c_2863,plain,
( sdtpldt0(sdtasdt0(smndt0(sz10),A),sdtasdt0(smndt0(sz10),A)) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_351,c_478]) ).
cnf(c_2864,plain,
sdtpldt0(sdtasdt0(smndt0(sz10),xp),sdtasdt0(smndt0(sz10),xp)) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),xp),
inference(resolve,[status(thm)],[c_2863,c_285]) ).
cnf(c_2865,plain,
sdtpldt0(smndt0(xp),sdtasdt0(smndt0(sz10),xp)) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),xp),
inference(paramod,[status(thm)],[c_700,c_2864]) ).
cnf(c_2866,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),xp),
inference(paramod,[status(thm)],[c_700,c_2865]) ).
cnf(c_2867,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtasdt0(xp,sK0),xp),
inference(paramod,[status(thm)],[c_444,c_2866]) ).
cnf(c_2868,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(xp,sdtasdt0(xp,sK0)),
inference(paramod,[status(thm)],[c_1058,c_2867]) ).
cnf(c_1798,plain,
sdtasdt0(xp,sdtasdt0(xp,sK0)) = sdtpldt0(smndt0(xp),smndt0(xp)),
inference(copy,[status(thm)],[c_2868]) ).
cnf(c_2869,plain,
( sdtpldt0(sdtasdt0(sz00,B),sdtasdt0(A,B)) = sdtasdt0(sdtpldt0(sz00,A),B)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_84,c_66]) ).
cnf(c_2870,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(xp,A)) = sdtasdt0(sdtpldt0(sz00,xp),A)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2869,c_285]) ).
cnf(c_2871,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(xp,smndt0(sz10))) = sdtasdt0(sdtpldt0(sz00,xp),smndt0(sz10)),
inference(resolve,[status(thm)],[c_2870,c_478]) ).
cnf(c_2872,plain,
sdtpldt0(sz00,sdtasdt0(xp,smndt0(sz10))) = sdtasdt0(sdtpldt0(sz00,xp),smndt0(sz10)),
inference(paramod,[status(thm)],[c_810,c_2871]) ).
cnf(c_2873,plain,
sdtpldt0(sz00,smndt0(xp)) = sdtasdt0(sdtpldt0(sz00,xp),smndt0(sz10)),
inference(paramod,[status(thm)],[c_699,c_2872]) ).
cnf(c_2874,plain,
sdtpldt0(sz00,smndt0(xp)) = sdtasdt0(xp,smndt0(sz10)),
inference(paramod,[status(thm)],[c_717,c_2873]) ).
cnf(c_1975,plain,
sdtpldt0(sz00,smndt0(xp)) = smndt0(xp),
inference(paramod,[status(thm)],[c_699,c_2874]) ).
cnf(c_2875,plain,
( sdtasdt0(sdtasdt0(sK1,A),B) = sdtasdt0(sK1,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_312]) ).
cnf(c_2876,plain,
( sdtasdt0(sdtasdt0(sK1,xp),A) = sdtasdt0(sK1,sdtasdt0(xp,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2875,c_285]) ).
cnf(c_2877,plain,
sdtasdt0(sdtasdt0(sK1,xp),smndt0(sz10)) = sdtasdt0(sK1,sdtasdt0(xp,smndt0(sz10))),
inference(resolve,[status(thm)],[c_2876,c_478]) ).
cnf(c_2878,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(sK1,sdtasdt0(xp,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1351,c_2877]) ).
cnf(c_2879,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)) = sdtasdt0(sK1,sdtasdt0(xp,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1692,c_2878]) ).
cnf(c_2011,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)) = sdtasdt0(sK1,smndt0(xp)),
inference(paramod,[status(thm)],[c_699,c_2879]) ).
cnf(c_2880,plain,
( sdtasdt0(sdtasdt0(sK0,A),B) = sdtasdt0(sK0,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_305]) ).
cnf(c_2881,plain,
( sdtasdt0(sdtasdt0(sK0,xp),A) = sdtasdt0(sK0,sdtasdt0(xp,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2880,c_285]) ).
cnf(c_2882,plain,
sdtasdt0(sdtasdt0(sK0,xp),smndt0(sz10)) = sdtasdt0(sK0,sdtasdt0(xp,smndt0(sz10))),
inference(resolve,[status(thm)],[c_2881,c_478]) ).
cnf(c_2883,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(sK0,sdtasdt0(xp,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1046,c_2882]) ).
cnf(c_2884,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)) = sdtasdt0(sK0,sdtasdt0(xp,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1692,c_2883]) ).
cnf(c_2885,plain,
sdtasdt0(sK1,smndt0(xp)) = sdtasdt0(sK0,sdtasdt0(xp,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2011,c_2884]) ).
cnf(c_2013,plain,
sdtasdt0(sK1,smndt0(xp)) = sdtasdt0(sK0,smndt0(xp)),
inference(paramod,[status(thm)],[c_699,c_2885]) ).
cnf(c_2886,plain,
( sdtasdt0(sdtasdt0(xp,A),B) = sdtasdt0(xp,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_285]) ).
cnf(c_2887,plain,
( sdtasdt0(sdtasdt0(xp,sK1),A) = sdtasdt0(xp,sdtasdt0(sK1,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2886,c_312]) ).
cnf(c_2888,plain,
sdtasdt0(sdtasdt0(xp,sK1),smndt0(sz10)) = sdtasdt0(xp,sdtasdt0(sK1,smndt0(sz10))),
inference(resolve,[status(thm)],[c_2887,c_478]) ).
cnf(c_2889,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(xp,sdtasdt0(sK1,smndt0(sz10))),
inference(paramod,[status(thm)],[c_445,c_2888]) ).
cnf(c_2890,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)) = sdtasdt0(xp,sdtasdt0(sK1,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1692,c_2889]) ).
cnf(c_2891,plain,
sdtasdt0(sK1,smndt0(xp)) = sdtasdt0(xp,sdtasdt0(sK1,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2011,c_2890]) ).
cnf(c_2892,plain,
sdtasdt0(sK0,smndt0(xp)) = sdtasdt0(xp,sdtasdt0(sK1,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2013,c_2891]) ).
cnf(c_2014,plain,
sdtasdt0(sK0,smndt0(xp)) = sdtasdt0(xp,smndt0(sK1)),
inference(paramod,[status(thm)],[c_1145,c_2892]) ).
cnf(c_2893,plain,
( sdtasdt0(sdtasdt0(xp,A),B) = sdtasdt0(xp,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_285]) ).
cnf(c_2894,plain,
( sdtasdt0(sdtasdt0(xp,sK0),A) = sdtasdt0(xp,sdtasdt0(sK0,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2893,c_305]) ).
cnf(c_2895,plain,
sdtasdt0(sdtasdt0(xp,sK0),smndt0(sz10)) = sdtasdt0(xp,sdtasdt0(sK0,smndt0(sz10))),
inference(resolve,[status(thm)],[c_2894,c_478]) ).
cnf(c_2896,plain,
sdtasdt0(smndt0(sz10),sdtasdt0(xp,sK0)) = sdtasdt0(xp,sdtasdt0(sK0,smndt0(sz10))),
inference(paramod,[status(thm)],[c_1692,c_2895]) ).
cnf(c_2897,plain,
sdtasdt0(sK1,smndt0(xp)) = sdtasdt0(xp,sdtasdt0(sK0,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2011,c_2896]) ).
cnf(c_2898,plain,
sdtasdt0(sK0,smndt0(xp)) = sdtasdt0(xp,sdtasdt0(sK0,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2013,c_2897]) ).
cnf(c_2899,plain,
sdtasdt0(xp,smndt0(sK1)) = sdtasdt0(xp,sdtasdt0(sK0,smndt0(sz10))),
inference(paramod,[status(thm)],[c_2014,c_2898]) ).
cnf(c_2015,plain,
sdtasdt0(xp,smndt0(sK1)) = sdtasdt0(xp,smndt0(sK0)),
inference(paramod,[status(thm)],[c_903,c_2899]) ).
cnf(c_2900,plain,
( sdtasdt0(sdtasdt0(xp,A),B) = sdtasdt0(xp,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_285]) ).
cnf(c_2901,plain,
( sdtasdt0(sdtasdt0(xp,smndt0(sz10)),A) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2900,c_478]) ).
cnf(c_2902,plain,
sdtasdt0(sdtasdt0(xp,smndt0(sz10)),sK0) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),sK0)),
inference(resolve,[status(thm)],[c_2901,c_305]) ).
cnf(c_2903,plain,
sdtasdt0(smndt0(xp),sK0) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),sK0)),
inference(paramod,[status(thm)],[c_699,c_2902]) ).
cnf(c_2031,plain,
sdtasdt0(smndt0(xp),sK0) = sdtasdt0(xp,smndt0(sK0)),
inference(paramod,[status(thm)],[c_904,c_2903]) ).
cnf(c_2904,plain,
( sdtasdt0(sdtasdt0(xp,A),B) = sdtasdt0(xp,sdtasdt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_77,c_285]) ).
cnf(c_2905,plain,
( sdtasdt0(sdtasdt0(xp,smndt0(sz10)),A) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2904,c_478]) ).
cnf(c_2906,plain,
sdtasdt0(sdtasdt0(xp,smndt0(sz10)),sz10) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),sz10)),
inference(resolve,[status(thm)],[c_2905,c_67]) ).
cnf(c_2907,plain,
sdtasdt0(smndt0(xp),sz10) = sdtasdt0(xp,sdtasdt0(smndt0(sz10),sz10)),
inference(paramod,[status(thm)],[c_699,c_2906]) ).
cnf(c_2908,plain,
sdtasdt0(smndt0(xp),sz10) = sdtasdt0(xp,smndt0(sz10)),
inference(paramod,[status(thm)],[c_596,c_2907]) ).
cnf(c_2032,plain,
sdtasdt0(smndt0(xp),sz10) = smndt0(xp),
inference(paramod,[status(thm)],[c_699,c_2908]) ).
cnf(c_2909,plain,
( sdtpldt0(sdtpldt0(xp,A),B) = sdtpldt0(xp,sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_71,c_285]) ).
cnf(c_2910,plain,
( sdtpldt0(sdtpldt0(xp,sz10),A) = sdtpldt0(xp,sdtpldt0(sz10,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2909,c_67]) ).
cnf(c_2911,plain,
sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)) = sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))),
inference(resolve,[status(thm)],[c_2910,c_478]) ).
cnf(c_2912,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))),
inference(paramod,[status(thm)],[c_782,c_2911]) ).
cnf(c_2913,plain,
sdtasdt0(xp,sK0) = sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))),
inference(paramod,[status(thm)],[c_444,c_2912]) ).
cnf(c_2914,plain,
sdtasdt0(xp,sK0) = sdtpldt0(xp,sz00),
inference(paramod,[status(thm)],[c_528,c_2913]) ).
cnf(c_2043,plain,
sdtasdt0(xp,sK0) = xp,
inference(paramod,[status(thm)],[c_718,c_2914]) ).
cnf(c_2915,plain,
sdtasdt0(smndt0(sz10),xp) = sdtasdt0(sK1,smndt0(xp)),
inference(paramod,[status(thm)],[c_2043,c_2011]) ).
cnf(c_2916,plain,
smndt0(xp) = sdtasdt0(sK1,smndt0(xp)),
inference(paramod,[status(thm)],[c_700,c_2915]) ).
cnf(c_2917,plain,
smndt0(xp) = sdtasdt0(sK0,smndt0(xp)),
inference(paramod,[status(thm)],[c_2013,c_2916]) ).
cnf(c_2918,plain,
smndt0(xp) = sdtasdt0(xp,smndt0(sK1)),
inference(paramod,[status(thm)],[c_2014,c_2917]) ).
cnf(c_2919,plain,
smndt0(xp) = sdtasdt0(xp,smndt0(sK0)),
inference(paramod,[status(thm)],[c_2015,c_2918]) ).
cnf(c_2112,plain,
sdtasdt0(xp,smndt0(sK0)) = smndt0(xp),
inference(copy,[status(thm)],[c_2919]) ).
cnf(c_2920,plain,
sdtasdt0(xp,xp) = sdtpldt0(smndt0(xp),smndt0(xp)),
inference(paramod,[status(thm)],[c_2043,c_1798]) ).
cnf(c_2125,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(xp,xp),
inference(copy,[status(thm)],[c_2920]) ).
cnf(c_2160,plain,
sdtasdt0(xp,sdtpldt0(sz10,sK0)) = sdtpldt0(xp,xp),
inference(paramod,[status(thm)],[c_2043,c_1027]) ).
cnf(c_2162,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = xp,
inference(paramod,[status(thm)],[c_2043,c_444]) ).
cnf(c_2196,plain,
sdtasdt0(smndt0(xp),sK0) = smndt0(xp),
inference(paramod,[status(thm)],[c_2112,c_2031]) ).
cnf(c_2431,plain,
sdtpldt0(smndt0(xp),smndt0(smndt0(xp))) = sz00,
inference(resolve,[status(thm)],[c_727,c_75]) ).
cnf(c_2921,plain,
( sdtpldt0(sdtasdt0(smndt0(xp),A),sdtasdt0(smndt0(xp),B)) = sdtasdt0(smndt0(xp),sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_82,c_727]) ).
cnf(c_2922,plain,
( sdtpldt0(sdtasdt0(smndt0(xp),sK0),sdtasdt0(smndt0(xp),A)) = sdtasdt0(smndt0(xp),sdtpldt0(sK0,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2921,c_305]) ).
cnf(c_2923,plain,
sdtpldt0(sdtasdt0(smndt0(xp),sK0),sdtasdt0(smndt0(xp),sz10)) = sdtasdt0(smndt0(xp),sdtpldt0(sK0,sz10)),
inference(resolve,[status(thm)],[c_2922,c_67]) ).
cnf(c_2924,plain,
sdtpldt0(smndt0(xp),sdtasdt0(smndt0(xp),sz10)) = sdtasdt0(smndt0(xp),sdtpldt0(sK0,sz10)),
inference(paramod,[status(thm)],[c_2196,c_2923]) ).
cnf(c_2925,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(smndt0(xp),sdtpldt0(sK0,sz10)),
inference(paramod,[status(thm)],[c_2032,c_2924]) ).
cnf(c_2926,plain,
sdtasdt0(xp,xp) = sdtasdt0(smndt0(xp),sdtpldt0(sK0,sz10)),
inference(paramod,[status(thm)],[c_2125,c_2925]) ).
cnf(c_2927,plain,
sdtasdt0(xp,xp) = sdtasdt0(smndt0(xp),sdtpldt0(sz10,sK0)),
inference(paramod,[status(thm)],[c_1063,c_2926]) ).
cnf(c_2738,plain,
sdtasdt0(smndt0(xp),sdtpldt0(sz10,sK0)) = sdtasdt0(xp,xp),
inference(copy,[status(thm)],[c_2927]) ).
cnf(c_2928,plain,
( sdtpldt0(sdtpldt0(smndt0(sz10),A),B) = sdtpldt0(smndt0(sz10),sdtpldt0(A,B))
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_71,c_478]) ).
cnf(c_2929,plain,
( sdtpldt0(sdtpldt0(smndt0(sz10),sz10),A) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,A))
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_2928,c_67]) ).
cnf(c_2930,plain,
sdtpldt0(sdtpldt0(smndt0(sz10),sz10),smndt0(xp)) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,smndt0(xp))),
inference(resolve,[status(thm)],[c_2929,c_727]) ).
cnf(c_2931,plain,
sdtpldt0(sz00,smndt0(xp)) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,smndt0(xp))),
inference(paramod,[status(thm)],[c_530,c_2930]) ).
cnf(c_2932,plain,
smndt0(xp) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,smndt0(xp))),
inference(paramod,[status(thm)],[c_1975,c_2931]) ).
cnf(c_2933,plain,
smndt0(xp) = sdtpldt0(smndt0(sz10),smndt0(sz10)),
inference(paramod,[status(thm)],[c_322,c_2932]) ).
cnf(c_2779,plain,
smndt0(xp) = xp,
inference(paramod,[status(thm)],[c_2162,c_2933]) ).
cnf(c_2934,plain,
sdtasdt0(xp,sdtpldt0(sz10,sK0)) = sdtasdt0(xp,xp),
inference(paramod,[status(thm)],[c_2779,c_2738]) ).
cnf(c_2935,plain,
sdtpldt0(xp,xp) = sdtasdt0(xp,xp),
inference(paramod,[status(thm)],[c_2160,c_2934]) ).
cnf(c_2793,plain,
sdtasdt0(xp,xp) = sdtpldt0(xp,xp),
inference(copy,[status(thm)],[c_2935]) ).
cnf(c_2936,plain,
sdtpldt0(xp,smndt0(smndt0(xp))) = sz00,
inference(paramod,[status(thm)],[c_2779,c_2431]) ).
cnf(c_2937,plain,
sdtpldt0(xp,smndt0(xp)) = sz00,
inference(paramod,[status(thm)],[c_2779,c_2936]) ).
cnf(c_2797,plain,
sdtpldt0(xp,xp) = sz00,
inference(paramod,[status(thm)],[c_2779,c_2937]) ).
cnf(c_2938,plain,
sdtpldt0(xp,xp) != sz00,
inference(paramod,[status(thm)],[c_2793,c_1543]) ).
cnf(c_2939,plain,
sz00 != sz00,
inference(paramod,[status(thm)],[c_2797,c_2938]) ).
cnf(c_2831,plain,
$false,
inference(copy,[status(thm)],[c_2939]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM454+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.39 % Computer : n015.cluster.edu
% 0.09/5.39 % Model : x86_64 x86_64
% 0.09/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.39 % Memory : 8046.5625MB
% 0.09/5.39 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Sat Sep 26 02:52:20 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.39 % Process 2952096 was started by sandbox on n015,
% 0.09/5.39 % Sat Sep 26 02:52:20 2026
% 0.09/5.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.41
% 0.14/5.41 % From the command line: assign(max_seconds, 300).
% 5.97/6.30
% 5.97/6.30 % SZS status Theorem for theBenchmark
% 5.97/6.30
% 5.97/6.30 % Proof 1 at 0.75 (+ 0.11) seconds.
% 5.97/6.30 % Length of proof is 104.
% 5.97/6.30 % Level of proof is 15.
% 5.97/6.30 % Maximum clause weight is 43.000.
% 5.97/6.30 % Given clauses 352.
% 5.97/6.30
% 5.97/6.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------