%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW318+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 : n009.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:08:58 PM UTC 2026
% Result : Theorem 0.94s 2.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW318+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:47:12 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.78/1.05 % Drodi V4.1.1
% 0.94/2.09 % Refutation found
% 0.94/2.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.94/2.09 % SZS output start CNFRefutation for theBenchmark
% 0.94/2.09 fof(f5,axiom,(
% 0.94/2.09 (! [V_Ga_2,V_ts_2,V_G_H_2,T_b] :( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_ts_2)=> ( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_G_H_2)=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_2) ) ) )),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f22,axiom,(
% 0.94/2.09 (! [V_A_2,V_x_2,T_b] : hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),V_A_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),V_A_2) )),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f700,axiom,(
% 0.94/2.09 (! [V_a_2,V_B_2,T_b] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_B_2),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_B_2))) )),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f740,axiom,(
% 0.94/2.09 (! [V_Ga_2,V_ts_2,T_b] :( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_ts_2),V_Ga_2))=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_2) ) )),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f5225,hypothesis,(
% 0.94/2.09 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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f5226,conjecture,(
% 0.94/2.09 c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) ),
% 0.94/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.94/2.09 fof(f5227,negated_conjecture,(
% 0.94/2.09 ~(c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))) )),
% 0.94/2.09 inference(negated_conjecture,[status(cth)],[f5226])).
% 0.94/2.09 fof(f5239,plain,(
% 0.94/2.09 ![V_Ga_2,V_ts_2,V_G_H_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_ts_2)|(~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_G_H_2)|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_2)))),
% 0.94/2.09 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.94/2.09 fof(f5240,plain,(
% 0.94/2.09 ![V_ts_2,V_G_H_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_ts_2)|(![V_Ga_2]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_G_H_2)|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_2))))),
% 0.94/2.09 inference(miniscoping,[status(thm)],[f5239])).
% 0.94/2.09 fof(f5241,plain,(
% 0.94/2.09 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X1)|c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f5240])).
% 0.94/2.09 fof(f5286,plain,(
% 0.94/2.09 ![X0,X1,X2]: (hAPP(hAPP(c_Set_Oinsert(X0),X1),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))=hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f22])).
% 0.94/2.09 fof(f7328,plain,(
% 0.94/2.09 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),hAPP(hAPP(c_Set_Oinsert(X0),X2),X1))))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f700])).
% 0.94/2.09 fof(f7444,plain,(
% 0.94/2.09 ![V_Ga_2,V_ts_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_ts_2),V_Ga_2))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_2))),
% 0.94/2.09 inference(pre_NNF_transformation,[status(thm)],[f740])).
% 0.94/2.09 fof(f7445,plain,(
% 0.94/2.09 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)),X1),X2))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X2,X1))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f7444])).
% 0.94/2.09 fof(f19964,plain,(
% 0.94/2.09 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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f5225])).
% 0.94/2.09 fof(f19965,plain,(
% 0.94/2.09 ~c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 0.94/2.09 inference(cnf_transformation,[status(thm)],[f5227])).
% 0.94/2.09 fof(f20763,plain,(
% 0.94/2.09 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),v_G),X0))),
% 0.94/2.09 inference(resolution,[status(thm)],[f5241,f19965])).
% 0.94/2.09 fof(f20768,plain,(
% 0.94/2.09 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),v_G),X0)|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,X0,X1))),
% 0.94/2.09 inference(resolution,[status(thm)],[f20763,f5241])).
% 0.94/2.09 fof(f20944,plain,(
% 0.94/2.09 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X1),X2),X2))),
% 0.94/2.09 inference(resolution,[status(thm)],[f7445,f7328])).
% 0.94/2.09 fof(f21016,plain,(
% 0.94/2.09 ![X0,X1]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Com_Ocom_OBODY,v_pn)),v_Q)),v_G),X0)|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),X1),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))))),
% 0.94/2.09 inference(resolution,[status(thm)],[f20944,f20768])).
% 0.94/2.09 fof(f21067,plain,(
% 0.94/2.09 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),X0),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))))),
% 0.94/2.09 inference(resolution,[status(thm)],[f21016,f20944])).
% 0.94/2.09 fof(f21108,plain,(
% 0.94/2.09 ~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),hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn))),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 0.94/2.11 inference(paramodulation,[status(thm)],[f5286,f21067])).
% 0.94/2.11 fof(f21500,plain,(
% 0.94/2.11 $false),
% 0.94/2.11 inference(forward_subsumption_resolution,[status(thm)],[f19964,f21108])).
% 0.94/2.11 % SZS output end CNFRefutation for theBenchmark.p
% 3.34/2.23 % Elapsed time: 1.839998 seconds
% 3.34/2.23 % CPU time: 9.177170 seconds
% 3.34/2.23 % Total memory used: 714.159 MB
% 3.34/2.23 % Net memory used: 708.650 MB
%------------------------------------------------------------------------------