%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV122+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:06 PM UTC 2026
% Result : Theorem 244.14s 31.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV122+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:31:53 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 244.14/31.17 % Refutation found
% 244.14/31.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 244.14/31.17 % SZS output start CNFRefutation for theBenchmark
% 244.14/31.17 fof(f26,axiom,(
% 244.14/31.17 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 244.14/31.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 244.14/31.17 fof(f27,axiom,(
% 244.14/31.17 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 244.14/31.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 244.14/31.17 fof(f39,axiom,(
% 244.14/31.17 (! [X] : minus(X,n1) = pred(X) )),
% 244.14/31.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 244.14/31.17 fof(f53,conjecture,(
% 244.14/31.17 ( ( (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,minus(n6,n1))& leq(B,minus(n6,n1)) )=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,minus(n3,n1))& leq(D,minus(n3,n1)) )=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ))& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,minus(n6,n1))& leq(F,minus(n6,n1)) )=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) ) ))=> ( (! [G,H] :( ( leq(n0,G)& leq(n0,H)& leq(G,minus(n6,n1))& leq(H,minus(n6,n1)) )=> a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G) ))& (! [I,J] :( ( leq(n0,I)& leq(n0,J)& leq(I,minus(n3,n1))& leq(J,minus(n3,n1)) )=> a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I) ))& (! [K,L] :( ( leq(n0,K)& leq(n0,L)& leq(K,minus(n6,n1))& leq(L,minus(n6,n1)) )=> a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_ds1_filter,L,K) ) )) ) ),
% 244.14/31.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 244.14/31.17 fof(f54,negated_conjecture,(
% 244.14/31.17 ~(( ( (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,minus(n6,n1))& leq(B,minus(n6,n1)) )=> a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,minus(n3,n1))& leq(D,minus(n3,n1)) )=> a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ))& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,minus(n6,n1))& leq(F,minus(n6,n1)) )=> a_select3(pminus_ds1_filter,E,F) = a_select3(pminus_ds1_filter,F,E) ) ))=> ( (! [G,H] :( ( leq(n0,G)& leq(n0,H)& leq(G,minus(n6,n1))& leq(H,minus(n6,n1)) )=> a_select3(q_ds1_filter,G,H) = a_select3(q_ds1_filter,H,G) ))& (! [I,J] :( ( leq(n0,I)& leq(n0,J)& leq(I,minus(n3,n1))& leq(J,minus(n3,n1)) )=> a_select3(r_ds1_filter,I,J) = a_select3(r_ds1_filter,J,I) ))& (! [K,L] :( ( leq(n0,K)& leq(n0,L)& leq(K,minus(n6,n1))& leq(L,minus(n6,n1)) )=> a_select3(pminus_ds1_filter,K,L) = a_select3(pminus_ds1_filter,L,K) ) )) ) )),
% 244.14/31.17 inference(negated_conjecture,[status(cth)],[f53])).
% 244.14/31.17 fof(f206,plain,(
% 244.14/31.17 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f26])).
% 244.14/31.17 fof(f207,plain,(
% 244.14/31.17 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f27])).
% 244.14/31.17 fof(f219,plain,(
% 244.14/31.17 ![X0]: (minus(X0,n1)=pred(X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f39])).
% 244.14/31.17 fof(f253,plain,(
% 244.14/31.17 ((((![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,minus(n6,n1)))|~leq(B,minus(n6,n1)))|a_select3(q_ds1_filter,A,B)=a_select3(q_ds1_filter,B,A)))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,minus(n3,n1)))|~leq(D,minus(n3,n1)))|a_select3(r_ds1_filter,C,D)=a_select3(r_ds1_filter,D,C))))&(![E,F]: ((((~leq(n0,E)|~leq(n0,F))|~leq(E,minus(n6,n1)))|~leq(F,minus(n6,n1)))|a_select3(pminus_ds1_filter,E,F)=a_select3(pminus_ds1_filter,F,E))))&(((?[G,H]: ((((leq(n0,G)&leq(n0,H))&leq(G,minus(n6,n1)))&leq(H,minus(n6,n1)))&~a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G)))|(?[I,J]: ((((leq(n0,I)&leq(n0,J))&leq(I,minus(n3,n1)))&leq(J,minus(n3,n1)))&~a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I))))|(?[K,L]: ((((leq(n0,K)&leq(n0,L))&leq(K,minus(n6,n1)))&leq(L,minus(n6,n1)))&~a_select3(pminus_ds1_filter,K,L)=a_select3(pminus_ds1_filter,L,K)))))),
% 244.14/31.17 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 244.14/31.17 fof(f254,definition,(
% 244.14/31.17 sP3_prd<=>((?[G,H]: ((((leq(n0,G)&leq(n0,H))&leq(G,minus(n6,n1)))&leq(H,minus(n6,n1)))&~a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G)))|(?[I,J]: ((((leq(n0,I)&leq(n0,J))&leq(I,minus(n3,n1)))&leq(J,minus(n3,n1)))&~a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I))))),
% 244.14/31.17 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 244.14/31.17 fof(f255,plain,(
% 244.14/31.17 (((![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,minus(n6,n1)))|~leq(B,minus(n6,n1)))|a_select3(q_ds1_filter,A,B)=a_select3(q_ds1_filter,B,A)))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,minus(n3,n1)))|~leq(D,minus(n3,n1)))|a_select3(r_ds1_filter,C,D)=a_select3(r_ds1_filter,D,C))))&(![E,F]: ((((~leq(n0,E)|~leq(n0,F))|~leq(E,minus(n6,n1)))|~leq(F,minus(n6,n1)))|a_select3(pminus_ds1_filter,E,F)=a_select3(pminus_ds1_filter,F,E))))&(sP3_prd|(?[K,L]: ((((leq(n0,K)&leq(n0,L))&leq(K,minus(n6,n1)))&leq(L,minus(n6,n1)))&~a_select3(pminus_ds1_filter,K,L)=a_select3(pminus_ds1_filter,L,K))))),
% 244.14/31.17 inference(formula_renaming,[status(thm)],[f253,f254])).
% 244.14/31.17 fof(f256,plain,(
% 244.14/31.17 (((![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,minus(n6,n1)))|~leq(B,minus(n6,n1)))|a_select3(q_ds1_filter,A,B)=a_select3(q_ds1_filter,B,A)))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,minus(n3,n1)))|~leq(D,minus(n3,n1)))|a_select3(r_ds1_filter,C,D)=a_select3(r_ds1_filter,D,C))))&(![E,F]: ((((~leq(n0,E)|~leq(n0,F))|~leq(E,minus(n6,n1)))|~leq(F,minus(n6,n1)))|a_select3(pminus_ds1_filter,E,F)=a_select3(pminus_ds1_filter,F,E))))&(sP3_prd|((((leq(n0,sK23_skl)&leq(n0,sK24_skl))&leq(sK23_skl,minus(n6,n1)))&leq(sK24_skl,minus(n6,n1)))&~a_select3(pminus_ds1_filter,sK23_skl,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)))),
% 244.14/31.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(K,sK23_skl),skolemize(L,sK24_skl)],[f255])).
% 244.14/31.17 fof(f257,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,minus(n6,n1))|~leq(X1,minus(n6,n1))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f258,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,minus(n3,n1))|~leq(X1,minus(n3,n1))|a_select3(r_ds1_filter,X0,X1)=a_select3(r_ds1_filter,X1,X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f259,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,minus(n6,n1))|~leq(X1,minus(n6,n1))|a_select3(pminus_ds1_filter,X0,X1)=a_select3(pminus_ds1_filter,X1,X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f260,plain,(
% 244.14/31.17 sP3_prd|leq(n0,sK23_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f261,plain,(
% 244.14/31.17 sP3_prd|leq(n0,sK24_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f262,plain,(
% 244.14/31.17 sP3_prd|leq(sK23_skl,minus(n6,n1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f263,plain,(
% 244.14/31.17 sP3_prd|leq(sK24_skl,minus(n6,n1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f264,plain,(
% 244.14/31.17 sP3_prd|~a_select3(pminus_ds1_filter,sK23_skl,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f256])).
% 244.14/31.17 fof(f341,definition,(
% 244.14/31.17 ![G,H]: (sP5_prd(H,G)<=>((((leq(n0,G)&leq(n0,H))&leq(G,minus(n6,n1)))&leq(H,minus(n6,n1)))&~a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G)))),
% 244.14/31.17 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 244.14/31.17 fof(f342,plain,(
% 244.14/31.17 sP3_prd<=>((?[G,H]: sP5_prd(H,G))|(?[I,J]: ((((leq(n0,I)&leq(n0,J))&leq(I,minus(n3,n1)))&leq(J,minus(n3,n1)))&~a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I))))),
% 244.14/31.17 inference(formula_renaming,[status(thm)],[f254,f341])).
% 244.14/31.17 fof(f343,plain,(
% 244.14/31.17 (~sP3_prd|((?[G,H]: sP5_prd(H,G))|(?[I,J]: ((((leq(n0,I)&leq(n0,J))&leq(I,minus(n3,n1)))&leq(J,minus(n3,n1)))&~a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I)))))&(sP3_prd|((![G,H]: ~sP5_prd(H,G))&(![I,J]: ((((~leq(n0,I)|~leq(n0,J))|~leq(I,minus(n3,n1)))|~leq(J,minus(n3,n1)))|a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I)))))),
% 244.14/31.17 inference(NNF_transformation,[status(thm)],[f342])).
% 244.14/31.17 fof(f344,plain,(
% 244.14/31.17 (~sP3_prd|(sP5_prd(sK30_skl,sK29_skl)|((((leq(n0,sK31_skl)&leq(n0,sK32_skl))&leq(sK31_skl,minus(n3,n1)))&leq(sK32_skl,minus(n3,n1)))&~a_select3(r_ds1_filter,sK31_skl,sK32_skl)=a_select3(r_ds1_filter,sK32_skl,sK31_skl))))&(sP3_prd|((![G,H]: ~sP5_prd(H,G))&(![I,J]: ((((~leq(n0,I)|~leq(n0,J))|~leq(I,minus(n3,n1)))|~leq(J,minus(n3,n1)))|a_select3(r_ds1_filter,I,J)=a_select3(r_ds1_filter,J,I)))))),
% 244.14/31.17 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl,sK31_skl,sK32_skl]),skolemize(G,sK29_skl),skolemize(H,sK30_skl),skolemize(I,sK31_skl),skolemize(J,sK32_skl)],[f343])).
% 244.14/31.17 fof(f345,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(n0,sK31_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f344])).
% 244.14/31.17 fof(f346,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(n0,sK32_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f344])).
% 244.14/31.17 fof(f347,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(sK31_skl,minus(n3,n1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f344])).
% 244.14/31.17 fof(f348,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(sK32_skl,minus(n3,n1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f344])).
% 244.14/31.17 fof(f349,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|~a_select3(r_ds1_filter,sK31_skl,sK32_skl)=a_select3(r_ds1_filter,sK32_skl,sK31_skl)),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f344])).
% 244.14/31.17 fof(f360,plain,(
% 244.14/31.17 ![G,H]: ((~sP5_prd(H,G)|((((leq(n0,G)&leq(n0,H))&leq(G,minus(n6,n1)))&leq(H,minus(n6,n1)))&~a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G)))&(sP5_prd(H,G)|((((~leq(n0,G)|~leq(n0,H))|~leq(G,minus(n6,n1)))|~leq(H,minus(n6,n1)))|a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G))))),
% 244.14/31.17 inference(NNF_transformation,[status(thm)],[f341])).
% 244.14/31.17 fof(f361,plain,(
% 244.14/31.17 (![G,H]: (~sP5_prd(H,G)|((((leq(n0,G)&leq(n0,H))&leq(G,minus(n6,n1)))&leq(H,minus(n6,n1)))&~a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G))))&(![G,H]: (sP5_prd(H,G)|((((~leq(n0,G)|~leq(n0,H))|~leq(G,minus(n6,n1)))|~leq(H,minus(n6,n1)))|a_select3(q_ds1_filter,G,H)=a_select3(q_ds1_filter,H,G))))),
% 244.14/31.17 inference(miniscoping,[status(thm)],[f360])).
% 244.14/31.17 fof(f362,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(n0,X1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f361])).
% 244.14/31.17 fof(f363,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(n0,X0))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f361])).
% 244.14/31.17 fof(f364,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(X1,minus(n6,n1)))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f361])).
% 244.14/31.17 fof(f365,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(X0,minus(n6,n1)))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f361])).
% 244.14/31.17 fof(f366,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|~a_select3(q_ds1_filter,X1,X0)=a_select3(q_ds1_filter,X0,X1))),
% 244.14/31.17 inference(cnf_transformation,[status(thm)],[f361])).
% 244.14/31.17 fof(f368,plain,(
% 244.14/31.17 tptp_float_0_0=n0),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f207,f206])).
% 244.14/31.17 fof(f383,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n6))|~leq(X1,minus(n6,n1))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f257])).
% 244.14/31.17 fof(f384,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f383])).
% 244.14/31.17 fof(f385,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n3))|~leq(X1,minus(n3,n1))|a_select3(r_ds1_filter,X0,X1)=a_select3(r_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f258])).
% 244.14/31.17 fof(f386,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n3))|~leq(X1,pred(n3))|a_select3(r_ds1_filter,X0,X1)=a_select3(r_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f385])).
% 244.14/31.17 fof(f387,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n6))|~leq(X1,minus(n6,n1))|a_select3(pminus_ds1_filter,X0,X1)=a_select3(pminus_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f259])).
% 244.14/31.17 fof(f388,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(pminus_ds1_filter,X0,X1)=a_select3(pminus_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f387])).
% 244.14/31.17 fof(f389,plain,(
% 244.14/31.17 sP3_prd|leq(sK23_skl,pred(n6))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f262])).
% 244.14/31.17 fof(f390,plain,(
% 244.14/31.17 sP3_prd|leq(sK24_skl,pred(n6))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f263])).
% 244.14/31.17 fof(f406,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(sK31_skl,pred(n3))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f347])).
% 244.14/31.17 fof(f407,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(sK32_skl,pred(n3))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f348])).
% 244.14/31.17 fof(f410,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(X1,pred(n6)))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f364])).
% 244.14/31.17 fof(f411,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(X0,pred(n6)))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f219,f365])).
% 244.14/31.17 fof(f414,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(tptp_float_0_0,X0))),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f363])).
% 244.14/31.17 fof(f415,plain,(
% 244.14/31.17 ![X0,X1]: (~sP5_prd(X0,X1)|leq(tptp_float_0_0,X1))),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f362])).
% 244.14/31.17 fof(f419,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(tptp_float_0_0,sK32_skl)),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f346])).
% 244.14/31.17 fof(f420,plain,(
% 244.14/31.17 ~sP3_prd|sP5_prd(sK30_skl,sK29_skl)|leq(tptp_float_0_0,sK31_skl)),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f345])).
% 244.14/31.17 fof(f449,plain,(
% 244.14/31.17 sP3_prd|leq(tptp_float_0_0,sK24_skl)),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f261])).
% 244.14/31.17 fof(f450,plain,(
% 244.14/31.17 sP3_prd|leq(tptp_float_0_0,sK23_skl)),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f260])).
% 244.14/31.17 fof(f451,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(pminus_ds1_filter,X0,X1)=a_select3(pminus_ds1_filter,X1,X0))),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f388])).
% 244.14/31.17 fof(f452,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n3))|~leq(X1,pred(n3))|a_select3(r_ds1_filter,X0,X1)=a_select3(r_ds1_filter,X1,X0))),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f386])).
% 244.14/31.17 fof(f453,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0))),
% 244.14/31.17 inference(backward_demodulation,[status(thm)],[f368,f384])).
% 244.14/31.17 fof(f520,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(pminus_ds1_filter,X0,X1)=a_select3(pminus_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f368,f451])).
% 244.14/31.17 fof(f521,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n3))|~leq(X1,pred(n3))|a_select3(r_ds1_filter,X0,X1)=a_select3(r_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f368,f452])).
% 244.14/31.17 fof(f522,plain,(
% 244.14/31.17 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n6))|~leq(X1,pred(n6))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0))),
% 244.14/31.17 inference(forward_demodulation,[status(thm)],[f368,f453])).
% 244.14/31.17 fof(f654,plain,(
% 244.14/31.17 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,sK24_skl)|~leq(X0,pred(n6))|a_select3(pminus_ds1_filter,X0,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,X0)|sP3_prd)),
% 244.14/31.17 inference(resolution,[status(thm)],[f520,f390])).
% 244.14/31.17 fof(f663,plain,(
% 244.14/31.17 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(n6))|a_select3(pminus_ds1_filter,X0,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,X0)|sP3_prd)),
% 244.14/31.17 inference(forward_subsumption_resolution,[status(thm)],[f654,f449])).
% 244.14/31.17 fof(f669,plain,(
% 244.14/31.17 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,sK31_skl)|~leq(X0,pred(n3))|a_select3(r_ds1_filter,X0,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,X0)|~sP3_prd|sP5_prd(sK30_skl,sK29_skl))),
% 244.14/31.17 inference(resolution,[status(thm)],[f521,f406])).
% 244.14/31.17 fof(f676,plain,(
% 244.14/31.17 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(n3))|a_select3(r_ds1_filter,X0,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,X0)|~sP3_prd|sP5_prd(sK30_skl,sK29_skl))),
% 244.14/31.17 inference(forward_subsumption_resolution,[status(thm)],[f669,f420])).
% 244.14/31.17 fof(f681,plain,(
% 244.14/31.17 ![X0,X1,X2]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,pred(n6))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0)|~sP5_prd(X2,X1))),
% 244.14/31.17 inference(resolution,[status(thm)],[f522,f410])).
% 244.14/31.17 fof(f690,plain,(
% 244.14/31.17 ![X0,X1,X2]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(n6))|a_select3(q_ds1_filter,X0,X1)=a_select3(q_ds1_filter,X1,X0)|~sP5_prd(X2,X1))),
% 244.14/31.17 inference(forward_subsumption_resolution,[status(thm)],[f681,f415])).
% 244.14/31.17 fof(f766,plain,(
% 244.14/31.17 ~leq(tptp_float_0_0,sK23_skl)|a_select3(pminus_ds1_filter,sK23_skl,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)|sP3_prd|sP3_prd),
% 244.14/31.20 inference(resolution,[status(thm)],[f663,f389])).
% 244.14/31.20 fof(f774,plain,(
% 244.14/31.20 ~leq(tptp_float_0_0,sK23_skl)|a_select3(pminus_ds1_filter,sK23_skl,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)|sP3_prd),
% 244.14/31.20 inference(duplicate_literals_removal,[status(thm)],[f766])).
% 244.14/31.20 fof(f775,plain,(
% 244.14/31.20 sP3_prd),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f264,f776])).
% 244.14/31.20 fof(f776,plain,(
% 244.14/31.20 a_select3(pminus_ds1_filter,sK23_skl,sK24_skl)=a_select3(pminus_ds1_filter,sK24_skl,sK23_skl)|sP3_prd),
% 244.14/31.20 inference(forward_subsumption_resolution,[status(thm)],[f774,f450])).
% 244.14/31.20 fof(f778,plain,(
% 244.14/31.20 sP5_prd(sK30_skl,sK29_skl)|~a_select3(r_ds1_filter,sK31_skl,sK32_skl)=a_select3(r_ds1_filter,sK32_skl,sK31_skl)),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f349,f775])).
% 244.14/31.20 fof(f779,plain,(
% 244.14/31.20 sP5_prd(sK30_skl,sK29_skl)|leq(sK32_skl,pred(n3))),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f407,f775])).
% 244.14/31.20 fof(f785,plain,(
% 244.14/31.20 sP5_prd(sK30_skl,sK29_skl)|leq(tptp_float_0_0,sK32_skl)),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f419,f775])).
% 244.14/31.20 fof(f790,plain,(
% 244.14/31.20 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(n3))|a_select3(r_ds1_filter,X0,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,X0)|sP5_prd(sK30_skl,sK29_skl))),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f676,f775])).
% 244.14/31.20 fof(f963,plain,(
% 244.14/31.20 ~leq(tptp_float_0_0,sK32_skl)|a_select3(r_ds1_filter,sK32_skl,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,sK32_skl)|sP5_prd(sK30_skl,sK29_skl)|sP5_prd(sK30_skl,sK29_skl)),
% 244.14/31.20 inference(resolution,[status(thm)],[f790,f779])).
% 244.14/31.20 fof(f969,plain,(
% 244.14/31.20 ~leq(tptp_float_0_0,sK32_skl)|a_select3(r_ds1_filter,sK32_skl,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,sK32_skl)|sP5_prd(sK30_skl,sK29_skl)),
% 244.14/31.20 inference(duplicate_literals_removal,[status(thm)],[f963])).
% 244.14/31.20 fof(f970,plain,(
% 244.14/31.20 sP5_prd(sK30_skl,sK29_skl)),
% 244.14/31.20 inference(backward_subsumption_resolution,[status(thm)],[f778,f971])).
% 244.14/31.20 fof(f971,plain,(
% 244.14/31.20 a_select3(r_ds1_filter,sK32_skl,sK31_skl)=a_select3(r_ds1_filter,sK31_skl,sK32_skl)|sP5_prd(sK30_skl,sK29_skl)),
% 244.14/31.20 inference(forward_subsumption_resolution,[status(thm)],[f969,f785])).
% 244.14/31.20 fof(f1112,plain,(
% 244.14/31.20 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(n6))|a_select3(q_ds1_filter,X0,sK29_skl)=a_select3(q_ds1_filter,sK29_skl,X0))),
% 244.14/31.20 inference(resolution,[status(thm)],[f970,f690])).
% 244.14/31.20 fof(f1550,plain,(
% 244.14/31.20 ![X0,X1]: (~leq(tptp_float_0_0,X0)|a_select3(q_ds1_filter,X0,sK29_skl)=a_select3(q_ds1_filter,sK29_skl,X0)|~sP5_prd(X0,X1))),
% 244.14/31.20 inference(resolution,[status(thm)],[f1112,f411])).
% 244.14/31.20 fof(f1557,plain,(
% 244.14/31.20 ![X0,X1]: (a_select3(q_ds1_filter,X0,sK29_skl)=a_select3(q_ds1_filter,sK29_skl,X0)|~sP5_prd(X0,X1))),
% 244.14/31.20 inference(forward_subsumption_resolution,[status(thm)],[f1550,f414])).
% 244.14/31.20 fof(f2596,plain,(
% 244.14/31.20 a_select3(q_ds1_filter,sK30_skl,sK29_skl)=a_select3(q_ds1_filter,sK29_skl,sK30_skl)),
% 244.14/31.20 inference(resolution,[status(thm)],[f1557,f970])).
% 244.14/31.20 fof(f5124,plain,(
% 244.14/31.20 ~sP5_prd(sK30_skl,sK29_skl)),
% 244.14/31.20 inference(resolution,[status(thm)],[f2596,f366])).
% 244.14/31.20 fof(f5127,plain,(
% 244.14/31.20 $false),
% 244.14/31.20 inference(forward_subsumption_resolution,[status(thm)],[f5124,f970])).
% 244.14/31.20 % SZS output end CNFRefutation for theBenchmark.p
% 176.30/31.27 % Elapsed time: 30.901607 seconds
% 176.30/31.27 % CPU time: 245.442803 seconds
% 176.30/31.27 % Total memory used: 958.250 MB
% 176.30/31.27 % Net memory used: 812.946 MB
%------------------------------------------------------------------------------