%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW474+1 : TPTP v9.3.1. Released v5.3.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 03:09:15 PM UTC 2026
% Result : Theorem 215.71s 27.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.34 % Computer : n014.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.35 % WCLimit : 300
% 0.06/0.35 % DateTime : Mon Sep 21 09:58:35 UTC 2026
% 0.06/0.35 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 215.71/27.72 % Refutation found
% 215.71/27.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 215.71/27.72 % SZS output start CNFRefutation for theBenchmark
% 215.71/27.72 fof(f3,axiom,(
% 215.71/27.72 (! [B_1_1] :( is_bool(B_1_1)=> is_fun_pname_bool(cOMBK_bool_pname(B_1_1)) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f14,hypothesis,(
% 215.71/27.72 (! [B_1_1] : is_fun_pname_bool(dom_pname_com(B_1_1)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f17,axiom,(
% 215.71/27.72 is_fun1661590463l_bool(bot_bo1649642514l_bool) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f30,axiom,(
% 215.71/27.72 is_bool(fFalse) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f54,axiom,(
% 215.71/27.72 (! [G] : hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),bot_bo620288102e_bool)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f55,axiom,(
% 215.71/27.72 (! [Ts,G] :( hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,Ts),G))=> hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),Ts)) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f58,axiom,(
% 215.71/27.72 (! [G,G_1,Ts] :( hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))=> ( hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),G_1))=> hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),Ts)) ) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f68,axiom,(
% 215.71/27.72 (! [H,Fa] :( hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,Fa))=> hBOOL(hAPP_f971112728l_bool(finite364844667_state,image_2003357581_state(H,Fa))) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f96,axiom,(
% 215.71/27.72 (! [A_2,A] :( hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,A))=> hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(A_2,A))) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f97,axiom,(
% 215.71/27.72 hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,bot_bo844097828e_bool)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f100,axiom,(
% 215.71/27.72 hBOOL(hAPP_f468958928l_bool(finite796539827l_bool,bot_bo1761158942l_bool)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f101,axiom,(
% 215.71/27.72 hBOOL(hAPP_f166538662l_bool(finite464017571e_bool,bot_bo535777328l_bool)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f102,axiom,(
% 215.71/27.72 hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,bot_bo1649642514l_bool)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f131,axiom,(
% 215.71/27.72 (! [F,X_2,Y_2] :( hAPP_p799580910on_com(F,X_2) = some_com(Y_2)=> insert_pname(X_2,dom_pname_com(F)) = dom_pname_com(F) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f157,axiom,(
% 215.71/27.72 (! [C_1] :( hBOOL(hoare_165779456gleton)=> ( hBOOL(wT_bodies)=> ( hBOOL(wt(C_1))=> hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,C_1),bot_bo620288102e_bool))) ) ) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f158,axiom,(
% 215.71/27.72 (! [A_2] : ~ hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A_2),bot_bo620288102e_bool)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f159,axiom,(
% 215.71/27.72 (! [A_2] : ~ hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,A_2),bot_bo1649642514l_bool)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f160,axiom,(
% 215.71/27.72 (! [A_2] : ~ hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,A_2),bot_bo535777328l_bool)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f161,axiom,(
% 215.71/27.72 (! [A_2] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),bot_bo844097828e_bool)) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f163,axiom,(
% 215.71/27.72 (! [B_1,A_2,B] :( ( ~ hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,A_2),B))=> A_2 = B_1 )=> hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,A_2),insert1325755072e_bool(B_1,B))) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f164,axiom,(
% 215.71/27.72 (! [B_1,A_2,B] :( ( ~ hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,A_2),B))=> A_2 = B_1 )=> hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,A_2),insert1556680138e_bool(B_1,B))) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f218,axiom,(
% 215.71/27.72 bot_bo535777328l_bool = collec1823980261e_bool(cOMBK_129401207e_bool(fFalse)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f219,axiom,(
% 215.71/27.72 bot_bo1649642514l_bool = collec1974731493e_bool(cOMBK_1857069011e_bool(fFalse)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f221,axiom,(
% 215.71/27.72 bot_bo844097828e_bool = collect_pname(cOMBK_bool_pname(fFalse)) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f247,axiom,(
% 215.71/27.72 (! [A,B] :( A = B=> ~ ( hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,A),B))=> ~ hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,B),A)) ) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f283,axiom,(
% 215.71/27.72 (! [A_2,A] : insert_pname(A_2,A) != bot_bo844097828e_bool )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f284,axiom,(
% 215.71/27.72 (! [A_2,A] : insert1415133716_state(A_2,A) != bot_bo620288102e_bool )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f294,axiom,(
% 215.71/27.72 (! [F] : image_2003357581_state(F,bot_bo844097828e_bool) = bot_bo620288102e_bool )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f308,axiom,(
% 215.71/27.72 (! [P_1] :( is_fun_pname_bool(P_1)=> collect_pname(P_1) = P_1 ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f309,axiom,(
% 215.71/27.72 (! [P_1] : collec307967673_state(P_1) = P_1 )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f310,axiom,(
% 215.71/27.72 (! [P_1] :( is_fun1661590463l_bool(P_1)=> collec1974731493e_bool(P_1) = P_1 ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f311,axiom,(
% 215.71/27.72 (! [P_1] : collec1823980261e_bool(P_1) = P_1 )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f338,axiom,(
% 215.71/27.72 (! [A_2] : collec307967673_state(hAPP_H1049623551e_bool(fequal1111551311_state,A_2)) = insert1415133716_state(A_2,bot_bo620288102e_bool) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f342,axiom,(
% 215.71/27.72 (! [Pn,B_2] :( hBOOL(wT_bodies)=> ( hAPP_p799580910on_com(body,Pn) = some_com(B_2)=> hBOOL(wt(B_2)) ) ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f352,axiom,(
% 215.71/27.72 hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body))) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f362,axiom,(
% 215.71/27.72 ~ hBOOL(fFalse) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f397,axiom,(
% 215.71/27.72 (! [P,Q] :( is_bool(P)=> hAPP_f971112728l_bool(cOMBK_129401207e_bool(P),Q) = P ) )),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f421,hypothesis,(
% 215.71/27.72 hBOOL(hoare_165779456gleton) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f422,hypothesis,(
% 215.71/27.72 hBOOL(wT_bodies) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f426,hypothesis,(
% 215.71/27.72 hAPP_p799580910on_com(body,pn) = some_com(y) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f428,conjecture,(
% 215.71/27.72 hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))) ),
% 215.71/27.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 215.71/27.72 fof(f429,negated_conjecture,(
% 215.71/27.72 ~(hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))) )),
% 215.71/27.72 inference(negated_conjecture,[status(cth)],[f428])).
% 215.71/27.72 fof(f436,plain,(
% 215.71/27.72 ![B_1_1]: (~is_bool(B_1_1)|is_fun_pname_bool(cOMBK_bool_pname(B_1_1)))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 215.71/27.72 fof(f437,plain,(
% 215.71/27.72 ![X0]: (~is_bool(X0)|is_fun_pname_bool(cOMBK_bool_pname(X0)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f436])).
% 215.71/27.72 fof(f453,plain,(
% 215.71/27.72 ![X0]: (is_fun_pname_bool(dom_pname_com(X0)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f14])).
% 215.71/27.72 fof(f456,plain,(
% 215.71/27.72 is_fun1661590463l_bool(bot_bo1649642514l_bool)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f17])).
% 215.71/27.72 fof(f479,plain,(
% 215.71/27.72 is_bool(fFalse)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f30])).
% 215.71/27.72 fof(f523,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),bot_bo620288102e_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f54])).
% 215.71/27.72 fof(f524,plain,(
% 215.71/27.72 ![Ts,G]: (~hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,Ts),G))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),Ts)))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 215.71/27.72 fof(f525,plain,(
% 215.71/27.72 ![X0,X1]: (~hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,X0),X1))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X1),X0)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f524])).
% 215.71/27.72 fof(f532,plain,(
% 215.71/27.72 ![G,G_1,Ts]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))|(~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),G_1))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),Ts))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 215.71/27.72 fof(f533,plain,(
% 215.71/27.72 ![G_1,Ts]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))|(![G]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),G_1))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G),Ts)))))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f532])).
% 215.71/27.72 fof(f534,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),X1))|~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X2),X0))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X2),X1)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f533])).
% 215.71/27.72 fof(f555,plain,(
% 215.71/27.72 ![H,Fa]: (~hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,Fa))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,image_2003357581_state(H,Fa))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 215.71/27.72 fof(f556,plain,(
% 215.71/27.72 ![Fa]: (~hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,Fa))|(![H]: hBOOL(hAPP_f971112728l_bool(finite364844667_state,image_2003357581_state(H,Fa)))))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f555])).
% 215.71/27.72 fof(f557,plain,(
% 215.71/27.72 ![X0,X1]: (~hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,X0))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,image_2003357581_state(X1,X0))))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f556])).
% 215.71/27.72 fof(f631,plain,(
% 215.71/27.72 ![A_2,A]: (~hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,A))|hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(A_2,A))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 215.71/27.72 fof(f632,plain,(
% 215.71/27.72 ![A]: (~hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,A))|(![A_2]: hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(A_2,A)))))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f631])).
% 215.71/27.72 fof(f633,plain,(
% 215.71/27.72 ![X0,X1]: (~hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,X0))|hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(X1,X0))))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f632])).
% 215.71/27.72 fof(f634,plain,(
% 215.71/27.72 hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,bot_bo844097828e_bool))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f97])).
% 215.71/27.72 fof(f637,plain,(
% 215.71/27.72 hBOOL(hAPP_f468958928l_bool(finite796539827l_bool,bot_bo1761158942l_bool))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f100])).
% 215.71/27.72 fof(f638,plain,(
% 215.71/27.72 hBOOL(hAPP_f166538662l_bool(finite464017571e_bool,bot_bo535777328l_bool))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f101])).
% 215.71/27.72 fof(f639,plain,(
% 215.71/27.72 hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,bot_bo1649642514l_bool))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f102])).
% 215.71/27.72 fof(f735,plain,(
% 215.71/27.72 ![F,X_2,Y_2]: (~hAPP_p799580910on_com(F,X_2)=some_com(Y_2)|insert_pname(X_2,dom_pname_com(F))=dom_pname_com(F))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f131])).
% 215.71/27.72 fof(f736,plain,(
% 215.71/27.72 ![F,X_2]: ((![Y_2]: ~hAPP_p799580910on_com(F,X_2)=some_com(Y_2))|insert_pname(X_2,dom_pname_com(F))=dom_pname_com(F))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f735])).
% 215.71/27.72 fof(f737,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~hAPP_p799580910on_com(X0,X1)=some_com(X2)|insert_pname(X1,dom_pname_com(X0))=dom_pname_com(X0))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f736])).
% 215.71/27.72 fof(f811,plain,(
% 215.71/27.72 ![C_1]: (~hBOOL(hoare_165779456gleton)|(~hBOOL(wT_bodies)|(~hBOOL(wt(C_1))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,C_1),bot_bo620288102e_bool))))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f157])).
% 215.71/27.72 fof(f812,plain,(
% 215.71/27.72 ~hBOOL(hoare_165779456gleton)|(~hBOOL(wT_bodies)|(![C_1]: (~hBOOL(wt(C_1))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,C_1),bot_bo620288102e_bool))))))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f811])).
% 215.71/27.72 fof(f813,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hoare_165779456gleton)|~hBOOL(wT_bodies)|~hBOOL(wt(X0))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,X0),bot_bo620288102e_bool))))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f812])).
% 215.71/27.72 fof(f814,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X0),bot_bo620288102e_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f158])).
% 215.71/27.72 fof(f815,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,X0),bot_bo1649642514l_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f159])).
% 215.71/27.72 fof(f816,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,X0),bot_bo535777328l_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f160])).
% 215.71/27.72 fof(f817,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f161])).
% 215.71/27.72 fof(f821,plain,(
% 215.71/27.72 ![B_1,A_2,B]: ((~hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,A_2),B))&~A_2=B_1)|hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,A_2),insert1325755072e_bool(B_1,B))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f163])).
% 215.71/27.72 fof(f823,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~X0=X1|hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,X0),insert1325755072e_bool(X1,X2))))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f821])).
% 215.71/27.72 fof(f824,plain,(
% 215.71/27.72 ![B_1,A_2,B]: ((~hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,A_2),B))&~A_2=B_1)|hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,A_2),insert1556680138e_bool(B_1,B))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f164])).
% 215.71/27.72 fof(f826,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~X0=X1|hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,X0),insert1556680138e_bool(X1,X2))))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f824])).
% 215.71/27.72 fof(f1026,plain,(
% 215.71/27.72 bot_bo535777328l_bool=collec1823980261e_bool(cOMBK_129401207e_bool(fFalse))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f218])).
% 215.71/27.72 fof(f1027,plain,(
% 215.71/27.72 bot_bo1649642514l_bool=collec1974731493e_bool(cOMBK_1857069011e_bool(fFalse))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f219])).
% 215.71/27.72 fof(f1029,plain,(
% 215.71/27.72 bot_bo844097828e_bool=collect_pname(cOMBK_bool_pname(fFalse))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f221])).
% 215.71/27.72 fof(f1090,plain,(
% 215.71/27.72 ![A,B]: (~A=B|(hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,A),B))&hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,B),A))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f247])).
% 215.71/27.72 fof(f1091,plain,(
% 215.71/27.72 ![X0,X1]: (~X0=X1|hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,X0),X1)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f1090])).
% 215.71/27.72 fof(f1206,plain,(
% 215.71/27.72 ![X0,X1]: (~insert_pname(X0,X1)=bot_bo844097828e_bool)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f283])).
% 215.71/27.72 fof(f1207,plain,(
% 215.71/27.72 ![X0,X1]: (~insert1415133716_state(X0,X1)=bot_bo620288102e_bool)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f284])).
% 215.71/27.72 fof(f1239,plain,(
% 215.71/27.72 ![X0]: (image_2003357581_state(X0,bot_bo844097828e_bool)=bot_bo620288102e_bool)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f294])).
% 215.71/27.72 fof(f1279,plain,(
% 215.71/27.72 ![P_1]: (~is_fun_pname_bool(P_1)|collect_pname(P_1)=P_1)),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f308])).
% 215.71/27.72 fof(f1280,plain,(
% 215.71/27.72 ![X0]: (~is_fun_pname_bool(X0)|collect_pname(X0)=X0)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f1279])).
% 215.71/27.72 fof(f1281,plain,(
% 215.71/27.72 ![X0]: (collec307967673_state(X0)=X0)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f309])).
% 215.71/27.72 fof(f1282,plain,(
% 215.71/27.72 ![P_1]: (~is_fun1661590463l_bool(P_1)|collec1974731493e_bool(P_1)=P_1)),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f310])).
% 215.71/27.72 fof(f1283,plain,(
% 215.71/27.72 ![X0]: (~is_fun1661590463l_bool(X0)|collec1974731493e_bool(X0)=X0)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f1282])).
% 215.71/27.72 fof(f1284,plain,(
% 215.71/27.72 ![X0]: (collec1823980261e_bool(X0)=X0)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f311])).
% 215.71/27.72 fof(f1367,plain,(
% 215.71/27.72 ![X0]: (collec307967673_state(hAPP_H1049623551e_bool(fequal1111551311_state,X0))=insert1415133716_state(X0,bot_bo620288102e_bool))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f338])).
% 215.71/27.72 fof(f1376,plain,(
% 215.71/27.72 ![Pn,B_2]: (~hBOOL(wT_bodies)|(~hAPP_p799580910on_com(body,Pn)=some_com(B_2)|hBOOL(wt(B_2))))),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f342])).
% 215.71/27.72 fof(f1377,plain,(
% 215.71/27.72 ~hBOOL(wT_bodies)|(![B_2]: ((![Pn]: ~hAPP_p799580910on_com(body,Pn)=some_com(B_2))|hBOOL(wt(B_2))))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f1376])).
% 215.71/27.72 fof(f1378,plain,(
% 215.71/27.72 ![X0,X1]: (~hBOOL(wT_bodies)|~hAPP_p799580910on_com(body,X0)=some_com(X1)|hBOOL(wt(X1)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f1377])).
% 215.71/27.72 fof(f1439,plain,(
% 215.71/27.72 hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f352])).
% 215.71/27.72 fof(f1457,plain,(
% 215.71/27.72 ~hBOOL(fFalse)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f362])).
% 215.71/27.72 fof(f1512,plain,(
% 215.71/27.72 ![P,Q]: (~is_bool(P)|hAPP_f971112728l_bool(cOMBK_129401207e_bool(P),Q)=P)),
% 215.71/27.72 inference(pre_NNF_transformation,[status(thm)],[f397])).
% 215.71/27.72 fof(f1513,plain,(
% 215.71/27.72 ![P]: (~is_bool(P)|(![Q]: hAPP_f971112728l_bool(cOMBK_129401207e_bool(P),Q)=P))),
% 215.71/27.72 inference(miniscoping,[status(thm)],[f1512])).
% 215.71/27.72 fof(f1514,plain,(
% 215.71/27.72 ![X0,X1]: (~is_bool(X0)|hAPP_f971112728l_bool(cOMBK_129401207e_bool(X0),X1)=X0)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f1513])).
% 215.71/27.72 fof(f1544,plain,(
% 215.71/27.72 hBOOL(hoare_165779456gleton)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f421])).
% 215.71/27.72 fof(f1545,plain,(
% 215.71/27.72 hBOOL(wT_bodies)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f422])).
% 215.71/27.72 fof(f1549,plain,(
% 215.71/27.72 hAPP_p799580910on_com(body,pn)=some_com(y)),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f426])).
% 215.71/27.72 fof(f1551,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))),
% 215.71/27.72 inference(cnf_transformation,[status(thm)],[f429])).
% 215.71/27.72 fof(f1552,definition,(
% 215.71/27.72 sQ0_spl <=> (hBOOL(hoare_165779456gleton))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f1554,plain,(
% 215.71/27.72 ~hBOOL(hoare_165779456gleton)|sQ0_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f1552])).
% 215.71/27.72 fof(f1555,definition,(
% 215.71/27.72 sQ1_spl <=> (hBOOL(wT_bodies))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f1557,plain,(
% 215.71/27.72 ~hBOOL(wT_bodies)|sQ1_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f1555])).
% 215.71/27.72 fof(f1558,definition,(
% 215.71/27.72 ![X0]: (sQ2_spl <=> (~hBOOL(wt(X0))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,X0),bot_bo620288102e_bool)))))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f1559,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(wt(X0))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,X0),bot_bo620288102e_bool)))|~sQ2_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f1558])).
% 215.71/27.72 fof(f1561,plain,(
% 215.71/27.72 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 215.71/27.72 inference(split_clause,[status(thm)],[f813,f1552,f1555,f1558])).
% 215.71/27.72 fof(f1574,definition,(
% 215.71/27.72 ![X0,X1]: (sQ6_spl <=> (~hAPP_p799580910on_com(body,X0)=some_com(X1)|hBOOL(wt(X1))))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f1575,plain,(
% 215.71/27.72 ![X0,X1]: (~hAPP_p799580910on_com(body,X0)=some_com(X1)|hBOOL(wt(X1))|~sQ6_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f1574])).
% 215.71/27.72 fof(f1577,plain,(
% 215.71/27.72 ~sQ1_spl|sQ6_spl),
% 215.71/27.72 inference(split_clause,[status(thm)],[f1378,f1555,f1574])).
% 215.71/27.72 fof(f1590,plain,(
% 215.71/27.72 ![X0,X1]: (hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,X0),insert1325755072e_bool(X0,X1))))),
% 215.71/27.72 inference(destructive_equality_resolution,[status(thm)],[f823])).
% 215.71/27.72 fof(f1591,plain,(
% 215.71/27.72 ![X0,X1]: (hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,X0),insert1556680138e_bool(X0,X1))))),
% 215.71/27.72 inference(destructive_equality_resolution,[status(thm)],[f826])).
% 215.71/27.72 fof(f1624,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f971112728l_bool(hAPP_f72706945l_bool(ord_le1285840794e_bool,X0),X0)))),
% 215.71/27.72 inference(destructive_equality_resolution,[status(thm)],[f1091])).
% 215.71/27.72 fof(f1685,plain,(
% 215.71/27.72 $false|sQ0_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f1554,f1544])).
% 215.71/27.72 fof(f1686,plain,(
% 215.71/27.72 sQ0_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f1685])).
% 215.71/27.72 fof(f1688,plain,(
% 215.71/27.72 $false|sQ1_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f1557,f1545])).
% 215.71/27.72 fof(f1689,plain,(
% 215.71/27.72 sQ1_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f1688])).
% 215.71/27.72 fof(f1694,plain,(
% 215.71/27.72 is_fun_pname_bool(cOMBK_bool_pname(fFalse))),
% 215.71/27.72 inference(resolution,[status(thm)],[f437,f479])).
% 215.71/27.72 fof(f1766,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))|~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))),X0)))),
% 215.71/27.72 inference(resolution,[status(thm)],[f534,f1551])).
% 215.71/27.72 fof(f1806,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))),
% 215.71/27.72 inference(resolution,[status(thm)],[f1766,f523])).
% 215.71/27.72 fof(f1872,plain,(
% 215.71/27.72 collect_pname(cOMBK_bool_pname(fFalse))=cOMBK_bool_pname(fFalse)),
% 215.71/27.72 inference(resolution,[status(thm)],[f1280,f1694])).
% 215.71/27.72 fof(f1967,definition,(
% 215.71/27.72 sQ10_spl <=> (hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,bot_bo844097828e_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f1969,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,bot_bo844097828e_bool))|sQ10_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f1967])).
% 215.71/27.72 fof(f1991,plain,(
% 215.71/27.72 collec1974731493e_bool(bot_bo1649642514l_bool)=bot_bo1649642514l_bool),
% 215.71/27.72 inference(resolution,[status(thm)],[f1283,f456])).
% 215.71/27.72 fof(f2192,plain,(
% 215.71/27.72 $false|sQ10_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f634,f1969])).
% 215.71/27.72 fof(f2193,plain,(
% 215.71/27.72 sQ10_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f2192])).
% 215.71/27.72 fof(f2194,plain,(
% 215.71/27.72 bot_bo535777328l_bool=cOMBK_129401207e_bool(fFalse)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f1284,f1026])).
% 215.71/27.72 fof(f3423,definition,(
% 215.71/27.72 sQ22_spl <=> (wT_bodies=fFalse)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f3424,plain,(
% 215.71/27.72 wT_bodies=fFalse|~sQ22_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f3423])).
% 215.71/27.72 fof(f3559,plain,(
% 215.71/27.72 hBOOL(fFalse)|~sQ22_spl),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f3424,f1545])).
% 215.71/27.72 fof(f3560,plain,(
% 215.71/27.72 $false|~sQ22_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f3559,f1457])).
% 215.71/27.72 fof(f3561,plain,(
% 215.71/27.72 ~sQ22_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f3560])).
% 215.71/27.72 fof(f5741,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(X0,bot_bo1649642514l_bool))))),
% 215.71/27.72 inference(resolution,[status(thm)],[f633,f639])).
% 215.71/27.72 fof(f5995,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),X0)))),
% 215.71/27.72 inference(resolution,[status(thm)],[f1624,f525])).
% 215.71/27.72 fof(f6116,definition,(
% 215.71/27.72 sQ29_spl <=> (hBOOL(hAPP_f468958928l_bool(finite796539827l_bool,bot_bo1761158942l_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f6118,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f468958928l_bool(finite796539827l_bool,bot_bo1761158942l_bool))|sQ29_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f6116])).
% 215.71/27.72 fof(f6123,plain,(
% 215.71/27.72 $false|sQ29_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f6118,f637])).
% 215.71/27.72 fof(f6124,plain,(
% 215.71/27.72 sQ29_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f6123])).
% 215.71/27.72 fof(f6439,definition,(
% 215.71/27.72 sQ32_spl <=> (hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,bot_bo1649642514l_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f6441,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,bot_bo1649642514l_bool))|sQ32_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f6439])).
% 215.71/27.72 fof(f6457,plain,(
% 215.71/27.72 $false|sQ32_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f6441,f639])).
% 215.71/27.72 fof(f6458,plain,(
% 215.71/27.72 sQ32_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f6457])).
% 215.71/27.72 fof(f6782,plain,(
% 215.71/27.72 ![X0]: (hAPP_f971112728l_bool(cOMBK_129401207e_bool(fFalse),X0)=fFalse)),
% 215.71/27.72 inference(resolution,[status(thm)],[f1514,f479])).
% 215.71/27.72 fof(f6822,plain,(
% 215.71/27.72 ![X0]: (hAPP_f971112728l_bool(bot_bo535777328l_bool,X0)=fFalse)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f2194,f6782])).
% 215.71/27.72 fof(f7031,definition,(
% 215.71/27.72 sQ44_spl <=> (cOMBK_bool_pname(fFalse)=bot_bo844097828e_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f7033,plain,(
% 215.71/27.72 ~cOMBK_bool_pname(fFalse)=bot_bo844097828e_bool|sQ44_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f7031])).
% 215.71/27.72 fof(f7045,definition,(
% 215.71/27.72 ![X0]: (sQ48_spl <=> (image_2003357581_state(cOMBK_367030522_pname(X0),bot_bo844097828e_bool)=insert1415133716_state(X0,bot_bo620288102e_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f7046,plain,(
% 215.71/27.72 ![X0]: (image_2003357581_state(cOMBK_367030522_pname(X0),bot_bo844097828e_bool)=insert1415133716_state(X0,bot_bo620288102e_bool)|~sQ48_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f7045])).
% 215.71/27.72 fof(f7304,definition,(
% 215.71/27.72 ![X0]: (sQ53_spl <=> (bot_bo844097828e_bool=insert_pname(X0,bot_bo844097828e_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f7305,plain,(
% 215.71/27.72 ![X0]: (bot_bo844097828e_bool=insert_pname(X0,bot_bo844097828e_bool)|~sQ53_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f7304])).
% 215.71/27.72 fof(f7312,definition,(
% 215.71/27.72 ![X2]: (sQ55_spl <=> (X2=bot_bo620288102e_bool))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f7313,plain,(
% 215.71/27.72 ![X0]: (X0=bot_bo620288102e_bool|~sQ55_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f7312])).
% 215.71/27.72 fof(f7348,plain,(
% 215.71/27.72 $false|~sQ53_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f7305,f1206])).
% 215.71/27.72 fof(f7349,plain,(
% 215.71/27.72 ~sQ53_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f7348])).
% 215.71/27.72 fof(f7404,definition,(
% 215.71/27.72 ![X0]: (sQ74_spl <=> (bot_bo535777328l_bool=insert1556680138e_bool(X0,bot_bo535777328l_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f7405,plain,(
% 215.71/27.72 ![X0]: (bot_bo535777328l_bool=insert1556680138e_bool(X0,bot_bo535777328l_bool)|~sQ74_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f7404])).
% 215.71/27.72 fof(f7500,plain,(
% 215.71/27.72 $false|~sQ55_spl),
% 215.71/27.72 inference(backward_subsumption_resolution,[status(thm)],[f1207,f7313])).
% 215.71/27.72 fof(f7618,plain,(
% 215.71/27.72 ~sQ55_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f7500])).
% 215.71/27.72 fof(f8617,definition,(
% 215.71/27.72 sQ87_spl <=> (insert1325755072e_bool(bot_bo844097828e_bool,cOMBK_1857069011e_bool(fFalse))=bot_bo1649642514l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f8618,plain,(
% 215.71/27.72 insert1325755072e_bool(bot_bo844097828e_bool,cOMBK_1857069011e_bool(fFalse))=bot_bo1649642514l_bool|~sQ87_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f8617])).
% 215.71/27.72 fof(f8624,definition,(
% 215.71/27.72 sQ89_spl <=> (insert1325755072e_bool(bot_bo844097828e_bool,cOMBK_1857069011e_bool(fTrue))=bot_bo1649642514l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f8625,plain,(
% 215.71/27.72 insert1325755072e_bool(bot_bo844097828e_bool,cOMBK_1857069011e_bool(fTrue))=bot_bo1649642514l_bool|~sQ89_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f8624])).
% 215.71/27.72 fof(f8631,definition,(
% 215.71/27.72 sQ91_spl <=> (insert1325755072e_bool(bot_bo844097828e_bool,finite_finite_pname)=bot_bo1649642514l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f8632,plain,(
% 215.71/27.72 insert1325755072e_bool(bot_bo844097828e_bool,finite_finite_pname)=bot_bo1649642514l_bool|~sQ91_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f8631])).
% 215.71/27.72 fof(f9434,definition,(
% 215.71/27.72 ![X0]: (sQ126_spl <=> (dom_pname_com(X0)=bot_bo844097828e_bool))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f9435,plain,(
% 215.71/27.72 ![X0]: (dom_pname_com(X0)=bot_bo844097828e_bool|~sQ126_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f9434])).
% 215.71/27.72 fof(f9453,plain,(
% 215.71/27.72 ![X0]: (bot_bo620288102e_bool=insert1415133716_state(X0,bot_bo620288102e_bool)|~sQ48_spl)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f1239,f7046])).
% 215.71/27.72 fof(f9454,plain,(
% 215.71/27.72 $false|~sQ48_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f9453,f1207])).
% 215.71/27.72 fof(f9455,plain,(
% 215.71/27.72 ~sQ48_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f9454])).
% 215.71/27.72 fof(f9613,definition,(
% 215.71/27.72 ![X0]: (sQ127_spl <=> (insert1415133716_state(X0,bot_bo620288102e_bool)=bot_bo620288102e_bool))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f9614,plain,(
% 215.71/27.72 ![X0]: (insert1415133716_state(X0,bot_bo620288102e_bool)=bot_bo620288102e_bool|~sQ127_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f9613])).
% 215.71/27.72 fof(f9902,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~hAPP_p799580910on_com(X0,X1)=some_com(X2)|insert_pname(X1,bot_bo844097828e_bool)=dom_pname_com(X0)|~sQ126_spl)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f9435,f737])).
% 215.71/27.72 fof(f9903,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~hAPP_p799580910on_com(X0,X1)=some_com(X2)|insert_pname(X1,bot_bo844097828e_bool)=bot_bo844097828e_bool|~sQ126_spl)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f9435,f9902])).
% 215.71/27.72 fof(f9904,plain,(
% 215.71/27.72 ![X0,X1,X2]: (~hAPP_p799580910on_com(X0,X1)=some_com(X2)|~sQ126_spl)),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f9903,f1206])).
% 215.71/27.72 fof(f10110,definition,(
% 215.71/27.72 sQ131_spl <=> (hBOOL(hAPP_f166538662l_bool(finite464017571e_bool,bot_bo535777328l_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f10112,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f166538662l_bool(finite464017571e_bool,bot_bo535777328l_bool))|sQ131_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f10110])).
% 215.71/27.72 fof(f10124,plain,(
% 215.71/27.72 $false|sQ131_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f10112,f638])).
% 215.71/27.72 fof(f10125,plain,(
% 215.71/27.72 sQ131_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f10124])).
% 215.71/27.72 fof(f10414,plain,(
% 215.71/27.72 $false|~sQ126_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f1549,f9904])).
% 215.71/27.72 fof(f10415,plain,(
% 215.71/27.72 ~sQ126_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f10414])).
% 215.71/27.72 fof(f10544,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f971112728l_bool(finite364844667_state,image_2003357581_state(X0,dom_pname_com(body)))))),
% 215.71/27.72 inference(resolution,[status(thm)],[f1439,f557])).
% 215.71/27.72 fof(f10875,plain,(
% 215.71/27.72 bot_bo844097828e_bool=cOMBK_bool_pname(fFalse)),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f1029,f1872])).
% 215.71/27.72 fof(f10876,plain,(
% 215.71/27.72 $false|sQ44_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f10875,f7033])).
% 215.71/27.72 fof(f10877,plain,(
% 215.71/27.72 sQ44_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f10876])).
% 215.71/27.72 fof(f11262,definition,(
% 215.71/27.72 sQ145_spl <=> (is_fun1661590463l_bool(bot_bo1649642514l_bool))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f11264,plain,(
% 215.71/27.72 ~is_fun1661590463l_bool(bot_bo1649642514l_bool)|sQ145_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f11262])).
% 215.71/27.72 fof(f12630,plain,(
% 215.71/27.72 hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,bot_bo844097828e_bool),bot_bo1649642514l_bool))|~sQ89_spl),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f8625,f1590])).
% 215.71/27.72 fof(f12632,plain,(
% 215.71/27.72 hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,bot_bo844097828e_bool),bot_bo1649642514l_bool))|~sQ91_spl),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f8632,f1590])).
% 215.71/27.72 fof(f12633,plain,(
% 215.71/27.72 $false|~sQ89_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f12630,f815])).
% 215.71/27.72 fof(f12634,plain,(
% 215.71/27.72 ~sQ89_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f12633])).
% 215.71/27.72 fof(f12637,plain,(
% 215.71/27.72 $false|~sQ91_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f12632,f815])).
% 215.71/27.72 fof(f12638,plain,(
% 215.71/27.72 ~sQ91_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f12637])).
% 215.71/27.72 fof(f12707,definition,(
% 215.71/27.72 sQ147_spl <=> (collec1974731493e_bool(cOMBK_1857069011e_bool(fFalse))=bot_bo1649642514l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f12709,plain,(
% 215.71/27.72 ~collec1974731493e_bool(cOMBK_1857069011e_bool(fFalse))=bot_bo1649642514l_bool|sQ147_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f12707])).
% 215.71/27.72 fof(f13080,plain,(
% 215.71/27.72 hBOOL(hAPP_f1935102916l_bool(hAPP_f556039215l_bool(member799430823e_bool,bot_bo844097828e_bool),bot_bo1649642514l_bool))|~sQ87_spl),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f8618,f1590])).
% 215.71/27.72 fof(f13085,plain,(
% 215.71/27.72 $false|~sQ87_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f13080,f815])).
% 215.71/27.72 fof(f13086,plain,(
% 215.71/27.72 ~sQ87_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f13085])).
% 215.71/27.72 fof(f13316,plain,(
% 215.71/27.72 $false|~sQ127_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f9614,f1207])).
% 215.71/27.72 fof(f13317,plain,(
% 215.71/27.72 ~sQ127_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f13316])).
% 215.71/27.72 fof(f13327,plain,(
% 215.71/27.72 $false|sQ145_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f11264,f456])).
% 215.71/27.72 fof(f13328,plain,(
% 215.71/27.72 sQ145_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f13327])).
% 215.71/27.72 fof(f15900,definition,(
% 215.71/27.72 sQ202_spl <=> (finite364844667_state=bot_bo535777328l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f15901,plain,(
% 215.71/27.72 finite364844667_state=bot_bo535777328l_bool|~sQ202_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f15900])).
% 215.71/27.72 fof(f15935,definition,(
% 215.71/27.72 sQ211_spl <=> (hoare_1598289066_state(fa)=bot_bo535777328l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f15936,plain,(
% 215.71/27.72 hoare_1598289066_state(fa)=bot_bo535777328l_bool|~sQ211_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f15935])).
% 215.71/27.72 fof(f15942,definition,(
% 215.71/27.72 sQ213_spl <=> (hoare_1598289066_state(bot_bo620288102e_bool)=bot_bo535777328l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f15943,plain,(
% 215.71/27.72 hoare_1598289066_state(bot_bo620288102e_bool)=bot_bo535777328l_bool|~sQ213_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f15942])).
% 215.71/27.72 fof(f15959,definition,(
% 215.71/27.72 sQ216_spl <=> (hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body)))=bot_bo535777328l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f15960,plain,(
% 215.71/27.72 hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body)))=bot_bo535777328l_bool|~sQ216_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f15959])).
% 215.71/27.72 fof(f16000,plain,(
% 215.71/27.72 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))))|~sQ216_spl),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f15960,f5995])).
% 215.71/27.72 fof(f16204,plain,(
% 215.71/27.72 hBOOL(fFalse)|~sQ216_spl),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f6822,f16000])).
% 215.71/27.72 fof(f16205,plain,(
% 215.71/27.72 $false|~sQ216_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16204,f1457])).
% 215.71/27.72 fof(f16206,plain,(
% 215.71/27.72 ~sQ216_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16205])).
% 215.71/27.72 fof(f16310,plain,(
% 215.71/27.72 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,bot_bo620288102e_bool))|~sQ213_spl),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f15943,f5995])).
% 215.71/27.72 fof(f16431,definition,(
% 215.71/27.72 sQ247_spl <=> (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(fa),bot_bo620288102e_bool)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f16433,plain,(
% 215.71/27.72 ~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(fa),bot_bo620288102e_bool))|sQ247_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f16431])).
% 215.71/27.72 fof(f16439,definition,(
% 215.71/27.72 ![X0]: (sQ248_spl <=> (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(fa),X0))|~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),bot_bo620288102e_bool))))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f16440,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(fa),X0))|~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(X0),bot_bo620288102e_bool))|~sQ248_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f16439])).
% 215.71/27.72 fof(f16465,plain,(
% 215.71/27.72 hBOOL(fFalse)|~sQ213_spl),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f6822,f16310])).
% 215.71/27.72 fof(f16466,plain,(
% 215.71/27.72 $false|~sQ213_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16465,f1457])).
% 215.71/27.72 fof(f16467,plain,(
% 215.71/27.72 ~sQ213_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16466])).
% 215.71/27.72 fof(f16468,plain,(
% 215.71/27.72 $false|sQ247_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16433,f523])).
% 215.71/27.72 fof(f16469,plain,(
% 215.71/27.72 sQ247_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16468])).
% 215.71/27.72 fof(f16470,plain,(
% 215.71/27.72 ![X0]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(fa),X0))|~sQ248_spl)),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16440,f523])).
% 215.71/27.72 fof(f16526,plain,(
% 215.71/27.72 $false|~sQ248_spl),
% 215.71/27.72 inference(resolution,[status(thm)],[f16470,f523])).
% 215.71/27.72 fof(f16530,plain,(
% 215.71/27.72 ~sQ248_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16526])).
% 215.71/27.72 fof(f16550,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,image_2003357581_state(X0,dom_pname_com(body))))|~sQ202_spl)),
% 215.71/27.72 inference(backward_demodulation,[status(thm)],[f15901,f10544])).
% 215.71/27.72 fof(f16577,plain,(
% 215.71/27.72 hBOOL(fFalse)|~sQ202_spl),
% 215.71/27.72 inference(forward_demodulation,[status(thm)],[f6822,f16550])).
% 215.71/27.72 fof(f16578,plain,(
% 215.71/27.72 $false|~sQ202_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16577,f1457])).
% 215.71/27.72 fof(f16579,plain,(
% 215.71/27.72 ~sQ202_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16578])).
% 215.71/27.72 fof(f16582,plain,(
% 215.71/27.72 ![X0]: (hBOOL(hAPP_f166538662l_bool(hAPP_f210337421l_bool(member2114907555e_bool,X0),bot_bo535777328l_bool))|~sQ74_spl)),
% 215.71/27.72 inference(paramodulation,[status(thm)],[f7405,f1591])).
% 215.71/27.72 fof(f16583,plain,(
% 215.71/27.72 $false|~sQ74_spl),
% 215.71/27.72 inference(forward_subsumption_resolution,[status(thm)],[f16582,f816])).
% 215.71/27.72 fof(f16584,plain,(
% 215.71/27.72 ~sQ74_spl),
% 215.71/27.72 inference(contradiction_clause,[status(thm)],[f16583])).
% 215.71/27.72 fof(f16617,definition,(
% 215.71/27.72 sQ253_spl <=> (is_fun_pname_bool(dom_pname_com(body)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f16619,plain,(
% 215.71/27.72 ~is_fun_pname_bool(dom_pname_com(body))|sQ253_spl),
% 215.71/27.72 inference(component_clause,[status(thm)],[f16617])).
% 215.71/27.72 fof(f16624,definition,(
% 215.71/27.72 ![X0]: (sQ255_spl <=> (~is_fun_pname_bool(X0)))),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f16625,plain,(
% 215.71/27.72 ![X0]: (~is_fun_pname_bool(X0)|~sQ255_spl)),
% 215.71/27.72 inference(component_clause,[status(thm)],[f16624])).
% 215.71/27.72 fof(f16628,definition,(
% 215.71/27.72 sQ256_spl <=> (collec1974731493e_bool(bot_bo1649642514l_bool)=bot_bo1649642514l_bool)),
% 215.71/27.72 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 215.71/27.72 fof(f16630,plain,(
% 215.71/27.72 ~collec1974731493e_bool(bot_bo1649642514l_bool)=bot_bo1649642514l_bool|sQ256_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f16628])).
% 215.71/27.73 fof(f16634,plain,(
% 215.71/27.73 ~bot_bo1649642514l_bool=bot_bo1649642514l_bool|sQ256_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f1991,f16630])).
% 215.71/27.73 fof(f16635,plain,(
% 215.71/27.73 $false|sQ256_spl),
% 215.71/27.73 inference(trivial_equality_resolution,[status(thm)],[f16634])).
% 215.71/27.73 fof(f16636,plain,(
% 215.71/27.73 sQ256_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f16635])).
% 215.71/27.73 fof(f16637,plain,(
% 215.71/27.73 $false|sQ253_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f16619,f453])).
% 215.71/27.73 fof(f16638,plain,(
% 215.71/27.73 sQ253_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f16637])).
% 215.71/27.73 fof(f16656,definition,(
% 215.71/27.73 ![X0]: (sQ257_spl <=> (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(sK2_skl(hoare_1598289066_state(fa))),X0))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f16657,plain,(
% 215.71/27.73 ![X0]: (~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(sK2_skl(hoare_1598289066_state(fa))),X0))|~sQ257_spl)),
% 215.71/27.73 inference(component_clause,[status(thm)],[f16656])).
% 215.71/27.73 fof(f16673,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,fa))|~sQ211_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f15936,f5995])).
% 215.71/27.73 fof(f16697,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ211_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f16673])).
% 215.71/27.73 fof(f16698,plain,(
% 215.71/27.73 $false|~sQ211_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f16697,f1457])).
% 215.71/27.73 fof(f16699,plain,(
% 215.71/27.73 ~sQ211_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f16698])).
% 215.71/27.73 fof(f16716,plain,(
% 215.71/27.73 $false|~sQ255_spl),
% 215.71/27.73 inference(backward_subsumption_resolution,[status(thm)],[f453,f16625])).
% 215.71/27.73 fof(f16877,plain,(
% 215.71/27.73 ~sQ255_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f16716])).
% 215.71/27.73 fof(f16909,plain,(
% 215.71/27.73 $false|~sQ257_spl),
% 215.71/27.73 inference(resolution,[status(thm)],[f16657,f523])).
% 215.71/27.73 fof(f16913,plain,(
% 215.71/27.73 ~sQ257_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f16909])).
% 215.71/27.73 fof(f20086,definition,(
% 215.71/27.73 sQ312_spl <=> (bot_bo535777328l_bool=hoare_1598289066_state(sK2_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f20087,plain,(
% 215.71/27.73 bot_bo535777328l_bool=hoare_1598289066_state(sK2_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body)))))|~sQ312_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f20086])).
% 215.71/27.73 fof(f20435,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,sK2_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))))))|~sQ312_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f20087,f5995])).
% 215.71/27.73 fof(f20468,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ312_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f20435])).
% 215.71/27.73 fof(f20469,plain,(
% 215.71/27.73 $false|~sQ312_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f20468,f1457])).
% 215.71/27.73 fof(f20470,plain,(
% 215.71/27.73 ~sQ312_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f20469])).
% 215.71/27.73 fof(f20572,definition,(
% 215.71/27.73 sQ335_spl <=> (bot_bo535777328l_bool=hoare_1598289066_state(sK8_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f20573,plain,(
% 215.71/27.73 bot_bo535777328l_bool=hoare_1598289066_state(sK8_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body)))))|~sQ335_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f20572])).
% 215.71/27.73 fof(f20906,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,sK8_skl(hoare_1598289066_state(image_2003357581_state(cOMBB_699532858_pname(hoare_Mirabelle_MGT,body_1),dom_pname_com(body))))))|~sQ335_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f20573,f5995])).
% 215.71/27.73 fof(f20943,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ335_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f20906])).
% 215.71/27.73 fof(f20944,plain,(
% 215.71/27.73 $false|~sQ335_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f20943,f1457])).
% 215.71/27.73 fof(f20945,plain,(
% 215.71/27.73 ~sQ335_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f20944])).
% 215.71/27.73 fof(f22521,definition,(
% 215.71/27.73 sQ353_spl <=> (hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))=bot_bo535777328l_bool)),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f22522,plain,(
% 215.71/27.73 hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))=bot_bo535777328l_bool|~sQ353_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f22521])).
% 215.71/27.73 fof(f22562,definition,(
% 215.71/27.73 sQ358_spl <=> (insert_pname(pn,cOMBK_bool_pname(fTrue))=bot_bo844097828e_bool)),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f22563,plain,(
% 215.71/27.73 insert_pname(pn,cOMBK_bool_pname(fTrue))=bot_bo844097828e_bool|~sQ358_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f22562])).
% 215.71/27.73 fof(f22578,plain,(
% 215.71/27.73 $false|~sQ358_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f22563,f1206])).
% 215.71/27.73 fof(f22579,plain,(
% 215.71/27.73 ~sQ358_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f22578])).
% 215.71/27.73 fof(f22719,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))|~sQ353_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f22522,f1624])).
% 215.71/27.73 fof(f22739,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ353_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f22719])).
% 215.71/27.73 fof(f22740,plain,(
% 215.71/27.73 $false|~sQ353_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f22739,f1457])).
% 215.71/27.73 fof(f22741,plain,(
% 215.71/27.73 ~sQ353_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f22740])).
% 215.71/27.73 fof(f25457,definition,(
% 215.71/27.73 sQ388_spl <=> (hAPP_f72706945l_bool(ord_le1285840794e_bool,sK2_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))))=bot_bo535777328l_bool)),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f25458,plain,(
% 215.71/27.73 hAPP_f72706945l_bool(ord_le1285840794e_bool,sK2_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))))=bot_bo535777328l_bool|~sQ388_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f25457])).
% 215.71/27.73 fof(f25533,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,sK2_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))))|~sQ388_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f25458,f1624])).
% 215.71/27.73 fof(f25558,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ388_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f25533])).
% 215.71/27.73 fof(f25559,plain,(
% 215.71/27.73 $false|~sQ388_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f25558,f1457])).
% 215.71/27.73 fof(f25560,plain,(
% 215.71/27.73 ~sQ388_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f25559])).
% 215.71/27.73 fof(f26310,definition,(
% 215.71/27.73 sQ440_spl <=> (insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)=bot_bo620288102e_bool)),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f26311,plain,(
% 215.71/27.73 insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)=bot_bo620288102e_bool|~sQ440_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f26310])).
% 215.71/27.73 fof(f26339,plain,(
% 215.71/27.73 $false|~sQ440_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f26311,f1207])).
% 215.71/27.73 fof(f26340,plain,(
% 215.71/27.73 ~sQ440_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f26339])).
% 215.71/27.73 fof(f27795,definition,(
% 215.71/27.73 sQ465_spl <=> (bot_bo535777328l_bool=hAPP_f72706945l_bool(ord_le1285840794e_bool,sK8_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ465_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f27796,plain,(
% 215.71/27.73 bot_bo535777328l_bool=hAPP_f72706945l_bool(ord_le1285840794e_bool,sK8_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool))))|~sQ465_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f27795])).
% 215.71/27.73 fof(f27813,plain,(
% 215.71/27.73 hBOOL(hAPP_f971112728l_bool(bot_bo535777328l_bool,sK8_skl(hAPP_f72706945l_bool(ord_le1285840794e_bool,insert1415133716_state(hAPP_c1126217667_state(hoare_Mirabelle_MGT,y),bot_bo620288102e_bool)))))|~sQ465_spl),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f27796,f1624])).
% 215.71/27.73 fof(f27843,plain,(
% 215.71/27.73 hBOOL(fFalse)|~sQ465_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f6822,f27813])).
% 215.71/27.73 fof(f27844,plain,(
% 215.71/27.73 $false|~sQ465_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f27843,f1457])).
% 215.71/27.73 fof(f27845,plain,(
% 215.71/27.73 ~sQ465_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f27844])).
% 215.71/27.73 fof(f30766,definition,(
% 215.71/27.73 ![X0]: (sQ513_spl <=> (hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ513_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f30767,plain,(
% 215.71/27.73 ![X0]: (hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool))|~sQ513_spl)),
% 215.71/27.73 inference(component_clause,[status(thm)],[f30766])).
% 215.71/27.73 fof(f31055,definition,(
% 215.71/27.73 ![X0]: (sQ520_spl <=> (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X0),bot_bo620288102e_bool))))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f31056,plain,(
% 215.71/27.73 ![X0]: (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X0),bot_bo620288102e_bool))|~sQ520_spl)),
% 215.71/27.73 inference(component_clause,[status(thm)],[f31055])).
% 215.71/27.73 fof(f31523,plain,(
% 215.71/27.73 $false|~sQ513_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f30767,f817])).
% 215.71/27.73 fof(f31524,plain,(
% 215.71/27.73 ~sQ513_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f31523])).
% 215.71/27.73 fof(f31727,plain,(
% 215.71/27.73 $false|~sQ520_spl),
% 215.71/27.73 inference(forward_subsumption_resolution,[status(thm)],[f31056,f814])).
% 215.71/27.73 fof(f31728,plain,(
% 215.71/27.73 ~sQ520_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f31727])).
% 215.71/27.73 fof(f33550,definition,(
% 215.71/27.73 ![X0]: (sQ539_spl <=> (~some_com(y)=some_com(X0)))),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ539_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f33551,plain,(
% 215.71/27.73 ![X0]: (~some_com(y)=some_com(X0)|~sQ539_spl)),
% 215.71/27.73 inference(component_clause,[status(thm)],[f33550])).
% 215.71/27.73 fof(f33634,plain,(
% 215.71/27.73 $false|~sQ539_spl),
% 215.71/27.73 inference(equality_resolution,[status(thm)],[f33551])).
% 215.71/27.73 fof(f33635,plain,(
% 215.71/27.73 ~sQ539_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f33634])).
% 215.71/27.73 fof(f34743,plain,(
% 215.71/27.73 ~bot_bo1649642514l_bool=bot_bo1649642514l_bool|sQ147_spl),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f1027,f12709])).
% 215.71/27.73 fof(f34744,plain,(
% 215.71/27.73 $false|sQ147_spl),
% 215.71/27.73 inference(trivial_equality_resolution,[status(thm)],[f34743])).
% 215.71/27.73 fof(f34745,plain,(
% 215.71/27.73 sQ147_spl),
% 215.71/27.73 inference(contradiction_clause,[status(thm)],[f34744])).
% 215.71/27.73 fof(f35598,plain,(
% 215.71/27.73 ~hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),hAPP_H1049623551e_bool(fequal1111551311_state,hAPP_c1126217667_state(hoare_Mirabelle_MGT,y))))),
% 215.71/27.73 inference(backward_demodulation,[status(thm)],[f35658,f1806])).
% 215.71/27.73 fof(f35658,plain,(
% 215.71/27.73 ![X0]: (hAPP_H1049623551e_bool(fequal1111551311_state,X0)=insert1415133716_state(X0,bot_bo620288102e_bool))),
% 215.71/27.73 inference(forward_demodulation,[status(thm)],[f1281,f1367])).
% 215.71/27.73 fof(f35693,plain,(
% 215.71/27.73 ![X0]: (~hAPP_H1049623551e_bool(fequal1111551311_state,X0)=bot_bo620288102e_bool)),
% 215.71/27.73 inference(paramodulation,[status(thm)],[f35658,f1207])).
% 215.71/27.73 fof(f35848,definition,(
% 215.71/27.73 sQ607_spl <=> (hAPP_H1049623551e_bool(fequal1111551311_state,hAPP_c1126217667_state(hoare_Mirabelle_MGT,y))=bot_bo620288102e_bool)),
% 215.71/27.73 introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition])).
% 215.71/27.73 fof(f35849,plain,(
% 215.71/27.73 hAPP_H1049623551e_bool(fequal1111551311_state,hAPP_c1126217667_state(hoare_Mirabelle_MGT,y))=bot_bo620288102e_bool|~sQ607_spl),
% 215.71/27.73 inference(component_clause,[status(thm)],[f35848])).
% 215.71/27.73 fof(f35861,plain,(
% 80.95/27.83 $false|~sQ607_spl),
% 80.95/27.83 inference(forward_subsumption_resolution,[status(thm)],[f35849,f35693])).
% 80.95/27.83 fof(f35862,plain,(
% 80.95/27.83 ~sQ607_spl),
% 80.95/27.83 inference(contradiction_clause,[status(thm)],[f35861])).
% 80.95/27.83 fof(f36340,definition,(
% 80.95/27.83 sQ628_spl <=> (hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(dom_pname_com(body),bot_bo1649642514l_bool))))),
% 80.95/27.83 introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition])).
% 80.95/27.83 fof(f36342,plain,(
% 80.95/27.83 ~hBOOL(hAPP_f1935102916l_bool(finite595471783e_bool,insert1325755072e_bool(dom_pname_com(body),bot_bo1649642514l_bool)))|sQ628_spl),
% 80.95/27.83 inference(component_clause,[status(thm)],[f36340])).
% 80.95/27.83 fof(f41311,plain,(
% 80.95/27.83 $false|sQ628_spl),
% 80.95/27.83 inference(forward_subsumption_resolution,[status(thm)],[f36342,f5741])).
% 80.95/27.83 fof(f41312,plain,(
% 80.95/27.83 sQ628_spl),
% 80.95/27.83 inference(contradiction_clause,[status(thm)],[f41311])).
% 80.95/27.83 fof(f52664,definition,(
% 80.95/27.83 sQ1345_spl <=> (hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body))))),
% 80.95/27.83 introduced(definition,[new_symbols(definition,[sQ1345_spl])],[split_symbol_definition])).
% 80.95/27.83 fof(f52666,plain,(
% 80.95/27.83 ~hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body)))|sQ1345_spl),
% 80.95/27.83 inference(component_clause,[status(thm)],[f52664])).
% 80.95/27.83 fof(f52700,plain,(
% 80.95/27.83 $false|sQ1345_spl),
% 80.95/27.83 inference(forward_subsumption_resolution,[status(thm)],[f52666,f1439])).
% 80.95/27.83 fof(f52701,plain,(
% 80.95/27.83 sQ1345_spl),
% 80.95/27.83 inference(contradiction_clause,[status(thm)],[f52700])).
% 80.95/27.83 fof(f53236,plain,(
% 80.95/27.83 ![X0]: (~hBOOL(wt(X0))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),hAPP_H1049623551e_bool(fequal1111551311_state,hAPP_c1126217667_state(hoare_Mirabelle_MGT,X0))))|~sQ2_spl)),
% 80.95/27.83 inference(forward_demodulation,[status(thm)],[f35658,f1559])).
% 80.95/27.83 fof(f54505,plain,(
% 80.95/27.83 hBOOL(wt(y))|~sQ6_spl),
% 80.95/27.83 inference(resolution,[status(thm)],[f1575,f1549])).
% 80.95/27.83 fof(f54734,plain,(
% 80.95/27.83 hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),hAPP_H1049623551e_bool(fequal1111551311_state,hAPP_c1126217667_state(hoare_Mirabelle_MGT,y))))|~sQ6_spl|~sQ2_spl),
% 80.95/27.83 inference(resolution,[status(thm)],[f54505,f53236])).
% 80.95/27.83 fof(f54743,plain,(
% 80.95/27.83 $false|~sQ6_spl|~sQ2_spl),
% 80.95/27.83 inference(forward_subsumption_resolution,[status(thm)],[f54734,f35598])).
% 80.95/27.83 fof(f54744,plain,(
% 80.95/27.83 ~sQ6_spl|~sQ2_spl),
% 80.95/27.83 inference(contradiction_clause,[status(thm)],[f54743])).
% 80.95/27.83 fof(f54745,plain,(
% 80.95/27.83 $false),
% 80.95/27.83 inference(sat_refutation,[status(thm)],[f1561,f1577,f1686,f1689,f2193,f3561,f6124,f6458,f7349,f7618,f9455,f10125,f10415,f10877,f12634,f12638,f13086,f13317,f13328,f16206,f16467,f16469,f16530,f16579,f16584,f16636,f16638,f16699,f16877,f16913,f20470,f20945,f22579,f22741,f25560,f26340,f27845,f31524,f31728,f33635,f34745,f35862,f41312,f52701,f54744])).
% 80.95/27.83 % SZS output end CNFRefutation for theBenchmark.p
% 80.95/27.90 % Elapsed time: 27.520911 seconds
% 80.95/27.90 % CPU time: 217.492138 seconds
% 80.95/27.90 % Total memory used: 880.353 MB
% 80.95/27.90 % Net memory used: 834.865 MB
%------------------------------------------------------------------------------