%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:08:00 PM UTC 2026
% Result : Theorem 33.41s 4.73s
% Output : CNFRefutation 31.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 19
% Syntax : Number of formulae : 78 ( 48 unt; 0 def)
% Number of atoms : 129 ( 52 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 100 ( 49 ~; 44 |; 0 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 14 con; 0-4 aty)
% Number of variables : 107 ( 107 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,hypothesis,
ti(bool,wT_bodies) = wT_bodies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
ti(bool,hoare_1883395792gleton) = hoare_1883395792gleton,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
ti(bool,fTrue) = fTrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X_a,X_c,B_1_1,B_2_1] : hAPP(X_a,X_c,B_1_1,ti(X_a,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [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)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [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)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [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))))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [X_b,X_a,X_c,F,G_1,A_1] : hAPP(fun(X_b,bool),fun(X_a,bool),hAPP(fun(X_b,X_a),fun(fun(X_b,bool),fun(X_a,bool)),image(X_b,X_a),F),hAPP(fun(X_c,bool),fun(X_b,bool),hAPP(fun(X_c,X_b),fun(fun(X_c,bool),fun(X_b,bool)),image(X_c,X_b),G_1),A_1)) = hAPP(fun(X_c,bool),fun(X_a,bool),hAPP(fun(X_c,X_a),fun(fun(X_c,bool),fun(X_a,bool)),image(X_c,X_a),hAPP(fun(X_c,X_b),fun(X_c,X_a),hAPP(fun(X_b,X_a),fun(fun(X_c,X_b),fun(X_c,X_a)),combb(X_b,X_a,X_c),F),G_1)),A_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [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))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [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)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,axiom,
! [X_a,P] : hAPP(X_a,X_a,combi(X_a),P) = ti(X_a,P),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,axiom,
! [P] :
( ti(bool,P) = fFalse
| ti(bool,P) = fTrue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
hBOOL(hoare_1883395792gleton),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
hBOOL(wT_bodies),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,conjecture,
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))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,negated_conjecture,
~ 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))))),
inference(negated_conjecture,[status(cth)],[f169]) ).
fof(f177,plain,
ti(bool,wT_bodies) = wT_bodies,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f184,plain,
ti(bool,hoare_1883395792gleton) = hoare_1883395792gleton,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f195,plain,
ti(bool,fTrue) = fTrue,
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f201,plain,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f202,plain,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f211,plain,
! [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)))),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f220,plain,
! [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),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_2),Ts)) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f221,plain,
! [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),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_2),Ts)) ),
inference(miniscoping,[status(thm)],[f220]) ).
fof(f222,plain,
! [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),X3),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),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f259,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,C_1))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1883395792gleton) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f260,plain,
( ! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,C_1)) )
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1883395792gleton) ),
inference(miniscoping,[status(thm)],[f259]) ).
fof(f261,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1883395792gleton) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f374,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),X2),hAPP(fun(X3,bool),fun(X0,bool),hAPP(fun(X3,X0),fun(fun(X3,bool),fun(X0,bool)),image(X3,X0),X4),X5)) = hAPP(fun(X3,bool),fun(X1,bool),hAPP(fun(X3,X1),fun(fun(X3,bool),fun(X1,bool)),image(X3,X1),hAPP(fun(X3,X0),fun(X3,X1),hAPP(fun(X0,X1),fun(fun(X3,X0),fun(X3,X1)),combb(X0,X1,X3),X2),X4)),X5),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f425,plain,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = ti(fun(X0,bool),X1),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f465,plain,
! [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))),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f471,plain,
! [Pn,B_2] :
( hBOOL(hAPP(com,bool,wt,B_2))
| hAPP(pname,option(com),body,Pn) != hAPP(com,option(com),some(com),B_2)
| ~ hBOOL(wT_bodies) ),
inference(pre_NNF_transformation,[status(thm)],[f130]) ).
fof(f472,plain,
( ! [B_2] :
( hBOOL(hAPP(com,bool,wt,B_2))
| ! [Pn] : hAPP(pname,option(com),body,Pn) != hAPP(com,option(com),some(com),B_2) )
| ~ hBOOL(wT_bodies) ),
inference(miniscoping,[status(thm)],[f471]) ).
fof(f473,plain,
! [X0,X1] :
( hBOOL(hAPP(com,bool,wt,X1))
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| ~ hBOOL(wT_bodies) ),
inference(cnf_transformation,[status(thm)],[f472]) ).
fof(f514,plain,
! [X0,X1] : hAPP(X0,X0,combi(X0),X1) = ti(X0,X1),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f528,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f529,plain,
! [X0] :
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f538,plain,
hBOOL(hoare_1883395792gleton),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f539,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f543,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f545,plain,
~ 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))))),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f566,plain,
! [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),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))
| ~ 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))))) ),
inference(resolution,[status(thm)],[f222,f545]) ).
fof(f732,plain,
! [X0,X1,X2] :
( ti(bool,X2) = fFalse
| hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f529,f201]) ).
fof(f1245,plain,
! [X0,X1] :
( hoare_1883395792gleton = fFalse
| hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,hoare_1883395792gleton) ),
inference(paramodulation,[status(thm)],[f184,f732]) ).
fof(f1246,plain,
! [X0,X1] :
( wT_bodies = fFalse
| hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,wT_bodies) ),
inference(paramodulation,[status(thm)],[f177,f732]) ).
fof(f1268,plain,
! [X0,X1] :
( hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,hoare_1883395792gleton)
| hBOOL(fFalse) ),
inference(paramodulation,[status(thm)],[f1245,f538]) ).
fof(f1270,plain,
! [X0,X1] : hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,hoare_1883395792gleton),
inference(forward_subsumption_resolution,[status(thm)],[f1268,f528]) ).
fof(f1276,plain,
hAPP(bool,bool,combi(bool),fTrue) = ti(bool,hoare_1883395792gleton),
inference(paramodulation,[status(thm)],[f514,f1270]) ).
fof(f1311,plain,
ti(bool,fTrue) = ti(bool,hoare_1883395792gleton),
inference(forward_demodulation,[status(thm)],[f514,f1276]) ).
fof(f1312,plain,
fTrue = ti(bool,hoare_1883395792gleton),
inference(forward_demodulation,[status(thm)],[f195,f1311]) ).
fof(f1313,plain,
fTrue = hoare_1883395792gleton,
inference(forward_demodulation,[status(thm)],[f184,f1312]) ).
fof(f1353,plain,
hBOOL(fTrue),
inference(backward_demodulation,[status(thm)],[f1313,f538]) ).
fof(f1420,plain,
! [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),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),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))))) ),
inference(backward_demodulation,[status(thm)],[f374,f566]) ).
fof(f1487,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(fTrue) ),
inference(forward_demodulation,[status(thm)],[f1313,f261]) ).
fof(f1488,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies) ),
inference(forward_subsumption_resolution,[status(thm)],[f1487,f1353]) ).
fof(f1848,plain,
! [X0,X1] :
( hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,wT_bodies)
| ~ hBOOL(wT_bodies) ),
inference(paramodulation,[status(thm)],[f1246,f528]) ).
fof(f1850,plain,
! [X0,X1] : hAPP(bool,X0,X1,fTrue) = hAPP(bool,X0,X1,wT_bodies),
inference(forward_subsumption_resolution,[status(thm)],[f1848,f539]) ).
fof(f1860,plain,
hAPP(bool,bool,combi(bool),fTrue) = ti(bool,wT_bodies),
inference(paramodulation,[status(thm)],[f514,f1850]) ).
fof(f1924,plain,
ti(bool,fTrue) = ti(bool,wT_bodies),
inference(forward_demodulation,[status(thm)],[f514,f1860]) ).
fof(f1925,plain,
fTrue = ti(bool,wT_bodies),
inference(forward_demodulation,[status(thm)],[f195,f1924]) ).
fof(f1926,plain,
fTrue = wT_bodies,
inference(forward_demodulation,[status(thm)],[f177,f1925]) ).
fof(f2134,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(fTrue) ),
inference(backward_demodulation,[status(thm)],[f1926,f1488]) ).
fof(f2140,plain,
! [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)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2134,f1353]) ).
fof(f10012,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f425,f465]) ).
fof(f10048,plain,
! [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),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),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(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))) ),
inference(backward_demodulation,[status(thm)],[f10075,f1420]) ).
fof(f10075,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f202,f10012]) ).
fof(f10366,plain,
! [X0,X1] :
( hBOOL(hAPP(com,bool,wt,X1))
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| ~ hBOOL(fTrue) ),
inference(forward_demodulation,[status(thm)],[f1926,f473]) ).
fof(f10367,plain,
! [X0,X1] :
( hBOOL(hAPP(com,bool,wt,X1))
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f10366,f1353]) ).
fof(f17066,plain,
! [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))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(forward_demodulation,[status(thm)],[f10075,f2140]) ).
fof(f17068,plain,
( ~ 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(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),bot_bot(fun(hoare_509422987triple(state),bool))))
| ~ hBOOL(hAPP(com,bool,wt,y)) ),
inference(resolution,[status(thm)],[f17066,f10048]) ).
fof(f17082,plain,
~ hBOOL(hAPP(com,bool,wt,y)),
inference(forward_subsumption_resolution,[status(thm)],[f17068,f211]) ).
fof(f17137,plain,
! [X0] : hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),y),
inference(resolution,[status(thm)],[f17082,f10367]) ).
fof(f17142,plain,
! [X0] : hAPP(pname,option(com),body,X0) != hAPP(pname,option(com),body,pn),
inference(forward_demodulation,[status(thm)],[f543,f17137]) ).
fof(f17455,plain,
$false,
inference(resolution,[status(thm)],[f17142,f201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:01:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 33.41/4.73 % Refutation found
% 33.41/4.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 33.41/4.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.47/4.86 % Elapsed time: 4.481105 seconds
% 4.47/4.86 % CPU time: 34.745407 seconds
% 4.47/4.86 % Total memory used: 583.048 MB
% 4.47/4.86 % Net memory used: 569.338 MB
%------------------------------------------------------------------------------