%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG082+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:26:35 AM UTC 2026
% Result : Theorem 0.22s 5.90s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 14
% Syntax : Number of formulae : 159 ( 98 unt; 0 def)
% Number of atoms : 259 ( 142 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 182 ( 82 ~; 78 |; 12 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 96 ( 0 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsU,axiom,
! [W0] :
( aElement0(W0)
=> aElement0(smndt0(W0)) ),
file('theBenchmark.p',mSortsU) ).
fof(mSortsB,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtpldt0(W0,W1)) ),
file('theBenchmark.p',mSortsB) ).
fof(mSortsB_02,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mSortsB_02) ).
fof(mAddComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('theBenchmark.p',mAddComm) ).
fof(mAddAsso,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ),
file('theBenchmark.p',mAddAsso) ).
fof(mAddZero,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('theBenchmark.p',mAddZero) ).
fof(mAddInvr,axiom,
! [W0] :
( aElement0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('theBenchmark.p',mAddInvr) ).
fof(mMulComm,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
fof(mMulUnit,axiom,
! [W0] :
( aElement0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('theBenchmark.p',mMulUnit) ).
fof(mAMDistr,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ( sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) ) ),
file('theBenchmark.p',mAMDistr) ).
fof(m__,conjecture,
sdtasdt0(smndt0(sz10),xx) = smndt0(xx),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
sdtasdt0(smndt0(sz10),xx) != smndt0(xx),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mSortsC,axiom,
aElement0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_14,plain,
aElement0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
fof(mSortsC_01,axiom,
aElement0(sz10),
file('theBenchmark.p',mSortsC_01) ).
cnf(c_15,plain,
aElement0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
cnf(c_16,plain,
( aElement0(smndt0(A))
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mSortsU]) ).
cnf(c_17,plain,
( aElement0(sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mSortsB]) ).
cnf(c_18,plain,
( aElement0(sdtasdt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_19,plain,
( sdtpldt0(B,A) = sdtpldt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddComm]) ).
cnf(c_20,plain,
( sdtpldt0(sdtpldt0(A,B),C) = sdtpldt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddAsso]) ).
cnf(c_21,plain,
( sdtpldt0(A,sz00) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_22,plain,
( sdtpldt0(sz00,A) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddZero]) ).
cnf(c_23,plain,
( sdtpldt0(A,smndt0(A)) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddInvr]) ).
cnf(c_24,plain,
( sdtpldt0(smndt0(A),A) = sz00
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAddInvr]) ).
cnf(c_25,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_27,plain,
( sdtasdt0(A,sz10) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulUnit]) ).
cnf(c_28,plain,
( sdtasdt0(sz10,A) = A
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mMulUnit]) ).
cnf(c_29,plain,
( sdtasdt0(A,sdtpldt0(B,C)) = sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAMDistr]) ).
cnf(c_30,plain,
( sdtpldt0(sdtasdt0(A,B),sdtasdt0(A,C)) = sdtasdt0(A,sdtpldt0(B,C))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_29]) ).
cnf(c_31,plain,
( sdtasdt0(sdtpldt0(B,C),A) = sdtpldt0(sdtasdt0(B,A),sdtasdt0(C,A))
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[mAMDistr]) ).
cnf(c_32,plain,
( sdtpldt0(sdtasdt0(B,A),sdtasdt0(C,A)) = sdtasdt0(sdtpldt0(B,C),A)
| ~ aElement0(C)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(copy,[status(thm)],[c_31]) ).
fof(m__444,axiom,
aElement0(xx),
file('theBenchmark.p',m__444) ).
cnf(c_33,plain,
aElement0(xx),
inference(clausify,[status(thm)],[m__444]) ).
cnf(c_34,negated_conjecture,
sdtasdt0(smndt0(sz10),xx) != smndt0(xx),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_35,negated_conjecture,
smndt0(xx) != sdtasdt0(smndt0(sz10),xx),
inference(copy,[status(thm)],[c_34]) ).
cnf(c_36,plain,
aElement0(smndt0(sz10)),
inference(resolve,[status(thm)],[c_16,c_15]) ).
cnf(c_1674,plain,
( aElement0(sdtpldt0(sz10,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_17,c_15]) ).
cnf(c_38,plain,
aElement0(sdtpldt0(sz10,sz10)),
inference(resolve,[status(thm)],[c_1674,c_15]) ).
cnf(c_1675,plain,
( sdtpldt0(A,sz10) = sdtpldt0(sz10,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_19,c_15]) ).
cnf(c_1676,plain,
sdtpldt0(sz00,sz10) = sdtpldt0(sz10,sz00),
inference(resolve,[status(thm)],[c_1675,c_14]) ).
cnf(c_46,plain,
sdtpldt0(sz10,sz00) = sdtpldt0(sz00,sz10),
inference(copy,[status(thm)],[c_1676]) ).
cnf(c_1677,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(resolve,[status(thm)],[c_21,c_15]) ).
cnf(c_58,plain,
sdtpldt0(sz00,sz10) = sz10,
inference(paramod,[status(thm)],[c_46,c_1677]) ).
cnf(c_59,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(resolve,[status(thm)],[c_21,c_14]) ).
cnf(c_61,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(paramod,[status(thm)],[c_58,c_46]) ).
cnf(c_63,plain,
sdtpldt0(sz10,smndt0(sz10)) = sz00,
inference(resolve,[status(thm)],[c_23,c_15]) ).
cnf(c_65,plain,
sdtpldt0(smndt0(sz10),sz10) = sz00,
inference(resolve,[status(thm)],[c_24,c_15]) ).
cnf(c_1678,plain,
( sdtasdt0(A,sz10) = sdtasdt0(sz10,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25,c_15]) ).
cnf(c_1679,plain,
sdtasdt0(sz00,sz10) = sdtasdt0(sz10,sz00),
inference(resolve,[status(thm)],[c_1678,c_14]) ).
cnf(c_67,plain,
sdtasdt0(sz10,sz00) = sdtasdt0(sz00,sz10),
inference(copy,[status(thm)],[c_1679]) ).
cnf(c_80,plain,
sdtasdt0(sz00,sz10) = sz00,
inference(resolve,[status(thm)],[c_27,c_14]) ).
cnf(c_83,plain,
sdtasdt0(sz10,sz00) = sz00,
inference(paramod,[status(thm)],[c_80,c_67]) ).
cnf(c_1680,plain,
( sdtpldt0(sdtasdt0(A,sz00),sdtasdt0(B,sz00)) = sdtasdt0(sdtpldt0(A,B),sz00)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_32,c_14]) ).
cnf(c_1681,plain,
( sdtpldt0(sdtasdt0(sz10,sz00),sdtasdt0(A,sz00)) = sdtasdt0(sdtpldt0(sz10,A),sz00)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1680,c_15]) ).
cnf(c_1682,plain,
sdtpldt0(sdtasdt0(sz10,sz00),sdtasdt0(sz10,sz00)) = sdtasdt0(sdtpldt0(sz10,sz10),sz00),
inference(resolve,[status(thm)],[c_1681,c_15]) ).
cnf(c_1683,plain,
sdtpldt0(sz00,sdtasdt0(sz10,sz00)) = sdtasdt0(sdtpldt0(sz10,sz10),sz00),
inference(paramod,[status(thm)],[c_83,c_1682]) ).
cnf(c_1684,plain,
sdtpldt0(sz00,sz00) = sdtasdt0(sdtpldt0(sz10,sz10),sz00),
inference(paramod,[status(thm)],[c_83,c_1683]) ).
cnf(c_1685,plain,
sz00 = sdtasdt0(sdtpldt0(sz10,sz10),sz00),
inference(paramod,[status(thm)],[c_59,c_1684]) ).
cnf(c_90,plain,
sdtasdt0(sdtpldt0(sz10,sz10),sz00) = sz00,
inference(copy,[status(thm)],[c_1685]) ).
cnf(c_1686,plain,
( sdtpldt0(sdtasdt0(A,xx),sdtasdt0(B,xx)) = sdtasdt0(sdtpldt0(A,B),xx)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_32,c_33]) ).
cnf(c_1687,plain,
( sdtpldt0(sdtasdt0(sz10,xx),sdtasdt0(A,xx)) = sdtasdt0(sdtpldt0(sz10,A),xx)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1686,c_15]) ).
cnf(c_1688,plain,
sdtpldt0(sdtasdt0(sz10,xx),sdtasdt0(sz00,xx)) = sdtasdt0(sdtpldt0(sz10,sz00),xx),
inference(resolve,[status(thm)],[c_1687,c_14]) ).
cnf(c_107,plain,
sdtpldt0(sdtasdt0(sz10,xx),sdtasdt0(sz00,xx)) = sdtasdt0(sz10,xx),
inference(paramod,[status(thm)],[c_61,c_1688]) ).
cnf(c_1689,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_14]) ).
cnf(c_1690,plain,
( sdtpldt0(sdtasdt0(sz00,sz10),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(sz10,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1689,c_15]) ).
cnf(c_1691,plain,
sdtpldt0(sdtasdt0(sz00,sz10),sdtasdt0(sz00,xx)) = sdtasdt0(sz00,sdtpldt0(sz10,xx)),
inference(resolve,[status(thm)],[c_1690,c_33]) ).
cnf(c_1692,plain,
sdtpldt0(sz00,sdtasdt0(sz00,xx)) = sdtasdt0(sz00,sdtpldt0(sz10,xx)),
inference(paramod,[status(thm)],[c_80,c_1691]) ).
cnf(c_117,plain,
sdtasdt0(sz00,sdtpldt0(sz10,xx)) = sdtpldt0(sz00,sdtasdt0(sz00,xx)),
inference(copy,[status(thm)],[c_1692]) ).
cnf(c_1693,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_14]) ).
cnf(c_1694,plain,
( sdtpldt0(sdtasdt0(sz00,xx),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(xx,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1693,c_33]) ).
cnf(c_1695,plain,
sdtpldt0(sdtasdt0(sz00,xx),sdtasdt0(sz00,sz10)) = sdtasdt0(sz00,sdtpldt0(xx,sz10)),
inference(resolve,[status(thm)],[c_1694,c_15]) ).
cnf(c_123,plain,
sdtpldt0(sdtasdt0(sz00,xx),sz00) = sdtasdt0(sz00,sdtpldt0(xx,sz10)),
inference(paramod,[status(thm)],[c_80,c_1695]) ).
cnf(c_1696,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_14]) ).
cnf(c_1697,plain,
( sdtpldt0(sdtasdt0(sz00,xx),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(xx,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1696,c_33]) ).
cnf(c_124,plain,
sdtpldt0(sdtasdt0(sz00,xx),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtpldt0(xx,sz00)),
inference(resolve,[status(thm)],[c_1697,c_14]) ).
cnf(c_129,plain,
sdtasdt0(sz10,xx) = xx,
inference(resolve,[status(thm)],[c_28,c_33]) ).
cnf(c_130,plain,
sdtasdt0(xx,sz10) = xx,
inference(resolve,[status(thm)],[c_27,c_33]) ).
cnf(c_1698,plain,
( sdtasdt0(A,sz00) = sdtasdt0(sz00,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25,c_14]) ).
cnf(c_144,plain,
sdtasdt0(xx,sz00) = sdtasdt0(sz00,xx),
inference(resolve,[status(thm)],[c_1698,c_33]) ).
cnf(c_145,plain,
sdtpldt0(smndt0(xx),xx) = sz00,
inference(resolve,[status(thm)],[c_24,c_33]) ).
cnf(c_147,plain,
sdtpldt0(sz00,xx) = xx,
inference(resolve,[status(thm)],[c_22,c_33]) ).
cnf(c_148,plain,
sdtpldt0(xx,sz00) = xx,
inference(resolve,[status(thm)],[c_21,c_33]) ).
cnf(c_1699,plain,
( sdtpldt0(A,sz10) = sdtpldt0(sz10,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_19,c_15]) ).
cnf(c_162,plain,
sdtpldt0(xx,sz10) = sdtpldt0(sz10,xx),
inference(resolve,[status(thm)],[c_1699,c_33]) ).
cnf(c_1700,plain,
( aElement0(sdtasdt0(sz00,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_18,c_14]) ).
cnf(c_164,plain,
aElement0(sdtasdt0(sz00,xx)),
inference(resolve,[status(thm)],[c_1700,c_33]) ).
cnf(c_167,plain,
aElement0(smndt0(xx)),
inference(resolve,[status(thm)],[c_16,c_33]) ).
cnf(c_1701,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = sdtasdt0(sz10,xx),
inference(paramod,[status(thm)],[c_129,c_107]) ).
cnf(c_173,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = xx,
inference(paramod,[status(thm)],[c_129,c_1701]) ).
cnf(c_186,plain,
sdtpldt0(sdtasdt0(sz00,xx),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,xx),
inference(paramod,[status(thm)],[c_148,c_124]) ).
cnf(c_1702,plain,
sdtpldt0(sdtasdt0(sz00,xx),sz00) = sdtasdt0(sz00,sdtpldt0(sz10,xx)),
inference(paramod,[status(thm)],[c_162,c_123]) ).
cnf(c_192,plain,
sdtpldt0(sdtasdt0(sz00,xx),sz00) = sdtpldt0(sz00,sdtasdt0(sz00,xx)),
inference(paramod,[status(thm)],[c_117,c_1702]) ).
cnf(c_1703,plain,
( sdtpldt0(sdtasdt0(A,smndt0(sz10)),sdtasdt0(B,smndt0(sz10))) = sdtasdt0(sdtpldt0(A,B),smndt0(sz10))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_32,c_36]) ).
cnf(c_1704,plain,
( sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(A,smndt0(sz10))) = sdtasdt0(sdtpldt0(sz00,A),smndt0(sz10))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1703,c_14]) ).
cnf(c_1705,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(sdtpldt0(sz00,xx),smndt0(sz10)),
inference(resolve,[status(thm)],[c_1704,c_33]) ).
cnf(c_241,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,smndt0(sz10)),
inference(paramod,[status(thm)],[c_147,c_1705]) ).
cnf(c_1706,plain,
( sdtpldt0(sdtasdt0(xx,A),sdtasdt0(xx,B)) = sdtasdt0(xx,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_33]) ).
cnf(c_1707,plain,
( sdtpldt0(sdtasdt0(xx,sz10),sdtasdt0(xx,A)) = sdtasdt0(xx,sdtpldt0(sz10,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1706,c_15]) ).
cnf(c_1708,plain,
sdtpldt0(sdtasdt0(xx,sz10),sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,sdtpldt0(sz10,smndt0(sz10))),
inference(resolve,[status(thm)],[c_1707,c_36]) ).
cnf(c_1709,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,sdtpldt0(sz10,smndt0(sz10))),
inference(paramod,[status(thm)],[c_130,c_1708]) ).
cnf(c_1710,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,sz00),
inference(paramod,[status(thm)],[c_63,c_1709]) ).
cnf(c_250,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(sz00,xx),
inference(paramod,[status(thm)],[c_144,c_1710]) ).
cnf(c_1711,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_14]) ).
cnf(c_1712,plain,
( sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(smndt0(sz10),A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1711,c_36]) ).
cnf(c_1713,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sz00,sz10)) = sdtasdt0(sz00,sdtpldt0(smndt0(sz10),sz10)),
inference(resolve,[status(thm)],[c_1712,c_15]) ).
cnf(c_1714,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sz00) = sdtasdt0(sz00,sdtpldt0(smndt0(sz10),sz10)),
inference(paramod,[status(thm)],[c_80,c_1713]) ).
cnf(c_270,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sz00) = sdtasdt0(sz00,sz00),
inference(paramod,[status(thm)],[c_65,c_1714]) ).
cnf(c_1715,plain,
( sdtpldt0(sdtasdt0(sz00,A),sdtasdt0(sz00,B)) = sdtasdt0(sz00,sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_30,c_14]) ).
cnf(c_1716,plain,
( sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sz00,A)) = sdtasdt0(sz00,sdtpldt0(smndt0(sz10),A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1715,c_36]) ).
cnf(c_271,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtpldt0(smndt0(sz10),sz00)),
inference(resolve,[status(thm)],[c_1716,c_14]) ).
cnf(c_1717,plain,
( sdtasdt0(A,xx) = sdtasdt0(xx,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25,c_33]) ).
cnf(c_312,plain,
sdtasdt0(smndt0(sz10),xx) = sdtasdt0(xx,smndt0(sz10)),
inference(resolve,[status(thm)],[c_1717,c_36]) ).
cnf(c_1718,plain,
( sdtasdt0(A,sz00) = sdtasdt0(sz00,A)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_25,c_14]) ).
cnf(c_313,plain,
sdtasdt0(smndt0(sz10),sz00) = sdtasdt0(sz00,smndt0(sz10)),
inference(resolve,[status(thm)],[c_1718,c_36]) ).
cnf(c_317,plain,
sdtpldt0(smndt0(sz10),sz00) = smndt0(sz10),
inference(resolve,[status(thm)],[c_21,c_36]) ).
cnf(c_1719,plain,
( sdtpldt0(sdtpldt0(smndt0(sz10),A),B) = sdtpldt0(smndt0(sz10),sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20,c_36]) ).
cnf(c_1720,plain,
( sdtpldt0(sdtpldt0(smndt0(sz10),sz10),A) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1719,c_15]) ).
cnf(c_1721,plain,
sdtpldt0(sdtpldt0(smndt0(sz10),sz10),sz10) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),
inference(resolve,[status(thm)],[c_1720,c_15]) ).
cnf(c_1722,plain,
sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),
inference(paramod,[status(thm)],[c_65,c_1721]) ).
cnf(c_1723,plain,
sz10 = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),
inference(paramod,[status(thm)],[c_58,c_1722]) ).
cnf(c_340,plain,
sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)) = sz10,
inference(copy,[status(thm)],[c_1723]) ).
cnf(c_1724,plain,
( aElement0(sdtasdt0(xx,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_18,c_33]) ).
cnf(c_343,plain,
aElement0(sdtasdt0(xx,smndt0(sz10))),
inference(resolve,[status(thm)],[c_1724,c_36]) ).
cnf(c_371,negated_conjecture,
smndt0(xx) != sdtasdt0(xx,smndt0(sz10)),
inference(paramod,[status(thm)],[c_312,c_35]) ).
cnf(c_382,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,smndt0(sz10)),
inference(paramod,[status(thm)],[c_317,c_271]) ).
cnf(c_772,plain,
sdtpldt0(smndt0(xx),sz00) = smndt0(xx),
inference(resolve,[status(thm)],[c_21,c_167]) ).
cnf(c_1725,plain,
( sdtpldt0(sdtasdt0(A,sz00),sdtasdt0(B,sz00)) = sdtasdt0(sdtpldt0(A,B),sz00)
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_32,c_14]) ).
cnf(c_1726,plain,
( sdtpldt0(sdtasdt0(smndt0(sz10),sz00),sdtasdt0(A,sz00)) = sdtasdt0(sdtpldt0(smndt0(sz10),A),sz00)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1725,c_36]) ).
cnf(c_1727,plain,
sdtpldt0(sdtasdt0(smndt0(sz10),sz00),sdtasdt0(sdtpldt0(sz10,sz10),sz00)) = sdtasdt0(sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),sz00),
inference(resolve,[status(thm)],[c_1726,c_38]) ).
cnf(c_1728,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sdtasdt0(sdtpldt0(sz10,sz10),sz00)) = sdtasdt0(sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),sz00),
inference(paramod,[status(thm)],[c_313,c_1727]) ).
cnf(c_1729,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sz00) = sdtasdt0(sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),sz00),
inference(paramod,[status(thm)],[c_90,c_1728]) ).
cnf(c_1730,plain,
sdtasdt0(sz00,sz00) = sdtasdt0(sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sz10)),sz00),
inference(paramod,[status(thm)],[c_270,c_1729]) ).
cnf(c_1731,plain,
sdtasdt0(sz00,sz00) = sdtasdt0(sz10,sz00),
inference(paramod,[status(thm)],[c_340,c_1730]) ).
cnf(c_951,plain,
sdtasdt0(sz00,sz00) = sz00,
inference(paramod,[status(thm)],[c_83,c_1731]) ).
cnf(c_1732,plain,
sdtpldt0(sdtasdt0(sz00,smndt0(sz10)),sz00) = sdtasdt0(sz00,smndt0(sz10)),
inference(paramod,[status(thm)],[c_951,c_382]) ).
cnf(c_1733,plain,
sdtasdt0(sz00,sz00) = sdtasdt0(sz00,smndt0(sz10)),
inference(paramod,[status(thm)],[c_270,c_1732]) ).
cnf(c_1734,plain,
sz00 = sdtasdt0(sz00,smndt0(sz10)),
inference(paramod,[status(thm)],[c_951,c_1733]) ).
cnf(c_1045,plain,
sdtasdt0(sz00,smndt0(sz10)) = sz00,
inference(copy,[status(thm)],[c_1734]) ).
cnf(c_1735,plain,
sdtpldt0(sdtasdt0(sz00,xx),sz00) = sdtasdt0(sz00,xx),
inference(paramod,[status(thm)],[c_951,c_186]) ).
cnf(c_1046,plain,
sdtpldt0(sz00,sdtasdt0(sz00,xx)) = sdtasdt0(sz00,xx),
inference(paramod,[status(thm)],[c_192,c_1735]) ).
cnf(c_1079,plain,
sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,smndt0(sz10)),
inference(paramod,[status(thm)],[c_1045,c_241]) ).
cnf(c_1736,plain,
( sdtpldt0(sdtpldt0(smndt0(xx),A),B) = sdtpldt0(smndt0(xx),sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20,c_167]) ).
cnf(c_1737,plain,
( sdtpldt0(sdtpldt0(smndt0(xx),xx),A) = sdtpldt0(smndt0(xx),sdtpldt0(xx,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1736,c_33]) ).
cnf(c_1738,plain,
sdtpldt0(sdtpldt0(smndt0(xx),xx),sdtasdt0(sz00,xx)) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(sz00,xx))),
inference(resolve,[status(thm)],[c_1737,c_164]) ).
cnf(c_1739,plain,
sdtpldt0(sz00,sdtasdt0(sz00,xx)) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(sz00,xx))),
inference(paramod,[status(thm)],[c_145,c_1738]) ).
cnf(c_1740,plain,
sdtasdt0(sz00,xx) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(sz00,xx))),
inference(paramod,[status(thm)],[c_1046,c_1739]) ).
cnf(c_1741,plain,
sdtasdt0(sz00,xx) = sdtpldt0(smndt0(xx),xx),
inference(paramod,[status(thm)],[c_173,c_1740]) ).
cnf(c_1405,plain,
sdtasdt0(sz00,xx) = sz00,
inference(paramod,[status(thm)],[c_145,c_1741]) ).
cnf(c_1429,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sz00,
inference(paramod,[status(thm)],[c_1405,c_250]) ).
cnf(c_1742,plain,
( sdtpldt0(sdtpldt0(smndt0(xx),A),B) = sdtpldt0(smndt0(xx),sdtpldt0(A,B))
| ~ aElement0(B)
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_20,c_167]) ).
cnf(c_1743,plain,
( sdtpldt0(sdtpldt0(smndt0(xx),xx),A) = sdtpldt0(smndt0(xx),sdtpldt0(xx,A))
| ~ aElement0(A) ),
inference(resolve,[status(thm)],[c_1742,c_33]) ).
cnf(c_1744,plain,
sdtpldt0(sdtpldt0(smndt0(xx),xx),sdtasdt0(xx,smndt0(sz10))) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10)))),
inference(resolve,[status(thm)],[c_1743,c_343]) ).
cnf(c_1745,plain,
sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10)))),
inference(paramod,[status(thm)],[c_145,c_1744]) ).
cnf(c_1746,plain,
sdtasdt0(xx,smndt0(sz10)) = sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10)))),
inference(paramod,[status(thm)],[c_1079,c_1745]) ).
cnf(c_1747,plain,
sdtasdt0(xx,smndt0(sz10)) = sdtpldt0(smndt0(xx),sz00),
inference(paramod,[status(thm)],[c_1429,c_1746]) ).
cnf(c_1748,plain,
sdtasdt0(xx,smndt0(sz10)) = smndt0(xx),
inference(paramod,[status(thm)],[c_772,c_1747]) ).
cnf(c_1672,plain,
smndt0(xx) = sdtasdt0(xx,smndt0(sz10)),
inference(copy,[status(thm)],[c_1748]) ).
cnf(c_1673,plain,
$false,
inference(resolve,[status(thm)],[c_1672,c_371]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG082+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.65 % Computer : n009.cluster.edu
% 0.18/5.65 % Model : x86_64 x86_64
% 0.18/5.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.65 % Memory : 8046.5625MB
% 0.18/5.65 % OS : Linux 6.8.0-71-generic
% 0.18/5.65 % CPULimit : 300
% 0.18/5.65 % WCLimit : 300
% 0.18/5.65 % DateTime : Sat Sep 26 06:01:04 UTC 2026
% 0.18/5.65 % CPUTime :
% 0.18/5.65 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.65 % Process 3516043 was started by sandbox2 on n009,
% 0.18/5.65 % Sat Sep 26 06:01:04 2026
% 0.18/5.65 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/5.66
% 0.18/5.66 % From the command line: assign(max_seconds, 300).
% 0.22/5.90
% 0.22/5.90 % SZS status Theorem for theBenchmark
% 0.22/5.90
% 0.22/5.90 % Proof 1 at 0.17 (+ 0.05) seconds.
% 0.22/5.90 % Length of proof is 80.
% 0.22/5.90 % Level of proof is 10.
% 0.22/5.90 % Maximum clause weight is 27.000.
% 0.22/5.90 % Given clauses 48.
% 0.22/5.90
% 0.22/5.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------