%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV373+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:40 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV373+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:41:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f27,axiom,(
% 0.09/0.39 (! [U,V,W,X] :( contains_cpq(triple(U,V,W),X)<=> contains_slb(V,X) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f39,axiom,(
% 0.09/0.39 (! [U,V,W,X] :( V != create_slb=> findmin_cpq_res(triple(U,V,W)) = findmin_pqp_res(U) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f42,lemma,(
% 0.09/0.39 (! [U,V,W] :( ok(findmin_cpq_eff(triple(U,V,W)))=> ( V != create_slb& contains_slb(V,findmin_pqp_res(U))& less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U)) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f43,conjecture,(
% 0.09/0.39 (! [U,V,W] :( ~ contains_cpq(triple(U,V,W),findmin_cpq_res(triple(U,V,W)))=> ~ ok(findmin_cpq_eff(triple(U,V,W))) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f44,negated_conjecture,(
% 0.09/0.39 ~((! [U,V,W] :( ~ contains_cpq(triple(U,V,W),findmin_cpq_res(triple(U,V,W)))=> ~ ok(findmin_cpq_eff(triple(U,V,W))) ) ))),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f43])).
% 0.09/0.39 fof(f108,plain,(
% 0.09/0.39 ![U,V,W,X]: ((~contains_cpq(triple(U,V,W),X)|contains_slb(V,X))&(contains_cpq(triple(U,V,W),X)|~contains_slb(V,X)))),
% 0.09/0.39 inference(NNF_transformation,[status(thm)],[f27])).
% 0.09/0.39 fof(f109,plain,(
% 0.09/0.39 (![V,X]: ((![U,W]: ~contains_cpq(triple(U,V,W),X))|contains_slb(V,X)))&(![V,X]: ((![U,W]: contains_cpq(triple(U,V,W),X))|~contains_slb(V,X)))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f108])).
% 0.09/0.39 fof(f111,plain,(
% 0.09/0.39 ![X0,X1,X2,X3]: (contains_cpq(triple(X0,X1,X2),X3)|~contains_slb(X1,X3))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f109])).
% 0.09/0.39 fof(f140,plain,(
% 0.09/0.39 ![U,V,W,X]: (V=create_slb|findmin_cpq_res(triple(U,V,W))=findmin_pqp_res(U))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.09/0.39 fof(f141,plain,(
% 0.09/0.39 ![V]: (V=create_slb|(![U,W]: findmin_cpq_res(triple(U,V,W))=findmin_pqp_res(U)))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f140])).
% 0.09/0.39 fof(f142,plain,(
% 0.09/0.39 ![X0,X1,X2]: (X0=create_slb|findmin_cpq_res(triple(X1,X0,X2))=findmin_pqp_res(X1))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f141])).
% 0.09/0.39 fof(f145,plain,(
% 0.09/0.39 ![U,V,W]: (~ok(findmin_cpq_eff(triple(U,V,W)))|((~V=create_slb&contains_slb(V,findmin_pqp_res(U)))&less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.09/0.39 fof(f146,plain,(
% 0.09/0.39 ![U,V]: ((![W]: ~ok(findmin_cpq_eff(triple(U,V,W))))|((~V=create_slb&contains_slb(V,findmin_pqp_res(U)))&less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f145])).
% 0.09/0.39 fof(f147,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ok(findmin_cpq_eff(triple(X0,X1,X2)))|~X1=create_slb)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f146])).
% 0.09/0.39 fof(f148,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ok(findmin_cpq_eff(triple(X0,X1,X2)))|contains_slb(X1,findmin_pqp_res(X0)))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f146])).
% 0.09/0.39 fof(f150,plain,(
% 0.09/0.39 (?[U,V,W]: (~contains_cpq(triple(U,V,W),findmin_cpq_res(triple(U,V,W)))&ok(findmin_cpq_eff(triple(U,V,W)))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.09/0.39 fof(f151,plain,(
% 0.09/0.39 (~contains_cpq(triple(sK0_skl,sK1_skl,sK2_skl),findmin_cpq_res(triple(sK0_skl,sK1_skl,sK2_skl)))&ok(findmin_cpq_eff(triple(sK0_skl,sK1_skl,sK2_skl))))),
% 0.09/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl),skolemize(W,sK2_skl)],[f150])).
% 0.09/0.39 fof(f152,plain,(
% 0.09/0.39 ~contains_cpq(triple(sK0_skl,sK1_skl,sK2_skl),findmin_cpq_res(triple(sK0_skl,sK1_skl,sK2_skl)))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f151])).
% 0.09/0.39 fof(f153,plain,(
% 0.09/0.39 ok(findmin_cpq_eff(triple(sK0_skl,sK1_skl,sK2_skl)))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f151])).
% 0.09/0.39 fof(f156,plain,(
% 0.09/0.39 ![X0,X1]: (~ok(findmin_cpq_eff(triple(X0,create_slb,X1))))),
% 0.09/0.39 inference(destructive_equality_resolution,[status(thm)],[f147])).
% 0.09/0.39 fof(f158,plain,(
% 0.09/0.39 ~contains_cpq(triple(sK0_skl,sK1_skl,sK2_skl),findmin_pqp_res(sK0_skl))|sK1_skl=create_slb),
% 0.09/0.39 inference(paramodulation,[status(thm)],[f142,f152])).
% 0.09/0.39 fof(f159,definition,(
% 0.09/0.39 sQ0_spl <=> (contains_cpq(triple(sK0_skl,sK1_skl,sK2_skl),findmin_pqp_res(sK0_skl)))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f161,plain,(
% 0.09/0.40 ~contains_cpq(triple(sK0_skl,sK1_skl,sK2_skl),findmin_pqp_res(sK0_skl))|sQ0_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f159])).
% 0.09/0.40 fof(f162,definition,(
% 0.09/0.40 sQ1_spl <=> (sK1_skl=create_slb)),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f163,plain,(
% 0.09/0.40 sK1_skl=create_slb|~sQ1_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f162])).
% 0.09/0.40 fof(f165,plain,(
% 0.09/0.40 ~sQ0_spl|sQ1_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f158,f159,f162])).
% 0.09/0.40 fof(f166,plain,(
% 0.09/0.40 contains_slb(sK1_skl,findmin_pqp_res(sK0_skl))),
% 0.09/0.40 inference(resolution,[status(thm)],[f148,f153])).
% 0.09/0.40 fof(f167,plain,(
% 0.09/0.40 ![X0,X1]: (contains_cpq(triple(X0,sK1_skl,X1),findmin_pqp_res(sK0_skl)))),
% 0.09/0.40 inference(resolution,[status(thm)],[f166,f111])).
% 0.09/0.40 fof(f168,plain,(
% 0.09/0.40 $false|sQ0_spl),
% 0.09/0.40 inference(backward_subsumption_resolution,[status(thm)],[f161,f167])).
% 0.09/0.40 fof(f170,plain,(
% 0.09/0.40 sQ0_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f168])).
% 0.09/0.40 fof(f172,plain,(
% 0.09/0.40 ![X0,X1]: (~ok(findmin_cpq_eff(triple(X0,sK1_skl,X1)))|~sQ1_spl)),
% 0.09/0.40 inference(backward_demodulation,[status(thm)],[f163,f156])).
% 0.09/0.40 fof(f173,plain,(
% 0.09/0.40 $false|~sQ1_spl),
% 0.09/0.40 inference(backward_subsumption_resolution,[status(thm)],[f153,f172])).
% 0.09/0.40 fof(f174,plain,(
% 0.09/0.40 ~sQ1_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f173])).
% 0.09/0.40 fof(f175,plain,(
% 0.09/0.40 $false),
% 0.09/0.40 inference(sat_refutation,[status(thm)],[f165,f170,f174])).
% 0.09/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.41 % Elapsed time: 0.042599 seconds
% 0.09/0.41 % CPU time: 0.110983 seconds
% 0.09/0.41 % Total memory used: 54.822 MB
% 0.09/0.41 % Net memory used: 54.790 MB
%------------------------------------------------------------------------------