%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG050+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 : 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:26:30 AM UTC 2026
% Result : Theorem 0.20s 0.59s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 21 ( 10 unt; 0 def)
% Number of atoms : 43 ( 20 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 39 ( 17 ~; 13 |; 2 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 8 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mLERef,axiom,
! [W0] :
( aScalar0(W0)
=> sdtlseqdt0(W0,W0) ),
file('theBenchmark.p',mLERef) ).
fof(mDefSPZ,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( ( aDimensionOf0(W1) = sz00
& aDimensionOf0(W0) = aDimensionOf0(W1) )
=> sdtasasdt0(W0,W1) = sz0z00 ) ),
file('theBenchmark.p',mDefSPZ) ).
fof(m__,conjecture,
( ( aDimensionOf0(xs) != sz00
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( aDimensionOf0(xs) != sz00
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )
=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mSZeroSc,axiom,
aScalar0(sz0z00),
file('theBenchmark.p',mSZeroSc) ).
cnf(c_44,plain,
aScalar0(sz0z00),
inference(clausify,[status(thm)],[mSZeroSc]) ).
cnf(c_69,plain,
( sdtlseqdt0(A,A)
| ~ aScalar0(A) ),
inference(clausify,[status(thm)],[mLERef]) ).
cnf(c_88,plain,
( sdtasasdt0(A,B) = sz0z00
| aDimensionOf0(B) != sz00
| aDimensionOf0(B) != aDimensionOf0(A)
| ~ aVector0(B)
| ~ aVector0(A) ),
inference(clausify,[status(thm)],[mDefSPZ]) ).
fof(m__1542,axiom,
aVector0(xs),
file('theBenchmark.p',m__1542) ).
cnf(c_91,plain,
aVector0(xs),
inference(clausify,[status(thm)],[m__1542]) ).
cnf(c_93,negated_conjecture,
( sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))
| aDimensionOf0(xs) = sz00 ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_94,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_289,plain,
( sdtasasdt0(A,A) = sz0z00
| aDimensionOf0(A) != sz00
| aDimensionOf0(A) != aDimensionOf0(A)
| ~ aVector0(A) ),
inference(factor,[status(thm)],[c_88]) ).
cnf(c_140,plain,
( sdtasasdt0(A,A) = sz0z00
| aDimensionOf0(A) != sz00
| ~ aVector0(A) ),
inference(copy,[status(thm)],[c_289]) ).
cnf(c_142,negated_conjecture,
aDimensionOf0(xs) = sz00,
inference(resolve,[status(thm)],[c_94,c_93]) ).
cnf(c_245,plain,
sdtlseqdt0(sz0z00,sz0z00),
inference(resolve,[status(thm)],[c_69,c_44]) ).
cnf(c_290,plain,
( sdtasasdt0(xs,xs) = sz0z00
| aDimensionOf0(xs) != sz00 ),
inference(resolve,[status(thm)],[c_140,c_91]) ).
cnf(c_291,plain,
( sdtasasdt0(xs,xs) = sz0z00
| sz00 != sz00 ),
inference(paramod,[status(thm)],[c_142,c_290]) ).
cnf(c_287,plain,
sdtasasdt0(xs,xs) = sz0z00,
inference(copy,[status(thm)],[c_291]) ).
cnf(c_292,negated_conjecture,
~ sdtlseqdt0(sz0z00,sz0z00),
inference(paramod,[status(thm)],[c_287,c_94]) ).
cnf(c_288,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_245,c_292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG050+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.40 % Computer : n004.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.41 % CPULimit : 300
% 0.09/0.41 % WCLimit : 300
% 0.09/0.41 % DateTime : Sat Sep 26 05:52:36 UTC 2026
% 0.09/0.41 % CPUTime :
% 0.09/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.41 % Process 962992 was started by sandbox on n004,
% 0.09/0.41 % Sat Sep 26 05:52:36 2026
% 0.09/0.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.42
% 0.09/0.42 % From the command line: assign(max_seconds, 300).
% 0.20/0.59
% 0.20/0.59 % SZS status Theorem for theBenchmark
% 0.20/0.59
% 0.20/0.59 % Proof 1 at 0.03 (+ 0.00) seconds.
% 0.20/0.59 % Length of proof is 14.
% 0.20/0.59 % Level of proof is 4.
% 0.20/0.59 % Maximum clause weight is 18.000.
% 0.20/0.59 % Given clauses 94.
% 0.20/0.59
% 0.20/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------