%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG047+1 : 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 : n005.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:29 AM UTC 2026
% Result : Theorem 2.34s 0.81s
% Output : CNFRefutation 2.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 41 ( 17 unt; 0 def)
% Number of atoms : 88 ( 59 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 79 ( 32 ~; 35 |; 5 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 27 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSuccEqu,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)
=> W0 = W1 ) ),
file('theBenchmark.p',mSuccEqu) ).
fof(mDimNat,axiom,
! [W0] :
( aVector0(W0)
=> aNaturalNumber0(aDimensionOf0(W0)) ),
file('theBenchmark.p',mDimNat) ).
fof(mDefInit,axiom,
! [W0] :
( aVector0(W0)
=> ( aDimensionOf0(W0) != sz00
=> ! [W1] :
( W1 = sziznziztdt0(W0)
<=> ( ! [W2] :
( aNaturalNumber0(W2)
=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) ) ) ) ),
file('theBenchmark.p',mDefInit) ).
fof(m__1329,axiom,
( aVector0(xt)
& aVector0(xs) ),
file('theBenchmark.p',m__1329) ).
fof(m__1329_01,axiom,
( aDimensionOf0(xt) != sz00
& aDimensionOf0(xs) = aDimensionOf0(xt) ),
file('theBenchmark.p',m__1329_01) ).
fof(m__,conjecture,
aDimensionOf0(sziznziztdt0(xs)) = aDimensionOf0(sziznziztdt0(xt)),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
aDimensionOf0(sziznziztdt0(xs)) != aDimensionOf0(sziznziztdt0(xt)),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_34,negated_conjecture,
aDimensionOf0(sziznziztdt0(xt)) != aDimensionOf0(sziznziztdt0(xs)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_35,plain,
aDimensionOf0(xt) != sz00,
inference(clausify,[status(thm)],[m__1329_01]) ).
cnf(c_36,plain,
aDimensionOf0(xt) = aDimensionOf0(xs),
inference(clausify,[status(thm)],[m__1329_01]) ).
cnf(c_37,plain,
aVector0(xt),
inference(clausify,[status(thm)],[m__1329]) ).
cnf(c_38,plain,
aVector0(xs),
inference(clausify,[status(thm)],[m__1329]) ).
cnf(c_42,plain,
( aDimensionOf0(A) = szszuzczcdt0(aDimensionOf0(B))
| sziznziztdt0(A) != B
| aDimensionOf0(A) = sz00
| ~ aVector0(A) ),
inference(clausify,[status(thm)],[mDefInit]) ).
cnf(c_43,plain,
( aVector0(B)
| sziznziztdt0(A) != B
| aDimensionOf0(A) = sz00
| ~ aVector0(A) ),
inference(clausify,[status(thm)],[mDefInit]) ).
cnf(c_45,plain,
( aNaturalNumber0(aDimensionOf0(A))
| ~ aVector0(A) ),
inference(clausify,[status(thm)],[mDimNat]) ).
cnf(c_81,plain,
( B = A
| szszuzczcdt0(B) != szszuzczcdt0(A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSuccEqu]) ).
cnf(c_87,plain,
aDimensionOf0(xs) != sz00,
inference(paramod,[status(thm)],[c_36,c_35]) ).
cnf(c_652,plain,
( aDimensionOf0(xs) = szszuzczcdt0(aDimensionOf0(A))
| sziznziztdt0(xs) != A
| aDimensionOf0(xs) = sz00 ),
inference(resolve,[status(thm)],[c_42,c_38]) ).
cnf(c_653,plain,
( szszuzczcdt0(aDimensionOf0(A)) = aDimensionOf0(xs)
| sziznziztdt0(xs) != A
| aDimensionOf0(xs) = sz00 ),
inference(copy,[status(thm)],[c_652]) ).
cnf(c_173,plain,
( szszuzczcdt0(aDimensionOf0(A)) = aDimensionOf0(xs)
| sziznziztdt0(xs) != A ),
inference(resolve,[status(thm)],[c_87,c_653]) ).
cnf(c_654,plain,
( aDimensionOf0(xt) = szszuzczcdt0(aDimensionOf0(A))
| sziznziztdt0(xt) != A
| aDimensionOf0(xt) = sz00 ),
inference(resolve,[status(thm)],[c_42,c_37]) ).
cnf(c_655,plain,
( aDimensionOf0(xt) = szszuzczcdt0(aDimensionOf0(A))
| sziznziztdt0(xt) != A
| aDimensionOf0(xs) = sz00 ),
inference(paramod,[status(thm)],[c_36,c_654]) ).
cnf(c_656,plain,
( aDimensionOf0(xs) = szszuzczcdt0(aDimensionOf0(A))
| sziznziztdt0(xt) != A
| aDimensionOf0(xs) = sz00 ),
inference(paramod,[status(thm)],[c_36,c_655]) ).
cnf(c_657,plain,
( szszuzczcdt0(aDimensionOf0(A)) = aDimensionOf0(xs)
| sziznziztdt0(xt) != A
| aDimensionOf0(xs) = sz00 ),
inference(copy,[status(thm)],[c_656]) ).
cnf(c_174,plain,
( szszuzczcdt0(aDimensionOf0(A)) = aDimensionOf0(xs)
| sziznziztdt0(xt) != A ),
inference(resolve,[status(thm)],[c_87,c_657]) ).
cnf(c_658,plain,
( aVector0(A)
| sziznziztdt0(xs) != A
| aDimensionOf0(xs) = sz00 ),
inference(resolve,[status(thm)],[c_43,c_38]) ).
cnf(c_176,plain,
( aVector0(A)
| sziznziztdt0(xs) != A ),
inference(resolve,[status(thm)],[c_87,c_658]) ).
cnf(c_659,plain,
( aVector0(A)
| sziznziztdt0(xt) != A
| aDimensionOf0(xt) = sz00 ),
inference(resolve,[status(thm)],[c_43,c_37]) ).
cnf(c_660,plain,
( aVector0(A)
| sziznziztdt0(xt) != A
| aDimensionOf0(xs) = sz00 ),
inference(paramod,[status(thm)],[c_36,c_659]) ).
cnf(c_177,plain,
( aVector0(A)
| sziznziztdt0(xt) != A ),
inference(resolve,[status(thm)],[c_87,c_660]) ).
cnf(c_338,plain,
aVector0(sziznziztdt0(xs)),
inference(xxres,[status(thm)],[c_176]) ).
cnf(c_341,plain,
aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))),
inference(resolve,[status(thm)],[c_338,c_45]) ).
cnf(c_346,plain,
aVector0(sziznziztdt0(xt)),
inference(xxres,[status(thm)],[c_177]) ).
cnf(c_349,plain,
aNaturalNumber0(aDimensionOf0(sziznziztdt0(xt))),
inference(resolve,[status(thm)],[c_346,c_45]) ).
cnf(c_591,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(xxres,[status(thm)],[c_173]) ).
cnf(c_661,plain,
( A = aDimensionOf0(sziznziztdt0(xs))
| szszuzczcdt0(A) != szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_81,c_341]) ).
cnf(c_662,plain,
( aDimensionOf0(sziznziztdt0(xt)) = aDimensionOf0(sziznziztdt0(xs))
| szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) != szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(resolve,[status(thm)],[c_661,c_349]) ).
cnf(c_663,negated_conjecture,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) != szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))),
inference(resolve,[status(thm)],[c_662,c_34]) ).
cnf(c_650,negated_conjecture,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) != aDimensionOf0(xs),
inference(paramod,[status(thm)],[c_591,c_663]) ).
cnf(c_664,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xs),
inference(xxres,[status(thm)],[c_174]) ).
cnf(c_651,plain,
$false,
inference(resolve,[status(thm)],[c_650,c_664]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG047+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n005.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sat Sep 26 05:51:47 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.45 % Process 1358233 was started by sandbox on n005,
% 0.16/0.45 % Sat Sep 26 05:51:47 2026
% 0.16/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.47
% 0.16/0.47 % From the command line: assign(max_seconds, 300).
% 2.34/0.81
% 2.34/0.81 % SZS status Theorem for theBenchmark
% 2.34/0.81
% 2.34/0.81 % Proof 1 at 0.19 (+ 0.05) seconds.
% 2.34/0.81 % Length of proof is 27.
% 2.34/0.81 % Level of proof is 7.
% 2.34/0.81 % Maximum clause weight is 22.000.
% 2.34/0.81 % Given clauses 159.
% 2.34/0.81
% 2.34/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------