%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM557+3 : 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 : n004.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:23 AM UTC 2026
% Result : Theorem 0.27s 0.52s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 24 ( 12 unt; 0 def)
% Number of atoms : 54 ( 22 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 47 ( 17 ~; 12 |; 13 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 5 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__2291,axiom,
( sbrdtbr0(xQ) = xk
& isFinite0(xQ)
& aSet0(xQ) ),
file('theBenchmark.p',m__2291) ).
fof(m__2357,axiom,
( xP = sdtpldt0(sdtmndt0(xQ,xy),xx)
& ! [W0] :
( aElementOf0(W0,xP)
<=> ( ( W0 = xx
| aElementOf0(W0,sdtmndt0(xQ,xy)) )
& aElement0(W0) ) )
& aSet0(xP)
& ! [W0] :
( aElementOf0(W0,sdtmndt0(xQ,xy))
<=> ( W0 != xy
& aElementOf0(W0,xQ)
& aElement0(W0) ) )
& aSet0(sdtmndt0(xQ,xy)) ),
file('theBenchmark.p',m__2357) ).
fof(m__2431,axiom,
( sbrdtbr0(xP) = xk
& aSubsetOf0(xP,xS)
& ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xS) ) ),
file('theBenchmark.p',m__2431) ).
fof(m__,conjecture,
( aElementOf0(xP,slbdtsldtrb0(xS,xk))
| ( sbrdtbr0(xP) = xk
& ( aSubsetOf0(xP,xS)
| ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xS) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( aElementOf0(xP,slbdtsldtrb0(xS,xk))
| ( sbrdtbr0(xP) = xk
& ( aSubsetOf0(xP,xS)
| ! [W0] :
( aElementOf0(W0,xP)
=> aElementOf0(W0,xS) ) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_68,negated_conjecture,
( sbrdtbr0(xP) != xk
| ~ aSubsetOf0(xP,xS) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_71,plain,
sbrdtbr0(xP) = xk,
inference(clausify,[status(thm)],[m__2431]) ).
cnf(c_72,plain,
xk = sbrdtbr0(xP),
inference(copy,[status(thm)],[c_71]) ).
cnf(c_73,plain,
aSubsetOf0(xP,xS),
inference(clausify,[status(thm)],[m__2431]) ).
cnf(c_81,plain,
sdtpldt0(sdtmndt0(xQ,xy),xx) = xP,
inference(clausify,[status(thm)],[m__2357]) ).
cnf(c_82,plain,
xP = sdtpldt0(sdtmndt0(xQ,xy),xx),
inference(copy,[status(thm)],[c_81]) ).
cnf(c_96,plain,
sbrdtbr0(xQ) = xk,
inference(clausify,[status(thm)],[m__2291]) ).
cnf(c_288,plain,
sbrdtbr0(xQ) = sbrdtbr0(xP),
inference(paramod,[status(thm)],[c_72,c_96]) ).
cnf(c_289,plain,
sbrdtbr0(xQ) = sbrdtbr0(sdtpldt0(sdtmndt0(xQ,xy),xx)),
inference(paramod,[status(thm)],[c_82,c_288]) ).
cnf(c_97,plain,
sbrdtbr0(sdtpldt0(sdtmndt0(xQ,xy),xx)) = sbrdtbr0(xQ),
inference(copy,[status(thm)],[c_289]) ).
cnf(c_290,negated_conjecture,
( sbrdtbr0(xP) != xk
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_82,c_68]) ).
cnf(c_291,negated_conjecture,
( sbrdtbr0(sdtpldt0(sdtmndt0(xQ,xy),xx)) != xk
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_82,c_290]) ).
cnf(c_292,negated_conjecture,
( sbrdtbr0(xQ) != xk
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_97,c_291]) ).
cnf(c_293,negated_conjecture,
( sbrdtbr0(xQ) != sbrdtbr0(xP)
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_72,c_292]) ).
cnf(c_294,negated_conjecture,
( sbrdtbr0(xQ) != sbrdtbr0(sdtpldt0(sdtmndt0(xQ,xy),xx))
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_82,c_293]) ).
cnf(c_295,negated_conjecture,
( sbrdtbr0(xQ) != sbrdtbr0(xQ)
| ~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS) ),
inference(paramod,[status(thm)],[c_97,c_294]) ).
cnf(c_284,negated_conjecture,
~ aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS),
inference(copy,[status(thm)],[c_295]) ).
cnf(c_296,plain,
aSubsetOf0(sdtpldt0(sdtmndt0(xQ,xy),xx),xS),
inference(paramod,[status(thm)],[c_82,c_73]) ).
cnf(c_287,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_284,c_296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM557+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n004.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 03:13:22 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 689724 was started by sandbox on n004,
% 0.18/0.45 % Sat Sep 26 03:13:22 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.48
% 0.18/0.48 % From the command line: assign(max_seconds, 300).
% 0.18/0.50 --- backtrace (15 frames) ---
% 0.18/0.50 [0x41fd9f]
% 0.18/0.50 [0x484fd0]
% 0.18/0.50 [0x467349]
% 0.18/0.50 [0x46b3ab]
% 0.18/0.50 [0x416b10]
% 0.18/0.50 [0x41887f]
% 0.18/0.50 [0x419d4e]
% 0.18/0.50 [0x41c798]
% 0.18/0.50 [0x4039a8]
% 0.18/0.50 [0x403f27]
% 0.18/0.50 [0x4049d4]
% 0.18/0.50 [0x402997]
% 0.18/0.50 [0x482698]
% 0.18/0.50 [0x484860]
% 0.18/0.50 [0x402a35]
% 0.18/0.50 --- end backtrace ---
% 0.18/0.51 --- backtrace (15 frames) ---
% 0.18/0.51 [0x41fd9f]
% 0.18/0.51 [0x484fd0]
% 0.18/0.51 [0x467349]
% 0.18/0.51 [0x46b3ab]
% 0.18/0.51 [0x416b10]
% 0.18/0.51 [0x41887f]
% 0.18/0.51 [0x419d4e]
% 0.18/0.51 [0x41c798]
% 0.18/0.51 [0x4039a8]
% 0.18/0.51 [0x403f27]
% 0.18/0.51 [0x4049d4]
% 0.18/0.51 [0x402997]
% 0.18/0.51 [0x482698]
% 0.18/0.51 [0x484860]
% 0.18/0.51 [0x402a35]
% 0.18/0.51 --- end backtrace ---
% 0.18/0.51 --- backtrace (15 frames) ---
% 0.18/0.51 [0x41fd9f]
% 0.18/0.51 [0x484fd0]
% 0.18/0.51 [0x467349]
% 0.18/0.51 [0x46b3ab]
% 0.18/0.51 [0x416b10]
% 0.18/0.51 [0x41887f]
% 0.18/0.51 [0x419d4e]
% 0.18/0.51 [0x41c798]
% 0.18/0.51 [0x4039a8]
% 0.18/0.51 [0x403f27]
% 0.18/0.51 [0x4049d4]
% 0.18/0.51 [0x402997]
% 0.18/0.51 [0x482698]
% 0.18/0.51 [0x484860]
% 0.18/0.51 [0x402a35]
% 0.18/0.51 --- end backtrace ---
% 0.27/0.52
% 0.27/0.52 % SZS status Theorem for theBenchmark
% 0.27/0.52
% 0.27/0.52 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.27/0.52 % Length of proof is 14.
% 0.27/0.52 % Level of proof is 5.
% 0.27/0.52 % Maximum clause weight is 9.000.
% 0.27/0.52 % Given clauses 0.
% 0.27/0.52
% 0.27/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------