%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV408+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 : n001.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:43 PM UTC 2026
% Result : Theorem 1.18s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV408+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n001.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 08:50:59 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 1.18/0.64 % Refutation found
% 1.18/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.18/0.64 % SZS output start CNFRefutation for theBenchmark
% 1.18/0.64 fof(f8,axiom,(
% 1.18/0.64 (! [U] : ~ contains_slb(create_slb,U) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f27,axiom,(
% 1.18/0.64 (! [U,V,W,X] :( contains_cpq(triple(U,V,W),X)<=> contains_slb(V,X) ) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f39,axiom,(
% 1.18/0.64 (! [U,V,W,X] :( V != create_slb=> findmin_cpq_res(triple(U,V,W)) = findmin_pqp_res(U) ) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f41,axiom,(
% 1.18/0.64 (! [U] : removemin_cpq_res(U) = findmin_cpq_res(U) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f42,lemma,(
% 1.18/0.64 (! [U,V,W] :( ( contains_slb(U,V)& strictly_less_than(V,W) )=> ( pair_in_list(update_slb(U,W),V,W)| (? [X] :( pair_in_list(update_slb(U,W),V,X)& less_than(W,X) ) )) ) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f43,conjecture,(
% 1.18/0.64 (! [U,V,W,X] :( ( contains_slb(V,X)& strictly_less_than(X,findmin_cpq_res(triple(U,V,W))) )=> ( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))| (? [Y] :( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y)& less_than(findmin_pqp_res(U),Y) ) )) ) )),
% 1.18/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.18/0.64 fof(f44,negated_conjecture,(
% 1.18/0.64 ~((! [U,V,W,X] :( ( contains_slb(V,X)& strictly_less_than(X,findmin_cpq_res(triple(U,V,W))) )=> ( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))| (? [Y] :( pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y)& less_than(findmin_pqp_res(U),Y) ) )) ) ))),
% 1.18/0.64 inference(negated_conjecture,[status(cth)],[f43])).
% 1.18/0.64 fof(f58,plain,(
% 1.18/0.64 ![X0]: (~contains_slb(create_slb,X0))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f8])).
% 1.18/0.64 fof(f108,plain,(
% 1.18/0.64 ![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)))),
% 1.18/0.64 inference(NNF_transformation,[status(thm)],[f27])).
% 1.18/0.64 fof(f109,plain,(
% 1.18/0.64 (![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)))),
% 1.18/0.64 inference(miniscoping,[status(thm)],[f108])).
% 1.18/0.64 fof(f111,plain,(
% 1.18/0.64 ![X0,X1,X2,X3]: (contains_cpq(triple(X0,X1,X2),X3)|~contains_slb(X1,X3))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f109])).
% 1.18/0.64 fof(f140,plain,(
% 1.18/0.64 ![U,V,W,X]: (V=create_slb|findmin_cpq_res(triple(U,V,W))=findmin_pqp_res(U))),
% 1.18/0.64 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 1.18/0.64 fof(f141,plain,(
% 1.18/0.64 ![V]: (V=create_slb|(![U,W]: findmin_cpq_res(triple(U,V,W))=findmin_pqp_res(U)))),
% 1.18/0.64 inference(miniscoping,[status(thm)],[f140])).
% 1.18/0.64 fof(f142,plain,(
% 1.18/0.64 ![X0,X1,X2]: (X0=create_slb|findmin_cpq_res(triple(X1,X0,X2))=findmin_pqp_res(X1))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f141])).
% 1.18/0.64 fof(f144,plain,(
% 1.18/0.64 ![X0]: (removemin_cpq_res(X0)=findmin_cpq_res(X0))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f41])).
% 1.18/0.64 fof(f145,plain,(
% 1.18/0.64 ![U,V,W]: ((~contains_slb(U,V)|~strictly_less_than(V,W))|(pair_in_list(update_slb(U,W),V,W)|(?[X]: (pair_in_list(update_slb(U,W),V,X)&less_than(W,X)))))),
% 1.18/0.64 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 1.18/0.64 fof(f146,plain,(
% 1.18/0.64 ![U,V,W]: ((~contains_slb(U,V)|~strictly_less_than(V,W))|(pair_in_list(update_slb(U,W),V,W)|(pair_in_list(update_slb(U,W),V,sK0_skl(W,V,U))&less_than(W,sK0_skl(W,V,U)))))),
% 1.18/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(W,V,U))],[f145])).
% 1.18/0.64 fof(f147,plain,(
% 1.18/0.64 ![X0,X1,X2]: (~contains_slb(X0,X1)|~strictly_less_than(X1,X2)|pair_in_list(update_slb(X0,X2),X1,X2)|pair_in_list(update_slb(X0,X2),X1,sK0_skl(X2,X1,X0)))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f146])).
% 1.18/0.64 fof(f148,plain,(
% 1.18/0.64 ![X0,X1,X2]: (~contains_slb(X0,X1)|~strictly_less_than(X1,X2)|pair_in_list(update_slb(X0,X2),X1,X2)|less_than(X2,sK0_skl(X2,X1,X0)))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f146])).
% 1.18/0.64 fof(f149,plain,(
% 1.18/0.64 (?[U,V,W,X]: ((contains_slb(V,X)&strictly_less_than(X,findmin_cpq_res(triple(U,V,W))))&(~pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))&(![Y]: (~pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y)|~less_than(findmin_pqp_res(U),Y))))))),
% 1.18/0.64 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 1.18/0.64 fof(f150,plain,(
% 1.18/0.64 ?[U,V,X]: ((contains_slb(V,X)&(?[W]: strictly_less_than(X,findmin_cpq_res(triple(U,V,W)))))&(~pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))&(![Y]: (~pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y)|~less_than(findmin_pqp_res(U),Y)))))),
% 1.18/0.64 inference(miniscoping,[status(thm)],[f149])).
% 1.18/0.64 fof(f151,plain,(
% 1.18/0.64 ((contains_slb(sK2_skl,sK3_skl)&strictly_less_than(sK3_skl,findmin_cpq_res(triple(sK1_skl,sK2_skl,sK4_skl))))&(~pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl))&(![Y]: (~pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,Y)|~less_than(findmin_pqp_res(sK1_skl),Y)))))),
% 1.18/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(U,sK1_skl),skolemize(V,sK2_skl),skolemize(X,sK3_skl),skolemize(W,sK4_skl)],[f150])).
% 1.18/0.64 fof(f152,plain,(
% 1.18/0.64 contains_slb(sK2_skl,sK3_skl)),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f151])).
% 1.18/0.64 fof(f153,plain,(
% 1.18/0.64 strictly_less_than(sK3_skl,findmin_cpq_res(triple(sK1_skl,sK2_skl,sK4_skl)))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f151])).
% 1.18/0.64 fof(f154,plain,(
% 1.18/0.64 ~pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f151])).
% 1.18/0.64 fof(f155,plain,(
% 1.18/0.64 ![X0]: (~pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,X0)|~less_than(findmin_pqp_res(sK1_skl),X0))),
% 1.18/0.64 inference(cnf_transformation,[status(thm)],[f151])).
% 1.18/0.64 fof(f167,plain,(
% 1.18/0.64 strictly_less_than(sK3_skl,removemin_cpq_res(triple(sK1_skl,sK2_skl,sK4_skl)))),
% 1.18/0.64 inference(backward_demodulation,[status(thm)],[f144,f153])).
% 1.18/0.64 fof(f178,plain,(
% 1.18/0.64 ![X0,X1,X2]: (X0=create_slb|removemin_cpq_res(triple(X1,X0,X2))=findmin_pqp_res(X1))),
% 1.18/0.64 inference(forward_demodulation,[status(thm)],[f144,f142])).
% 1.18/0.64 fof(f179,plain,(
% 1.18/0.64 strictly_less_than(sK3_skl,findmin_pqp_res(sK1_skl))|sK2_skl=create_slb),
% 1.18/0.64 inference(paramodulation,[status(thm)],[f178,f167])).
% 1.18/0.64 fof(f181,definition,(
% 1.18/0.64 sQ0_spl <=> (strictly_less_than(sK3_skl,findmin_pqp_res(sK1_skl)))),
% 1.18/0.64 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.18/0.64 fof(f184,definition,(
% 1.18/0.64 sQ1_spl <=> (sK2_skl=create_slb)),
% 1.18/0.64 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.18/0.64 fof(f185,plain,(
% 1.18/0.64 sK2_skl=create_slb|~sQ1_spl),
% 1.18/0.64 inference(component_clause,[status(thm)],[f184])).
% 1.18/0.64 fof(f187,plain,(
% 1.18/0.64 sQ0_spl|sQ1_spl),
% 1.18/0.64 inference(split_clause,[status(thm)],[f179,f181,f184])).
% 1.18/0.64 fof(f197,plain,(
% 1.18/0.64 contains_slb(create_slb,sK3_skl)|~sQ1_spl),
% 1.18/0.64 inference(backward_demodulation,[status(thm)],[f185,f152])).
% 1.18/0.64 fof(f201,plain,(
% 1.18/0.64 $false|~sQ1_spl),
% 1.18/0.64 inference(forward_subsumption_resolution,[status(thm)],[f197,f58])).
% 1.18/0.64 fof(f202,plain,(
% 1.18/0.64 ~sQ1_spl),
% 1.18/0.64 inference(contradiction_clause,[status(thm)],[f201])).
% 1.18/0.64 fof(f480,definition,(
% 1.18/0.64 sQ14_spl <=> (contains_slb(sK2_skl,sK3_skl))),
% 1.18/0.64 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.18/0.64 fof(f482,plain,(
% 1.18/0.64 ~contains_slb(sK2_skl,sK3_skl)|sQ14_spl),
% 1.18/0.64 inference(component_clause,[status(thm)],[f480])).
% 1.18/0.64 fof(f597,definition,(
% 1.18/0.64 sQ21_spl <=> (pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl)))),
% 1.18/0.64 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.18/0.64 fof(f598,plain,(
% 1.18/0.64 pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl))|~sQ21_spl),
% 1.18/0.64 inference(component_clause,[status(thm)],[f597])).
% 1.18/0.64 fof(f609,plain,(
% 1.18/0.64 $false|sQ14_spl),
% 1.18/0.64 inference(forward_subsumption_resolution,[status(thm)],[f482,f152])).
% 1.18/0.64 fof(f610,plain,(
% 1.18/0.64 sQ14_spl),
% 1.18/0.64 inference(contradiction_clause,[status(thm)],[f609])).
% 1.18/0.64 fof(f611,plain,(
% 1.18/0.64 $false|~sQ21_spl),
% 1.18/0.64 inference(forward_subsumption_resolution,[status(thm)],[f598,f154])).
% 1.18/0.64 fof(f612,plain,(
% 1.18/0.64 ~sQ21_spl),
% 1.18/0.64 inference(contradiction_clause,[status(thm)],[f611])).
% 1.18/0.64 fof(f678,plain,(
% 1.18/0.64 ![X0,X1]: (~contains_slb(X0,X1)|~strictly_less_than(X1,findmin_pqp_res(sK1_skl))|pair_in_list(update_slb(X0,findmin_pqp_res(sK1_skl)),X1,findmin_pqp_res(sK1_skl))|~pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,sK0_skl(findmin_pqp_res(sK1_skl),X1,X0)))),
% 1.18/0.66 inference(resolution,[status(thm)],[f148,f155])).
% 1.18/0.66 fof(f1597,definition,(
% 1.18/0.66 ![X0,X1]: (sQ64_spl <=> (~contains_cpq(triple(X0,sK2_skl,bad),X1)))),
% 1.18/0.66 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 1.18/0.66 fof(f1598,plain,(
% 1.18/0.66 ![X0,X1]: (~contains_cpq(triple(X0,sK2_skl,bad),X1)|~sQ64_spl)),
% 1.18/0.66 inference(component_clause,[status(thm)],[f1597])).
% 1.18/0.66 fof(f1608,plain,(
% 1.18/0.66 ![X0]: (~contains_slb(sK2_skl,X0)|~sQ64_spl)),
% 1.18/0.66 inference(resolution,[status(thm)],[f1598,f111])).
% 1.18/0.66 fof(f1609,plain,(
% 1.18/0.66 $false|~sQ64_spl),
% 1.18/0.66 inference(backward_subsumption_resolution,[status(thm)],[f152,f1608])).
% 1.18/0.66 fof(f1613,plain,(
% 1.18/0.66 ~sQ64_spl),
% 1.18/0.66 inference(contradiction_clause,[status(thm)],[f1609])).
% 1.18/0.66 fof(f2148,plain,(
% 1.18/0.66 ~contains_slb(sK2_skl,sK3_skl)|~strictly_less_than(sK3_skl,findmin_pqp_res(sK1_skl))|pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl))|~contains_slb(sK2_skl,sK3_skl)|~strictly_less_than(sK3_skl,findmin_pqp_res(sK1_skl))|pair_in_list(update_slb(sK2_skl,findmin_pqp_res(sK1_skl)),sK3_skl,findmin_pqp_res(sK1_skl))),
% 1.18/0.66 inference(resolution,[status(thm)],[f678,f147])).
% 1.18/0.66 fof(f2149,plain,(
% 1.18/0.66 ~sQ14_spl|~sQ0_spl|sQ21_spl),
% 1.18/0.66 inference(split_clause,[status(thm)],[f2148,f480,f181,f597])).
% 1.18/0.66 fof(f2150,plain,(
% 1.18/0.66 $false),
% 1.18/0.66 inference(sat_refutation,[status(thm)],[f187,f202,f610,f612,f1613,f2149])).
% 1.18/0.66 % SZS output end CNFRefutation for theBenchmark.p
% 1.18/0.68 % Elapsed time: 0.298534 seconds
% 1.18/0.68 % CPU time: 2.012325 seconds
% 1.18/0.68 % Total memory used: 130.584 MB
% 1.18/0.68 % Net memory used: 127.528 MB
%------------------------------------------------------------------------------