%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW470+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:07:55 PM UTC 2026
% Result : Theorem 3.36s 1.13s
% Output : CNFRefutation 3.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 8
% Syntax : Number of formulae : 29 ( 20 unt; 0 def)
% Number of atoms : 45 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 31 ( 15 ~; 10 |; 2 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 11 con; 0-5 aty)
% Number of variables : 61 ( 59 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f67,hypothesis,
ti(bool,fFalse) = fFalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [X_a,X_c,B_1_1,B_2_1] : hAPP(X_a,X_c,ti(fun(X_a,X_c),B_1_1),B_2_1) = hAPP(X_a,X_c,B_1_1,B_2_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [X_b,Ga] : hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),bot_bot(fun(hoare_2118899576triple(X_b),bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [X_b,Ga,G_1,Ts] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),G_1),Ts))
=> ( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),G_1))
=> hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),Ts)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [X_b,Ga,Ca,Q_3,Pa] :
( ! [Z_4,S_3] :
( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_4),S_3))
=> hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),S_3))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,Z_4)))),bot_bot(fun(hoare_2118899576triple(X_b),bool))))) )
=> hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1179,axiom,
! [X_b,X_a,P,Q] : hAPP(X_b,X_a,hAPP(X_a,fun(X_b,X_a),combk(X_a,X_b),P),Q) = ti(X_a,P),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1187,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1194,conjecture,
hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1195,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))),
inference(negated_conjecture,[status(cth)],[f1194]) ).
fof(f1292,plain,
ti(bool,fFalse) = fFalse,
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f1299,plain,
! [X0,X1,X2,X3] : hAPP(X0,X1,ti(fun(X0,X1),X2),X3) = hAPP(X0,X1,X2,X3),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f1311,plain,
! [X0,X1] : hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X1),bot_bot(fun(hoare_2118899576triple(X0),bool)))),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f1318,plain,
! [X_b,Ga,G_1,Ts] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),Ts))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),G_1))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),G_1),Ts)) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f1319,plain,
! [X_b,G_1,Ts] :
( ! [Ga] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),Ts))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),G_1)) )
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),G_1),Ts)) ),
inference(miniscoping,[status(thm)],[f1318]) ).
fof(f1320,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X3),X2))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X3),X1))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f1319]) ).
fof(f1327,plain,
! [X_b,Ga,Ca,Q_3,Pa] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool)))))
| ? [Z_4,S_3] :
( ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),S_3))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,Z_4)))),bot_bot(fun(hoare_2118899576triple(X_b),bool)))))
& hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_4),S_3)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f1328,plain,
! [X_b,Ga,Ca,Q_3,Pa] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool)))))
| ( ~ hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),sK1_skl(Pa,Q_3,Ca,Ga,X_b)))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,sK0_skl(Pa,Q_3,Ca,Ga,X_b))))),bot_bot(fun(hoare_2118899576triple(X_b),bool)))))
& hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,sK0_skl(Pa,Q_3,Ca,Ga,X_b)),sK1_skl(Pa,Q_3,Ca,Ga,X_b))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_4,sK0_skl(Pa,Q_3,Ca,Ga,X_b)),skolemize(S_3,sK1_skl(Pa,Q_3,Ca,Ga,X_b))],[f1327]) ).
fof(f1329,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X4),hAPP(fun(hoare_2118899576triple(X0),bool),fun(hoare_2118899576triple(X0),bool),hAPP(hoare_2118899576triple(X0),fun(fun(hoare_2118899576triple(X0),bool),fun(hoare_2118899576triple(X0),bool)),insert(hoare_2118899576triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_2118899576triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_2118899576triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_2118899576triple(X0))),hoare_759811442triple(X0),X1),X3),X2)),bot_bot(fun(hoare_2118899576triple(X0),bool)))))
| hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,sK0_skl(X1,X2,X3,X4,X0)),sK1_skl(X1,X2,X3,X4,X0))) ),
inference(cnf_transformation,[status(thm)],[f1328]) ).
fof(f4495,plain,
! [X0,X1,X2,X3] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f4508,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(thm)],[f1187]) ).
fof(f4518,plain,
~ hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))),
inference(cnf_transformation,[status(thm)],[f1195]) ).
fof(f4612,plain,
! [X0] :
( ~ hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),X0))
| ~ hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),X0),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))) ),
inference(resolution,[status(thm)],[f1320,f4518]) ).
fof(f4615,plain,
~ hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),bot_bot(fun(hoare_2118899576triple(x_a),bool))),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))),
inference(resolution,[status(thm)],[f4612,f1311]) ).
fof(f7689,plain,
hBOOL(hAPP(state,bool,hAPP(x_a,fun(state,bool),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),sK0_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,bot_bot(fun(hoare_2118899576triple(x_a),bool)),x_a)),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,bot_bot(fun(hoare_2118899576triple(x_a),bool)),x_a))),
inference(resolution,[status(thm)],[f1329,f4615]) ).
fof(f7696,plain,
hBOOL(hAPP(state,bool,ti(fun(state,bool),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,bot_bot(fun(hoare_2118899576triple(x_a),bool)),x_a))),
inference(forward_demodulation,[status(thm)],[f4495,f7689]) ).
fof(f7697,plain,
hBOOL(hAPP(state,bool,hAPP(bool,fun(state,bool),combk(bool,state),fFalse),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,bot_bot(fun(hoare_2118899576triple(x_a),bool)),x_a))),
inference(forward_demodulation,[status(thm)],[f1299,f7696]) ).
fof(f7698,plain,
hBOOL(ti(bool,fFalse)),
inference(forward_demodulation,[status(thm)],[f4495,f7697]) ).
fof(f7699,plain,
hBOOL(fFalse),
inference(forward_demodulation,[status(thm)],[f1292,f7698]) ).
fof(f7700,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f7699,f4508]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:56:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.46 % Drodi V4.1.1
% 3.36/1.13 % Refutation found
% 3.36/1.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.36/1.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.36/1.20 % Elapsed time: 0.829624 seconds
% 3.36/1.20 % CPU time: 5.367516 seconds
% 3.36/1.20 % Total memory used: 383.631 MB
% 3.36/1.20 % Net memory used: 380.872 MB
%------------------------------------------------------------------------------