%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV826-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 : n013.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:13 PM UTC 2026
% Result : Unsatisfiable 186.87s 24.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV826-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n013.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 09:27:05 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.50 % Drodi V4.1.1
% 186.87/24.46 % Refutation found
% 186.87/24.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 186.87/24.46 % SZS output start CNFRefutation for theBenchmark
% 186.87/24.46 fof(f13,axiom,(
% 186.87/24.46 (![V_x,V_S,T_a]: (( hBOOL(c_in(V_x,V_S,T_a))| ~ hBOOL(hAPP(V_S,V_x)) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f88,axiom,(
% 186.87/24.46 (![V_P,T_a]: (c_Collect(V_P,T_a) = V_P ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f261,axiom,(
% 186.87/24.46 (![T_a,V_A]: (c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f377,axiom,(
% 186.87/24.46 (![T_a,V_a,V_C,V_D]: (( c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_C),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_D),tc_fun(T_a,tc_bool))| ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool)) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f398,axiom,(
% 186.87/24.46 (![T_a,V_a,V_A]: (( hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = V_A| ~ hBOOL(c_in(V_a,V_A,T_a)) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f405,axiom,(
% 186.87/24.46 (![V_G,V_ts,T_a]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f413,axiom,(
% 186.87/24.46 (![V_a,T_a]: (c_Collect(c_fequal(V_a,T_a),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f441,axiom,(
% 186.87/24.46 (![V_G,V_P,V_c,V_Q,V_xa,V_Z_H,V_x]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f442,axiom,(
% 186.87/24.46 (![V_G,V_P,V_c,V_Q]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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))) ) ))),
% 186.87/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 186.87/24.46 fof(f443,axiom,(
% 186.87/24.46 (![V_G,V_P,V_c,V_Q,V_x,V_xa]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a) ) ))),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f453,axiom,(
% 189.24/24.46 (![V_G,V_ts,T_a,V_G_H]: (( c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a) ) ))),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f471,negated_conjecture,(
% 189.24/24.46 c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P_H,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f472,negated_conjecture,(
% 189.24/24.46 ~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a) ),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f473,negated_conjecture,(
% 189.24/24.46 (![V_Z,V_s]: (( hBOOL(hAPP(hAPP(v_P_H,V_Z),V_s))| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s)) ) ))),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f498,axiom,(
% 189.24/24.46 (![V_x,T_a]: (hBOOL(hAPP(c_fequal(V_x,T_a),V_x)) ))),
% 189.24/24.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 189.24/24.46 fof(f518,plain,(
% 189.24/24.46 ![V_x,V_S]: ((![T_a]: hBOOL(c_in(V_x,V_S,T_a)))|~hBOOL(hAPP(V_S,V_x)))),
% 189.24/24.46 inference(miniscoping,[status(thm)],[f13])).
% 189.24/24.46 fof(f519,plain,(
% 189.24/24.46 ![X0,X1,X2]: (hBOOL(c_in(X0,X1,X2))|~hBOOL(hAPP(X1,X0)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f518])).
% 189.24/24.46 fof(f635,plain,(
% 189.24/24.46 ![X0,X1]: (c_Collect(X0,X1)=X0)),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f88])).
% 189.24/24.46 fof(f919,plain,(
% 189.24/24.46 ![X0,X1]: (c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f261])).
% 189.24/24.46 fof(f1111,plain,(
% 189.24/24.46 ![T_a,V_C,V_D]: ((![V_a]: c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_C),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_D),tc_fun(T_a,tc_bool)))|~c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool)))),
% 189.24/24.46 inference(miniscoping,[status(thm)],[f377])).
% 189.24/24.46 fof(f1112,plain,(
% 189.24/24.46 ![X0,X1,X2,X3]: (c_lessequals(hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),hAPP(hAPP(c_Set_Oinsert(X0),X1),X3),tc_fun(X0,tc_bool))|~c_lessequals(X2,X3,tc_fun(X0,tc_bool)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f1111])).
% 189.24/24.46 fof(f1143,plain,(
% 189.24/24.46 ![X0,X1,X2]: (hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)=X2|~hBOOL(c_in(X1,X2,X0)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f398])).
% 189.24/24.46 fof(f1151,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~c_lessequals(X1,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f405])).
% 189.24/24.46 fof(f1160,plain,(
% 189.24/24.46 ![X0,X1]: (c_Collect(c_fequal(X0,X1),X1)=hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f413])).
% 189.24/24.46 fof(f1201,plain,(
% 189.24/24.46 ![V_G,V_c,V_xa,V_x]: ((![V_P,V_Q,V_Z_H]: ((c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(miniscoping,[status(thm)],[f441])).
% 189.24/24.46 fof(f1202,plain,(
% 189.24/24.46 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f1201])).
% 189.24/24.46 fof(f1203,plain,(
% 189.24/24.46 ![X0,X1,X2,X3]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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))))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f442])).
% 189.24/24.46 fof(f1204,plain,(
% 189.24/24.46 ![V_G,V_c,V_x,V_xa]: ((![V_P,V_Q]: (c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(miniscoping,[status(thm)],[f443])).
% 189.24/24.46 fof(f1205,plain,(
% 189.24/24.46 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),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(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f1204])).
% 189.24/24.46 fof(f1220,plain,(
% 189.24/24.46 ![V_ts,T_a,V_G_H]: ((![V_G]: (c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)|~c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)))|~c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a))),
% 189.24/24.46 inference(miniscoping,[status(thm)],[f453])).
% 189.24/24.46 fof(f1221,plain,(
% 189.24/24.46 ![X0,X1,X2,X3]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2)|~c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2)|~c_Hoare__Mirabelle_Ohoare__derivs(X3,X1,X2))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f1220])).
% 189.24/24.46 fof(f1249,plain,(
% 189.24/24.46 c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P_H,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f471])).
% 189.24/24.46 fof(f1250,plain,(
% 189.24/24.46 ~c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a)),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f472])).
% 189.24/24.46 fof(f1251,plain,(
% 189.24/24.46 ![X0,X1]: (hBOOL(hAPP(hAPP(v_P_H,X0),X1))|~hBOOL(hAPP(hAPP(v_P,X0),X1)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f473])).
% 189.24/24.46 fof(f1288,plain,(
% 189.24/24.46 ![X0,X1]: (hBOOL(hAPP(c_fequal(X0,X1),X0)))),
% 189.24/24.46 inference(cnf_transformation,[status(thm)],[f498])).
% 189.24/24.46 fof(f1304,plain,(
% 189.24/24.46 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(v_G,X0,t_a)|~c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(resolution,[status(thm)],[f1221,f1250])).
% 189.24/24.46 fof(f1341,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_lessequals(hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),tc_fun(X0,tc_bool)))),
% 189.24/24.46 inference(resolution,[status(thm)],[f1112,f919])).
% 189.24/24.46 fof(f3185,plain,(
% 189.24/24.46 ![X0,X1,X2]: (hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)=X2|~hBOOL(hAPP(X2,X1)))),
% 189.24/24.46 inference(resolution,[status(thm)],[f1143,f519])).
% 189.24/24.46 fof(f3195,plain,(
% 189.24/24.46 ![X0,X1,X2]: (hAPP(hAPP(c_Set_Oinsert(X0),X1),c_fequal(X1,X2))=c_fequal(X1,X2))),
% 189.24/24.46 inference(resolution,[status(thm)],[f3185,f1288])).
% 189.24/24.46 fof(f23307,plain,(
% 189.24/24.46 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(v_G,X0,t_a)|~c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 189.24/24.46 inference(backward_demodulation,[status(thm)],[f23332,f1304])).
% 189.24/24.46 fof(f23311,plain,(
% 189.24/24.46 c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P_H,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)),
% 189.24/24.46 inference(backward_demodulation,[status(thm)],[f23332,f1249])).
% 189.24/24.46 fof(f23327,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_lessequals(c_fequal(X0,X1),hAPP(hAPP(c_Set_Oinsert(X1),X0),X2),tc_fun(X1,tc_bool)))),
% 189.24/24.46 inference(backward_demodulation,[status(thm)],[f23332,f1341])).
% 189.24/24.46 fof(f23332,plain,(
% 189.24/24.46 ![X0,X1]: (c_fequal(X0,X1)=hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))))),
% 189.24/24.46 inference(forward_demodulation,[status(thm)],[f635,f1160])).
% 189.24/24.46 fof(f23688,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_lessequals(c_fequal(X0,X1),c_fequal(X0,X2),tc_fun(X1,tc_bool)))),
% 189.24/24.46 inference(paramodulation,[status(thm)],[f3195,f23327])).
% 189.24/24.46 fof(f23710,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(c_fequal(X0,X1),c_fequal(X0,tc_Hoare__Mirabelle_Otriple(X2)),X2))),
% 189.24/24.46 inference(resolution,[status(thm)],[f23688,f1151])).
% 189.24/24.46 fof(f23723,plain,(
% 189.24/24.46 ![X0]: (~c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),X0),t_a))),
% 189.24/24.46 inference(resolution,[status(thm)],[f23710,f23307])).
% 189.24/24.46 fof(f45718,plain,(
% 189.24/24.46 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 189.24/24.46 inference(forward_demodulation,[status(thm)],[f23332,f1202])).
% 189.24/24.46 fof(f45719,plain,(
% 189.24/24.46 ![X0,X1,X2,X3,X4,X5,X6]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),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_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 189.24/24.46 inference(forward_demodulation,[status(thm)],[f23332,f45718])).
% 189.24/24.46 fof(f45740,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|hBOOL(hAPP(hAPP(v_Q,X2),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,X0,X1,v_c,v_P_H,v_Q)))|~hBOOL(hAPP(hAPP(v_P_H,X2),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(v_G,X0,X1,v_c))))),
% 189.24/24.46 inference(resolution,[status(thm)],[f45719,f23311])).
% 189.24/24.46 fof(f46510,plain,(
% 189.24/24.46 ![X0,X1,X2,X3]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),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))))),
% 189.24/24.46 inference(forward_demodulation,[status(thm)],[f23332,f1203])).
% 189.24/24.46 fof(f46511,plain,(
% 189.24/24.46 ![X0,X1,X2]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,X1,X2,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|hBOOL(hAPP(hAPP(v_P_H,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,v_P,X2,X1)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,v_P,X2,X1))))),
% 189.24/24.46 inference(resolution,[status(thm)],[f46510,f1251])).
% 189.24/24.46 fof(f46567,plain,(
% 189.24/24.46 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),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,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),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))),t_a))),
% 95.96/24.64 inference(forward_demodulation,[status(thm)],[f23332,f1205])).
% 95.96/24.64 fof(f46568,plain,(
% 95.96/24.64 ![X0,X1,X2,X3,X4,X5]: (c_Hoare__Mirabelle_Ohoare__derivs(X0,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),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_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 95.96/24.64 inference(forward_demodulation,[status(thm)],[f23332,f46567])).
% 95.96/24.64 fof(f46589,plain,(
% 95.96/24.64 ![X0,X1]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(X0,v_c,X1,t_a),tc_Hoare__Mirabelle_Otriple(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,v_P_H,v_Q))))),
% 95.96/24.64 inference(resolution,[status(thm)],[f46568,f23311])).
% 95.96/24.64 fof(f49142,plain,(
% 95.96/24.64 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,X0,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,X0,t_a),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,X0,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,v_P,X0,v_c,v_P_H,v_Q))))),
% 95.96/24.64 inference(resolution,[status(thm)],[f46511,f45740])).
% 95.96/24.64 fof(f49168,plain,(
% 95.96/24.64 ![X0]: (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,X0,t_a),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,X0,v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(v_G,v_P,X0,v_c,v_P_H,v_Q))))),
% 95.96/24.64 inference(duplicate_literals_removal,[status(thm)],[f49142])).
% 95.96/24.64 fof(f69061,plain,(
% 95.96/24.64 c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)),
% 95.96/24.64 inference(resolution,[status(thm)],[f49168,f46589])).
% 95.96/24.64 fof(f69094,definition,(
% 95.96/24.64 sQ529_spl <=> (c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a))),
% 95.96/24.64 introduced(definition,[new_symbols(definition,[sQ529_spl])],[split_symbol_definition])).
% 95.96/24.64 fof(f69095,plain,(
% 95.96/24.64 c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_fequal(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),t_a)|~sQ529_spl),
% 95.96/24.64 inference(component_clause,[status(thm)],[f69094])).
% 95.96/24.64 fof(f69097,plain,(
% 95.96/24.64 sQ529_spl),
% 95.96/24.64 inference(split_clause,[status(thm)],[f69061,f69094])).
% 95.96/24.64 fof(f69098,plain,(
% 95.96/24.64 $false|~sQ529_spl),
% 95.96/24.64 inference(forward_subsumption_resolution,[status(thm)],[f69095,f23723])).
% 95.96/24.64 fof(f69099,plain,(
% 95.96/24.64 ~sQ529_spl),
% 95.96/24.64 inference(contradiction_clause,[status(thm)],[f69098])).
% 95.96/24.64 fof(f69100,plain,(
% 95.96/24.64 $false),
% 95.96/24.64 inference(sat_refutation,[status(thm)],[f69097,f69099])).
% 95.96/24.64 % SZS output end CNFRefutation for theBenchmark.p
% 54.40/24.71 % Elapsed time: 24.261256 seconds
% 54.40/24.71 % CPU time: 190.892508 seconds
% 54.40/24.71 % Total memory used: 1.240 GB
% 54.40/24.71 % Net memory used: 1.179 GB
%------------------------------------------------------------------------------