%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW391+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 03:09:04 PM UTC 2026
% Result : Theorem 7.15s 2.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW391+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n008.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 09:51:08 UTC 2026
% 0.19/0.46 % CPUTime :
% 1.25/1.52 % Drodi V4.1.1
% 7.15/2.40 % Refutation found
% 7.15/2.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.15/2.40 % SZS output start CNFRefutation for theBenchmark
% 7.15/2.40 fof(f5228,hypothesis,(
% 7.15/2.40 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
% 7.15/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.15/2.40 fof(f5229,hypothesis,(
% 7.15/2.40 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P_H),v_c),v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
% 7.15/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.15/2.40 fof(f5230,conjecture,(
% 7.15/2.40 (! [B_Z,B_s] :( ( hBOOL(hAPP(hAPP(v_P,B_Z),B_s))| hBOOL(hAPP(hAPP(v_P_H,B_Z),B_s)) )=> (? [B_P_H,B_Q_H] :( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))& (! [B_s_H] :( (! [B_Z_H] :( hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s))=> hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H)) ))=> ( hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H))| hBOOL(hAPP(hAPP(v_Q_H,B_Z),B_s_H)) ) ) )) )) )),
% 7.15/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.15/2.40 fof(f5231,negated_conjecture,(
% 7.15/2.40 ~((! [B_Z,B_s] :( ( hBOOL(hAPP(hAPP(v_P,B_Z),B_s))| hBOOL(hAPP(hAPP(v_P_H,B_Z),B_s)) )=> (? [B_P_H,B_Q_H] :( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))& (! [B_s_H] :( (! [B_Z_H] :( hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s))=> hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H)) ))=> ( hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H))| hBOOL(hAPP(hAPP(v_Q_H,B_Z),B_s_H)) ) ) )) )) ))),
% 7.15/2.40 inference(negated_conjecture,[status(cth)],[f5230])).
% 7.15/2.40 fof(f20072,plain,(
% 7.15/2.40 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 7.15/2.40 inference(cnf_transformation,[status(thm)],[f5228])).
% 7.15/2.40 fof(f20073,plain,(
% 7.15/2.40 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P_H),v_c),v_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 7.15/2.40 inference(cnf_transformation,[status(thm)],[f5229])).
% 7.15/2.40 fof(f20074,plain,(
% 7.15/2.40 (?[B_Z,B_s]: ((hBOOL(hAPP(hAPP(v_P,B_Z),B_s))|hBOOL(hAPP(hAPP(v_P_H,B_Z),B_s)))&(![B_P_H,B_Q_H]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|(?[B_s_H]: ((![B_Z_H]: (~hBOOL(hAPP(hAPP(B_P_H,B_Z_H),B_s))|hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),B_s_H))))&(~hBOOL(hAPP(hAPP(v_Q,B_Z),B_s_H))&~hBOOL(hAPP(hAPP(v_Q_H,B_Z),B_s_H)))))))))),
% 7.15/2.40 inference(pre_NNF_transformation,[status(thm)],[f5231])).
% 7.15/2.40 fof(f20075,plain,(
% 7.15/2.40 ((hBOOL(hAPP(hAPP(v_P,sK577_skl),sK578_skl))|hBOOL(hAPP(hAPP(v_P_H,sK577_skl),sK578_skl)))&(![B_P_H,B_Q_H]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),B_P_H),v_c),B_Q_H)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|((![B_Z_H]: (~hBOOL(hAPP(hAPP(B_P_H,B_Z_H),sK578_skl))|hBOOL(hAPP(hAPP(B_Q_H,B_Z_H),sK579_skl(B_Q_H,B_P_H)))))&(~hBOOL(hAPP(hAPP(v_Q,sK577_skl),sK579_skl(B_Q_H,B_P_H)))&~hBOOL(hAPP(hAPP(v_Q_H,sK577_skl),sK579_skl(B_Q_H,B_P_H))))))))),
% 7.15/2.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK577_skl,sK578_skl,sK579_skl]),skolemize(B_Z,sK577_skl),skolemize(B_s,sK578_skl),skolemize(B_s_H,sK579_skl(B_Q_H,B_P_H))],[f20074])).
% 7.94/2.44 fof(f20076,plain,(
% 7.94/2.44 hBOOL(hAPP(hAPP(v_P,sK577_skl),sK578_skl))|hBOOL(hAPP(hAPP(v_P_H,sK577_skl),sK578_skl))),
% 7.94/2.44 inference(cnf_transformation,[status(thm)],[f20075])).
% 7.94/2.44 fof(f20077,plain,(
% 7.94/2.44 ![X0,X1,X2]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),X0),v_c),X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~hBOOL(hAPP(hAPP(X0,X2),sK578_skl))|hBOOL(hAPP(hAPP(X1,X2),sK579_skl(X1,X0))))),
% 7.94/2.44 inference(cnf_transformation,[status(thm)],[f20075])).
% 7.94/2.44 fof(f20078,plain,(
% 7.94/2.44 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),X0),v_c),X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~hBOOL(hAPP(hAPP(v_Q,sK577_skl),sK579_skl(X1,X0))))),
% 7.94/2.44 inference(cnf_transformation,[status(thm)],[f20075])).
% 7.94/2.44 fof(f20079,plain,(
% 7.94/2.44 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),X0),v_c),X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~hBOOL(hAPP(hAPP(v_Q_H,sK577_skl),sK579_skl(X1,X0))))),
% 7.94/2.44 inference(cnf_transformation,[status(thm)],[f20075])).
% 7.94/2.44 fof(f20405,definition,(
% 7.94/2.44 sQ8_spl <=> (hBOOL(hAPP(hAPP(v_P,sK577_skl),sK578_skl)))),
% 7.94/2.44 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 7.94/2.44 fof(f20406,plain,(
% 7.94/2.44 hBOOL(hAPP(hAPP(v_P,sK577_skl),sK578_skl))|~sQ8_spl),
% 7.94/2.44 inference(component_clause,[status(thm)],[f20405])).
% 7.94/2.44 fof(f20408,definition,(
% 7.94/2.44 sQ9_spl <=> (hBOOL(hAPP(hAPP(v_P_H,sK577_skl),sK578_skl)))),
% 7.94/2.44 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 7.94/2.44 fof(f20409,plain,(
% 7.94/2.44 hBOOL(hAPP(hAPP(v_P_H,sK577_skl),sK578_skl))|~sQ9_spl),
% 7.94/2.44 inference(component_clause,[status(thm)],[f20408])).
% 7.94/2.44 fof(f20411,plain,(
% 7.94/2.44 sQ8_spl|sQ9_spl),
% 7.94/2.44 inference(split_clause,[status(thm)],[f20076,f20405,f20408])).
% 7.94/2.44 fof(f21446,plain,(
% 7.94/2.44 ~hBOOL(hAPP(hAPP(v_Q,sK577_skl),sK579_skl(v_Q,v_P)))),
% 7.94/2.44 inference(resolution,[status(thm)],[f20072,f20078])).
% 7.94/2.44 fof(f21447,plain,(
% 7.94/2.44 ![X0]: (~hBOOL(hAPP(hAPP(v_P,X0),sK578_skl))|hBOOL(hAPP(hAPP(v_Q,X0),sK579_skl(v_Q,v_P))))),
% 7.94/2.44 inference(resolution,[status(thm)],[f20072,f20077])).
% 7.94/2.44 fof(f21460,plain,(
% 7.94/2.44 ~hBOOL(hAPP(hAPP(v_Q_H,sK577_skl),sK579_skl(v_Q_H,v_P_H)))),
% 7.94/2.44 inference(resolution,[status(thm)],[f20073,f20079])).
% 7.94/2.44 fof(f21462,plain,(
% 7.94/2.44 ![X0]: (~hBOOL(hAPP(hAPP(v_P_H,X0),sK578_skl))|hBOOL(hAPP(hAPP(v_Q_H,X0),sK579_skl(v_Q_H,v_P_H))))),
% 7.94/2.44 inference(resolution,[status(thm)],[f20073,f20077])).
% 7.94/2.44 fof(f21546,plain,(
% 7.94/2.44 hBOOL(hAPP(hAPP(v_Q,sK577_skl),sK579_skl(v_Q,v_P)))|~sQ8_spl),
% 7.94/2.44 inference(resolution,[status(thm)],[f21447,f20406])).
% 7.94/2.44 fof(f21547,plain,(
% 7.94/2.44 $false|~sQ8_spl),
% 7.94/2.44 inference(forward_subsumption_resolution,[status(thm)],[f21546,f21446])).
% 7.94/2.44 fof(f21548,plain,(
% 7.94/2.44 ~sQ8_spl),
% 7.94/2.44 inference(contradiction_clause,[status(thm)],[f21547])).
% 7.94/2.44 fof(f21720,plain,(
% 7.94/2.44 hBOOL(hAPP(hAPP(v_Q_H,sK577_skl),sK579_skl(v_Q_H,v_P_H)))|~sQ9_spl),
% 7.94/2.44 inference(resolution,[status(thm)],[f21462,f20409])).
% 7.94/2.44 fof(f21721,plain,(
% 7.94/2.44 $false|~sQ9_spl),
% 7.94/2.44 inference(forward_subsumption_resolution,[status(thm)],[f21720,f21460])).
% 7.94/2.44 fof(f21722,plain,(
% 7.94/2.44 ~sQ9_spl),
% 7.94/2.44 inference(contradiction_clause,[status(thm)],[f21721])).
% 7.94/2.44 fof(f21723,plain,(
% 7.94/2.44 $false),
% 7.94/2.44 inference(sat_refutation,[status(thm)],[f20411,f21548,f21722])).
% 7.94/2.44 % SZS output end CNFRefutation for theBenchmark.p
% 4.87/2.59 % Elapsed time: 2.103894 seconds
% 4.87/2.59 % CPU time: 8.253574 seconds
% 4.87/2.59 % Total memory used: 696.520 MB
% 4.87/2.59 % Net memory used: 689.508 MB
%------------------------------------------------------------------------------