%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG050+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Thu Sep 24 02:05:13 PM UTC 2026
% Result : Theorem 0.08s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG050+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 04:15:42 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.40 % Refutation found
% 0.08/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.40 fof(f9,axiom,(
% 0.08/0.40 aScalar0(sz0z00) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f20,axiom,(
% 0.08/0.40 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f35,axiom,(
% 0.08/0.40 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) = sz00 )=> sdtasasdt0(W0,W1) = sz0z00 ) ) )),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f37,hypothesis,(
% 0.08/0.40 aVector0(xs) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f39,conjecture,(
% 0.08/0.40 ( ( aDimensionOf0(xs) != sz00=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ) ),
% 0.08/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.40 fof(f40,negated_conjecture,(
% 0.08/0.40 ~(( ( aDimensionOf0(xs) != sz00=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ) )),
% 0.08/0.40 inference(negated_conjecture,[status(cth)],[f39])).
% 0.08/0.40 fof(f61,plain,(
% 0.08/0.40 aScalar0(sz0z00)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.08/0.40 fof(f94,plain,(
% 0.08/0.40 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.08/0.40 fof(f95,plain,(
% 0.08/0.40 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f94])).
% 0.08/0.40 fof(f133,plain,(
% 0.08/0.40 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|~aDimensionOf0(W1)=sz00)|sdtasasdt0(W0,W1)=sz0z00))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.08/0.40 fof(f134,plain,(
% 0.08/0.40 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|~aDimensionOf0(X1)=sz00|sdtasasdt0(X0,X1)=sz0z00)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f133])).
% 0.08/0.40 fof(f137,plain,(
% 0.08/0.40 aVector0(xs)),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f37])).
% 0.08/0.40 fof(f140,plain,(
% 0.08/0.40 ((aDimensionOf0(xs)=sz00|sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)))&~sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)))),
% 0.08/0.40 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.08/0.40 fof(f141,plain,(
% 0.08/0.40 aDimensionOf0(xs)=sz00|sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f140])).
% 0.08/0.40 fof(f142,plain,(
% 0.08/0.40 ~sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 0.08/0.40 inference(cnf_transformation,[status(thm)],[f140])).
% 0.08/0.40 fof(f143,plain,(
% 0.08/0.40 aDimensionOf0(xs)=sz00),
% 0.08/0.40 inference(backward_subsumption_resolution,[status(thm)],[f141,f142])).
% 0.08/0.40 fof(f147,plain,(
% 0.08/0.40 ![X0]: (~aVector0(X0)|~aVector0(xs)|~aDimensionOf0(X0)=aDimensionOf0(xs)|sdtasasdt0(X0,xs)=sz0z00)),
% 0.08/0.40 inference(resolution,[status(thm)],[f134,f143])).
% 0.08/0.40 fof(f149,plain,(
% 0.08/0.40 ![X0]: (~aVector0(X0)|~aVector0(xs)|~aDimensionOf0(X0)=sz00|sdtasasdt0(X0,xs)=sz0z00)),
% 0.08/0.40 inference(forward_demodulation,[status(thm)],[f143,f147])).
% 0.08/0.40 fof(f150,plain,(
% 0.08/0.40 ![X0]: (~aVector0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(X0,xs)=sz0z00)),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f149,f137])).
% 0.08/0.40 fof(f153,plain,(
% 0.08/0.40 ~aVector0(xs)|sdtasasdt0(xs,xs)=sz0z00),
% 0.08/0.40 inference(resolution,[status(thm)],[f150,f143])).
% 0.08/0.40 fof(f156,plain,(
% 0.08/0.40 ~sdtlseqdt0(sz0z00,sz0z00)),
% 0.08/0.40 inference(backward_demodulation,[status(thm)],[f157,f142])).
% 0.08/0.40 fof(f157,plain,(
% 0.08/0.40 sdtasasdt0(xs,xs)=sz0z00),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f153,f137])).
% 0.08/0.40 fof(f161,plain,(
% 0.08/0.40 sdtlseqdt0(sz0z00,sz0z00)),
% 0.08/0.40 inference(resolution,[status(thm)],[f61,f95])).
% 0.08/0.40 fof(f164,plain,(
% 0.08/0.40 $false),
% 0.08/0.40 inference(forward_subsumption_resolution,[status(thm)],[f161,f156])).
% 0.08/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.42 % Elapsed time: 0.050246 seconds
% 0.08/0.42 % CPU time: 0.159405 seconds
% 0.08/0.42 % Total memory used: 62.119 MB
% 0.08/0.42 % Net memory used: 61.975 MB
%------------------------------------------------------------------------------