%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:09:15 PM UTC 2026
% Result : Theorem 80.07s 10.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:59:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 80.07/10.54 % Refutation found
% 80.07/10.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 80.07/10.54 % SZS output start CNFRefutation for theBenchmark
% 80.07/10.54 fof(f23,axiom,(
% 80.07/10.54 ti(bool,fFalse) = fFalse ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f32,axiom,(
% 80.07/10.54 (! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f38,axiom,(
% 80.07/10.54 (! [X_a,G] : hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),bot_bot(fun(hoare_509422987triple(X_a),bool)))) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f42,axiom,(
% 80.07/10.54 (! [X_a,G,G_2,Ts] :( hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G_2),Ts))=> ( hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),G_2))=> hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),Ts)) ) ) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f57,axiom,(
% 80.07/10.54 (! [C_1] :( hBOOL(hoare_1883395792gleton)=> ( hBOOL(wT_bodies)=> ( hBOOL(hAPP(com,bool,wt,C_1))=> hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_509422987triple(state),bool))))) ) ) ) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f115,axiom,(
% 80.07/10.54 (! [X_a,P_1] : hAPP(fun(X_a,bool),fun(X_a,bool),collect(X_a),P_1) = ti(fun(X_a,bool),P_1) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f128,axiom,(
% 80.07/10.54 (! [X_a,A_3] : hAPP(fun(X_a,bool),fun(X_a,bool),collect(X_a),hAPP(X_a,fun(X_a,bool),fequal(X_a),A_3)) = hAPP(fun(X_a,bool),fun(X_a,bool),hAPP(X_a,fun(fun(X_a,bool),fun(X_a,bool)),insert(X_a),A_3),bot_bot(fun(X_a,bool))) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f130,axiom,(
% 80.07/10.54 (! [Pn,B_2] :( hBOOL(wT_bodies)=> ( hAPP(pname,option(com),body,Pn) = hAPP(com,option(com),some(com),B_2)=> hBOOL(hAPP(com,bool,wt,B_2)) ) ) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f146,axiom,(
% 80.07/10.54 (! [X_a,P] : hAPP(X_a,X_a,combi(X_a),P) = ti(X_a,P) )),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f155,axiom,(
% 80.07/10.54 ~ hBOOL(fFalse) ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f162,hypothesis,(
% 80.07/10.54 hBOOL(hoare_1883395792gleton) ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f163,hypothesis,(
% 80.07/10.54 hBOOL(wT_bodies) ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f167,hypothesis,(
% 80.07/10.54 hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y) ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f169,conjecture,(
% 80.07/10.54 hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))) ),
% 80.07/10.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 80.07/10.54 fof(f170,negated_conjecture,(
% 80.07/10.54 ~(hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))) )),
% 80.07/10.54 inference(negated_conjecture,[status(cth)],[f169])).
% 80.07/10.54 fof(f193,plain,(
% 80.07/10.54 ti(bool,fFalse)=fFalse),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f23])).
% 80.07/10.54 fof(f202,plain,(
% 80.07/10.54 ![X0,X1,X2,X3]: (ti(X0,hAPP(X1,X0,X2,X3))=hAPP(X1,X0,X2,X3))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f32])).
% 80.07/10.54 fof(f211,plain,(
% 80.07/10.54 ![X0,X1]: (hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),bot_bot(fun(hoare_509422987triple(X0),bool)))))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f38])).
% 80.07/10.54 fof(f220,plain,(
% 80.07/10.54 ![X_a,G,G_2,Ts]: (~hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G_2),Ts))|(~hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),G_2))|hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),Ts))))),
% 80.07/10.54 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 80.07/10.54 fof(f221,plain,(
% 80.07/10.54 ![X_a,G_2,Ts]: (~hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G_2),Ts))|(![G]: (~hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),G_2))|hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),Ts)))))),
% 80.07/10.54 inference(miniscoping,[status(thm)],[f220])).
% 80.07/10.54 fof(f222,plain,(
% 80.07/10.54 ![X0,X1,X2,X3]: (~hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X2))|~hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X3),X1))|hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X3),X2)))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f221])).
% 80.07/10.54 fof(f259,plain,(
% 80.07/10.54 ![C_1]: (~hBOOL(hoare_1883395792gleton)|(~hBOOL(wT_bodies)|(~hBOOL(hAPP(com,bool,wt,C_1))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_509422987triple(state),bool))))))))),
% 80.07/10.54 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 80.07/10.54 fof(f260,plain,(
% 80.07/10.54 ~hBOOL(hoare_1883395792gleton)|(~hBOOL(wT_bodies)|(![C_1]: (~hBOOL(hAPP(com,bool,wt,C_1))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_509422987triple(state),bool))))))))),
% 80.07/10.54 inference(miniscoping,[status(thm)],[f259])).
% 80.07/10.54 fof(f261,plain,(
% 80.07/10.54 ![X0]: (~hBOOL(hoare_1883395792gleton)|~hBOOL(wT_bodies)|~hBOOL(hAPP(com,bool,wt,X0))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool))))))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f260])).
% 80.07/10.54 fof(f425,plain,(
% 80.07/10.54 ![X0,X1]: (hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)=ti(fun(X0,bool),X1))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f115])).
% 80.07/10.54 fof(f465,plain,(
% 80.07/10.54 ![X0,X1]: (hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1))=hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f128])).
% 80.07/10.54 fof(f471,plain,(
% 80.07/10.54 ![Pn,B_2]: (~hBOOL(wT_bodies)|(~hAPP(pname,option(com),body,Pn)=hAPP(com,option(com),some(com),B_2)|hBOOL(hAPP(com,bool,wt,B_2))))),
% 80.07/10.54 inference(pre_NNF_transformation,[status(thm)],[f130])).
% 80.07/10.54 fof(f472,plain,(
% 80.07/10.54 ~hBOOL(wT_bodies)|(![B_2]: ((![Pn]: ~hAPP(pname,option(com),body,Pn)=hAPP(com,option(com),some(com),B_2))|hBOOL(hAPP(com,bool,wt,B_2))))),
% 80.07/10.54 inference(miniscoping,[status(thm)],[f471])).
% 80.07/10.54 fof(f473,plain,(
% 80.07/10.54 ![X0,X1]: (~hBOOL(wT_bodies)|~hAPP(pname,option(com),body,X0)=hAPP(com,option(com),some(com),X1)|hBOOL(hAPP(com,bool,wt,X1)))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f472])).
% 80.07/10.54 fof(f514,plain,(
% 80.07/10.54 ![X0,X1]: (hAPP(X0,X0,combi(X0),X1)=ti(X0,X1))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f146])).
% 80.07/10.54 fof(f528,plain,(
% 80.07/10.54 ~hBOOL(fFalse)),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f155])).
% 80.07/10.54 fof(f538,plain,(
% 80.07/10.54 hBOOL(hoare_1883395792gleton)),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f162])).
% 80.07/10.54 fof(f539,plain,(
% 80.07/10.54 hBOOL(wT_bodies)),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f163])).
% 80.07/10.54 fof(f543,plain,(
% 80.07/10.54 hAPP(pname,option(com),body,pn)=hAPP(com,option(com),some(com),y)),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f167])).
% 80.07/10.54 fof(f545,plain,(
% 80.07/10.54 ~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool)))))),
% 80.07/10.54 inference(cnf_transformation,[status(thm)],[f170])).
% 80.07/10.54 fof(f546,definition,(
% 80.07/10.54 sQ0_spl <=> (hBOOL(hoare_1883395792gleton))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f548,plain,(
% 80.07/10.54 ~hBOOL(hoare_1883395792gleton)|sQ0_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f546])).
% 80.07/10.54 fof(f549,definition,(
% 80.07/10.54 sQ1_spl <=> (hBOOL(wT_bodies))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f551,plain,(
% 80.07/10.54 ~hBOOL(wT_bodies)|sQ1_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f549])).
% 80.07/10.54 fof(f552,definition,(
% 80.07/10.54 ![X0]: (sQ2_spl <=> (~hBOOL(hAPP(com,bool,wt,X0))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool)))))))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f553,plain,(
% 80.07/10.54 ![X0]: (~hBOOL(hAPP(com,bool,wt,X0))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool)))))|~sQ2_spl)),
% 80.07/10.54 inference(component_clause,[status(thm)],[f552])).
% 80.07/10.54 fof(f555,plain,(
% 80.07/10.54 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 80.07/10.54 inference(split_clause,[status(thm)],[f261,f546,f549,f552])).
% 80.07/10.54 fof(f564,definition,(
% 80.07/10.54 ![X0,X1]: (sQ5_spl <=> (~hAPP(pname,option(com),body,X0)=hAPP(com,option(com),some(com),X1)|hBOOL(hAPP(com,bool,wt,X1))))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f565,plain,(
% 80.07/10.54 ![X0,X1]: (~hAPP(pname,option(com),body,X0)=hAPP(com,option(com),some(com),X1)|hBOOL(hAPP(com,bool,wt,X1))|~sQ5_spl)),
% 80.07/10.54 inference(component_clause,[status(thm)],[f564])).
% 80.07/10.54 fof(f567,plain,(
% 80.07/10.54 ~sQ1_spl|sQ5_spl),
% 80.07/10.54 inference(split_clause,[status(thm)],[f473,f549,f564])).
% 80.07/10.54 fof(f570,plain,(
% 80.07/10.54 $false|sQ0_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f548,f538])).
% 80.07/10.54 fof(f571,plain,(
% 80.07/10.54 sQ0_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f570])).
% 80.07/10.54 fof(f572,plain,(
% 80.07/10.54 $false|sQ1_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f551,f539])).
% 80.07/10.54 fof(f573,plain,(
% 80.07/10.54 sQ1_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f572])).
% 80.07/10.54 fof(f587,definition,(
% 80.07/10.54 sQ7_spl <=> (pn=pn)),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f589,plain,(
% 80.07/10.54 ~pn=pn|sQ7_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f587])).
% 80.07/10.54 fof(f744,plain,(
% 80.07/10.54 ![X0]: (~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),X0),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool)))))|~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),X0)))),
% 80.07/10.54 inference(resolution,[status(thm)],[f222,f545])).
% 80.07/10.54 fof(f756,definition,(
% 80.07/10.54 sQ28_spl <=> (hBOOL(fFalse))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f757,plain,(
% 80.07/10.54 hBOOL(fFalse)|~sQ28_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f756])).
% 80.07/10.54 fof(f869,plain,(
% 80.07/10.54 ~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool)))))),
% 80.07/10.54 inference(resolution,[status(thm)],[f744,f211])).
% 80.07/10.54 fof(f871,plain,(
% 80.07/10.54 ![X0]: (~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),X0),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool)))))|~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),X0)))),
% 80.07/10.54 inference(resolution,[status(thm)],[f869,f222])).
% 80.07/10.54 fof(f1043,definition,(
% 80.07/10.54 sQ43_spl <=> (hoare_1883395792gleton=fFalse)),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f1044,plain,(
% 80.07/10.54 hoare_1883395792gleton=fFalse|~sQ43_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f1043])).
% 80.07/10.54 fof(f1050,definition,(
% 80.07/10.54 sQ45_spl <=> (wT_bodies=fFalse)),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f1051,plain,(
% 80.07/10.54 wT_bodies=fFalse|~sQ45_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f1050])).
% 80.07/10.54 fof(f1108,definition,(
% 80.07/10.54 ![X0]: (sQ52_spl <=> (hBOOL(X0)))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f1109,plain,(
% 80.07/10.54 ![X0]: (hBOOL(X0)|~sQ52_spl)),
% 80.07/10.54 inference(component_clause,[status(thm)],[f1108])).
% 80.07/10.54 fof(f1206,plain,(
% 80.07/10.54 hBOOL(fFalse)|~sQ45_spl),
% 80.07/10.54 inference(backward_demodulation,[status(thm)],[f1051,f539])).
% 80.07/10.54 fof(f1207,plain,(
% 80.07/10.54 $false|~sQ45_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f1206,f528])).
% 80.07/10.54 fof(f1208,plain,(
% 80.07/10.54 ~sQ45_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f1207])).
% 80.07/10.54 fof(f1217,plain,(
% 80.07/10.54 hBOOL(fFalse)|~sQ43_spl),
% 80.07/10.54 inference(backward_demodulation,[status(thm)],[f1044,f538])).
% 80.07/10.54 fof(f1218,plain,(
% 80.07/10.54 $false|~sQ43_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f1217,f528])).
% 80.07/10.54 fof(f1219,plain,(
% 80.07/10.54 ~sQ43_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f1218])).
% 80.07/10.54 fof(f1303,plain,(
% 80.07/10.54 $false|~sQ28_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f757,f528])).
% 80.07/10.54 fof(f1304,plain,(
% 80.07/10.54 ~sQ28_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f1303])).
% 80.07/10.54 fof(f2955,plain,(
% 80.07/10.54 $false|sQ7_spl),
% 80.07/10.54 inference(trivial_equality_resolution,[status(thm)],[f589])).
% 80.07/10.54 fof(f2956,plain,(
% 80.07/10.54 sQ7_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f2955])).
% 80.07/10.54 fof(f2971,definition,(
% 80.07/10.54 sQ106_spl <=> (fTrue=fTrue)),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f2973,plain,(
% 80.07/10.54 ~fTrue=fTrue|sQ106_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f2971])).
% 80.07/10.54 fof(f3015,definition,(
% 80.07/10.54 sQ112_spl <=> (y=y)),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f3017,plain,(
% 80.07/10.54 ~y=y|sQ112_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f3015])).
% 80.07/10.54 fof(f4627,definition,(
% 80.07/10.54 ![X0]: (sQ119_spl <=> (~bot_bot(fun(X0,bool))=bot_bot(fun(X0,bool))))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f4628,plain,(
% 80.07/10.54 ![X0]: (~bot_bot(fun(X0,bool))=bot_bot(fun(X0,bool))|~sQ119_spl)),
% 80.07/10.54 inference(component_clause,[status(thm)],[f4627])).
% 80.07/10.54 fof(f5323,definition,(
% 80.07/10.54 sQ163_spl <=> (bot_bot(fun(fun(hoare_509422987triple(state),bool),bool))=bot_bot(fun(fun(hoare_509422987triple(state),bool),bool)))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f5325,plain,(
% 80.07/10.54 ~bot_bot(fun(fun(hoare_509422987triple(state),bool),bool))=bot_bot(fun(fun(hoare_509422987triple(state),bool),bool))|sQ163_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f5323])).
% 80.07/10.54 fof(f6104,plain,(
% 80.07/10.54 $false|sQ163_spl),
% 80.07/10.54 inference(trivial_equality_resolution,[status(thm)],[f5325])).
% 80.07/10.54 fof(f6105,plain,(
% 80.07/10.54 sQ163_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f6104])).
% 80.07/10.54 fof(f6131,definition,(
% 80.07/10.54 sQ232_spl <=> (hBOOL(hAPP(bool,bool,combi(bool),fFalse)))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f6132,plain,(
% 80.07/10.54 hBOOL(hAPP(bool,bool,combi(bool),fFalse))|~sQ232_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f6131])).
% 80.07/10.54 fof(f6141,plain,(
% 80.07/10.54 hBOOL(ti(bool,fFalse))|~sQ232_spl),
% 80.07/10.54 inference(forward_demodulation,[status(thm)],[f514,f6132])).
% 80.07/10.54 fof(f6142,plain,(
% 80.07/10.54 hBOOL(fFalse)|~sQ232_spl),
% 80.07/10.54 inference(forward_demodulation,[status(thm)],[f193,f6141])).
% 80.07/10.54 fof(f6143,plain,(
% 80.07/10.54 $false|~sQ232_spl),
% 80.07/10.54 inference(forward_subsumption_resolution,[status(thm)],[f6142,f528])).
% 80.07/10.54 fof(f6144,plain,(
% 80.07/10.54 ~sQ232_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f6143])).
% 80.07/10.54 fof(f8857,definition,(
% 80.07/10.54 sQ482_spl <=> (bot_bot(fun(bool,bool))=bot_bot(fun(bool,bool)))),
% 80.07/10.54 introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition])).
% 80.07/10.54 fof(f8859,plain,(
% 80.07/10.54 ~bot_bot(fun(bool,bool))=bot_bot(fun(bool,bool))|sQ482_spl),
% 80.07/10.54 inference(component_clause,[status(thm)],[f8857])).
% 80.07/10.54 fof(f8867,plain,(
% 80.07/10.54 $false|~sQ119_spl),
% 80.07/10.54 inference(trivial_equality_resolution,[status(thm)],[f4628])).
% 80.07/10.54 fof(f8868,plain,(
% 80.07/10.54 ~sQ119_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f8867])).
% 80.07/10.54 fof(f9318,plain,(
% 80.07/10.54 $false|sQ106_spl),
% 80.07/10.54 inference(trivial_equality_resolution,[status(thm)],[f2973])).
% 80.07/10.54 fof(f9319,plain,(
% 80.07/10.54 sQ106_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f9318])).
% 80.07/10.54 fof(f10187,plain,(
% 80.07/10.54 $false|sQ482_spl),
% 80.07/10.54 inference(trivial_equality_resolution,[status(thm)],[f8859])).
% 80.07/10.54 fof(f10188,plain,(
% 80.07/10.54 sQ482_spl),
% 80.07/10.54 inference(contradiction_clause,[status(thm)],[f10187])).
% 80.07/10.54 fof(f11854,plain,(
% 80.07/10.54 ![X0]: (~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),X0),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool)))))|~sQ52_spl)),
% 58.70/10.63 inference(backward_subsumption_resolution,[status(thm)],[f871,f1109])).
% 58.70/10.63 fof(f11927,plain,(
% 58.70/10.63 $false|~sQ52_spl),
% 58.70/10.63 inference(forward_subsumption_resolution,[status(thm)],[f11854,f1109])).
% 58.70/10.63 fof(f11928,plain,(
% 58.70/10.63 ~sQ52_spl),
% 58.70/10.63 inference(contradiction_clause,[status(thm)],[f11927])).
% 58.70/10.63 fof(f25024,plain,(
% 58.70/10.63 ![X0,X1]: (ti(fun(X0,bool),hAPP(X0,fun(X0,bool),fequal(X0),X1))=hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))))),
% 58.70/10.63 inference(forward_demodulation,[status(thm)],[f425,f465])).
% 58.70/10.63 fof(f25046,plain,(
% 58.70/10.63 ![X0,X1]: (hAPP(X0,fun(X0,bool),fequal(X0),X1)=hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))))),
% 58.70/10.63 inference(forward_demodulation,[status(thm)],[f202,f25024])).
% 58.70/10.63 fof(f34287,plain,(
% 58.70/10.63 $false|sQ112_spl),
% 58.70/10.63 inference(trivial_equality_resolution,[status(thm)],[f3017])).
% 58.70/10.63 fof(f34288,plain,(
% 58.70/10.63 sQ112_spl),
% 58.70/10.63 inference(contradiction_clause,[status(thm)],[f34287])).
% 58.70/10.63 fof(f35147,plain,(
% 58.70/10.63 ~hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y))))),
% 58.70/10.63 inference(forward_demodulation,[status(thm)],[f25046,f869])).
% 58.70/10.63 fof(f38827,plain,(
% 58.70/10.63 ![X0]: (~hBOOL(hAPP(com,bool,wt,X0))|hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0))))|~sQ2_spl)),
% 58.70/10.63 inference(forward_demodulation,[status(thm)],[f25046,f553])).
% 58.70/10.63 fof(f38840,plain,(
% 58.70/10.63 hBOOL(hAPP(com,bool,wt,y))|~sQ5_spl),
% 58.70/10.63 inference(resolution,[status(thm)],[f565,f543])).
% 58.70/10.63 fof(f39195,plain,(
% 58.70/10.63 hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y))))|~sQ5_spl|~sQ2_spl),
% 58.70/10.63 inference(resolution,[status(thm)],[f38840,f38827])).
% 58.70/10.63 fof(f39209,plain,(
% 58.70/10.63 $false|~sQ5_spl|~sQ2_spl),
% 58.70/10.63 inference(forward_subsumption_resolution,[status(thm)],[f39195,f35147])).
% 58.70/10.63 fof(f39210,plain,(
% 58.70/10.63 ~sQ5_spl|~sQ2_spl),
% 58.70/10.63 inference(contradiction_clause,[status(thm)],[f39209])).
% 58.70/10.63 fof(f39211,plain,(
% 58.70/10.63 $false),
% 58.70/10.63 inference(sat_refutation,[status(thm)],[f555,f567,f571,f573,f1208,f1219,f1304,f2956,f6105,f6144,f8868,f9319,f10188,f11928,f34288,f39210])).
% 58.70/10.63 % SZS output end CNFRefutation for theBenchmark.p
% 10.51/10.80 % Elapsed time: 10.420364 seconds
% 10.51/10.80 % CPU time: 81.605319 seconds
% 10.51/10.80 % Total memory used: 1.320 GB
% 10.51/10.80 % Net memory used: 1.301 GB
%------------------------------------------------------------------------------