%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW319+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:08:58 PM UTC 2026
% Result : Theorem 0.48s 1.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW319+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.08/0.34 % Computer : n008.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % 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 09:47:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.40/0.64 % Drodi V4.1.1
% 0.48/1.11 % Refutation found
% 0.48/1.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.48/1.11 % SZS output start CNFRefutation for theBenchmark
% 0.48/1.11 fof(f4,axiom,(
% 0.48/1.11 (! [V_Ga_2,V_tsa_2,V_G_H_2,T_b] :( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_tsa_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_tsa_2) ) ) )),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f41,axiom,(
% 0.48/1.11 (! [V_A_2,T_b] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))),V_A_2)) )),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f84,axiom,(
% 0.48/1.11 (! [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.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f86,axiom,(
% 0.48/1.11 (! [V_a_2,V_D_2,V_C_2,T_b] :( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2))=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2))) ) )),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f87,axiom,(
% 0.48/1.11 (! [V_Ga_2,V_tsa_2,T_b] :( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_tsa_2),V_Ga_2))=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_tsa_2) ) )),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f88,axiom,(
% 0.48/1.11 (! [V_tsa_2,V_ts_H_2,V_Ga_2,T_b] :( c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_H_2)=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_tsa_2),V_ts_H_2))=> c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_tsa_2) ) ) )),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f5226,hypothesis,(
% 0.48/1.11 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)) ),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f5227,conjecture,(
% 0.48/1.11 ( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))& c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts) ) ),
% 0.48/1.11 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/1.11 fof(f5228,negated_conjecture,(
% 0.48/1.11 ~(( c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))& c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts) ) )),
% 0.48/1.11 inference(negated_conjecture,[status(cth)],[f5227])).
% 0.48/1.11 fof(f5234,plain,(
% 0.48/1.11 ![V_Ga_2,V_tsa_2,V_G_H_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_tsa_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_tsa_2)))),
% 0.48/1.11 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.48/1.11 fof(f5235,plain,(
% 0.48/1.11 ![V_tsa_2,V_G_H_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_G_H_2,V_tsa_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_tsa_2))))),
% 0.48/1.11 inference(miniscoping,[status(thm)],[f5234])).
% 0.48/1.11 fof(f5236,plain,(
% 0.48/1.11 ![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.48/1.11 inference(cnf_transformation,[status(thm)],[f5235])).
% 0.48/1.11 fof(f5340,plain,(
% 0.48/1.11 ![X0,X1]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))),X1)))),
% 0.48/1.11 inference(cnf_transformation,[status(thm)],[f41])).
% 0.48/1.11 fof(f5489,plain,(
% 0.48/1.11 ![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.48/1.11 inference(cnf_transformation,[status(thm)],[f84])).
% 0.48/1.11 fof(f5493,plain,(
% 0.48/1.11 ![V_a_2,V_D_2,V_C_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2))))),
% 0.48/1.11 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.48/1.11 fof(f5494,plain,(
% 0.48/1.11 ![V_D_2,V_C_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2))|(![V_a_2]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2)))))),
% 0.48/1.11 inference(miniscoping,[status(thm)],[f5493])).
% 0.48/1.11 fof(f5495,plain,(
% 0.48/1.11 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X2))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X3),X1)),hAPP(hAPP(c_Set_Oinsert(X0),X3),X2))))),
% 0.48/1.11 inference(cnf_transformation,[status(thm)],[f5494])).
% 0.48/1.11 fof(f5496,plain,(
% 0.48/1.11 ![V_Ga_2,V_tsa_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_tsa_2),V_Ga_2))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_tsa_2))),
% 0.48/1.11 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 0.48/1.11 fof(f5497,plain,(
% 0.48/1.11 ![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.48/1.11 inference(cnf_transformation,[status(thm)],[f5496])).
% 0.48/1.11 fof(f5498,plain,(
% 0.48/1.11 ![V_tsa_2,V_ts_H_2,V_Ga_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_H_2)|(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_tsa_2),V_ts_H_2))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_tsa_2)))),
% 0.48/1.11 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 0.48/1.11 fof(f5499,plain,(
% 0.48/1.11 ![V_ts_H_2,V_Ga_2,T_b]: (~c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_ts_H_2)|(![V_tsa_2]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_b),tc_HOL_Obool)),V_tsa_2),V_ts_H_2))|c_Hoare__Mirabelle_Ohoare__derivs(T_b,V_Ga_2,V_tsa_2))))),
% 0.48/1.11 inference(miniscoping,[status(thm)],[f5498])).
% 0.48/1.11 fof(f5500,plain,(
% 0.48/1.11 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)),X3),X2))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X3))),
% 0.48/1.11 inference(cnf_transformation,[status(thm)],[f5499])).
% 0.48/1.11 fof(f20072,plain,(
% 0.48/1.11 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts))),
% 0.48/1.11 inference(cnf_transformation,[status(thm)],[f5226])).
% 0.48/1.11 fof(f20073,plain,(
% 0.48/1.11 (~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts))),
% 0.48/1.11 inference(pre_NNF_transformation,[status(thm)],[f5228])).
% 0.48/1.11 fof(f20074,plain,(
% 0.48/1.11 ~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))|~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts)),
% 0.48/1.11 inference(cnf_transformation,[status(thm)],[f20073])).
% 0.48/1.11 fof(f20523,plain,(
% 0.48/1.11 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X1),X2),X2))),
% 0.48/1.11 inference(resolution,[status(thm)],[f5489,f5497])).
% 0.48/1.11 fof(f20528,plain,(
% 0.48/1.11 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),X3))|c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X3))),
% 0.48/1.11 inference(resolution,[status(thm)],[f20523,f5236])).
% 0.48/1.11 fof(f20531,plain,(
% 0.48/1.11 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,v_ts)),
% 0.48/1.11 inference(resolution,[status(thm)],[f20528,f20072])).
% 0.48/1.11 fof(f20535,plain,(
% 0.48/1.11 ~c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 3.96/1.17 inference(backward_subsumption_resolution,[status(thm)],[f20074,f20531])).
% 3.96/1.17 fof(f20639,plain,(
% 3.96/1.17 ![X0]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),X0),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),v_ts)))|c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,X0))),
% 3.96/1.17 inference(resolution,[status(thm)],[f5500,f20072])).
% 3.96/1.17 fof(f21115,plain,(
% 3.96/1.17 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))))),
% 3.96/1.17 inference(resolution,[status(thm)],[f5495,f5340])).
% 3.96/1.17 fof(f21363,plain,(
% 3.96/1.17 c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool))))),
% 3.96/1.17 inference(resolution,[status(thm)],[f20639,f21115])).
% 3.96/1.17 fof(f21371,plain,(
% 3.96/1.17 $false),
% 3.96/1.17 inference(forward_subsumption_resolution,[status(thm)],[f21363,f20535])).
% 3.96/1.17 % SZS output end CNFRefutation for theBenchmark.p
% 3.96/1.22 % Elapsed time: 0.857378 seconds
% 3.96/1.22 % CPU time: 4.101898 seconds
% 3.96/1.22 % Total memory used: 684.728 MB
% 3.96/1.22 % Net memory used: 678.514 MB
%------------------------------------------------------------------------------