%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW470+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:09:11 PM UTC 2026
% Result : Theorem 0.48s 1.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n003.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 09:57:46 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.28/0.56 % Drodi V4.1.1
% 0.48/1.16 % Refutation found
% 0.48/1.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.48/1.16 % SZS output start CNFRefutation for theBenchmark
% 0.48/1.16 fof(f53,hypothesis,(
% 0.48/1.16 ti(bool,fFalse) = fFalse ),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f60,axiom,(
% 0.48/1.16 (! [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) )),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f74,axiom,(
% 0.48/1.16 (! [X_b,Ga,Ca,Q_1,Pa] :( (! [Z_2,S_2] :( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_2),S_2))=> hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(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_2))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_1,Z_2)))),bot_bot(fun(hoare_1656922687triple(X_b),bool))))) ))=> hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_1656922687triple(X_b),bool))))) ) )),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f608,axiom,(
% 0.48/1.16 (! [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) )),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f616,axiom,(
% 0.48/1.16 ~ hBOOL(fFalse) ),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f623,conjecture,(
% 0.48/1.16 hBOOL(hAPP(fun(hoare_1656922687triple(x_a),bool),bool,hAPP(fun(hoare_1656922687triple(x_a),bool),fun(fun(hoare_1656922687triple(x_a),bool),bool),hoare_279057269derivs(x_a),g),hAPP(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool),hAPP(hoare_1656922687triple(x_a),fun(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool)),insert(hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a))),hoare_246368825triple(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_1656922687triple(x_a),bool))))) ),
% 0.48/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.48/1.16 fof(f624,negated_conjecture,(
% 0.48/1.16 ~(hBOOL(hAPP(fun(hoare_1656922687triple(x_a),bool),bool,hAPP(fun(hoare_1656922687triple(x_a),bool),fun(fun(hoare_1656922687triple(x_a),bool),bool),hoare_279057269derivs(x_a),g),hAPP(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool),hAPP(hoare_1656922687triple(x_a),fun(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool)),insert(hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a))),hoare_246368825triple(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_1656922687triple(x_a),bool))))) )),
% 0.48/1.16 inference(negated_conjecture,[status(cth)],[f623])).
% 0.48/1.16 fof(f684,plain,(
% 0.48/1.16 ti(bool,fFalse)=fFalse),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f53])).
% 0.48/1.16 fof(f691,plain,(
% 0.48/1.16 ![X0,X1,X2,X3]: (hAPP(X0,X1,ti(fun(X0,X1),X2),X3)=hAPP(X0,X1,X2,X3))),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f60])).
% 0.48/1.16 fof(f719,plain,(
% 0.48/1.16 ![X_b,Ga,Ca,Q_1,Pa]: ((?[Z_2,S_2]: (hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_2),S_2))&~hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(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_2))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_1,Z_2)))),bot_bot(fun(hoare_1656922687triple(X_b),bool)))))))|hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_1656922687triple(X_b),bool))))))),
% 0.48/1.16 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.48/1.16 fof(f720,plain,(
% 0.48/1.16 ![X_b,Ga,Ca,Q_1,Pa]: ((hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,sK0_skl(Pa,Q_1,Ca,Ga,X_b)),sK1_skl(Pa,Q_1,Ca,Ga,X_b)))&~hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(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_1,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_1,sK0_skl(Pa,Q_1,Ca,Ga,X_b))))),bot_bot(fun(hoare_1656922687triple(X_b),bool))))))|hBOOL(hAPP(fun(hoare_1656922687triple(X_b),bool),bool,hAPP(fun(hoare_1656922687triple(X_b),bool),fun(fun(hoare_1656922687triple(X_b),bool),bool),hoare_279057269derivs(X_b),Ga),hAPP(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool),hAPP(hoare_1656922687triple(X_b),fun(fun(hoare_1656922687triple(X_b),bool),fun(hoare_1656922687triple(X_b),bool)),insert(hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_1656922687triple(X_b))),hoare_246368825triple(X_b),Pa),Ca),Q_1)),bot_bot(fun(hoare_1656922687triple(X_b),bool))))))),
% 0.48/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_2,sK0_skl(Pa,Q_1,Ca,Ga,X_b)),skolemize(S_2,sK1_skl(Pa,Q_1,Ca,Ga,X_b))],[f719])).
% 0.48/1.16 fof(f721,plain,(
% 0.48/1.16 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,sK0_skl(X1,X2,X3,X4,X0)),sK1_skl(X1,X2,X3,X4,X0)))|hBOOL(hAPP(fun(hoare_1656922687triple(X0),bool),bool,hAPP(fun(hoare_1656922687triple(X0),bool),fun(fun(hoare_1656922687triple(X0),bool),bool),hoare_279057269derivs(X0),X4),hAPP(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool),hAPP(hoare_1656922687triple(X0),fun(fun(hoare_1656922687triple(X0),bool),fun(hoare_1656922687triple(X0),bool)),insert(hoare_1656922687triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_1656922687triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_1656922687triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_1656922687triple(X0))),hoare_246368825triple(X0),X1),X3),X2)),bot_bot(fun(hoare_1656922687triple(X0),bool))))))),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f720])).
% 0.48/1.16 fof(f2175,plain,(
% 0.48/1.16 ![X0,X1,X2,X3]: (hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3)=ti(X1,X2))),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f608])).
% 0.48/1.16 fof(f2188,plain,(
% 0.48/1.16 ~hBOOL(fFalse)),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f616])).
% 0.48/1.16 fof(f2198,plain,(
% 0.48/1.16 ~hBOOL(hAPP(fun(hoare_1656922687triple(x_a),bool),bool,hAPP(fun(hoare_1656922687triple(x_a),bool),fun(fun(hoare_1656922687triple(x_a),bool),bool),hoare_279057269derivs(x_a),g),hAPP(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool),hAPP(hoare_1656922687triple(x_a),fun(fun(hoare_1656922687triple(x_a),bool),fun(hoare_1656922687triple(x_a),bool)),insert(hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_1656922687triple(x_a))),hoare_246368825triple(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_1656922687triple(x_a),bool)))))),
% 0.48/1.16 inference(cnf_transformation,[status(thm)],[f624])).
% 0.48/1.16 fof(f3171,plain,(
% 0.48/1.16 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,g,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,g,x_a)))),
% 0.48/1.16 inference(resolution,[status(thm)],[f721,f2198])).
% 0.48/1.18 fof(f3182,plain,(
% 0.48/1.18 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,g,x_a)))),
% 0.48/1.18 inference(forward_demodulation,[status(thm)],[f2175,f3171])).
% 0.48/1.18 fof(f3183,plain,(
% 0.48/1.18 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,g,x_a)))),
% 0.48/1.18 inference(forward_demodulation,[status(thm)],[f691,f3182])).
% 0.48/1.18 fof(f3184,plain,(
% 0.48/1.18 hBOOL(ti(bool,fFalse))),
% 0.48/1.18 inference(forward_demodulation,[status(thm)],[f2175,f3183])).
% 0.48/1.18 fof(f3185,plain,(
% 0.48/1.18 hBOOL(fFalse)),
% 0.48/1.18 inference(forward_demodulation,[status(thm)],[f684,f3184])).
% 0.48/1.18 fof(f3186,plain,(
% 0.48/1.18 $false),
% 0.48/1.18 inference(forward_subsumption_resolution,[status(thm)],[f3185,f2188])).
% 0.48/1.18 % SZS output end CNFRefutation for theBenchmark.p
% 0.57/1.22 % Elapsed time: 0.854907 seconds
% 0.57/1.22 % CPU time: 5.044287 seconds
% 0.57/1.22 % Total memory used: 297.154 MB
% 0.57/1.22 % Net memory used: 294.629 MB
%------------------------------------------------------------------------------