%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : RNG082+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:25:49 AM UTC 2026
% Result : Theorem 198.20s 29.32s
% Output : CNFRefutation 198.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 14
% Syntax : Number of formulae : 131 ( 65 unt; 0 def)
% Number of atoms : 236 ( 119 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 191 ( 86 ~; 82 |; 13 &)
% ( 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 : 97 ( 0 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsC,axiom,
aElement0(sz00) ).
fof(mSortsC_01,axiom,
aElement0(sz10) ).
fof(mSortsU,axiom,
! [X0] :
( aElement0(X0)
=> aElement0(smndt0(X0)) ) ).
fof(mSortsB_02,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aElement0(X0) )
=> aElement0(sdtasdt0(X0,X1)) ) ).
fof(mAddComm,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aElement0(X0) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ) ).
fof(mAddAsso,axiom,
! [X0,X1,X2] :
( ( aElement0(X2)
& aElement0(X1)
& aElement0(X0) )
=> sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ) ).
fof(mAddZero,axiom,
! [X0] :
( aElement0(X0)
=> ( X0 = sdtpldt0(sz00,X0)
& sdtpldt0(X0,sz00) = X0 ) ) ).
fof(mAddInvr,axiom,
! [X0] :
( aElement0(X0)
=> ( sz00 = sdtpldt0(smndt0(X0),X0)
& sdtpldt0(X0,smndt0(X0)) = sz00 ) ) ).
fof(mMulComm,axiom,
! [X0,X1] :
( ( aElement0(X1)
& aElement0(X0) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ).
fof(mMulAsso,axiom,
! [X0,X1,X2] :
( ( aElement0(X2)
& aElement0(X1)
& aElement0(X0) )
=> sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ) ).
fof(mMulUnit,axiom,
! [X0] :
( aElement0(X0)
=> ( X0 = sdtasdt0(sz10,X0)
& sdtasdt0(X0,sz10) = X0 ) ) ).
fof(mAMDistr,axiom,
! [X0,X1,X2] :
( ( aElement0(X2)
& aElement0(X1)
& aElement0(X0) )
=> ( sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
& sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ) ) ).
fof(m__444,hypothesis,
aElement0(xx) ).
fof(m__,conjecture,
sdtasdt0(smndt0(sz10),xx) = smndt0(xx) ).
fof(negated_conjecture,negated_conjecture,
sdtasdt0(smndt0(sz10),xx) != smndt0(xx),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(c0,plain,
aElement0(sz00),
inference(clausification,[status(esa)],[mSortsC]) ).
cnf(c1,plain,
aElement0(sz10),
inference(clausification,[status(esa)],[mSortsC_01]) ).
cnf(c2,plain,
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mSortsU]) ).
cnf(c4,plain,
( aElement0(sdtasdt0(X1,X0))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mSortsB_02]) ).
cnf(c5,plain,
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAddComm]) ).
cnf(c6,plain,
( sdtpldt0(X2,sdtpldt0(X0,X1)) = sdtpldt0(sdtpldt0(X2,X0),X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAddAsso]) ).
cnf(c7,plain,
( sdtpldt0(X0,sz00) = X0
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAddZero]) ).
cnf(c8,plain,
( sdtpldt0(sz00,X0) = X0
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAddZero]) ).
cnf(c10,plain,
( sdtpldt0(smndt0(X0),X0) = sz00
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAddInvr]) ).
cnf(c11,plain,
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mMulComm]) ).
cnf(c12,plain,
( sdtasdt0(X2,sdtasdt0(X0,X1)) = sdtasdt0(sdtasdt0(X2,X0),X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mMulAsso]) ).
cnf(c13,plain,
( sdtasdt0(X0,sz10) = X0
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mMulUnit]) ).
cnf(c14,plain,
( sdtasdt0(sz10,X0) = X0
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mMulUnit]) ).
cnf(c15,plain,
( sdtpldt0(sdtasdt0(X2,X0),sdtasdt0(X2,X1)) = sdtasdt0(X2,sdtpldt0(X0,X1))
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(clausification,[status(esa)],[mAMDistr]) ).
cnf(c17,plain,
aElement0(xx),
inference(clausification,[status(esa)],[m__444]) ).
cnf(c18,plain,
smndt0(xx) != sdtasdt0(smndt0(sz10),xx),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(X0),sz00) = smndt0(X0) ),
inference(resolution,[status(thm)],[c7,c2]) ).
cnf(d1,plain,
sdtpldt0(smndt0(xx),sz00) = smndt0(xx),
inference(resolution,[status(thm)],[d0,c17]) ).
cnf(d2,plain,
sdtpldt0(smndt0(xx),xx) = sz00,
inference(resolution,[status(thm)],[c10,c17]) ).
cnf(d3,plain,
sdtasdt0(xx,sz10) = xx,
inference(resolution,[status(thm)],[c13,c17]) ).
cnf(d4,plain,
sdtpldt0(sz00,sz10) = sz10,
inference(resolution,[status(thm)],[c8,c1]) ).
cnf(d5,plain,
( ~ aElement0(X0)
| sdtpldt0(xx,X0) = sdtpldt0(X0,xx) ),
inference(resolution,[status(thm)],[c5,c17]) ).
cnf(d6,plain,
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtpldt0(xx,sdtasdt0(X0,X1)) = sdtpldt0(sdtasdt0(X0,X1),xx) ),
inference(resolution,[status(thm)],[d5,c4]) ).
cnf(d7,plain,
( ~ aElement0(X0)
| sdtpldt0(xx,sdtasdt0(sz00,X0)) = sdtpldt0(sdtasdt0(sz00,X0),xx) ),
inference(resolution,[status(thm)],[d6,c0]) ).
cnf(d8,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = sdtpldt0(sdtasdt0(sz00,xx),xx),
inference(resolution,[status(thm)],[d7,c17]) ).
cnf(d9,plain,
( ~ aElement0(X0)
| sdtasdt0(sz00,X0) = sdtasdt0(X0,sz00) ),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(d10,plain,
sdtasdt0(sz00,xx) = sdtasdt0(xx,sz00),
inference(resolution,[status(thm)],[d9,c17]) ).
cnf(d11,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz10)) = sdtasdt0(X0,sdtpldt0(X1,sz10)) ),
inference(resolution,[status(thm)],[c15,c1]) ).
cnf(d12,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,X0),sdtasdt0(xx,sz10)) = sdtasdt0(xx,sdtpldt0(X0,sz10)) ),
inference(resolution,[status(thm)],[d11,c17]) ).
cnf(d13,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,X0),xx) = sdtasdt0(xx,sdtpldt0(X0,sz10)) ),
inference(demodulation,[status(thm)],[d12,d3]) ).
cnf(d14,plain,
sdtpldt0(sdtasdt0(xx,sz00),xx) = sdtasdt0(xx,sdtpldt0(sz00,sz10)),
inference(resolution,[status(thm)],[d13,c0]) ).
cnf(d15,plain,
sdtpldt0(sdtasdt0(sz00,xx),xx) = sdtasdt0(xx,sdtpldt0(sz00,sz10)),
inference(demodulation,[status(thm)],[d14,d10]) ).
cnf(d16,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = sdtasdt0(xx,sdtpldt0(sz00,sz10)),
inference(demodulation,[status(thm)],[d15,d8]) ).
cnf(d17,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = sdtasdt0(xx,sz10),
inference(demodulation,[status(thm)],[d16,d4]) ).
cnf(d18,plain,
sdtpldt0(xx,sdtasdt0(sz00,xx)) = xx,
inference(demodulation,[status(thm)],[d17,d3]) ).
cnf(d19,plain,
sdtasdt0(sz00,sz10) = sz00,
inference(resolution,[status(thm)],[c13,c0]) ).
cnf(d20,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(resolution,[status(thm)],[c7,c1]) ).
cnf(d21,plain,
( sdtpldt0(sz00,sdtasdt0(X0,X1)) = sdtasdt0(X0,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[c4,c8]) ).
cnf(d22,plain,
( ~ aElement0(X0)
| sdtpldt0(sz00,sdtasdt0(sz00,X0)) = sdtasdt0(sz00,X0) ),
inference(resolution,[status(thm)],[d21,c0]) ).
cnf(d23,plain,
sdtpldt0(sz00,sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sz00),
inference(resolution,[status(thm)],[d22,c0]) ).
cnf(d24,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz00)) = sdtasdt0(X0,sdtpldt0(X1,sz00)) ),
inference(resolution,[status(thm)],[c15,c0]) ).
cnf(d25,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(sz00,X0),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtpldt0(X0,sz00)) ),
inference(resolution,[status(thm)],[d24,c0]) ).
cnf(d26,plain,
sdtpldt0(sdtasdt0(sz00,sz10),sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtpldt0(sz10,sz00)),
inference(resolution,[status(thm)],[d25,c1]) ).
cnf(d27,plain,
sdtpldt0(sz00,sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtpldt0(sz10,sz00)),
inference(demodulation,[status(thm)],[d26,d19]) ).
cnf(d28,plain,
sdtasdt0(sz00,sz00) = sdtasdt0(sz00,sdtpldt0(sz10,sz00)),
inference(demodulation,[status(thm)],[d27,d23]) ).
cnf(d29,plain,
sdtasdt0(sz00,sz00) = sdtasdt0(sz00,sz10),
inference(demodulation,[status(thm)],[d28,d20]) ).
cnf(d30,plain,
sdtasdt0(sz00,sz00) = sz00,
inference(demodulation,[status(thm)],[d29,d19]) ).
cnf(d31,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtasdt0(sz00,sdtasdt0(X0,X1)) = sdtasdt0(sdtasdt0(sz00,X0),X1) ),
inference(resolution,[status(thm)],[c12,c0]) ).
cnf(d32,plain,
( ~ aElement0(X0)
| sdtasdt0(sz00,sdtasdt0(xx,X0)) = sdtasdt0(sdtasdt0(sz00,xx),X0) ),
inference(resolution,[status(thm)],[d31,c17]) ).
cnf(d33,plain,
sdtasdt0(sz00,sdtasdt0(xx,sz00)) = sdtasdt0(sdtasdt0(sz00,xx),sz00),
inference(resolution,[status(thm)],[d32,c0]) ).
cnf(d34,plain,
sdtasdt0(sz00,sdtasdt0(sz00,xx)) = sdtasdt0(sdtasdt0(sz00,xx),sz00),
inference(demodulation,[status(thm)],[d33,d10]) ).
cnf(d35,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtasdt0(xx,sdtasdt0(X0,X1)) = sdtasdt0(sdtasdt0(xx,X0),X1) ),
inference(resolution,[status(thm)],[c12,c17]) ).
cnf(d36,plain,
( ~ aElement0(X0)
| sdtasdt0(xx,sdtasdt0(sz00,X0)) = sdtasdt0(sdtasdt0(xx,sz00),X0) ),
inference(resolution,[status(thm)],[d35,c0]) ).
cnf(d37,plain,
( ~ aElement0(X0)
| sdtasdt0(xx,sdtasdt0(sz00,X0)) = sdtasdt0(sdtasdt0(sz00,xx),X0) ),
inference(demodulation,[status(thm)],[d36,d10]) ).
cnf(d38,plain,
sdtasdt0(xx,sdtasdt0(sz00,sz00)) = sdtasdt0(sdtasdt0(sz00,xx),sz00),
inference(resolution,[status(thm)],[d37,c0]) ).
cnf(d39,plain,
sdtasdt0(xx,sdtasdt0(sz00,sz00)) = sdtasdt0(sz00,sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d38,d34]) ).
cnf(d40,plain,
sdtasdt0(xx,sz00) = sdtasdt0(sz00,sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d39,d30]) ).
cnf(d41,plain,
sdtasdt0(sz00,xx) = sdtasdt0(sz00,sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d40,d10]) ).
cnf(d42,plain,
( ~ aElement0(X0)
| sdtasdt0(sz00,sdtasdt0(sz00,X0)) = sdtasdt0(sdtasdt0(sz00,sz00),X0) ),
inference(resolution,[status(thm)],[d31,c0]) ).
cnf(d43,plain,
sdtasdt0(sz00,sdtasdt0(sz00,xx)) = sdtasdt0(sdtasdt0(sz00,sz00),xx),
inference(resolution,[status(thm)],[d42,c17]) ).
cnf(d44,plain,
( ~ aElement0(xx)
| ~ aElement0(sdtasdt0(sz00,sz00))
| aElement0(sdtasdt0(sz00,sdtasdt0(sz00,xx))) ),
inference(superposition,[status(thm)],[d43,c4]) ).
cnf(d45,plain,
( aElement0(sdtasdt0(sz00,sdtasdt0(sz00,xx)))
| ~ aElement0(sdtasdt0(sz00,sz00)) ),
inference(resolution,[status(thm)],[c17,d44]) ).
cnf(d46,plain,
( aElement0(sdtasdt0(sz00,sdtasdt0(sz00,xx)))
| ~ aElement0(sz00) ),
inference(demodulation,[status(thm)],[d45,d30]) ).
cnf(d47,plain,
aElement0(sdtasdt0(sz00,sdtasdt0(sz00,xx))),
inference(resolution,[status(thm)],[c0,d46]) ).
cnf(d48,plain,
aElement0(sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d47,d41]) ).
cnf(d49,plain,
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtpldt0(X0,sdtpldt0(xx,X1)) = sdtpldt0(sdtpldt0(X0,xx),X1) ),
inference(resolution,[status(thm)],[c6,c17]) ).
cnf(d50,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtpldt0(smndt0(X0),sdtpldt0(xx,X1)) = sdtpldt0(sdtpldt0(smndt0(X0),xx),X1) ),
inference(resolution,[status(thm)],[d49,c2]) ).
cnf(d51,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(xx),sdtpldt0(xx,X0)) = sdtpldt0(sdtpldt0(smndt0(xx),xx),X0) ),
inference(resolution,[status(thm)],[d50,c17]) ).
cnf(d52,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(xx),sdtpldt0(xx,X0)) = sdtpldt0(sz00,X0) ),
inference(demodulation,[status(thm)],[d51,d2]) ).
cnf(d53,plain,
sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(sz00,xx))) = sdtpldt0(sz00,sdtasdt0(sz00,xx)),
inference(resolution,[status(thm)],[d52,d48]) ).
cnf(d54,plain,
sdtpldt0(smndt0(xx),xx) = sdtpldt0(sz00,sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d53,d18]) ).
cnf(d55,plain,
sz00 = sdtpldt0(sz00,sdtasdt0(sz00,xx)),
inference(demodulation,[status(thm)],[d54,d2]) ).
cnf(d56,plain,
sdtpldt0(sz00,sdtasdt0(sz00,xx)) = sdtasdt0(sz00,xx),
inference(resolution,[status(thm)],[d22,c17]) ).
cnf(d57,plain,
sz00 = sdtasdt0(sz00,xx),
inference(demodulation,[status(thm)],[d56,d55]) ).
cnf(d58,plain,
sz00 = sdtasdt0(xx,sz00),
inference(demodulation,[status(thm)],[d10,d57]) ).
cnf(d59,plain,
sdtpldt0(smndt0(sz10),sz10) = sz00,
inference(resolution,[status(thm)],[c10,c1]) ).
cnf(d60,plain,
( ~ aElement0(X0)
| sdtpldt0(xx,sdtasdt0(xx,X0)) = sdtpldt0(sdtasdt0(xx,X0),xx) ),
inference(resolution,[status(thm)],[d6,c17]) ).
cnf(d61,plain,
( ~ aElement0(X0)
| sdtpldt0(xx,sdtasdt0(xx,smndt0(X0))) = sdtpldt0(sdtasdt0(xx,smndt0(X0)),xx) ),
inference(resolution,[status(thm)],[d60,c2]) ).
cnf(d62,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtpldt0(sdtasdt0(xx,smndt0(sz10)),xx),
inference(resolution,[status(thm)],[d61,c1]) ).
cnf(d63,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,smndt0(X0)),xx) = sdtasdt0(xx,sdtpldt0(smndt0(X0),sz10)) ),
inference(resolution,[status(thm)],[d13,c2]) ).
cnf(d64,plain,
sdtpldt0(sdtasdt0(xx,smndt0(sz10)),xx) = sdtasdt0(xx,sdtpldt0(smndt0(sz10),sz10)),
inference(resolution,[status(thm)],[d63,c1]) ).
cnf(d65,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,sdtpldt0(smndt0(sz10),sz10)),
inference(demodulation,[status(thm)],[d64,d62]) ).
cnf(d66,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sdtasdt0(xx,sz00),
inference(demodulation,[status(thm)],[d65,d59]) ).
cnf(d67,plain,
sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10))) = sz00,
inference(demodulation,[status(thm)],[d66,d58]) ).
cnf(d68,plain,
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(X0,X1))) = sdtpldt0(sz00,sdtasdt0(X0,X1)) ),
inference(resolution,[status(thm)],[d52,c4]) ).
cnf(d69,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,X0))) = sdtpldt0(sz00,sdtasdt0(xx,X0)) ),
inference(resolution,[status(thm)],[d68,c17]) ).
cnf(d70,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,smndt0(X0)))) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(X0))) ),
inference(resolution,[status(thm)],[d69,c2]) ).
cnf(d71,plain,
sdtpldt0(smndt0(xx),sdtpldt0(xx,sdtasdt0(xx,smndt0(sz10)))) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))),
inference(resolution,[status(thm)],[d70,c1]) ).
cnf(d72,plain,
sdtpldt0(smndt0(xx),sz00) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))),
inference(demodulation,[status(thm)],[d71,d67]) ).
cnf(d73,plain,
smndt0(xx) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))),
inference(demodulation,[status(thm)],[d72,d1]) ).
cnf(d74,plain,
( sdtpldt0(sdtasdt0(X0,X1),sz00) = sdtasdt0(X0,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[c4,c7]) ).
cnf(d75,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,X0),sz00) = sdtasdt0(xx,X0) ),
inference(resolution,[status(thm)],[d74,c17]) ).
cnf(d76,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,smndt0(X0)),sz00) = sdtasdt0(xx,smndt0(X0)) ),
inference(resolution,[status(thm)],[d75,c2]) ).
cnf(d77,plain,
sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sz00) = sdtasdt0(xx,smndt0(sz10)),
inference(resolution,[status(thm)],[d76,c1]) ).
cnf(d78,plain,
( ~ aElement0(X0)
| sdtasdt0(xx,X0) = sdtasdt0(X0,xx) ),
inference(resolution,[status(thm)],[c11,c17]) ).
cnf(d79,plain,
( ~ aElement0(X0)
| sdtasdt0(xx,smndt0(X0)) = sdtasdt0(smndt0(X0),xx) ),
inference(resolution,[status(thm)],[d78,c2]) ).
cnf(d80,plain,
sdtasdt0(xx,smndt0(sz10)) = sdtasdt0(smndt0(sz10),xx),
inference(resolution,[status(thm)],[d79,c1]) ).
cnf(d81,plain,
( ~ aElement0(X1)
| ~ aElement0(X0)
| ~ aElement0(X2)
| sdtpldt0(sdtasdt0(X0,X1),X2) = sdtpldt0(X2,sdtasdt0(X0,X1)) ),
inference(resolution,[status(thm)],[c5,c4]) ).
cnf(d82,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| sdtpldt0(sdtasdt0(smndt0(X0),X1),X2) = sdtpldt0(X2,sdtasdt0(smndt0(X0),X1)) ),
inference(resolution,[status(thm)],[d81,c2]) ).
cnf(d83,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| sdtpldt0(sdtasdt0(smndt0(sz10),X0),X1) = sdtpldt0(X1,sdtasdt0(smndt0(sz10),X0)) ),
inference(resolution,[status(thm)],[d82,c1]) ).
cnf(d84,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(smndt0(sz10),xx),X0) = sdtpldt0(X0,sdtasdt0(smndt0(sz10),xx)) ),
inference(resolution,[status(thm)],[d83,c17]) ).
cnf(d85,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,smndt0(sz10)),X0) = sdtpldt0(X0,sdtasdt0(smndt0(sz10),xx)) ),
inference(demodulation,[status(thm)],[d84,d80]) ).
cnf(d86,plain,
( ~ aElement0(X0)
| sdtpldt0(sdtasdt0(xx,smndt0(sz10)),X0) = sdtpldt0(X0,sdtasdt0(xx,smndt0(sz10))) ),
inference(demodulation,[status(thm)],[d85,d80]) ).
cnf(d87,plain,
sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sz00) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))),
inference(resolution,[status(thm)],[d86,c0]) ).
cnf(d88,plain,
sdtasdt0(xx,smndt0(sz10)) = sdtpldt0(sz00,sdtasdt0(xx,smndt0(sz10))),
inference(demodulation,[status(thm)],[d87,d77]) ).
cnf(d89,plain,
sdtasdt0(xx,smndt0(sz10)) = smndt0(xx),
inference(demodulation,[status(thm)],[d88,d73]) ).
cnf(d90,plain,
smndt0(xx) != sdtasdt0(xx,smndt0(sz10)),
inference(demodulation,[status(thm)],[c18,d80]) ).
cnf(d91,plain,
smndt0(xx) != smndt0(xx),
inference(demodulation,[status(thm)],[d90,d89]) ).
cnf(d92,plain,
sdtasdt0(sz10,xx) = xx,
inference(resolution,[status(thm)],[c14,c17]) ).
cnf(d93,plain,
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtpldt0(smndt0(sdtasdt0(X0,X1)),sz00) = smndt0(sdtasdt0(X0,X1)) ),
inference(resolution,[status(thm)],[d0,c4]) ).
cnf(d94,plain,
( ~ aElement0(X0)
| sdtpldt0(smndt0(sdtasdt0(sz10,X0)),sz00) = smndt0(sdtasdt0(sz10,X0)) ),
inference(resolution,[status(thm)],[d93,c1]) ).
cnf(d95,plain,
sdtpldt0(smndt0(sdtasdt0(sz10,xx)),sz00) = smndt0(sdtasdt0(sz10,xx)),
inference(resolution,[status(thm)],[d94,c17]) ).
cnf(d96,plain,
sdtpldt0(smndt0(xx),sz00) = smndt0(sdtasdt0(sz10,xx)),
inference(demodulation,[status(thm)],[d95,d92]) ).
cnf(d97,plain,
smndt0(xx) = smndt0(sdtasdt0(sz10,xx)),
inference(demodulation,[status(thm)],[d96,d1]) ).
cnf(d98,plain,
smndt0(xx) = smndt0(xx),
inference(demodulation,[status(thm)],[d97,d92]) ).
cnf(d99,plain,
$false,
inference(resolution,[status(thm)],[d98,d91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG082+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n018.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Sat Sep 26 06:03:07 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 198.20/29.32 % SZS status Theorem for theBenchmark.p
% 198.20/29.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------