%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV831-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:14 PM UTC 2026
% Result : Unsatisfiable 1.32s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV831-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n014.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 09:27:04 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 1.32/0.73 % Refutation found
% 1.32/0.73 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.32/0.73 % SZS output start CNFRefutation for theBenchmark
% 1.32/0.73 fof(f81,axiom,(
% 1.32/0.73 (![V_P,T_a]: (c_Collect(V_P,T_a) = V_P ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f344,axiom,(
% 1.32/0.73 (![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) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f379,axiom,(
% 1.32/0.73 (![V_G,V_P,V_c,V_Q,V_xa,V_Z_H,V_x]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)| hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))| ~ hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(V_G,V_P,V_Q,V_c)))| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) ) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f380,axiom,(
% 1.32/0.73 (![V_G,V_P,V_c,V_Q]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)| hBOOL(hAPP(hAPP(V_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(V_G,V_P,V_Q,V_c))) ) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f381,axiom,(
% 1.32/0.73 (![V_G,V_P,V_c,V_Q,V_x,V_xa]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)| ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) ) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f390,axiom,(
% 1.32/0.73 (![T_a,V_a]: (c_Collect(hAPP(c_COMBC(c_fequal(T_a),T_a,T_a,tc_bool),V_a),T_a) = c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f414,axiom,(
% 1.32/0.73 (![V_P,T_a,T_b,V_Q]: (hAPP(c_COMBK(V_P,T_a,T_b),V_Q) = V_P ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f418,negated_conjecture,(
% 1.32/0.73 ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) ),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f419,negated_conjecture,(
% 1.32/0.73 (![V_s,V_Z]: (( c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(hAPP(c_COMBC(c_fequal(tc_Com_Ostate),tc_Com_Ostate,tc_Com_Ostate,tc_bool),V_s),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,c_COMBK(hAPP(v_Q,V_Z),tc_fun(tc_Com_Ostate,tc_bool),t_a),t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s)) ) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f452,axiom,(
% 1.32/0.73 (![T_a,V_x]: (hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ))),
% 1.32/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/0.73 fof(f583,plain,(
% 1.32/0.73 ![X0,X1]: (c_Collect(X0,X1)=X0)),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f81])).
% 1.32/0.73 fof(f984,plain,(
% 1.32/0.73 ![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))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f344])).
% 1.32/0.73 fof(f1036,plain,(
% 1.32/0.73 ![V_G,V_c,V_xa,V_x]: ((![V_P,V_Q,V_Z_H]: ((c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa))))|~hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(V_G,V_P,V_Q,V_c)))))|~c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(miniscoping,[status(thm)],[f379])).
% 1.32/0.73 fof(f1037,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X6,X4)))|~hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f1036])).
% 1.32/0.73 fof(f1038,plain,(
% 1.32/0.73 ![X0,X1,X2,X3]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2))))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f380])).
% 1.32/0.73 fof(f1039,plain,(
% 1.32/0.73 ![V_G,V_c,V_x,V_xa]: ((![V_P,V_Q]: (c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|~hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))))|~c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(miniscoping,[status(thm)],[f381])).
% 1.32/0.73 fof(f1040,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|~hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X4,X5)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f1039])).
% 1.32/0.73 fof(f1056,plain,(
% 1.32/0.73 ![X0,X1]: (c_Collect(hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1),X0)=c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f390])).
% 1.32/0.73 fof(f1092,plain,(
% 1.32/0.73 ![X0,X1,X2,X3]: (hAPP(c_COMBK(X0,X1,X2),X3)=X0)),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f414])).
% 1.32/0.73 fof(f1098,plain,(
% 1.32/0.73 ~c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f418])).
% 1.32/0.73 fof(f1099,plain,(
% 1.32/0.73 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(hAPP(c_COMBC(c_fequal(tc_Com_Ostate),tc_Com_Ostate,tc_Com_Ostate,tc_bool),X0),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,c_COMBK(hAPP(v_Q,X1),tc_fun(tc_Com_Ostate,tc_bool),t_a),t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|~hBOOL(hAPP(hAPP(v_P,X1),X0)))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f419])).
% 1.32/0.73 fof(f1142,plain,(
% 1.32/0.73 ![X0,X1]: (hBOOL(hAPP(hAPP(c_fequal(X0),X1),X1)))),
% 1.32/0.73 inference(cnf_transformation,[status(thm)],[f452])).
% 1.32/0.73 fof(f1172,plain,(
% 1.32/0.73 ![X0,X1]: (hAPP(c_fequal(X0),X1)=c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f583,f984])).
% 1.32/0.73 fof(f1204,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)|hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X6,X4)))|~hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1037])).
% 1.32/0.73 fof(f1205,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)|hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X6,X4)))|~hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a)),t_a))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1204])).
% 1.32/0.73 fof(f1206,plain,(
% 1.32/0.73 ![X0,X1,X2,X3]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)|hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2))))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1038])).
% 1.32/0.73 fof(f1207,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)|~hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X4,X5)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1040])).
% 1.32/0.73 fof(f1208,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)|~hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(X0,X1,X3,X2,X4,X5)))|~c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a)),t_a))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1207])).
% 1.32/0.73 fof(f1224,plain,(
% 1.32/0.73 ![X0,X1]: (hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1)=c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f583,f1056])).
% 1.32/0.73 fof(f1227,plain,(
% 1.32/0.73 ![X0,X1]: (hAPP(c_COMBC(c_fequal(X0),X0,X0,tc_bool),X1)=hAPP(c_fequal(X0),X1))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1224])).
% 1.32/0.73 fof(f1248,plain,(
% 1.32/0.73 ~c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1098])).
% 1.32/0.73 fof(f1249,plain,(
% 1.32/0.73 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(hAPP(c_COMBC(c_fequal(tc_Com_Ostate),tc_Com_Ostate,tc_Com_Ostate,tc_bool),X0),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,c_COMBK(hAPP(v_Q,X1),tc_fun(tc_Com_Ostate,tc_bool),t_a),t_a)),t_a)|~hBOOL(hAPP(hAPP(v_P,X1),X0)))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1172,f1099])).
% 1.32/0.73 fof(f1250,plain,(
% 1.32/0.73 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(hAPP(c_fequal(tc_Com_Ostate),X0),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,c_COMBK(hAPP(v_Q,X1),tc_fun(tc_Com_Ostate,tc_bool),t_a),t_a)),t_a)|~hBOOL(hAPP(hAPP(v_P,X1),X0)))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1227,f1249])).
% 1.32/0.73 fof(f1714,plain,(
% 1.32/0.73 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,X1,X2,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),t_a)),t_a))),
% 1.32/0.73 inference(resolution,[status(thm)],[f1206,f1250])).
% 1.32/0.73 fof(f1760,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,X1,X2,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X3,v_c,X4,t_a)),t_a)|hBOOL(hAPP(hAPP(c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,X3,X4,v_c,c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a))))|~hBOOL(hAPP(hAPP(c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,X3,X4,v_c))))),
% 1.32/0.73 inference(resolution,[status(thm)],[f1714,f1205])).
% 1.32/0.73 fof(f1765,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,X1,X2,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X3,v_c,X4,t_a)),t_a)|hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,X3,X4,v_c,c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a))))|~hBOOL(hAPP(hAPP(c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,X3,X4,v_c))))),
% 1.32/0.73 inference(forward_demodulation,[status(thm)],[f1092,f1760])).
% 1.32/0.73 fof(f1766,plain,(
% 1.32/0.73 ![X0,X1,X2,X3,X4]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,X1,X2,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X3,v_c,X4,t_a)),t_a)|hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,X3,X4,v_c,c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),tc_fun(tc_Com_Ostate,tc_bool),t_a))))|~hBOOL(hAPP(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,X3,X4,v_c))))),
% 1.32/0.75 inference(forward_demodulation,[status(thm)],[f1092,f1765])).
% 1.32/0.75 fof(f1874,plain,(
% 1.32/0.75 ![X0,X1,X2,X3,X4]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a)),t_a)|~hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(v_G,X0,X1,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,X0,X1,v_c,c_COMBK(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X2,v_P,X3,X4)),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBK(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X2,v_P,X3,X4)),tc_fun(tc_Com_Ostate,tc_bool),t_a))))|c_Hoare__Mirabelle_Ohoare__derivs(X2,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,X4,X3,t_a)),t_a))),
% 1.32/0.75 inference(resolution,[status(thm)],[f1208,f1714])).
% 1.32/0.75 fof(f2660,plain,(
% 1.32/0.75 c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)|~hBOOL(hAPP(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)))),
% 1.32/0.75 inference(resolution,[status(thm)],[f1874,f1766])).
% 1.32/0.75 fof(f2668,plain,(
% 1.32/0.75 c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a)|~hBOOL(hAPP(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)))),
% 1.32/0.75 inference(duplicate_literals_removal,[status(thm)],[f2660])).
% 1.32/0.75 fof(f2669,plain,(
% 1.32/0.75 ~hBOOL(hAPP(hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,v_P,v_Q,v_c)))),
% 1.32/0.75 inference(forward_subsumption_resolution,[status(thm)],[f2668,f1248])).
% 1.32/0.75 fof(f2954,plain,(
% 1.32/0.75 $false),
% 1.32/0.75 inference(resolution,[status(thm)],[f2669,f1142])).
% 1.32/0.75 % SZS output end CNFRefutation for theBenchmark.p
% 1.18/0.76 % Elapsed time: 0.398552 seconds
% 1.18/0.76 % CPU time: 2.694682 seconds
% 1.18/0.76 % Total memory used: 178.927 MB
% 1.18/0.76 % Net memory used: 175.606 MB
%------------------------------------------------------------------------------