%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV153+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:50:09 PM UTC 2026
% Result : Theorem 0.90s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV153+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 08:33:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.90/0.53 % Refutation found
% 0.90/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.90/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.90/0.53 fof(f9,axiom,(
% 0.90/0.53 (! [X,Y] :( ( leq(X,Y)& X != Y )=> gt(Y,X) ) )),
% 0.90/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.53 fof(f10,axiom,(
% 0.90/0.53 (! [X,Y] :( leq(X,pred(Y))<=> gt(Y,X) ) )),
% 0.90/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.53 fof(f53,conjecture,(
% 0.90/0.53 ( ( pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))& leq(n0,pv10)& leq(n0,pv12)& leq(pv10,n135299)& leq(pv12,n4)& (! [A] :( ( leq(n0,A)& leq(A,pred(pv12)) )=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ))& (! [B] :( ( leq(n0,B)& leq(B,pred(pv10)) )=> sum(n0,n4,a_select3(q,B,tptp_sum_index)) = n1 ) ))=> (! [C] :( ( leq(n0,C)& leq(C,pv12) )=> ( pv12 != C=> a_select3(q,pv10,C) = divide(sqrt(times(minus(a_select3(center,C,n0),a_select2(x,pv10)),minus(a_select3(center,C,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ) ) )) ),
% 0.90/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.53 fof(f54,negated_conjecture,(
% 0.90/0.53 ~(( ( pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))& leq(n0,pv10)& leq(n0,pv12)& leq(pv10,n135299)& leq(pv12,n4)& (! [A] :( ( leq(n0,A)& leq(A,pred(pv12)) )=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ))& (! [B] :( ( leq(n0,B)& leq(B,pred(pv10)) )=> sum(n0,n4,a_select3(q,B,tptp_sum_index)) = n1 ) ))=> (! [C] :( ( leq(n0,C)& leq(C,pv12) )=> ( pv12 != C=> a_select3(q,pv10,C) = divide(sqrt(times(minus(a_select3(center,C,n0),a_select2(x,pv10)),minus(a_select3(center,C,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ) ) )) )),
% 0.90/0.53 inference(negated_conjecture,[status(cth)],[f53])).
% 0.90/0.53 fof(f113,plain,(
% 0.90/0.53 ![X,Y]: ((~leq(X,Y)|X=Y)|gt(Y,X))),
% 0.90/0.53 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.90/0.53 fof(f114,plain,(
% 0.90/0.53 ![X0,X1]: (~leq(X0,X1)|X0=X1|gt(X1,X0))),
% 0.90/0.53 inference(cnf_transformation,[status(thm)],[f113])).
% 0.90/0.53 fof(f115,plain,(
% 0.90/0.53 ![X,Y]: ((~leq(X,pred(Y))|gt(Y,X))&(leq(X,pred(Y))|~gt(Y,X)))),
% 0.90/0.53 inference(NNF_transformation,[status(thm)],[f10])).
% 0.90/0.53 fof(f116,plain,(
% 0.90/0.53 (![X,Y]: (~leq(X,pred(Y))|gt(Y,X)))&(![X,Y]: (leq(X,pred(Y))|~gt(Y,X)))),
% 0.90/0.53 inference(miniscoping,[status(thm)],[f115])).
% 0.90/0.53 fof(f118,plain,(
% 0.90/0.53 ![X0,X1]: (leq(X0,pred(X1))|~gt(X1,X0))),
% 0.90/0.53 inference(cnf_transformation,[status(thm)],[f116])).
% 0.90/0.53 fof(f251,plain,(
% 0.90/0.53 (((((((pv70=sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))&leq(n0,pv10))&leq(n0,pv12))&leq(pv10,n135299))&leq(pv12,n4))&(![A]: ((~leq(n0,A)|~leq(A,pred(pv12)))|a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))))))&(![B]: ((~leq(n0,B)|~leq(B,pred(pv10)))|sum(n0,n4,a_select3(q,B,tptp_sum_index))=n1)))&(?[C]: ((leq(n0,C)&leq(C,pv12))&(~pv12=C&~a_select3(q,pv10,C)=divide(sqrt(times(minus(a_select3(center,C,n0),a_select2(x,pv10)),minus(a_select3(center,C,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))))),
% 0.90/0.54 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.90/0.54 fof(f252,plain,(
% 0.90/0.54 ((((((pv70=sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))&leq(n0,pv10))&leq(n0,pv12))&leq(pv10,n135299))&leq(pv12,n4))&(![A]: ((~leq(n0,A)|~leq(A,pred(pv12)))|a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))))))&(![B]: ((~leq(n0,B)|~leq(B,pred(pv10)))|sum(n0,n4,a_select3(q,B,tptp_sum_index))=n1)))&((leq(n0,sK23_skl)&leq(sK23_skl,pv12))&(~pv12=sK23_skl&~a_select3(q,pv10,sK23_skl)=divide(sqrt(times(minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)),minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))))),
% 0.90/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(C,sK23_skl)],[f251])).
% 0.90/0.54 fof(f253,plain,(
% 0.90/0.54 pv70=sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f258,plain,(
% 0.90/0.54 ![X0]: (~leq(n0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))))),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f260,plain,(
% 0.90/0.54 leq(n0,sK23_skl)),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f261,plain,(
% 0.90/0.54 leq(sK23_skl,pv12)),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f262,plain,(
% 0.90/0.54 ~pv12=sK23_skl),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f263,plain,(
% 0.90/0.54 ~a_select3(q,pv10,sK23_skl)=divide(sqrt(times(minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)),minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))),
% 0.90/0.54 inference(cnf_transformation,[status(thm)],[f252])).
% 0.90/0.54 fof(f354,plain,(
% 0.90/0.54 ![X0]: (~leq(n0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),pv70))),
% 0.90/0.54 inference(forward_demodulation,[status(thm)],[f253,f258])).
% 0.90/0.54 fof(f355,plain,(
% 0.90/0.54 ~a_select3(q,pv10,sK23_skl)=divide(sqrt(times(minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)),minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)))),pv70)),
% 0.90/0.54 inference(forward_demodulation,[status(thm)],[f253,f263])).
% 0.90/0.54 fof(f378,plain,(
% 0.90/0.54 ![X0]: (~gt(pv12,X0)|~leq(n0,X0)|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),pv70))),
% 0.90/0.54 inference(resolution,[status(thm)],[f118,f354])).
% 0.90/0.54 fof(f398,plain,(
% 0.90/0.54 sK23_skl=pv12|gt(pv12,sK23_skl)),
% 0.90/0.54 inference(resolution,[status(thm)],[f114,f261])).
% 0.90/0.54 fof(f408,plain,(
% 0.90/0.54 gt(pv12,sK23_skl)),
% 0.90/0.54 inference(forward_subsumption_resolution,[status(thm)],[f398,f262])).
% 0.90/0.54 fof(f578,plain,(
% 0.90/0.54 ~leq(n0,sK23_skl)|a_select3(q,pv10,sK23_skl)=divide(sqrt(times(minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)),minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)))),pv70)),
% 0.90/0.54 inference(resolution,[status(thm)],[f378,f408])).
% 0.90/0.54 fof(f587,plain,(
% 0.90/0.54 ~a_select3(q,pv10,sK23_skl)=a_select3(q,pv10,sK23_skl)),
% 0.90/0.54 inference(backward_demodulation,[status(thm)],[f588,f355])).
% 0.90/0.54 fof(f588,plain,(
% 0.90/0.54 a_select3(q,pv10,sK23_skl)=divide(sqrt(times(minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)),minus(a_select3(center,sK23_skl,n0),a_select2(x,pv10)))),pv70)),
% 0.90/0.54 inference(forward_subsumption_resolution,[status(thm)],[f578,f260])).
% 0.90/0.54 fof(f589,plain,(
% 0.90/0.54 $false),
% 0.90/0.54 inference(trivial_equality_resolution,[status(thm)],[f587])).
% 0.90/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.90/0.55 % Elapsed time: 0.240157 seconds
% 0.90/0.55 % CPU time: 1.686991 seconds
% 0.90/0.55 % Total memory used: 136.788 MB
% 0.90/0.55 % Net memory used: 131.993 MB
%------------------------------------------------------------------------------