%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV906-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 : n018.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 10.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV906-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/10.45 % Computer : n018.cluster.edu
% 0.20/10.45 % Model : x86_64 x86_64
% 0.20/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/10.45 % Memory : 8046.5625MB
% 0.20/10.45 % OS : Linux 6.8.0-71-generic
% 0.20/10.45 % CPULimit : 300
% 0.20/10.45 % WCLimit : 300
% 0.20/10.45 % DateTime : Mon Sep 21 09:33:24 UTC 2026
% 0.20/10.46 % CPUTime :
% 0.20/10.49 % Drodi V4.1.1
% 0.22/10.56 % Refutation found
% 0.22/10.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/10.56 % SZS output start CNFRefutation for theBenchmark
% 0.22/10.56 fof(f115,axiom,(
% 0.22/10.56 (![V_P,T_a]: (c_Collect(V_P,T_a) = V_P ))),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f247,axiom,(
% 0.22/10.56 (![V_xa,T_a]: (c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a) ))),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f398,axiom,(
% 0.22/10.56 (![T_a,V_a]: (c_Collect(hAPP(c_fequal(T_a),V_a),T_a) = c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) ))),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f436,axiom,(
% 0.22/10.56 (![V_pn]: (( c_Com_OWT(hAPP(c_Com_Ocom_OBODY,V_pn))| hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ) ))),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f451,axiom,(
% 0.22/10.56 (![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(hAPP(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/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f474,negated_conjecture,(
% 0.22/10.56 c_Hoare__Mirabelle_Ostate__not__singleton ),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f475,negated_conjecture,(
% 0.22/10.56 c_Com_OWT__bodies ),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f477,negated_conjecture,(
% 0.22/10.56 hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom) ),
% 0.22/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f479,negated_conjecture,(
% 0.22/10.56 ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn)),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/10.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/10.56 fof(f696,plain,(
% 0.22/10.56 ![X0,X1]: (c_Collect(X0,X1)=X0)),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f115])).
% 0.22/10.56 fof(f898,plain,(
% 0.22/10.56 ![X0,X1]: (~c_Option_Ooption_OSome(X0,X1)=c_Option_Ooption_ONone(X1))),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f247])).
% 0.22/10.56 fof(f1116,plain,(
% 0.22/10.56 ![X0,X1]: (c_Collect(hAPP(c_fequal(X0),X1),X0)=c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f398])).
% 0.22/10.56 fof(f1171,plain,(
% 0.22/10.56 ![X0]: (c_Com_OWT(hAPP(c_Com_Ocom_OBODY,X0))|hAPP(c_Com_Obody,X0)=c_Option_Ooption_ONone(tc_Com_Ocom))),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f436])).
% 0.22/10.56 fof(f1194,plain,(
% 0.22/10.56 ((![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(hAPP(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/10.56 inference(miniscoping,[status(thm)],[f451])).
% 0.22/10.56 fof(f1195,plain,(
% 0.22/10.56 ![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(hAPP(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/10.56 inference(cnf_transformation,[status(thm)],[f1194])).
% 0.22/10.56 fof(f1230,plain,(
% 0.22/10.56 c_Hoare__Mirabelle_Ostate__not__singleton),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f474])).
% 0.22/10.56 fof(f1231,plain,(
% 0.22/10.56 c_Com_OWT__bodies),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f475])).
% 0.22/10.56 fof(f1233,plain,(
% 0.22/10.56 hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_OSome(v_y,tc_Com_Ocom)),
% 0.22/10.56 inference(cnf_transformation,[status(thm)],[f477])).
% 0.22/10.56 fof(f1235,plain,(
% 0.22/10.56 ~c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn)),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/10.56 inference(cnf_transformation,[status(thm)],[f479])).
% 0.22/10.56 fof(f1309,plain,(
% 0.22/10.56 ![X0,X1]: (hAPP(c_fequal(X0),X1)=c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 0.22/10.56 inference(forward_demodulation,[status(thm)],[f696,f1116])).
% 0.22/10.56 fof(f1353,plain,(
% 0.22/10.56 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,X0)),tc_Com_Ostate)|~c_Com_OWT(X0)|~c_Com_OWT__bodies|~c_Hoare__Mirabelle_Ostate__not__singleton)),
% 0.22/10.56 inference(forward_demodulation,[status(thm)],[f1309,f1195])).
% 0.22/10.56 fof(f1368,plain,(
% 0.22/10.56 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,X0)),tc_Com_Ostate)|~c_Com_OWT(X0)|~c_Com_OWT__bodies)),
% 0.22/10.56 inference(backward_subsumption_resolution,[status(thm)],[f1353,f1230])).
% 0.22/10.56 fof(f1374,plain,(
% 0.22/10.56 ~c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn))),tc_Com_Ostate)),
% 0.22/10.56 inference(forward_demodulation,[status(thm)],[f1309,f1235])).
% 0.22/10.56 fof(f1378,plain,(
% 0.22/10.56 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,X0)),tc_Com_Ostate)|~c_Com_OWT(X0))),
% 0.22/10.56 inference(forward_subsumption_resolution,[status(thm)],[f1368,f1231])).
% 0.22/10.56 fof(f1384,plain,(
% 0.22/10.56 ~c_Com_OWT(hAPP(c_Com_Ocom_OBODY,v_pn))),
% 0.22/10.56 inference(resolution,[status(thm)],[f1374,f1378])).
% 0.22/10.56 fof(f1395,plain,(
% 0.22/10.56 hAPP(c_Com_Obody,v_pn)=c_Option_Ooption_ONone(tc_Com_Ocom)),
% 0.22/10.56 inference(resolution,[status(thm)],[f1171,f1384])).
% 0.22/10.56 fof(f1396,plain,(
% 0.22/10.56 c_Option_Ooption_ONone(tc_Com_Ocom)=c_Option_Ooption_OSome(v_y,tc_Com_Ocom)),
% 0.22/10.56 inference(backward_demodulation,[status(thm)],[f1395,f1233])).
% 0.22/10.56 fof(f1397,plain,(
% 0.22/10.56 $false),
% 0.22/10.56 inference(forward_subsumption_resolution,[status(thm)],[f1396,f898])).
% 0.22/10.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/10.61 % Elapsed time: 0.143285 seconds
% 0.22/10.61 % CPU time: 0.497879 seconds
% 0.22/10.61 % Total memory used: 111.426 MB
% 0.22/10.61 % Net memory used: 111.186 MB
%------------------------------------------------------------------------------