%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV905-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:53:20 PM UTC 2026
% Result : Unsatisfiable 0.22s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV905-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.48 % Computer : n017.cluster.edu
% 0.17/0.48 % Model : x86_64 x86_64
% 0.17/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.48 % Memory : 8046.5625MB
% 0.17/0.48 % OS : Linux 6.8.0-71-generic
% 0.17/0.48 % CPULimit : 300
% 0.17/0.48 % WCLimit : 300
% 0.17/0.48 % DateTime : Mon Sep 21 09:26:27 UTC 2026
% 0.17/0.48 % CPUTime :
% 0.22/0.57 % Drodi V4.1.1
% 0.22/0.69 % Refutation found
% 0.22/0.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.69 fof(f3,axiom,(
% 0.22/0.69 (![V_m,V_n,T_b,T_a,V_k]: (( hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k) != c_Option_Ooption_ONone(T_a)| hAPP(V_m,V_k) = c_Option_Ooption_ONone(T_a) ) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f385,axiom,(
% 0.22/0.69 (![V_l1,V_l2,T_a,T_b,V_m]: (( hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m) = hAPP(V_l2,V_m)| ~ hBOOL(c_in(V_m,c_Map_Odom(V_l2,T_a,T_b),T_a)) ) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f398,axiom,(
% 0.22/0.69 (![V_pn]: (( c_Com_OWT(c_Com_Ocom_OBODY(V_pn))| hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f415,axiom,(
% 0.22/0.69 (![V_c]: (( c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)| ~ c_Com_OWT(V_c)| ~ c_Com_OWT__bodies| ~ c_Hoare__Mirabelle_Ostate__not__singleton ) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f422,axiom,(
% 0.22/0.69 (![T_a,V_x]: (~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f435,axiom,(
% 0.22/0.69 (![V_S,V_x,T_a]: (( hBOOL(hAPP(V_S,V_x))| ~ hBOOL(c_in(V_x,V_S,T_a)) ) ))),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f445,negated_conjecture,(
% 0.22/0.69 c_Hoare__Mirabelle_Ostate__not__singleton ),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f446,negated_conjecture,(
% 0.22/0.69 c_Com_OWT__bodies ),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f448,negated_conjecture,(
% 0.22/0.69 hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname)) ),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f449,negated_conjecture,(
% 0.22/0.69 ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OBODY(v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
% 0.22/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.69 fof(f491,plain,(
% 0.22/0.69 ![V_m,T_a,V_k]: ((![V_n,T_b]: ~hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)=c_Option_Ooption_ONone(T_a))|hAPP(V_m,V_k)=c_Option_Ooption_ONone(T_a))),
% 0.22/0.69 inference(miniscoping,[status(thm)],[f3])).
% 0.22/0.69 fof(f492,plain,(
% 0.22/0.69 ![X0,X1,X2,X3,X4]: (~hAPP(c_Map_Omap__add(X0,X1,X2,X3),X4)=c_Option_Ooption_ONone(X3)|hAPP(X0,X4)=c_Option_Ooption_ONone(X3))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f491])).
% 0.22/0.69 fof(f1111,plain,(
% 0.22/0.69 ![V_l2,T_a,T_b,V_m]: ((![V_l1]: hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m)=hAPP(V_l2,V_m))|~hBOOL(c_in(V_m,c_Map_Odom(V_l2,T_a,T_b),T_a)))),
% 0.22/0.69 inference(miniscoping,[status(thm)],[f385])).
% 0.22/0.69 fof(f1112,plain,(
% 0.22/0.69 ![X0,X1,X2,X3,X4]: (hAPP(c_Map_Omap__add(X0,X1,X2,X3),X4)=hAPP(X1,X4)|~hBOOL(c_in(X4,c_Map_Odom(X1,X2,X3),X2)))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f1111])).
% 0.22/0.69 fof(f1131,plain,(
% 0.22/0.69 ![X0]: (c_Com_OWT(c_Com_Ocom_OBODY(X0))|hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f398])).
% 0.22/0.69 fof(f1157,plain,(
% 0.22/0.69 ((![V_c]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)|~c_Com_OWT(V_c)))|~c_Com_OWT__bodies)|~c_Hoare__Mirabelle_Ostate__not__singleton),
% 0.22/0.69 inference(miniscoping,[status(thm)],[f415])).
% 0.22/0.69 fof(f1158,plain,(
% 0.22/0.69 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)|~c_Com_OWT(X0)|~c_Com_OWT__bodies|~c_Hoare__Mirabelle_Ostate__not__singleton)),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f1157])).
% 0.22/0.69 fof(f1169,plain,(
% 0.22/0.69 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f422])).
% 0.22/0.69 fof(f1186,plain,(
% 0.22/0.69 ![V_S,V_x]: (hBOOL(hAPP(V_S,V_x))|(![T_a]: ~hBOOL(c_in(V_x,V_S,T_a))))),
% 0.22/0.69 inference(miniscoping,[status(thm)],[f435])).
% 0.22/0.69 fof(f1187,plain,(
% 0.22/0.69 ![X0,X1,X2]: (hBOOL(hAPP(X0,X1))|~hBOOL(c_in(X1,X0,X2)))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f1186])).
% 0.22/0.69 fof(f1202,plain,(
% 0.22/0.69 c_Hoare__Mirabelle_Ostate__not__singleton),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f445])).
% 0.22/0.69 fof(f1203,plain,(
% 0.22/0.69 c_Com_OWT__bodies),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f446])).
% 0.22/0.69 fof(f1205,plain,(
% 0.22/0.69 hBOOL(c_in(v_x,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname))),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f448])).
% 0.22/0.69 fof(f1206,plain,(
% 0.22/0.69 ~c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(c_Com_Ocom_OBODY(v_x)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)),
% 0.22/0.69 inference(cnf_transformation,[status(thm)],[f449])).
% 0.22/0.69 fof(f1842,plain,(
% 0.22/0.69 hBOOL(hAPP(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_x))),
% 0.22/0.69 inference(resolution,[status(thm)],[f1187,f1205])).
% 0.22/0.69 fof(f1882,plain,(
% 0.22/0.69 ![X0]: (hAPP(c_Map_Omap__add(X0,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_x)=hAPP(c_Com_Obody,v_x))),
% 0.22/0.69 inference(resolution,[status(thm)],[f1112,f1205])).
% 0.22/0.69 fof(f2067,plain,(
% 0.22/0.69 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)|~c_Com_OWT(X0)|~c_Hoare__Mirabelle_Ostate__not__singleton)),
% 0.22/0.69 inference(forward_subsumption_resolution,[status(thm)],[f1158,f1203])).
% 0.22/0.69 fof(f2068,plain,(
% 0.22/0.69 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(c_Hoare__Mirabelle_OMGT(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate)|~c_Com_OWT(X0))),
% 0.22/0.69 inference(resolution,[status(thm)],[f2067,f1202])).
% 0.22/0.69 fof(f2205,plain,(
% 0.22/0.69 ~c_Com_OWT(c_Com_Ocom_OBODY(v_x))),
% 0.22/0.69 inference(resolution,[status(thm)],[f2068,f1206])).
% 0.22/0.69 fof(f2230,plain,(
% 0.22/0.69 hAPP(c_Com_Obody,v_x)=c_Option_Ooption_ONone(tc_Com_Ocom)),
% 0.22/0.69 inference(resolution,[status(thm)],[f2205,f1131])).
% 0.22/0.69 fof(f2232,plain,(
% 0.22/0.69 ![X0]: (hAPP(c_Map_Omap__add(X0,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_x)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/0.69 inference(backward_demodulation,[status(thm)],[f2230,f1882])).
% 0.22/0.69 fof(f2322,plain,(
% 0.22/0.69 ![X0]: (hAPP(X0,v_x)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/0.69 inference(resolution,[status(thm)],[f2232,f492])).
% 0.22/0.69 fof(f2337,plain,(
% 0.22/0.69 hBOOL(c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/0.69 inference(backward_demodulation,[status(thm)],[f2322,f1842])).
% 0.22/0.69 fof(f2346,plain,(
% 0.22/0.69 ~hBOOL(c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/0.69 inference(paramodulation,[status(thm)],[f2322,f1169])).
% 0.22/0.69 fof(f2470,plain,(
% 0.22/0.69 $false),
% 0.22/0.69 inference(forward_subsumption_resolution,[status(thm)],[f2346,f2337])).
% 0.22/0.69 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.74 % Elapsed time: 0.240955 seconds
% 0.22/0.74 % CPU time: 0.932344 seconds
% 0.22/0.74 % Total memory used: 113.391 MB
% 0.22/0.74 % Net memory used: 112.917 MB
%------------------------------------------------------------------------------