%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW474+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 67.59s 9.36s
% Output : CNFRefutation 54.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 73 ( 26 unt; 0 def)
% Number of atoms : 155 ( 36 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 148 ( 66 ~; 64 |; 6 &)
% ( 2 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 15 con; 0-4 aty)
% Number of variables : 116 ( 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f60,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(f61,hypothesis,
! [B_1_1] :
( hBOOL(ti(bool,B_1_1))
<=> hBOOL(B_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X_a,G_1] : hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),bot_bot(fun(hoare_1656922687triple(X_a),bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X_a,Ts,G_1,Ts_1] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts_1))
=> ( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),ord_less_eq(fun(hoare_1656922687triple(X_a),bool)),Ts),Ts_1))
=> hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [X_a,G_1,G_2,Ts] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_2),Ts))
=> ( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),G_2))
=> hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [X_a,G_1,T_3,Ts] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),hAPP(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool),hAPP(hoare_1656922687triple(X_a),fun(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool)),insert(hoare_1656922687triple(X_a)),T_3),Ts)))
=> ( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
& hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),hAPP(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool),hAPP(hoare_1656922687triple(X_a),fun(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool)),insert(hoare_1656922687triple(X_a)),T_3),bot_bot(fun(hoare_1656922687triple(X_a),bool))))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [X_a,A_1] : hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),bot_bot(fun(X_a,bool))),A_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [C_1] :
( hBOOL(hoare_1924220188gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP(com,bool,wt,C_1))
=> hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),bot_bot(fun(hoare_1656922687triple(state),bool))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_1656922687triple(state),bool))))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [X_a,A_1] :
( hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),A_1),bot_bot(fun(X_a,bool))))
<=> ti(fun(X_a,bool),A_1) = bot_bot(fun(X_a,bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,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(f301,axiom,
hBOOL(hAPP(com,bool,wt,skip)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f593,axiom,
! [P] :
( ti(bool,P) = fFalse
| ti(bool,P) = fTrue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f608,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f615,hypothesis,
hBOOL(hoare_1924220188gleton),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f616,hypothesis,
hBOOL(wT_bodies),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f620,hypothesis,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f622,conjecture,
hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),hAPP(fun(pname,bool),fun(hoare_1656922687triple(state),bool),hAPP(fun(pname,hoare_1656922687triple(state)),fun(fun(pname,bool),fun(hoare_1656922687triple(state),bool)),image(pname,hoare_1656922687triple(state)),hAPP(fun(pname,com),fun(pname,hoare_1656922687triple(state)),hAPP(fun(com,hoare_1656922687triple(state)),fun(fun(pname,com),fun(pname,hoare_1656922687triple(state))),combb(com,hoare_1656922687triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_1656922687triple(state),bool))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f623,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),hAPP(fun(pname,bool),fun(hoare_1656922687triple(state),bool),hAPP(fun(pname,hoare_1656922687triple(state)),fun(fun(pname,bool),fun(hoare_1656922687triple(state),bool)),image(pname,hoare_1656922687triple(state)),hAPP(fun(pname,com),fun(pname,hoare_1656922687triple(state)),hAPP(fun(com,hoare_1656922687triple(state)),fun(fun(pname,com),fun(pname,hoare_1656922687triple(state))),combb(com,hoare_1656922687triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_1656922687triple(state),bool))))),
inference(negated_conjecture,[status(cth)],[f622]) ).
fof(f688,plain,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f689,plain,
! [B_1_1] :
( ( ~ hBOOL(B_1_1)
| hBOOL(ti(bool,B_1_1)) )
& ( hBOOL(B_1_1)
| ~ hBOOL(ti(bool,B_1_1)) ) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f690,plain,
( ! [B_1_1] :
( ~ hBOOL(B_1_1)
| hBOOL(ti(bool,B_1_1)) )
& ! [B_1_1] :
( hBOOL(B_1_1)
| ~ hBOOL(ti(bool,B_1_1)) ) ),
inference(miniscoping,[status(thm)],[f689]) ).
fof(f691,plain,
! [X0] :
( hBOOL(X0)
| ~ hBOOL(ti(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f690]) ).
fof(f697,plain,
! [X0,X1] : hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),bot_bot(fun(hoare_1656922687triple(X0),bool)))),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f700,plain,
! [X_a,Ts,G_1,Ts_1] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),ord_less_eq(fun(hoare_1656922687triple(X_a),bool)),Ts),Ts_1))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts_1)) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f701,plain,
! [X_a,G_1,Ts_1] :
( ! [Ts] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),ord_less_eq(fun(hoare_1656922687triple(X_a),bool)),Ts),Ts_1)) )
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts_1)) ),
inference(miniscoping,[status(thm)],[f700]) ).
fof(f702,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),X3))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),ord_less_eq(fun(hoare_1656922687triple(X0),bool)),X3),X2))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f701]) ).
fof(f706,plain,
! [X_a,G_1,G_2,Ts] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),G_2))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_2),Ts)) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f707,plain,
! [X_a,G_2,Ts] :
( ! [G_1] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),G_2)) )
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_2),Ts)) ),
inference(miniscoping,[status(thm)],[f706]) ).
fof(f708,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X3),X2))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X3),X1))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f712,plain,
! [X_a,G_1,T_3,Ts] :
( ( hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),Ts))
& hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),hAPP(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool),hAPP(hoare_1656922687triple(X_a),fun(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool)),insert(hoare_1656922687triple(X_a)),T_3),bot_bot(fun(hoare_1656922687triple(X_a),bool))))) )
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X_a),bool),bool,hAPP(fun(hoare_1656922687triple(X_a),bool),fun(fun(hoare_1656922687triple(X_a),bool),bool),hoare_279057269derivs(X_a),G_1),hAPP(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool),hAPP(hoare_1656922687triple(X_a),fun(fun(hoare_1656922687triple(X_a),bool),fun(hoare_1656922687triple(X_a),bool)),insert(hoare_1656922687triple(X_a)),T_3),Ts))) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f713,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),hAPP(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool),hAPP(hoare_1656922687triple(X0),fun(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool)),insert(hoare_1656922687triple(X0)),X2),bot_bot(fun(hoare_1656922687triple(X0),bool)))))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X1),hAPP(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool),hAPP(hoare_1656922687triple(X0),fun(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool)),insert(hoare_1656922687triple(X0)),X2),X3))) ),
inference(cnf_transformation,[status(thm)],[f712]) ).
fof(f722,plain,
! [X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),bot_bot(fun(X0,bool))),X1)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f745,plain,
! [C_1] :
( hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),bot_bot(fun(hoare_1656922687triple(state),bool))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_1656922687triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,C_1))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1924220188gleton) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f746,plain,
( ! [C_1] :
( hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),bot_bot(fun(hoare_1656922687triple(state),bool))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_1656922687triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,C_1)) )
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1924220188gleton) ),
inference(miniscoping,[status(thm)],[f745]) ).
fof(f747,plain,
! [X0] :
( hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),bot_bot(fun(hoare_1656922687triple(state),bool))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_1656922687triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1924220188gleton) ),
inference(cnf_transformation,[status(thm)],[f746]) ).
fof(f883,plain,
! [X_a,A_1] :
( ( ti(fun(X_a,bool),A_1) != bot_bot(fun(X_a,bool))
| hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),A_1),bot_bot(fun(X_a,bool)))) )
& ( ti(fun(X_a,bool),A_1) = bot_bot(fun(X_a,bool))
| ~ hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),A_1),bot_bot(fun(X_a,bool)))) ) ),
inference(NNF_transformation,[status(thm)],[f134]) ).
fof(f884,plain,
( ! [X_a,A_1] :
( ti(fun(X_a,bool),A_1) != bot_bot(fun(X_a,bool))
| hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),A_1),bot_bot(fun(X_a,bool)))) )
& ! [X_a,A_1] :
( ti(fun(X_a,bool),A_1) = bot_bot(fun(X_a,bool))
| ~ hBOOL(hAPP(fun(X_a,bool),bool,hAPP(fun(X_a,bool),fun(fun(X_a,bool),bool),ord_less_eq(fun(X_a,bool)),A_1),bot_bot(fun(X_a,bool)))) ) ),
inference(miniscoping,[status(thm)],[f883]) ).
fof(f885,plain,
! [X0,X1] :
( ti(fun(X0,bool),X1) = bot_bot(fun(X0,bool))
| ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X1),bot_bot(fun(X0,bool)))) ),
inference(cnf_transformation,[status(thm)],[f884]) ).
fof(f886,plain,
! [X0,X1] :
( ti(fun(X0,bool),X1) != bot_bot(fun(X0,bool))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X1),bot_bot(fun(X0,bool)))) ),
inference(cnf_transformation,[status(thm)],[f884]) ).
fof(f957,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)],[f158]) ).
fof(f958,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)],[f957]) ).
fof(f959,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)],[f958]) ).
fof(f1386,plain,
hBOOL(hAPP(com,bool,wt,skip)),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f2153,plain,
! [X0] :
( ti(bool,X0) = fFalse
| ti(bool,X0) = fTrue ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f2174,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(thm)],[f608]) ).
fof(f2184,plain,
hBOOL(hoare_1924220188gleton),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f2185,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[status(thm)],[f616]) ).
fof(f2189,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f2191,plain,
~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),hAPP(fun(pname,bool),fun(hoare_1656922687triple(state),bool),hAPP(fun(pname,hoare_1656922687triple(state)),fun(fun(pname,bool),fun(hoare_1656922687triple(state),bool)),image(pname,hoare_1656922687triple(state)),hAPP(fun(pname,com),fun(pname,hoare_1656922687triple(state)),hAPP(fun(com,hoare_1656922687triple(state)),fun(fun(pname,com),fun(pname,hoare_1656922687triple(state))),combb(com,hoare_1656922687triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_1656922687triple(state),bool))))),
inference(cnf_transformation,[status(thm)],[f623]) ).
fof(f2220,plain,
! [X0] :
( ~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),hAPP(fun(pname,bool),fun(hoare_1656922687triple(state),bool),hAPP(fun(pname,hoare_1656922687triple(state)),fun(fun(pname,bool),fun(hoare_1656922687triple(state),bool)),image(pname,hoare_1656922687triple(state)),hAPP(fun(pname,com),fun(pname,hoare_1656922687triple(state)),hAPP(fun(com,hoare_1656922687triple(state)),fun(fun(pname,com),fun(pname,hoare_1656922687triple(state))),combb(com,hoare_1656922687triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),X0))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),X0),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_1656922687triple(state),bool))))) ),
inference(resolution,[status(thm)],[f708,f2191]) ).
fof(f2247,plain,
! [X0] : ti(fun(X0,bool),bot_bot(fun(X0,bool))) = bot_bot(fun(X0,bool)),
inference(resolution,[status(thm)],[f885,f722]) ).
fof(f2258,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X2),X1))
| ~ hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X2),bot_bot(fun(hoare_1656922687triple(X0),bool))))
| ti(fun(hoare_1656922687triple(X0),bool),X1) != bot_bot(fun(hoare_1656922687triple(X0),bool)) ),
inference(resolution,[status(thm)],[f886,f702]) ).
fof(f2261,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X2),X1))
| ti(fun(hoare_1656922687triple(X0),bool),X1) != bot_bot(fun(hoare_1656922687triple(X0),bool)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2258,f697]) ).
fof(f2266,plain,
! [X0] :
( ~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),X0),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_1656922687triple(state),bool)))))
| ti(fun(hoare_1656922687triple(state),bool),X0) != bot_bot(fun(hoare_1656922687triple(state),bool)) ),
inference(resolution,[status(thm)],[f2261,f2220]) ).
fof(f2327,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),X0),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,y)),X1)))
| ti(fun(hoare_1656922687triple(state),bool),X0) != bot_bot(fun(hoare_1656922687triple(state),bool)) ),
inference(resolution,[status(thm)],[f2266,f713]) ).
fof(f2352,plain,
! [X0] :
( ti(bool,X0) = fFalse
| hBOOL(X0)
| ~ hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f2153,f691]) ).
fof(f2785,plain,
! [X0,X1,X2] :
( ti(bool,hAPP(X0,bool,X1,X2)) = fFalse
| fTrue = hAPP(X0,bool,X1,X2) ),
inference(paramodulation,[status(thm)],[f2153,f688]) ).
fof(f2800,plain,
! [X0,X1,X2] :
( hAPP(X0,bool,X1,X2) = fFalse
| fTrue = hAPP(X0,bool,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f688,f2785]) ).
fof(f3383,plain,
( hAPP(com,bool,wt,skip) = fFalse
| hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f2800,f1386]) ).
fof(f3463,plain,
( hBOOL(fTrue)
| hBOOL(fFalse) ),
inference(paramodulation,[status(thm)],[f3383,f1386]) ).
fof(f3468,plain,
hBOOL(fTrue),
inference(forward_subsumption_resolution,[status(thm)],[f3463,f2174]) ).
fof(f3472,plain,
! [X0] :
( ti(bool,X0) = fFalse
| hBOOL(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2352,f3468]) ).
fof(f3481,plain,
! [X0,X1,X2] :
( hAPP(X0,bool,X1,X2) = fFalse
| hBOOL(hAPP(X0,bool,X1,X2)) ),
inference(paramodulation,[status(thm)],[f688,f3472]) ).
fof(f5898,plain,
! [X0] :
( hBOOL(hAPP(fun(hoare_1656922687triple(state),bool),bool,hAPP(fun(hoare_1656922687triple(state),bool),fun(fun(hoare_1656922687triple(state),bool),bool),hoare_279057269derivs(state),bot_bot(fun(hoare_1656922687triple(state),bool))),hAPP(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool),hAPP(hoare_1656922687triple(state),fun(fun(hoare_1656922687triple(state),bool),fun(hoare_1656922687triple(state),bool)),insert(hoare_1656922687triple(state)),hAPP(com,hoare_1656922687triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_1656922687triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies) ),
inference(forward_subsumption_resolution,[status(thm)],[f747,f2184]) ).
fof(f5901,plain,
( ti(fun(hoare_1656922687triple(state),bool),bot_bot(fun(hoare_1656922687triple(state),bool))) != bot_bot(fun(hoare_1656922687triple(state),bool))
| ~ hBOOL(hAPP(com,bool,wt,y))
| ~ hBOOL(wT_bodies) ),
inference(resolution,[status(thm)],[f5898,f2327]) ).
fof(f5918,plain,
( bot_bot(fun(hoare_1656922687triple(state),bool)) != bot_bot(fun(hoare_1656922687triple(state),bool))
| ~ hBOOL(hAPP(com,bool,wt,y))
| ~ hBOOL(wT_bodies) ),
inference(forward_demodulation,[status(thm)],[f2247,f5901]) ).
fof(f5919,plain,
( ~ hBOOL(hAPP(com,bool,wt,y))
| ~ hBOOL(wT_bodies) ),
inference(trivial_equality_resolution,[status(thm)],[f5918]) ).
fof(f5920,plain,
~ hBOOL(hAPP(com,bool,wt,y)),
inference(forward_subsumption_resolution,[status(thm)],[f5919,f2185]) ).
fof(f5963,plain,
hAPP(com,bool,wt,y) = fFalse,
inference(resolution,[status(thm)],[f5920,f3481]) ).
fof(f18007,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)],[f959,f2185]) ).
fof(f22011,plain,
hBOOL(hAPP(com,bool,wt,y)),
inference(resolution,[status(thm)],[f2189,f18007]) ).
fof(f22020,plain,
hBOOL(fFalse),
inference(forward_demodulation,[status(thm)],[f5963,f22011]) ).
fof(f22021,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f22020,f2174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW474+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.40 % Computer : n003.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Mon Sep 21 10:00:46 UTC 2026
% 0.16/0.40 % CPUTime :
% 0.23/0.51 % Drodi V4.1.1
% 67.59/9.36 % Refutation found
% 67.59/9.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 67.59/9.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 26.34/10.65 % Elapsed time: 10.035459 seconds
% 26.34/10.65 % CPU time: 66.694057 seconds
% 26.34/10.65 % Total memory used: 768.598 MB
% 26.34/10.65 % Net memory used: 752.517 MB
%------------------------------------------------------------------------------