%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 09:14:18 AM UTC 2026
% Result : Theorem 5.98s 6.18s
% Output : CNFRefutation 5.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 34 ( 28 unt; 0 def)
% Number of atoms : 59 ( 18 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 40 ( 15 ~; 14 |; 7 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 3 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 11 con; 0-7 aty)
% Number of variables : 110 ( 5 sgn 57 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_hAPP_res,axiom,
! [X_c,X_a,B_1_1,B_2] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2)) = hAPP(X_a,X_c,B_1_1,B_2),
file('theBenchmark.p',tsy_c_hAPP_res) ).
fof(fact_12_singleton__conv2,axiom,
! [X_b,A_4] : hAPP(fun(X_b,bool),fun(X_b,bool),collect(X_b),hAPP(X_b,fun(X_b,bool),fequal(X_b),A_4)) = hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),A_4),bot_bot(fun(X_b,bool))),
file('theBenchmark.p',fact_12_singleton__conv2) ).
fof(fact_54_the__sym__eq__trivial,axiom,
! [X_b,X_1] : hAPP(fun(X_b,bool),X_b,the(X_b),hAPP(X_b,fun(X_b,bool),fequal(X_b),X_1)) = ti(X_b,X_1),
file('theBenchmark.p',fact_54_the__sym__eq__trivial) ).
fof(fact_62_conseq,axiom,
! [X_b,Q_1,Ga,Ca,Pa] :
( ! [Z_1,S] :
( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_1),S))
=> ? [P_1,Q_2] :
( ! [S_1] :
( ! [Z_2] :
( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),P_1,Z_2),S))
=> hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_2,Z_2),S_1)) )
=> hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_1,Z_1),S_1)) )
& hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),P_1),Ca),Q_2)),bot_bot(fun(hoare_509422987triple(X_b),bool))))) ) )
=> hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_509422987triple(X_b),bool))))) ),
file('theBenchmark.p',fact_62_conseq) ).
fof(help_COMBK_1_1_U,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('theBenchmark.p',help_COMBK_1_1_U) ).
fof(conj_0,conjecture,
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),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(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_509422987triple(x_a),bool))))),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ 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),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(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_509422987triple(x_a),bool))))),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(tsy_c_fFalse_res,axiom,
ti(bool,fFalse) = fFalse,
file('theBenchmark.p',tsy_c_fFalse_res) ).
cnf(c_216,plain,
ti(bool,fFalse) = fFalse,
inference(clausify,[status(thm)],[tsy_c_fFalse_res]) ).
cnf(c_226,plain,
hAPP(A,B,C,D) = ti(B,hAPP(A,B,C,D)),
inference(clausify,[status(thm)],[tsy_c_hAPP_res]) ).
cnf(c_227,plain,
ti(A,hAPP(B,A,C,D)) = hAPP(B,A,C,D),
inference(copy,[status(thm)],[c_226]) ).
cnf(c_258,plain,
hAPP(fun(A,bool),fun(A,bool),hAPP(A,fun(fun(A,bool),fun(A,bool)),insert(A),B),bot_bot(fun(A,bool))) = hAPP(fun(A,bool),fun(A,bool),collect(A),hAPP(A,fun(A,bool),fequal(A),B)),
inference(clausify,[status(thm)],[fact_12_singleton__conv2]) ).
cnf(c_318,plain,
hAPP(fun(A,bool),A,the(A),hAPP(A,fun(A,bool),fequal(A),B)) = ti(A,B),
inference(clausify,[status(thm)],[fact_54_the__sym__eq__trivial]) ).
cnf(c_319,plain,
ti(A,B) = hAPP(fun(A,bool),A,the(A),hAPP(A,fun(A,bool),fequal(A),B)),
inference(copy,[status(thm)],[c_318]) ).
fof(nnf_72,plain,
! [X_b,Q_1,Ga,Ca,Pa] :
( hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_509422987triple(X_b),bool)))))
| ? [Z_1,S] :
( ! [P_1,Q_2] :
( ? [S_1] :
( ~ hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_1,Z_1),S_1))
& ! [Z_2] :
( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_2,Z_2),S_1))
| ~ hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),P_1,Z_2),S)) ) )
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),P_1),Ca),Q_2)),bot_bot(fun(hoare_509422987triple(X_b),bool))))) )
& hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_1),S)) ) ),
inference(fof_nnf,[status(thm)],[fact_62_conseq]) ).
fof(sk_fact_62_conseq_sk,plain,
! [X_b,Q_1,Ga,Ca,Pa] :
( hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_509422987triple(X_b),bool)))))
| ( ! [P_1,Q_2] :
( ( ~ hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_1,sK0(X_b,Q_1,Ga,Ca,Pa)),sK2(X_b,Q_1,Ga,Ca,Pa,P_1,Q_2)))
& ! [Z_2] :
( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Q_2,Z_2),sK2(X_b,Q_1,Ga,Ca,Pa,P_1,Q_2)))
| ~ hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),P_1,Z_2),sK1(X_b,Q_1,Ga,Ca,Pa))) ) )
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X_b),bool),bool,hAPP(fun(hoare_509422987triple(X_b),bool),fun(fun(hoare_509422987triple(X_b),bool),bool),hoare_122391849derivs(X_b),Ga),hAPP(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool),hAPP(hoare_509422987triple(X_b),fun(fun(hoare_509422987triple(X_b),bool),fun(hoare_509422987triple(X_b),bool)),insert(hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_509422987triple(X_b))),hoare_1008221573triple(X_b),P_1),Ca),Q_2)),bot_bot(fun(hoare_509422987triple(X_b),bool))))) )
& hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,sK0(X_b,Q_1,Ga,Ca,Pa)),sK1(X_b,Q_1,Ga,Ca,Pa))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(Z_1,sK0(X_b,Q_1,Ga,Ca,Pa)),skolemize(S,sK1(X_b,Q_1,Ga,Ca,Pa)),skolemize(S_1,sK2(X_b,Q_1,Ga,Ca,Pa,P_1,Q_2))],[nnf_72]) ).
fof(sk_fact_62_conseq,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( hBOOL(hAPP(fun(hoare_509422987triple(VAR_0),bool),bool,hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(fun(hoare_509422987triple(VAR_0),bool),bool),hoare_122391849derivs(VAR_0),VAR_1),hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool),hAPP(hoare_509422987triple(VAR_0),fun(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool)),insert(hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0),hAPP(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),fun(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0))),hoare_1008221573triple(VAR_0),VAR_6),VAR_3),VAR_5)),bot_bot(fun(hoare_509422987triple(VAR_0),bool)))))
| ~ hBOOL(hAPP(state,bool,hAPP(VAR_0,fun(state,bool),VAR_5,sK0(VAR_0,VAR_5,VAR_1,VAR_3,VAR_6)),sK2(VAR_0,VAR_5,VAR_1,VAR_3,VAR_6,VAR_2,VAR_4)))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(VAR_0),bool),bool,hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(fun(hoare_509422987triple(VAR_0),bool),bool),hoare_122391849derivs(VAR_0),VAR_1),hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool),hAPP(hoare_509422987triple(VAR_0),fun(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool)),insert(hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0),hAPP(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),fun(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0))),hoare_1008221573triple(VAR_0),VAR_2),VAR_3),VAR_4)),bot_bot(fun(hoare_509422987triple(VAR_0),bool))))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( hBOOL(hAPP(fun(hoare_509422987triple(VAR_0),bool),bool,hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(fun(hoare_509422987triple(VAR_0),bool),bool),hoare_122391849derivs(VAR_0),VAR_1),hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool),hAPP(hoare_509422987triple(VAR_0),fun(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool)),insert(hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0),hAPP(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),fun(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0))),hoare_1008221573triple(VAR_0),VAR_7),VAR_3),VAR_6)),bot_bot(fun(hoare_509422987triple(VAR_0),bool)))))
| hBOOL(hAPP(state,bool,hAPP(VAR_0,fun(state,bool),VAR_4,VAR_5),sK2(VAR_0,VAR_6,VAR_1,VAR_3,VAR_7,VAR_2,VAR_4)))
| ~ hBOOL(hAPP(state,bool,hAPP(VAR_0,fun(state,bool),VAR_2,VAR_5),sK1(VAR_0,VAR_6,VAR_1,VAR_3,VAR_7)))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(VAR_0),bool),bool,hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(fun(hoare_509422987triple(VAR_0),bool),bool),hoare_122391849derivs(VAR_0),VAR_1),hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool),hAPP(hoare_509422987triple(VAR_0),fun(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool)),insert(hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0),hAPP(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),fun(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0))),hoare_1008221573triple(VAR_0),VAR_2),VAR_3),VAR_4)),bot_bot(fun(hoare_509422987triple(VAR_0),bool))))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( hBOOL(hAPP(fun(hoare_509422987triple(VAR_0),bool),bool,hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(fun(hoare_509422987triple(VAR_0),bool),bool),hoare_122391849derivs(VAR_0),VAR_3),hAPP(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool),hAPP(hoare_509422987triple(VAR_0),fun(fun(hoare_509422987triple(VAR_0),bool),fun(hoare_509422987triple(VAR_0),bool)),insert(hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0),hAPP(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0)),hAPP(fun(VAR_0,fun(state,bool)),fun(com,fun(fun(VAR_0,fun(state,bool)),hoare_509422987triple(VAR_0))),hoare_1008221573triple(VAR_0),VAR_1),VAR_4),VAR_2)),bot_bot(fun(hoare_509422987triple(VAR_0),bool)))))
| hBOOL(hAPP(state,bool,hAPP(VAR_0,fun(state,bool),VAR_1,sK0(VAR_0,VAR_2,VAR_3,VAR_4,VAR_1)),sK1(VAR_0,VAR_2,VAR_3,VAR_4,VAR_1))) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_62_conseq_sk]) ).
cnf(c_342,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),D),hAPP(fun(hoare_509422987triple(A),bool),fun(hoare_509422987triple(A),bool),hAPP(hoare_509422987triple(A),fun(fun(hoare_509422987triple(A),bool),fun(hoare_509422987triple(A),bool)),insert(hoare_509422987triple(A)),hAPP(fun(A,fun(state,bool)),hoare_509422987triple(A),hAPP(com,fun(fun(A,fun(state,bool)),hoare_509422987triple(A)),hAPP(fun(A,fun(state,bool)),fun(com,fun(fun(A,fun(state,bool)),hoare_509422987triple(A))),hoare_1008221573triple(A),B),E),C)),bot_bot(fun(hoare_509422987triple(A),bool)))))
| hBOOL(hAPP(state,bool,hAPP(A,fun(state,bool),B,sK0(A,C,D,E,B)),sK1(A,C,D,E,B))) ),
inference(split_conjunct,[status(thm)],[sk_fact_62_conseq]) ).
cnf(c_343,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),D),hAPP(fun(hoare_509422987triple(A),bool),fun(hoare_509422987triple(A),bool),collect(hoare_509422987triple(A)),hAPP(hoare_509422987triple(A),fun(hoare_509422987triple(A),bool),fequal(hoare_509422987triple(A)),hAPP(fun(A,fun(state,bool)),hoare_509422987triple(A),hAPP(com,fun(fun(A,fun(state,bool)),hoare_509422987triple(A)),hAPP(fun(A,fun(state,bool)),fun(com,fun(fun(A,fun(state,bool)),hoare_509422987triple(A))),hoare_1008221573triple(A),B),E),C)))))
| hBOOL(hAPP(state,bool,hAPP(A,fun(state,bool),B,sK0(A,C,D,E,B)),sK1(A,C,D,E,B))) ),
inference(paramod,[status(thm)],[c_258,c_342]) ).
cnf(c_458,plain,
hAPP(A,B,hAPP(B,fun(A,B),combk(B,A),C),D) = ti(B,C),
inference(clausify,[status(thm)],[help_COMBK_1_1_U]) ).
cnf(c_2872,plain,
hAPP(A,B,hAPP(B,fun(A,B),combk(B,A),C),D) = hAPP(fun(B,bool),B,the(B),hAPP(B,fun(B,bool),fequal(B),C)),
inference(paramod,[status(thm)],[c_319,c_458]) ).
cnf(c_459,plain,
hAPP(fun(A,bool),A,the(A),hAPP(A,fun(A,bool),fequal(A),B)) = hAPP(C,A,hAPP(A,fun(C,A),combk(A,C),B),D),
inference(copy,[status(thm)],[c_2872]) ).
fof(help_fFalse_1_1_U,axiom,
~ hBOOL(fFalse),
file('theBenchmark.p',help_fFalse_1_1_U) ).
cnf(c_467,plain,
~ hBOOL(fFalse),
inference(clausify,[status(thm)],[help_fFalse_1_1_U]) ).
cnf(c_477,negated_conjecture,
~ 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),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),hAPP(hoare_509422987triple(x_a),fun(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool)),insert(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(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_509422987triple(x_a),bool))))),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_478,negated_conjecture,
~ 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),hAPP(fun(hoare_509422987triple(x_a),bool),fun(hoare_509422987triple(x_a),bool),collect(hoare_509422987triple(x_a)),hAPP(hoare_509422987triple(x_a),fun(hoare_509422987triple(x_a),bool),fequal(hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_509422987triple(x_a))),hoare_1008221573triple(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))))))),
inference(paramod,[status(thm)],[c_258,c_477]) ).
cnf(c_529,plain,
hAPP(fun(A,bool),A,the(A),hAPP(A,fun(A,bool),fequal(A),hAPP(B,A,C,D))) = hAPP(B,A,C,D),
inference(paramod,[status(thm)],[c_319,c_227]) ).
cnf(c_538,plain,
hAPP(fun(bool,bool),bool,the(bool),hAPP(bool,fun(bool,bool),fequal(bool),fFalse)) = fFalse,
inference(paramod,[status(thm)],[c_319,c_216]) ).
cnf(c_664,plain,
hAPP(A,bool,hAPP(bool,fun(A,bool),combk(bool,A),fFalse),B) = fFalse,
inference(paramod,[status(thm)],[c_459,c_538]) ).
cnf(c_668,plain,
hAPP(A,B,hAPP(B,fun(A,B),combk(B,A),hAPP(C,B,D,E)),F) = hAPP(C,B,D,E),
inference(paramod,[status(thm)],[c_459,c_529]) ).
cnf(c_2873,negated_conjecture,
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(x_a,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)),g,c,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)))),sK1(x_a,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)),g,c,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))))),
inference(resolve,[status(thm)],[c_343,c_478]) ).
cnf(c_2874,negated_conjecture,
hBOOL(hAPP(state,bool,hAPP(bool,fun(state,bool),combk(bool,state),fFalse),sK1(x_a,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)),g,c,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))))),
inference(paramod,[status(thm)],[c_668,c_2873]) ).
cnf(c_2875,negated_conjecture,
hBOOL(fFalse),
inference(paramod,[status(thm)],[c_664,c_2874]) ).
cnf(c_2871,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_467,c_2875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/5.32 % Computer : n012.cluster.edu
% 0.05/5.32 % Model : x86_64 x86_64
% 0.05/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.32 % Memory : 8046.5625MB
% 0.05/5.32 % OS : Linux 6.8.0-71-generic
% 0.05/5.32 % CPULimit : 300
% 0.05/5.32 % WCLimit : 300
% 0.05/5.32 % DateTime : Sat Sep 26 15:57:56 UTC 2026
% 0.05/5.33 % CPUTime :
% 0.05/5.33 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.05/5.33 % Process 966024 was started by sandbox on n012,
% 0.05/5.33 % Sat Sep 26 15:57:56 2026
% 0.05/5.33 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.05/5.35
% 0.05/5.35 % From the command line: assign(max_seconds, 300).
% 0.05/5.35
% 0.05/5.35 % SInE: 134 to sos, 28 to usable, of 162 axioms (tolerance 2.00, depth 0 fixpoint).
% 5.98/6.18
% 5.98/6.18 % SZS status Theorem for theBenchmark
% 5.98/6.18
% 5.98/6.18 % Proof 1 at 0.71 (+ 0.08) seconds.
% 5.98/6.18 % Length of proof is 24.
% 5.98/6.18 % Level of proof is 5.
% 5.98/6.18 % Maximum clause weight is 476.000.
% 5.98/6.18 % Given clauses 291.
% 5.98/6.18
% 5.98/6.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------