%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM443+4 : 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 : n003.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:01 AM UTC 2026
% Result : Theorem 9.15s 1.82s
% Output : CNFRefutation 9.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 5
% Syntax : Number of formulae : 44 ( 14 unt; 0 def)
% Number of atoms : 208 ( 32 equ)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 239 ( 75 ~; 93 |; 55 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 43 ( 0 sgn 11 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
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__1962,axiom,
( xq != sz00
& aInteger0(xq)
& aInteger0(xa) ),
file('theBenchmark.p',m__1962) ).
fof(m__2010,axiom,
( aInteger0(xc)
& aInteger0(xb) ),
file('theBenchmark.p',m__2010) ).
fof(m__,conjecture,
( ( sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [W0] :
( sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb))
& aInteger0(W0) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( sdteqdtlpzmzozddtrp0(xc,xb,xq)
& aDivisorOf0(xq,sdtpldt0(xc,smndt0(xb)))
& ? [W0] :
( sdtasdt0(xq,W0) = sdtpldt0(xc,smndt0(xb))
& aInteger0(W0) )
& aElementOf0(xb,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( aElementOf0(xc,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_83,plain,
( sdteqdtlpzmzozddtrp0(B,A,C)
| ~ sdteqdtlpzmzozddtrp0(A,B,C)
| C = sz00
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mEquModSym]) ).
cnf(c_84,plain,
( sdteqdtlpzmzozddtrp0(B,A,C)
| ~ sdteqdtlpzmzozddtrp0(A,B,C)
| sz00 = C
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_83]) ).
cnf(c_85,plain,
( sdteqdtlpzmzozddtrp0(A,D,C)
| ~ sdteqdtlpzmzozddtrp0(B,D,C)
| ~ sdteqdtlpzmzozddtrp0(A,B,C)
| ~ aInteger0(D)
| C = sz00
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[mEquModTrn]) ).
cnf(c_86,plain,
( sdteqdtlpzmzozddtrp0(A,D,C)
| ~ sdteqdtlpzmzozddtrp0(B,D,C)
| ~ sdteqdtlpzmzozddtrp0(A,B,C)
| ~ aInteger0(D)
| sz00 = C
| ~ aInteger0(C)
| ~ aInteger0(B)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_165,plain,
aInteger0(xa),
inference(clausify,[status(thm)],[m__1962]) ).
cnf(c_166,plain,
aInteger0(xq),
inference(clausify,[status(thm)],[m__1962]) ).
cnf(c_167,plain,
xq != sz00,
inference(clausify,[status(thm)],[m__1962]) ).
cnf(c_168,plain,
aInteger0(xb),
inference(clausify,[status(thm)],[m__2010]) ).
cnf(c_169,plain,
aInteger0(xc),
inference(clausify,[status(thm)],[m__2010]) ).
cnf(c_176,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xa,xq)
| ~ aElementOf0(A,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_179,negated_conjecture,
( aElementOf0(A,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sdteqdtlpzmzozddtrp0(A,xa,xq)
| ~ aInteger0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_180,negated_conjecture,
~ aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_186,negated_conjecture,
sdteqdtlpzmzozddtrp0(xc,xb,xq),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_190,negated_conjecture,
aElementOf0(xc,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_10696,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(xb)
| sz00 = xq
| ~ aInteger0(xq)
| ~ aInteger0(xc)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_186,c_86]) ).
cnf(c_10697,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(xb)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(xc)
| ~ aInteger0(A) ),
inference(copy,[status(thm)],[c_10696]) ).
cnf(c_10698,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(xb)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_169,c_10697]) ).
cnf(c_10699,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(xb)
| xq = sz00
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_166,c_10698]) ).
cnf(c_10700,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(xb)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_167,c_10699]) ).
cnf(c_712,negated_conjecture,
( sdteqdtlpzmzozddtrp0(A,xb,xq)
| ~ sdteqdtlpzmzozddtrp0(A,xc,xq)
| ~ aInteger0(A) ),
inference(resolve,[status(thm)],[c_168,c_10700]) ).
cnf(c_717,plain,
sdteqdtlpzmzozddtrp0(xc,xa,xq),
inference(resolve,[status(thm)],[c_190,c_176]) ).
cnf(c_10701,plain,
( sdteqdtlpzmzozddtrp0(xa,xc,xq)
| sz00 = xq
| ~ aInteger0(xq)
| ~ aInteger0(xa)
| ~ aInteger0(xc) ),
inference(resolve,[status(thm)],[c_717,c_84]) ).
cnf(c_10702,plain,
( sdteqdtlpzmzozddtrp0(xa,xc,xq)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(xa)
| ~ aInteger0(xc) ),
inference(copy,[status(thm)],[c_10701]) ).
cnf(c_10703,plain,
( sdteqdtlpzmzozddtrp0(xa,xc,xq)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(xa) ),
inference(resolve,[status(thm)],[c_169,c_10702]) ).
cnf(c_10704,plain,
( sdteqdtlpzmzozddtrp0(xa,xc,xq)
| xq = sz00
| ~ aInteger0(xq) ),
inference(resolve,[status(thm)],[c_165,c_10703]) ).
cnf(c_10705,plain,
( sdteqdtlpzmzozddtrp0(xa,xc,xq)
| xq = sz00 ),
inference(resolve,[status(thm)],[c_166,c_10704]) ).
cnf(c_1100,plain,
sdteqdtlpzmzozddtrp0(xa,xc,xq),
inference(resolve,[status(thm)],[c_167,c_10705]) ).
cnf(c_10706,plain,
( sdteqdtlpzmzozddtrp0(xa,xb,xq)
| ~ aInteger0(xa) ),
inference(resolve,[status(thm)],[c_712,c_1100]) ).
cnf(c_10685,plain,
sdteqdtlpzmzozddtrp0(xa,xb,xq),
inference(resolve,[status(thm)],[c_165,c_10706]) ).
cnf(c_10707,plain,
( sdteqdtlpzmzozddtrp0(xb,xa,xq)
| sz00 = xq
| ~ aInteger0(xq)
| ~ aInteger0(xb)
| ~ aInteger0(xa) ),
inference(resolve,[status(thm)],[c_10685,c_84]) ).
cnf(c_10708,plain,
( sdteqdtlpzmzozddtrp0(xb,xa,xq)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(xb)
| ~ aInteger0(xa) ),
inference(copy,[status(thm)],[c_10707]) ).
cnf(c_10709,plain,
( sdteqdtlpzmzozddtrp0(xb,xa,xq)
| xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(xb) ),
inference(resolve,[status(thm)],[c_165,c_10708]) ).
cnf(c_10710,plain,
( sdteqdtlpzmzozddtrp0(xb,xa,xq)
| xq = sz00
| ~ aInteger0(xq) ),
inference(resolve,[status(thm)],[c_168,c_10709]) ).
cnf(c_10711,plain,
( sdteqdtlpzmzozddtrp0(xb,xa,xq)
| xq = sz00 ),
inference(resolve,[status(thm)],[c_166,c_10710]) ).
cnf(c_10691,plain,
sdteqdtlpzmzozddtrp0(xb,xa,xq),
inference(resolve,[status(thm)],[c_167,c_10711]) ).
cnf(c_10712,negated_conjecture,
( aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(xb) ),
inference(resolve,[status(thm)],[c_10691,c_179]) ).
cnf(c_10713,negated_conjecture,
aElementOf0(xb,szAzrzSzezqlpdtcmdtrp0(xa,xq)),
inference(resolve,[status(thm)],[c_168,c_10712]) ).
cnf(c_10695,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_180,c_10713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM443+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.46 % Computer : n003.cluster.edu
% 0.21/0.46 % Model : x86_64 x86_64
% 0.21/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.46 % Memory : 8046.5625MB
% 0.21/0.46 % OS : Linux 6.8.0-71-generic
% 0.21/0.46 % CPULimit : 300
% 0.21/0.46 % WCLimit : 300
% 0.21/0.46 % DateTime : Sat Sep 26 02:46:23 UTC 2026
% 0.21/0.46 % CPUTime :
% 0.21/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.21/0.47 % Process 1855349 was started by sandbox on n003,
% 0.21/0.47 % Sat Sep 26 02:46:23 2026
% 0.21/0.47 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.21/0.49
% 0.21/0.49 % From the command line: assign(max_seconds, 300).
% 9.15/1.82
% 9.15/1.82 % given #500 (W,wt=15): 420 sdtasdt0(xa,sz10) = xa. [resolve(165,a,58,a)].
% 9.15/1.82
% 9.15/1.82 % SZS status Theorem for theBenchmark
% 9.15/1.82
% 9.15/1.82 % Proof 1 at 1.02 (+ 0.27) seconds.
% 9.15/1.82 % Length of proof is 25.
% 9.15/1.82 % Level of proof is 6.
% 9.15/1.82 % Maximum clause weight is 28.000.
% 9.15/1.82 % Given clauses 565.
% 9.15/1.82
% 9.15/1.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------