%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV221+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:15 PM UTC 2026
% Result : Theorem 4.72s 1.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV221+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 08:35:05 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 4.72/1.10 % Refutation found
% 4.72/1.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.72/1.10 % SZS output start CNFRefutation for theBenchmark
% 4.72/1.10 fof(f26,axiom,(
% 4.72/1.10 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 4.72/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.72/1.10 fof(f27,axiom,(
% 4.72/1.10 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 4.72/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.72/1.10 fof(f53,conjecture,(
% 4.72/1.10 ( ( leq(n0,pv5)& leq(n0,pv57)& leq(pv5,n998)& leq(pv57,n5)& leq(pv58,n5)& gt(pv58,pv57)& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n5)& leq(B,n5) )=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,n2) )=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ))& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,n5)& leq(F,n5) )=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) ))& (! [G,H] :( ( leq(n0,G)& leq(n0,H)& leq(G,n5)& leq(H,n5) )=> ( ( G = pv57& gt(pv58,H) )=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) ))& (! [I,J] :( ( leq(n0,I)& leq(n0,J)& leq(I,n5)& leq(J,n5) )=> ( gt(pv57,I)=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) ))& (! [K] :( ( leq(n0,K)& leq(K,pred(pv57)) )=> (! [L] :( ( leq(n0,L)& leq(L,n5) )=> a_select3(id_ds1_filter,K,L) = a_select3(id_ds1_filter,L,K) ) )) ))=> (! [M] :( ( leq(n0,M)& leq(M,pred(pv57)) )=> (! [N] :( ( leq(n0,N)& leq(N,n5) )=> ( ( ~ ( pv57 = N& N = M )& pv57 != M )=> a_select3(id_ds1_filter,M,N) = a_select3(id_ds1_filter,N,M) ) ) )) )) ),
% 4.72/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.72/1.10 fof(f54,negated_conjecture,(
% 4.72/1.10 ~(( ( leq(n0,pv5)& leq(n0,pv57)& leq(pv5,n998)& leq(pv57,n5)& leq(pv58,n5)& gt(pv58,pv57)& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n5)& leq(B,n5) )=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,n2) )=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ))& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,n5)& leq(F,n5) )=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) ))& (! [G,H] :( ( leq(n0,G)& leq(n0,H)& leq(G,n5)& leq(H,n5) )=> ( ( G = pv57& gt(pv58,H) )=> a_select3(id_ds1_filter,G,H) = a_select3(id_ds1_filter,H,G) ) ))& (! [I,J] :( ( leq(n0,I)& leq(n0,J)& leq(I,n5)& leq(J,n5) )=> ( gt(pv57,I)=> a_select3(id_ds1_filter,I,J) = a_select3(id_ds1_filter,J,I) ) ))& (! [K] :( ( leq(n0,K)& leq(K,pred(pv57)) )=> (! [L] :( ( leq(n0,L)& leq(L,n5) )=> a_select3(id_ds1_filter,K,L) = a_select3(id_ds1_filter,L,K) ) )) ))=> (! [M] :( ( leq(n0,M)& leq(M,pred(pv57)) )=> (! [N] :( ( leq(n0,N)& leq(N,n5) )=> ( ( ~ ( pv57 = N& N = M )& pv57 != M )=> a_select3(id_ds1_filter,M,N) = a_select3(id_ds1_filter,N,M) ) ) )) )) )),
% 4.72/1.10 inference(negated_conjecture,[status(cth)],[f53])).
% 4.72/1.10 fof(f204,plain,(
% 4.72/1.10 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 4.72/1.10 inference(cnf_transformation,[status(thm)],[f26])).
% 4.72/1.10 fof(f205,plain,(
% 4.72/1.10 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 4.72/1.10 inference(cnf_transformation,[status(thm)],[f27])).
% 4.72/1.10 fof(f251,plain,(
% 4.72/1.10 ((((((((((((leq(n0,pv5)&leq(n0,pv57))&leq(pv5,n998))&leq(pv57,n5))&leq(pv58,n5))>(pv58,pv57))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n5))|~leq(B,n5))|a_select3(q_ds1_filter,A,B)=a_select3(q_ds1_filter,B,A))))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,n2))|~leq(D,n2))|a_select3(r_ds1_filter,C,D)=a_select3(r_ds1_filter,D,C))))&(![E,F]: ((((~leq(n0,E)|~leq(n0,F))|~leq(E,n5))|~leq(F,n5))|a_select3(pminus_ds1_filter,E,F)=a_select3(pminus_ds1_filter,F,E))))&(![G,H]: ((((~leq(n0,G)|~leq(n0,H))|~leq(G,n5))|~leq(H,n5))|((~G=pv57|~gt(pv58,H))|a_select3(id_ds1_filter,G,H)=a_select3(id_ds1_filter,H,G)))))&(![I,J]: ((((~leq(n0,I)|~leq(n0,J))|~leq(I,n5))|~leq(J,n5))|(~gt(pv57,I)|a_select3(id_ds1_filter,I,J)=a_select3(id_ds1_filter,J,I)))))&(![K]: ((~leq(n0,K)|~leq(K,pred(pv57)))|(![L]: ((~leq(n0,L)|~leq(L,n5))|a_select3(id_ds1_filter,K,L)=a_select3(id_ds1_filter,L,K))))))&(?[M]: ((leq(n0,M)&leq(M,pred(pv57)))&(?[N]: ((leq(n0,N)&leq(N,n5))&(((~pv57=N|~N=M)&~pv57=M)&~a_select3(id_ds1_filter,M,N)=a_select3(id_ds1_filter,N,M)))))))),
% 4.72/1.10 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 4.72/1.11 fof(f252,plain,(
% 4.72/1.11 (((((((((((leq(n0,pv5)&leq(n0,pv57))&leq(pv5,n998))&leq(pv57,n5))&leq(pv58,n5))>(pv58,pv57))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n5))|~leq(B,n5))|a_select3(q_ds1_filter,A,B)=a_select3(q_ds1_filter,B,A))))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,n2))|~leq(D,n2))|a_select3(r_ds1_filter,C,D)=a_select3(r_ds1_filter,D,C))))&(![E,F]: ((((~leq(n0,E)|~leq(n0,F))|~leq(E,n5))|~leq(F,n5))|a_select3(pminus_ds1_filter,E,F)=a_select3(pminus_ds1_filter,F,E))))&(![G,H]: ((((~leq(n0,G)|~leq(n0,H))|~leq(G,n5))|~leq(H,n5))|((~G=pv57|~gt(pv58,H))|a_select3(id_ds1_filter,G,H)=a_select3(id_ds1_filter,H,G)))))&(![I,J]: ((((~leq(n0,I)|~leq(n0,J))|~leq(I,n5))|~leq(J,n5))|(~gt(pv57,I)|a_select3(id_ds1_filter,I,J)=a_select3(id_ds1_filter,J,I)))))&(![K]: ((~leq(n0,K)|~leq(K,pred(pv57)))|(![L]: ((~leq(n0,L)|~leq(L,n5))|a_select3(id_ds1_filter,K,L)=a_select3(id_ds1_filter,L,K))))))&((leq(n0,sK23_skl)&leq(sK23_skl,pred(pv57)))&((leq(n0,sK24_skl)&leq(sK24_skl,n5))&(((~pv57=sK24_skl|~sK24_skl=sK23_skl)&~pv57=sK23_skl)&~a_select3(id_ds1_filter,sK23_skl,sK24_skl)=a_select3(id_ds1_filter,sK24_skl,sK23_skl))))),
% 4.72/1.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(M,sK23_skl),skolemize(N,sK24_skl)],[f251])).
% 4.72/1.11 fof(f264,plain,(
% 4.72/1.11 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv57))|~leq(n0,X1)|~leq(X1,n5)|a_select3(id_ds1_filter,X0,X1)=a_select3(id_ds1_filter,X1,X0))),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f265,plain,(
% 4.72/1.11 leq(n0,sK23_skl)),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f266,plain,(
% 4.72/1.11 leq(sK23_skl,pred(pv57))),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f267,plain,(
% 4.72/1.11 leq(n0,sK24_skl)),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f268,plain,(
% 4.72/1.11 leq(sK24_skl,n5)),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f271,plain,(
% 4.72/1.11 ~a_select3(id_ds1_filter,sK23_skl,sK24_skl)=a_select3(id_ds1_filter,sK24_skl,sK23_skl)),
% 4.72/1.11 inference(cnf_transformation,[status(thm)],[f252])).
% 4.72/1.11 fof(f353,plain,(
% 4.72/1.11 tptp_float_0_0=n0),
% 4.72/1.11 inference(backward_demodulation,[status(thm)],[f205,f204])).
% 4.72/1.11 fof(f410,plain,(
% 4.72/1.11 leq(tptp_float_0_0,sK24_skl)),
% 4.72/1.11 inference(backward_demodulation,[status(thm)],[f353,f267])).
% 4.72/1.11 fof(f411,plain,(
% 4.72/1.11 leq(tptp_float_0_0,sK23_skl)),
% 4.72/1.11 inference(backward_demodulation,[status(thm)],[f353,f265])).
% 4.72/1.11 fof(f412,plain,(
% 4.72/1.11 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv57))|~leq(tptp_float_0_0,X1)|~leq(X1,n5)|a_select3(id_ds1_filter,X0,X1)=a_select3(id_ds1_filter,X1,X0))),
% 4.72/1.11 inference(backward_demodulation,[status(thm)],[f353,f264])).
% 4.72/1.11 fof(f484,plain,(
% 4.72/1.11 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv57))|~leq(tptp_float_0_0,X1)|~leq(X1,n5)|a_select3(id_ds1_filter,X0,X1)=a_select3(id_ds1_filter,X1,X0))),
% 4.72/1.11 inference(forward_demodulation,[status(thm)],[f353,f412])).
% 4.72/1.11 fof(f684,plain,(
% 4.72/1.11 ![X0]: (~leq(tptp_float_0_0,sK23_skl)|~leq(tptp_float_0_0,X0)|~leq(X0,n5)|a_select3(id_ds1_filter,sK23_skl,X0)=a_select3(id_ds1_filter,X0,sK23_skl))),
% 4.72/1.11 inference(resolution,[status(thm)],[f484,f266])).
% 4.72/1.11 fof(f689,plain,(
% 4.72/1.11 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,n5)|a_select3(id_ds1_filter,sK23_skl,X0)=a_select3(id_ds1_filter,X0,sK23_skl))),
% 4.72/1.11 inference(forward_subsumption_resolution,[status(thm)],[f684,f411])).
% 4.72/1.11 fof(f934,plain,(
% 4.72/1.11 ~leq(tptp_float_0_0,sK24_skl)|a_select3(id_ds1_filter,sK23_skl,sK24_skl)=a_select3(id_ds1_filter,sK24_skl,sK23_skl)),
% 4.72/1.11 inference(resolution,[status(thm)],[f689,f268])).
% 4.72/1.11 fof(f940,plain,(
% 4.72/1.11 ~a_select3(id_ds1_filter,sK23_skl,sK24_skl)=a_select3(id_ds1_filter,sK23_skl,sK24_skl)),
% 4.72/1.11 inference(backward_demodulation,[status(thm)],[f941,f271])).
% 4.72/1.11 fof(f941,plain,(
% 4.72/1.11 a_select3(id_ds1_filter,sK23_skl,sK24_skl)=a_select3(id_ds1_filter,sK24_skl,sK23_skl)),
% 4.72/1.11 inference(forward_subsumption_resolution,[status(thm)],[f934,f410])).
% 4.72/1.11 fof(f943,plain,(
% 4.72/1.11 $false),
% 4.72/1.11 inference(trivial_equality_resolution,[status(thm)],[f940])).
% 4.72/1.11 % SZS output end CNFRefutation for theBenchmark.p
% 0.68/1.12 % Elapsed time: 0.738802 seconds
% 0.68/1.12 % CPU time: 5.638809 seconds
% 0.68/1.12 % Total memory used: 155.717 MB
% 0.68/1.12 % Net memory used: 147.509 MB
%------------------------------------------------------------------------------