%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV174+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 : n017.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:11 PM UTC 2026
% Result : Theorem 1.23s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV174+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.08/0.35 % Computer : n017.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:29:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 1.23/0.64 % Refutation found
% 1.23/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.23/0.64 % SZS output start CNFRefutation for theBenchmark
% 1.23/0.64 fof(f10,axiom,(
% 1.23/0.64 (! [X,Y] :( leq(X,pred(Y))<=> gt(Y,X) ) )),
% 1.23/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.23/0.64 fof(f53,conjecture,(
% 1.23/0.64 ( ( leq(n0,pv10)& leq(pv10,n135299)& (! [A] :( ( leq(n0,A)& leq(A,pred(pv10)) )=> (! [B] :( ( leq(n0,B)& leq(B,n4) )=> a_select3(q_init,A,B) = init ) )))& (! [C] :( ( leq(n0,C)& leq(C,n4) )=> a_select3(center_init,C,n0) = init ) ))=> (! [D,E] :( ( leq(n0,D)& leq(n0,E)& leq(D,n135299)& leq(E,n4) )=> ( gt(pv10,D)=> a_select3(q_init,D,E) = init ) ) )) ),
% 1.23/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.23/0.64 fof(f54,negated_conjecture,(
% 1.23/0.64 ~(( ( leq(n0,pv10)& leq(pv10,n135299)& (! [A] :( ( leq(n0,A)& leq(A,pred(pv10)) )=> (! [B] :( ( leq(n0,B)& leq(B,n4) )=> a_select3(q_init,A,B) = init ) )))& (! [C] :( ( leq(n0,C)& leq(C,n4) )=> a_select3(center_init,C,n0) = init ) ))=> (! [D,E] :( ( leq(n0,D)& leq(n0,E)& leq(D,n135299)& leq(E,n4) )=> ( gt(pv10,D)=> a_select3(q_init,D,E) = init ) ) )) )),
% 1.23/0.64 inference(negated_conjecture,[status(cth)],[f53])).
% 1.23/0.64 fof(f115,plain,(
% 1.23/0.64 ![X,Y]: ((~leq(X,pred(Y))|gt(Y,X))&(leq(X,pred(Y))|~gt(Y,X)))),
% 1.23/0.64 inference(NNF_transformation,[status(thm)],[f10])).
% 1.23/0.64 fof(f116,plain,(
% 1.23/0.64 (![X,Y]: (~leq(X,pred(Y))|gt(Y,X)))&(![X,Y]: (leq(X,pred(Y))|~gt(Y,X)))),
% 1.23/0.64 inference(miniscoping,[status(thm)],[f115])).
% 1.23/0.64 fof(f118,plain,(
% 1.23/0.64 ![X0,X1]: (leq(X0,pred(X1))|~gt(X1,X0))),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f116])).
% 1.23/0.64 fof(f251,plain,(
% 1.23/0.64 ((((leq(n0,pv10)&leq(pv10,n135299))&(![A]: ((~leq(n0,A)|~leq(A,pred(pv10)))|(![B]: ((~leq(n0,B)|~leq(B,n4))|a_select3(q_init,A,B)=init)))))&(![C]: ((~leq(n0,C)|~leq(C,n4))|a_select3(center_init,C,n0)=init)))&(?[D,E]: ((((leq(n0,D)&leq(n0,E))&leq(D,n135299))&leq(E,n4))&(gt(pv10,D)&~a_select3(q_init,D,E)=init))))),
% 1.23/0.64 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 1.23/0.64 fof(f252,plain,(
% 1.23/0.64 (((leq(n0,pv10)&leq(pv10,n135299))&(![A]: ((~leq(n0,A)|~leq(A,pred(pv10)))|(![B]: ((~leq(n0,B)|~leq(B,n4))|a_select3(q_init,A,B)=init)))))&(![C]: ((~leq(n0,C)|~leq(C,n4))|a_select3(center_init,C,n0)=init)))&((((leq(n0,sK23_skl)&leq(n0,sK24_skl))&leq(sK23_skl,n135299))&leq(sK24_skl,n4))&(gt(pv10,sK23_skl)&~a_select3(q_init,sK23_skl,sK24_skl)=init))),
% 1.23/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(D,sK23_skl),skolemize(E,sK24_skl)],[f251])).
% 1.23/0.64 fof(f255,plain,(
% 1.23/0.64 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv10))|~leq(n0,X1)|~leq(X1,n4)|a_select3(q_init,X0,X1)=init)),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f257,plain,(
% 1.23/0.64 leq(n0,sK23_skl)),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f258,plain,(
% 1.23/0.64 leq(n0,sK24_skl)),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f260,plain,(
% 1.23/0.64 leq(sK24_skl,n4)),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f261,plain,(
% 1.23/0.64 gt(pv10,sK23_skl)),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f262,plain,(
% 1.23/0.64 ~a_select3(q_init,sK23_skl,sK24_skl)=init),
% 1.23/0.64 inference(cnf_transformation,[status(thm)],[f252])).
% 1.23/0.64 fof(f354,plain,(
% 1.23/0.64 leq(sK23_skl,pred(pv10))),
% 1.23/0.64 inference(resolution,[status(thm)],[f261,f118])).
% 1.23/0.64 fof(f398,plain,(
% 1.23/0.64 ![X0]: (~leq(n0,sK23_skl)|~leq(n0,X0)|~leq(X0,n4)|a_select3(q_init,sK23_skl,X0)=init)),
% 1.23/0.64 inference(resolution,[status(thm)],[f354,f255])).
% 1.23/0.64 fof(f401,definition,(
% 1.23/0.64 sQ2_spl <=> (leq(n0,sK23_skl))),
% 1.23/0.64 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.23/0.64 fof(f403,plain,(
% 1.23/0.64 ~leq(n0,sK23_skl)|sQ2_spl),
% 1.23/0.64 inference(component_clause,[status(thm)],[f401])).
% 1.23/0.64 fof(f404,definition,(
% 1.23/0.64 ![X0]: (sQ3_spl <=> (~leq(n0,X0)|~leq(X0,n4)|a_select3(q_init,sK23_skl,X0)=init))),
% 1.23/0.64 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.23/0.64 fof(f405,plain,(
% 1.23/0.64 ![X0]: (~leq(n0,X0)|~leq(X0,n4)|a_select3(q_init,sK23_skl,X0)=init|~sQ3_spl)),
% 1.23/0.64 inference(component_clause,[status(thm)],[f404])).
% 1.23/0.64 fof(f407,plain,(
% 1.23/0.64 ~sQ2_spl|sQ3_spl),
% 1.23/0.64 inference(split_clause,[status(thm)],[f398,f401,f404])).
% 1.23/0.64 fof(f408,plain,(
% 1.23/0.64 $false|sQ2_spl),
% 1.23/0.64 inference(forward_subsumption_resolution,[status(thm)],[f403,f257])).
% 1.23/0.65 fof(f409,plain,(
% 1.23/0.65 sQ2_spl),
% 1.23/0.65 inference(contradiction_clause,[status(thm)],[f408])).
% 1.23/0.65 fof(f429,definition,(
% 1.23/0.65 sQ4_spl <=> (leq(n0,sK24_skl))),
% 1.23/0.65 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.23/0.65 fof(f431,plain,(
% 1.23/0.65 ~leq(n0,sK24_skl)|sQ4_spl),
% 1.23/0.65 inference(component_clause,[status(thm)],[f429])).
% 1.23/0.65 fof(f443,plain,(
% 1.23/0.65 $false|sQ4_spl),
% 1.23/0.65 inference(forward_subsumption_resolution,[status(thm)],[f431,f258])).
% 1.23/0.65 fof(f444,plain,(
% 1.23/0.65 sQ4_spl),
% 1.23/0.65 inference(contradiction_clause,[status(thm)],[f443])).
% 1.23/0.65 fof(f981,plain,(
% 1.23/0.65 ~leq(n0,sK24_skl)|a_select3(q_init,sK23_skl,sK24_skl)=init|~sQ3_spl),
% 1.23/0.65 inference(resolution,[status(thm)],[f405,f260])).
% 1.23/0.65 fof(f994,definition,(
% 1.23/0.65 sQ27_spl <=> (a_select3(q_init,sK23_skl,sK24_skl)=init)),
% 1.23/0.65 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.23/0.65 fof(f995,plain,(
% 1.23/0.65 a_select3(q_init,sK23_skl,sK24_skl)=init|~sQ27_spl),
% 1.23/0.65 inference(component_clause,[status(thm)],[f994])).
% 1.23/0.65 fof(f997,plain,(
% 1.23/0.65 ~sQ4_spl|sQ27_spl|~sQ3_spl),
% 1.23/0.65 inference(split_clause,[status(thm)],[f981,f429,f994,f404])).
% 1.23/0.65 fof(f1006,plain,(
% 1.23/0.65 $false|~sQ27_spl),
% 1.23/0.65 inference(forward_subsumption_resolution,[status(thm)],[f995,f262])).
% 1.23/0.65 fof(f1007,plain,(
% 1.23/0.65 ~sQ27_spl),
% 1.23/0.65 inference(contradiction_clause,[status(thm)],[f1006])).
% 1.23/0.65 fof(f1008,plain,(
% 1.23/0.65 $false),
% 1.23/0.65 inference(sat_refutation,[status(thm)],[f407,f409,f444,f997,f1007])).
% 1.23/0.65 % SZS output end CNFRefutation for theBenchmark.p
% 1.23/0.67 % Elapsed time: 0.295699 seconds
% 1.23/0.67 % CPU time: 2.045451 seconds
% 1.23/0.67 % Total memory used: 130.358 MB
% 1.23/0.67 % Net memory used: 126.463 MB
%------------------------------------------------------------------------------