%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.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 : Fri Sep 25 03:29:45 PM UTC 2026
% Result : Theorem 27.78s 6.09s
% Output : CNFRefutation 27.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 16
% Syntax : Number of formulae : 86 ( 66 unt; 0 def)
% Number of atoms : 117 ( 57 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 58 ( 27 ~; 21 |; 6 &)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 11 con; 0-5 aty)
% Number of variables : 202 ( 0 sgn 198 !; 4 ?; 90 :)
% Comments :
%------------------------------------------------------------------------------
fof(f23,axiom,
ti(bool,fFalse) = fFalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_fFalse_res) ).
fof(f31,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_arg2) ).
fof(f32,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4] :
( ! [X5,X6] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,X5),X6))
=> 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),X6))),X2),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(X0,fun(state,bool),X3,X5)))),bot_bot(fun(hoare_509422987triple(X0),bool))))) )
=> 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X2),X3)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_escape) ).
fof(f50,axiom,
! [X0,X1] : ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_emptyE) ).
fof(f51,axiom,
! [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))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_singleton__conv2) ).
fof(f52,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,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))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_singleton__conv) ).
fof(f59,axiom,
! [X0,X1] :
( bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)
<=> ! [X2] : ~ hBOOL(hAPP(X0,bool,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_empty__Collect__eq) ).
fof(f62,axiom,
! [X0] : bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_empty__def) ).
fof(f93,axiom,
! [X0,X1] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = ti(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_the__sym__eq__trivial) ).
fof(f94,axiom,
! [X0,X1] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)) = ti(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_the__eq__trivial) ).
fof(f105,axiom,
! [X0,X1] :
( hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1))
<=> hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_bot__empty__eq) ).
fof(f116,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = ti(fun(X0,bool),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Collect__def) ).
fof(f148,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).
fof(f156,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f163,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('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f164,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(negated_conjecture,[status(cth)],[f163]) ).
fof(f165,plain,
~ 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(flattening,[],[f164]) ).
fof(f181,plain,
! [X0,X1,X2,X3,X4] :
( ? [X5,X6] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,X5),X6))
& ~ 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),X6))),X2),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(X0,fun(state,bool),X3,X5)))),bot_bot(fun(hoare_509422987triple(X0),bool))))) )
| 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X2),X3)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
inference(ennf_transformation,[],[f44]) ).
fof(f220,plain,
! [X0,X1,X2,X3,X4] :
( ( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,sK14(X0,X1,X2,X3,X4)),sK15(X0,X1,X2,X3,X4)))
& ~ 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),sK15(X0,X1,X2,X3,X4)))),X2),hAPP(fun(state,bool),fun(X0,fun(state,bool)),combk(fun(state,bool),X0),hAPP(X0,fun(state,bool),X3,sK14(X0,X1,X2,X3,X4))))),bot_bot(fun(hoare_509422987triple(X0),bool))))) )
| 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X2),X3)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15]),skolemize(X5,sK14(X0,X1,X2,X3,X4)),skolemize(X6,sK15(X0,X1,X2,X3,X4))],[f181]) ).
fof(f225,plain,
! [X0,X1] :
( ( bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)
| ! [X2] : ~ hBOOL(hAPP(X0,bool,X1,X2)) )
& ( ? [X2] : hBOOL(hAPP(X0,bool,X1,X2))
| bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(nnf_transformation,[],[f59]) ).
fof(f226,plain,
! [X0,X1] :
( ( bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)
| ! [X3] : ~ hBOOL(hAPP(X0,bool,X1,X3)) )
& ( ? [X2] : hBOOL(hAPP(X0,bool,X1,X2))
| bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(rectify,[],[f225]) ).
fof(f227,plain,
! [X0,X1] :
( ( bot_bot(fun(X0,bool)) != hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1)
| ! [X3] : ~ hBOOL(hAPP(X0,bool,X1,X3)) )
& ( hBOOL(hAPP(X0,bool,X1,sK16(X0,X1)))
| bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X2,sK16(X0,X1))],[f226]) ).
fof(f244,plain,
! [X0,X1] :
( ( ~ hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))) )
& ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool))))
| hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1)) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f261,plain,
fFalse = ti(bool,fFalse),
inference(cnf_transformation,[],[f23]) ).
fof(f270,plain,
~ 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(cnf_transformation,[],[f165]) ).
fof(f273,plain,
! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = ti(X0,hAPP(X1,X0,X2,X3)),
inference(cnf_transformation,[],[f32]) ).
fof(f274,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
inference(cnf_transformation,[],[f31]) ).
fof(f276,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f156]) ).
fof(f277,plain,
! [X0] : bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse)),
inference(cnf_transformation,[],[f62]) ).
fof(f313,plain,
! [X0,X1] : ti(X0,X1) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)),
inference(cnf_transformation,[],[f94]) ).
fof(f314,plain,
! [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))) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)),
inference(cnf_transformation,[],[f52]) ).
fof(f316,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
inference(cnf_transformation,[],[f148]) ).
fof(f317,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X4,sK14(X0,X1,X2,X3,X4)),sK15(X0,X1,X2,X3,X4)))
| 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X4),X2),X3)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
inference(cnf_transformation,[],[f220]) ).
fof(f341,plain,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = ti(fun(X0,bool),X1),
inference(cnf_transformation,[],[f116]) ).
fof(f343,plain,
! [X0,X1] :
( hBOOL(hAPP(X0,bool,X1,sK16(X0,X1)))
| bot_bot(fun(X0,bool)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) ),
inference(cnf_transformation,[],[f227]) ).
fof(f346,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,[],[f51]) ).
fof(f356,plain,
! [X0,X1] : ti(X0,X1) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f93]) ).
fof(f385,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1))
| hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))) ),
inference(cnf_transformation,[],[f244]) ).
fof(f412,plain,
! [X0,X1] : ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))),
inference(cnf_transformation,[],[f50]) ).
fof(f417,plain,
fFalse = hAPP(fun(bool,bool),bool,the(bool),hAPP(bool,fun(bool,bool),hAPP(fun(bool,fun(bool,bool)),fun(bool,fun(bool,bool)),combc(bool,bool,bool),fequal(bool)),fFalse)),
inference(definition_unfolding,[],[f261,f313]) ).
fof(f428,plain,
! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),hAPP(X1,X0,X2,X3))),
inference(definition_unfolding,[],[f273,f313]) ).
fof(f429,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X3))),
inference(definition_unfolding,[],[f274,f313]) ).
fof(f436,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = hAPP(fun(X1,bool),X1,the(X1),hAPP(X1,fun(X1,bool),hAPP(fun(X1,fun(X1,bool)),fun(X1,fun(X1,bool)),combc(X1,X1,bool),fequal(X1)),X2)),
inference(definition_unfolding,[],[f316,f313]) ).
fof(f450,plain,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = hAPP(fun(fun(X0,bool),bool),fun(X0,bool),the(fun(X0,bool)),hAPP(fun(X0,bool),fun(fun(X0,bool),bool),hAPP(fun(fun(X0,bool),fun(fun(X0,bool),bool)),fun(fun(X0,bool),fun(fun(X0,bool),bool)),combc(fun(X0,bool),fun(X0,bool),bool),fequal(fun(X0,bool))),X1)),
inference(definition_unfolding,[],[f341,f313]) ).
fof(f458,plain,
! [X0,X1] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)),
inference(definition_unfolding,[],[f356,f313]) ).
tcf(c_49,plain,
hAPP(fun(bool,bool),bool,the(bool),hAPP(bool,fun(bool,bool),hAPP(fun(bool,fun(bool,bool)),fun(bool,fun(bool,bool)),combc(bool,bool,bool),fequal(bool)),fFalse)) = fFalse,
inference(cnf_transformation,[],[f417]) ).
tcf(c_58,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(cnf_transformation,[],[f270]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),hAPP(X1,X0,X2,X3))) = hAPP(X1,X0,X2,X3),
inference(cnf_transformation,[],[f428]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(X0,X1,X2,hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X3))) = hAPP(X0,X1,X2,X3),
inference(cnf_transformation,[],[f429]) ).
tcf(c_64,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f276]) ).
tcf(c_65,plain,
! [X0: $i] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse)) = bot_bot(fun(X0,bool)),
inference(cnf_transformation,[],[f277]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,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,[],[f314]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)) = hAPP(X2,X0,hAPP(X0,fun(X2,X0),combk(X0,X2),X1),X3),
inference(cnf_transformation,[],[f436]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,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),X1),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] : hAPP(fun(fun(X0,bool),bool),fun(X0,bool),the(fun(X0,bool)),hAPP(fun(X0,bool),fun(fun(X0,bool),bool),hAPP(fun(fun(X0,bool),fun(fun(X0,bool),bool)),fun(fun(X0,bool),fun(fun(X0,bool),bool)),combc(fun(X0,bool),fun(X0,bool),bool),fequal(fun(X0,bool))),X1)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1),
inference(cnf_transformation,[],[f450]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(X0,bool,X1,sK16(X0,X1)))
| ( hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1) = bot_bot(fun(X0,bool)) ) ),
inference(cnf_transformation,[],[f343]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] : hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f346]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)) = hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f458]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool))))
| ~ hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1)) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i] : ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),bot_bot(fun(X0,bool)))),
inference(cnf_transformation,[],[f412]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] : ~ hBOOL(hAPP(X0,bool,bot_bot(fun(X0,bool)),X1)),
inference(global_subsumption_just,[status(thm)],[c_172,c_198,c_172]) ).
tcf(c_372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,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),X1),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),hAPP(hoare_509422987triple(X0),fun(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool)),insert(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4)),bot_bot(fun(hoare_509422987triple(X0),bool))))) ),
inference(prop_impl_just,[status(thm)],[c_104]) ).
tcf(c_1444,plain,
hAPP(fun(bool,bool),bool,the(bool),hAPP(bool,fun(bool,bool),fequal(bool),fFalse)) = fFalse,
inference(demodulation,[status(thm)],[c_49,c_142]) ).
tcf(c_1447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(X0,X1,X2,hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X3))) = hAPP(X0,X1,X2,X3),
inference(demodulation,[status(thm)],[c_62,c_142]) ).
tcf(c_1448,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),hAPP(X1,X0,X2,X3))) = hAPP(X1,X0,X2,X3),
inference(demodulation,[status(thm)],[c_61,c_142]) ).
tcf(c_1495,plain,
! [X0: $i,X1: $i] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(light_normalisation,[status(thm)],[c_100,c_132]) ).
tcf(c_1528,plain,
! [X0: $i,X1: $i] : hAPP(fun(fun(X0,bool),bool),fun(X0,bool),the(fun(X0,bool)),hAPP(fun(X0,bool),fun(fun(X0,bool),bool),fequal(fun(X0,bool)),X1)) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X1),
inference(demodulation,[status(thm)],[c_127,c_142]) ).
tcf(c_1718,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,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),X1),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),collect(hoare_509422987triple(X0)),hAPP(hoare_509422987triple(X0),fun(hoare_509422987triple(X0),bool),fequal(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4))))) ),
inference(demodulation,[status(thm)],[c_372,c_132]) ).
tcf(c_2108,plain,
~ 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(demodulation,[status(thm)],[c_58,c_132]) ).
tcf(c_2353,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( 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),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),collect(hoare_509422987triple(X0)),hAPP(hoare_509422987triple(X0),fun(hoare_509422987triple(X0),bool),fequal(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4)))))
| hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,X2))) ),
inference(prop_impl_just,[status(thm)],[c_1718]) ).
tcf(c_2354,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,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),X1),hAPP(fun(hoare_509422987triple(X0),bool),fun(hoare_509422987triple(X0),bool),collect(hoare_509422987triple(X0)),hAPP(hoare_509422987triple(X0),fun(hoare_509422987triple(X0),bool),fequal(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4))))) ),
inference(renaming,[status(thm)],[c_2353]) ).
tcf(c_6123,plain,
! [X0: $i] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),bot_bot(fun(X0,bool))) = bot_bot(fun(X0,bool)),
inference(superposition,[status(thm)],[c_128,c_313]) ).
tcf(c_6438,plain,
! [X0: $i] : hAPP(fun(fun(X0,bool),bool),fun(X0,bool),the(fun(X0,bool)),hAPP(fun(X0,bool),fun(fun(X0,bool),bool),fequal(fun(X0,bool)),bot_bot(fun(X0,bool)))) = bot_bot(fun(X0,bool)),
inference(superposition,[status(thm)],[c_6123,c_1448]) ).
tcf(c_7879,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),X1,X2,hAPP(fun(X0,bool),fun(X0,bool),collect(X0),X3)) = hAPP(fun(X0,bool),X1,X2,X3),
inference(superposition,[status(thm)],[c_1528,c_1447]) ).
tcf(c_7880,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X1,fun(X0,bool),X2,X3)) = hAPP(X1,fun(X0,bool),X2,X3),
inference(superposition,[status(thm)],[c_1528,c_1448]) ).
tcf(c_7906,plain,
! [X0: $i] : hAPP(bool,fun(X0,bool),combk(bool,X0),fFalse) = bot_bot(fun(X0,bool)),
inference(demodulation,[status(thm)],[c_65,c_7880]) ).
tcf(c_7934,plain,
~ 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(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(demodulation,[status(thm)],[c_2108,c_7880]) ).
tcf(c_8388,plain,
~ 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(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),bot_bot(fun(state,bool)))),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(demodulation,[status(thm)],[c_7934,c_7906]) ).
tcf(c_8825,plain,
! [X0: $i,X1: $i] : hAPP(fun(bool,bool),bool,the(bool),hAPP(bool,fun(bool,bool),hAPP(fun(bool,fun(bool,bool)),fun(bool,fun(bool,bool)),combc(bool,bool,bool),fequal(bool)),fFalse)) = hAPP(X0,bool,bot_bot(fun(X0,bool)),X1),
inference(superposition,[status(thm)],[c_7906,c_102]) ).
tcf(c_9879,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(fun(X0,bool),X0,the(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(X2,X0,hAPP(X0,fun(X2,X0),combk(X0,X2),X1),X3),
inference(superposition,[status(thm)],[c_142,c_102]) ).
tcf(c_11166,plain,
! [X0: $i,X1: $i] : hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1) = hAPP(X0,fun(X0,bool),fequal(X0),X1),
inference(demodulation,[status(thm)],[c_1495,c_7880]) ).
tcf(c_12106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X2,sK14(X0,X1,X3,X4,X2)),sK15(X0,X1,X3,X4,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),X1),hAPP(hoare_509422987triple(X0),fun(hoare_509422987triple(X0),bool),fequal(hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_509422987triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_509422987triple(X0))),hoare_1008221573triple(X0),X2),X3),X4)))) ),
inference(demodulation,[status(thm)],[c_2354,c_7879]) ).
tcf(c_12135,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),bot_bot(fun(state,bool))),sK14(x_a,g,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)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),bot_bot(fun(state,bool))))),sK15(x_a,g,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)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),bot_bot(fun(state,bool)))))),
inference(superposition,[status(thm)],[c_12106,c_8388]) ).
tcf(c_13369,plain,
hBOOL(fFalse),
inference(demodulation,[status(thm)],[c_12135,c_1444,c_6438,c_8825,c_9879,c_11166]) ).
tcf(c_13370,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_13369,c_64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW470+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.18/0.44 % Computer : n001.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Thu Sep 24 22:35:54 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.18/0.50 Running first-order theorem proving
% 0.18/0.50 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.26/0.52
% 0.26/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.26/0.52
% 0.26/0.52 % Detected problem language: tptp
% 0.26/0.54 % Proving...
% 27.78/6.09 % SZS status Started for theBenchmark.p
% 27.78/6.09 % SZS status Theorem for theBenchmark.p
% 27.78/6.09
% 27.78/6.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 27.78/6.09
% 27.78/6.09 % ------ iProver source info
% 27.78/6.09
% 27.78/6.09 % git: date: 2026-07-19 20:42:38 +0200
% 27.78/6.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 27.78/6.09 % git: non_committed_changes: false
% 27.78/6.09
% 27.78/6.09 % ------ Parsing...
% 27.78/6.09 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 27.78/6.09
% 27.78/6.09 % ------ Preprocessing... sup_sim: 88 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 27.78/6.09
% 27.78/6.09 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 27.78/6.09
% 27.78/6.09 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 27.78/6.09 % ------ Proving...
% 27.78/6.09 % ------ Problem Properties
% 27.78/6.09
% 27.78/6.09 %
% 27.78/6.09 % clauses 141
% 27.78/6.09 % conjectures 0
% 27.78/6.09 % EPR 1
% 27.78/6.09 % Horn 101
% 27.78/6.09 % unary 44
% 27.78/6.09 % binary 53
% 27.78/6.09 % lits 302
% 27.78/6.09 % lits eq 109
% 27.78/6.09 % fd_pure 0
% 27.78/6.09 % fd_pseudo 0
% 27.78/6.09 % fd_cond 0
% 27.78/6.09 % fd_pseudo_cond 3
% 27.78/6.09 % AC symbols 0
% 27.78/6.09
% 27.78/6.09 % ------ Schedule dynamic 5 is on
% 27.78/6.09
% 27.78/6.09 % ------ no conjectures: strip conj schedule
% 27.78/6.09
% 27.78/6.09 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 27.78/6.09
% 27.78/6.09
% 27.78/6.09 % ------
% 27.78/6.09 % Current options:
% 27.78/6.09 % ------
% 27.78/6.09
% 27.78/6.09
% 27.78/6.09 %
% 27.78/6.09
% 27.78/6.09 % ------ Proving...
% 27.78/6.09 %
% 27.78/6.09
% 27.78/6.09 % SZS status Theorem for theBenchmark.p
% 27.78/6.09
% 27.78/6.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 27.78/6.09
% 27.78/6.09
%------------------------------------------------------------------------------